Certified arcsine potential bounds (U04)

theorem Zeta5Irrational.U_52_1 : Uω (aρ 1) (bρ 1) (41071178579 / 2000000000000) ≤ -(10677082056811715580897 / 2500000000000000000000)

theorem Zeta5Irrational.U_52_2 : Uω (aρ 2) (bρ 2) (41071178579 / 2000000000000) ≤ -(45357165225401575594487 / 10000000000000000000000)

theorem Zeta5Irrational.U_52_3 : Uω (aρ 3) (bρ 3) (41071178579 / 2000000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_52_4 : Uω (aρ 4) (bρ 4) (41071178579 / 2000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_52_5 : Uω (aρ 5) (bρ 5) (41071178579 / 2000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_52 : Uρ (41071178579 / 2000000000000) ≤ -(28080017513087561787613 / 10000000000000000000000)

theorem Zeta5Irrational.U_53_1 : Uω (aρ 1) (bρ 1) (34934779437 / 1600000000000) ≤ -(8362590788884110065771 / 2000000000000000000000)

theorem Zeta5Irrational.U_53_2 : Uω (aρ 2) (bρ 2) (34934779437 / 1600000000000) ≤ -(1764723410583048654431 / 400000000000000000000)

theorem Zeta5Irrational.U_53_3 : Uω (aρ 3) (bρ 3) (34934779437 / 1600000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_53_4 : Uω (aρ 4) (bρ 4) (34934779437 / 1600000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_53_5 : Uω (aρ 5) (bρ 5) (34934779437 / 1600000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_53_6 : Uω (aρ 6) (bρ 6) (34934779437 / 1600000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_53_7 : Uω (aρ 7) (bρ 7) (34934779437 / 1600000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_53 : Uρ (34934779437 / 1600000000000) ≤ -(28034084278989397482397 / 10000000000000000000000)

theorem Zeta5Irrational.U_54_1 : Uω (aρ 1) (bρ 1) (92531540027 / 4000000000000) ≤ -(20496075350021699854459 / 5000000000000000000000)

theorem Zeta5Irrational.U_54_2 : Uω (aρ 2) (bρ 2) (92531540027 / 4000000000000) ≤ -(21517316490172672414011 / 5000000000000000000000)

theorem Zeta5Irrational.U_54_3 : Uω (aρ 3) (bρ 3) (92531540027 / 4000000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_54_4 : Uω (aρ 4) (bρ 4) (92531540027 / 4000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_54_5 : Uω (aρ 5) (bρ 5) (92531540027 / 4000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_54_6 : Uω (aρ 6) (bρ 6) (92531540027 / 4000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_54_7 : Uω (aρ 7) (bρ 7) (92531540027 / 4000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_54_8 : Uω (aρ 8) (bρ 8) (92531540027 / 4000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_54_9 : Uω (aρ 9) (bρ 9) (92531540027 / 4000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_54_10 : Uω (aρ 10) (bρ 10) (92531540027 / 4000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_54_11 : Uω (aρ 11) (bρ 11) (92531540027 / 4000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_54_12 : Uω (aρ 12) (bρ 12) (92531540027 / 4000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_54_13 : Uω (aρ 13) (bρ 13) (92531540027 / 4000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_54_14 : Uω (aρ 14) (bρ 14) (92531540027 / 4000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

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

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

theorem Zeta5Irrational.U_54 : Uρ (92531540027 / 4000000000000) ≤ -(27993521821896214356369 / 10000000000000000000000)

theorem Zeta5Irrational.U_55_1 : Uω (aρ 1) (bρ 1) (6432545181 / 250000000000) ≤ -(19765204149885397770799 / 5000000000000000000000)

theorem Zeta5Irrational.U_55_2 : Uω (aρ 2) (bρ 2) (6432545181 / 250000000000) ≤ -(20598094011261554616851 / 5000000000000000000000)

theorem Zeta5Irrational.U_55_3 : Uω (aρ 3) (bρ 3) (6432545181 / 250000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_55_4 : Uω (aρ 4) (bρ 4) (6432545181 / 250000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_55_5 : Uω (aρ 5) (bρ 5) (6432545181 / 250000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_55 : Uρ (6432545181 / 250000000000) ≤ -(3490496070168995482161 / 1250000000000000000000)

theorem Zeta5Irrational.U_56_1 : Uω (aρ 1) (bρ 1) (213931144553 / 8000000000000) ≤ -(19507472141650856272829 / 5000000000000000000000)

theorem Zeta5Irrational.U_56_2 : Uω (aρ 2) (bρ 2) (213931144553 / 8000000000000) ≤ -(40569578445247696299549 / 10000000000000000000000)

theorem Zeta5Irrational.U_56_3 : Uω (aρ 3) (bρ 3) (213931144553 / 8000000000000) ≤ -(46974446160582055541859 / 10000000000000000000000)

theorem Zeta5Irrational.U_56_4 : Uω (aρ 4) (bρ 4) (213931144553 / 8000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_56_5 : Uω (aρ 5) (bρ 5) (213931144553 / 8000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_56 : Uρ (213931144553 / 8000000000000) ≤ -(13863102336300848802043 / 5000000000000000000000)

theorem Zeta5Irrational.U_57_1 : Uω (aρ 1) (bρ 1) (435951987867 / 16000000000000) ≤ -(38766920785090621061557 / 10000000000000000000000)

theorem Zeta5Irrational.U_57_2 : Uω (aρ 2) (bρ 2) (435951987867 / 16000000000000) ≤ -(8054285062790282216923 / 2000000000000000000000)

theorem Zeta5Irrational.U_57_3 : Uω (aρ 3) (bρ 3) (435951987867 / 16000000000000) ≤ -(46080796762313820607457 / 10000000000000000000000)

theorem Zeta5Irrational.U_57_4 : Uω (aρ 4) (bρ 4) (435951987867 / 16000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_57_5 : Uω (aρ 5) (bρ 5) (435951987867 / 16000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_57 : Uρ (435951987867 / 16000000000000) ≤ -(5535288239441576547317 / 2000000000000000000000)

theorem Zeta5Irrational.U_58_1 : Uω (aρ 1) (bρ 1) (111010421657 / 4000000000000) ≤ -(38524944569892604705309 / 10000000000000000000000)

theorem Zeta5Irrational.U_58_2 : Uω (aρ 2) (bρ 2) (111010421657 / 4000000000000) ≤ -(19991241739447185349551 / 5000000000000000000000)

theorem Zeta5Irrational.U_58_3 : Uω (aρ 3) (bρ 3) (111010421657 / 4000000000000) ≤ -(45334787031774164684501 / 10000000000000000000000)

theorem Zeta5Irrational.U_58_4 : Uω (aρ 4) (bρ 4) (111010421657 / 4000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_58_5 : Uω (aρ 5) (bρ 5) (111010421657 / 4000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_58_6 : Uω (aρ 6) (bρ 6) (111010421657 / 4000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_58_7 : Uω (aρ 7) (bρ 7) (111010421657 / 4000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_58_8 : Uω (aρ 8) (bρ 8) (111010421657 / 4000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_58_9 : Uω (aρ 9) (bρ 9) (111010421657 / 4000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_58_10 : Uω (aρ 10) (bρ 10) (111010421657 / 4000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_58_11 : Uω (aρ 11) (bρ 11) (111010421657 / 4000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_58_12 : Uω (aρ 12) (bρ 12) (111010421657 / 4000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_58_13 : Uω (aρ 13) (bρ 13) (111010421657 / 4000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_58_14 : Uω (aρ 14) (bρ 14) (111010421657 / 4000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

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

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

theorem Zeta5Irrational.U_58 : Uρ (111010421657 / 4000000000000) ≤ -(27633351600905070070711 / 10000000000000000000000)

theorem Zeta5Irrational.U_59_1 : Uω (aρ 1) (bρ 1) (452131385389 / 16000000000000) ≤ -(19144362876016614852763 / 5000000000000000000000)

theorem Zeta5Irrational.U_59_2 : Uω (aρ 2) (bρ 2) (452131385389 / 16000000000000) ≤ -(7940433853980462156227 / 2000000000000000000000)

theorem Zeta5Irrational.U_59_3 : Uω (aρ 3) (bρ 3) (452131385389 / 16000000000000) ≤ -(44683833187501300822249 / 10000000000000000000000)

theorem Zeta5Irrational.U_59_4 : Uω (aρ 4) (bρ 4) (452131385389 / 16000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_59_5 : Uω (aρ 5) (bρ 5) (452131385389 / 16000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_59 : Uρ (452131385389 / 16000000000000) ≤ -(3449332247790833623903 / 1250000000000000000000)

theorem Zeta5Irrational.U_60_1 : Uω (aρ 1) (bρ 1) (912352469539 / 32000000000000) ≤ -(19086345216926816612793 / 5000000000000000000000)

theorem Zeta5Irrational.U_60_2 : Uω (aρ 2) (bρ 2) (912352469539 / 32000000000000) ≤ -(791301614016874710873 / 200000000000000000000)

theorem Zeta5Irrational.U_60_3 : Uω (aρ 3) (bρ 3) (912352469539 / 32000000000000) ≤ -(22192513593791331396327 / 5000000000000000000000)

theorem Zeta5Irrational.U_60_4 : Uω (aρ 4) (bρ 4) (912352469539 / 32000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_60_5 : Uω (aρ 5) (bρ 5) (912352469539 / 32000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_60 : Uρ (912352469539 / 32000000000000) ≤ -(27576568517522084070211 / 10000000000000000000000)

theorem Zeta5Irrational.U_61_1 : Uω (aρ 1) (bρ 1) (9204421683 / 320000000000) ≤ -(19028997467622808750993 / 5000000000000000000000)

theorem Zeta5Irrational.U_61_2 : Uω (aρ 2) (bρ 2) (9204421683 / 320000000000) ≤ -(19714977607198277378769 / 5000000000000000000000)

theorem Zeta5Irrational.U_61_3 : Uω (aρ 3) (bρ 3) (9204421683 / 320000000000) ≤ -(22050425163131483974353 / 5000000000000000000000)

theorem Zeta5Irrational.U_61_4 : Uω (aρ 4) (bρ 4) (9204421683 / 320000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_61_5 : Uω (aρ 5) (bρ 5) (9204421683 / 320000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_61_6 : Uω (aρ 6) (bρ 6) (9204421683 / 320000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_61_7 : Uω (aρ 7) (bρ 7) (9204421683 / 320000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_61_8 : Uω (aρ 8) (bρ 8) (9204421683 / 320000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_61_9 : Uω (aρ 9) (bρ 9) (9204421683 / 320000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_61_10 : Uω (aρ 10) (bρ 10) (9204421683 / 320000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_61_11 : Uω (aρ 11) (bρ 11) (9204421683 / 320000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_61_12 : Uω (aρ 12) (bρ 12) (9204421683 / 320000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_61_13 : Uω (aρ 13) (bρ 13) (9204421683 / 320000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_61_14 : Uω (aρ 14) (bρ 14) (9204421683 / 320000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_61_15 : Uω (aρ 15) (bρ 15) (9204421683 / 320000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_61_16 : Uω (aρ 16) (bρ 16) (9204421683 / 320000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_61 : Uρ (9204421683 / 320000000000) ≤ -(27559179089952747868089 / 10000000000000000000000)

theorem Zeta5Irrational.U_62_1 : Uω (aρ 1) (bρ 1) (928531867061 / 32000000000000) ≤ -(7588921694372028541901 / 2000000000000000000000)

theorem Zeta5Irrational.U_62_2 : Uω (aρ 2) (bρ 2) (928531867061 / 32000000000000) ≤ -(39296734472550530549671 / 10000000000000000000000)

theorem Zeta5Irrational.U_62_3 : Uω (aρ 3) (bρ 3) (928531867061 / 32000000000000) ≤ -(2739346502402930483743 / 625000000000000000000)

theorem Zeta5Irrational.U_62_4 : Uω (aρ 4) (bρ 4) (928531867061 / 32000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_62_5 : Uω (aρ 5) (bρ 5) (928531867061 / 32000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_62 : Uρ (928531867061 / 32000000000000) ≤ -(6885603038426120732053 / 2500000000000000000000)

theorem Zeta5Irrational.U_63_1 : Uω (aρ 1) (bρ 1) (468310782911 / 16000000000000) ≤ -(4729062664342235400103 / 1250000000000000000000)

theorem Zeta5Irrational.U_63_2 : Uω (aρ 2) (bρ 2) (468310782911 / 16000000000000) ≤ -(9791340702794776363367 / 2500000000000000000000)

theorem Zeta5Irrational.U_63_3 : Uω (aρ 3) (bρ 3) (468310782911 / 16000000000000) ≤ -(43569679477317919277667 / 10000000000000000000000)

theorem Zeta5Irrational.U_63_4 : Uω (aρ 4) (bρ 4) (468310782911 / 16000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_63_5 : Uω (aρ 5) (bρ 5) (468310782911 / 16000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_63 : Uρ (468310782911 / 16000000000000) ≤ -(27526204409010125473529 / 10000000000000000000000)