Certified arcsine potential bounds (U55)

theorem Zeta5Irrational.U_664_1 : Uω (aρ 1) (bρ 1) (199912686621581 / 256000000000000) ≤ -(1277964907620946027673 / 5000000000000000000000)

theorem Zeta5Irrational.U_664_2 : Uω (aρ 2) (bρ 2) (199912686621581 / 256000000000000) ≤ -(103472765751352777257 / 400000000000000000000)

theorem Zeta5Irrational.U_664_3 : Uω (aρ 3) (bρ 3) (199912686621581 / 256000000000000) ≤ -(2648846011764422714851 / 10000000000000000000000)

theorem Zeta5Irrational.U_664_4 : Uω (aρ 4) (bρ 4) (199912686621581 / 256000000000000) ≤ -(2752598967989138191723 / 10000000000000000000000)

theorem Zeta5Irrational.U_664_5 : Uω (aρ 5) (bρ 5) (199912686621581 / 256000000000000) ≤ -(291237749004709474387 / 1000000000000000000000)

theorem Zeta5Irrational.U_664_6 : Uω (aρ 6) (bρ 6) (199912686621581 / 256000000000000) ≤ -(3145329015573109930877 / 10000000000000000000000)

theorem Zeta5Irrational.U_664_7 : Uω (aρ 7) (bρ 7) (199912686621581 / 256000000000000) ≤ -(3470509010608891617659 / 10000000000000000000000)

theorem Zeta5Irrational.U_664_8 : Uω (aρ 8) (bρ 8) (199912686621581 / 256000000000000) ≤ -(1953955403703193484059 / 5000000000000000000000)

theorem Zeta5Irrational.U_664_9 : Uω (aρ 9) (bρ 9) (199912686621581 / 256000000000000) ≤ -(4477459106514180083733 / 10000000000000000000000)

theorem Zeta5Irrational.U_664_10 : Uω (aρ 10) (bρ 10) (199912686621581 / 256000000000000) ≤ -(1299476206458049317223 / 2500000000000000000000)

theorem Zeta5Irrational.U_664_11 : Uω (aρ 11) (bρ 11) (199912686621581 / 256000000000000) ≤ -(6085421088558797644903 / 10000000000000000000000)

theorem Zeta5Irrational.U_664_12 : Uω (aρ 12) (bρ 12) (199912686621581 / 256000000000000) ≤ -(3575650047906401257211 / 5000000000000000000000)

theorem Zeta5Irrational.U_664_13 : Uω (aρ 13) (bρ 13) (199912686621581 / 256000000000000) ≤ -(4198484460239256737569 / 5000000000000000000000)

theorem Zeta5Irrational.U_664_14 : Uω (aρ 14) (bρ 14) (199912686621581 / 256000000000000) ≤ -(1960132106122831270009 / 2000000000000000000000)

theorem Zeta5Irrational.U_664_15 : Uω (aρ 15) (bρ 15) (199912686621581 / 256000000000000) ≤ -(225512837703902044943 / 200000000000000000000)

theorem Zeta5Irrational.U_664_16 : Uω (aρ 16) (bρ 16) (199912686621581 / 256000000000000) ≤ -(1253266360243979778637 / 1000000000000000000000)

theorem Zeta5Irrational.U_664 : Uρ (199912686621581 / 256000000000000) ≤ -(4636648990333002156281 / 10000000000000000000000)

theorem Zeta5Irrational.U_665_1 : Uω (aρ 1) (bρ 1) (25145756165739 / 32000000000000) ≤ -(249291082670160325427 / 1000000000000000000000)

theorem Zeta5Irrational.U_665_2 : Uω (aρ 2) (bρ 2) (25145756165739 / 32000000000000) ≤ -(252360486208296023661 / 1000000000000000000000)

theorem Zeta5Irrational.U_665_3 : Uω (aρ 3) (bρ 3) (25145756165739 / 32000000000000) ≤ -(2585236824123272191887 / 10000000000000000000000)

theorem Zeta5Irrational.U_665_4 : Uω (aρ 4) (bρ 4) (25145756165739 / 32000000000000) ≤ -(1344160446545207092199 / 5000000000000000000000)

theorem Zeta5Irrational.U_665_5 : Uω (aρ 5) (bρ 5) (25145756165739 / 32000000000000) ≤ -(355881058895171594713 / 1250000000000000000000)

theorem Zeta5Irrational.U_665_6 : Uω (aρ 6) (bρ 6) (25145756165739 / 32000000000000) ≤ -(3078420738767238145273 / 10000000000000000000000)

theorem Zeta5Irrational.U_665_7 : Uω (aρ 7) (bρ 7) (25145756165739 / 32000000000000) ≤ -(340129780488928500307 / 1000000000000000000000)

theorem Zeta5Irrational.U_665_8 : Uω (aρ 8) (bρ 8) (25145756165739 / 32000000000000) ≤ -(3835406704026617134509 / 10000000000000000000000)

