Certified arcsine potential bounds (U26)

theorem Zeta5Irrational.U_316_1 : Uω (aρ 1) (bρ 1) (7470559844389 / 25600000000000) ≤ -(313497993542335413487 / 250000000000000000000)

theorem Zeta5Irrational.U_316_2 : Uω (aρ 2) (bρ 2) (7470559844389 / 25600000000000) ≤ -(12624687248934936222979 / 10000000000000000000000)

theorem Zeta5Irrational.U_316_3 : Uω (aρ 3) (bρ 3) (7470559844389 / 25600000000000) ≤ -(12797043708037897056853 / 10000000000000000000000)

theorem Zeta5Irrational.U_316_4 : Uω (aρ 4) (bρ 4) (7470559844389 / 25600000000000) ≤ -(13092092856450291711527 / 10000000000000000000000)

theorem Zeta5Irrational.U_316_5 : Uω (aρ 5) (bρ 5) (7470559844389 / 25600000000000) ≤ -(13564627096277214139309 / 10000000000000000000000)

theorem Zeta5Irrational.U_316_6 : Uω (aρ 6) (bρ 6) (7470559844389 / 25600000000000) ≤ -(14299702482758872198407 / 10000000000000000000000)

theorem Zeta5Irrational.U_316_7 : Uω (aρ 7) (bρ 7) (7470559844389 / 25600000000000) ≤ -(7722035347185278864809 / 5000000000000000000000)

theorem Zeta5Irrational.U_316_8 : Uω (aρ 8) (bρ 8) (7470559844389 / 25600000000000) ≤ -(17321650244358947368713 / 10000000000000000000000)

theorem Zeta5Irrational.U_316_9 : Uω (aρ 9) (bρ 9) (7470559844389 / 25600000000000) ≤ -(2128541148575158751237 / 1000000000000000000000)

