Certified arcsine potential bounds (U49)

theorem Zeta5Irrational.U_592_1 : Uω (aρ 1) (bρ 1) (8782653354179 / 12800000000000) ≤ -(3861145048423655657401 / 10000000000000000000000)

theorem Zeta5Irrational.U_592_2 : Uω (aρ 2) (bρ 2) (8782653354179 / 12800000000000) ≤ -(243523295113786450747 / 625000000000000000000)

theorem Zeta5Irrational.U_592_3 : Uω (aρ 3) (bρ 3) (8782653354179 / 12800000000000) ≤ -(991795346368845415999 / 2500000000000000000000)

theorem Zeta5Irrational.U_592_4 : Uω (aρ 4) (bρ 4) (8782653354179 / 12800000000000) ≤ -(51072963081599011411 / 125000000000000000000)

theorem Zeta5Irrational.U_592_5 : Uω (aρ 5) (bρ 5) (8782653354179 / 12800000000000) ≤ -(4269103245193693824213 / 10000000000000000000000)

theorem Zeta5Irrational.U_592_6 : Uω (aρ 6) (bρ 6) (8782653354179 / 12800000000000) ≤ -(4537521459674536368377 / 10000000000000000000000)

theorem Zeta5Irrational.U_592_7 : Uω (aρ 7) (bρ 7) (8782653354179 / 12800000000000) ≤ -(614350511180361655339 / 1250000000000000000000)

theorem Zeta5Irrational.U_592_8 : Uω (aρ 8) (bρ 8) (8782653354179 / 12800000000000) ≤ -(1356885589740886941109 / 2500000000000000000000)

theorem Zeta5Irrational.U_592_9 : Uω (aρ 9) (bρ 9) (8782653354179 / 12800000000000) ≤ -(6105539499798913087489 / 10000000000000000000000)

theorem Zeta5Irrational.U_592_10 : Uω (aρ 10) (bρ 10) (8782653354179 / 12800000000000) ≤ -(43646592711571477181 / 62500000000000000000)

theorem Zeta5Irrational.U_592_11 : Uω (aρ 11) (bρ 11) (8782653354179 / 12800000000000) ≤ -(253299539840680361623 / 312500000000000000000)

theorem Zeta5Irrational.U_592_12 : Uω (aρ 12) (bρ 12) (8782653354179 / 12800000000000) ≤ -(9539803762064064091603 / 10000000000000000000000)

theorem Zeta5Irrational.U_592_13 : Uω (aρ 13) (bρ 13) (8782653354179 / 12800000000000) ≤ -(11428424110941748224189 / 10000000000000000000000)

theorem Zeta5Irrational.U_592_14 : Uω (aρ 14) (bρ 14) (8782653354179 / 12800000000000) ≤ -(7171437141596351498281 / 5000000000000000000000)

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

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

theorem Zeta5Irrational.U_592 : Uρ (8782653354179 / 12800000000000) ≤ -(6493372085490171878343 / 10000000000000000000000)

theorem Zeta5Irrational.U_593_1 : Uω (aρ 1) (bρ 1) (10991296491131 / 16000000000000) ≤ -(76984335362129264989 / 200000000000000000000)

theorem Zeta5Irrational.U_593_2 : Uω (aρ 2) (bρ 2) (10991296491131 / 16000000000000) ≤ -(9711005343742677657 / 25000000000000000000)

theorem Zeta5Irrational.U_593_3 : Uω (aρ 3) (bρ 3) (10991296491131 / 16000000000000) ≤ -(31641000668466948117 / 80000000000000000000)

theorem Zeta5Irrational.U_593_4 : Uω (aρ 4) (bρ 4) (10991296491131 / 16000000000000) ≤ -(4073635020287535188957 / 10000000000000000000000)

theorem Zeta5Irrational.U_593_5 : Uω (aρ 5) (bρ 5) (10991296491131 / 16000000000000) ≤ -(4256670869576362918179 / 10000000000000000000000)

theorem Zeta5Irrational.U_593_6 : Uω (aρ 6) (bρ 6) (10991296491131 / 16000000000000) ≤ -(452473964593663599121 / 1000000000000000000000)

theorem Zeta5Irrational.U_593_7 : Uω (aρ 7) (bρ 7) (10991296491131 / 16000000000000) ≤ -(4901505303743168612503 / 10000000000000000000000)