theorem Zeta5Irrational.U_665_9 : Uω (aρ 9) (bρ 9) (25145756165739 / 32000000000000) ≤ -(4400294372036981046643 / 10000000000000000000000)

theorem Zeta5Irrational.U_665_10 : Uω (aρ 10) (bρ 10) (25145756165739 / 32000000000000) ≤ -(2557073977047964558419 / 5000000000000000000000)

theorem Zeta5Irrational.U_665_11 : Uω (aρ 11) (bρ 11) (25145756165739 / 32000000000000) ≤ -(5992249965690502151559 / 10000000000000000000000)

theorem Zeta5Irrational.U_665_12 : Uω (aρ 12) (bρ 12) (25145756165739 / 32000000000000) ≤ -(1408879486035550407403 / 2000000000000000000000)

theorem Zeta5Irrational.U_665_13 : Uω (aρ 13) (bρ 13) (25145756165739 / 32000000000000) ≤ -(4134674394368595173987 / 5000000000000000000000)

theorem Zeta5Irrational.U_665_14 : Uω (aρ 14) (bρ 14) (25145756165739 / 32000000000000) ≤ -(9640365382064048121153 / 10000000000000000000000)

theorem Zeta5Irrational.U_665_15 : Uω (aρ 15) (bρ 15) (25145756165739 / 32000000000000) ≤ -(442487964087878460311 / 400000000000000000000)

theorem Zeta5Irrational.U_665_16 : Uω (aρ 16) (bρ 16) (25145756165739 / 32000000000000) ≤ -(12243810141211648147373 / 10000000000000000000000)

theorem Zeta5Irrational.U_665 : Uρ (25145756165739 / 32000000000000) ≤ -(4553883503740599041333 / 10000000000000000000000)

theorem Zeta5Irrational.U_666_1 : Uω (aρ 1) (bρ 1) (202419412030243 / 256000000000000) ≤ -(2430286493772126347773 / 10000000000000000000000)

theorem Zeta5Irrational.U_666_2 : Uω (aρ 2) (bρ 2) (202419412030243 / 256000000000000) ≤ -(49215753797925468473 / 200000000000000000000)

theorem Zeta5Irrational.U_666_3 : Uω (aρ 3) (bρ 3) (202419412030243 / 256000000000000) ≤ -(1261014871413616783293 / 5000000000000000000000)

theorem Zeta5Irrational.U_666_4 : Uω (aρ 4) (bρ 4) (202419412030243 / 256000000000000) ≤ -(656113373712938037237 / 2500000000000000000000)

theorem Zeta5Irrational.U_666_5 : Uω (aρ 5) (bρ 5) (202419412030243 / 256000000000000) ≤ -(1391071934225770335259 / 5000000000000000000000)

theorem Zeta5Irrational.U_666_6 : Uω (aρ 6) (bρ 6) (202419412030243 / 256000000000000) ≤ -(1505979082273865270421 / 5000000000000000000000)

theorem Zeta5Irrational.U_666_7 : Uω (aρ 7) (bρ 7) (202419412030243 / 256000000000000) ≤ -(208285297068072753121 / 625000000000000000000)

theorem Zeta5Irrational.U_666_8 : Uω (aρ 8) (bρ 8) (202419412030243 / 256000000000000) ≤ -(37634301630337236271 / 100000000000000000000)

theorem Zeta5Irrational.U_666_9 : Uω (aρ 9) (bρ 9) (202419412030243 / 256000000000000) ≤ -(864746693025047178221 / 2000000000000000000000)

theorem Zeta5Irrational.U_666_10 : Uω (aρ 10) (bρ 10) (202419412030243 / 256000000000000) ≤ -(31444476630483468137 / 62500000000000000000)

theorem Zeta5Irrational.U_666_11 : Uω (aρ 11) (bρ 11) (202419412030243 / 256000000000000) ≤ -(2950003497771861187207 / 5000000000000000000000)

theorem Zeta5Irrational.U_666_12 : Uω (aρ 12) (bρ 12) (202419412030243 / 256000000000000) ≤ -(3469394193332567164563 / 5000000000000000000000)

theorem Zeta5Irrational.U_666_13 : Uω (aρ 13) (bρ 13) (202419412030243 / 256000000000000) ≤ -(8143751499644154206229 / 10000000000000000000000)

theorem Zeta5Irrational.U_666_14 : Uω (aρ 14) (bρ 14) (202419412030243 / 256000000000000) ≤ -(9483755677962245212443 / 10000000000000000000000)

theorem Zeta5Irrational.U_666_15 : Uω (aρ 15) (bρ 15) (202419412030243 / 256000000000000) ≤ -(5428388530800015652507 / 5000000000000000000000)

theorem Zeta5Irrational.U_666_16 : Uω (aρ 16) (bρ 16) (202419412030243 / 256000000000000) ≤ -(748334846524065932333 / 625000000000000000000)

theorem Zeta5Irrational.U_666 : Uρ (202419412030243 / 256000000000000) ≤ -(4472242976673732246981 / 10000000000000000000000)