theorem Zeta5Irrational.U_316_10 : Uω (aρ 10) (bρ 10) (7470559844389 / 25600000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_316_11 : Uω (aρ 11) (bρ 11) (7470559844389 / 25600000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_316_12 : Uω (aρ 12) (bρ 12) (7470559844389 / 25600000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_316_13 : Uω (aρ 13) (bρ 13) (7470559844389 / 25600000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_316_14 : Uω (aρ 14) (bρ 14) (7470559844389 / 25600000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_316_15 : Uω (aρ 15) (bρ 15) (7470559844389 / 25600000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_316_16 : Uω (aρ 16) (bρ 16) (7470559844389 / 25600000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_316 : Uρ (7470559844389 / 25600000000000) ≤ -(16433043457405759501447 / 10000000000000000000000)

theorem Zeta5Irrational.U_317_1 : Uω (aρ 1) (bρ 1) (18715271389599 / 64000000000000) ≤ -(1564832224170227175487 / 1250000000000000000000)

theorem Zeta5Irrational.U_317_2 : Uω (aρ 2) (bρ 2) (18715271389599 / 64000000000000) ≤ -(12603242087980496131311 / 10000000000000000000000)

theorem Zeta5Irrational.U_317_3 : Uω (aρ 3) (bρ 3) (18715271389599 / 64000000000000) ≤ -(51100874429049288073 / 40000000000000000000)

theorem Zeta5Irrational.U_317_4 : Uω (aρ 4) (bρ 4) (18715271389599 / 64000000000000) ≤ -(653479665454582040087 / 500000000000000000000)

theorem Zeta5Irrational.U_317_5 : Uω (aρ 5) (bρ 5) (18715271389599 / 64000000000000) ≤ -(13540979465010177493251 / 10000000000000000000000)

theorem Zeta5Irrational.U_317_6 : Uω (aρ 6) (bρ 6) (18715271389599 / 64000000000000) ≤ -(14274081709003551513581 / 10000000000000000000000)

theorem Zeta5Irrational.U_317_7 : Uω (aρ 7) (bρ 7) (18715271389599 / 64000000000000) ≤ -(3853706432000757266593 / 2500000000000000000000)

theorem Zeta5Irrational.U_317_8 : Uω (aρ 8) (bρ 8) (18715271389599 / 64000000000000) ≤ -(1728438790549203311371 / 1000000000000000000000)

theorem Zeta5Irrational.U_317_9 : Uω (aρ 9) (bρ 9) (18715271389599 / 64000000000000) ≤ -(21210927637829035889281 / 10000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_317 : Uρ (18715271389599 / 64000000000000) ≤ -(1641393523257367651801 / 1000000000000000000000)

theorem Zeta5Irrational.U_318_1 : Uω (aρ 1) (bρ 1) (37508286336451 / 128000000000000) ≤ -(2499488191591324361 / 2000000000000000000)

theorem Zeta5Irrational.U_318_2 : Uω (aρ 2) (bρ 2) (37508286336451 / 128000000000000) ≤ -(3145460707552018440057 / 2500000000000000000000)

theorem Zeta5Irrational.U_318_3 : Uω (aρ 3) (bρ 3) (37508286336451 / 128000000000000) ≤ -(797090067591125847769 / 625000000000000000000)

theorem Zeta5Irrational.U_318_4 : Uω (aρ 4) (bρ 4) (37508286336451 / 128000000000000) ≤ -(652357220802502956437 / 500000000000000000000)

theorem Zeta5Irrational.U_318_5 : Uω (aρ 5) (bρ 5) (37508286336451 / 128000000000000) ≤ -(13517388069351791248559 / 10000000000000000000000)

theorem Zeta5Irrational.U_318_6 : Uω (aρ 6) (bρ 6) (37508286336451 / 128000000000000) ≤ -(14248527817117285144357 / 10000000000000000000000)

theorem Zeta5Irrational.U_318_7 : Uω (aρ 7) (bρ 7) (37508286336451 / 128000000000000) ≤ -(7692835495468796043633 / 5000000000000000000000)

theorem Zeta5Irrational.U_318_8 : Uω (aρ 8) (bρ 8) (37508286336451 / 128000000000000) ≤ -(431182196363598939487 / 250000000000000000000)

theorem Zeta5Irrational.U_318_9 : Uω (aρ 9) (bρ 9) (37508286336451 / 128000000000000) ≤ -(21137493907044255191037 / 10000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_318 : Uρ (37508286336451 / 128000000000000) ≤ -(16394957714446851550457 / 10000000000000000000000)

theorem Zeta5Irrational.U_319_1 : Uω (aρ 1) (bρ 1) (4698253736713 / 16000000000000) ≤ -(2495253808887446669611 / 2000000000000000000000)

theorem Zeta5Irrational.U_319_2 : Uω (aρ 2) (bρ 2) (4698253736713 / 16000000000000) ≤ -(2512097855895038717213 / 2000000000000000000000)

theorem Zeta5Irrational.U_319_3 : Uω (aρ 3) (bρ 3) (4698253736713 / 16000000000000) ≤ -(12731710923469879778623 / 10000000000000000000000)

theorem Zeta5Irrational.U_319_4 : Uω (aρ 4) (bρ 4) (4698253736713 / 16000000000000) ≤ -(3256186487277326469717 / 2500000000000000000000)

theorem Zeta5Irrational.U_319_5 : Uω (aρ 5) (bρ 5) (4698253736713 / 16000000000000) ≤ -(421682895011645082857 / 312500000000000000000)

theorem Zeta5Irrational.U_319_6 : Uω (aρ 6) (bρ 6) (4698253736713 / 16000000000000) ≤ -(2844608090322516779093 / 2000000000000000000000)

theorem Zeta5Irrational.U_319_7 : Uω (aρ 7) (bρ 7) (4698253736713 / 16000000000000) ≤ -(15356605898681968251623 / 10000000000000000000000)

theorem Zeta5Irrational.U_319_8 : Uω (aρ 8) (bρ 8) (4698253736713 / 16000000000000) ≤ -(17210348493441849799951 / 10000000000000000000000)

theorem Zeta5Irrational.U_319_9 : Uω (aρ 9) (bρ 9) (4698253736713 / 16000000000000) ≤ -(5266267722922526326391 / 2500000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_319 : Uρ (4698253736713 / 16000000000000) ≤ -(2047013394536089855583 / 1250000000000000000000)

theorem Zeta5Irrational.U_320_1 : Uω (aρ 1) (bρ 1) (37663773450957 / 128000000000000) ≤ -(3113785465743511281037 / 2500000000000000000000)

theorem Zeta5Irrational.U_320_2 : Uω (aρ 2) (bρ 2) (37663773450957 / 128000000000000) ≤ -(12539181240894190232013 / 10000000000000000000000)

theorem Zeta5Irrational.U_320_3 : Uω (aρ 3) (bρ 3) (37663773450957 / 128000000000000) ≤ -(198594186367096513121 / 156250000000000000000)

theorem Zeta5Irrational.U_320_4 : Uω (aρ 4) (bρ 4) (37663773450957 / 128000000000000) ≤ -(13002397681596293197851 / 10000000000000000000000)

theorem Zeta5Irrational.U_320_5 : Uω (aρ 5) (bρ 5) (37663773450957 / 128000000000000) ≤ -(2694074582216508070629 / 2000000000000000000000)

theorem Zeta5Irrational.U_320_6 : Uω (aρ 6) (bρ 6) (37663773450957 / 128000000000000) ≤ -(7098809629941692031279 / 5000000000000000000000)

theorem Zeta5Irrational.U_320_7 : Uω (aρ 7) (bρ 7) (37663773450957 / 128000000000000) ≤ -(1532762987265952141441 / 1000000000000000000000)

theorem Zeta5Irrational.U_320_8 : Uω (aρ 8) (bρ 8) (37663773450957 / 128000000000000) ≤ -(8586784124854736362831 / 5000000000000000000000)

theorem Zeta5Irrational.U_320_9 : Uω (aρ 9) (bρ 9) (37663773450957 / 128000000000000) ≤ -(1312101351333463023481 / 625000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_320 : Uρ (37663773450957 / 128000000000000) ≤ -(16357380029375922820787 / 10000000000000000000000)

theorem Zeta5Irrational.U_321_1 : Uω (aρ 1) (bρ 1) (3774151700821 / 12800000000000) ≤ -(12434059224938226750533 / 10000000000000000000000)

theorem Zeta5Irrational.U_321_2 : Uω (aρ 2) (bρ 2) (3774151700821 / 12800000000000) ≤ -(12517918520821526742451 / 10000000000000000000000)

theorem Zeta5Irrational.U_321_3 : Uω (aρ 3) (bρ 3) (3774151700821 / 12800000000000) ≤ -(1268839188906676708531 / 1000000000000000000000)

theorem Zeta5Irrational.U_321_4 : Uω (aρ 4) (bρ 4) (3774151700821 / 12800000000000) ≤ -(3245024847091790789197 / 2500000000000000000000)

theorem Zeta5Irrational.U_321_5 : Uω (aρ 5) (bρ 5) (3774151700821 / 12800000000000) ≤ -(3361737154102947906173 / 2500000000000000000000)

theorem Zeta5Irrational.U_321_6 : Uω (aρ 6) (bρ 6) (3774151700821 / 12800000000000) ≤ -(2834452778434685974403 / 2000000000000000000000)

theorem Zeta5Irrational.U_321_7 : Uω (aρ 7) (bρ 7) (3774151700821 / 12800000000000) ≤ -(3059748468025370392999 / 2000000000000000000000)

theorem Zeta5Irrational.U_321_8 : Uω (aρ 8) (bρ 8) (3774151700821 / 12800000000000) ≤ -(4284236393973365117899 / 2500000000000000000000)

theorem Zeta5Irrational.U_321_9 : Uω (aρ 9) (bρ 9) (3774151700821 / 12800000000000) ≤ -(326923614860068943593 / 156250000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_321 : Uρ (3774151700821 / 12800000000000) ≤ -(1021173312797747915237 / 625000000000000000000)

theorem Zeta5Irrational.U_322_1 : Uω (aρ 1) (bρ 1) (37819260565463 / 128000000000000) ≤ -(496520837715664407951 / 400000000000000000000)

theorem Zeta5Irrational.U_322_2 : Uω (aρ 2) (bρ 2) (37819260565463 / 128000000000000) ≤ -(124967009268472262333 / 100000000000000000000)

theorem Zeta5Irrational.U_322_3 : Uω (aρ 3) (bρ 3) (37819260565463 / 128000000000000) ≤ -(253336052101030294349 / 200000000000000000000)

theorem Zeta5Irrational.U_322_4 : Uω (aρ 4) (bρ 4) (37819260565463 / 128000000000000) ≤ -(6478925422896764806271 / 5000000000000000000000)

theorem Zeta5Irrational.U_322_5 : Uω (aρ 5) (bρ 5) (37819260565463 / 128000000000000) ≤ -(13423579493192682497527 / 10000000000000000000000)

theorem Zeta5Irrational.U_322_6 : Uω (aρ 6) (bρ 6) (37819260565463 / 128000000000000) ≤ -(2829394800309022849977 / 2000000000000000000000)

theorem Zeta5Irrational.U_322_7 : Uω (aρ 7) (bρ 7) (37819260565463 / 128000000000000) ≤ -(15269942734092825618979 / 10000000000000000000000)

theorem Zeta5Irrational.U_322_8 : Uω (aρ 8) (bρ 8) (37819260565463 / 128000000000000) ≤ -(1710047894900604801367 / 1000000000000000000000)

theorem Zeta5Irrational.U_322_9 : Uω (aρ 9) (bρ 9) (37819260565463 / 128000000000000) ≤ -(20853507377490201335747 / 10000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_322 : Uρ (37819260565463 / 128000000000000) ≤ -(16320282936987819977121 / 10000000000000000000000)

theorem Zeta5Irrational.U_323_1 : Uω (aρ 1) (bρ 1) (9474251030679 / 32000000000000) ≤ -(3098006707644175633397 / 2500000000000000000000)

theorem Zeta5Irrational.U_323_2 : Uω (aρ 2) (bρ 2) (9474251030679 / 32000000000000) ≤ -(12475528267784406772859 / 10000000000000000000000)

theorem Zeta5Irrational.U_323_3 : Uω (aρ 3) (bρ 3) (9474251030679 / 32000000000000) ≤ -(2529051974725758156739 / 2000000000000000000000)

theorem Zeta5Irrational.U_323_4 : Uω (aρ 4) (bρ 4) (9474251030679 / 32000000000000) ≤ -(6467825915874434987103 / 5000000000000000000000)

theorem Zeta5Irrational.U_323_5 : Uω (aρ 5) (bρ 5) (9474251030679 / 32000000000000) ≤ -(13400265280141196180749 / 10000000000000000000000)

theorem Zeta5Irrational.U_323_6 : Uω (aρ 6) (bρ 6) (9474251030679 / 32000000000000) ≤ -(1412174924384875215969 / 1000000000000000000000)

theorem Zeta5Irrational.U_323_7 : Uω (aρ 7) (bρ 7) (9474251030679 / 32000000000000) ≤ -(15241230493239060186719 / 10000000000000000000000)

theorem Zeta5Irrational.U_323_8 : Uω (aρ 8) (bρ 8) (9474251030679 / 32000000000000) ≤ -(8532083434991892629273 / 5000000000000000000000)

theorem Zeta5Irrational.U_323_9 : Uω (aρ 9) (bρ 9) (9474251030679 / 32000000000000) ≤ -(20784778876778594280753 / 10000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_323 : Uρ (9474251030679 / 32000000000000) ≤ -(815095342484062068619 / 500000000000000000000)

theorem Zeta5Irrational.U_324_1 : Uω (aρ 1) (bρ 1) (37974747679969 / 128000000000000) ≤ -(1546384587863347391307 / 1250000000000000000000)

theorem Zeta5Irrational.U_324_2 : Uω (aρ 2) (bρ 2) (37974747679969 / 128000000000000) ≤ -(12454400353658942523317 / 10000000000000000000000)

theorem Zeta5Irrational.U_324_3 : Uω (aρ 3) (bρ 3) (37974747679969 / 128000000000000) ≤ -(6311881747142055395947 / 5000000000000000000000)

theorem Zeta5Irrational.U_324_4 : Uω (aρ 4) (bρ 4) (37974747679969 / 128000000000000) ≤ -(6456751062797533349511 / 5000000000000000000000)

theorem Zeta5Irrational.U_324_5 : Uω (aρ 5) (bρ 5) (37974747679969 / 128000000000000) ≤ -(1337700571783894728703 / 1000000000000000000000)

theorem Zeta5Irrational.U_324_6 : Uω (aρ 6) (bρ 6) (37974747679969 / 128000000000000) ≤ -(704829463884613062753 / 500000000000000000000)

theorem Zeta5Irrational.U_324_7 : Uω (aρ 7) (bρ 7) (37974747679969 / 128000000000000) ≤ -(15212605061841808395923 / 10000000000000000000000)

theorem Zeta5Irrational.U_324_8 : Uω (aρ 8) (bρ 8) (37974747679969 / 128000000000000) ≤ -(17028007863161623062419 / 10000000000000000000000)

theorem Zeta5Irrational.U_324_9 : Uω (aρ 9) (bρ 9) (37974747679969 / 128000000000000) ≤ -(4143379349202316265587 / 2000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_324 : Uρ (37974747679969 / 128000000000000) ≤ -(8141820960763928849147 / 5000000000000000000000)

theorem Zeta5Irrational.U_325_1 : Uω (aρ 1) (bρ 1) (19026245618611 / 64000000000000) ≤ -(12350170375956099393281 / 10000000000000000000000)

theorem Zeta5Irrational.U_325_2 : Uω (aρ 2) (bρ 2) (19026245618611 / 64000000000000) ≤ -(248666339913984400827 / 200000000000000000000)

theorem Zeta5Irrational.U_325_3 : Uω (aρ 3) (bρ 3) (19026245618611 / 64000000000000) ≤ -(2520462653559380998639 / 2000000000000000000000)

theorem Zeta5Irrational.U_325_4 : Uω (aρ 4) (bρ 4) (19026245618611 / 64000000000000) ≤ -(12891401508169105599223 / 10000000000000000000000)

theorem Zeta5Irrational.U_325_5 : Uω (aρ 5) (bρ 5) (19026245618611 / 64000000000000) ≤ -(3338450137178833629859 / 2500000000000000000000)

theorem Zeta5Irrational.U_325_6 : Uω (aρ 6) (bρ 6) (19026245618611 / 64000000000000) ≤ -(1758936720551409517731 / 1250000000000000000000)

theorem Zeta5Irrational.U_325_7 : Uω (aρ 7) (bρ 7) (19026245618611 / 64000000000000) ≤ -(15184065889695235582767 / 10000000000000000000000)

theorem Zeta5Irrational.U_325_8 : Uω (aρ 8) (bρ 8) (19026245618611 / 64000000000000) ≤ -(8496000237880936070873 / 5000000000000000000000)

theorem Zeta5Irrational.U_325_9 : Uω (aρ 9) (bρ 9) (19026245618611 / 64000000000000) ≤ -(10324916742774442850357 / 5000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_325 : Uρ (19026245618611 / 64000000000000) ≤ -(16265485475807527019511 / 10000000000000000000000)

theorem Zeta5Irrational.U_326_1 : Uω (aρ 1) (bρ 1) (1525209391779 / 5120000000000) ≤ -(308232691673755184269 / 250000000000000000000)

theorem Zeta5Irrational.U_326_2 : Uω (aρ 2) (bρ 2) (1525209391779 / 5120000000000) ≤ -(775767375395375690883 / 625000000000000000000)

theorem Zeta5Irrational.U_326_3 : Uω (aρ 3) (bρ 3) (1525209391779 / 5120000000000) ≤ -(2516181799245877235259 / 2000000000000000000000)

theorem Zeta5Irrational.U_326_4 : Uω (aρ 4) (bρ 4) (1525209391779 / 5120000000000) ≤ -(12869349761769917993087 / 10000000000000000000000)

theorem Zeta5Irrational.U_326_5 : Uω (aρ 5) (bρ 5) (1525209391779 / 5120000000000) ≤ -(533225980681196273301 / 400000000000000000000)

theorem Zeta5Irrational.U_326_6 : Uω (aρ 6) (bρ 6) (1525209391779 / 5120000000000) ≤ -(3511615592009915733251 / 2500000000000000000000)

theorem Zeta5Irrational.U_326_7 : Uω (aρ 7) (bρ 7) (1525209391779 / 5120000000000) ≤ -(473612888501125712317 / 312500000000000000000)

theorem Zeta5Irrational.U_326_8 : Uω (aρ 8) (bρ 8) (1525209391779 / 5120000000000) ≤ -(16956143277397500307727 / 10000000000000000000000)

theorem Zeta5Irrational.U_326_9 : Uω (aρ 9) (bρ 9) (1525209391779 / 5120000000000) ≤ -(20583563068231126965171 / 10000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_326 : Uρ (1525209391779 / 5120000000000) ≤ -(162474349687928098737 / 100000000000000000000)

theorem Zeta5Irrational.U_327_1 : Uω (aρ 1) (bρ 1) (2387998646983 / 8000000000000) ≤ -(492339535770254087997 / 400000000000000000000)

theorem Zeta5Irrational.U_327_2 : Uω (aρ 2) (bρ 2) (2387998646983 / 8000000000000) ≤ -(12391283199142446414239 / 10000000000000000000000)

theorem Zeta5Irrational.U_327_3 : Uω (aρ 3) (bρ 3) (2387998646983 / 8000000000000) ≤ -(12559550482915562925899 / 10000000000000000000000)

theorem Zeta5Irrational.U_327_4 : Uω (aρ 4) (bρ 4) (2387998646983 / 8000000000000) ≤ -(2569469334029075128739 / 2000000000000000000000)

theorem Zeta5Irrational.U_327_5 : Uω (aρ 5) (bρ 5) (2387998646983 / 8000000000000) ≤ -(532302094754197904583 / 400000000000000000000)

theorem Zeta5Irrational.U_327_6 : Uω (aρ 6) (bρ 6) (2387998646983 / 8000000000000) ≤ -(3505373688820111534097 / 2500000000000000000000)

theorem Zeta5Irrational.U_327_7 : Uω (aρ 7) (bρ 7) (2387998646983 / 8000000000000) ≤ -(15127244149469302294097 / 10000000000000000000000)

theorem Zeta5Irrational.U_327_8 : Uω (aρ 8) (bρ 8) (2387998646983 / 8000000000000) ≤ -(52876358936216522127 / 31250000000000000000)

theorem Zeta5Irrational.U_327_9 : Uω (aρ 9) (bρ 9) (2387998646983 / 8000000000000) ≤ -(4103612166609828334827 / 2000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_327 : Uρ (2387998646983 / 8000000000000) ≤ -(8114743990152761941807 / 5000000000000000000000)