Certified arcsine potential bounds (U50)

theorem Zeta5Irrational.U_604_1 : Uω (aρ 1) (bρ 1) (5573527036009 / 8000000000000) ≤ -(185358815803223170541 / 500000000000000000000)

theorem Zeta5Irrational.U_604_2 : Uω (aρ 2) (bρ 2) (5573527036009 / 8000000000000) ≤ -(3741861849853575925477 / 10000000000000000000000)

theorem Zeta5Irrational.U_604_3 : Uω (aρ 3) (bρ 3) (5573527036009 / 8000000000000) ≤ -(762314428217885278549 / 2000000000000000000000)

theorem Zeta5Irrational.U_604_4 : Uω (aρ 4) (bρ 4) (5573527036009 / 8000000000000) ≤ -(392836090377941199433 / 1000000000000000000000)

theorem Zeta5Irrational.U_604_5 : Uω (aρ 5) (bρ 5) (5573527036009 / 8000000000000) ≤ -(2054338537821379043431 / 5000000000000000000000)

theorem Zeta5Irrational.U_604_6 : Uω (aρ 6) (bρ 6) (5573527036009 / 8000000000000) ≤ -(1093155636640941648659 / 2500000000000000000000)

theorem Zeta5Irrational.U_604_7 : Uω (aρ 7) (bρ 7) (5573527036009 / 8000000000000) ≤ -(948658707005702538837 / 2000000000000000000000)

theorem Zeta5Irrational.U_604_8 : Uω (aρ 8) (bρ 8) (5573527036009 / 8000000000000) ≤ -(5246381739293769484407 / 10000000000000000000000)

theorem Zeta5Irrational.U_604_9 : Uω (aρ 9) (bρ 9) (5573527036009 / 8000000000000) ≤ -(591028782044301194203 / 1000000000000000000000)

theorem Zeta5Irrational.U_604_10 : Uω (aρ 10) (bρ 10) (5573527036009 / 8000000000000) ≤ -(6767284209621708981663 / 10000000000000000000000)

theorem Zeta5Irrational.U_604_11 : Uω (aρ 11) (bρ 11) (5573527036009 / 8000000000000) ≤ -(1964276446295185408741 / 2500000000000000000000)

theorem Zeta5Irrational.U_604_12 : Uω (aρ 12) (bρ 12) (5573527036009 / 8000000000000) ≤ -(9237298431489610316859 / 10000000000000000000000)

theorem Zeta5Irrational.U_604_13 : Uω (aρ 13) (bρ 13) (5573527036009 / 8000000000000) ≤ -(440752782161147218229 / 400000000000000000000)

theorem Zeta5Irrational.U_604_14 : Uω (aρ 14) (bρ 14) (5573527036009 / 8000000000000) ≤ -(13569695675472187431089 / 10000000000000000000000)

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

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

theorem Zeta5Irrational.U_604 : Uρ (5573527036009 / 8000000000000) ≤ -(392603247597578016043 / 625000000000000000000)

theorem Zeta5Irrational.U_605_1 : Uω (aρ 1) (bρ 1) (4469205467533 / 6400000000000) ≤ -(3683697828136284471879 / 10000000000000000000000)

theorem Zeta5Irrational.U_605_2 : Uω (aρ 2) (bρ 2) (4469205467533 / 6400000000000) ≤ -(743660286677977302009 / 2000000000000000000000)

theorem Zeta5Irrational.U_605_3 : Uω (aρ 3) (bρ 3) (4469205467533 / 6400000000000) ≤ -(236740360101894332047 / 625000000000000000000)

theorem Zeta5Irrational.U_605_4 : Uω (aρ 4) (bρ 4) (4469205467533 / 6400000000000) ≤ -(488044063950332874121 / 1250000000000000000000)

theorem Zeta5Irrational.U_605_5 : Uω (aρ 5) (bρ 5) (4469205467533 / 6400000000000) ≤ -(1021055811405140322069 / 2500000000000000000000)

theorem Zeta5Irrational.U_605_6 : Uω (aρ 6) (bρ 6) (4469205467533 / 6400000000000) ≤ -(4347493813142281048483 / 10000000000000000000000)

theorem Zeta5Irrational.U_605_7 : Uω (aρ 7) (bρ 7) (4469205467533 / 6400000000000) ≤ -(235858409498393209151 / 500000000000000000000)