theorem Zeta5Irrational.U_667_1 : Uω (aρ 1) (bρ 1) (101836387367287 / 128000000000000) ≤ -(1184025952061820073691 / 5000000000000000000000)

theorem Zeta5Irrational.U_667_2 : Uω (aρ 2) (bρ 2) (101836387367287 / 128000000000000) ≤ -(149897666808250901199 / 625000000000000000000)

theorem Zeta5Irrational.U_667_3 : Uω (aρ 3) (bρ 3) (101836387367287 / 128000000000000) ≤ -(2459219715338930544141 / 10000000000000000000000)

theorem Zeta5Irrational.U_667_4 : Uω (aρ 4) (bρ 4) (101836387367287 / 128000000000000) ≤ -(2560991557050394938723 / 10000000000000000000000)

theorem Zeta5Irrational.U_667_5 : Uω (aρ 5) (bρ 5) (101836387367287 / 128000000000000) ≤ -(1358829098960116310293 / 5000000000000000000000)

theorem Zeta5Irrational.U_667_6 : Uω (aρ 6) (bρ 6) (101836387367287 / 128000000000000) ≤ -(2945935381077970403423 / 10000000000000000000000)

theorem Zeta5Irrational.U_667_7 : Uω (aρ 7) (bρ 7) (101836387367287 / 128000000000000) ≤ -(130572130440057185229 / 400000000000000000000)

theorem Zeta5Irrational.U_667_8 : Uω (aρ 8) (bρ 8) (101836387367287 / 128000000000000) ≤ -(1845986741144000437987 / 5000000000000000000000)

theorem Zeta5Irrational.U_667_9 : Uω (aρ 9) (bρ 9) (101836387367287 / 128000000000000) ≤ -(2123883406626890648073 / 5000000000000000000000)

theorem Zeta5Irrational.U_667_10 : Uω (aρ 10) (bρ 10) (101836387367287 / 128000000000000) ≤ -(618599601174517764213 / 1250000000000000000000)

theorem Zeta5Irrational.U_667_11 : Uω (aρ 11) (bρ 11) (101836387367287 / 128000000000000) ≤ -(1452168150311807516473 / 2500000000000000000000)

theorem Zeta5Irrational.U_667_12 : Uω (aρ 12) (bρ 12) (101836387367287 / 128000000000000) ≤ -(6834438478415439925663 / 10000000000000000000000)

theorem Zeta5Irrational.U_667_13 : Uω (aρ 13) (bρ 13) (101836387367287 / 128000000000000) ≤ -(802010272264151745109 / 1000000000000000000000)

theorem Zeta5Irrational.U_667_14 : Uω (aρ 14) (bρ 14) (101836387367287 / 128000000000000) ≤ -(4665312136517286567177 / 5000000000000000000000)

theorem Zeta5Irrational.U_667_15 : Uω (aρ 15) (bρ 15) (101836387367287 / 128000000000000) ≤ -(10658612229026117417291 / 10000000000000000000000)

theorem Zeta5Irrational.U_667_16 : Uω (aρ 16) (bρ 16) (101836387367287 / 128000000000000) ≤ -(5859174174619187689721 / 5000000000000000000000)

theorem Zeta5Irrational.U_667 : Uρ (101836387367287 / 128000000000000) ≤ -(1097916055907063284131 / 2500000000000000000000)

theorem Zeta5Irrational.U_668_1 : Uω (aρ 1) (bρ 1) (40985227487781 / 51200000000000) ≤ -(28827527957205322453 / 125000000000000000000)

theorem Zeta5Irrational.U_668_2 : Uω (aρ 2) (bρ 2) (40985227487781 / 51200000000000) ≤ -(46726498663784903531 / 200000000000000000000)

theorem Zeta5Irrational.U_668_3 : Uω (aρ 3) (bρ 3) (40985227487781 / 51200000000000) ≤ -(2396801783767159707439 / 10000000000000000000000)

theorem Zeta5Irrational.U_668_4 : Uω (aρ 4) (bρ 4) (40985227487781 / 51200000000000) ≤ -(312241245281524448941 / 1250000000000000000000)

theorem Zeta5Irrational.U_668_5 : Uω (aρ 5) (bρ 5) (40985227487781 / 51200000000000) ≤ -(663396520318592504421 / 2500000000000000000000)

theorem Zeta5Irrational.U_668_6 : Uω (aρ 6) (bρ 6) (40985227487781 / 51200000000000) ≤ -(115213863744958042733 / 400000000000000000000)

theorem Zeta5Irrational.U_668_7 : Uω (aρ 7) (bρ 7) (40985227487781 / 51200000000000) ≤ -(3196506870553017259521 / 10000000000000000000000)

theorem Zeta5Irrational.U_668_8 : Uω (aρ 8) (bρ 8) (40985227487781 / 51200000000000) ≤ -(3621029128780322054959 / 10000000000000000000000)

