Certified arcsine potential bounds (U29)

theorem Zeta5Irrational.U_352_1 : Uω (aρ 1) (bρ 1) (11358017183769 / 32000000000000) ≤ -(10541638900952844384301 / 10000000000000000000000)

theorem Zeta5Irrational.U_352_2 : Uω (aρ 2) (bρ 2) (11358017183769 / 32000000000000) ≤ -(1061083124688201051313 / 1000000000000000000000)

theorem Zeta5Irrational.U_352_3 : Uω (aρ 3) (bρ 3) (11358017183769 / 32000000000000) ≤ -(2150201267515562619751 / 2000000000000000000000)

theorem Zeta5Irrational.U_352_4 : Uω (aρ 4) (bρ 4) (11358017183769 / 32000000000000) ≤ -(5494661672584152532607 / 5000000000000000000000)

theorem Zeta5Irrational.U_352_5 : Uω (aρ 5) (bρ 5) (11358017183769 / 32000000000000) ≤ -(5683228812996067015517 / 5000000000000000000000)

theorem Zeta5Irrational.U_352_6 : Uω (aρ 6) (bρ 6) (11358017183769 / 32000000000000) ≤ -(5970540392073785020387 / 5000000000000000000000)

theorem Zeta5Irrational.U_352_7 : Uω (aρ 7) (bρ 7) (11358017183769 / 32000000000000) ≤ -(6401244525886062483541 / 5000000000000000000000)

theorem Zeta5Irrational.U_352_8 : Uω (aρ 8) (bρ 8) (11358017183769 / 32000000000000) ≤ -(2821675808831815775213 / 2000000000000000000000)

theorem Zeta5Irrational.U_352_9 : Uω (aρ 9) (bρ 9) (11358017183769 / 32000000000000) ≤ -(4058587466679611612501 / 2500000000000000000000)

