Certified arcsine potential bounds (U32)

theorem Zeta5Irrational.U_388_1 : Uω (aρ 1) (bρ 1) (24474094522977 / 64000000000000) ≤ -(9782892679034460345389 / 10000000000000000000000)

theorem Zeta5Irrational.U_388_2 : Uω (aρ 2) (bρ 2) (24474094522977 / 64000000000000) ≤ -(9846961784527956511941 / 10000000000000000000000)

theorem Zeta5Irrational.U_388_3 : Uω (aρ 3) (bρ 3) (24474094522977 / 64000000000000) ≤ -(9976602955068756301647 / 10000000000000000000000)

theorem Zeta5Irrational.U_388_4 : Uω (aρ 4) (bρ 4) (24474094522977 / 64000000000000) ≤ -(5098260374562509612519 / 5000000000000000000000)

theorem Zeta5Irrational.U_388_5 : Uω (aρ 5) (bρ 5) (24474094522977 / 64000000000000) ≤ -(10543212587579755254357 / 10000000000000000000000)

theorem Zeta5Irrational.U_388_6 : Uω (aρ 6) (bρ 6) (24474094522977 / 64000000000000) ≤ -(11068065731103946049403 / 10000000000000000000000)

theorem Zeta5Irrational.U_388_7 : Uω (aρ 7) (bρ 7) (24474094522977 / 64000000000000) ≤ -(1480771428879991064171 / 1250000000000000000000)

theorem Zeta5Irrational.U_388_8 : Uω (aρ 8) (bρ 8) (24474094522977 / 64000000000000) ≤ -(13001460302417974526679 / 10000000000000000000000)

theorem Zeta5Irrational.U_388_9 : Uω (aρ 9) (bρ 9) (24474094522977 / 64000000000000) ≤ -(7397103440139706118931 / 5000000000000000000000)