theorem Zeta5Irrational.U_668_9 : Uω (aρ 9) (bρ 9) (40985227487781 / 51200000000000) ≤ -(2086192537048560607821 / 5000000000000000000000)

theorem Zeta5Irrational.U_668_10 : Uω (aρ 10) (bρ 10) (40985227487781 / 51200000000000) ≤ -(4867177017714833062951 / 10000000000000000000000)

theorem Zeta5Irrational.U_668_11 : Uω (aρ 11) (bρ 11) (40985227487781 / 51200000000000) ≤ -(571822785259138887833 / 1000000000000000000000)

theorem Zeta5Irrational.U_668_12 : Uω (aρ 12) (bρ 12) (40985227487781 / 51200000000000) ≤ -(420707167491835697151 / 625000000000000000000)

theorem Zeta5Irrational.U_668_13 : Uω (aρ 13) (bρ 13) (40985227487781 / 51200000000000) ≤ -(1579666510826825980323 / 2000000000000000000000)

theorem Zeta5Irrational.U_668_14 : Uω (aρ 14) (bρ 14) (40985227487781 / 51200000000000) ≤ -(1836156577461968690781 / 2000000000000000000000)

theorem Zeta5Irrational.U_668_15 : Uω (aρ 15) (bρ 15) (40985227487781 / 51200000000000) ≤ -(5233528120475439557461 / 5000000000000000000000)

theorem Zeta5Irrational.U_668_16 : Uω (aρ 16) (bρ 16) (40985227487781 / 51200000000000) ≤ -(11476547035735173474157 / 10000000000000000000000)

theorem Zeta5Irrational.U_668 : Uρ (40985227487781 / 51200000000000) ≤ -(431209322955317224327 / 1000000000000000000000)

theorem Zeta5Irrational.U_669_1 : Uω (aρ 1) (bρ 1) (51544875035809 / 64000000000000) ≤ -(2244732758859609584141 / 10000000000000000000000)

theorem Zeta5Irrational.U_669_2 : Uω (aρ 2) (bρ 2) (51544875035809 / 64000000000000) ≤ -(227466970668141009613 / 1000000000000000000000)

theorem Zeta5Irrational.U_669_3 : Uω (aρ 3) (bρ 3) (51544875035809 / 64000000000000) ≤ -(2334771082517334658739 / 10000000000000000000000)

theorem Zeta5Irrational.U_669_4 : Uω (aρ 4) (bρ 4) (51544875035809 / 64000000000000) ≤ -(304407961166478728341 / 1250000000000000000000)

theorem Zeta5Irrational.U_669_5 : Uω (aρ 5) (bρ 5) (51544875035809 / 64000000000000) ≤ -(647480560805871238739 / 2500000000000000000000)

theorem Zeta5Irrational.U_669_6 : Uω (aρ 6) (bρ 6) (51544875035809 / 64000000000000) ≤ -(87974566296101048461 / 312500000000000000000)

theorem Zeta5Irrational.U_669_7 : Uω (aρ 7) (bρ 7) (51544875035809 / 64000000000000) ≤ -(391146157008232414821 / 1250000000000000000000)

theorem Zeta5Irrational.U_669_8 : Uω (aρ 8) (bρ 8) (51544875035809 / 64000000000000) ≤ -(355058973366974848083 / 1000000000000000000000)

theorem Zeta5Irrational.U_669_9 : Uω (aρ 9) (bρ 9) (51544875035809 / 64000000000000) ≤ -(1024394782019966389091 / 2500000000000000000000)

theorem Zeta5Irrational.U_669_10 : Uω (aρ 10) (bρ 10) (51544875035809 / 64000000000000) ≤ -(11965611613780661111 / 25000000000000000000)

theorem Zeta5Irrational.U_669_11 : Uω (aρ 11) (bρ 11) (51544875035809 / 64000000000000) ≤ -(5628654436701494422077 / 10000000000000000000000)

theorem Zeta5Irrational.U_669_12 : Uω (aρ 12) (bρ 12) (51544875035809 / 64000000000000) ≤ -(6629385355911510922651 / 10000000000000000000000)

theorem Zeta5Irrational.U_669_13 : Uω (aρ 13) (bρ 13) (51544875035809 / 64000000000000) ≤ -(972296894257070220027 / 1250000000000000000000)

theorem Zeta5Irrational.U_669_14 : Uω (aρ 14) (bρ 14) (51544875035809 / 64000000000000) ≤ -(9034059768671761378607 / 10000000000000000000000)

theorem Zeta5Irrational.U_669_15 : Uω (aρ 15) (bρ 15) (51544875035809 / 64000000000000) ≤ -(10281552864863602885801 / 10000000000000000000000)

theorem Zeta5Irrational.U_669_16 : Uω (aρ 16) (bρ 16) (51544875035809 / 64000000000000) ≤ -(5623107287608835128659 / 5000000000000000000000)

theorem Zeta5Irrational.U_669 : Uρ (51544875035809 / 64000000000000) ≤ -(4233482968561500353719 / 10000000000000000000000)

