Certified arcsine potential bounds (U30)

theorem Zeta5Irrational.U_364_1 : Uω (aρ 1) (bρ 1) (23469488719869 / 64000000000000) ≤ -(1020938856758552771767 / 1000000000000000000000)

theorem Zeta5Irrational.U_364_2 : Uω (aρ 2) (bρ 2) (23469488719869 / 64000000000000) ≤ -(1284536029434866094411 / 1250000000000000000000)

theorem Zeta5Irrational.U_364_3 : Uω (aρ 3) (bρ 3) (23469488719869 / 64000000000000) ≤ -(2602936549286429362049 / 2500000000000000000000)

theorem Zeta5Irrational.U_364_4 : Uω (aρ 4) (bρ 4) (23469488719869 / 64000000000000) ≤ -(10641813674947082111827 / 10000000000000000000000)

theorem Zeta5Irrational.U_364_5 : Uω (aρ 5) (bρ 5) (23469488719869 / 64000000000000) ≤ -(1100526919862125627921 / 1000000000000000000000)

theorem Zeta5Irrational.U_364_6 : Uω (aρ 6) (bρ 6) (23469488719869 / 64000000000000) ≤ -(11557446623523384046263 / 10000000000000000000000)

theorem Zeta5Irrational.U_364_7 : Uω (aρ 7) (bρ 7) (23469488719869 / 64000000000000) ≤ -(2476208400660810589321 / 2000000000000000000000)

theorem Zeta5Irrational.U_364_8 : Uω (aρ 8) (bρ 8) (23469488719869 / 64000000000000) ≤ -(1702213703203382586437 / 1250000000000000000000)

theorem Zeta5Irrational.U_364_9 : Uω (aρ 9) (bρ 9) (23469488719869 / 64000000000000) ≤ -(155857949416357088431 / 100000000000000000000)

theorem Zeta5Irrational.U_364_10 : Uω (aρ 10) (bρ 10) (23469488719869 / 64000000000000) ≤ -(19736085683035117132133 / 10000000000000000000000)

