Certified arcsine potential bounds (U16)

theorem Zeta5Irrational.U_196_1 : Uω (aρ 1) (bρ 1) (242277170987 / 1600000000000) ≤ -(2414101464838475762107 / 1250000000000000000000)

theorem Zeta5Irrational.U_196_2 : Uω (aρ 2) (bρ 2) (242277170987 / 1600000000000) ≤ -(19482577160501416685469 / 10000000000000000000000)

theorem Zeta5Irrational.U_196_3 : Uω (aρ 3) (bρ 3) (242277170987 / 1600000000000) ≤ -(4958726199469246675321 / 2500000000000000000000)

theorem Zeta5Irrational.U_196_4 : Uω (aρ 4) (bρ 4) (242277170987 / 1600000000000) ≤ -(10231450584493624514443 / 5000000000000000000000)

theorem Zeta5Irrational.U_196_5 : Uω (aρ 5) (bρ 5) (242277170987 / 1600000000000) ≤ -(2154930242961830379761 / 1000000000000000000000)

theorem Zeta5Irrational.U_196_6 : Uω (aρ 6) (bρ 6) (242277170987 / 1600000000000) ≤ -(5883976514400672601683 / 2500000000000000000000)

theorem Zeta5Irrational.U_196_7 : Uω (aρ 7) (bρ 7) (242277170987 / 1600000000000) ≤ -(28835587643811316305909 / 10000000000000000000000)