theorem Zeta5Irrational.U_605_8 : Uω (aρ 8) (bρ 8) (4469205467533 / 6400000000000) ≤ -(5218804088661256319739 / 10000000000000000000000)

theorem Zeta5Irrational.U_605_9 : Uω (aρ 9) (bρ 9) (4469205467533 / 6400000000000) ≤ -(1470148674486619797487 / 2500000000000000000000)

theorem Zeta5Irrational.U_605_10 : Uω (aρ 10) (bρ 10) (4469205467533 / 6400000000000) ≤ -(3367231395774420070013 / 5000000000000000000000)

theorem Zeta5Irrational.U_605_11 : Uω (aρ 11) (bρ 11) (4469205467533 / 6400000000000) ≤ -(977435570934079413611 / 1250000000000000000000)

theorem Zeta5Irrational.U_605_12 : Uω (aρ 12) (bρ 12) (4469205467533 / 6400000000000) ≤ -(4595875065596004995123 / 5000000000000000000000)

theorem Zeta5Irrational.U_605_13 : Uω (aρ 13) (bρ 13) (4469205467533 / 6400000000000) ≤ -(10958002953060884909373 / 10000000000000000000000)

theorem Zeta5Irrational.U_605_14 : Uω (aρ 14) (bρ 14) (4469205467533 / 6400000000000) ≤ -(6731579740574347026997 / 5000000000000000000000)

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

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

theorem Zeta5Irrational.U_605 : Uρ (4469205467533 / 6400000000000) ≤ -(781257351911533191943 / 1250000000000000000000)

theorem Zeta5Irrational.U_606_1 : Uω (aρ 1) (bρ 1) (11198973265647 / 16000000000000) ≤ -(36602743354238826769 / 100000000000000000000)

theorem Zeta5Irrational.U_606_2 : Uω (aρ 2) (bρ 2) (11198973265647 / 16000000000000) ≤ -(1847398199132677266083 / 5000000000000000000000)

theorem Zeta5Irrational.U_606_3 : Uω (aρ 3) (bρ 3) (11198973265647 / 16000000000000) ≤ -(47052194398732723493 / 125000000000000000000)

theorem Zeta5Irrational.U_606_4 : Uω (aρ 4) (bρ 4) (11198973265647 / 16000000000000) ≤ -(1940200824024491061991 / 5000000000000000000000)

theorem Zeta5Irrational.U_606_5 : Uω (aρ 5) (bρ 5) (11198973265647 / 16000000000000) ≤ -(4059829140506769287007 / 10000000000000000000000)

theorem Zeta5Irrational.U_606_6 : Uω (aρ 6) (bρ 6) (11198973265647 / 16000000000000) ≤ -(2161214125510321744941 / 5000000000000000000000)

theorem Zeta5Irrational.U_606_7 : Uω (aρ 7) (bρ 7) (11198973265647 / 16000000000000) ≤ -(4691111374317235430867 / 10000000000000000000000)

theorem Zeta5Irrational.U_606_8 : Uω (aρ 8) (bρ 8) (11198973265647 / 16000000000000) ≤ -(2595651686485454946769 / 5000000000000000000000)

theorem Zeta5Irrational.U_606_9 : Uω (aρ 9) (bρ 9) (11198973265647 / 16000000000000) ≤ -(5850992094238623056519 / 10000000000000000000000)

theorem Zeta5Irrational.U_606_10 : Uω (aρ 10) (bρ 10) (11198973265647 / 16000000000000) ≤ -(837719390211303050617 / 1250000000000000000000)

theorem Zeta5Irrational.U_606_11 : Uω (aρ 11) (bρ 11) (11198973265647 / 16000000000000) ≤ -(7782020821850845249701 / 10000000000000000000000)

theorem Zeta5Irrational.U_606_12 : Uω (aρ 12) (bρ 12) (11198973265647 / 16000000000000) ≤ -(2286614058101796570093 / 2500000000000000000000)

theorem Zeta5Irrational.U_606_13 : Uω (aρ 13) (bρ 13) (11198973265647 / 16000000000000) ≤ -(5448867091589979705297 / 5000000000000000000000)

theorem Zeta5Irrational.U_606_14 : Uω (aρ 14) (bρ 14) (11198973265647 / 16000000000000) ≤ -(13359251881499432432203 / 10000000000000000000000)

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

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

theorem Zeta5Irrational.U_606 : Uρ (11198973265647 / 16000000000000) ≤ -(1554673099640420038419 / 2500000000000000000000)