theorem Zeta5Irrational.U_364_11 : Uω (aρ 11) (bρ 11) (23469488719869 / 64000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_364_12 : Uω (aρ 12) (bρ 12) (23469488719869 / 64000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_364_13 : Uω (aρ 13) (bρ 13) (23469488719869 / 64000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_364_14 : Uω (aρ 14) (bρ 14) (23469488719869 / 64000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_364_15 : Uω (aρ 15) (bρ 15) (23469488719869 / 64000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_364_16 : Uω (aρ 16) (bρ 16) (23469488719869 / 64000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_364 : Uρ (23469488719869 / 64000000000000) ≤ -(142079071854851839327 / 100000000000000000000)

theorem Zeta5Irrational.U_365_1 : Uω (aρ 1) (bρ 1) (47022694589997 / 128000000000000) ≤ -(5095624977928167751467 / 5000000000000000000000)

theorem Zeta5Irrational.U_365_2 : Uω (aρ 2) (bρ 2) (47022694589997 / 128000000000000) ≤ -(2051605339881276118719 / 2000000000000000000000)

theorem Zeta5Irrational.U_365_3 : Uω (aρ 3) (bρ 3) (47022694589997 / 128000000000000) ≤ -(5196615945586448281083 / 5000000000000000000000)

theorem Zeta5Irrational.U_365_4 : Uω (aρ 4) (bρ 4) (47022694589997 / 128000000000000) ≤ -(1327857223199951105543 / 1250000000000000000000)

theorem Zeta5Irrational.U_365_5 : Uω (aρ 5) (bρ 5) (47022694589997 / 128000000000000) ≤ -(10985582464399812475231 / 10000000000000000000000)

theorem Zeta5Irrational.U_365_6 : Uω (aρ 6) (bρ 6) (47022694589997 / 128000000000000) ≤ -(11536564440637285168937 / 10000000000000000000000)

theorem Zeta5Irrational.U_365_7 : Uω (aρ 7) (bρ 7) (47022694589997 / 128000000000000) ≤ -(12358157290836437477463 / 10000000000000000000000)

theorem Zeta5Irrational.U_365_8 : Uω (aρ 8) (bρ 8) (47022694589997 / 128000000000000) ≤ -(6795599808089037888341 / 5000000000000000000000)

theorem Zeta5Irrational.U_365_9 : Uω (aρ 9) (bρ 9) (47022694589997 / 128000000000000) ≤ -(3887811822798896889681 / 2500000000000000000000)

theorem Zeta5Irrational.U_365_10 : Uω (aρ 10) (bρ 10) (47022694589997 / 128000000000000) ≤ -(19659633305412022108387 / 10000000000000000000000)

theorem Zeta5Irrational.U_365_11 : Uω (aρ 11) (bρ 11) (47022694589997 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_365_12 : Uω (aρ 12) (bρ 12) (47022694589997 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_365_13 : Uω (aρ 13) (bρ 13) (47022694589997 / 128000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_365_14 : Uω (aρ 14) (bρ 14) (47022694589997 / 128000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_365_15 : Uω (aρ 15) (bρ 15) (47022694589997 / 128000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_365_16 : Uω (aρ 16) (bρ 16) (47022694589997 / 128000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_365 : Uρ (47022694589997 / 128000000000000) ≤ -(14188403341773910537759 / 10000000000000000000000)

theorem Zeta5Irrational.U_366_1 : Uω (aρ 1) (bρ 1) (1472075366883 / 4000000000000) ≤ -(1017314418630376217589 / 1000000000000000000000)

theorem Zeta5Irrational.U_366_2 : Uω (aρ 2) (bρ 2) (1472075366883 / 4000000000000) ≤ -(10239798456410631867589 / 10000000000000000000000)

theorem Zeta5Irrational.U_366_3 : Uω (aρ 3) (bρ 3) (1472075366883 / 4000000000000) ≤ -(64842198875117124881 / 62500000000000000000)

theorem Zeta5Irrational.U_366_4 : Uω (aρ 4) (bρ 4) (1472075366883 / 4000000000000) ≤ -(10603937823945748174413 / 10000000000000000000000)

theorem Zeta5Irrational.U_366_5 : Uω (aρ 5) (bρ 5) (1472075366883 / 4000000000000) ≤ -(2741483649062919691693 / 2500000000000000000000)

theorem Zeta5Irrational.U_366_6 : Uω (aρ 6) (bρ 6) (1472075366883 / 4000000000000) ≤ -(5757863156105059112447 / 5000000000000000000000)

theorem Zeta5Irrational.U_366_7 : Uω (aρ 7) (bρ 7) (1472075366883 / 4000000000000) ≤ -(3083831613937107456921 / 2500000000000000000000)

theorem Zeta5Irrational.U_366_8 : Uω (aρ 8) (bρ 8) (1472075366883 / 4000000000000) ≤ -(1356476525443648126067 / 1000000000000000000000)

theorem Zeta5Irrational.U_366_9 : Uω (aρ 9) (bρ 9) (1472075366883 / 4000000000000) ≤ -(969802835152118119703 / 625000000000000000000)

theorem Zeta5Irrational.U_366_10 : Uω (aρ 10) (bρ 10) (1472075366883 / 4000000000000) ≤ -(4896117841857481864347 / 2500000000000000000000)

theorem Zeta5Irrational.U_366_11 : Uω (aρ 11) (bρ 11) (1472075366883 / 4000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_366_12 : Uω (aρ 12) (bρ 12) (1472075366883 / 4000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_366_13 : Uω (aρ 13) (bρ 13) (1472075366883 / 4000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_366_14 : Uω (aρ 14) (bρ 14) (1472075366883 / 4000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_366_15 : Uω (aρ 15) (bρ 15) (1472075366883 / 4000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_366_16 : Uω (aρ 16) (bρ 16) (1472075366883 / 4000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_366 : Uρ (1472075366883 / 4000000000000) ≤ -(2833808993384900581253 / 2000000000000000000000)

theorem Zeta5Irrational.U_367_1 : Uω (aρ 1) (bρ 1) (9438025778103 / 25600000000000) ≤ -(10155071140210231970999 / 10000000000000000000000)

theorem Zeta5Irrational.U_367_2 : Uω (aρ 2) (bρ 2) (9438025778103 / 25600000000000) ≤ -(5110801692648868227249 / 5000000000000000000000)

theorem Zeta5Irrational.U_367_3 : Uω (aρ 3) (bρ 3) (9438025778103 / 25600000000000) ≤ -(10356305857235350616427 / 10000000000000000000000)

theorem Zeta5Irrational.U_367_4 : Uω (aρ 4) (bρ 4) (9438025778103 / 25600000000000) ≤ -(5292526826907858834617 / 5000000000000000000000)

theorem Zeta5Irrational.U_367_5 : Uω (aρ 5) (bρ 5) (9438025778103 / 25600000000000) ≤ -(10946325440292095100241 / 10000000000000000000000)

theorem Zeta5Irrational.U_367_6 : Uω (aρ 6) (bρ 6) (9438025778103 / 25600000000000) ≤ -(11494932050507656954393 / 10000000000000000000000)

theorem Zeta5Irrational.U_367_7 : Uω (aρ 7) (bρ 7) (9438025778103 / 25600000000000) ≤ -(12312549237462678980321 / 10000000000000000000000)

theorem Zeta5Irrational.U_367_8 : Uω (aρ 8) (bρ 8) (9438025778103 / 25600000000000) ≤ -(3384601519907263353979 / 2500000000000000000000)

theorem Zeta5Irrational.U_367_9 : Uω (aρ 9) (bρ 9) (9438025778103 / 25600000000000) ≤ -(7741293864429637342667 / 5000000000000000000000)

theorem Zeta5Irrational.U_367_10 : Uω (aρ 10) (bρ 10) (9438025778103 / 25600000000000) ≤ -(19510540693039739543589 / 10000000000000000000000)

theorem Zeta5Irrational.U_367_11 : Uω (aρ 11) (bρ 11) (9438025778103 / 25600000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_367_12 : Uω (aρ 12) (bρ 12) (9438025778103 / 25600000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_367_13 : Uω (aρ 13) (bρ 13) (9438025778103 / 25600000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_367_14 : Uω (aρ 14) (bρ 14) (9438025778103 / 25600000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_367_15 : Uω (aρ 15) (bρ 15) (9438025778103 / 25600000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_367_16 : Uω (aρ 16) (bρ 16) (9438025778103 / 25600000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_367 : Uρ (9438025778103 / 25600000000000) ≤ -(2829965354122144662707 / 2000000000000000000000)

theorem Zeta5Irrational.U_368_1 : Uω (aρ 1) (bρ 1) (23636923020387 / 64000000000000) ≤ -(5068515349750366186051 / 5000000000000000000000)

theorem Zeta5Irrational.U_368_2 : Uω (aρ 2) (bρ 2) (23636923020387 / 64000000000000) ≤ -(10203441365534420333661 / 10000000000000000000000)

theorem Zeta5Irrational.U_368_3 : Uω (aρ 3) (bρ 3) (23636923020387 / 64000000000000) ≤ -(10337893877074504726461 / 10000000000000000000000)

theorem Zeta5Irrational.U_368_4 : Uω (aρ 4) (bρ 4) (23636923020387 / 64000000000000) ≤ -(10566205139813757343053 / 10000000000000000000000)

theorem Zeta5Irrational.U_368_5 : Uω (aρ 5) (bρ 5) (23636923020387 / 64000000000000) ≤ -(2185350968710533704413 / 2000000000000000000000)

theorem Zeta5Irrational.U_368_6 : Uω (aρ 6) (bρ 6) (23636923020387 / 64000000000000) ≤ -(11474181469007055192813 / 10000000000000000000000)

theorem Zeta5Irrational.U_368_7 : Uω (aρ 7) (bρ 7) (23636923020387 / 64000000000000) ≤ -(6144912688669251179439 / 5000000000000000000000)

theorem Zeta5Irrational.U_368_8 : Uω (aρ 8) (bρ 8) (23636923020387 / 64000000000000) ≤ -(13512121635417570816127 / 10000000000000000000000)

theorem Zeta5Irrational.U_368_9 : Uω (aρ 9) (bρ 9) (23636923020387 / 64000000000000) ≤ -(3089694597383226710451 / 2000000000000000000000)

theorem Zeta5Irrational.U_368_10 : Uω (aρ 10) (bρ 10) (23636923020387 / 64000000000000) ≤ -(19437786537202591506609 / 10000000000000000000000)

theorem Zeta5Irrational.U_368_11 : Uω (aρ 11) (bρ 11) (23636923020387 / 64000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_368_12 : Uω (aρ 12) (bρ 12) (23636923020387 / 64000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_368_13 : Uω (aρ 13) (bρ 13) (23636923020387 / 64000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_368_14 : Uω (aρ 14) (bρ 14) (23636923020387 / 64000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_368_15 : Uω (aρ 15) (bρ 15) (23636923020387 / 64000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_368_16 : Uω (aρ 16) (bρ 16) (23636923020387 / 64000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_368 : Uρ (23636923020387 / 64000000000000) ≤ -(3532685961019217504731 / 2500000000000000000000)

theorem Zeta5Irrational.U_369_1 : Uω (aρ 1) (bρ 1) (47357563191033 / 128000000000000) ≤ -(5059511373369090753989 / 5000000000000000000000)

theorem Zeta5Irrational.U_369_2 : Uω (aρ 2) (bρ 2) (47357563191033 / 128000000000000) ≤ -(5092656138621636409351 / 5000000000000000000000)

theorem Zeta5Irrational.U_369_3 : Uω (aρ 3) (bρ 3) (47357563191033 / 128000000000000) ≤ -(10319515754482508126191 / 10000000000000000000000)

theorem Zeta5Irrational.U_369_4 : Uω (aρ 4) (bρ 4) (47357563191033 / 128000000000000) ≤ -(10547392147312262476351 / 10000000000000000000000)

theorem Zeta5Irrational.U_369_5 : Uω (aρ 5) (bρ 5) (47357563191033 / 128000000000000) ≤ -(1090722265397408139433 / 1000000000000000000000)

theorem Zeta5Irrational.U_369_6 : Uω (aρ 6) (bρ 6) (47357563191033 / 128000000000000) ≤ -(1431684297798292659107 / 1250000000000000000000)

theorem Zeta5Irrational.U_369_7 : Uω (aρ 7) (bρ 7) (47357563191033 / 128000000000000) ≤ -(12267154618652294812397 / 10000000000000000000000)

theorem Zeta5Irrational.U_369_8 : Uω (aρ 8) (bρ 8) (47357563191033 / 128000000000000) ≤ -(6742955734919824914827 / 5000000000000000000000)

theorem Zeta5Irrational.U_369_9 : Uω (aρ 9) (bρ 9) (47357563191033 / 128000000000000) ≤ -(3082899951093501236787 / 2000000000000000000000)

theorem Zeta5Irrational.U_369_10 : Uω (aρ 10) (bρ 10) (47357563191033 / 128000000000000) ≤ -(19366158133686468909589 / 10000000000000000000000)

theorem Zeta5Irrational.U_369_11 : Uω (aρ 11) (bρ 11) (47357563191033 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_369_12 : Uω (aρ 12) (bρ 12) (47357563191033 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_369_13 : Uω (aρ 13) (bρ 13) (47357563191033 / 128000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_369_14 : Uω (aρ 14) (bρ 14) (47357563191033 / 128000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_369_15 : Uω (aρ 15) (bρ 15) (47357563191033 / 128000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_369_16 : Uω (aρ 16) (bρ 16) (47357563191033 / 128000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_369 : Uρ (47357563191033 / 128000000000000) ≤ -(7055895810716133855411 / 5000000000000000000000)

theorem Zeta5Irrational.U_370_1 : Uω (aρ 1) (bρ 1) (11860320085323 / 32000000000000) ≤ -(10101047165118847851507 / 10000000000000000000000)

theorem Zeta5Irrational.U_370_2 : Uω (aρ 2) (bρ 2) (11860320085323 / 32000000000000) ≤ -(317725500037437652139 / 312500000000000000000)

theorem Zeta5Irrational.U_370_3 : Uω (aρ 3) (bρ 3) (11860320085323 / 32000000000000) ≤ -(10301171365095080003113 / 10000000000000000000000)

theorem Zeta5Irrational.U_370_4 : Uω (aρ 4) (bρ 4) (11860320085323 / 32000000000000) ≤ -(2632153635611494003493 / 2500000000000000000000)

theorem Zeta5Irrational.U_370_5 : Uω (aρ 5) (bρ 5) (11860320085323 / 32000000000000) ≤ -(5443864360199435669073 / 5000000000000000000000)

theorem Zeta5Irrational.U_370_6 : Uω (aρ 6) (bρ 6) (11860320085323 / 32000000000000) ≤ -(11432810606514017181871 / 10000000000000000000000)

theorem Zeta5Irrational.U_370_7 : Uω (aρ 7) (bρ 7) (11860320085323 / 32000000000000) ≤ -(15305670883222720007 / 12500000000000000000)

theorem Zeta5Irrational.U_370_8 : Uω (aρ 8) (bρ 8) (11860320085323 / 32000000000000) ≤ -(13459775135250613273287 / 10000000000000000000000)

theorem Zeta5Irrational.U_370_9 : Uω (aρ 9) (bρ 9) (11860320085323 / 32000000000000) ≤ -(61522666701171816901 / 40000000000000000000)

theorem Zeta5Irrational.U_370_10 : Uω (aρ 10) (bρ 10) (11860320085323 / 32000000000000) ≤ -(3859121660113755047557 / 2000000000000000000000)

theorem Zeta5Irrational.U_370_11 : Uω (aρ 11) (bρ 11) (11860320085323 / 32000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_370_12 : Uω (aρ 12) (bρ 12) (11860320085323 / 32000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_370_13 : Uω (aρ 13) (bρ 13) (11860320085323 / 32000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_370_14 : Uω (aρ 14) (bρ 14) (11860320085323 / 32000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_370_15 : Uω (aρ 15) (bρ 15) (11860320085323 / 32000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_370_16 : Uω (aρ 16) (bρ 16) (11860320085323 / 32000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_370 : Uρ (11860320085323 / 32000000000000) ≤ -(1761620730734933931937 / 1250000000000000000000)

theorem Zeta5Irrational.U_371_1 : Uω (aρ 1) (bρ 1) (47524997491551 / 128000000000000) ≤ -(10083103838467802937571 / 10000000000000000000000)

theorem Zeta5Irrational.U_371_2 : Uω (aρ 2) (bρ 2) (47524997491551 / 128000000000000) ≤ -(10149152418818740405747 / 10000000000000000000000)

theorem Zeta5Irrational.U_371_3 : Uω (aρ 3) (bρ 3) (47524997491551 / 128000000000000) ≤ -(2570715146308073706789 / 2500000000000000000000)

theorem Zeta5Irrational.U_371_4 : Uω (aρ 4) (bρ 4) (47524997491551 / 128000000000000) ≤ -(10509872192106231280577 / 10000000000000000000000)

theorem Zeta5Irrational.U_371_5 : Uω (aρ 5) (bρ 5) (47524997491551 / 128000000000000) ≤ -(2173654578512854934223 / 2000000000000000000000)

theorem Zeta5Irrational.U_371_6 : Uω (aρ 6) (bρ 6) (47524997491551 / 128000000000000) ≤ -(1426523744804845731913 / 1250000000000000000000)

theorem Zeta5Irrational.U_371_7 : Uω (aρ 7) (bρ 7) (47524997491551 / 128000000000000) ≤ -(381936605880278124109 / 312500000000000000000)

theorem Zeta5Irrational.U_371_8 : Uω (aρ 8) (bρ 8) (47524997491551 / 128000000000000) ≤ -(13433712188266326115151 / 10000000000000000000000)

theorem Zeta5Irrational.U_371_9 : Uω (aρ 9) (bρ 9) (47524997491551 / 128000000000000) ≤ -(191837155107511234621 / 125000000000000000000)

theorem Zeta5Irrational.U_371_10 : Uω (aρ 10) (bρ 10) (47524997491551 / 128000000000000) ≤ -(9613046547344408264177 / 5000000000000000000000)

theorem Zeta5Irrational.U_371_11 : Uω (aρ 11) (bρ 11) (47524997491551 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_371_12 : Uω (aρ 12) (bρ 12) (47524997491551 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_371_13 : Uω (aρ 13) (bρ 13) (47524997491551 / 128000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_371_14 : Uω (aρ 14) (bρ 14) (47524997491551 / 128000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_371_15 : Uω (aρ 15) (bρ 15) (47524997491551 / 128000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_371_16 : Uω (aρ 16) (bρ 16) (47524997491551 / 128000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_371 : Uρ (47524997491551 / 128000000000000) ≤ -(112594100321021907347 / 80000000000000000000)

theorem Zeta5Irrational.U_372_1 : Uω (aρ 1) (bρ 1) (4760871464181 / 12800000000000) ≤ -(5032596325617203968613 / 5000000000000000000000)

theorem Zeta5Irrational.U_372_2 : Uω (aρ 2) (bρ 2) (4760871464181 / 12800000000000) ≤ -(10131121412167346282789 / 10000000000000000000000)

theorem Zeta5Irrational.U_372_3 : Uω (aρ 3) (bρ 3) (4760871464181 / 12800000000000) ≤ -(641536455743347809409 / 625000000000000000000)

theorem Zeta5Irrational.U_372_4 : Uω (aρ 4) (bρ 4) (4760871464181 / 12800000000000) ≤ -(10491164963935251592369 / 10000000000000000000000)

theorem Zeta5Irrational.U_372_5 : Uω (aρ 5) (bρ 5) (4760871464181 / 12800000000000) ≤ -(10848855021095157620113 / 10000000000000000000000)

theorem Zeta5Irrational.U_372_6 : Uω (aρ 6) (bρ 6) (4760871464181 / 12800000000000) ≤ -(2847903064094822168529 / 2500000000000000000000)

theorem Zeta5Irrational.U_372_7 : Uω (aρ 7) (bρ 7) (4760871464181 / 12800000000000) ≤ -(12199458412337004357933 / 10000000000000000000000)

theorem Zeta5Irrational.U_372_8 : Uω (aρ 8) (bρ 8) (4760871464181 / 12800000000000) ≤ -(3351930547426756303613 / 2500000000000000000000)

theorem Zeta5Irrational.U_372_9 : Uω (aρ 9) (bρ 9) (4760871464181 / 12800000000000) ≤ -(7656707819277447128447 / 5000000000000000000000)

theorem Zeta5Irrational.U_372_10 : Uω (aρ 10) (bρ 10) (4760871464181 / 12800000000000) ≤ -(19157571507822823325749 / 10000000000000000000000)

theorem Zeta5Irrational.U_372_11 : Uω (aρ 11) (bρ 11) (4760871464181 / 12800000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_372_12 : Uω (aρ 12) (bρ 12) (4760871464181 / 12800000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_372_13 : Uω (aρ 13) (bρ 13) (4760871464181 / 12800000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_372_14 : Uω (aρ 14) (bρ 14) (4760871464181 / 12800000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_372_15 : Uω (aρ 15) (bρ 15) (4760871464181 / 12800000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_372_16 : Uω (aρ 16) (bρ 16) (4760871464181 / 12800000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_372 : Uρ (4760871464181 / 12800000000000) ≤ -(7027838990186991712099 / 5000000000000000000000)

theorem Zeta5Irrational.U_373_1 : Uω (aρ 1) (bρ 1) (47692431792069 / 128000000000000) ≤ -(2009462697697571396643 / 2000000000000000000000)

theorem Zeta5Irrational.U_373_2 : Uω (aρ 2) (bρ 2) (47692431792069 / 128000000000000) ≤ -(252828071598570374709 / 250000000000000000000)

theorem Zeta5Irrational.U_373_3 : Uω (aρ 3) (bρ 3) (47692431792069 / 128000000000000) ≤ -(512316968137633730297 / 500000000000000000000)

theorem Zeta5Irrational.U_373_4 : Uω (aρ 4) (bρ 4) (47692431792069 / 128000000000000) ≤ -(5236246363160253772561 / 5000000000000000000000)

theorem Zeta5Irrational.U_373_5 : Uω (aρ 5) (bρ 5) (47692431792069 / 128000000000000) ≤ -(5414737478748498833533 / 5000000000000000000000)

theorem Zeta5Irrational.U_373_6 : Uω (aρ 6) (bρ 6) (47692431792069 / 128000000000000) ≤ -(2274215463942847126499 / 2000000000000000000000)

theorem Zeta5Irrational.U_373_7 : Uω (aρ 7) (bρ 7) (47692431792069 / 128000000000000) ≤ -(1522124691229523665977 / 1250000000000000000000)

theorem Zeta5Irrational.U_373_8 : Uω (aρ 8) (bρ 8) (47692431792069 / 128000000000000) ≤ -(3345451176135521414619 / 2500000000000000000000)

theorem Zeta5Irrational.U_373_9 : Uω (aρ 9) (bρ 9) (47692431792069 / 128000000000000) ≤ -(15279995068813354745051 / 10000000000000000000000)

theorem Zeta5Irrational.U_373_10 : Uω (aρ 10) (bρ 10) (47692431792069 / 128000000000000) ≤ -(4772501299645587367841 / 2500000000000000000000)

theorem Zeta5Irrational.U_373_11 : Uω (aρ 11) (bρ 11) (47692431792069 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_373_12 : Uω (aρ 12) (bρ 12) (47692431792069 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_373_13 : Uω (aρ 13) (bρ 13) (47692431792069 / 128000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_373_14 : Uω (aρ 14) (bρ 14) (47692431792069 / 128000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_373_15 : Uω (aρ 15) (bρ 15) (47692431792069 / 128000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_373_16 : Uω (aρ 16) (bρ 16) (47692431792069 / 128000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_373 : Uρ (47692431792069 / 128000000000000) ≤ -(701860433666920155633 / 500000000000000000000)

theorem Zeta5Irrational.U_374_1 : Uω (aρ 1) (bρ 1) (5972018617791 / 16000000000000) ≤ -(10029466235912752073139 / 10000000000000000000000)

theorem Zeta5Irrational.U_374_2 : Uω (aρ 2) (bρ 2) (5972018617791 / 16000000000000) ≤ -(2523789164369170187899 / 2500000000000000000000)

theorem Zeta5Irrational.U_374_3 : Uω (aρ 3) (bρ 3) (5972018617791 / 16000000000000) ≤ -(10228128676152854997047 / 10000000000000000000000)

theorem Zeta5Irrational.U_374_4 : Uω (aρ 4) (bρ 4) (5972018617791 / 16000000000000) ≤ -(10453855348389118523381 / 10000000000000000000000)

theorem Zeta5Irrational.U_374_5 : Uω (aρ 5) (bρ 5) (5972018617791 / 16000000000000) ≤ -(10810132554148952355511 / 10000000000000000000000)

theorem Zeta5Irrational.U_374_6 : Uω (aρ 6) (bρ 6) (5972018617791 / 16000000000000) ≤ -(11350584968972253481687 / 10000000000000000000000)

theorem Zeta5Irrational.U_374_7 : Uω (aρ 7) (bρ 7) (5972018617791 / 16000000000000) ≤ -(3038647123310739096387 / 2500000000000000000000)

theorem Zeta5Irrational.U_374_8 : Uω (aρ 8) (bρ 8) (5972018617791 / 16000000000000) ≤ -(534238372073429131109 / 400000000000000000000)

theorem Zeta5Irrational.U_374_9 : Uω (aρ 9) (bρ 9) (5972018617791 / 16000000000000) ≤ -(15246709423082283256313 / 10000000000000000000000)

theorem Zeta5Irrational.U_374_10 : Uω (aρ 10) (bρ 10) (5972018617791 / 16000000000000) ≤ -(760934330201234651191 / 400000000000000000000)

theorem Zeta5Irrational.U_374_11 : Uω (aρ 11) (bρ 11) (5972018617791 / 16000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_374_12 : Uω (aρ 12) (bρ 12) (5972018617791 / 16000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_374_13 : Uω (aρ 13) (bρ 13) (5972018617791 / 16000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_374_14 : Uω (aρ 14) (bρ 14) (5972018617791 / 16000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_374_15 : Uω (aρ 15) (bρ 15) (5972018617791 / 16000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_374_16 : Uω (aρ 16) (bρ 16) (5972018617791 / 16000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_374 : Uρ (5972018617791 / 16000000000000) ≤ -(14018851335926930024331 / 10000000000000000000000)

theorem Zeta5Irrational.U_375_1 : Uω (aρ 1) (bρ 1) (47859866092587 / 128000000000000) ≤ -(10011650779804707866637 / 10000000000000000000000)

theorem Zeta5Irrational.U_375_2 : Uω (aρ 2) (bρ 2) (47859866092587 / 128000000000000) ≤ -(10077222676728475367993 / 10000000000000000000000)

theorem Zeta5Irrational.U_375_3 : Uω (aρ 3) (bρ 3) (47859866092587 / 128000000000000) ≤ -(1020995111110190420443 / 1000000000000000000000)

theorem Zeta5Irrational.U_375_4 : Uω (aρ 4) (bρ 4) (47859866092587 / 128000000000000) ≤ -(521762635000115749317 / 500000000000000000000)

theorem Zeta5Irrational.U_375_5 : Uω (aρ 5) (bρ 5) (47859866092587 / 128000000000000) ≤ -(10790827664296983932529 / 10000000000000000000000)

theorem Zeta5Irrational.U_375_6 : Uω (aρ 6) (bρ 6) (47859866092587 / 128000000000000) ≤ -(1133013502582213637493 / 1000000000000000000000)

theorem Zeta5Irrational.U_375_7 : Uω (aρ 7) (bρ 7) (47859866092587 / 128000000000000) ≤ -(6066115528469227373073 / 5000000000000000000000)

theorem Zeta5Irrational.U_375_8 : Uω (aρ 8) (bρ 8) (47859866092587 / 128000000000000) ≤ -(6665092777346813657789 / 5000000000000000000000)

theorem Zeta5Irrational.U_375_9 : Uω (aρ 9) (bρ 9) (47859866092587 / 128000000000000) ≤ -(15213557444680535887109 / 10000000000000000000000)

theorem Zeta5Irrational.U_375_10 : Uω (aρ 10) (bρ 10) (47859866092587 / 128000000000000) ≤ -(18957596983821605453081 / 10000000000000000000000)

theorem Zeta5Irrational.U_375_11 : Uω (aρ 11) (bρ 11) (47859866092587 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_375_12 : Uω (aρ 12) (bρ 12) (47859866092587 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_375_13 : Uω (aρ 13) (bρ 13) (47859866092587 / 128000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_375_14 : Uω (aρ 14) (bρ 14) (47859866092587 / 128000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_375_15 : Uω (aρ 15) (bρ 15) (47859866092587 / 128000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_375_16 : Uω (aρ 16) (bρ 16) (47859866092587 / 128000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_375 : Uρ (47859866092587 / 128000000000000) ≤ -(14000602877161742308257 / 10000000000000000000000)