Certified arcsine potential bounds (U11)

theorem Zeta5Irrational.U_136_1 : Uω (aρ 1) (bρ 1) (257805414251 / 3200000000000) ≤ -(26024389347350076319563 / 10000000000000000000000)

theorem Zeta5Irrational.U_136_2 : Uω (aρ 2) (bρ 2) (257805414251 / 3200000000000) ≤ -(26368086404189464320953 / 10000000000000000000000)

theorem Zeta5Irrational.U_136_3 : Uω (aρ 3) (bρ 3) (257805414251 / 3200000000000) ≤ -(3389297048001651951123 / 1250000000000000000000)

theorem Zeta5Irrational.U_136_4 : Uω (aρ 4) (bρ 4) (257805414251 / 3200000000000) ≤ -(7147172329350315520741 / 2500000000000000000000)

theorem Zeta5Irrational.U_136_5 : Uω (aρ 5) (bρ 5) (257805414251 / 3200000000000) ≤ -(31984033130623965837531 / 10000000000000000000000)

theorem Zeta5Irrational.U_136_6 : Uω (aρ 6) (bρ 6) (257805414251 / 3200000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_136_7 : Uω (aρ 7) (bρ 7) (257805414251 / 3200000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_136_8 : Uω (aρ 8) (bρ 8) (257805414251 / 3200000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_136_9 : Uω (aρ 9) (bρ 9) (257805414251 / 3200000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_136_10 : Uω (aρ 10) (bρ 10) (257805414251 / 3200000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_136_11 : Uω (aρ 11) (bρ 11) (257805414251 / 3200000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_136_12 : Uω (aρ 12) (bρ 12) (257805414251 / 3200000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_136_13 : Uω (aρ 13) (bρ 13) (257805414251 / 3200000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_136_14 : Uω (aρ 14) (bρ 14) (257805414251 / 3200000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

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

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

theorem Zeta5Irrational.U_136 : Uρ (257805414251 / 3200000000000) ≤ -(24683602313731326949681 / 10000000000000000000000)

theorem Zeta5Irrational.U_137_1 : Uω (aρ 1) (bρ 1) (2611684090831 / 32000000000000) ≤ -(25883504479644690843899 / 10000000000000000000000)

theorem Zeta5Irrational.U_137_2 : Uω (aρ 2) (bρ 2) (2611684090831 / 32000000000000) ≤ -(5244411439855569471477 / 2000000000000000000000)

theorem Zeta5Irrational.U_137_3 : Uω (aρ 3) (bρ 3) (2611684090831 / 32000000000000) ≤ -(26956144140679057589663 / 10000000000000000000000)

theorem Zeta5Irrational.U_137_4 : Uω (aρ 4) (bρ 4) (2611684090831 / 32000000000000) ≤ -(1136048455279144140469 / 400000000000000000000)

theorem Zeta5Irrational.U_137_5 : Uω (aρ 5) (bρ 5) (2611684090831 / 32000000000000) ≤ -(15841971990601673642843 / 5000000000000000000000)

theorem Zeta5Irrational.U_137_6 : Uω (aρ 6) (bρ 6) (2611684090831 / 32000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_137_7 : Uω (aρ 7) (bρ 7) (2611684090831 / 32000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_137 : Uρ (2611684090831 / 32000000000000) ≤ -(12319697019856429271619 / 5000000000000000000000)

theorem Zeta5Irrational.U_138_1 : Uω (aρ 1) (bρ 1) (165332127447 / 2000000000000) ≤ -(25744578028657117086197 / 10000000000000000000000)

theorem Zeta5Irrational.U_138_2 : Uω (aρ 2) (bρ 2) (165332127447 / 2000000000000) ≤ -(3259767267427656465799 / 1250000000000000000000)

theorem Zeta5Irrational.U_138_3 : Uω (aρ 3) (bρ 3) (165332127447 / 2000000000000) ≤ -(3350052051316778232639 / 1250000000000000000000)

theorem Zeta5Irrational.U_138_4 : Uω (aρ 4) (bρ 4) (165332127447 / 2000000000000) ≤ -(14108699468577326473109 / 5000000000000000000000)

theorem Zeta5Irrational.U_138_5 : Uω (aρ 5) (bρ 5) (165332127447 / 2000000000000) ≤ -(627911566201869230741 / 200000000000000000000)

theorem Zeta5Irrational.U_138_6 : Uω (aρ 6) (bρ 6) (165332127447 / 2000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_138_7 : Uω (aρ 7) (bρ 7) (165332127447 / 2000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_138_8 : Uω (aρ 8) (bρ 8) (165332127447 / 2000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_138_9 : Uω (aρ 9) (bρ 9) (165332127447 / 2000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_138_10 : Uω (aρ 10) (bρ 10) (165332127447 / 2000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_138_11 : Uω (aρ 11) (bρ 11) (165332127447 / 2000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_138_12 : Uω (aρ 12) (bρ 12) (165332127447 / 2000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_138_13 : Uω (aρ 13) (bρ 13) (165332127447 / 2000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_138_14 : Uω (aρ 14) (bρ 14) (165332127447 / 2000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_138_15 : Uω (aρ 15) (bρ 15) (165332127447 / 2000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_138_16 : Uω (aρ 16) (bρ 16) (165332127447 / 2000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_138 : Uρ (165332127447 / 2000000000000) ≤ -(4919279757412061629749 / 2000000000000000000000)

theorem Zeta5Irrational.U_139_1 : Uω (aρ 1) (bρ 1) (2678943987473 / 32000000000000) ≤ -(25607556263304084967409 / 10000000000000000000000)

theorem Zeta5Irrational.U_139_2 : Uω (aρ 2) (bρ 2) (2678943987473 / 32000000000000) ≤ -(3242033609723343368109 / 1250000000000000000000)

theorem Zeta5Irrational.U_139_3 : Uω (aρ 3) (bρ 3) (2678943987473 / 32000000000000) ≤ -(5329422790878437414709 / 2000000000000000000000)

theorem Zeta5Irrational.U_139_4 : Uω (aρ 4) (bρ 4) (2678943987473 / 32000000000000) ≤ -(350463796210277297691 / 125000000000000000000)

theorem Zeta5Irrational.U_139_5 : Uω (aρ 5) (bρ 5) (2678943987473 / 32000000000000) ≤ -(15558937803900991527783 / 5000000000000000000000)

theorem Zeta5Irrational.U_139_6 : Uω (aρ 6) (bρ 6) (2678943987473 / 32000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_139_7 : Uω (aρ 7) (bρ 7) (2678943987473 / 32000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_139 : Uρ (2678943987473 / 32000000000000) ≤ -(3069316120527173883389 / 1250000000000000000000)

theorem Zeta5Irrational.U_140_1 : Uω (aρ 1) (bρ 1) (1356286967897 / 16000000000000) ≤ -(25472387635023400139573 / 10000000000000000000000)

theorem Zeta5Irrational.U_140_2 : Uω (aρ 2) (bρ 2) (1356286967897 / 16000000000000) ≤ -(12898195814616624135193 / 5000000000000000000000)

theorem Zeta5Irrational.U_140_3 : Uω (aρ 3) (bρ 3) (1356286967897 / 16000000000000) ≤ -(26496161287310828503139 / 10000000000000000000000)

theorem Zeta5Irrational.U_140_4 : Uω (aρ 4) (bρ 4) (1356286967897 / 16000000000000) ≤ -(217657707718408659519 / 78125000000000000000)

theorem Zeta5Irrational.U_140_5 : Uω (aρ 5) (bρ 5) (1356286967897 / 16000000000000) ≤ -(30849926669156202687773 / 10000000000000000000000)

theorem Zeta5Irrational.U_140_6 : Uω (aρ 6) (bρ 6) (1356286967897 / 16000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_140_7 : Uω (aρ 7) (bρ 7) (1356286967897 / 16000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_140 : Uρ (1356286967897 / 16000000000000) ≤ -(12256854110596322856331 / 5000000000000000000000)

theorem Zeta5Irrational.U_141_1 : Uω (aρ 1) (bρ 1) (694958458109 / 8000000000000) ≤ -(1260370690780799325851 / 500000000000000000000)

theorem Zeta5Irrational.U_141_2 : Uω (aρ 2) (bρ 2) (694958458109 / 8000000000000) ≤ -(3190299248545577399671 / 1250000000000000000000)

theorem Zeta5Irrational.U_141_3 : Uω (aρ 3) (bρ 3) (694958458109 / 8000000000000) ≤ -(3275127593940399875157 / 1250000000000000000000)

theorem Zeta5Irrational.U_141_4 : Uω (aρ 4) (bρ 4) (694958458109 / 8000000000000) ≤ -(13757985990762632792871 / 5000000000000000000000)

theorem Zeta5Irrational.U_141_5 : Uω (aρ 5) (bρ 5) (694958458109 / 8000000000000) ≤ -(30340243654537166784837 / 10000000000000000000000)

theorem Zeta5Irrational.U_141_6 : Uω (aρ 6) (bρ 6) (694958458109 / 8000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_141_7 : Uω (aρ 7) (bρ 7) (694958458109 / 8000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_141_8 : Uω (aρ 8) (bρ 8) (694958458109 / 8000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_141 : Uρ (694958458109 / 8000000000000) ≤ -(24434952955612677719747 / 10000000000000000000000)

theorem Zeta5Irrational.U_142_1 : Uω (aρ 1) (bρ 1) (1423546864539 / 16000000000000) ≤ -(3118660448249061296987 / 1250000000000000000000)

theorem Zeta5Irrational.U_142_2 : Uω (aρ 2) (bρ 2) (1423546864539 / 16000000000000) ≤ -(12627864479779576637511 / 5000000000000000000000)

theorem Zeta5Irrational.U_142_3 : Uω (aρ 3) (bρ 3) (1423546864539 / 16000000000000) ≤ -(25914457472574753600061 / 10000000000000000000000)

theorem Zeta5Irrational.U_142_4 : Uω (aρ 4) (bρ 4) (1423546864539 / 16000000000000) ≤ -(217470394859432947223 / 80000000000000000000)

theorem Zeta5Irrational.U_142_5 : Uω (aρ 5) (bρ 5) (1423546864539 / 16000000000000) ≤ -(7465335220405714049317 / 2500000000000000000000)

theorem Zeta5Irrational.U_142_6 : Uω (aρ 6) (bρ 6) (1423546864539 / 16000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_142_7 : Uω (aρ 7) (bρ 7) (1423546864539 / 16000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_142 : Uρ (1423546864539 / 16000000000000) ≤ -(12179839953679917785211 / 5000000000000000000000)

theorem Zeta5Irrational.U_143_1 : Uω (aρ 1) (bρ 1) (72858840643 / 800000000000) ≤ -(4939530432806504756481 / 2000000000000000000000)

theorem Zeta5Irrational.U_143_2 : Uω (aρ 2) (bρ 2) (72858840643 / 800000000000) ≤ -(12498006527585179078093 / 5000000000000000000000)

theorem Zeta5Irrational.U_143_3 : Uω (aρ 3) (bρ 3) (72858840643 / 800000000000) ≤ -(25635980836800211611331 / 10000000000000000000000)

theorem Zeta5Irrational.U_143_4 : Uω (aρ 4) (bρ 4) (72858840643 / 800000000000) ≤ -(26862818505948193076349 / 10000000000000000000000)

theorem Zeta5Irrational.U_143_5 : Uω (aρ 5) (bρ 5) (72858840643 / 800000000000) ≤ -(3676145772901062746707 / 1250000000000000000000)

theorem Zeta5Irrational.U_143_6 : Uω (aρ 6) (bρ 6) (72858840643 / 800000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_143_7 : Uω (aρ 7) (bρ 7) (72858840643 / 800000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_143_8 : Uω (aρ 8) (bρ 8) (72858840643 / 800000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_143_9 : Uω (aρ 9) (bρ 9) (72858840643 / 800000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_143_10 : Uω (aρ 10) (bρ 10) (72858840643 / 800000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_143_11 : Uω (aρ 11) (bρ 11) (72858840643 / 800000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_143_12 : Uω (aρ 12) (bρ 12) (72858840643 / 800000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_143_13 : Uω (aρ 13) (bρ 13) (72858840643 / 800000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_143_14 : Uω (aρ 14) (bρ 14) (72858840643 / 800000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_143_15 : Uω (aρ 15) (bρ 15) (72858840643 / 800000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_143_16 : Uω (aρ 16) (bρ 16) (72858840643 / 800000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_143 : Uρ (72858840643 / 800000000000) ≤ -(189746280053298967991 / 78125000000000000000)

theorem Zeta5Irrational.U_144_1 : Uω (aρ 1) (bρ 1) (762218354751 / 8000000000000) ≤ -(24212631311087841507319 / 10000000000000000000000)

theorem Zeta5Irrational.U_144_2 : Uω (aρ 2) (bρ 2) (762218354751 / 8000000000000) ≤ -(24496038767204679231087 / 10000000000000000000000)

theorem Zeta5Irrational.U_144_3 : Uω (aρ 3) (bρ 3) (762218354751 / 8000000000000) ≤ -(25101527446924252214789 / 10000000000000000000000)

theorem Zeta5Irrational.U_144_4 : Uω (aρ 4) (bρ 4) (762218354751 / 8000000000000) ≤ -(13125734602345873881497 / 5000000000000000000000)

theorem Zeta5Irrational.U_144_5 : Uω (aρ 5) (bρ 5) (762218354751 / 8000000000000) ≤ -(28572647461235244444859 / 10000000000000000000000)

theorem Zeta5Irrational.U_144_6 : Uω (aρ 6) (bρ 6) (762218354751 / 8000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_144_7 : Uω (aρ 7) (bρ 7) (762218354751 / 8000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_144_8 : Uω (aρ 8) (bρ 8) (762218354751 / 8000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_144 : Uρ (762218354751 / 8000000000000) ≤ -(6037851914004356594239 / 2500000000000000000000)

theorem Zeta5Irrational.U_145_1 : Uω (aρ 1) (bρ 1) (24870259471 / 250000000000) ≤ -(5937514892280973947171 / 2500000000000000000000)

theorem Zeta5Irrational.U_145_2 : Uω (aρ 2) (bρ 2) (24870259471 / 250000000000) ≤ -(24019940915667638914899 / 10000000000000000000000)

theorem Zeta5Irrational.U_145_3 : Uω (aρ 3) (bρ 3) (24870259471 / 250000000000) ≤ -(12297242736766437788551 / 5000000000000000000000)

theorem Zeta5Irrational.U_145_4 : Uω (aρ 4) (bρ 4) (24870259471 / 250000000000) ≤ -(25676711922883085692547 / 10000000000000000000000)

theorem Zeta5Irrational.U_145_5 : Uω (aρ 5) (bρ 5) (24870259471 / 250000000000) ≤ -(13905575961864639085561 / 5000000000000000000000)

theorem Zeta5Irrational.U_145_6 : Uω (aρ 6) (bρ 6) (24870259471 / 250000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_145_7 : Uω (aρ 7) (bρ 7) (24870259471 / 250000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_145_8 : Uω (aρ 8) (bρ 8) (24870259471 / 250000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_145_9 : Uω (aρ 9) (bρ 9) (24870259471 / 250000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_145_10 : Uω (aρ 10) (bρ 10) (24870259471 / 250000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_145_11 : Uω (aρ 11) (bρ 11) (24870259471 / 250000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_145_12 : Uω (aρ 12) (bρ 12) (24870259471 / 250000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_145_13 : Uω (aρ 13) (bρ 13) (24870259471 / 250000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_145_14 : Uω (aρ 14) (bρ 14) (24870259471 / 250000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_145_15 : Uω (aρ 15) (bρ 15) (24870259471 / 250000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_145_16 : Uω (aρ 16) (bρ 16) (24870259471 / 250000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_145 : Uρ (24870259471 / 250000000000) ≤ -(6006179333855527615251 / 2500000000000000000000)

theorem Zeta5Irrational.U_146_1 : Uω (aρ 1) (bρ 1) (1614118950931 / 16000000000000) ≤ -(23600490741746310132633 / 10000000000000000000000)

theorem Zeta5Irrational.U_146_2 : Uω (aρ 2) (bρ 2) (1614118950931 / 16000000000000) ≤ -(23866145357694081674823 / 10000000000000000000000)

theorem Zeta5Irrational.U_146_3 : Uω (aρ 3) (bρ 3) (1614118950931 / 16000000000000) ≤ -(4886213425407009894147 / 2000000000000000000000)

theorem Zeta5Irrational.U_146_4 : Uω (aρ 4) (bρ 4) (1614118950931 / 16000000000000) ≤ -(25492478055288563125353 / 10000000000000000000000)

theorem Zeta5Irrational.U_146_5 : Uω (aρ 5) (bρ 5) (1614118950931 / 16000000000000) ≤ -(27571482204858512832921 / 10000000000000000000000)

theorem Zeta5Irrational.U_146_6 : Uω (aρ 6) (bρ 6) (1614118950931 / 16000000000000) ≤ -(17303896956176881585291 / 5000000000000000000000)

theorem Zeta5Irrational.U_146_7 : Uω (aρ 7) (bρ 7) (1614118950931 / 16000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_146 : Uρ (1614118950931 / 16000000000000) ≤ -(1189858212400226247237 / 500000000000000000000)

theorem Zeta5Irrational.U_147_1 : Uω (aρ 1) (bρ 1) (818270647859 / 8000000000000) ≤ -(586328171474169128263 / 250000000000000000000)

theorem Zeta5Irrational.U_147_2 : Uω (aρ 2) (bρ 2) (818270647859 / 8000000000000) ≤ -(23714685092528748377319 / 10000000000000000000000)

theorem Zeta5Irrational.U_147_3 : Uω (aρ 3) (bρ 3) (818270647859 / 8000000000000) ≤ -(3033787739285829484113 / 1250000000000000000000)

theorem Zeta5Irrational.U_147_4 : Uω (aρ 4) (bρ 4) (818270647859 / 8000000000000) ≤ -(25311691807556838955743 / 10000000000000000000000)

theorem Zeta5Irrational.U_147_5 : Uω (aρ 5) (bρ 5) (818270647859 / 8000000000000) ≤ -(13669097951678662512941 / 5000000000000000000000)

theorem Zeta5Irrational.U_147_6 : Uω (aρ 6) (bρ 6) (818270647859 / 8000000000000) ≤ -(2102041636154490140537 / 625000000000000000000)

theorem Zeta5Irrational.U_147_7 : Uω (aρ 7) (bρ 7) (818270647859 / 8000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_147_8 : Uω (aρ 8) (bρ 8) (818270647859 / 8000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_147 : Uρ (818270647859 / 8000000000000) ≤ -(23680709076845825592017 / 10000000000000000000000)