Certified arcsine potential bounds (U08)

theorem Zeta5Irrational.U_100_1 : Uω (aρ 1) (bρ 1) (1700229173627 / 32000000000000) ≤ -(30651298815258709468093 / 10000000000000000000000)

theorem Zeta5Irrational.U_100_2 : Uω (aρ 2) (bρ 2) (1700229173627 / 32000000000000) ≤ -(78052365153972182917 / 25000000000000000000)

theorem Zeta5Irrational.U_100_3 : Uω (aρ 3) (bρ 3) (1700229173627 / 32000000000000) ≤ -(16271501953539078684187 / 5000000000000000000000)

theorem Zeta5Irrational.U_100_4 : Uω (aρ 4) (bρ 4) (1700229173627 / 32000000000000) ≤ -(35764101527639732941787 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_100 : Uρ (1700229173627 / 32000000000000) ≤ -(408736191272622967401 / 156250000000000000000)

theorem Zeta5Irrational.U_101_1 : Uω (aρ 1) (bρ 1) (107760667809 / 2000000000000) ≤ -(3049206840087526189059 / 1000000000000000000000)

theorem Zeta5Irrational.U_101_2 : Uω (aρ 2) (bρ 2) (107760667809 / 2000000000000) ≤ -(3881460057703866310033 / 1250000000000000000000)

theorem Zeta5Irrational.U_101_3 : Uω (aρ 3) (bρ 3) (107760667809 / 2000000000000) ≤ -(126352851143046549433 / 39062500000000000000)

theorem Zeta5Irrational.U_101_4 : Uω (aρ 4) (bρ 4) (107760667809 / 2000000000000) ≤ -(2216324696954452647823 / 625000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_101 : Uρ (107760667809 / 2000000000000) ≤ -(13063189390197467979439 / 5000000000000000000000)

theorem Zeta5Irrational.U_102_1 : Uω (aρ 1) (bρ 1) (886026853789 / 16000000000000) ≤ -(7545257017708016980781 / 2500000000000000000000)

theorem Zeta5Irrational.U_102_2 : Uω (aρ 2) (bρ 2) (886026853789 / 16000000000000) ≤ -(30721594805733174632861 / 10000000000000000000000)

theorem Zeta5Irrational.U_102_3 : Uω (aρ 3) (bρ 3) (886026853789 / 16000000000000) ≤ -(15982371816390557011147 / 5000000000000000000000)

theorem Zeta5Irrational.U_102_4 : Uω (aρ 4) (bρ 4) (886026853789 / 16000000000000) ≤ -(34888585885879677851941 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_102 : Uρ (886026853789 / 16000000000000) ≤ -(26063668361683246214947 / 10000000000000000000000)

theorem Zeta5Irrational.U_103_1 : Uω (aρ 1) (bρ 1) (454984182553 / 8000000000000) ≤ -(14939691773495747728407 / 5000000000000000000000)

theorem Zeta5Irrational.U_103_2 : Uω (aρ 2) (bρ 2) (454984182553 / 8000000000000) ≤ -(7600539775674981056863 / 2500000000000000000000)

theorem Zeta5Irrational.U_103_3 : Uω (aρ 3) (bρ 3) (454984182553 / 8000000000000) ≤ -(1974862208469201710963 / 625000000000000000000)

theorem Zeta5Irrational.U_103_4 : Uω (aρ 4) (bρ 4) (454984182553 / 8000000000000) ≤ -(17177194607766529470513 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_103 : Uρ (454984182553 / 8000000000000) ≤ -(26004234865315178925071 / 10000000000000000000000)

theorem Zeta5Irrational.U_104_1 : Uω (aρ 1) (bρ 1) (47892569387 / 800000000000) ≤ -(3662765284919319541649 / 1250000000000000000000)

theorem Zeta5Irrational.U_104_2 : Uω (aρ 2) (bρ 2) (47892569387 / 800000000000) ≤ -(3724076594691395072657 / 1250000000000000000000)

theorem Zeta5Irrational.U_104_3 : Uω (aρ 3) (bρ 3) (47892569387 / 800000000000) ≤ -(6180690102931800358943 / 2000000000000000000000)

theorem Zeta5Irrational.U_104_4 : Uω (aρ 4) (bρ 4) (47892569387 / 800000000000) ≤ -(33380218915095679924057 / 10000000000000000000000)

theorem Zeta5Irrational.U_104_5 : Uω (aρ 5) (bρ 5) (47892569387 / 800000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_104 : Uρ (47892569387 / 800000000000) ≤ -(25893688140692916112373 / 10000000000000000000000)

theorem Zeta5Irrational.U_105_1 : Uω (aρ 1) (bρ 1) (502867205187 / 8000000000000) ≤ -(7189101795739181296169 / 2500000000000000000000)

theorem Zeta5Irrational.U_105_2 : Uω (aρ 2) (bρ 2) (502867205187 / 8000000000000) ≤ -(1826148073864402492947 / 625000000000000000000)

theorem Zeta5Irrational.U_105_3 : Uω (aρ 3) (bρ 3) (502867205187 / 8000000000000) ≤ -(1210229666652526991207 / 400000000000000000000)

theorem Zeta5Irrational.U_105_4 : Uω (aρ 4) (bρ 4) (502867205187 / 8000000000000) ≤ -(16253431555359706555137 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_105 : Uρ (502867205187 / 8000000000000) ≤ -(1289619184650899952501 / 500000000000000000000)

theorem Zeta5Irrational.U_106_1 : Uω (aρ 1) (bρ 1) (65851089563 / 1000000000000) ≤ -(28238965150618197558677 / 10000000000000000000000)

theorem Zeta5Irrational.U_106_2 : Uω (aρ 2) (bρ 2) (65851089563 / 1000000000000) ≤ -(28675535425575934481119 / 10000000000000000000000)

theorem Zeta5Irrational.U_106_3 : Uω (aρ 3) (bρ 3) (65851089563 / 1000000000000) ≤ -(29648629442586589394293 / 10000000000000000000000)

theorem Zeta5Irrational.U_106_4 : Uω (aρ 4) (bρ 4) (65851089563 / 1000000000000) ≤ -(7928346505977301990569 / 2500000000000000000000)

theorem Zeta5Irrational.U_106_5 : Uω (aρ 5) (bρ 5) (65851089563 / 1000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_106_6 : Uω (aρ 6) (bρ 6) (65851089563 / 1000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_106_7 : Uω (aρ 7) (bρ 7) (65851089563 / 1000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_106_8 : Uω (aρ 8) (bρ 8) (65851089563 / 1000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_106 : Uρ (65851089563 / 1000000000000) ≤ -(25698694525139896448587 / 10000000000000000000000)

theorem Zeta5Irrational.U_107_1 : Uω (aρ 1) (bρ 1) (2140864814337 / 32000000000000) ≤ -(7015858174040562655969 / 2500000000000000000000)

theorem Zeta5Irrational.U_107_2 : Uω (aρ 2) (bρ 2) (2140864814337 / 32000000000000) ≤ -(3561466998880705627953 / 1250000000000000000000)

theorem Zeta5Irrational.U_107_3 : Uω (aρ 3) (bρ 3) (2140864814337 / 32000000000000) ≤ -(14722060556063304097267 / 5000000000000000000000)

theorem Zeta5Irrational.U_107_4 : Uω (aρ 4) (bρ 4) (2140864814337 / 32000000000000) ≤ -(6290166566300702968681 / 2000000000000000000000)

theorem Zeta5Irrational.U_107_5 : Uω (aρ 5) (bρ 5) (2140864814337 / 32000000000000) ≤ -(38623722698065706631519 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_107 : Uρ (2140864814337 / 32000000000000) ≤ -(12746317531850535099639 / 5000000000000000000000)

theorem Zeta5Irrational.U_108_1 : Uω (aρ 1) (bρ 1) (1087247381329 / 16000000000000) ≤ -(13945465483393786464533 / 5000000000000000000000)

theorem Zeta5Irrational.U_108_2 : Uω (aρ 2) (bρ 2) (1087247381329 / 16000000000000) ≤ -(14155637296061263611593 / 5000000000000000000000)

theorem Zeta5Irrational.U_108_3 : Uω (aρ 3) (bρ 3) (1087247381329 / 16000000000000) ≤ -(29243820169079584143899 / 10000000000000000000000)

theorem Zeta5Irrational.U_108_4 : Uω (aρ 4) (bρ 4) (1087247381329 / 16000000000000) ≤ -(31195782612954482994049 / 10000000000000000000000)

theorem Zeta5Irrational.U_108_5 : Uω (aρ 5) (bρ 5) (1087247381329 / 16000000000000) ≤ -(1174524119975398790487 / 312500000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_108 : Uρ (1087247381329 / 16000000000000) ≤ -(25390331102288743661441 / 10000000000000000000000)

theorem Zeta5Irrational.U_109_1 : Uω (aρ 1) (bρ 1) (2208124710979 / 32000000000000) ≤ -(13860678498047024113487 / 5000000000000000000000)

theorem Zeta5Irrational.U_109_2 : Uω (aρ 2) (bρ 2) (2208124710979 / 32000000000000) ≤ -(7033507858092569809221 / 2500000000000000000000)

theorem Zeta5Irrational.U_109_3 : Uω (aρ 3) (bρ 3) (2208124710979 / 32000000000000) ≤ -(29047552827988840937373 / 10000000000000000000000)

theorem Zeta5Irrational.U_109_4 : Uω (aρ 4) (bρ 4) (2208124710979 / 32000000000000) ≤ -(7736944871340474206587 / 2500000000000000000000)

theorem Zeta5Irrational.U_109_5 : Uω (aρ 5) (bρ 5) (2208124710979 / 32000000000000) ≤ -(36793825325521051304251 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_109 : Uρ (2208124710979 / 32000000000000) ≤ -(5061171551165133003801 / 2000000000000000000000)

theorem Zeta5Irrational.U_110_1 : Uω (aρ 1) (bρ 1) (4449879370279 / 64000000000000) ≤ -(3454704645218149241057 / 1250000000000000000000)

theorem Zeta5Irrational.U_110_2 : Uω (aρ 2) (bρ 2) (4449879370279 / 64000000000000) ≤ -(28046581010402783172551 / 10000000000000000000000)

theorem Zeta5Irrational.U_110_3 : Uω (aρ 3) (bρ 3) (4449879370279 / 64000000000000) ≤ -(28950880422802094840081 / 10000000000000000000000)

theorem Zeta5Irrational.U_110_4 : Uω (aρ 4) (bρ 4) (4449879370279 / 64000000000000) ≤ -(30826290029214530827127 / 10000000000000000000000)

theorem Zeta5Irrational.U_110_5 : Uω (aρ 5) (bρ 5) (4449879370279 / 64000000000000) ≤ -(36450498271319145357943 / 10000000000000000000000)

theorem Zeta5Irrational.U_110_6 : Uω (aρ 6) (bρ 6) (4449879370279 / 64000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_110_7 : Uω (aρ 7) (bρ 7) (4449879370279 / 64000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_110_8 : Uω (aρ 8) (bρ 8) (4449879370279 / 64000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_110_9 : Uω (aρ 9) (bρ 9) (4449879370279 / 64000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_110 : Uρ (4449879370279 / 64000000000000) ≤ -(12633737911984751501131 / 5000000000000000000000)

theorem Zeta5Irrational.U_111_1 : Uω (aρ 1) (bρ 1) (22417546593 / 320000000000) ≤ -(27554612974095860072559 / 10000000000000000000000)

theorem Zeta5Irrational.U_111_2 : Uω (aρ 2) (bρ 2) (22417546593 / 320000000000) ≤ -(2795989308656552345633 / 1000000000000000000000)

theorem Zeta5Irrational.U_111_3 : Uω (aρ 3) (bρ 3) (22417546593 / 320000000000) ≤ -(14427578041578170897611 / 5000000000000000000000)

theorem Zeta5Irrational.U_111_4 : Uω (aρ 4) (bρ 4) (22417546593 / 320000000000) ≤ -(3838301319880865820711 / 1250000000000000000000)

theorem Zeta5Irrational.U_111_5 : Uω (aρ 5) (bρ 5) (22417546593 / 320000000000) ≤ -(36132153701588461327473 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_111 : Uρ (22417546593 / 320000000000) ≤ -(25230982823289889081561 / 10000000000000000000000)