theorem Zeta5Irrational.U_593_8 : Uω (aρ 8) (bρ 8) (10991296491131 / 16000000000000) ≤ -(2706744031536615135693 / 5000000000000000000000)

theorem Zeta5Irrational.U_593_9 : Uω (aρ 9) (bρ 9) (10991296491131 / 16000000000000) ≤ -(1522594958593701806993 / 2500000000000000000000)

theorem Zeta5Irrational.U_593_10 : Uω (aρ 10) (bρ 10) (10991296491131 / 16000000000000) ≤ -(6966649033551154060933 / 10000000000000000000000)

theorem Zeta5Irrational.U_593_11 : Uω (aρ 11) (bρ 11) (10991296491131 / 16000000000000) ≤ -(8086223519225050504341 / 10000000000000000000000)

theorem Zeta5Irrational.U_593_12 : Uω (aρ 12) (bρ 12) (10991296491131 / 16000000000000) ≤ -(1903224998521094270931 / 2000000000000000000000)

theorem Zeta5Irrational.U_593_13 : Uω (aρ 13) (bρ 13) (10991296491131 / 16000000000000) ≤ -(1424498049762649303159 / 1250000000000000000000)

theorem Zeta5Irrational.U_593_14 : Uω (aρ 14) (bρ 14) (10991296491131 / 16000000000000) ≤ -(713865897465215119503 / 500000000000000000000)

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

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

theorem Zeta5Irrational.U_593 : Uρ (10991296491131 / 16000000000000) ≤ -(6476639339068879338977 / 10000000000000000000000)

theorem Zeta5Irrational.U_594_1 : Uω (aρ 1) (bρ 1) (44017105158153 / 64000000000000) ≤ -(3837302699325395042261 / 10000000000000000000000)

theorem Zeta5Irrational.U_594_2 : Uω (aρ 2) (bρ 2) (44017105158153 / 64000000000000) ≤ -(3872445866191089838999 / 10000000000000000000000)

theorem Zeta5Irrational.U_594_3 : Uω (aρ 3) (bρ 3) (44017105158153 / 64000000000000) ≤ -(1971541650973881459497 / 5000000000000000000000)

theorem Zeta5Irrational.U_594_4 : Uω (aρ 4) (bρ 4) (44017105158153 / 64000000000000) ≤ -(2030723935954041162807 / 5000000000000000000000)

theorem Zeta5Irrational.U_594_5 : Uω (aρ 5) (bρ 5) (44017105158153 / 64000000000000) ≤ -(4244253950414137293169 / 10000000000000000000000)

theorem Zeta5Irrational.U_594_6 : Uω (aρ 6) (bρ 6) (44017105158153 / 64000000000000) ≤ -(4511974198329091467151 / 10000000000000000000000)

theorem Zeta5Irrational.U_594_7 : Uω (aρ 7) (bρ 7) (44017105158153 / 64000000000000) ≤ -(2444112151337690036797 / 5000000000000000000000)

theorem Zeta5Irrational.U_594_8 : Uω (aρ 8) (bρ 8) (44017105158153 / 64000000000000) ≤ -(43195630299015583237 / 80000000000000000000)

theorem Zeta5Irrational.U_594_9 : Uω (aρ 9) (bρ 9) (44017105158153 / 64000000000000) ≤ -(1215048765630322143733 / 2000000000000000000000)

theorem Zeta5Irrational.U_594_10 : Uω (aρ 10) (bρ 10) (44017105158153 / 64000000000000) ≤ -(1389974637746149243031 / 2000000000000000000000)

theorem Zeta5Irrational.U_594_11 : Uω (aρ 11) (bρ 11) (44017105158153 / 64000000000000) ≤ -(8066903811869647594891 / 10000000000000000000000)

theorem Zeta5Irrational.U_594_12 : Uω (aρ 12) (bρ 12) (44017105158153 / 64000000000000) ≤ -(4746258070544322986259 / 5000000000000000000000)

theorem Zeta5Irrational.U_594_13 : Uω (aρ 13) (bρ 13) (44017105158153 / 64000000000000) ≤ -(2272741445869784425119 / 2000000000000000000000)

theorem Zeta5Irrational.U_594_14 : Uω (aρ 14) (bρ 14) (44017105158153 / 64000000000000) ≤ -(14212960197935088470847 / 10000000000000000000000)

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

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

theorem Zeta5Irrational.U_594 : Uρ (44017105158153 / 64000000000000) ≤ -(3229994991353601011403 / 5000000000000000000000)

