Certified arcsine potential bounds (U24)

theorem Zeta5Irrational.U_292_1 : Uω (aρ 1) (bρ 1) (2052407623963 / 8000000000000) ≤ -(3464788411850854761307 / 2500000000000000000000)

theorem Zeta5Irrational.U_292_2 : Uω (aρ 2) (bρ 2) (2052407623963 / 8000000000000) ≤ -(3489029123349057418429 / 2500000000000000000000)

theorem Zeta5Irrational.U_292_3 : Uω (aρ 3) (bρ 3) (2052407623963 / 8000000000000) ≤ -(14153838244717469109831 / 10000000000000000000000)

theorem Zeta5Irrational.U_292_4 : Uω (aρ 4) (bρ 4) (2052407623963 / 8000000000000) ≤ -(3623542733545598920361 / 2500000000000000000000)

theorem Zeta5Irrational.U_292_5 : Uω (aρ 5) (bρ 5) (2052407623963 / 8000000000000) ≤ -(3761145976967960412099 / 2500000000000000000000)

theorem Zeta5Irrational.U_292_6 : Uω (aρ 6) (bρ 6) (2052407623963 / 8000000000000) ≤ -(1989507064440686596057 / 1250000000000000000000)

theorem Zeta5Irrational.U_292_7 : Uω (aρ 7) (bρ 7) (2052407623963 / 8000000000000) ≤ -(8660390319253113093879 / 5000000000000000000000)