theorem Zeta5Irrational.U_607_1 : Uω (aρ 1) (bρ 1) (22449865724923 / 32000000000000) ≤ -(727381116177924738757 / 2000000000000000000000)

theorem Zeta5Irrational.U_607_2 : Uω (aρ 2) (bρ 2) (22449865724923 / 32000000000000) ≤ -(1835673242359555576149 / 5000000000000000000000)

theorem Zeta5Irrational.U_607_3 : Uω (aρ 3) (bρ 3) (22449865724923 / 32000000000000) ≤ -(748112249305770301769 / 2000000000000000000000)

theorem Zeta5Irrational.U_607_4 : Uω (aρ 4) (bρ 4) (22449865724923 / 32000000000000) ≤ -(3856508037953090883837 / 10000000000000000000000)

theorem Zeta5Irrational.U_607_5 : Uω (aρ 5) (bρ 5) (22449865724923 / 32000000000000) ≤ -(4035494468925474550957 / 10000000000000000000000)

theorem Zeta5Irrational.U_607_6 : Uω (aρ 6) (bρ 6) (22449865724923 / 32000000000000) ≤ -(4297425542463654092731 / 10000000000000000000000)

theorem Zeta5Irrational.U_607_7 : Uω (aρ 7) (bρ 7) (22449865724923 / 32000000000000) ≤ -(466512272714342381551 / 1000000000000000000000)

theorem Zeta5Irrational.U_607_8 : Uω (aρ 8) (bρ 8) (22449865724923 / 32000000000000) ≤ -(1032775831632319691089 / 2000000000000000000000)

theorem Zeta5Irrational.U_607_9 : Uω (aρ 9) (bρ 9) (22449865724923 / 32000000000000) ≤ -(29107397217795261913 / 50000000000000000000)

theorem Zeta5Irrational.U_607_10 : Uω (aρ 10) (bρ 10) (22449865724923 / 32000000000000) ≤ -(666916037184109468323 / 1000000000000000000000)

theorem Zeta5Irrational.U_607_11 : Uω (aρ 11) (bρ 11) (22449865724923 / 32000000000000) ≤ -(193617827665090779411 / 250000000000000000000)

theorem Zeta5Irrational.U_607_12 : Uω (aρ 12) (bρ 12) (22449865724923 / 32000000000000) ≤ -(9101413433336903069591 / 10000000000000000000000)

theorem Zeta5Irrational.U_607_13 : Uω (aρ 13) (bρ 13) (22449865724923 / 32000000000000) ≤ -(2709500208247898408319 / 2500000000000000000000)

theorem Zeta5Irrational.U_607_14 : Uω (aρ 14) (bρ 14) (22449865724923 / 32000000000000) ≤ -(1325779785845717507177 / 1000000000000000000000)

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

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

theorem Zeta5Irrational.U_607 : Uρ (22449865724923 / 32000000000000) ≤ -(6187543587831002428899 / 10000000000000000000000)

theorem Zeta5Irrational.U_608_1 : Uω (aρ 1) (bρ 1) (2812723114819 / 4000000000000) ≤ -(3613591309293704288903 / 10000000000000000000000)

theorem Zeta5Irrational.U_608_2 : Uω (aρ 2) (bρ 2) (2812723114819 / 4000000000000) ≤ -(1823975717406834395501 / 5000000000000000000000)

theorem Zeta5Irrational.U_608_3 : Uω (aρ 3) (bρ 3) (2812723114819 / 4000000000000) ≤ -(29039082672124137669 / 78125000000000000000)

theorem Zeta5Irrational.U_608_4 : Uω (aρ 4) (bρ 4) (2812723114819 / 4000000000000) ≤ -(479083926015013648739 / 1250000000000000000000)

theorem Zeta5Irrational.U_608_5 : Uω (aρ 5) (bρ 5) (2812723114819 / 4000000000000) ≤ -(2005609470815187270507 / 5000000000000000000000)

theorem Zeta5Irrational.U_608_6 : Uω (aρ 6) (bρ 6) (2812723114819 / 4000000000000) ≤ -(4272485372134123980927 / 10000000000000000000000)

theorem Zeta5Irrational.U_608_7 : Uω (aρ 7) (bρ 7) (2812723114819 / 4000000000000) ≤ -(4639201890375419235181 / 10000000000000000000000)