theorem Zeta5Irrational.U_670_1 : Uω (aρ 1) (bρ 1) (104343112775949 / 128000000000000) ≤ -(2122915875407152198241 / 10000000000000000000000)

theorem Zeta5Irrational.U_670_2 : Uω (aρ 2) (bρ 2) (104343112775949 / 128000000000000) ≤ -(2152488114323455304571 / 10000000000000000000000)

theorem Zeta5Irrational.U_670_3 : Uω (aρ 3) (bρ 3) (104343112775949 / 128000000000000) ≤ -(2211852356495572801771 / 10000000000000000000000)

theorem Zeta5Irrational.U_670_4 : Uω (aρ 4) (bρ 4) (104343112775949 / 128000000000000) ≤ -(23110974918272984411 / 100000000000000000000)

theorem Zeta5Irrational.U_670_5 : Uω (aρ 5) (bρ 5) (104343112775949 / 128000000000000) ≤ -(2463798801145355917777 / 10000000000000000000000)

theorem Zeta5Irrational.U_670_6 : Uω (aρ 6) (bρ 6) (104343112775949 / 128000000000000) ≤ -(671531988149197401087 / 2500000000000000000000)

theorem Zeta5Irrational.U_670_7 : Uω (aρ 7) (bρ 7) (104343112775949 / 128000000000000) ≤ -(1497922846347504928719 / 5000000000000000000000)

theorem Zeta5Irrational.U_670_8 : Uω (aρ 8) (bρ 8) (104343112775949 / 128000000000000) ≤ -(426399641951322608969 / 1250000000000000000000)

theorem Zeta5Irrational.U_670_9 : Uω (aρ 9) (bρ 9) (104343112775949 / 128000000000000) ≤ -(3949659208324676186013 / 10000000000000000000000)

theorem Zeta5Irrational.U_670_10 : Uω (aρ 10) (bρ 10) (104343112775949 / 128000000000000) ≤ -(4626394831317498006823 / 10000000000000000000000)

theorem Zeta5Irrational.U_670_11 : Uω (aρ 11) (bρ 11) (104343112775949 / 128000000000000) ≤ -(2726025637081969480721 / 5000000000000000000000)

theorem Zeta5Irrational.U_670_12 : Uω (aρ 12) (bρ 12) (104343112775949 / 128000000000000) ≤ -(1607247505027276502399 / 2500000000000000000000)

theorem Zeta5Irrational.U_670_13 : Uω (aρ 13) (bρ 13) (104343112775949 / 128000000000000) ≤ -(7543653695001394939451 / 10000000000000000000000)

theorem Zeta5Irrational.U_670_14 : Uω (aρ 14) (bρ 14) (104343112775949 / 128000000000000) ≤ -(8749352398163579758549 / 10000000000000000000000)

theorem Zeta5Irrational.U_670_15 : Uω (aρ 15) (bρ 15) (104343112775949 / 128000000000000) ≤ -(2481709788466278231419 / 2500000000000000000000)

theorem Zeta5Irrational.U_670_16 : Uω (aρ 16) (bρ 16) (104343112775949 / 128000000000000) ≤ -(1081467769326687780553 / 1000000000000000000000)

theorem Zeta5Irrational.U_670 : Uρ (104343112775949 / 128000000000000) ≤ -(32631863470159351417 / 80000000000000000000)

theorem Zeta5Irrational.U_671_1 : Uω (aρ 1) (bρ 1) (2639911887007 / 3200000000000) ≤ -(500641273210134050889 / 2500000000000000000000)

theorem Zeta5Irrational.U_671_2 : Uω (aρ 2) (bρ 2) (2639911887007 / 3200000000000) ≤ -(1015890701030451598891 / 5000000000000000000000)

theorem Zeta5Irrational.U_671_3 : Uω (aρ 3) (bρ 3) (2639911887007 / 3200000000000) ≤ -(1045213186822443644979 / 5000000000000000000000)

theorem Zeta5Irrational.U_671_4 : Uω (aρ 4) (bρ 4) (2639911887007 / 3200000000000) ≤ -(2188454632258100397817 / 10000000000000000000000)

theorem Zeta5Irrational.U_671_5 : Uω (aρ 5) (bρ 5) (2639911887007 / 3200000000000) ≤ -(2339247632052252958919 / 10000000000000000000000)

theorem Zeta5Irrational.U_671_6 : Uω (aρ 6) (bρ 6) (2639911887007 / 3200000000000) ≤ -(127935879922268966083 / 500000000000000000000)

theorem Zeta5Irrational.U_671_7 : Uω (aρ 7) (bρ 7) (2639911887007 / 3200000000000) ≤ -(143214223958901012311 / 500000000000000000000)

theorem Zeta5Irrational.U_671_8 : Uω (aρ 8) (bρ 8) (2639911887007 / 3200000000000) ≤ -(3273739843396933459351 / 10000000000000000000000)

