Certified arcsine potential bounds (U20)

theorem Zeta5Irrational.U_244_1 : Uω (aρ 1) (bρ 1) (132802102197 / 640000000000) ≤ -(80211196028750566739 / 50000000000000000000)

theorem Zeta5Irrational.U_244_2 : Uω (aρ 2) (bρ 2) (132802102197 / 640000000000) ≤ -(1010215922572068434639 / 625000000000000000000)

theorem Zeta5Irrational.U_244_3 : Uω (aρ 3) (bρ 3) (132802102197 / 640000000000) ≤ -(8206032948370699617277 / 5000000000000000000000)

theorem Zeta5Irrational.U_244_4 : Uω (aρ 4) (bρ 4) (132802102197 / 640000000000) ≤ -(8422407421941390401861 / 5000000000000000000000)

theorem Zeta5Irrational.U_244_5 : Uω (aρ 5) (bρ 5) (132802102197 / 640000000000) ≤ -(877963093041325964747 / 500000000000000000000)

theorem Zeta5Irrational.U_244_6 : Uω (aρ 6) (bρ 6) (132802102197 / 640000000000) ≤ -(4684014389455247979343 / 2500000000000000000000)

theorem Zeta5Irrational.U_244_7 : Uω (aρ 7) (bρ 7) (132802102197 / 640000000000) ≤ -(20809744920160066222079 / 10000000000000000000000)

theorem Zeta5Irrational.U_244_8 : Uω (aρ 8) (bρ 8) (132802102197 / 640000000000) ≤ -(26362368852389073231951 / 10000000000000000000000)