theorem Zeta5Irrational.U_608_8 : Uω (aρ 8) (bρ 8) (2812723114819 / 4000000000000) ≤ -(1027306202776836780947 / 2000000000000000000000)

theorem Zeta5Irrational.U_608_9 : Uω (aρ 9) (bρ 9) (2812723114819 / 4000000000000) ≤ -(579205618557146584257 / 1000000000000000000000)

theorem Zeta5Irrational.U_608_10 : Uω (aρ 10) (bρ 10) (2812723114819 / 4000000000000) ≤ -(3318338861609870053377 / 5000000000000000000000)

theorem Zeta5Irrational.U_608_11 : Uω (aρ 11) (bρ 11) (2812723114819 / 4000000000000) ≤ -(481722500072513733311 / 625000000000000000000)

theorem Zeta5Irrational.U_608_12 : Uω (aρ 12) (bρ 12) (2812723114819 / 4000000000000) ≤ -(4528309251245035771429 / 5000000000000000000000)

theorem Zeta5Irrational.U_608_13 : Uω (aρ 13) (bρ 13) (2812723114819 / 4000000000000) ≤ -(538939547868169931167 / 500000000000000000000)

theorem Zeta5Irrational.U_608_14 : Uω (aρ 14) (bρ 14) (2812723114819 / 4000000000000) ≤ -(13158641155386919367299 / 10000000000000000000000)

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

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

theorem Zeta5Irrational.U_608 : Uρ (2812723114819 / 4000000000000) ≤ -(6156604129477609587247 / 10000000000000000000000)

theorem Zeta5Irrational.U_609_1 : Uω (aρ 1) (bρ 1) (22553704112181 / 32000000000000) ≤ -(718066253435485445603 / 2000000000000000000000)

theorem Zeta5Irrational.U_609_2 : Uω (aρ 2) (bρ 2) (22553704112181 / 32000000000000) ≤ -(1812305496208947558473 / 5000000000000000000000)

theorem Zeta5Irrational.U_609_3 : Uω (aρ 3) (bρ 3) (22553704112181 / 32000000000000) ≤ -(1846749648388671706299 / 5000000000000000000000)

theorem Zeta5Irrational.U_609_4 : Uω (aρ 4) (bρ 4) (22553704112181 / 32000000000000) ≤ -(119027858978336842039 / 312500000000000000000)

theorem Zeta5Irrational.U_609_5 : Uω (aρ 5) (bρ 5) (22553704112181 / 32000000000000) ≤ -(797400454296810172779 / 2000000000000000000000)

theorem Zeta5Irrational.U_609_6 : Uω (aρ 6) (bρ 6) (22553704112181 / 32000000000000) ≤ -(212380371353436732361 / 500000000000000000000)

theorem Zeta5Irrational.U_609_7 : Uω (aρ 7) (bρ 7) (22553704112181 / 32000000000000) ≤ -(2306674254387015104923 / 5000000000000000000000)

theorem Zeta5Irrational.U_609_8 : Uω (aρ 8) (bρ 8) (22553704112181 / 32000000000000) ≤ -(5109258513458795500777 / 10000000000000000000000)

theorem Zeta5Irrational.U_609_9 : Uω (aρ 9) (bρ 9) (22553704112181 / 32000000000000) ≤ -(720340220661621150801 / 1250000000000000000000)

theorem Zeta5Irrational.U_609_10 : Uω (aρ 10) (bρ 10) (22553704112181 / 32000000000000) ≤ -(1651076591580467623333 / 2500000000000000000000)

theorem Zeta5Irrational.U_609_11 : Uω (aρ 11) (bρ 11) (22553704112181 / 32000000000000) ≤ -(3835280052829488580907 / 5000000000000000000000)

theorem Zeta5Irrational.U_609_12 : Uω (aρ 12) (bρ 12) (22553704112181 / 32000000000000) ≤ -(2253017069146923309059 / 2500000000000000000000)

theorem Zeta5Irrational.U_609_13 : Uω (aρ 13) (bρ 13) (22553704112181 / 32000000000000) ≤ -(2144018610618247468463 / 2000000000000000000000)

theorem Zeta5Irrational.U_609_14 : Uω (aρ 14) (bρ 14) (22553704112181 / 32000000000000) ≤ -(6530820785372481273627 / 5000000000000000000000)

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

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

theorem Zeta5Irrational.U_609 : Uρ (22553704112181 / 32000000000000) ≤ -(6125866517931195617109 / 10000000000000000000000)