theorem Zeta5Irrational.U_595_1 : Uω (aρ 1) (bρ 1) (22034512175891 / 32000000000000) ≤ -(3825402808256825816339 / 10000000000000000000000)

theorem Zeta5Irrational.U_595_2 : Uω (aρ 2) (bρ 2) (22034512175891 / 32000000000000) ≤ -(965125968428573373733 / 2500000000000000000000)

theorem Zeta5Irrational.U_595_3 : Uω (aρ 3) (bρ 3) (22034512175891 / 32000000000000) ≤ -(786211201140834157933 / 2000000000000000000000)

theorem Zeta5Irrational.U_595_4 : Uω (aρ 4) (bρ 4) (22034512175891 / 32000000000000) ≤ -(2024637782567805178767 / 5000000000000000000000)

theorem Zeta5Irrational.U_595_5 : Uω (aρ 5) (bρ 5) (22034512175891 / 32000000000000) ≤ -(528981556159355254323 / 1250000000000000000000)

theorem Zeta5Irrational.U_595_6 : Uω (aρ 6) (bρ 6) (22034512175891 / 32000000000000) ≤ -(4499225074868244073119 / 10000000000000000000000)

theorem Zeta5Irrational.U_595_7 : Uω (aρ 7) (bρ 7) (22034512175891 / 32000000000000) ≤ -(97499220768220577801 / 200000000000000000000)

theorem Zeta5Irrational.U_595_8 : Uω (aρ 8) (bρ 8) (22034512175891 / 32000000000000) ≤ -(5385439474086395814851 / 10000000000000000000000)

theorem Zeta5Irrational.U_595_9 : Uω (aρ 9) (bρ 9) (22034512175891 / 32000000000000) ≤ -(94689553206502731041 / 156250000000000000000)

theorem Zeta5Irrational.U_595_10 : Uω (aρ 10) (bρ 10) (22034512175891 / 32000000000000) ≤ -(3466563593368778755967 / 5000000000000000000000)

theorem Zeta5Irrational.U_595_11 : Uω (aρ 11) (bρ 11) (22034512175891 / 32000000000000) ≤ -(502976621982016817177 / 625000000000000000000)

theorem Zeta5Irrational.U_595_12 : Uω (aρ 12) (bρ 12) (22034512175891 / 32000000000000) ≤ -(9468976722227678351319 / 10000000000000000000000)

theorem Zeta5Irrational.U_595_13 : Uω (aρ 13) (bρ 13) (22034512175891 / 32000000000000) ≤ -(708224407302227743551 / 625000000000000000000)

theorem Zeta5Irrational.U_595_14 : Uω (aρ 14) (bρ 14) (22034512175891 / 32000000000000) ≤ -(1768717515541818394809 / 1250000000000000000000)

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

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

theorem Zeta5Irrational.U_595 : Uρ (22034512175891 / 32000000000000) ≤ -(3221710550820856703479 / 5000000000000000000000)

theorem Zeta5Irrational.U_596_1 : Uω (aρ 1) (bρ 1) (44120943545411 / 64000000000000) ≤ -(3813517061197737683561 / 10000000000000000000000)

theorem Zeta5Irrational.U_596_2 : Uω (aρ 2) (bρ 2) (44120943545411 / 64000000000000) ≤ -(962144031500172235307 / 2500000000000000000000)

theorem Zeta5Irrational.U_596_3 : Uω (aρ 3) (bρ 3) (44120943545411 / 64000000000000) ≤ -(1959521580007089325513 / 5000000000000000000000)

theorem Zeta5Irrational.U_596_4 : Uω (aρ 4) (bρ 4) (44120943545411 / 64000000000000) ≤ -(2018559031924290803153 / 5000000000000000000000)

theorem Zeta5Irrational.U_596_5 : Uω (aρ 5) (bρ 5) (44120943545411 / 64000000000000) ≤ -(105486658196741034191 / 250000000000000000000)

theorem Zeta5Irrational.U_596_6 : Uω (aρ 6) (bρ 6) (44120943545411 / 64000000000000) ≤ -(4486492233732258104221 / 10000000000000000000000)

theorem Zeta5Irrational.U_596_7 : Uω (aρ 7) (bρ 7) (44120943545411 / 64000000000000) ≤ -(4861715463315582096821 / 10000000000000000000000)