theorem Zeta5Irrational.U_671_9 : Uω (aρ 9) (bρ 9) (2639911887007 / 3200000000000) ≤ -(3803938287939391401999 / 10000000000000000000000)

theorem Zeta5Irrational.U_671_10 : Uω (aρ 10) (bρ 10) (2639911887007 / 3200000000000) ≤ -(4469155812153975488917 / 10000000000000000000000)

theorem Zeta5Irrational.U_671_11 : Uω (aρ 11) (bρ 11) (2639911887007 / 3200000000000) ≤ -(5278727945726234280523 / 10000000000000000000000)

theorem Zeta5Irrational.U_671_12 : Uω (aρ 12) (bρ 12) (2639911887007 / 3200000000000) ≤ -(1558256031449427925669 / 2500000000000000000000)

theorem Zeta5Irrational.U_671_13 : Uω (aρ 13) (bρ 13) (2639911887007 / 3200000000000) ≤ -(7315481309970044122373 / 10000000000000000000000)

theorem Zeta5Irrational.U_671_14 : Uω (aρ 14) (bρ 14) (2639911887007 / 3200000000000) ≤ -(132427977383954035777 / 156250000000000000000)

theorem Zeta5Irrational.U_671_15 : Uω (aρ 15) (bρ 15) (2639911887007 / 3200000000000) ≤ -(4795647034182452320199 / 5000000000000000000000)

theorem Zeta5Irrational.U_671_16 : Uω (aρ 16) (bρ 16) (2639911887007 / 3200000000000) ≤ -(10415420626330915702817 / 10000000000000000000000)

theorem Zeta5Irrational.U_671 : Uρ (2639911887007 / 3200000000000) ≤ -(122746261948983473009 / 312500000000000000000)

theorem Zeta5Irrational.U_672_1 : Uω (aρ 1) (bρ 1) (106849838184611 / 128000000000000) ≤ -(235455692546499870873 / 1250000000000000000000)

theorem Zeta5Irrational.U_672_2 : Uω (aρ 2) (bρ 2) (106849838184611 / 128000000000000) ≤ -(191251438587919057173 / 1000000000000000000000)

theorem Zeta5Irrational.U_672_3 : Uω (aρ 3) (bρ 3) (106849838184611 / 128000000000000) ≤ -(123153581774262376029 / 625000000000000000000)

theorem Zeta5Irrational.U_672_4 : Uω (aρ 4) (bρ 4) (106849838184611 / 128000000000000) ≤ -(413459634607695491819 / 2000000000000000000000)

theorem Zeta5Irrational.U_672_5 : Uω (aρ 5) (bρ 5) (106849838184611 / 128000000000000) ≤ -(2216229985259282885979 / 10000000000000000000000)

theorem Zeta5Irrational.U_672_6 : Uω (aρ 6) (bρ 6) (106849838184611 / 128000000000000) ≤ -(486582685306763027307 / 2000000000000000000000)

theorem Zeta5Irrational.U_672_7 : Uω (aρ 7) (bρ 7) (106849838184611 / 128000000000000) ≤ -(341804927920539353553 / 1250000000000000000000)

theorem Zeta5Irrational.U_672_8 : Uω (aρ 8) (bρ 8) (106849838184611 / 128000000000000) ≤ -(3138164350541981558903 / 10000000000000000000000)

theorem Zeta5Irrational.U_672_9 : Uω (aρ 9) (bρ 9) (106849838184611 / 128000000000000) ≤ -(915087684084109970181 / 2500000000000000000000)

theorem Zeta5Irrational.U_672_10 : Uω (aρ 10) (bρ 10) (106849838184611 / 128000000000000) ≤ -(2157220375553611875821 / 5000000000000000000000)

theorem Zeta5Irrational.U_672_11 : Uω (aρ 11) (bρ 11) (106849838184611 / 128000000000000) ≤ -(2554278773373393057629 / 5000000000000000000000)

theorem Zeta5Irrational.U_672_12 : Uω (aρ 12) (bρ 12) (106849838184611 / 128000000000000) ≤ -(188789903102745975883 / 312500000000000000000)

theorem Zeta5Irrational.U_672_13 : Uω (aρ 13) (bρ 13) (106849838184611 / 128000000000000) ≤ -(1773362058072074792879 / 2500000000000000000000)

theorem Zeta5Irrational.U_672_14 : Uω (aρ 14) (bρ 14) (106849838184611 / 128000000000000) ≤ -(8211227049645739158739 / 10000000000000000000000)

theorem Zeta5Irrational.U_672_15 : Uω (aρ 15) (bρ 15) (106849838184611 / 128000000000000) ≤ -(1854487086372971585059 / 2000000000000000000000)

theorem Zeta5Irrational.U_672_16 : Uω (aρ 16) (bρ 16) (106849838184611 / 128000000000000) ≤ -(10042650893961810327003 / 10000000000000000000000)

theorem Zeta5Irrational.U_672 : Uρ (106849838184611 / 128000000000000) ≤ -(3779941234837194175711 / 10000000000000000000000)