theorem Zeta5Irrational.U_610_1 : Uω (aρ 1) (bρ 1) (2260562330581 / 3200000000000) ≤ -(3567125202846665950607 / 10000000000000000000000)

theorem Zeta5Irrational.U_610_2 : Uω (aρ 2) (bρ 2) (2260562330581 / 3200000000000) ≤ -(720264980638036197189 / 2000000000000000000000)

theorem Zeta5Irrational.U_610_3 : Uω (aρ 3) (bρ 3) (2260562330581 / 3200000000000) ≤ -(146802045239044294797 / 400000000000000000000)

theorem Zeta5Irrational.U_610_4 : Uω (aρ 4) (bρ 4) (2260562330581 / 3200000000000) ≤ -(1892584003101455628531 / 5000000000000000000000)

theorem Zeta5Irrational.U_610_5 : Uω (aρ 5) (bρ 5) (2260562330581 / 3200000000000) ≤ -(3962844173437486658913 / 10000000000000000000000)

theorem Zeta5Irrational.U_610_6 : Uω (aρ 6) (bρ 6) (2260562330581 / 3200000000000) ≤ -(2111395698327103507627 / 5000000000000000000000)

theorem Zeta5Irrational.U_610_7 : Uω (aρ 7) (bρ 7) (2260562330581 / 3200000000000) ≤ -(4587562229901919172883 / 10000000000000000000000)

theorem Zeta5Irrational.U_610_8 : Uω (aρ 8) (bρ 8) (2260562330581 / 3200000000000) ≤ -(2541030616916354549827 / 5000000000000000000000)

theorem Zeta5Irrational.U_610_9 : Uω (aρ 9) (bρ 9) (2260562330581 / 3200000000000) ≤ -(179171113532017318017 / 312500000000000000000)

theorem Zeta5Irrational.U_610_10 : Uω (aρ 10) (bρ 10) (2260562330581 / 3200000000000) ≤ -(821505687596867965743 / 1250000000000000000000)

theorem Zeta5Irrational.U_610_11 : Uω (aρ 11) (bρ 11) (2260562330581 / 3200000000000) ≤ -(7633712040526915893759 / 10000000000000000000000)

theorem Zeta5Irrational.U_610_12 : Uω (aρ 12) (bρ 12) (2260562330581 / 3200000000000) ≤ -(8967759658547838351263 / 10000000000000000000000)

theorem Zeta5Irrational.U_610_13 : Uω (aρ 13) (bρ 13) (2260562330581 / 3200000000000) ≤ -(10661896036179101416151 / 10000000000000000000000)

theorem Zeta5Irrational.U_610_14 : Uω (aρ 14) (bρ 14) (2260562330581 / 3200000000000) ≤ -(6483336367110149200723 / 5000000000000000000000)

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

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

theorem Zeta5Irrational.U_610 : Uρ (2260562330581 / 3200000000000) ≤ -(3047661947672350956073 / 5000000000000000000000)

theorem Zeta5Irrational.U_611_1 : Uω (aρ 1) (bρ 1) (22657542499439 / 32000000000000) ≤ -(1771986433177761046279 / 5000000000000000000000)

theorem Zeta5Irrational.U_611_2 : Uω (aρ 2) (bρ 2) (22657542499439 / 32000000000000) ≤ -(715618582912362501781 / 2000000000000000000000)

theorem Zeta5Irrational.U_611_3 : Uω (aρ 3) (bρ 3) (22657542499439 / 32000000000000) ≤ -(91166445666578071919 / 250000000000000000000)

theorem Zeta5Irrational.U_611_4 : Uω (aρ 4) (bρ 4) (22657542499439 / 32000000000000) ≤ -(3761500697413053400093 / 10000000000000000000000)

theorem Zeta5Irrational.U_611_5 : Uω (aρ 5) (bρ 5) (22657542499439 / 32000000000000) ≤ -(1969372182254922753893 / 5000000000000000000000)

theorem Zeta5Irrational.U_611_6 : Uω (aρ 6) (bρ 6) (22657542499439 / 32000000000000) ≤ -(4198036972603761804577 / 10000000000000000000000)

theorem Zeta5Irrational.U_611_7 : Uω (aρ 7) (bρ 7) (22657542499439 / 32000000000000) ≤ -(912368540818807209291 / 2000000000000000000000)

theorem Zeta5Irrational.U_611_8 : Uω (aρ 8) (bρ 8) (22657542499439 / 32000000000000) ≤ -(5054938755538850791503 / 10000000000000000000000)