theorem Zeta5Irrational.U_388_10 : Uω (aρ 10) (bρ 10) (24474094522977 / 64000000000000) ≤ -(3634209441235360305123 / 2000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_388 : Uρ (24474094522977 / 64000000000000) ≤ -(6886071039805945481207 / 5000000000000000000000)

theorem Zeta5Irrational.U_389_1 : Uω (aρ 1) (bρ 1) (6139452918309 / 16000000000000) ≤ -(4874079507725232605329 / 5000000000000000000000)

theorem Zeta5Irrational.U_389_2 : Uω (aρ 2) (bρ 2) (6139452918309 / 16000000000000) ≤ -(9812003014569464231753 / 10000000000000000000000)

theorem Zeta5Irrational.U_389_3 : Uω (aρ 3) (bρ 3) (6139452918309 / 16000000000000) ≤ -(310661935157438047953 / 312500000000000000000)

theorem Zeta5Irrational.U_389_4 : Uω (aρ 4) (bρ 4) (6139452918309 / 16000000000000) ≤ -(10160294209093882698789 / 10000000000000000000000)

theorem Zeta5Irrational.U_389_5 : Uω (aρ 5) (bρ 5) (6139452918309 / 16000000000000) ≤ -(10505658718397677553489 / 10000000000000000000000)

theorem Zeta5Irrational.U_389_6 : Uω (aρ 6) (bρ 6) (6139452918309 / 16000000000000) ≤ -(11028356902751511319297 / 10000000000000000000000)

theorem Zeta5Irrational.U_389_7 : Uω (aρ 7) (bρ 7) (6139452918309 / 16000000000000) ≤ -(11802899846123785371143 / 10000000000000000000000)

theorem Zeta5Irrational.U_389_8 : Uω (aρ 8) (bρ 8) (6139452918309 / 16000000000000) ≤ -(12951899506522119733701 / 10000000000000000000000)

theorem Zeta5Irrational.U_389_9 : Uω (aρ 9) (bρ 9) (6139452918309 / 16000000000000) ≤ -(14731518704915448957371 / 10000000000000000000000)

theorem Zeta5Irrational.U_389_10 : Uω (aρ 10) (bρ 10) (6139452918309 / 16000000000000) ≤ -(9029794594203179324451 / 5000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_389 : Uρ (6139452918309 / 16000000000000) ≤ -(6869138820388027502371 / 5000000000000000000000)

theorem Zeta5Irrational.U_390_1 : Uω (aρ 1) (bρ 1) (4928305764699 / 12800000000000) ≤ -(9713545579860973935019 / 10000000000000000000000)

theorem Zeta5Irrational.U_390_2 : Uω (aρ 2) (bρ 2) (4928305764699 / 12800000000000) ≤ -(1955433209774552219883 / 2000000000000000000000)

theorem Zeta5Irrational.U_390_3 : Uω (aρ 3) (bρ 3) (4928305764699 / 12800000000000) ≤ -(9905885984557209782699 / 10000000000000000000000)

theorem Zeta5Irrational.U_390_4 : Uω (aρ 4) (bρ 4) (4928305764699 / 12800000000000) ≤ -(10124198641054031683193 / 10000000000000000000000)

theorem Zeta5Irrational.U_390_5 : Uω (aρ 5) (bρ 5) (4928305764699 / 12800000000000) ≤ -(10468245961831071935927 / 10000000000000000000000)

theorem Zeta5Irrational.U_390_6 : Uω (aρ 6) (bρ 6) (4928305764699 / 12800000000000) ≤ -(1098880688224468762929 / 1000000000000000000000)

theorem Zeta5Irrational.U_390_7 : Uω (aρ 7) (bρ 7) (4928305764699 / 12800000000000) ≤ -(5879909935102141370187 / 5000000000000000000000)

theorem Zeta5Irrational.U_390_8 : Uω (aρ 8) (bρ 8) (4928305764699 / 12800000000000) ≤ -(12902600052262391086187 / 10000000000000000000000)

theorem Zeta5Irrational.U_390_9 : Uω (aρ 9) (bρ 9) (4928305764699 / 12800000000000) ≤ -(7334647102916508509139 / 5000000000000000000000)

theorem Zeta5Irrational.U_390_10 : Uω (aρ 10) (bρ 10) (4928305764699 / 12800000000000) ≤ -(17950290879875761555441 / 10000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_390 : Uρ (4928305764699 / 12800000000000) ≤ -(13704718217822075139391 / 10000000000000000000000)

theorem Zeta5Irrational.U_391_1 : Uω (aρ 1) (bρ 1) (12362622986877 / 32000000000000) ≤ -(9679051542797064085659 / 10000000000000000000000)

theorem Zeta5Irrational.U_391_2 : Uω (aρ 2) (bρ 2) (12362622986877 / 32000000000000) ≤ -(608903127591907559467 / 625000000000000000000)

theorem Zeta5Irrational.U_391_3 : Uω (aρ 3) (bρ 3) (12362622986877 / 32000000000000) ≤ -(4935357126377696842237 / 5000000000000000000000)

theorem Zeta5Irrational.U_391_4 : Uω (aρ 4) (bρ 4) (12362622986877 / 32000000000000) ≤ -(10088233099897932006419 / 10000000000000000000000)

theorem Zeta5Irrational.U_391_5 : Uω (aρ 5) (bρ 5) (12362622986877 / 32000000000000) ≤ -(10430973256828805279317 / 10000000000000000000000)

theorem Zeta5Irrational.U_391_6 : Uω (aρ 6) (bρ 6) (12362622986877 / 32000000000000) ≤ -(1094941439062756986717 / 1000000000000000000000)

theorem Zeta5Irrational.U_391_7 : Uω (aρ 7) (bρ 7) (12362622986877 / 32000000000000) ≤ -(11716929769262015717329 / 10000000000000000000000)

theorem Zeta5Irrational.U_391_8 : Uω (aρ 8) (bρ 8) (12362622986877 / 32000000000000) ≤ -(12853559027970004128109 / 10000000000000000000000)

theorem Zeta5Irrational.U_391_9 : Uω (aρ 9) (bρ 9) (12362622986877 / 32000000000000) ≤ -(14607525600897892519987 / 10000000000000000000000)

theorem Zeta5Irrational.U_391_10 : Uω (aρ 10) (bρ 10) (12362622986877 / 32000000000000) ≤ -(17843043740896604037687 / 10000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_391 : Uρ (12362622986877 / 32000000000000) ≤ -(1708931642661093442263 / 1250000000000000000000)

theorem Zeta5Irrational.U_392_1 : Uω (aρ 1) (bρ 1) (24808963124013 / 64000000000000) ≤ -(9644676083344422677201 / 10000000000000000000000)

theorem Zeta5Irrational.U_392_2 : Uω (aρ 2) (bρ 2) (24808963124013 / 64000000000000) ≤ -(4853927077589738354537 / 5000000000000000000000)

theorem Zeta5Irrational.U_392_3 : Uω (aρ 3) (bρ 3) (24808963124013 / 64000000000000) ≤ -(983566585803844534669 / 1000000000000000000000)

theorem Zeta5Irrational.U_392_4 : Uω (aρ 4) (bρ 4) (24808963124013 / 64000000000000) ≤ -(10052396650727247046407 / 10000000000000000000000)

theorem Zeta5Irrational.U_392_5 : Uω (aρ 5) (bρ 5) (24808963124013 / 64000000000000) ≤ -(10393839554312362094071 / 10000000000000000000000)

theorem Zeta5Irrational.U_392_6 : Uω (aρ 6) (bρ 6) (24808963124013 / 64000000000000) ≤ -(5455089082246591798157 / 5000000000000000000000)

theorem Zeta5Irrational.U_392_7 : Uω (aρ 7) (bρ 7) (24808963124013 / 64000000000000) ≤ -(11674227833276534326773 / 10000000000000000000000)

theorem Zeta5Irrational.U_392_8 : Uω (aρ 8) (bρ 8) (24808963124013 / 64000000000000) ≤ -(12804773572830401849953 / 10000000000000000000000)

theorem Zeta5Irrational.U_392_9 : Uω (aρ 9) (bρ 9) (24808963124013 / 64000000000000) ≤ -(14546205320110649728969 / 10000000000000000000000)

theorem Zeta5Irrational.U_392_10 : Uω (aρ 10) (bρ 10) (24808963124013 / 64000000000000) ≤ -(8868874065295747246851 / 5000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_392 : Uρ (24808963124013 / 64000000000000) ≤ -(13638472530975199410167 / 10000000000000000000000)

theorem Zeta5Irrational.U_393_1 : Uω (aρ 1) (bρ 1) (777896258571 / 2000000000000) ≤ -(9610418389026122523323 / 10000000000000000000000)

theorem Zeta5Irrational.U_393_2 : Uω (aρ 2) (bρ 2) (777896258571 / 2000000000000) ≤ -(9673377561479211552663 / 10000000000000000000000)

theorem Zeta5Irrational.U_393_3 : Uω (aρ 3) (bρ 3) (777896258571 / 2000000000000) ≤ -(4900369968979588461839 / 5000000000000000000000)

theorem Zeta5Irrational.U_393_4 : Uω (aρ 4) (bρ 4) (777896258571 / 2000000000000) ≤ -(10016688368706092780689 / 10000000000000000000000)

theorem Zeta5Irrational.U_393_5 : Uω (aρ 5) (bρ 5) (777896258571 / 2000000000000) ≤ -(1294605477124456972273 / 1250000000000000000000)

theorem Zeta5Irrational.U_393_6 : Uω (aρ 6) (bρ 6) (777896258571 / 2000000000000) ≤ -(10871096955729972325563 / 10000000000000000000000)

theorem Zeta5Irrational.U_393_7 : Uω (aρ 7) (bρ 7) (777896258571 / 2000000000000) ≤ -(5815856187888038278651 / 5000000000000000000000)

theorem Zeta5Irrational.U_393_8 : Uω (aρ 8) (bρ 8) (777896258571 / 2000000000000) ≤ -(6378120437829771179201 / 5000000000000000000000)

theorem Zeta5Irrational.U_393_9 : Uω (aρ 9) (bρ 9) (777896258571 / 2000000000000) ≤ -(7242662998772565864273 / 5000000000000000000000)

theorem Zeta5Irrational.U_393_10 : Uω (aρ 10) (bρ 10) (777896258571 / 2000000000000) ≤ -(17634312313178388895607 / 10000000000000000000000)

theorem Zeta5Irrational.U_393_11 : Uω (aρ 11) (bρ 11) (777896258571 / 2000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_393_12 : Uω (aρ 12) (bρ 12) (777896258571 / 2000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_393_13 : Uω (aρ 13) (bρ 13) (777896258571 / 2000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_393_14 : Uω (aρ 14) (bρ 14) (777896258571 / 2000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_393_15 : Uω (aρ 15) (bρ 15) (777896258571 / 2000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_393_16 : Uω (aρ 16) (bρ 16) (777896258571 / 2000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_393 : Uρ (777896258571 / 2000000000000) ≤ -(13605767210096107167543 / 10000000000000000000000)

theorem Zeta5Irrational.U_394_1 : Uω (aρ 1) (bρ 1) (24976397424531 / 64000000000000) ≤ -(478813882784368812437 / 500000000000000000000)

theorem Zeta5Irrational.U_394_2 : Uω (aρ 2) (bρ 2) (24976397424531 / 64000000000000) ≤ -(4819509720196513865331 / 5000000000000000000000)

theorem Zeta5Irrational.U_394_3 : Uω (aρ 3) (bρ 3) (24976397424531 / 64000000000000) ≤ -(152592744360776913309 / 156250000000000000000)

theorem Zeta5Irrational.U_394_4 : Uω (aρ 4) (bρ 4) (24976397424531 / 64000000000000) ≤ -(1247638417364616165651 / 1250000000000000000000)

theorem Zeta5Irrational.U_394_5 : Uω (aρ 5) (bρ 5) (24976397424531 / 64000000000000) ≤ -(10319985019208236224207 / 10000000000000000000000)

theorem Zeta5Irrational.U_394_6 : Uω (aρ 6) (bρ 6) (24976397424531 / 64000000000000) ≤ -(2708042382818369174677 / 2500000000000000000000)

theorem Zeta5Irrational.U_394_7 : Uω (aρ 7) (bρ 7) (24976397424531 / 64000000000000) ≤ -(11589381733398019179671 / 10000000000000000000000)

theorem Zeta5Irrational.U_394_8 : Uω (aρ 8) (bρ 8) (24976397424531 / 64000000000000) ≤ -(12707958173717871882943 / 10000000000000000000000)

theorem Zeta5Irrational.U_394_9 : Uω (aρ 9) (bρ 9) (24976397424531 / 64000000000000) ≤ -(14424880463678895676333 / 10000000000000000000000)

theorem Zeta5Irrational.U_394_10 : Uω (aρ 10) (bρ 10) (24976397424531 / 64000000000000) ≤ -(2191581450344132072969 / 1250000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_394 : Uρ (24976397424531 / 64000000000000) ≤ -(3393332157828625400013 / 2500000000000000000000)

theorem Zeta5Irrational.U_395_1 : Uω (aρ 1) (bρ 1) (2506011457479 / 6400000000000) ≤ -(1908450617476454881111 / 2000000000000000000000)

theorem Zeta5Irrational.U_395_2 : Uω (aρ 2) (bρ 2) (2506011457479 / 6400000000000) ≤ -(9604778980370867307719 / 10000000000000000000000)

theorem Zeta5Irrational.U_395_3 : Uω (aρ 3) (bρ 3) (2506011457479 / 6400000000000) ≤ -(4865626058448077485459 / 5000000000000000000000)

theorem Zeta5Irrational.U_395_4 : Uω (aρ 4) (bρ 4) (2506011457479 / 6400000000000) ≤ -(9945652656219027259689 / 10000000000000000000000)

theorem Zeta5Irrational.U_395_5 : Uω (aρ 5) (bρ 5) (2506011457479 / 6400000000000) ≤ -(2570815536680449644243 / 2500000000000000000000)

theorem Zeta5Irrational.U_395_6 : Uω (aρ 6) (bρ 6) (2506011457479 / 6400000000000) ≤ -(2698348668215771873327 / 2500000000000000000000)

theorem Zeta5Irrational.U_395_7 : Uω (aρ 7) (bρ 7) (2506011457479 / 6400000000000) ≤ -(11547234265459707690501 / 10000000000000000000000)

theorem Zeta5Irrational.U_395_8 : Uω (aρ 8) (bρ 8) (2506011457479 / 6400000000000) ≤ -(6329961375780254349371 / 5000000000000000000000)

theorem Zeta5Irrational.U_395_9 : Uω (aρ 9) (bρ 9) (2506011457479 / 6400000000000) ≤ -(14364861738092443484433 / 10000000000000000000000)

theorem Zeta5Irrational.U_395_10 : Uω (aρ 10) (bρ 10) (2506011457479 / 6400000000000) ≤ -(4358171905916996388157 / 2500000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_395 : Uρ (2506011457479 / 6400000000000) ≤ -(13541148812692470789573 / 10000000000000000000000)

theorem Zeta5Irrational.U_396_1 : Uω (aρ 1) (bρ 1) (25143831725049 / 64000000000000) ≤ -(9508343896262421957543 / 10000000000000000000000)

theorem Zeta5Irrational.U_396_2 : Uω (aρ 2) (bρ 2) (25143831725049 / 64000000000000) ≤ -(4785327689087111628957 / 5000000000000000000000)

theorem Zeta5Irrational.U_396_3 : Uω (aρ 3) (bρ 3) (25143831725049 / 64000000000000) ≤ -(9696688535615259549621 / 10000000000000000000000)

theorem Zeta5Irrational.U_396_4 : Uω (aρ 4) (bρ 4) (25143831725049 / 64000000000000) ≤ -(9910323425109448560787 / 10000000000000000000000)

theorem Zeta5Irrational.U_396_5 : Uω (aρ 5) (bρ 5) (25143831725049 / 64000000000000) ≤ -(10246674196579949227919 / 10000000000000000000000)

theorem Zeta5Irrational.U_396_6 : Uω (aρ 6) (bρ 6) (25143831725049 / 64000000000000) ≤ -(5377385588401860750483 / 5000000000000000000000)

theorem Zeta5Irrational.U_396_7 : Uω (aρ 7) (bρ 7) (25143831725049 / 64000000000000) ≤ -(2876317088384850507541 / 2500000000000000000000)

theorem Zeta5Irrational.U_396_8 : Uω (aρ 8) (bρ 8) (25143831725049 / 64000000000000) ≤ -(12612131939922347998239 / 10000000000000000000000)

theorem Zeta5Irrational.U_396_9 : Uω (aρ 9) (bρ 9) (25143831725049 / 64000000000000) ≤ -(7152631511257893339269 / 5000000000000000000000)

theorem Zeta5Irrational.U_396_10 : Uω (aρ 10) (bρ 10) (25143831725049 / 64000000000000) ≤ -(17334347667952915807461 / 10000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_396 : Uρ (25143831725049 / 64000000000000) ≤ -(13509220281971782976273 / 10000000000000000000000)

theorem Zeta5Irrational.U_397_1 : Uω (aρ 1) (bρ 1) (6306887218827 / 16000000000000) ≤ -(9474549302467474731171 / 10000000000000000000000)

theorem Zeta5Irrational.U_397_2 : Uω (aρ 2) (bρ 2) (6306887218827 / 16000000000000) ≤ -(2384161959690752671551 / 2500000000000000000000)

theorem Zeta5Irrational.U_397_3 : Uω (aρ 3) (bρ 3) (6306887218827 / 16000000000000) ≤ -(483112203406672262523 / 500000000000000000000)

theorem Zeta5Irrational.U_397_4 : Uω (aρ 4) (bρ 4) (6306887218827 / 16000000000000) ≤ -(395004750383460144211 / 400000000000000000000)

theorem Zeta5Irrational.U_397_5 : Uω (aρ 5) (bρ 5) (6306887218827 / 16000000000000) ≤ -(10210220176931123704729 / 10000000000000000000000)

theorem Zeta5Irrational.U_397_6 : Uω (aρ 6) (bρ 6) (6306887218827 / 16000000000000) ≤ -(1071629785373233403567 / 1000000000000000000000)

theorem Zeta5Irrational.U_397_7 : Uω (aρ 7) (bρ 7) (6306887218827 / 16000000000000) ≤ -(1146348240106701236677 / 1000000000000000000000)

theorem Zeta5Irrational.U_397_8 : Uω (aρ 8) (bρ 8) (6306887218827 / 16000000000000) ≤ -(785286444664797924013 / 625000000000000000000)

theorem Zeta5Irrational.U_397_9 : Uω (aρ 9) (bρ 9) (6306887218827 / 16000000000000) ≤ -(14246077694202213291207 / 10000000000000000000000)

theorem Zeta5Irrational.U_397_10 : Uω (aρ 10) (bρ 10) (6306887218827 / 16000000000000) ≤ -(17237564134643599097387 / 10000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_397 : Uρ (6306887218827 / 16000000000000) ≤ -(2695507205577800469069 / 2000000000000000000000)

theorem Zeta5Irrational.U_398_1 : Uω (aρ 1) (bρ 1) (12697491587913 / 32000000000000) ≤ -(4703650413353603050421 / 5000000000000000000000)

theorem Zeta5Irrational.U_398_2 : Uω (aρ 2) (bρ 2) (12697491587913 / 32000000000000) ≤ -(9468977808463272198431 / 10000000000000000000000)

theorem Zeta5Irrational.U_398_3 : Uω (aρ 3) (bρ 3) (12697491587913 / 32000000000000) ≤ -(1199213651081101815863 / 1250000000000000000000)

theorem Zeta5Irrational.U_398_4 : Uω (aρ 4) (bρ 4) (12697491587913 / 32000000000000) ≤ -(9805079627997499469213 / 10000000000000000000000)

theorem Zeta5Irrational.U_398_5 : Uω (aρ 5) (bρ 5) (12697491587913 / 32000000000000) ≤ -(10137710016249584730821 / 10000000000000000000000)

theorem Zeta5Irrational.U_398_6 : Uω (aρ 6) (bρ 6) (12697491587913 / 32000000000000) ≤ -(10639797039393326246521 / 10000000000000000000000)

theorem Zeta5Irrational.U_398_7 : Uω (aρ 7) (bρ 7) (12697491587913 / 32000000000000) ≤ -(11380444095054808415279 / 10000000000000000000000)

theorem Zeta5Irrational.U_398_8 : Uω (aρ 8) (bρ 8) (12697491587913 / 32000000000000) ≤ -(12470201145686833426751 / 10000000000000000000000)

theorem Zeta5Irrational.U_398_9 : Uω (aρ 9) (bρ 9) (12697491587913 / 32000000000000) ≤ -(3532230387094757563699 / 2500000000000000000000)

theorem Zeta5Irrational.U_398_10 : Uω (aρ 10) (bρ 10) (12697491587913 / 32000000000000) ≤ -(17048418578553716535903 / 10000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_398 : Uρ (12697491587913 / 32000000000000) ≤ -(13414874358368062389781 / 10000000000000000000000)

theorem Zeta5Irrational.U_399_1 : Uω (aρ 1) (bρ 1) (3195302184543 / 8000000000000) ≤ -(4670250788467362062751 / 5000000000000000000000)

theorem Zeta5Irrational.U_399_2 : Uω (aρ 2) (bρ 2) (3195302184543 / 8000000000000) ≤ -(376070507557605859629 / 400000000000000000000)

theorem Zeta5Irrational.U_399_3 : Uω (aρ 3) (bρ 3) (3195302184543 / 8000000000000) ≤ -(1905128218010882884229 / 2000000000000000000000)

theorem Zeta5Irrational.U_399_4 : Uω (aρ 4) (bρ 4) (3195302184543 / 8000000000000) ≤ -(243388208960620545919 / 250000000000000000000)

theorem Zeta5Irrational.U_399_5 : Uω (aρ 5) (bρ 5) (3195302184543 / 8000000000000) ≤ -(5032861972902583863707 / 5000000000000000000000)

theorem Zeta5Irrational.U_399_6 : Uω (aρ 6) (bρ 6) (3195302184543 / 8000000000000) ≤ -(5281941496501066055649 / 5000000000000000000000)

theorem Zeta5Irrational.U_399_7 : Uω (aρ 7) (bρ 7) (3195302184543 / 8000000000000) ≤ -(1412263374616923864879 / 1250000000000000000000)

theorem Zeta5Irrational.U_399_8 : Uω (aρ 8) (bρ 8) (3195302184543 / 8000000000000) ≤ -(3094189178564688703663 / 2500000000000000000000)

theorem Zeta5Irrational.U_399_9 : Uω (aρ 9) (bρ 9) (3195302184543 / 8000000000000) ≤ -(14013343596192001386277 / 10000000000000000000000)

theorem Zeta5Irrational.U_399_10 : Uω (aρ 10) (bρ 10) (3195302184543 / 8000000000000) ≤ -(843239751853213725649 / 500000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_399 : Uρ (3195302184543 / 8000000000000) ≤ -(13353115432411953119471 / 10000000000000000000000)