theorem Zeta5Irrational.U_244_9 : Uω (aρ 9) (bρ 9) (132802102197 / 640000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_244_10 : Uω (aρ 10) (bρ 10) (132802102197 / 640000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_244_11 : Uω (aρ 11) (bρ 11) (132802102197 / 640000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_244_12 : Uω (aρ 12) (bρ 12) (132802102197 / 640000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_244_13 : Uω (aρ 13) (bρ 13) (132802102197 / 640000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_244_14 : Uω (aρ 14) (bρ 14) (132802102197 / 640000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_244_15 : Uω (aρ 15) (bρ 15) (132802102197 / 640000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_244_16 : Uω (aρ 16) (bρ 16) (132802102197 / 640000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_244 : Uρ (132802102197 / 640000000000) ≤ -(2416425266355531027053 / 1250000000000000000000)

theorem Zeta5Irrational.U_245_1 : Uω (aρ 1) (bρ 1) (6674225226937 / 32000000000000) ≤ -(15989341814769083441683 / 10000000000000000000000)

theorem Zeta5Irrational.U_245_2 : Uω (aρ 2) (bρ 2) (6674225226937 / 32000000000000) ≤ -(251717216120021689271 / 156250000000000000000)

theorem Zeta5Irrational.U_245_3 : Uω (aρ 3) (bρ 3) (6674225226937 / 32000000000000) ≤ -(16357129540002021346027 / 10000000000000000000000)

theorem Zeta5Irrational.U_245_4 : Uω (aρ 4) (bρ 4) (6674225226937 / 32000000000000) ≤ -(839366889642839072517 / 500000000000000000000)

theorem Zeta5Irrational.U_245_5 : Uω (aρ 5) (bρ 5) (6674225226937 / 32000000000000) ≤ -(8748589672698357586477 / 5000000000000000000000)

theorem Zeta5Irrational.U_245_6 : Uω (aρ 6) (bρ 6) (6674225226937 / 32000000000000) ≤ -(18665037439110731528699 / 10000000000000000000000)

theorem Zeta5Irrational.U_245_7 : Uω (aρ 7) (bρ 7) (6674225226937 / 32000000000000) ≤ -(129481655524811388393 / 62500000000000000000)

theorem Zeta5Irrational.U_245_8 : Uω (aρ 8) (bρ 8) (6674225226937 / 32000000000000) ≤ -(26081207921134859408713 / 10000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_245 : Uρ (6674225226937 / 32000000000000) ≤ -(19280957920972008264119 / 10000000000000000000000)

theorem Zeta5Irrational.U_246_1 : Uω (aρ 1) (bρ 1) (838543168003 / 4000000000000) ≤ -(1992090348424161097649 / 1250000000000000000000)

theorem Zeta5Irrational.U_246_2 : Uω (aρ 2) (bρ 2) (838543168003 / 4000000000000) ≤ -(8028317158933071913149 / 5000000000000000000000)

theorem Zeta5Irrational.U_246_3 : Uω (aρ 3) (bρ 3) (838543168003 / 4000000000000) ≤ -(4075623479472093816281 / 2500000000000000000000)

theorem Zeta5Irrational.U_246_4 : Uω (aρ 4) (bρ 4) (838543168003 / 4000000000000) ≤ -(16730191195247513018179 / 10000000000000000000000)

theorem Zeta5Irrational.U_246_5 : Uω (aρ 5) (bρ 5) (838543168003 / 4000000000000) ≤ -(8717743323121730710593 / 5000000000000000000000)

theorem Zeta5Irrational.U_246_6 : Uω (aρ 6) (bρ 6) (838543168003 / 4000000000000) ≤ -(18594544327930489474517 / 10000000000000000000000)

theorem Zeta5Irrational.U_246_7 : Uω (aρ 7) (bρ 7) (838543168003 / 4000000000000) ≤ -(825015431120082058003 / 400000000000000000000)

theorem Zeta5Irrational.U_246_8 : Uω (aρ 8) (bρ 8) (838543168003 / 4000000000000) ≤ -(3227522382415953287113 / 1250000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_246 : Uρ (838543168003 / 4000000000000) ≤ -(961624510270881730459 / 500000000000000000000)

theorem Zeta5Irrational.U_247_1 : Uω (aρ 1) (bρ 1) (6742465461111 / 32000000000000) ≤ -(15884379209042150851217 / 10000000000000000000000)

theorem Zeta5Irrational.U_247_2 : Uω (aρ 2) (bρ 2) (6742465461111 / 32000000000000) ≤ -(16003649191942420646063 / 10000000000000000000000)

theorem Zeta5Irrational.U_247_3 : Uω (aρ 3) (bρ 3) (6742465461111 / 32000000000000) ≤ -(8124077874733012623601 / 5000000000000000000000)

theorem Zeta5Irrational.U_247_4 : Uω (aρ 4) (bρ 4) (6742465461111 / 32000000000000) ≤ -(16673371250703288171891 / 10000000000000000000000)

theorem Zeta5Irrational.U_247_5 : Uω (aρ 5) (bρ 5) (6742465461111 / 32000000000000) ≤ -(43435447039729323767 / 25000000000000000000)

theorem Zeta5Irrational.U_247_6 : Uω (aρ 6) (bρ 6) (6742465461111 / 32000000000000) ≤ -(4631142522539577805907 / 2500000000000000000000)

theorem Zeta5Irrational.U_247_7 : Uω (aρ 7) (bρ 7) (6742465461111 / 32000000000000) ≤ -(20534683322764266391341 / 10000000000000000000000)

theorem Zeta5Irrational.U_247_8 : Uω (aρ 8) (bρ 8) (6742465461111 / 32000000000000) ≤ -(25575639136592379083153 / 10000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_247 : Uρ (6742465461111 / 32000000000000) ≤ -(19185673420397004360467 / 10000000000000000000000)

theorem Zeta5Irrational.U_248_1 : Uω (aρ 1) (bρ 1) (3388292789099 / 16000000000000) ≤ -(15832308210675581165643 / 10000000000000000000000)

theorem Zeta5Irrational.U_248_2 : Uω (aρ 2) (bρ 2) (3388292789099 / 16000000000000) ≤ -(7975471737047489165407 / 5000000000000000000000)

theorem Zeta5Irrational.U_248_3 : Uω (aρ 3) (bρ 3) (3388292789099 / 16000000000000) ≤ -(3238822361460214488721 / 2000000000000000000000)

theorem Zeta5Irrational.U_248_4 : Uω (aρ 4) (bρ 4) (3388292789099 / 16000000000000) ≤ -(3323374844885987262029 / 2000000000000000000000)

theorem Zeta5Irrational.U_248_5 : Uω (aρ 5) (bρ 5) (3388292789099 / 16000000000000) ≤ -(3462650200390808338077 / 2000000000000000000000)

theorem Zeta5Irrational.U_248_6 : Uω (aρ 6) (bρ 6) (3388292789099 / 16000000000000) ≤ -(18455106786157723315289 / 10000000000000000000000)

theorem Zeta5Irrational.U_248_7 : Uω (aρ 7) (bρ 7) (3388292789099 / 16000000000000) ≤ -(20444934186107947075261 / 10000000000000000000000)

theorem Zeta5Irrational.U_248_8 : Uω (aρ 8) (bρ 8) (3388292789099 / 16000000000000) ≤ -(792029153694985536973 / 312500000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_248 : Uρ (3388292789099 / 16000000000000) ≤ -(3828053887706228677047 / 2000000000000000000000)

theorem Zeta5Irrational.U_249_1 : Uω (aρ 1) (bρ 1) (1362141139057 / 6400000000000) ≤ -(7890253483925033164729 / 5000000000000000000000)

theorem Zeta5Irrational.U_249_2 : Uω (aρ 2) (bρ 2) (1362141139057 / 6400000000000) ≤ -(3179702846290115685933 / 2000000000000000000000)

theorem Zeta5Irrational.U_249_3 : Uω (aρ 3) (bρ 3) (1362141139057 / 6400000000000) ≤ -(3228071783260219938387 / 2000000000000000000000)

theorem Zeta5Irrational.U_249_4 : Uω (aρ 4) (bρ 4) (1362141139057 / 6400000000000) ≤ -(16560696445683286189297 / 10000000000000000000000)

theorem Zeta5Irrational.U_249_5 : Uω (aρ 5) (bρ 5) (1362141139057 / 6400000000000) ≤ -(1725269844467385308997 / 1000000000000000000000)

theorem Zeta5Irrational.U_249_6 : Uω (aρ 6) (bρ 6) (1362141139057 / 6400000000000) ≤ -(735445866576952836003 / 400000000000000000000)

theorem Zeta5Irrational.U_249_7 : Uω (aρ 7) (bρ 7) (1362141139057 / 6400000000000) ≤ -(10178057967148668099869 / 5000000000000000000000)

theorem Zeta5Irrational.U_249_8 : Uω (aρ 8) (bρ 8) (1362141139057 / 6400000000000) ≤ -(201008430917706393269 / 80000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_249 : Uρ (1362141139057 / 6400000000000) ≤ -(19096097579846410691343 / 10000000000000000000000)

theorem Zeta5Irrational.U_250_1 : Uω (aρ 1) (bρ 1) (1711206453093 / 8000000000000) ≤ -(15728972699799062262617 / 10000000000000000000000)

theorem Zeta5Irrational.U_250_2 : Uω (aρ 2) (bρ 2) (1711206453093 / 8000000000000) ≤ -(7923179288548330911731 / 5000000000000000000000)

theorem Zeta5Irrational.U_250_3 : Uω (aρ 3) (bρ 3) (1711206453093 / 8000000000000) ≤ -(1608689395258738273783 / 1000000000000000000000)

theorem Zeta5Irrational.U_250_4 : Uω (aρ 4) (bρ 4) (1711206453093 / 8000000000000) ≤ -(16504834306304953880329 / 10000000000000000000000)

theorem Zeta5Irrational.U_250_5 : Uω (aρ 5) (bρ 5) (1711206453093 / 8000000000000) ≤ -(17192516474548806354561 / 10000000000000000000000)

theorem Zeta5Irrational.U_250_6 : Uω (aρ 6) (bρ 6) (1711206453093 / 8000000000000) ≤ -(9158841077746681639 / 5000000000000000000)

theorem Zeta5Irrational.U_250_7 : Uω (aρ 7) (bρ 7) (1711206453093 / 8000000000000) ≤ -(4053641396807687271301 / 2000000000000000000000)

theorem Zeta5Irrational.U_250_8 : Uω (aρ 8) (bρ 8) (1711206453093 / 8000000000000) ≤ -(24917441486620581692963 / 10000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_250 : Uρ (1711206453093 / 8000000000000) ≤ -(2381627086733213812727 / 1250000000000000000000)

theorem Zeta5Irrational.U_251_1 : Uω (aρ 1) (bρ 1) (13723771741831 / 64000000000000) ≤ -(15703304824046411768787 / 10000000000000000000000)

theorem Zeta5Irrational.U_251_2 : Uω (aρ 2) (bρ 2) (13723771741831 / 64000000000000) ≤ -(15820382455700095831141 / 10000000000000000000000)

theorem Zeta5Irrational.U_251_3 : Uω (aρ 3) (bρ 3) (13723771741831 / 64000000000000) ≤ -(8030134240491908589773 / 5000000000000000000000)

theorem Zeta5Irrational.U_251_4 : Uω (aρ 4) (bρ 4) (13723771741831 / 64000000000000) ≤ -(1029813780661990088497 / 625000000000000000000)

theorem Zeta5Irrational.U_251_5 : Uω (aρ 5) (bρ 5) (13723771741831 / 64000000000000) ≤ -(17162563024561307747881 / 10000000000000000000000)

theorem Zeta5Irrational.U_251_6 : Uω (aρ 6) (bρ 6) (13723771741831 / 64000000000000) ≤ -(18283633438707248311039 / 10000000000000000000000)

theorem Zeta5Irrational.U_251_7 : Uω (aρ 7) (bρ 7) (13723771741831 / 64000000000000) ≤ -(4044917394737842997651 / 2000000000000000000000)

theorem Zeta5Irrational.U_251_8 : Uω (aρ 8) (bρ 8) (13723771741831 / 64000000000000) ≤ -(24816587177418204207001 / 10000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_251 : Uρ (13723771741831 / 64000000000000) ≤ -(19031849196494214193577 / 10000000000000000000000)

theorem Zeta5Irrational.U_252_1 : Uω (aρ 1) (bρ 1) (6878945929459 / 32000000000000) ≤ -(7838851334268503496127 / 5000000000000000000000)

theorem Zeta5Irrational.U_252_2 : Uω (aρ 2) (bρ 2) (6878945929459 / 32000000000000) ≤ -(3158894733825103070931 / 2000000000000000000000)

theorem Zeta5Irrational.U_252_3 : Uω (aρ 3) (bρ 3) (6878945929459 / 32000000000000) ≤ -(8016856921198687784309 / 5000000000000000000000)

theorem Zeta5Irrational.U_252_4 : Uω (aρ 4) (bρ 4) (6878945929459 / 32000000000000) ≤ -(8224642129649983668167 / 5000000000000000000000)

theorem Zeta5Irrational.U_252_5 : Uω (aρ 5) (bρ 5) (6878945929459 / 32000000000000) ≤ -(3426540102006141285593 / 2000000000000000000000)

theorem Zeta5Irrational.U_252_6 : Uω (aρ 6) (bρ 6) (6878945929459 / 32000000000000) ≤ -(18249705866105557760711 / 10000000000000000000000)

theorem Zeta5Irrational.U_252_7 : Uω (aρ 7) (bρ 7) (6878945929459 / 32000000000000) ≤ -(20181186557770656385763 / 10000000000000000000000)

theorem Zeta5Irrational.U_252_8 : Uω (aρ 8) (bρ 8) (6878945929459 / 32000000000000) ≤ -(6179463379973671333507 / 2500000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_252 : Uρ (6878945929459 / 32000000000000) ≤ -(19010913855813137707793 / 10000000000000000000000)

theorem Zeta5Irrational.U_253_1 : Uω (aρ 1) (bρ 1) (2758402395201 / 12800000000000) ≤ -(31304331795127864129 / 20000000000000000000)

theorem Zeta5Irrational.U_253_2 : Uω (aρ 2) (bρ 2) (2758402395201 / 12800000000000) ≤ -(3153726373802742696967 / 2000000000000000000000)

theorem Zeta5Irrational.U_253_3 : Uω (aρ 3) (bρ 3) (2758402395201 / 12800000000000) ≤ -(16007229660263138625569 / 10000000000000000000000)

theorem Zeta5Irrational.U_253_4 : Uω (aρ 4) (bρ 4) (2758402395201 / 12800000000000) ≤ -(4105406294596253327 / 2500000000000000000)

theorem Zeta5Irrational.U_253_5 : Uω (aρ 5) (bρ 5) (2758402395201 / 12800000000000) ≤ -(4275732092910269981083 / 2500000000000000000000)

theorem Zeta5Irrational.U_253_6 : Uω (aρ 6) (bρ 6) (2758402395201 / 12800000000000) ≤ -(9107949270071717081159 / 5000000000000000000000)

theorem Zeta5Irrational.U_253_7 : Uω (aρ 7) (bρ 7) (2758402395201 / 12800000000000) ≤ -(2013800325814052412029 / 1000000000000000000000)

theorem Zeta5Irrational.U_253_8 : Uω (aρ 8) (bρ 8) (2758402395201 / 12800000000000) ≤ -(24621121171626664245687 / 10000000000000000000000)

theorem Zeta5Irrational.U_253_9 : Uω (aρ 9) (bρ 9) (2758402395201 / 12800000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_253_10 : Uω (aρ 10) (bρ 10) (2758402395201 / 12800000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_253 : Uρ (2758402395201 / 12800000000000) ≤ -(4747549936875150188239 / 2500000000000000000000)

theorem Zeta5Irrational.U_254_1 : Uω (aρ 1) (bρ 1) (3456533023273 / 16000000000000) ≤ -(15626694177986153223101 / 10000000000000000000000)

theorem Zeta5Irrational.U_254_2 : Uω (aρ 2) (bρ 2) (3456533023273 / 16000000000000) ≤ -(15742856709703212177573 / 10000000000000000000000)

theorem Zeta5Irrational.U_254_3 : Uω (aρ 3) (bρ 3) (3456533023273 / 16000000000000) ≤ -(1997601945127060592757 / 1250000000000000000000)

theorem Zeta5Irrational.U_254_4 : Uω (aρ 4) (bρ 4) (3456533023273 / 16000000000000) ≤ -(4098510704363691246301 / 2500000000000000000000)

theorem Zeta5Irrational.U_254_5 : Uω (aρ 5) (bρ 5) (3456533023273 / 16000000000000) ≤ -(4268311513824813753719 / 2500000000000000000000)

theorem Zeta5Irrational.U_254_6 : Uω (aρ 6) (bρ 6) (3456533023273 / 16000000000000) ≤ -(1818221057360102248173 / 1000000000000000000000)

theorem Zeta5Irrational.U_254_7 : Uω (aρ 7) (bρ 7) (3456533023273 / 16000000000000) ≤ -(10047517320976467956059 / 5000000000000000000000)

theorem Zeta5Irrational.U_254_8 : Uω (aρ 8) (bρ 8) (3456533023273 / 16000000000000) ≤ -(3065785211127408859203 / 1250000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_254 : Uρ (3456533023273 / 16000000000000) ≤ -(9484848458057468868523 / 5000000000000000000000)

theorem Zeta5Irrational.U_255_1 : Uω (aρ 1) (bρ 1) (13860252210179 / 64000000000000) ≤ -(3900321794800609828613 / 2500000000000000000000)

theorem Zeta5Irrational.U_255_2 : Uω (aρ 2) (bρ 2) (13860252210179 / 64000000000000) ≤ -(15717147848202477416551 / 10000000000000000000000)

theorem Zeta5Irrational.U_255_3 : Uω (aρ 3) (bρ 3) (13860252210179 / 64000000000000) ≤ -(15954471174061227251973 / 10000000000000000000000)

theorem Zeta5Irrational.U_255_4 : Uω (aρ 4) (bρ 4) (13860252210179 / 64000000000000) ≤ -(255727136714500718647 / 156250000000000000000)

theorem Zeta5Irrational.U_255_5 : Uω (aρ 5) (bρ 5) (13860252210179 / 64000000000000) ≤ -(17043653012069059339703 / 10000000000000000000000)

theorem Zeta5Irrational.U_255_6 : Uω (aρ 6) (bρ 6) (13860252210179 / 64000000000000) ≤ -(18148641089420613638953 / 10000000000000000000000)

theorem Zeta5Irrational.U_255_7 : Uω (aρ 7) (bρ 7) (13860252210179 / 64000000000000) ≤ -(5013069580125437245247 / 2500000000000000000000)

theorem Zeta5Irrational.U_255_8 : Uω (aρ 8) (bρ 8) (13860252210179 / 64000000000000) ≤ -(6108309044709731099283 / 2500000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_255 : Uρ (13860252210179 / 64000000000000) ≤ -(18949396255775099006671 / 10000000000000000000000)