theorem Zeta5Irrational.U_611_9 : Uω (aρ 9) (bρ 9) (22657542499439 / 32000000000000) ≤ -(713039655535341428553 / 1250000000000000000000)

theorem Zeta5Irrational.U_611_10 : Uω (aρ 10) (bρ 10) (22657542499439 / 32000000000000) ≤ -(6539894335196580513757 / 10000000000000000000000)

theorem Zeta5Irrational.U_611_11 : Uω (aρ 11) (bρ 11) (22657542499439 / 32000000000000) ≤ -(1899253611517541986453 / 2500000000000000000000)

theorem Zeta5Irrational.U_611_12 : Uω (aρ 12) (bρ 12) (22657542499439 / 32000000000000) ≤ -(8923689615546948989069 / 10000000000000000000000)

theorem Zeta5Irrational.U_611_13 : Uω (aρ 13) (bρ 13) (22657542499439 / 32000000000000) ≤ -(1325523652575441464269 / 1250000000000000000000)

theorem Zeta5Irrational.U_611_14 : Uω (aρ 14) (bρ 14) (22657542499439 / 32000000000000) ≤ -(3218405066046634124583 / 2500000000000000000000)

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

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

theorem Zeta5Irrational.U_611 : Uρ (22657542499439 / 32000000000000) ≤ -(1516242492074414445773 / 2500000000000000000000)

theorem Zeta5Irrational.U_612_1 : Uω (aρ 1) (bρ 1) (5677365423267 / 8000000000000) ≤ -(704174801898035062819 / 2000000000000000000000)

theorem Zeta5Irrational.U_612_2 : Uω (aρ 2) (bρ 2) (5677365423267 / 8000000000000) ≤ -(888728693930132351883 / 2500000000000000000000)

theorem Zeta5Irrational.U_612_3 : Uω (aρ 3) (bρ 3) (5677365423267 / 8000000000000) ≤ -(3623319127680336539177 / 10000000000000000000000)

theorem Zeta5Irrational.U_612_4 : Uω (aρ 4) (bρ 4) (5677365423267 / 8000000000000) ≤ -(116809040482449137779 / 312500000000000000000)

theorem Zeta5Irrational.U_612_5 : Uω (aρ 5) (bρ 5) (5677365423267 / 8000000000000) ≤ -(1957351281884243234707 / 5000000000000000000000)

theorem Zeta5Irrational.U_612_6 : Uω (aρ 6) (bρ 6) (5677365423267 / 8000000000000) ≤ -(4173343848933882049953 / 10000000000000000000000)

theorem Zeta5Irrational.U_612_7 : Uω (aρ 7) (bρ 7) (5677365423267 / 8000000000000) ≤ -(2268094792214219806731 / 5000000000000000000000)

theorem Zeta5Irrational.U_612_8 : Uω (aρ 8) (bρ 8) (5677365423267 / 8000000000000) ≤ -(2513945331327445238627 / 5000000000000000000000)

theorem Zeta5Irrational.U_612_9 : Uω (aρ 9) (bρ 9) (5677365423267 / 8000000000000) ≤ -(5675246059732281515241 / 10000000000000000000000)

theorem Zeta5Irrational.U_612_10 : Uω (aρ 10) (bρ 10) (5677365423267 / 8000000000000) ≤ -(650785208705559288509 / 1000000000000000000000)

theorem Zeta5Irrational.U_612_11 : Uω (aρ 11) (bρ 11) (5677365423267 / 8000000000000) ≤ -(7560465982075085006291 / 10000000000000000000000)

theorem Zeta5Irrational.U_612_12 : Uω (aρ 12) (bρ 12) (5677365423267 / 8000000000000) ≤ -(8879855177153937258143 / 10000000000000000000000)

theorem Zeta5Irrational.U_612_13 : Uω (aρ 13) (bρ 13) (5677365423267 / 8000000000000) ≤ -(2636740574611385909277 / 2500000000000000000000)

theorem Zeta5Irrational.U_612_14 : Uω (aρ 14) (bρ 14) (5677365423267 / 8000000000000) ≤ -(12782380229451382714503 / 10000000000000000000000)

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

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

theorem Zeta5Irrational.U_612 : Uρ (5677365423267 / 8000000000000) ≤ -(48278391504829887333 / 80000000000000000000)