theorem Zeta5Irrational.U_673_1 : Uω (aρ 1) (bρ 1) (54051600444471 / 64000000000000) ≤ -(441530894174971766827 / 2500000000000000000000)

theorem Zeta5Irrational.U_673_2 : Uω (aρ 2) (bρ 2) (54051600444471 / 64000000000000) ≤ -(358930625195043976947 / 2000000000000000000000)

theorem Zeta5Irrational.U_673_3 : Uω (aρ 3) (bρ 3) (54051600444471 / 64000000000000) ≤ -(1851910609720033326851 / 10000000000000000000000)

theorem Zeta5Irrational.U_673_4 : Uω (aρ 4) (bρ 4) (54051600444471 / 64000000000000) ≤ -(973796252202356616109 / 5000000000000000000000)

theorem Zeta5Irrational.U_673_5 : Uω (aρ 5) (bρ 5) (54051600444471 / 64000000000000) ≤ -(1047354263203227591767 / 5000000000000000000000)

theorem Zeta5Irrational.U_673_6 : Uω (aρ 6) (bρ 6) (54051600444471 / 64000000000000) ≤ -(2308675365543395899577 / 10000000000000000000000)

theorem Zeta5Irrational.U_673_7 : Uω (aρ 7) (bρ 7) (54051600444471 / 64000000000000) ≤ -(2606266133502291094023 / 10000000000000000000000)

theorem Zeta5Irrational.U_673_8 : Uω (aρ 8) (bρ 8) (54051600444471 / 64000000000000) ≤ -(375552419867593022027 / 1250000000000000000000)

theorem Zeta5Irrational.U_673_9 : Uω (aρ 9) (bρ 9) (54051600444471 / 64000000000000) ≤ -(3518833867664006306331 / 10000000000000000000000)

theorem Zeta5Irrational.U_673_10 : Uω (aρ 10) (bρ 10) (54051600444471 / 64000000000000) ≤ -(4162167202080293224863 / 10000000000000000000000)

theorem Zeta5Irrational.U_673_11 : Uω (aρ 11) (bρ 11) (54051600444471 / 64000000000000) ≤ -(4941420751005724572059 / 10000000000000000000000)

theorem Zeta5Irrational.U_673_12 : Uω (aρ 12) (bρ 12) (54051600444471 / 64000000000000) ≤ -(1463388324566729199727 / 2500000000000000000000)

theorem Zeta5Irrational.U_673_13 : Uω (aρ 13) (bρ 13) (54051600444471 / 64000000000000) ≤ -(687718534739097609481 / 1000000000000000000000)

theorem Zeta5Irrational.U_673_14 : Uω (aρ 14) (bρ 14) (54051600444471 / 64000000000000) ≤ -(994505843548616338199 / 1250000000000000000000)

theorem Zeta5Irrational.U_673_15 : Uω (aρ 15) (bρ 15) (54051600444471 / 64000000000000) ≤ -(8968279189791174831113 / 10000000000000000000000)

theorem Zeta5Irrational.U_673_16 : Uω (aρ 16) (bρ 16) (54051600444471 / 64000000000000) ≤ -(387685589835395029451 / 400000000000000000000)

theorem Zeta5Irrational.U_673 : Uρ (54051600444471 / 64000000000000) ≤ -(363496725301935166593 / 1000000000000000000000)

theorem Zeta5Irrational.U_674_1 : Uω (aρ 1) (bρ 1) (27652481574401 / 32000000000000) ≤ -(383785914618737645777 / 2500000000000000000000)

theorem Zeta5Irrational.U_674_2 : Uω (aρ 2) (bρ 2) (27652481574401 / 32000000000000) ≤ -(48844312258711844961 / 312500000000000000000)

theorem Zeta5Irrational.U_674_3 : Uω (aρ 3) (bρ 3) (27652481574401 / 32000000000000) ≤ -(404738031473057972023 / 2500000000000000000000)

theorem Zeta5Irrational.U_674_4 : Uω (aρ 4) (bρ 4) (27652481574401 / 32000000000000) ≤ -(342479473035474896289 / 2000000000000000000000)

theorem Zeta5Irrational.U_674_5 : Uω (aρ 5) (bρ 5) (27652481574401 / 32000000000000) ≤ -(185601151129559812207 / 1000000000000000000000)

theorem Zeta5Irrational.U_674_6 : Uω (aρ 6) (bρ 6) (27652481574401 / 32000000000000) ≤ -(1032372319093198975119 / 5000000000000000000000)

theorem Zeta5Irrational.U_674_7 : Uω (aρ 7) (bρ 7) (27652481574401 / 32000000000000) ≤ -(1177382868026010592239 / 5000000000000000000000)

theorem Zeta5Irrational.U_674_8 : Uω (aρ 8) (bρ 8) (27652481574401 / 32000000000000) ≤ -(2742226011902361903109 / 10000000000000000000000)