theorem Zeta5Irrational.U_596_8 : Uω (aρ 8) (bρ 8) (44120943545411 / 64000000000000) ≤ -(42971560525332844949 / 80000000000000000000)

theorem Zeta5Irrational.U_596_9 : Uω (aρ 9) (bρ 9) (44120943545411 / 64000000000000) ≤ -(1209008498005994149171 / 2000000000000000000000)

theorem Zeta5Irrational.U_596_10 : Uω (aρ 10) (bρ 10) (44120943545411 / 64000000000000) ≤ -(3458205459091484569321 / 5000000000000000000000)

theorem Zeta5Irrational.U_596_11 : Uω (aρ 11) (bρ 11) (44120943545411 / 64000000000000) ≤ -(8028389739178359166687 / 10000000000000000000000)

theorem Zeta5Irrational.U_596_12 : Uω (aρ 12) (bρ 12) (44120943545411 / 64000000000000) ≤ -(295172070509336324951 / 312500000000000000000)

theorem Zeta5Irrational.U_596_13 : Uω (aρ 13) (bρ 13) (44120943545411 / 64000000000000) ≤ -(2259926443505063997727 / 2000000000000000000000)

theorem Zeta5Irrational.U_596_14 : Uω (aρ 14) (bρ 14) (44120943545411 / 64000000000000) ≤ -(7043800923483328933247 / 5000000000000000000000)

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

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

theorem Zeta5Irrational.U_596 : Uρ (44120943545411 / 64000000000000) ≤ -(1606732501947162911213 / 2500000000000000000000)

theorem Zeta5Irrational.U_597_1 : Uω (aρ 1) (bρ 1) (276080392119 / 400000000000) ≤ -(475205678070643602751 / 1250000000000000000000)

theorem Zeta5Irrational.U_597_2 : Uω (aρ 2) (bρ 2) (276080392119 / 400000000000) ≤ -(959165647276513419161 / 2500000000000000000000)

theorem Zeta5Irrational.U_597_3 : Uω (aρ 3) (bρ 3) (276080392119 / 400000000000) ≤ -(195352236509487228353 / 500000000000000000000)

theorem Zeta5Irrational.U_597_4 : Uω (aρ 4) (bρ 4) (276080392119 / 400000000000) ≤ -(4024975332057229824131 / 10000000000000000000000)

theorem Zeta5Irrational.U_597_5 : Uω (aρ 5) (bρ 5) (276080392119 / 400000000000) ≤ -(4207095548052328053339 / 10000000000000000000000)

theorem Zeta5Irrational.U_597_6 : Uω (aρ 6) (bρ 6) (276080392119 / 400000000000) ≤ -(4473775633260287782671 / 10000000000000000000000)

theorem Zeta5Irrational.U_597_7 : Uω (aρ 7) (bρ 7) (276080392119 / 400000000000) ≤ -(4848487529947418754959 / 10000000000000000000000)

theorem Zeta5Irrational.U_597_8 : Uω (aρ 8) (bρ 8) (276080392119 / 400000000000) ≤ -(214298820193377640081 / 400000000000000000000)

theorem Zeta5Irrational.U_597_9 : Uω (aρ 9) (bρ 9) (276080392119 / 400000000000) ≤ -(6029977007426569530737 / 10000000000000000000000)

theorem Zeta5Irrational.U_597_10 : Uω (aρ 10) (bρ 10) (276080392119 / 400000000000) ≤ -(107808191664674528683 / 156250000000000000000)

theorem Zeta5Irrational.U_597_11 : Uω (aρ 11) (bρ 11) (276080392119 / 400000000000) ≤ -(2002298744056355109751 / 2500000000000000000000)

theorem Zeta5Irrational.U_597_12 : Uω (aρ 12) (bρ 12) (276080392119 / 400000000000) ≤ -(4711052134525300289301 / 5000000000000000000000)

theorem Zeta5Irrational.U_597_13 : Uω (aρ 13) (bρ 13) (276080392119 / 400000000000) ≤ -(1408478791481375428463 / 1250000000000000000000)

theorem Zeta5Irrational.U_597_14 : Uω (aρ 14) (bρ 14) (276080392119 / 400000000000) ≤ -(7013246972571734108403 / 5000000000000000000000)

