Certified arcsine potential bounds (U12)

theorem Zeta5Irrational.U_148_1 : Uω (aρ 1) (bρ 1) (331792728101 / 3200000000000) ≤ -(23307903831274102064587 / 10000000000000000000000)

theorem Zeta5Irrational.U_148_2 : Uω (aρ 2) (bρ 2) (331792728101 / 3200000000000) ≤ -(1472843130775668236677 / 625000000000000000000)

theorem Zeta5Irrational.U_148_3 : Uω (aρ 3) (bρ 3) (331792728101 / 3200000000000) ≤ -(24112104277449450185939 / 10000000000000000000000)

theorem Zeta5Irrational.U_148_4 : Uω (aρ 4) (bρ 4) (331792728101 / 3200000000000) ≤ -(25134222523221480039377 / 10000000000000000000000)

theorem Zeta5Irrational.U_148_5 : Uω (aρ 5) (bρ 5) (331792728101 / 3200000000000) ≤ -(13555463086437859904049 / 5000000000000000000000)

theorem Zeta5Irrational.U_148_6 : Uω (aρ 6) (bρ 6) (331792728101 / 3200000000000) ≤ -(1644480720294708417623 / 500000000000000000000)

theorem Zeta5Irrational.U_148_7 : Uω (aρ 7) (bρ 7) (331792728101 / 3200000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_148_8 : Uω (aρ 8) (bρ 8) (331792728101 / 3200000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_148_9 : Uω (aρ 9) (bρ 9) (331792728101 / 3200000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_148_10 : Uω (aρ 10) (bρ 10) (331792728101 / 3200000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_148_11 : Uω (aρ 11) (bρ 11) (331792728101 / 3200000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_148_12 : Uω (aρ 12) (bρ 12) (331792728101 / 3200000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_148_13 : Uω (aρ 13) (bρ 13) (331792728101 / 3200000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_148_14 : Uω (aρ 14) (bρ 14) (331792728101 / 3200000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_148_15 : Uω (aρ 15) (bρ 15) (331792728101 / 3200000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_148_16 : Uω (aρ 16) (bρ 16) (331792728101 / 3200000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_148 : Uρ (331792728101 / 3200000000000) ≤ -(23583366397967708671417 / 10000000000000000000000)

theorem Zeta5Irrational.U_149_1 : Uω (aρ 1) (bρ 1) (3340349625797 / 32000000000000) ≤ -(2904509483478323326409 / 1250000000000000000000)

theorem Zeta5Irrational.U_149_2 : Uω (aρ 2) (bρ 2) (3340349625797 / 32000000000000) ≤ -(2936465129834332087859 / 1250000000000000000000)

theorem Zeta5Irrational.U_149_3 : Uω (aρ 3) (bρ 3) (3340349625797 / 32000000000000) ≤ -(6008485673465917970041 / 2500000000000000000000)

theorem Zeta5Irrational.U_149_4 : Uω (aρ 4) (bρ 4) (3340349625797 / 32000000000000) ≤ -(25046692976457419243763 / 10000000000000000000000)

theorem Zeta5Irrational.U_149_5 : Uω (aρ 5) (bρ 5) (3340349625797 / 32000000000000) ≤ -(26999442017161149412787 / 10000000000000000000000)

theorem Zeta5Irrational.U_149_6 : Uω (aρ 6) (bρ 6) (3340349625797 / 32000000000000) ≤ -(16283427578860002476577 / 5000000000000000000000)

theorem Zeta5Irrational.U_149_7 : Uω (aρ 7) (bρ 7) (3340349625797 / 32000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_149_8 : Uω (aρ 8) (bρ 8) (3340349625797 / 32000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_149_9 : Uω (aρ 9) (bρ 9) (3340349625797 / 32000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_149_10 : Uω (aρ 10) (bρ 10) (3340349625797 / 32000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_149 : Uρ (3340349625797 / 32000000000000) ≤ -(2353883295077089915433 / 1000000000000000000000)

theorem Zeta5Irrational.U_150_1 : Uω (aρ 1) (bρ 1) (420346496323 / 4000000000000) ≤ -(5791190081092174150987 / 2500000000000000000000)

theorem Zeta5Irrational.U_150_2 : Uω (aρ 2) (bρ 2) (420346496323 / 4000000000000) ≤ -(2927311680014733944333 / 1250000000000000000000)

theorem Zeta5Irrational.U_150_3 : Uω (aρ 3) (bρ 3) (420346496323 / 4000000000000) ≤ -(93579659246677020249 / 39062500000000000000)

theorem Zeta5Irrational.U_150_4 : Uω (aρ 4) (bρ 4) (420346496323 / 4000000000000) ≤ -(4991989407247450880853 / 2000000000000000000000)

theorem Zeta5Irrational.U_150_5 : Uω (aρ 5) (bρ 5) (420346496323 / 4000000000000) ≤ -(1344466957828672674537 / 500000000000000000000)

theorem Zeta5Irrational.U_150_6 : Uω (aρ 6) (bρ 6) (420346496323 / 4000000000000) ≤ -(3226744951560163699253 / 1000000000000000000000)

theorem Zeta5Irrational.U_150_7 : Uω (aρ 7) (bρ 7) (420346496323 / 4000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_150_8 : Uω (aρ 8) (bρ 8) (420346496323 / 4000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_150_9 : Uω (aρ 9) (bρ 9) (420346496323 / 4000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_150_10 : Uω (aρ 10) (bρ 10) (420346496323 / 4000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_150 : Uρ (420346496323 / 4000000000000) ≤ -(23496330052534074716271 / 10000000000000000000000)

theorem Zeta5Irrational.U_151_1 : Uω (aρ 1) (bρ 1) (3385194315371 / 32000000000000) ≤ -(2886743742383077728029 / 1250000000000000000000)

theorem Zeta5Irrational.U_151_2 : Uω (aρ 2) (bρ 2) (3385194315371 / 32000000000000) ≤ -(4669159877652684528577 / 2000000000000000000000)

theorem Zeta5Irrational.U_151_3 : Uω (aρ 3) (bρ 3) (3385194315371 / 32000000000000) ≤ -(23879444915266449414989 / 10000000000000000000000)

theorem Zeta5Irrational.U_151_4 : Uω (aρ 4) (bρ 4) (3385194315371 / 32000000000000) ≤ -(24873970382882411377119 / 10000000000000000000000)

theorem Zeta5Irrational.U_151_5 : Uω (aρ 5) (bρ 5) (3385194315371 / 32000000000000) ≤ -(26780580354809959357677 / 10000000000000000000000)

theorem Zeta5Irrational.U_151_6 : Uω (aρ 6) (bρ 6) (3385194315371 / 32000000000000) ≤ -(3198718174266971398463 / 1000000000000000000000)

theorem Zeta5Irrational.U_151_7 : Uω (aρ 7) (bρ 7) (3385194315371 / 32000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_151_8 : Uω (aρ 8) (bρ 8) (3385194315371 / 32000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_151_9 : Uω (aρ 9) (bρ 9) (3385194315371 / 32000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_151_10 : Uω (aρ 10) (bρ 10) (3385194315371 / 32000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_151 : Uρ (3385194315371 / 32000000000000) ≤ -(4691104214003087231947 / 2000000000000000000000)

theorem Zeta5Irrational.U_152_1 : Uω (aρ 1) (bρ 1) (1703808330079 / 16000000000000) ≤ -(4604727520682233243737 / 2000000000000000000000)

theorem Zeta5Irrational.U_152_2 : Uω (aρ 2) (bρ 2) (1703808330079 / 16000000000000) ≤ -(5818407786757043322733 / 2500000000000000000000)

theorem Zeta5Irrational.U_152_3 : Uω (aρ 3) (bρ 3) (1703808330079 / 16000000000000) ≤ -(11901544890733755628069 / 5000000000000000000000)

theorem Zeta5Irrational.U_152_4 : Uω (aρ 4) (bρ 4) (1703808330079 / 16000000000000) ≤ -(309859363700855048777 / 125000000000000000000)

theorem Zeta5Irrational.U_152_5 : Uω (aρ 5) (bρ 5) (1703808330079 / 16000000000000) ≤ -(833535311543117281089 / 312500000000000000000)

theorem Zeta5Irrational.U_152_6 : Uω (aρ 6) (bρ 6) (1703808330079 / 16000000000000) ≤ -(31722978131427743478867 / 10000000000000000000000)

theorem Zeta5Irrational.U_152_7 : Uω (aρ 7) (bρ 7) (1703808330079 / 16000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_152_8 : Uω (aρ 8) (bρ 8) (1703808330079 / 16000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_152_9 : Uω (aρ 9) (bρ 9) (1703808330079 / 16000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_152_10 : Uω (aρ 10) (bρ 10) (1703808330079 / 16000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_152 : Uρ (1703808330079 / 16000000000000) ≤ -(23416159595012170387401 / 10000000000000000000000)

theorem Zeta5Irrational.U_153_1 : Uω (aρ 1) (bρ 1) (686007800989 / 6400000000000) ≤ -(286922704474371271327 / 125000000000000000000)

theorem Zeta5Irrational.U_153_2 : Uω (aρ 2) (bρ 2) (686007800989 / 6400000000000) ≤ -(23201981147737440312697 / 10000000000000000000000)

theorem Zeta5Irrational.U_153_3 : Uω (aρ 3) (bρ 3) (686007800989 / 6400000000000) ≤ -(949092729089347156587 / 400000000000000000000)

theorem Zeta5Irrational.U_153_4 : Uω (aρ 4) (bρ 4) (686007800989 / 6400000000000) ≤ -(6176067409942879644687 / 2500000000000000000000)

theorem Zeta5Irrational.U_153_5 : Uω (aρ 5) (bρ 5) (686007800989 / 6400000000000) ≤ -(5313390771513018446107 / 2000000000000000000000)

theorem Zeta5Irrational.U_153_6 : Uω (aρ 6) (bρ 6) (686007800989 / 6400000000000) ≤ -(15736257519806563902167 / 5000000000000000000000)

theorem Zeta5Irrational.U_153_7 : Uω (aρ 7) (bρ 7) (686007800989 / 6400000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_153_8 : Uω (aρ 8) (bρ 8) (686007800989 / 6400000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_153_9 : Uω (aρ 9) (bρ 9) (686007800989 / 6400000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_153_10 : Uω (aρ 10) (bρ 10) (686007800989 / 6400000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_153 : Uρ (686007800989 / 6400000000000) ≤ -(23378058521070381777983 / 10000000000000000000000)

theorem Zeta5Irrational.U_154_1 : Uω (aρ 1) (bρ 1) (863115337433 / 8000000000000) ≤ -(22884479388127094268989 / 10000000000000000000000)

theorem Zeta5Irrational.U_154_2 : Uω (aρ 2) (bρ 2) (863115337433 / 8000000000000) ≤ -(2891355248039883648733 / 1250000000000000000000)

theorem Zeta5Irrational.U_154_3 : Uω (aρ 3) (bρ 3) (863115337433 / 8000000000000) ≤ -(591303033137199082917 / 250000000000000000000)

theorem Zeta5Irrational.U_154_4 : Uω (aρ 4) (bρ 4) (863115337433 / 8000000000000) ≤ -(24620518847931819427187 / 10000000000000000000000)

theorem Zeta5Irrational.U_154_5 : Uω (aρ 5) (bρ 5) (863115337433 / 8000000000000) ≤ -(1653876205589663543733 / 625000000000000000000)

theorem Zeta5Irrational.U_154_6 : Uω (aρ 6) (bρ 6) (863115337433 / 8000000000000) ≤ -(15616992344826031747609 / 5000000000000000000000)

theorem Zeta5Irrational.U_154_7 : Uω (aρ 7) (bρ 7) (863115337433 / 8000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_154_8 : Uω (aρ 8) (bρ 8) (863115337433 / 8000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_154_9 : Uω (aρ 9) (bρ 9) (863115337433 / 8000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_154_10 : Uω (aρ 10) (bρ 10) (863115337433 / 8000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_154 : Uρ (863115337433 / 8000000000000) ≤ -(23341071564045878495493 / 10000000000000000000000)

theorem Zeta5Irrational.U_155_1 : Uω (aρ 1) (bρ 1) (6927345044251 / 64000000000000) ≤ -(22849990415668781578591 / 10000000000000000000000)

theorem Zeta5Irrational.U_155_2 : Uω (aρ 2) (bρ 2) (6927345044251 / 64000000000000) ≤ -(23095461694982195708649 / 10000000000000000000000)

theorem Zeta5Irrational.U_155_3 : Uω (aρ 3) (bρ 3) (6927345044251 / 64000000000000) ≤ -(11807367817896096737809 / 5000000000000000000000)

theorem Zeta5Irrational.U_155_4 : Uω (aρ 4) (bρ 4) (6927345044251 / 64000000000000) ≤ -(12289456342288177086599 / 5000000000000000000000)

theorem Zeta5Irrational.U_155_5 : Uω (aρ 5) (bρ 5) (6927345044251 / 64000000000000) ≤ -(5282001544501092498839 / 2000000000000000000000)

theorem Zeta5Irrational.U_155_6 : Uω (aρ 6) (bρ 6) (6927345044251 / 64000000000000) ≤ -(31118732925594350230399 / 10000000000000000000000)

theorem Zeta5Irrational.U_155_7 : Uω (aρ 7) (bρ 7) (6927345044251 / 64000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_155_8 : Uω (aρ 8) (bρ 8) (6927345044251 / 64000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_155_9 : Uω (aρ 9) (bρ 9) (6927345044251 / 64000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_155_10 : Uω (aρ 10) (bρ 10) (6927345044251 / 64000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_155 : Uρ (6927345044251 / 64000000000000) ≤ -(11661479184507404062013 / 5000000000000000000000)

theorem Zeta5Irrational.U_156_1 : Uω (aρ 1) (bρ 1) (3474883694519 / 32000000000000) ≤ -(5703905005074826194883 / 2500000000000000000000)

theorem Zeta5Irrational.U_156_2 : Uω (aρ 2) (bρ 2) (3474883694519 / 32000000000000) ≤ -(115301032043345084123 / 50000000000000000000)

theorem Zeta5Irrational.U_156_3 : Uω (aρ 3) (bρ 3) (3474883694519 / 32000000000000) ≤ -(23577490354072033648947 / 10000000000000000000000)

theorem Zeta5Irrational.U_156_4 : Uω (aρ 4) (bρ 4) (3474883694519 / 32000000000000) ≤ -(24537483910791336289901 / 10000000000000000000000)

theorem Zeta5Irrational.U_156_5 : Uω (aρ 5) (bρ 5) (3474883694519 / 32000000000000) ≤ -(26358294867270100871003 / 10000000000000000000000)

theorem Zeta5Irrational.U_156_6 : Uω (aρ 6) (bρ 6) (3474883694519 / 32000000000000) ≤ -(15502973708874956289793 / 5000000000000000000000)

theorem Zeta5Irrational.U_156_7 : Uω (aρ 7) (bρ 7) (3474883694519 / 32000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_156_8 : Uω (aρ 8) (bρ 8) (3474883694519 / 32000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_156_9 : Uω (aρ 9) (bρ 9) (3474883694519 / 32000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_156_10 : Uω (aρ 10) (bρ 10) (3474883694519 / 32000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_156 : Uρ (3474883694519 / 32000000000000) ≤ -(23305081601715584225839 / 10000000000000000000000)

theorem Zeta5Irrational.U_157_1 : Uω (aρ 1) (bρ 1) (278887589353 / 2560000000000) ≤ -(22781367389197025760763 / 10000000000000000000000)

theorem Zeta5Irrational.U_157_2 : Uω (aρ 2) (bρ 2) (278887589353 / 2560000000000) ≤ -(11512537621657838256657 / 5000000000000000000000)

theorem Zeta5Irrational.U_157_3 : Uω (aρ 3) (bρ 3) (278887589353 / 2560000000000) ≤ -(2942548052630913630127 / 1250000000000000000000)

theorem Zeta5Irrational.U_157_4 : Uω (aρ 4) (bρ 4) (278887589353 / 2560000000000) ≤ -(3062028872361546944299 / 1250000000000000000000)

theorem Zeta5Irrational.U_157_5 : Uω (aρ 5) (bρ 5) (278887589353 / 2560000000000) ≤ -(26306876994912978474327 / 10000000000000000000000)

theorem Zeta5Irrational.U_157_6 : Uω (aρ 6) (bρ 6) (278887589353 / 2560000000000) ≤ -(15447744896504633414501 / 5000000000000000000000)

theorem Zeta5Irrational.U_157_7 : Uω (aρ 7) (bρ 7) (278887589353 / 2560000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_157_8 : Uω (aρ 8) (bρ 8) (278887589353 / 2560000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_157_9 : Uω (aρ 9) (bρ 9) (278887589353 / 2560000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_157_10 : Uω (aρ 10) (bρ 10) (278887589353 / 2560000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_157_11 : Uω (aρ 11) (bρ 11) (278887589353 / 2560000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_157_12 : Uω (aρ 12) (bρ 12) (278887589353 / 2560000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_157_13 : Uω (aρ 13) (bρ 13) (278887589353 / 2560000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_157_14 : Uω (aρ 14) (bρ 14) (278887589353 / 2560000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_157_15 : Uω (aρ 15) (bρ 15) (278887589353 / 2560000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_157_16 : Uω (aρ 16) (bρ 16) (278887589353 / 2560000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_157 : Uρ (278887589353 / 2560000000000) ≤ -(931497196827963978981 / 400000000000000000000)

theorem Zeta5Irrational.U_158_1 : Uω (aρ 1) (bρ 1) (1748653019653 / 16000000000000) ≤ -(11373615858935949105329 / 5000000000000000000000)

theorem Zeta5Irrational.U_158_2 : Uω (aρ 2) (bρ 2) (1748653019653 / 16000000000000) ≤ -(22990067326181240245647 / 10000000000000000000000)

theorem Zeta5Irrational.U_158_3 : Uω (aρ 3) (bρ 3) (1748653019653 / 16000000000000) ≤ -(1175170839473725169687 / 500000000000000000000)

theorem Zeta5Irrational.U_158_4 : Uω (aρ 4) (bρ 4) (1748653019653 / 16000000000000) ≤ -(12227576180934471999219 / 5000000000000000000000)

theorem Zeta5Irrational.U_158_5 : Uω (aρ 5) (bρ 5) (1748653019653 / 16000000000000) ≤ -(13127875225417848178601 / 5000000000000000000000)

theorem Zeta5Irrational.U_158_6 : Uω (aρ 6) (bρ 6) (1748653019653 / 16000000000000) ≤ -(30787234291560992907967 / 10000000000000000000000)

theorem Zeta5Irrational.U_158_7 : Uω (aρ 7) (bρ 7) (1748653019653 / 16000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_158_8 : Uω (aρ 8) (bρ 8) (1748653019653 / 16000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_158_9 : Uω (aρ 9) (bρ 9) (1748653019653 / 16000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_158_10 : Uω (aρ 10) (bρ 10) (1748653019653 / 16000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_158 : Uρ (1748653019653 / 16000000000000) ≤ -(23269992986572398537807 / 10000000000000000000000)

theorem Zeta5Irrational.U_159_1 : Uω (aρ 1) (bρ 1) (7017034423399 / 64000000000000) ≤ -(5678303052512994256621 / 2500000000000000000000)

theorem Zeta5Irrational.U_159_2 : Uω (aρ 2) (bρ 2) (7017034423399 / 64000000000000) ≤ -(22955181793716472346763 / 10000000000000000000000)

theorem Zeta5Irrational.U_159_3 : Uω (aρ 3) (bρ 3) (7017034423399 / 64000000000000) ≤ -(11733293211981849575587 / 5000000000000000000000)

theorem Zeta5Irrational.U_159_4 : Uω (aρ 4) (bρ 4) (7017034423399 / 64000000000000) ≤ -(6103561638252420282721 / 2500000000000000000000)

theorem Zeta5Irrational.U_159_5 : Uω (aρ 5) (bρ 5) (7017034423399 / 64000000000000) ≤ -(6551227913151442296359 / 2500000000000000000000)

theorem Zeta5Irrational.U_159_6 : Uω (aρ 6) (bρ 6) (7017034423399 / 64000000000000) ≤ -(6136213241512007746819 / 2000000000000000000000)

theorem Zeta5Irrational.U_159_7 : Uω (aρ 7) (bρ 7) (7017034423399 / 64000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_159_8 : Uω (aρ 8) (bρ 8) (7017034423399 / 64000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_159_9 : Uω (aρ 9) (bρ 9) (7017034423399 / 64000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_159_10 : Uω (aρ 10) (bρ 10) (7017034423399 / 64000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_159 : Uρ (7017034423399 / 64000000000000) ≤ -(11626380669416506316129 / 5000000000000000000000)