theorem Zeta5Irrational.U_674_9 : Uω (aρ 9) (bρ 9) (27652481574401 / 32000000000000) ≤ -(129671004603477111227 / 400000000000000000000)

theorem Zeta5Irrational.U_674_10 : Uω (aρ 10) (bρ 10) (27652481574401 / 32000000000000) ≤ -(483079380526028675361 / 1250000000000000000000)

theorem Zeta5Irrational.U_674_11 : Uω (aρ 11) (bρ 11) (27652481574401 / 32000000000000) ≤ -(576975617282524960421 / 1250000000000000000000)

theorem Zeta5Irrational.U_674_12 : Uω (aρ 12) (bρ 12) (27652481574401 / 32000000000000) ≤ -(2744733037009107092033 / 5000000000000000000000)

theorem Zeta5Irrational.U_674_13 : Uω (aρ 13) (bρ 13) (27652481574401 / 32000000000000) ≤ -(3230332515999585509361 / 5000000000000000000000)

theorem Zeta5Irrational.U_674_14 : Uω (aρ 14) (bρ 14) (27652481574401 / 32000000000000) ≤ -(298795737915287152287 / 400000000000000000000)

theorem Zeta5Irrational.U_674_15 : Uω (aρ 15) (bρ 15) (27652481574401 / 32000000000000) ≤ -(2099471820989259101859 / 2500000000000000000000)

theorem Zeta5Irrational.U_674_16 : Uω (aρ 16) (bρ 16) (27652481574401 / 32000000000000) ≤ -(9045797086010213353117 / 10000000000000000000000)

theorem Zeta5Irrational.U_674 : Uρ (27652481574401 / 32000000000000) ≤ -(104789093514343343243 / 312500000000000000000)

theorem Zeta5Irrational.U_675_1 : Uω (aρ 1) (bρ 1) (56558325853133 / 64000000000000) ≤ -(1309378706805599354279 / 10000000000000000000000)

theorem Zeta5Irrational.U_675_2 : Uω (aρ 2) (bρ 2) (56558325853133 / 64000000000000) ≤ -(1336627245042598542631 / 10000000000000000000000)

theorem Zeta5Irrational.U_675_3 : Uω (aρ 3) (bρ 3) (56558325853133 / 64000000000000) ≤ -(1391297819368064538101 / 10000000000000000000000)

theorem Zeta5Irrational.U_675_4 : Uω (aρ 4) (bρ 4) (56558325853133 / 64000000000000) ≤ -(741304296202974127503 / 5000000000000000000000)

theorem Zeta5Irrational.U_675_5 : Uω (aρ 5) (bρ 5) (56558325853133 / 64000000000000) ≤ -(1622883744341165361017 / 10000000000000000000000)

theorem Zeta5Irrational.U_675_6 : Uω (aρ 6) (bρ 6) (56558325853133 / 64000000000000) ≤ -(913316624783847168869 / 5000000000000000000000)

theorem Zeta5Irrational.U_675_7 : Uω (aρ 7) (bρ 7) (56558325853133 / 64000000000000) ≤ -(527365195200048172033 / 2500000000000000000000)

theorem Zeta5Irrational.U_675_8 : Uω (aρ 8) (bρ 8) (56558325853133 / 64000000000000) ≤ -(1243394595876810300753 / 5000000000000000000000)

theorem Zeta5Irrational.U_675_9 : Uω (aρ 9) (bρ 9) (56558325853133 / 64000000000000) ≤ -(2972313060724690363641 / 10000000000000000000000)

theorem Zeta5Irrational.U_675_10 : Uω (aρ 10) (bρ 10) (56558325853133 / 64000000000000) ≤ -(893994214702231111179 / 2500000000000000000000)

theorem Zeta5Irrational.U_675_11 : Uω (aρ 11) (bρ 11) (56558325853133 / 64000000000000) ≤ -(215052782857109338981 / 500000000000000000000)

theorem Zeta5Irrational.U_675_12 : Uω (aρ 12) (bρ 12) (56558325853133 / 64000000000000) ≤ -(1027892171772619989907 / 2000000000000000000000)

theorem Zeta5Irrational.U_675_13 : Uω (aρ 13) (bρ 13) (56558325853133 / 64000000000000) ≤ -(1212718825538876018277 / 2000000000000000000000)

theorem Zeta5Irrational.U_675_14 : Uω (aρ 14) (bρ 14) (56558325853133 / 64000000000000) ≤ -(280489785711701105503 / 400000000000000000000)

theorem Zeta5Irrational.U_675_15 : Uω (aρ 15) (bρ 15) (56558325853133 / 64000000000000) ≤ -(7870167065046628959241 / 10000000000000000000000)

theorem Zeta5Irrational.U_675_16 : Uω (aρ 16) (bρ 16) (56558325853133 / 64000000000000) ≤ -(4229065425846391883387 / 5000000000000000000000)

theorem Zeta5Irrational.U_675 : Uρ (56558325853133 / 64000000000000) ≤ -(1540795269486682136973 / 5000000000000000000000)