theorem Zeta5Irrational.U_597_15 : Uω (aρ 15) (bρ 15) (276080392119 / 400000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_597_16 : Uω (aρ 16) (bρ 16) (276080392119 / 400000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_597 : Uρ (276080392119 / 400000000000) ≤ -(6410514213786317389521 / 10000000000000000000000)

theorem Zeta5Irrational.U_598_1 : Uω (aρ 1) (bρ 1) (44224781932669 / 64000000000000) ≤ -(3789787864895543404819 / 10000000000000000000000)

theorem Zeta5Irrational.U_598_2 : Uω (aρ 2) (bρ 2) (44224781932669 / 64000000000000) ≤ -(3824763229207356151267 / 10000000000000000000000)

theorem Zeta5Irrational.U_598_3 : Uω (aρ 3) (bρ 3) (44224781932669 / 64000000000000) ≤ -(3895060681667598397467 / 10000000000000000000000)

theorem Zeta5Irrational.U_598_4 : Uω (aρ 4) (bρ 4) (44224781932669 / 64000000000000) ≤ -(250802958368932343957 / 625000000000000000000)

theorem Zeta5Irrational.U_598_5 : Uω (aρ 5) (bρ 5) (44224781932669 / 64000000000000) ≤ -(2097370035909306309519 / 5000000000000000000000)

theorem Zeta5Irrational.U_598_6 : Uω (aρ 6) (bρ 6) (44224781932669 / 64000000000000) ≤ -(4461075231951651050771 / 10000000000000000000000)

theorem Zeta5Irrational.U_598_7 : Uω (aρ 7) (bρ 7) (44224781932669 / 64000000000000) ≤ -(967055438211356976147 / 2000000000000000000000)

theorem Zeta5Irrational.U_598_8 : Uω (aρ 8) (bρ 8) (44224781932669 / 64000000000000) ≤ -(534351573455711606301 / 1000000000000000000000)

theorem Zeta5Irrational.U_598_9 : Uω (aρ 9) (bρ 9) (44224781932669 / 64000000000000) ≤ -(187966715081535804873 / 312500000000000000000)

theorem Zeta5Irrational.U_598_10 : Uω (aρ 10) (bρ 10) (44224781932669 / 64000000000000) ≤ -(1720766780932629166881 / 2500000000000000000000)

theorem Zeta5Irrational.U_598_11 : Uω (aρ 11) (bρ 11) (44224781932669 / 64000000000000) ≤ -(7990041466326574167593 / 10000000000000000000000)

theorem Zeta5Irrational.U_598_12 : Uω (aρ 12) (bρ 12) (44224781932669 / 64000000000000) ≤ -(469938514580832882803 / 500000000000000000000)

theorem Zeta5Irrational.U_598_13 : Uω (aρ 13) (bρ 13) (44224781932669 / 64000000000000) ≤ -(11236182902422223580447 / 10000000000000000000000)

theorem Zeta5Irrational.U_598_14 : Uω (aρ 14) (bρ 14) (44224781932669 / 64000000000000) ≤ -(2793273795028130683401 / 2000000000000000000000)

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

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

theorem Zeta5Irrational.U_598 : Uρ (44224781932669 / 64000000000000) ≤ -(39963571329679689973 / 62500000000000000000)

theorem Zeta5Irrational.U_599_1 : Uω (aρ 1) (bρ 1) (22138350563149 / 32000000000000) ≤ -(944486087211076226443 / 2500000000000000000000)

theorem Zeta5Irrational.U_599_2 : Uω (aρ 2) (bρ 2) (22138350563149 / 32000000000000) ≤ -(381287801260218030659 / 1000000000000000000000)

theorem Zeta5Irrational.U_599_3 : Uω (aρ 3) (bρ 3) (22138350563149 / 32000000000000) ≤ -(1941545490004321403837 / 5000000000000000000000)

theorem Zeta5Irrational.U_599_4 : Uω (aρ 4) (bρ 4) (22138350563149 / 32000000000000) ≤ -(4000734033657501560457 / 10000000000000000000000)

theorem Zeta5Irrational.U_599_5 : Uω (aρ 5) (bρ 5) (22138350563149 / 32000000000000) ≤ -(418239986130542002681 / 1000000000000000000000)

theorem Zeta5Irrational.U_599_6 : Uω (aρ 6) (bρ 6) (22138350563149 / 32000000000000) ≤ -(4448390988465003952377 / 10000000000000000000000)

theorem Zeta5Irrational.U_599_7 : Uω (aρ 7) (bρ 7) (22138350563149 / 32000000000000) ≤ -(602760549948094116003 / 1250000000000000000000)

theorem Zeta5Irrational.U_599_8 : Uω (aρ 8) (bρ 8) (22138350563149 / 32000000000000) ≤ -(1065916139610143317519 / 2000000000000000000000)

theorem Zeta5Irrational.U_599_9 : Uω (aρ 9) (bρ 9) (22138350563149 / 32000000000000) ≤ -(5999916041147995132601 / 10000000000000000000000)

theorem Zeta5Irrational.U_599_10 : Uω (aρ 10) (bρ 10) (22138350563149 / 32000000000000) ≤ -(6866439379730423357791 / 10000000000000000000000)

theorem Zeta5Irrational.U_599_11 : Uω (aρ 11) (bρ 11) (22138350563149 / 32000000000000) ≤ -(7970929014454339731257 / 10000000000000000000000)

theorem Zeta5Irrational.U_599_12 : Uω (aρ 12) (bρ 12) (22138350563149 / 32000000000000) ≤ -(1875100772085846270361 / 2000000000000000000000)

theorem Zeta5Irrational.U_599_13 : Uω (aρ 13) (bρ 13) (22138350563149 / 32000000000000) ≤ -(2240937602556298459121 / 2000000000000000000000)

theorem Zeta5Irrational.U_599_14 : Uω (aρ 14) (bρ 14) (22138350563149 / 32000000000000) ≤ -(13907183051807184338793 / 10000000000000000000000)

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

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

theorem Zeta5Irrational.U_599 : Uρ (22138350563149 / 32000000000000) ≤ -(6377899458709971549779 / 10000000000000000000000)

theorem Zeta5Irrational.U_600_1 : Uω (aρ 1) (bρ 1) (44328620319927 / 64000000000000) ≤ -(3766114843185157129627 / 10000000000000000000000)

theorem Zeta5Irrational.U_600_2 : Uω (aρ 2) (bρ 2) (44328620319927 / 64000000000000) ≤ -(19005034528540760341 / 50000000000000000000)

theorem Zeta5Irrational.U_600_3 : Uω (aρ 3) (bρ 3) (44328620319927 / 64000000000000) ≤ -(38711355908973622577 / 100000000000000000000)

theorem Zeta5Irrational.U_600_4 : Uω (aρ 4) (bρ 4) (44328620319927 / 64000000000000) ≤ -(3988635395722701368637 / 10000000000000000000000)

theorem Zeta5Irrational.U_600_5 : Uω (aρ 5) (bρ 5) (44328620319927 / 64000000000000) ≤ -(834014975758038440671 / 2000000000000000000000)

theorem Zeta5Irrational.U_600_6 : Uω (aρ 6) (bρ 6) (44328620319927 / 64000000000000) ≤ -(887144572323505302381 / 2000000000000000000000)

theorem Zeta5Irrational.U_600_7 : Uω (aρ 7) (bρ 7) (44328620319927 / 64000000000000) ≤ -(4808909108662188216689 / 10000000000000000000000)

theorem Zeta5Irrational.U_600_8 : Uω (aρ 8) (bρ 8) (44328620319927 / 64000000000000) ≤ -(5315665338778738707151 / 10000000000000000000000)

theorem Zeta5Irrational.U_600_9 : Uω (aρ 9) (bρ 9) (44328620319927 / 64000000000000) ≤ -(598492040897808695309 / 1000000000000000000000)

theorem Zeta5Irrational.U_600_10 : Uω (aρ 10) (bρ 10) (44328620319927 / 64000000000000) ≤ -(6849840925155560255049 / 10000000000000000000000)

theorem Zeta5Irrational.U_600_11 : Uω (aρ 11) (bρ 11) (44328620319927 / 64000000000000) ≤ -(3975928713532320038747 / 5000000000000000000000)

theorem Zeta5Irrational.U_600_12 : Uω (aρ 12) (bρ 12) (44328620319927 / 64000000000000) ≤ -(9352304517135290160901 / 10000000000000000000000)

theorem Zeta5Irrational.U_600_13 : Uω (aρ 13) (bρ 13) (44328620319927 / 64000000000000) ≤ -(5586671893103846167657 / 5000000000000000000000)

theorem Zeta5Irrational.U_600_14 : Uω (aρ 14) (bρ 14) (44328620319927 / 64000000000000) ≤ -(2769779097549425911313 / 2000000000000000000000)

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

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

theorem Zeta5Irrational.U_600 : Uρ (44328620319927 / 64000000000000) ≤ -(3180848175369736682521 / 5000000000000000000000)

theorem Zeta5Irrational.U_601_1 : Uω (aρ 1) (bρ 1) (11095134878389 / 16000000000000) ≤ -(938574828702399587789 / 2500000000000000000000)

theorem Zeta5Irrational.U_601_2 : Uω (aρ 2) (bρ 2) (11095134878389 / 16000000000000) ≤ -(757829975012473701853 / 2000000000000000000000)

theorem Zeta5Irrational.U_601_3 : Uω (aρ 3) (bρ 3) (11095134878389 / 16000000000000) ≤ -(964798620035307040553 / 2500000000000000000000)

theorem Zeta5Irrational.U_601_4 : Uω (aρ 4) (bρ 4) (11095134878389 / 16000000000000) ≤ -(994137846157366722441 / 2500000000000000000000)

theorem Zeta5Irrational.U_601_5 : Uω (aρ 5) (bρ 5) (11095134878389 / 16000000000000) ≤ -(4157765086690188808493 / 10000000000000000000000)

theorem Zeta5Irrational.U_601_6 : Uω (aρ 6) (bρ 6) (11095134878389 / 16000000000000) ≤ -(2211535405192055338863 / 5000000000000000000000)

theorem Zeta5Irrational.U_601_7 : Uω (aρ 7) (bρ 7) (11095134878389 / 16000000000000) ≤ -(959150254321744450281 / 2000000000000000000000)

theorem Zeta5Irrational.U_601_8 : Uω (aρ 8) (bρ 8) (11095134878389 / 16000000000000) ≤ -(265088480022531474809 / 500000000000000000000)

theorem Zeta5Irrational.U_601_9 : Uω (aρ 9) (bρ 9) (11095134878389 / 16000000000000) ≤ -(5969947912396625863489 / 10000000000000000000000)

theorem Zeta5Irrational.U_601_10 : Uω (aρ 10) (bρ 10) (11095134878389 / 16000000000000) ≤ -(3416635825630334296627 / 5000000000000000000000)

theorem Zeta5Irrational.U_601_11 : Uω (aρ 11) (bρ 11) (11095134878389 / 16000000000000) ≤ -(7932826512081039083167 / 10000000000000000000000)

theorem Zeta5Irrational.U_601_12 : Uω (aρ 12) (bρ 12) (11095134878389 / 16000000000000) ≤ -(9329171808514020960711 / 10000000000000000000000)

theorem Zeta5Irrational.U_601_13 : Uω (aρ 13) (bρ 13) (11095134878389 / 16000000000000) ≤ -(11142148384564178563437 / 10000000000000000000000)

theorem Zeta5Irrational.U_601_14 : Uω (aρ 14) (bρ 14) (11095134878389 / 16000000000000) ≤ -(551658738635868358737 / 400000000000000000000)

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

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

theorem Zeta5Irrational.U_601 : Uρ (11095134878389 / 16000000000000) ≤ -(6345560218321767044647 / 10000000000000000000000)

theorem Zeta5Irrational.U_602_1 : Uω (aρ 1) (bρ 1) (8886491741437 / 12800000000000) ≤ -(233906108170397038313 / 625000000000000000000)

theorem Zeta5Irrational.U_602_2 : Uω (aρ 2) (bρ 2) (8886491741437 / 12800000000000) ≤ -(944326721830208510903 / 2500000000000000000000)

theorem Zeta5Irrational.U_602_3 : Uω (aρ 3) (bρ 3) (8886491741437 / 12800000000000) ≤ -(384726761367011421543 / 1000000000000000000000)

theorem Zeta5Irrational.U_602_4 : Uω (aρ 4) (bρ 4) (8886491741437 / 12800000000000) ≤ -(792896393007470868719 / 2000000000000000000000)

theorem Zeta5Irrational.U_602_5 : Uω (aρ 5) (bρ 5) (8886491741437 / 12800000000000) ≤ -(165818817902471995431 / 400000000000000000000)

theorem Zeta5Irrational.U_602_6 : Uω (aρ 6) (bρ 6) (8886491741437 / 12800000000000) ≤ -(88208695877931068533 / 200000000000000000000)

theorem Zeta5Irrational.U_602_7 : Uω (aρ 7) (bρ 7) (8886491741437 / 12800000000000) ≤ -(478261084193173771567 / 1000000000000000000000)

theorem Zeta5Irrational.U_602_8 : Uω (aρ 8) (bρ 8) (8886491741437 / 12800000000000) ≤ -(5287893427020350660491 / 10000000000000000000000)

theorem Zeta5Irrational.U_602_9 : Uω (aρ 9) (bρ 9) (8886491741437 / 12800000000000) ≤ -(5954998478060639171699 / 10000000000000000000000)

theorem Zeta5Irrational.U_602_10 : Uω (aρ 10) (bρ 10) (8886491741437 / 12800000000000) ≤ -(6816731449933417676493 / 10000000000000000000000)

theorem Zeta5Irrational.U_602_11 : Uω (aρ 11) (bρ 11) (8886491741437 / 12800000000000) ≤ -(3956918039439585658247 / 5000000000000000000000)

theorem Zeta5Irrational.U_602_12 : Uω (aρ 12) (bρ 12) (8886491741437 / 12800000000000) ≤ -(9306105286396064384171 / 10000000000000000000000)

theorem Zeta5Irrational.U_602_13 : Uω (aρ 13) (bρ 13) (8886491741437 / 12800000000000) ≤ -(5555550003594789216321 / 5000000000000000000000)

theorem Zeta5Irrational.U_602_14 : Uω (aρ 14) (bρ 14) (8886491741437 / 12800000000000) ≤ -(6867433388723770022023 / 5000000000000000000000)

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

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

theorem Zeta5Irrational.U_602 : Uρ (8886491741437 / 12800000000000) ≤ -(6329489309641351499701 / 10000000000000000000000)

theorem Zeta5Irrational.U_603_1 : Uω (aρ 1) (bρ 1) (22242188950407 / 32000000000000) ≤ -(3730710058060810453223 / 10000000000000000000000)

theorem Zeta5Irrational.U_603_2 : Uω (aρ 2) (bρ 2) (22242188950407 / 32000000000000) ≤ -(3765477909257897765203 / 10000000000000000000000)

theorem Zeta5Irrational.U_603_3 : Uω (aρ 3) (bρ 3) (22242188950407 / 32000000000000) ≤ -(1917677478767856130919 / 5000000000000000000000)

theorem Zeta5Irrational.U_603_4 : Uω (aρ 4) (bρ 4) (22242188950407 / 32000000000000) ≤ -(4940533877167384837 / 12500000000000000000)

theorem Zeta5Irrational.U_603_5 : Uω (aρ 5) (bρ 5) (22242188950407 / 32000000000000) ≤ -(413319092409985669183 / 1000000000000000000000)

theorem Zeta5Irrational.U_603_6 : Uω (aρ 6) (bρ 6) (22242188950407 / 32000000000000) ≤ -(87956295428855053233 / 200000000000000000000)

theorem Zeta5Irrational.U_603_7 : Uω (aρ 7) (bρ 7) (22242188950407 / 32000000000000) ≤ -(4769487773325352152819 / 10000000000000000000000)

theorem Zeta5Irrational.U_603_8 : Uω (aρ 8) (bρ 8) (22242188950407 / 32000000000000) ≤ -(5274036762684941512903 / 10000000000000000000000)

theorem Zeta5Irrational.U_603_9 : Uω (aρ 9) (bρ 9) (22242188950407 / 32000000000000) ≤ -(5940072032984582198809 / 10000000000000000000000)

theorem Zeta5Irrational.U_603_10 : Uω (aρ 10) (bρ 10) (22242188950407 / 32000000000000) ≤ -(6800220213689320315221 / 10000000000000000000000)

theorem Zeta5Irrational.U_603_11 : Uω (aρ 11) (bρ 11) (22242188950407 / 32000000000000) ≤ -(3947442969135704496559 / 5000000000000000000000)

theorem Zeta5Irrational.U_603_12 : Uω (aρ 12) (bρ 12) (22242188950407 / 32000000000000) ≤ -(9283104507584379732129 / 10000000000000000000000)

theorem Zeta5Irrational.U_603_13 : Uω (aρ 13) (bρ 13) (22242188950407 / 32000000000000) ≤ -(11080196889829367210413 / 10000000000000000000000)

theorem Zeta5Irrational.U_603_14 : Uω (aρ 14) (bρ 14) (22242188950407 / 32000000000000) ≤ -(341976439182884107769 / 250000000000000000000)

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

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

theorem Zeta5Irrational.U_603 : Uρ (22242188950407 / 32000000000000) ≤ -(1578370495051350464269 / 2500000000000000000000)