theorem Zeta5Irrational.U_352_10 : Uω (aρ 10) (bρ 10) (11358017183769 / 32000000000000) ≤ -(10725842193563147263599 / 5000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_352 : Uρ (11358017183769 / 32000000000000) ≤ -(14594288429791755881307 / 10000000000000000000000)

theorem Zeta5Irrational.U_353_1 : Uω (aρ 1) (bρ 1) (22799751517797 / 64000000000000) ≤ -(10504172329495590335047 / 10000000000000000000000)

theorem Zeta5Irrational.U_353_2 : Uω (aρ 2) (bρ 2) (22799751517797 / 64000000000000) ≤ -(10573102202839460368983 / 10000000000000000000000)

theorem Zeta5Irrational.U_353_3 : Uω (aρ 3) (bρ 3) (22799751517797 / 64000000000000) ≤ -(5356368502045391193103 / 5000000000000000000000)

theorem Zeta5Irrational.U_353_4 : Uω (aρ 4) (bρ 4) (22799751517797 / 64000000000000) ≤ -(684381767471699544513 / 625000000000000000000)

theorem Zeta5Irrational.U_353_5 : Uω (aρ 5) (bρ 5) (22799751517797 / 64000000000000) ≤ -(11325671971142371422989 / 10000000000000000000000)

theorem Zeta5Irrational.U_353_6 : Uω (aρ 6) (bρ 6) (22799751517797 / 64000000000000) ≤ -(11897711012095434041723 / 10000000000000000000000)

theorem Zeta5Irrational.U_353_7 : Uω (aρ 7) (bρ 7) (22799751517797 / 64000000000000) ≤ -(6377372591149652653381 / 5000000000000000000000)

theorem Zeta5Irrational.U_353_8 : Uω (aρ 8) (bρ 8) (22799751517797 / 64000000000000) ≤ -(878284501219037432057 / 625000000000000000000)

theorem Zeta5Irrational.U_353_9 : Uω (aρ 9) (bρ 9) (22799751517797 / 64000000000000) ≤ -(8079818672537926407997 / 5000000000000000000000)

theorem Zeta5Irrational.U_353_10 : Uω (aρ 10) (bρ 10) (22799751517797 / 64000000000000) ≤ -(10606782922981723231029 / 5000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_353 : Uρ (22799751517797 / 64000000000000) ≤ -(14546684338120957832659 / 10000000000000000000000)

theorem Zeta5Irrational.U_354_1 : Uω (aρ 1) (bρ 1) (2860433583507 / 8000000000000) ≤ -(5233422806154407011667 / 5000000000000000000000)

theorem Zeta5Irrational.U_354_2 : Uω (aρ 2) (bρ 2) (2860433583507 / 8000000000000) ≤ -(2107102999367314674609 / 2000000000000000000000)

theorem Zeta5Irrational.U_354_3 : Uω (aρ 3) (bρ 3) (2860433583507 / 8000000000000) ≤ -(2668653414571848144461 / 2500000000000000000000)

theorem Zeta5Irrational.U_354_4 : Uω (aρ 4) (bρ 4) (2860433583507 / 8000000000000) ≤ -(218220933654013876573 / 200000000000000000000)

theorem Zeta5Irrational.U_354_5 : Uω (aρ 5) (bρ 5) (2860433583507 / 8000000000000) ≤ -(5642526418193389259393 / 5000000000000000000000)

theorem Zeta5Irrational.U_354_6 : Uω (aρ 6) (bρ 6) (2860433583507 / 8000000000000) ≤ -(2963632752427058012139 / 2500000000000000000000)

theorem Zeta5Irrational.U_354_7 : Uω (aρ 7) (bρ 7) (2860433583507 / 8000000000000) ≤ -(12707235810376217255869 / 10000000000000000000000)

theorem Zeta5Irrational.U_354_8 : Uω (aρ 8) (bρ 8) (2860433583507 / 8000000000000) ≤ -(13997061889017450904763 / 10000000000000000000000)

theorem Zeta5Irrational.U_354_9 : Uω (aρ 9) (bρ 9) (2860433583507 / 8000000000000) ≤ -(4021405282280517378607 / 2500000000000000000000)

theorem Zeta5Irrational.U_354_10 : Uω (aρ 10) (bρ 10) (2860433583507 / 8000000000000) ≤ -(2099233755464236526453 / 1000000000000000000000)

theorem Zeta5Irrational.U_354_11 : Uω (aρ 11) (bρ 11) (2860433583507 / 8000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_354_12 : Uω (aρ 12) (bρ 12) (2860433583507 / 8000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_354_13 : Uω (aρ 13) (bρ 13) (2860433583507 / 8000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_354_14 : Uω (aρ 14) (bρ 14) (2860433583507 / 8000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_354_15 : Uω (aρ 15) (bρ 15) (2860433583507 / 8000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_354_16 : Uω (aρ 16) (bρ 16) (2860433583507 / 8000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_354 : Uρ (2860433583507 / 8000000000000) ≤ -(7250341187646458758631 / 5000000000000000000000)

theorem Zeta5Irrational.U_355_1 : Uω (aρ 1) (bρ 1) (4593437163663 / 12800000000000) ≤ -(10429657709158020939677 / 10000000000000000000000)

theorem Zeta5Irrational.U_355_2 : Uω (aρ 2) (bρ 2) (4593437163663 / 12800000000000) ≤ -(10498068566233714828257 / 10000000000000000000000)

theorem Zeta5Irrational.U_355_3 : Uω (aρ 3) (bρ 3) (4593437163663 / 12800000000000) ≤ -(10636635189896886432221 / 10000000000000000000000)

theorem Zeta5Irrational.U_355_4 : Uω (aρ 4) (bρ 4) (4593437163663 / 12800000000000) ≤ -(10872137355885766455087 / 10000000000000000000000)

theorem Zeta5Irrational.U_355_5 : Uω (aρ 5) (bρ 5) (4593437163663 / 12800000000000) ≤ -(11244598860684962943507 / 10000000000000000000000)

theorem Zeta5Irrational.U_355_6 : Uω (aρ 6) (bρ 6) (4593437163663 / 12800000000000) ≤ -(11811539102151936781149 / 10000000000000000000000)

theorem Zeta5Irrational.U_355_7 : Uω (aρ 7) (bρ 7) (4593437163663 / 12800000000000) ≤ -(12659958571089790164417 / 10000000000000000000000)

theorem Zeta5Irrational.U_355_8 : Uω (aρ 8) (bρ 8) (4593437163663 / 12800000000000) ≤ -(435684509515087757189 / 312500000000000000000)

theorem Zeta5Irrational.U_355_9 : Uω (aρ 9) (bρ 9) (4593437163663 / 12800000000000) ≤ -(16012286050680742624031 / 10000000000000000000000)

theorem Zeta5Irrational.U_355_10 : Uω (aρ 10) (bρ 10) (4593437163663 / 12800000000000) ≤ -(20784935530951146153959 / 10000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_355 : Uρ (4593437163663 / 12800000000000) ≤ -(722800917271618526219 / 500000000000000000000)

theorem Zeta5Irrational.U_356_1 : Uω (aρ 1) (bρ 1) (11525451484287 / 32000000000000) ≤ -(1299075948921488108637 / 1250000000000000000000)

theorem Zeta5Irrational.U_356_2 : Uω (aρ 2) (bρ 2) (11525451484287 / 32000000000000) ≤ -(1046076186029057426927 / 1000000000000000000000)

theorem Zeta5Irrational.U_356_3 : Uω (aρ 3) (bρ 3) (11525451484287 / 32000000000000) ≤ -(662425031329633293843 / 625000000000000000000)

theorem Zeta5Irrational.U_356_4 : Uω (aρ 4) (bρ 4) (11525451484287 / 32000000000000) ≤ -(5416689557187702177793 / 5000000000000000000000)

theorem Zeta5Irrational.U_356_5 : Uω (aρ 5) (bρ 5) (11525451484287 / 32000000000000) ≤ -(2240861739939409583837 / 2000000000000000000000)

theorem Zeta5Irrational.U_356_6 : Uω (aρ 6) (bρ 6) (11525451484287 / 32000000000000) ≤ -(5884366818469516185671 / 5000000000000000000000)

theorem Zeta5Irrational.U_356_7 : Uω (aρ 7) (bρ 7) (11525451484287 / 32000000000000) ≤ -(6306455568069282526061 / 5000000000000000000000)

theorem Zeta5Irrational.U_356_8 : Uω (aρ 8) (bρ 8) (11525451484287 / 32000000000000) ≤ -(13887075006321262224287 / 10000000000000000000000)

theorem Zeta5Irrational.U_356_9 : Uω (aρ 9) (bρ 9) (11525451484287 / 32000000000000) ≤ -(15939617482324508012211 / 10000000000000000000000)

theorem Zeta5Irrational.U_356_10 : Uω (aρ 10) (bρ 10) (11525451484287 / 32000000000000) ≤ -(102945636677137892163 / 50000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_356 : Uρ (11525451484287 / 32000000000000) ≤ -(3603124797497613790197 / 2500000000000000000000)

theorem Zeta5Irrational.U_357_1 : Uω (aρ 1) (bρ 1) (23134620118833 / 64000000000000) ≤ -(5177847120835798780771 / 5000000000000000000000)

theorem Zeta5Irrational.U_357_2 : Uω (aρ 2) (bρ 2) (23134620118833 / 64000000000000) ≤ -(10423593839989125093553 / 10000000000000000000000)

theorem Zeta5Irrational.U_357_3 : Uω (aρ 3) (bρ 3) (23134620118833 / 64000000000000) ≤ -(2640277126802199692219 / 2500000000000000000000)

theorem Zeta5Irrational.U_357_4 : Uω (aρ 4) (bρ 4) (23134620118833 / 64000000000000) ≤ -(1349346348405073664153 / 1250000000000000000000)

theorem Zeta5Irrational.U_357_5 : Uω (aρ 5) (bρ 5) (23134620118833 / 64000000000000) ≤ -(11164181025510258405207 / 10000000000000000000000)

theorem Zeta5Irrational.U_357_6 : Uω (aρ 6) (bρ 6) (23134620118833 / 64000000000000) ≤ -(5863056491764085571929 / 5000000000000000000000)

theorem Zeta5Irrational.U_357_7 : Uω (aρ 7) (bρ 7) (23134620118833 / 64000000000000) ≤ -(12566091213062274615969 / 10000000000000000000000)

theorem Zeta5Irrational.U_357_8 : Uω (aρ 8) (bρ 8) (23134620118833 / 64000000000000) ≤ -(13832569823690590154751 / 10000000000000000000000)

theorem Zeta5Irrational.U_357_9 : Uω (aρ 9) (bρ 9) (23134620118833 / 64000000000000) ≤ -(7933800655272450017953 / 5000000000000000000000)

theorem Zeta5Irrational.U_357_10 : Uω (aρ 10) (bρ 10) (23134620118833 / 64000000000000) ≤ -(10201613235986337760123 / 5000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_357 : Uρ (23134620118833 / 64000000000000) ≤ -(14369978574398285360333 / 10000000000000000000000)

theorem Zeta5Irrational.U_358_1 : Uω (aρ 1) (bρ 1) (5804584317273 / 16000000000000) ≤ -(5159458327001527128447 / 5000000000000000000000)

theorem Zeta5Irrational.U_358_2 : Uω (aρ 2) (bρ 2) (5804584317273 / 16000000000000) ≤ -(5193281738929938716601 / 5000000000000000000000)

theorem Zeta5Irrational.U_358_3 : Uω (aρ 3) (bρ 3) (5804584317273 / 16000000000000) ≤ -(10523558134738120583187 / 10000000000000000000000)

theorem Zeta5Irrational.U_358_4 : Uω (aρ 4) (bρ 4) (5804584317273 / 16000000000000) ≤ -(10756311217136471123861 / 10000000000000000000000)

theorem Zeta5Irrational.U_358_5 : Uω (aρ 5) (bρ 5) (5804584317273 / 16000000000000) ≤ -(1390526815796387017917 / 1250000000000000000000)

theorem Zeta5Irrational.U_358_6 : Uω (aρ 6) (bρ 6) (5804584317273 / 16000000000000) ≤ -(467347021317313664613 / 400000000000000000000)

theorem Zeta5Irrational.U_358_7 : Uω (aρ 7) (bρ 7) (5804584317273 / 16000000000000) ≤ -(6259748272245998521739 / 5000000000000000000000)

theorem Zeta5Irrational.U_358_8 : Uω (aρ 8) (bρ 8) (5804584317273 / 16000000000000) ≤ -(13778384661680333337793 / 10000000000000000000000)

theorem Zeta5Irrational.U_358_9 : Uω (aρ 9) (bρ 9) (5804584317273 / 16000000000000) ≤ -(7898111955309340951673 / 5000000000000000000000)

theorem Zeta5Irrational.U_358_10 : Uω (aρ 10) (bρ 10) (5804584317273 / 16000000000000) ≤ -(10112960883108076518971 / 5000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_358 : Uρ (5804584317273 / 16000000000000) ≤ -(14328342301148102981567 / 10000000000000000000000)

theorem Zeta5Irrational.U_359_1 : Uω (aρ 1) (bρ 1) (46520391688443 / 128000000000000) ≤ -(5150289229783770027499 / 5000000000000000000000)

theorem Zeta5Irrational.U_359_2 : Uω (aρ 2) (bρ 2) (46520391688443 / 128000000000000) ≤ -(5184049800320691189273 / 5000000000000000000000)

theorem Zeta5Irrational.U_359_3 : Uω (aρ 3) (bρ 3) (46520391688443 / 128000000000000) ≤ -(10504835724603574181621 / 10000000000000000000000)

theorem Zeta5Irrational.U_359_4 : Uω (aρ 4) (bρ 4) (46520391688443 / 128000000000000) ≤ -(2147427371592678436087 / 2000000000000000000000)

theorem Zeta5Irrational.U_359_5 : Uω (aρ 5) (bρ 5) (46520391688443 / 128000000000000) ≤ -(11104291311875286283503 / 10000000000000000000000)

theorem Zeta5Irrational.U_359_6 : Uω (aρ 6) (bρ 6) (46520391688443 / 128000000000000) ≤ -(11662525011682297601331 / 10000000000000000000000)

theorem Zeta5Irrational.U_359_7 : Uω (aρ 7) (bρ 7) (46520391688443 / 128000000000000) ≤ -(12496282984634089874379 / 10000000000000000000000)

theorem Zeta5Irrational.U_359_8 : Uω (aρ 8) (bρ 8) (46520391688443 / 128000000000000) ≤ -(13751410833669744054049 / 10000000000000000000000)

theorem Zeta5Irrational.U_359_9 : Uω (aρ 9) (bρ 9) (46520391688443 / 128000000000000) ≤ -(197009632752461729613 / 125000000000000000000)

theorem Zeta5Irrational.U_359_10 : Uω (aρ 10) (bρ 10) (46520391688443 / 128000000000000) ≤ -(1258759909477100777669 / 625000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_359 : Uρ (46520391688443 / 128000000000000) ≤ -(2861565311915866550951 / 2000000000000000000000)

theorem Zeta5Irrational.U_360_1 : Uω (aρ 1) (bρ 1) (23302054419351 / 64000000000000) ≤ -(10282273833372514520303 / 10000000000000000000000)

theorem Zeta5Irrational.U_360_2 : Uω (aρ 2) (bρ 2) (23302054419351 / 64000000000000) ≤ -(10349669757811332992301 / 10000000000000000000000)

theorem Zeta5Irrational.U_360_3 : Uω (aρ 3) (bρ 3) (23302054419351 / 64000000000000) ≤ -(1310768540370397377601 / 1250000000000000000000)

theorem Zeta5Irrational.U_360_4 : Uω (aρ 4) (bρ 4) (23302054419351 / 64000000000000) ≤ -(1071799926009268155151 / 1000000000000000000000)

theorem Zeta5Irrational.U_360_5 : Uω (aρ 5) (bρ 5) (23302054419351 / 64000000000000) ≤ -(11084407906422986722507 / 10000000000000000000000)

theorem Zeta5Irrational.U_360_6 : Uω (aρ 6) (bρ 6) (23302054419351 / 64000000000000) ≤ -(2328283939467763148137 / 2000000000000000000000)

theorem Zeta5Irrational.U_360_7 : Uω (aρ 7) (bρ 7) (23302054419351 / 64000000000000) ≤ -(3118281226855059681807 / 2500000000000000000000)

theorem Zeta5Irrational.U_360_8 : Uω (aρ 8) (bρ 8) (23302054419351 / 64000000000000) ≤ -(13724515514587036197389 / 10000000000000000000000)

theorem Zeta5Irrational.U_360_9 : Uω (aρ 9) (bρ 9) (23302054419351 / 64000000000000) ≤ -(15725472123040980563639 / 10000000000000000000000)

theorem Zeta5Irrational.U_360_10 : Uω (aρ 10) (bρ 10) (23302054419351 / 64000000000000) ≤ -(5014042440673356328323 / 2500000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_360 : Uρ (23302054419351 / 64000000000000) ≤ -(14287499111685594879077 / 10000000000000000000000)

theorem Zeta5Irrational.U_361_1 : Uω (aρ 1) (bρ 1) (46687825988961 / 128000000000000) ≤ -(2052800530549085513821 / 2000000000000000000000)

theorem Zeta5Irrational.U_361_2 : Uω (aρ 2) (bρ 2) (46687825988961 / 128000000000000) ≤ -(10331273824108637515949 / 10000000000000000000000)

theorem Zeta5Irrational.U_361_3 : Uω (aρ 3) (bρ 3) (46687825988961 / 128000000000000) ≤ -(5233747899529985342477 / 5000000000000000000000)

theorem Zeta5Irrational.U_361_4 : Uω (aρ 4) (bρ 4) (46687825988961 / 128000000000000) ≤ -(10698898282584064623033 / 10000000000000000000000)

theorem Zeta5Irrational.U_361_5 : Uω (aρ 5) (bρ 5) (46687825988961 / 128000000000000) ≤ -(1383070518809231514651 / 1250000000000000000000)

theorem Zeta5Irrational.U_361_6 : Uω (aρ 6) (bρ 6) (46687825988961 / 128000000000000) ≤ -(1452544924334053118787 / 1250000000000000000000)

theorem Zeta5Irrational.U_361_7 : Uω (aρ 7) (bρ 7) (46687825988961 / 128000000000000) ≤ -(778126377514180342509 / 625000000000000000000)

theorem Zeta5Irrational.U_361_8 : Uω (aρ 8) (bρ 8) (46687825988961 / 128000000000000) ≤ -(856106138484193971651 / 625000000000000000000)

theorem Zeta5Irrational.U_361_9 : Uω (aρ 9) (bρ 9) (46687825988961 / 128000000000000) ≤ -(15690326843274616969439 / 10000000000000000000000)

theorem Zeta5Irrational.U_361_10 : Uω (aρ 10) (bρ 10) (46687825988961 / 128000000000000) ≤ -(19973855197920723312371 / 10000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_361 : Uρ (46687825988961 / 128000000000000) ≤ -(14267351142315811764633 / 10000000000000000000000)

theorem Zeta5Irrational.U_362_1 : Uω (aρ 1) (bρ 1) (2338577156961 / 6400000000000) ≤ -(2049152959136992528997 / 2000000000000000000000)

theorem Zeta5Irrational.U_362_2 : Uω (aρ 2) (bρ 2) (2338577156961 / 6400000000000) ≤ -(5156455837481287013357 / 5000000000000000000000)

theorem Zeta5Irrational.U_362_3 : Uω (aρ 3) (bρ 3) (2338577156961 / 6400000000000) ≤ -(1306109752858577475561 / 1250000000000000000000)

theorem Zeta5Irrational.U_362_4 : Uω (aρ 4) (bρ 4) (2338577156961 / 6400000000000) ≤ -(10679833785307686060643 / 10000000000000000000000)

theorem Zeta5Irrational.U_362_5 : Uω (aρ 5) (bρ 5) (2338577156961 / 6400000000000) ≤ -(11044759885449248784207 / 10000000000000000000000)

theorem Zeta5Irrational.U_362_6 : Uω (aρ 6) (bρ 6) (2338577156961 / 6400000000000) ≤ -(11599343909730129726657 / 10000000000000000000000)

theorem Zeta5Irrational.U_362_7 : Uω (aρ 7) (bρ 7) (2338577156961 / 6400000000000) ≤ -(3106743528122563498903 / 2500000000000000000000)

theorem Zeta5Irrational.U_362_8 : Uω (aρ 8) (bρ 8) (2338577156961 / 6400000000000) ≤ -(13670958453277325403241 / 10000000000000000000000)

theorem Zeta5Irrational.U_362_9 : Uω (aρ 9) (bρ 9) (2338577156961 / 6400000000000) ≤ -(3913833307851789537159 / 2500000000000000000000)

theorem Zeta5Irrational.U_362_10 : Uω (aρ 10) (bρ 10) (2338577156961 / 6400000000000) ≤ -(9946561910692850307419 / 5000000000000000000000)

theorem Zeta5Irrational.U_362_11 : Uω (aρ 11) (bρ 11) (2338577156961 / 6400000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_362_12 : Uω (aρ 12) (bρ 12) (2338577156961 / 6400000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_362_13 : Uω (aρ 13) (bρ 13) (2338577156961 / 6400000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_362_14 : Uω (aρ 14) (bρ 14) (2338577156961 / 6400000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_362_15 : Uω (aρ 15) (bρ 15) (2338577156961 / 6400000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_362_16 : Uω (aρ 16) (bρ 16) (2338577156961 / 6400000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_362 : Uρ (2338577156961 / 6400000000000) ≤ -(7123687311461268586551 / 5000000000000000000000)

theorem Zeta5Irrational.U_363_1 : Uω (aρ 1) (bρ 1) (46855260289479 / 128000000000000) ≤ -(2045512028171230018933 / 2000000000000000000000)

theorem Zeta5Irrational.U_363_2 : Uω (aρ 2) (bρ 2) (46855260289479 / 128000000000000) ≤ -(5147291593243858290007 / 5000000000000000000000)

theorem Zeta5Irrational.U_363_3 : Uω (aρ 3) (bρ 3) (46855260289479 / 128000000000000) ≤ -(325946714534062058909 / 312500000000000000000)

theorem Zeta5Irrational.U_363_4 : Uω (aρ 4) (bρ 4) (46855260289479 / 128000000000000) ≤ -(2665201407234472898471 / 2500000000000000000000)

theorem Zeta5Irrational.U_363_5 : Uω (aρ 5) (bρ 5) (46855260289479 / 128000000000000) ≤ -(5512497476862254615211 / 5000000000000000000000)

theorem Zeta5Irrational.U_363_6 : Uω (aρ 6) (bρ 6) (46855260289479 / 128000000000000) ≤ -(11578373049824663123831 / 10000000000000000000000)

theorem Zeta5Irrational.U_363_7 : Uω (aρ 7) (bρ 7) (46855260289479 / 128000000000000) ≤ -(12403980855685154507843 / 10000000000000000000000)

theorem Zeta5Irrational.U_363_8 : Uω (aρ 8) (bρ 8) (46855260289479 / 128000000000000) ≤ -(13644295748051856774619 / 10000000000000000000000)

theorem Zeta5Irrational.U_363_9 : Uω (aρ 9) (bρ 9) (46855260289479 / 128000000000000) ≤ -(15620489763713965806193 / 10000000000000000000000)

theorem Zeta5Irrational.U_363_10 : Uω (aρ 10) (bρ 10) (46855260289479 / 128000000000000) ≤ -(3962778525587527231453 / 2000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_363 : Uρ (46855260289479 / 128000000000000) ≤ -(14227562214506348845581 / 10000000000000000000000)