theorem Zeta5Irrational.U_613_1 : Uω (aρ 1) (bρ 1) (22761380886697 / 32000000000000) ≤ -(874457096438228208609 / 2500000000000000000000)

theorem Zeta5Irrational.U_613_2 : Uω (aρ 2) (bρ 2) (22761380886697 / 32000000000000) ≤ -(3531790237594273493879 / 10000000000000000000000)

theorem Zeta5Irrational.U_613_3 : Uω (aρ 3) (bρ 3) (22761380886697 / 32000000000000) ≤ -(3600034779659862000939 / 10000000000000000000000)

theorem Zeta5Irrational.U_613_4 : Uω (aρ 4) (bρ 4) (22761380886697 / 32000000000000) ≤ -(371433353665875078499 / 1000000000000000000000)

theorem Zeta5Irrational.U_613_5 : Uω (aρ 5) (bρ 5) (22761380886697 / 32000000000000) ≤ -(486339811538652721501 / 1250000000000000000000)

theorem Zeta5Irrational.U_613_6 : Uω (aρ 6) (bρ 6) (22761380886697 / 32000000000000) ≤ -(1037177930485340854641 / 2500000000000000000000)

theorem Zeta5Irrational.U_613_7 : Uω (aρ 7) (bρ 7) (22761380886697 / 32000000000000) ≤ -(902120505339501589781 / 2000000000000000000000)

theorem Zeta5Irrational.U_613_8 : Uω (aρ 8) (bρ 8) (22761380886697 / 32000000000000) ≤ -(1250229135690731567857 / 2500000000000000000000)

theorem Zeta5Irrational.U_613_9 : Uω (aρ 9) (bρ 9) (22761380886697 / 32000000000000) ≤ -(141156538628002730241 / 250000000000000000000)

theorem Zeta5Irrational.U_613_10 : Uω (aρ 10) (bρ 10) (22761380886697 / 32000000000000) ≤ -(6475917982535767971497 / 10000000000000000000000)

theorem Zeta5Irrational.U_613_11 : Uω (aρ 11) (bρ 11) (22761380886697 / 32000000000000) ≤ -(7524065327419626836843 / 10000000000000000000000)

theorem Zeta5Irrational.U_613_12 : Uω (aρ 12) (bρ 12) (22761380886697 / 32000000000000) ≤ -(8836253433533761614819 / 10000000000000000000000)

theorem Zeta5Irrational.U_613_13 : Uω (aρ 13) (bρ 13) (22761380886697 / 32000000000000) ≤ -(2098041064256764806811 / 2000000000000000000000)

theorem Zeta5Irrational.U_613_14 : Uω (aρ 14) (bρ 14) (22761380886697 / 32000000000000) ≤ -(1586607232003425158267 / 1250000000000000000000)

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

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

theorem Zeta5Irrational.U_613 : Uρ (22761380886697 / 32000000000000) ≤ -(6004805442082874770883 / 10000000000000000000000)

theorem Zeta5Irrational.U_614_1 : Uω (aρ 1) (bρ 1) (11406650040163 / 16000000000000) ≤ -(347483575034634540937 / 1000000000000000000000)

theorem Zeta5Irrational.U_614_2 : Uω (aρ 2) (bρ 2) (11406650040163 / 16000000000000) ≤ -(350871905283512890253 / 1000000000000000000000)

theorem Zeta5Irrational.U_614_3 : Uω (aρ 3) (bρ 3) (11406650040163 / 16000000000000) ≤ -(894201132501833096559 / 2500000000000000000000)

theorem Zeta5Irrational.U_614_4 : Uω (aρ 4) (bρ 4) (11406650040163 / 16000000000000) ≤ -(3690833159315097836869 / 10000000000000000000000)

theorem Zeta5Irrational.U_614_5 : Uω (aρ 5) (bρ 5) (11406650040163 / 16000000000000) ≤ -(3866791873236816182813 / 10000000000000000000000)

theorem Zeta5Irrational.U_614_6 : Uω (aρ 6) (bρ 6) (11406650040163 / 16000000000000) ≤ -(412414029018064730309 / 1000000000000000000000)

theorem Zeta5Irrational.U_614_7 : Uω (aρ 7) (bρ 7) (11406650040163 / 16000000000000) ≤ -(897016237875904629603 / 2000000000000000000000)

theorem Zeta5Irrational.U_614_8 : Uω (aρ 8) (bρ 8) (11406650040163 / 16000000000000) ≤ -(4974015986909744955749 / 10000000000000000000000)