theorem Zeta5Irrational.U_292_8 : Uω (aρ 8) (bρ 8) (2052407623963 / 8000000000000) ≤ -(3967468627530778132021 / 2000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_292 : Uρ (2052407623963 / 8000000000000) ≤ -(17740742306804529030479 / 10000000000000000000000)

theorem Zeta5Irrational.U_293_1 : Uω (aρ 1) (bρ 1) (41730554821 / 160000000000) ≤ -(13690051247136983319469 / 10000000000000000000000)

theorem Zeta5Irrational.U_293_2 : Uω (aρ 2) (bρ 2) (41730554821 / 160000000000) ≤ -(13785355958980859419847 / 10000000000000000000000)

theorem Zeta5Irrational.U_293_3 : Uω (aρ 3) (bρ 3) (41730554821 / 160000000000) ≤ -(13979620201121910036697 / 10000000000000000000000)

theorem Zeta5Irrational.U_293_4 : Uω (aρ 4) (bρ 4) (41730554821 / 160000000000) ≤ -(2862750073378134468569 / 2000000000000000000000)

theorem Zeta5Irrational.U_293_5 : Uω (aρ 5) (bρ 5) (41730554821 / 160000000000) ≤ -(14853402445948760473001 / 10000000000000000000000)

theorem Zeta5Irrational.U_293_6 : Uω (aρ 6) (bρ 6) (41730554821 / 160000000000) ≤ -(15705721418374445952343 / 10000000000000000000000)

theorem Zeta5Irrational.U_293_7 : Uω (aρ 7) (bρ 7) (41730554821 / 160000000000) ≤ -(2134081990146632886253 / 1250000000000000000000)

theorem Zeta5Irrational.U_293_8 : Uω (aρ 8) (bρ 8) (41730554821 / 160000000000) ≤ -(19487658528202780408503 / 10000000000000000000000)

theorem Zeta5Irrational.U_293_9 : Uω (aρ 9) (bρ 9) (41730554821 / 160000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_293_10 : Uω (aρ 10) (bρ 10) (41730554821 / 160000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_293_11 : Uω (aρ 11) (bρ 11) (41730554821 / 160000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_293_12 : Uω (aρ 12) (bρ 12) (41730554821 / 160000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_293_13 : Uω (aρ 13) (bρ 13) (41730554821 / 160000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_293_14 : Uω (aρ 14) (bρ 14) (41730554821 / 160000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_293_15 : Uω (aρ 15) (bρ 15) (41730554821 / 160000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_293_16 : Uω (aρ 16) (bρ 16) (41730554821 / 160000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_293 : Uρ (41730554821 / 160000000000) ≤ -(881709807907133594019 / 500000000000000000000)

theorem Zeta5Irrational.U_294_1 : Uω (aρ 1) (bρ 1) (269345996903 / 1000000000000) ≤ -(13360191075021170630243 / 10000000000000000000000)

theorem Zeta5Irrational.U_294_2 : Uω (aρ 2) (bρ 2) (269345996903 / 1000000000000) ≤ -(26904688033233695969 / 20000000000000000000)

theorem Zeta5Irrational.U_294_3 : Uω (aρ 3) (bρ 3) (269345996903 / 1000000000000) ≤ -(3410010963726477067487 / 2500000000000000000000)

theorem Zeta5Irrational.U_294_4 : Uω (aρ 4) (bρ 4) (269345996903 / 1000000000000) ≤ -(13962424118052550522617 / 10000000000000000000000)

theorem Zeta5Irrational.U_294_5 : Uω (aρ 5) (bρ 5) (269345996903 / 1000000000000) ≤ -(14481773407649457578313 / 10000000000000000000000)

theorem Zeta5Irrational.U_294_6 : Uω (aρ 6) (bρ 6) (269345996903 / 1000000000000) ≤ -(1529822745192444888481 / 1000000000000000000000)

theorem Zeta5Irrational.U_294_7 : Uω (aρ 7) (bρ 7) (269345996903 / 1000000000000) ≤ -(16595518643128249441507 / 10000000000000000000000)

theorem Zeta5Irrational.U_294_8 : Uω (aρ 8) (bρ 8) (269345996903 / 1000000000000) ≤ -(18831930265090184175181 / 10000000000000000000000)

theorem Zeta5Irrational.U_294_9 : Uω (aρ 9) (bρ 9) (269345996903 / 1000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_294_10 : Uω (aρ 10) (bρ 10) (269345996903 / 1000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_294_11 : Uω (aρ 11) (bρ 11) (269345996903 / 1000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_294_12 : Uω (aρ 12) (bρ 12) (269345996903 / 1000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_294_13 : Uω (aρ 13) (bρ 13) (269345996903 / 1000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_294_14 : Uω (aρ 14) (bρ 14) (269345996903 / 1000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_294_15 : Uω (aρ 15) (bρ 15) (269345996903 / 1000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_294_16 : Uω (aρ 16) (bρ 16) (269345996903 / 1000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_294 : Uρ (269345996903 / 1000000000000) ≤ -(4357409086777446195519 / 2500000000000000000000)

theorem Zeta5Irrational.U_295_1 : Uω (aρ 1) (bρ 1) (8696815458149 / 32000000000000) ≤ -(265363977074615904323 / 200000000000000000000)

theorem Zeta5Irrational.U_295_2 : Uω (aρ 2) (bρ 2) (8696815458149 / 32000000000000) ≤ -(6679745953429830672479 / 5000000000000000000000)

theorem Zeta5Irrational.U_295_3 : Uω (aρ 3) (bρ 3) (8696815458149 / 32000000000000) ≤ -(13545402519784924013857 / 10000000000000000000000)

theorem Zeta5Irrational.U_295_4 : Uω (aρ 4) (bρ 4) (8696815458149 / 32000000000000) ≤ -(6932293049890189446321 / 5000000000000000000000)

theorem Zeta5Irrational.U_295_5 : Uω (aρ 5) (bρ 5) (8696815458149 / 32000000000000) ≤ -(1437843032608491819939 / 1000000000000000000000)

theorem Zeta5Irrational.U_295_6 : Uω (aρ 6) (bρ 6) (8696815458149 / 32000000000000) ≤ -(15185220254473415163101 / 10000000000000000000000)

theorem Zeta5Irrational.U_295_7 : Uω (aρ 7) (bρ 7) (8696815458149 / 32000000000000) ≤ -(3292797548244679441269 / 2000000000000000000000)

theorem Zeta5Irrational.U_295_8 : Uω (aρ 8) (bρ 8) (8696815458149 / 32000000000000) ≤ -(18654625142945181295753 / 10000000000000000000000)

theorem Zeta5Irrational.U_295_9 : Uω (aρ 9) (bρ 9) (8696815458149 / 32000000000000) ≤ -(12544728152889271956379 / 5000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_295 : Uρ (8696815458149 / 32000000000000) ≤ -(4301440739823679509847 / 2500000000000000000000)

theorem Zeta5Irrational.U_296_1 : Uω (aρ 1) (bρ 1) (4387279507701 / 16000000000000) ≤ -(6588522609675428053601 / 5000000000000000000000)

theorem Zeta5Irrational.U_296_2 : Uω (aρ 2) (bρ 2) (4387279507701 / 16000000000000) ≤ -(1326749428282152019991 / 1000000000000000000000)

theorem Zeta5Irrational.U_296_3 : Uω (aρ 3) (bρ 3) (4387279507701 / 16000000000000) ≤ -(6725824734455487825467 / 5000000000000000000000)

theorem Zeta5Irrational.U_296_4 : Uω (aρ 4) (bρ 4) (4387279507701 / 16000000000000) ≤ -(3441924802935448534447 / 2500000000000000000000)

theorem Zeta5Irrational.U_296_5 : Uω (aρ 5) (bρ 5) (4387279507701 / 16000000000000) ≤ -(1784519279932689038239 / 1250000000000000000000)

theorem Zeta5Irrational.U_296_6 : Uω (aρ 6) (bρ 6) (4387279507701 / 16000000000000) ≤ -(3768377053057300971997 / 2500000000000000000000)

theorem Zeta5Irrational.U_296_7 : Uω (aρ 7) (bρ 7) (4387279507701 / 16000000000000) ≤ -(16334286269266483063657 / 10000000000000000000000)

theorem Zeta5Irrational.U_296_8 : Uω (aρ 8) (bρ 8) (4387279507701 / 16000000000000) ≤ -(4620280082110656607647 / 2500000000000000000000)

theorem Zeta5Irrational.U_296_9 : Uω (aρ 9) (bρ 9) (4387279507701 / 16000000000000) ≤ -(24307602199671372227129 / 10000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_296 : Uρ (4387279507701 / 16000000000000) ≤ -(17081173195794320474823 / 10000000000000000000000)

theorem Zeta5Irrational.U_297_1 : Uω (aρ 1) (bρ 1) (1770460514531 / 6400000000000) ≤ -(13086715020354936082899 / 10000000000000000000000)

theorem Zeta5Irrational.U_297_2 : Uω (aρ 2) (bρ 2) (1770460514531 / 6400000000000) ≤ -(3294083889020482951309 / 2500000000000000000000)

theorem Zeta5Irrational.U_297_3 : Uω (aρ 3) (bρ 3) (1770460514531 / 6400000000000) ≤ -(13358768164879755402591 / 10000000000000000000000)

theorem Zeta5Irrational.U_297_4 : Uω (aρ 4) (bρ 4) (1770460514531 / 6400000000000) ≤ -(13671745074242828367393 / 10000000000000000000000)

theorem Zeta5Irrational.U_297_5 : Uω (aρ 5) (bρ 5) (1770460514531 / 6400000000000) ≤ -(14174923141875718530619 / 10000000000000000000000)

theorem Zeta5Irrational.U_297_6 : Uω (aρ 6) (bρ 6) (1770460514531 / 6400000000000) ≤ -(14963061266796872825393 / 10000000000000000000000)

theorem Zeta5Irrational.U_297_7 : Uω (aρ 7) (bρ 7) (1770460514531 / 6400000000000) ≤ -(1620636089527790470651 / 1000000000000000000000)

theorem Zeta5Irrational.U_297_8 : Uω (aρ 8) (bρ 8) (1770460514531 / 6400000000000) ≤ -(4577807632937310211223 / 2500000000000000000000)

theorem Zeta5Irrational.U_297_9 : Uω (aρ 9) (bρ 9) (1770460514531 / 6400000000000) ≤ -(23710349633563607825731 / 10000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_297 : Uρ (1770460514531 / 6400000000000) ≤ -(16973651665081069339969 / 10000000000000000000000)

theorem Zeta5Irrational.U_298_1 : Uω (aρ 1) (bρ 1) (17782348702563 / 64000000000000) ≤ -(6520927042978397703819 / 5000000000000000000000)

theorem Zeta5Irrational.U_298_2 : Uω (aρ 2) (bρ 2) (17782348702563 / 64000000000000) ≤ -(13131066023857589108797 / 10000000000000000000000)

theorem Zeta5Irrational.U_298_3 : Uω (aρ 3) (bρ 3) (17782348702563 / 64000000000000) ≤ -(13312649375703026812221 / 10000000000000000000000)

theorem Zeta5Irrational.U_298_4 : Uω (aρ 4) (bρ 4) (17782348702563 / 64000000000000) ≤ -(13624112191107404353649 / 10000000000000000000000)

theorem Zeta5Irrational.U_298_5 : Uω (aρ 5) (bρ 5) (17782348702563 / 64000000000000) ≤ -(2824938554749409884513 / 2000000000000000000000)

theorem Zeta5Irrational.U_298_6 : Uω (aρ 6) (bρ 6) (17782348702563 / 64000000000000) ≤ -(14908303102564459612481 / 10000000000000000000000)

theorem Zeta5Irrational.U_298_7 : Uω (aρ 7) (bρ 7) (17782348702563 / 64000000000000) ≤ -(16143048243093906018401 / 10000000000000000000000)

theorem Zeta5Irrational.U_298_8 : Uω (aρ 8) (bρ 8) (17782348702563 / 64000000000000) ≤ -(18227587364746944480603 / 10000000000000000000000)

theorem Zeta5Irrational.U_298_9 : Uω (aρ 9) (bρ 9) (17782348702563 / 64000000000000) ≤ -(2345044511846416428901 / 1000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_298 : Uρ (17782348702563 / 64000000000000) ≤ -(16923589864234457423761 / 10000000000000000000000)

theorem Zeta5Irrational.U_299_1 : Uω (aρ 1) (bρ 1) (2232511532477 / 8000000000000) ≤ -(6498596756097873732649 / 5000000000000000000000)

theorem Zeta5Irrational.U_299_2 : Uω (aρ 2) (bρ 2) (2232511532477 / 8000000000000) ≤ -(327150014026541970697 / 250000000000000000000)

theorem Zeta5Irrational.U_299_3 : Uω (aρ 3) (bρ 3) (2232511532477 / 8000000000000) ≤ -(1658342816041916903219 / 1250000000000000000000)

theorem Zeta5Irrational.U_299_4 : Uω (aρ 4) (bρ 4) (2232511532477 / 8000000000000) ≤ -(2715341168884718786139 / 2000000000000000000000)

theorem Zeta5Irrational.U_299_5 : Uω (aρ 5) (bρ 5) (2232511532477 / 8000000000000) ≤ -(14074715707090353918203 / 10000000000000000000000)

theorem Zeta5Irrational.U_299_6 : Uω (aρ 6) (bρ 6) (2232511532477 / 8000000000000) ≤ -(7426925208423690697017 / 5000000000000000000000)

theorem Zeta5Irrational.U_299_7 : Uω (aρ 7) (bρ 7) (2232511532477 / 8000000000000) ≤ -(3216032140314322800777 / 2000000000000000000000)

theorem Zeta5Irrational.U_299_8 : Uω (aρ 8) (bρ 8) (2232511532477 / 8000000000000) ≤ -(18144784941387903088781 / 10000000000000000000000)

theorem Zeta5Irrational.U_299_9 : Uω (aρ 9) (bρ 9) (2232511532477 / 8000000000000) ≤ -(11604530457872435747047 / 5000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_299 : Uρ (2232511532477 / 8000000000000) ≤ -(16875345848822549837269 / 10000000000000000000000)

theorem Zeta5Irrational.U_300_1 : Uω (aρ 1) (bρ 1) (17937835817069 / 64000000000000) ≤ -(12952731517223761911667 / 10000000000000000000000)

theorem Zeta5Irrational.U_300_2 : Uω (aρ 2) (bρ 2) (17937835817069 / 64000000000000) ≤ -(1630142166947326220879 / 1250000000000000000000)

theorem Zeta5Irrational.U_300_3 : Uω (aρ 3) (bρ 3) (17937835817069 / 64000000000000) ≤ -(13221045681674648191651 / 10000000000000000000000)

theorem Zeta5Irrational.U_300_4 : Uω (aρ 4) (bρ 4) (17937835817069 / 64000000000000) ≤ -(3382380970715133003067 / 2500000000000000000000)

theorem Zeta5Irrational.U_300_5 : Uω (aρ 5) (bρ 5) (17937835817069 / 64000000000000) ≤ -(1753123672217734173881 / 1250000000000000000000)

theorem Zeta5Irrational.U_300_6 : Uω (aρ 6) (bρ 6) (17937835817069 / 64000000000000) ≤ -(14799699741453893134069 / 10000000000000000000000)

theorem Zeta5Irrational.U_300_7 : Uω (aρ 7) (bρ 7) (17937835817069 / 64000000000000) ≤ -(320353845175740239713 / 200000000000000000000)

theorem Zeta5Irrational.U_300_8 : Uω (aρ 8) (bρ 8) (17937835817069 / 64000000000000) ≤ -(18062803918743756208487 / 10000000000000000000000)

theorem Zeta5Irrational.U_300_9 : Uω (aρ 9) (bρ 9) (17937835817069 / 64000000000000) ≤ -(22982841438817210519433 / 10000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_300 : Uρ (17937835817069 / 64000000000000) ≤ -(8414310178676383152373 / 5000000000000000000000)

theorem Zeta5Irrational.U_301_1 : Uω (aρ 1) (bρ 1) (9007789687161 / 32000000000000) ≤ -(12908466342858148682791 / 10000000000000000000000)

theorem Zeta5Irrational.U_301_2 : Uω (aρ 2) (bρ 2) (9007789687161 / 32000000000000) ≤ -(12996474539862435628569 / 10000000000000000000000)

theorem Zeta5Irrational.U_301_3 : Uω (aρ 3) (bρ 3) (9007789687161 / 32000000000000) ≤ -(1646944615148955121397 / 1250000000000000000000)

theorem Zeta5Irrational.U_301_4 : Uω (aρ 4) (bρ 4) (9007789687161 / 32000000000000) ≤ -(1348256418568254684709 / 1000000000000000000000)

theorem Zeta5Irrational.U_301_5 : Uω (aρ 5) (bρ 5) (9007789687161 / 32000000000000) ≤ -(3493877815151177753499 / 2500000000000000000000)

theorem Zeta5Irrational.U_301_6 : Uω (aρ 6) (bρ 6) (9007789687161 / 32000000000000) ≤ -(737292383409021471139 / 500000000000000000000)

theorem Zeta5Irrational.U_301_7 : Uω (aρ 7) (bρ 7) (9007789687161 / 32000000000000) ≤ -(7977818517863032778631 / 5000000000000000000000)

theorem Zeta5Irrational.U_301_8 : Uω (aρ 8) (bρ 8) (9007789687161 / 32000000000000) ≤ -(3596325135396607525091 / 2000000000000000000000)

theorem Zeta5Irrational.U_301_9 : Uω (aρ 9) (bρ 9) (9007789687161 / 32000000000000) ≤ -(2276934142411561312073 / 1000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_301 : Uρ (9007789687161 / 32000000000000) ≤ -(3356638919890918301819 / 2000000000000000000000)

theorem Zeta5Irrational.U_302_1 : Uω (aρ 1) (bρ 1) (723732917263 / 2560000000000) ≤ -(6432198127082150183279 / 5000000000000000000000)

theorem Zeta5Irrational.U_302_2 : Uω (aρ 2) (bρ 2) (723732917263 / 2560000000000) ≤ -(1619001298812421734721 / 1250000000000000000000)

theorem Zeta5Irrational.U_302_3 : Uω (aρ 3) (bρ 3) (723732917263 / 2560000000000) ≤ -(6565137179223193084959 / 5000000000000000000000)

theorem Zeta5Irrational.U_302_4 : Uω (aρ 4) (bρ 4) (723732917263 / 2560000000000) ≤ -(335895616554249685107 / 250000000000000000000)

theorem Zeta5Irrational.U_302_5 : Uω (aρ 5) (bρ 5) (723732917263 / 2560000000000) ≤ -(6963139434426427686679 / 5000000000000000000000)

theorem Zeta5Irrational.U_302_6 : Uω (aρ 6) (bρ 6) (723732917263 / 2560000000000) ≤ -(14692290847409693047619 / 10000000000000000000000)

theorem Zeta5Irrational.U_302_7 : Uω (aρ 7) (bρ 7) (723732917263 / 2560000000000) ≤ -(7946994641123173545093 / 5000000000000000000000)

theorem Zeta5Irrational.U_302_8 : Uω (aρ 8) (bρ 8) (723732917263 / 2560000000000) ≤ -(3580246456361628938953 / 2000000000000000000000)

theorem Zeta5Irrational.U_302_9 : Uω (aρ 9) (bρ 9) (723732917263 / 2560000000000) ≤ -(11283356655203721398811 / 5000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_302 : Uρ (723732917263 / 2560000000000) ≤ -(2092362830814368895911 / 1250000000000000000000)

theorem Zeta5Irrational.U_303_1 : Uω (aρ 1) (bρ 1) (4542766622207 / 16000000000000) ≤ -(12820519539047609253381 / 10000000000000000000000)

theorem Zeta5Irrational.U_303_2 : Uω (aρ 2) (bρ 2) (4542766622207 / 16000000000000) ≤ -(12907743127780000518383 / 10000000000000000000000)

theorem Zeta5Irrational.U_303_3 : Uω (aρ 3) (bρ 3) (4542766622207 / 16000000000000) ≤ -(6542598065307995406991 / 5000000000000000000000)

theorem Zeta5Irrational.U_303_4 : Uω (aρ 4) (bρ 4) (4542766622207 / 16000000000000) ≤ -(13389303251053762690677 / 10000000000000000000000)

theorem Zeta5Irrational.U_303_5 : Uω (aρ 5) (bρ 5) (4542766622207 / 16000000000000) ≤ -(13877289753155558398313 / 10000000000000000000000)

theorem Zeta5Irrational.U_303_6 : Uω (aρ 6) (bρ 6) (4542766622207 / 16000000000000) ≤ -(7319512993375079674599 / 5000000000000000000000)

theorem Zeta5Irrational.U_303_7 : Uω (aρ 7) (bρ 7) (4542766622207 / 16000000000000) ≤ -(15832743373195214114231 / 10000000000000000000000)

theorem Zeta5Irrational.U_303_8 : Uω (aρ 8) (bρ 8) (4542766622207 / 16000000000000) ≤ -(8910803224689173136883 / 5000000000000000000000)

theorem Zeta5Irrational.U_303_9 : Uω (aρ 9) (bρ 9) (4542766622207 / 16000000000000) ≤ -(11186760242463115104121 / 5000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_303 : Uρ (4542766622207 / 16000000000000) ≤ -(8347807468509570491919 / 5000000000000000000000)