theorem Zeta5Irrational.U_196_8 : Uω (aρ 8) (bρ 8) (242277170987 / 1600000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_196_9 : Uω (aρ 9) (bρ 9) (242277170987 / 1600000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_196_10 : Uω (aρ 10) (bρ 10) (242277170987 / 1600000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_196_11 : Uω (aρ 11) (bρ 11) (242277170987 / 1600000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_196_12 : Uω (aρ 12) (bρ 12) (242277170987 / 1600000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_196_13 : Uω (aρ 13) (bρ 13) (242277170987 / 1600000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_196_14 : Uω (aρ 14) (bρ 14) (242277170987 / 1600000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_196_15 : Uω (aρ 15) (bρ 15) (242277170987 / 1600000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_196_16 : Uω (aρ 16) (bρ 16) (242277170987 / 1600000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_196 : Uρ (242277170987 / 1600000000000) ≤ -(21470082810998145944539 / 10000000000000000000000)

theorem Zeta5Irrational.U_197_1 : Uω (aρ 1) (bρ 1) (9747866874751 / 64000000000000) ≤ -(9625896157689089085363 / 5000000000000000000000)

theorem Zeta5Irrational.U_197_2 : Uω (aρ 2) (bρ 2) (9747866874751 / 64000000000000) ≤ -(9710244426699519995267 / 5000000000000000000000)

theorem Zeta5Irrational.U_197_3 : Uω (aρ 3) (bρ 3) (9747866874751 / 64000000000000) ≤ -(9885252872164051723893 / 5000000000000000000000)

theorem Zeta5Irrational.U_197_4 : Uω (aρ 4) (bρ 4) (9747866874751 / 64000000000000) ≤ -(5098511423100886032829 / 2500000000000000000000)

theorem Zeta5Irrational.U_197_5 : Uω (aρ 5) (bρ 5) (9747866874751 / 64000000000000) ≤ -(5367882483107103412791 / 2500000000000000000000)

theorem Zeta5Irrational.U_197_6 : Uω (aρ 6) (bρ 6) (9747866874751 / 64000000000000) ≤ -(5859077040181952131849 / 2500000000000000000000)

theorem Zeta5Irrational.U_197_7 : Uω (aρ 7) (bρ 7) (9747866874751 / 64000000000000) ≤ -(7143266057875241232323 / 2500000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_197 : Uρ (9747866874751 / 64000000000000) ≤ -(2678167143913165181433 / 1250000000000000000000)

theorem Zeta5Irrational.U_198_1 : Uω (aρ 1) (bρ 1) (4902323455011 / 32000000000000) ≤ -(19191143047661083763181 / 10000000000000000000000)

theorem Zeta5Irrational.U_198_2 : Uω (aρ 2) (bρ 2) (4902323455011 / 32000000000000) ≤ -(9679392028817212299531 / 5000000000000000000000)

theorem Zeta5Irrational.U_198_3 : Uω (aρ 3) (bρ 3) (4902323455011 / 32000000000000) ≤ -(492663008624633561373 / 250000000000000000000)

theorem Zeta5Irrational.U_198_4 : Uω (aρ 4) (bρ 4) (4902323455011 / 32000000000000) ≤ -(20325666932152984631853 / 10000000000000000000000)

theorem Zeta5Irrational.U_198_5 : Uω (aρ 5) (bρ 5) (4902323455011 / 32000000000000) ≤ -(42788762652914107141 / 20000000000000000000)

theorem Zeta5Irrational.U_198_6 : Uω (aρ 6) (bρ 6) (4902323455011 / 32000000000000) ≤ -(23337831090964090934793 / 10000000000000000000000)

theorem Zeta5Irrational.U_198_7 : Uω (aρ 7) (bρ 7) (4902323455011 / 32000000000000) ≤ -(113301949068643981267 / 40000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_198 : Uρ (4902323455011 / 32000000000000) ≤ -(10691025983055117798807 / 5000000000000000000000)

theorem Zeta5Irrational.U_199_1 : Uω (aρ 1) (bρ 1) (9861426945293 / 64000000000000) ≤ -(19130859451563604787399 / 10000000000000000000000)

theorem Zeta5Irrational.U_199_2 : Uω (aρ 2) (bρ 2) (9861426945293 / 64000000000000) ≤ -(2412182257464382172739 / 1250000000000000000000)

theorem Zeta5Irrational.U_199_3 : Uω (aρ 3) (bρ 3) (9861426945293 / 64000000000000) ≤ -(19642943299792789663527 / 10000000000000000000000)

theorem Zeta5Irrational.U_199_4 : Uω (aρ 4) (bρ 4) (9861426945293 / 64000000000000) ≤ -(20257758253733241645161 / 10000000000000000000000)

theorem Zeta5Irrational.U_199_5 : Uω (aρ 5) (bρ 5) (9861426945293 / 64000000000000) ≤ -(5329461579391329115803 / 2500000000000000000000)

theorem Zeta5Irrational.U_199_6 : Uω (aρ 6) (bρ 6) (9861426945293 / 64000000000000) ≤ -(23240447077305945546461 / 10000000000000000000000)

theorem Zeta5Irrational.U_199_7 : Uω (aρ 7) (bρ 7) (9861426945293 / 64000000000000) ≤ -(28090691845157120020427 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_199 : Uρ (9861426945293 / 64000000000000) ≤ -(5335009962320976159597 / 2500000000000000000000)

theorem Zeta5Irrational.U_200_1 : Uω (aρ 1) (bρ 1) (2479551745141 / 16000000000000) ≤ -(9535468571688656894177 / 5000000000000000000000)

theorem Zeta5Irrational.U_200_2 : Uω (aρ 2) (bρ 2) (2479551745141 / 16000000000000) ≤ -(19236506232599800661231 / 10000000000000000000000)

theorem Zeta5Irrational.U_200_3 : Uω (aρ 3) (bρ 3) (2479551745141 / 16000000000000) ≤ -(19579769410281550678357 / 10000000000000000000000)

theorem Zeta5Irrational.U_200_4 : Uω (aρ 4) (bρ 4) (2479551745141 / 16000000000000) ≤ -(2019031316175803607789 / 1000000000000000000000)

theorem Zeta5Irrational.U_200_5 : Uω (aρ 5) (bρ 5) (2479551745141 / 16000000000000) ≤ -(21241914872470499005599 / 10000000000000000000000)

theorem Zeta5Irrational.U_200_6 : Uω (aρ 6) (bρ 6) (2479551745141 / 16000000000000) ≤ -(23144129448493782607159 / 10000000000000000000000)

theorem Zeta5Irrational.U_200_7 : Uω (aρ 7) (bρ 7) (2479551745141 / 16000000000000) ≤ -(13933497005570068083757 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_200 : Uρ (2479551745141 / 16000000000000) ≤ -(21299154326957743988867 / 10000000000000000000000)

theorem Zeta5Irrational.U_201_1 : Uω (aρ 1) (bρ 1) (19893193996399 / 128000000000000) ≤ -(3808222024764513750947 / 2000000000000000000000)

theorem Zeta5Irrational.U_201_2 : Uω (aρ 2) (bρ 2) (19893193996399 / 128000000000000) ≤ -(19206169210263464948851 / 10000000000000000000000)

theorem Zeta5Irrational.U_201_3 : Uω (aρ 3) (bρ 3) (19893193996399 / 128000000000000) ≤ -(9774166025761886195709 / 5000000000000000000000)

theorem Zeta5Irrational.U_201_4 : Uω (aρ 4) (bρ 4) (19893193996399 / 128000000000000) ≤ -(20156762467954930955953 / 10000000000000000000000)

theorem Zeta5Irrational.U_201_5 : Uω (aρ 5) (bρ 5) (19893193996399 / 128000000000000) ≤ -(10602086210028209019321 / 5000000000000000000000)

theorem Zeta5Irrational.U_201_6 : Uω (aρ 6) (bρ 6) (19893193996399 / 128000000000000) ≤ -(23096362479439773573517 / 10000000000000000000000)

theorem Zeta5Irrational.U_201_7 : Uω (aρ 7) (bρ 7) (19893193996399 / 128000000000000) ≤ -(27758876997846690296493 / 10000000000000000000000)

theorem Zeta5Irrational.U_201_8 : Uω (aρ 8) (bρ 8) (19893193996399 / 128000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_201_9 : Uω (aρ 9) (bρ 9) (19893193996399 / 128000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_201_10 : Uω (aρ 10) (bρ 10) (19893193996399 / 128000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_201 : Uρ (19893193996399 / 128000000000000) ≤ -(1063954824476878769469 / 500000000000000000000)

theorem Zeta5Irrational.U_202_1 : Uω (aρ 1) (bρ 1) (1994997403167 / 12800000000000) ≤ -(19011371817764254291277 / 10000000000000000000000)

theorem Zeta5Irrational.U_202_2 : Uω (aρ 2) (bρ 2) (1994997403167 / 12800000000000) ≤ -(19175924033595514993157 / 10000000000000000000000)

theorem Zeta5Irrational.U_202_3 : Uω (aρ 3) (bρ 3) (1994997403167 / 12800000000000) ≤ -(19516993576980804934593 / 10000000000000000000000)

theorem Zeta5Irrational.U_202_4 : Uω (aρ 4) (bρ 4) (1994997403167 / 12800000000000) ≤ -(10061662648026687643777 / 5000000000000000000000)

theorem Zeta5Irrational.U_202_5 : Uω (aρ 5) (bρ 5) (1994997403167 / 12800000000000) ≤ -(2645822151221018910863 / 1250000000000000000000)

theorem Zeta5Irrational.U_202_6 : Uω (aρ 6) (bρ 6) (1994997403167 / 12800000000000) ≤ -(5762213143197609709187 / 2500000000000000000000)

theorem Zeta5Irrational.U_202_7 : Uω (aρ 7) (bρ 7) (1994997403167 / 12800000000000) ≤ -(13826526486999273842053 / 5000000000000000000000)

theorem Zeta5Irrational.U_202_8 : Uω (aρ 8) (bρ 8) (1994997403167 / 12800000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_202 : Uρ (1994997403167 / 12800000000000) ≤ -(21259278159574063461509 / 10000000000000000000000)

theorem Zeta5Irrational.U_203_1 : Uω (aρ 1) (bρ 1) (20006754066941 / 128000000000000) ≤ -(18981721698975795827751 / 10000000000000000000000)

theorem Zeta5Irrational.U_203_2 : Uω (aρ 2) (bρ 2) (20006754066941 / 128000000000000) ≤ -(3829154029520808723151 / 2000000000000000000000)

theorem Zeta5Irrational.U_203_3 : Uω (aρ 3) (bρ 3) (20006754066941 / 128000000000000) ≤ -(19485753364276007235131 / 10000000000000000000000)

theorem Zeta5Irrational.U_203_4 : Uω (aρ 4) (bρ 4) (20006754066941 / 128000000000000) ≤ -(4018000174308122372943 / 2000000000000000000000)

theorem Zeta5Irrational.U_203_5 : Uω (aρ 5) (bρ 5) (20006754066941 / 128000000000000) ≤ -(4225825611375491178981 / 2000000000000000000000)

theorem Zeta5Irrational.U_203_6 : Uω (aρ 6) (bρ 6) (20006754066941 / 128000000000000) ≤ -(1437599792363333804987 / 625000000000000000000)

theorem Zeta5Irrational.U_203_7 : Uω (aρ 7) (bρ 7) (20006754066941 / 128000000000000) ≤ -(27549393096344733901133 / 10000000000000000000000)

theorem Zeta5Irrational.U_203_8 : Uω (aρ 8) (bρ 8) (20006754066941 / 128000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_203_9 : Uω (aρ 9) (bρ 9) (20006754066941 / 128000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_203_10 : Uω (aρ 10) (bρ 10) (20006754066941 / 128000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_203 : Uρ (20006754066941 / 128000000000000) ≤ -(21239687987825780551489 / 10000000000000000000000)

theorem Zeta5Irrational.U_204_1 : Uω (aρ 1) (bρ 1) (5015883525553 / 32000000000000) ≤ -(18952159245899628942921 / 10000000000000000000000)

theorem Zeta5Irrational.U_204_2 : Uω (aρ 2) (bρ 2) (5015883525553 / 32000000000000) ≤ -(2389463375289662657993 / 1250000000000000000000)

theorem Zeta5Irrational.U_204_3 : Uω (aρ 3) (bρ 3) (5015883525553 / 32000000000000) ≤ -(19454610796911121675621 / 10000000000000000000000)

theorem Zeta5Irrational.U_204_4 : Uω (aρ 4) (bρ 4) (5015883525553 / 32000000000000) ≤ -(20056788427891101095629 / 10000000000000000000000)

theorem Zeta5Irrational.U_204_5 : Uω (aρ 5) (bρ 5) (5015883525553 / 32000000000000) ≤ -(4218364758269121785757 / 2000000000000000000000)

theorem Zeta5Irrational.U_204_6 : Uω (aρ 6) (bρ 6) (5015883525553 / 32000000000000) ≤ -(22954591801955800902821 / 10000000000000000000000)

theorem Zeta5Irrational.U_204_7 : Uω (aρ 7) (bρ 7) (5015883525553 / 32000000000000) ≤ -(68619450712148196321 / 25000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_204 : Uρ (5015883525553 / 32000000000000) ≤ -(848812625190008480521 / 400000000000000000000)

theorem Zeta5Irrational.U_205_1 : Uω (aρ 1) (bρ 1) (20120314137483 / 128000000000000) ≤ -(4730670985398022320463 / 2500000000000000000000)

theorem Zeta5Irrational.U_205_2 : Uω (aρ 2) (bρ 2) (20120314137483 / 128000000000000) ≤ -(9542867026361629120287 / 5000000000000000000000)

theorem Zeta5Irrational.U_205_3 : Uω (aρ 3) (bρ 3) (20120314137483 / 128000000000000) ≤ -(3884713052838447392357 / 2000000000000000000000)

theorem Zeta5Irrational.U_205_4 : Uω (aρ 4) (bρ 4) (20120314137483 / 128000000000000) ≤ -(2502960900806985594063 / 1250000000000000000000)

theorem Zeta5Irrational.U_205_5 : Uω (aρ 5) (bρ 5) (20120314137483 / 128000000000000) ≤ -(421093265151500674027 / 200000000000000000000)

theorem Zeta5Irrational.U_205_6 : Uω (aρ 6) (bρ 6) (20120314137483 / 128000000000000) ≤ -(22907835009299187804699 / 10000000000000000000000)

theorem Zeta5Irrational.U_205_7 : Uω (aρ 7) (bρ 7) (20120314137483 / 128000000000000) ≤ -(27348107758450982129949 / 10000000000000000000000)

theorem Zeta5Irrational.U_205_8 : Uω (aρ 8) (bρ 8) (20120314137483 / 128000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_205_9 : Uω (aρ 9) (bρ 9) (20120314137483 / 128000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_205_10 : Uω (aρ 10) (bρ 10) (20120314137483 / 128000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_205 : Uρ (20120314137483 / 128000000000000) ≤ -(165633997039833799489 / 78125000000000000000)

theorem Zeta5Irrational.U_206_1 : Uω (aρ 1) (bρ 1) (10088547086377 / 64000000000000) ≤ -(151146362189353403557 / 80000000000000000000)

theorem Zeta5Irrational.U_206_2 : Uω (aρ 2) (bρ 2) (10088547086377 / 64000000000000) ≤ -(1905585075871011538629 / 1000000000000000000000)

theorem Zeta5Irrational.U_206_3 : Uω (aρ 3) (bρ 3) (10088547086377 / 64000000000000) ≤ -(775704646446275497539 / 400000000000000000000)

theorem Zeta5Irrational.U_206_4 : Uω (aρ 4) (bρ 4) (10088547086377 / 64000000000000) ≤ -(19990696456353944320339 / 10000000000000000000000)

theorem Zeta5Irrational.U_206_5 : Uω (aρ 5) (bρ 5) (10088547086377 / 64000000000000) ≤ -(21017645314166303358547 / 10000000000000000000000)

theorem Zeta5Irrational.U_206_6 : Uω (aρ 6) (bρ 6) (10088547086377 / 64000000000000) ≤ -(11430661709532966677083 / 5000000000000000000000)

theorem Zeta5Irrational.U_206_7 : Uω (aρ 7) (bρ 7) (10088547086377 / 64000000000000) ≤ -(13625138903623822801247 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_206 : Uρ (10088547086377 / 64000000000000) ≤ -(21182187273591068333859 / 10000000000000000000000)

theorem Zeta5Irrational.U_207_1 : Uω (aρ 1) (bρ 1) (809354968321 / 5120000000000) ≤ -(9431996367126526943871 / 5000000000000000000000)

theorem Zeta5Irrational.U_207_2 : Uω (aρ 2) (bρ 2) (809354968321 / 5120000000000) ≤ -(4756514146251913096419 / 2500000000000000000000)

theorem Zeta5Irrational.U_207_3 : Uω (aρ 3) (bρ 3) (809354968321 / 5120000000000) ≤ -(19361762888502309310361 / 10000000000000000000000)

theorem Zeta5Irrational.U_207_4 : Uω (aρ 4) (bρ 4) (809354968321 / 5120000000000) ≤ -(4989453858591348907371 / 2500000000000000000000)

theorem Zeta5Irrational.U_207_5 : Uω (aρ 5) (bρ 5) (809354968321 / 5120000000000) ≤ -(262259610421003907303 / 125000000000000000000)

theorem Zeta5Irrational.U_207_6 : Uω (aρ 6) (bρ 6) (809354968321 / 5120000000000) ≤ -(22815054204177024956727 / 10000000000000000000000)

theorem Zeta5Irrational.U_207_7 : Uω (aρ 7) (bρ 7) (809354968321 / 5120000000000) ≤ -(1086168029808033831629 / 400000000000000000000)

theorem Zeta5Irrational.U_207_8 : Uω (aρ 8) (bρ 8) (809354968321 / 5120000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_207_9 : Uω (aρ 9) (bρ 9) (809354968321 / 5120000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_207_10 : Uω (aρ 10) (bρ 10) (809354968321 / 5120000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_207_11 : Uω (aρ 11) (bρ 11) (809354968321 / 5120000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_207_12 : Uω (aρ 12) (bρ 12) (809354968321 / 5120000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_207_13 : Uω (aρ 13) (bρ 13) (809354968321 / 5120000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_207_14 : Uω (aρ 14) (bρ 14) (809354968321 / 5120000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_207_15 : Uω (aρ 15) (bρ 15) (809354968321 / 5120000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_207_16 : Uω (aρ 16) (bρ 16) (809354968321 / 5120000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_207 : Uρ (809354968321 / 5120000000000) ≤ -(169307316687165452409 / 80000000000000000000)