theorem Zeta5Irrational.U_614_9 : Uω (aρ 9) (bρ 9) (11406650040163 / 16000000000000) ≤ -(1404340792802545254119 / 2500000000000000000000)

theorem Zeta5Irrational.U_614_10 : Uω (aρ 10) (bρ 10) (11406650040163 / 16000000000000) ≤ -(6444091256402327224063 / 10000000000000000000000)

theorem Zeta5Irrational.U_614_11 : Uω (aρ 11) (bρ 11) (11406650040163 / 16000000000000) ≤ -(7487811179694703890357 / 10000000000000000000000)

theorem Zeta5Irrational.U_614_12 : Uω (aρ 12) (bρ 12) (11406650040163 / 16000000000000) ≤ -(8792881533717337725777 / 10000000000000000000000)

theorem Zeta5Irrational.U_614_13 : Uω (aρ 13) (bρ 13) (11406650040163 / 16000000000000) ≤ -(5216954341376271766899 / 5000000000000000000000)

theorem Zeta5Irrational.U_614_14 : Uω (aρ 14) (bρ 14) (11406650040163 / 16000000000000) ≤ -(6302483216415656992739 / 5000000000000000000000)

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

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

theorem Zeta5Irrational.U_614 : Uρ (11406650040163 / 16000000000000) ≤ -(5974984503744520764127 / 10000000000000000000000)

theorem Zeta5Irrational.U_615_1 : Uω (aρ 1) (bρ 1) (89520072139 / 125000000000) ≤ -(3429008473743938263037 / 10000000000000000000000)

theorem Zeta5Irrational.U_615_2 : Uω (aρ 2) (bρ 2) (89520072139 / 125000000000) ≤ -(432841970319017025881 / 1250000000000000000000)

theorem Zeta5Irrational.U_615_3 : Uω (aρ 3) (bρ 3) (89520072139 / 125000000000) ≤ -(882626331049433886807 / 2500000000000000000000)

theorem Zeta5Irrational.U_615_4 : Uω (aρ 4) (bρ 4) (89520072139 / 125000000000) ≤ -(728799502219952959019 / 2000000000000000000000)

theorem Zeta5Irrational.U_615_5 : Uω (aρ 5) (bρ 5) (89520072139 / 125000000000) ≤ -(954777473650250097291 / 2500000000000000000000)

theorem Zeta5Irrational.U_615_6 : Uω (aρ 6) (bρ 6) (89520072139 / 125000000000) ≤ -(1018794579431653135779 / 2500000000000000000000)

theorem Zeta5Irrational.U_615_7 : Uω (aρ 7) (bρ 7) (89520072139 / 125000000000) ≤ -(4434234323157178674073 / 10000000000000000000000)

theorem Zeta5Irrational.U_615_8 : Uω (aρ 8) (bρ 8) (89520072139 / 125000000000) ≤ -(307527121787241753561 / 625000000000000000000)

theorem Zeta5Irrational.U_615_9 : Uω (aρ 9) (bρ 9) (89520072139 / 125000000000) ≤ -(5559822753255195245599 / 10000000000000000000000)

theorem Zeta5Irrational.U_615_10 : Uω (aρ 10) (bρ 10) (89520072139 / 125000000000) ≤ -(6380756920479711852741 / 10000000000000000000000)

theorem Zeta5Irrational.U_615_11 : Uω (aρ 11) (bρ 11) (89520072139 / 125000000000) ≤ -(1853934321690048881789 / 2500000000000000000000)

theorem Zeta5Irrational.U_615_12 : Uω (aρ 12) (bρ 12) (89520072139 / 125000000000) ≤ -(272088004562792016049 / 312500000000000000000)

theorem Zeta5Irrational.U_615_13 : Uω (aρ 13) (bρ 13) (89520072139 / 125000000000) ≤ -(5161329804599260628999 / 5000000000000000000000)

theorem Zeta5Irrational.U_615_14 : Uω (aρ 14) (bρ 14) (89520072139 / 125000000000) ≤ -(6216882226043502495963 / 5000000000000000000000)

theorem Zeta5Irrational.U_615_15 : Uω (aρ 15) (bρ 15) (89520072139 / 125000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_615_16 : Uω (aρ 16) (bρ 16) (89520072139 / 125000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_615 : Uρ (89520072139 / 125000000000) ≤ -(5915842076011854104723 / 10000000000000000000000)