Certified arcsine potential bounds (U02)

theorem Zeta5Irrational.U_24_1 : Uω (aρ 1) (bρ 1) (280457333 / 200000000000) ≤ -(53593986196108414589993 / 10000000000000000000000)

theorem Zeta5Irrational.U_24_2 : Uω (aρ 2) (bρ 2) (280457333 / 200000000000) ≤ -(52043031588685060884247 / 10000000000000000000000)

theorem Zeta5Irrational.U_24_3 : Uω (aρ 3) (bρ 3) (280457333 / 200000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_24_4 : Uω (aρ 4) (bρ 4) (280457333 / 200000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_24_5 : Uω (aρ 5) (bρ 5) (280457333 / 200000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_24_6 : Uω (aρ 6) (bρ 6) (280457333 / 200000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_24_7 : Uω (aρ 7) (bρ 7) (280457333 / 200000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_24_8 : Uω (aρ 8) (bρ 8) (280457333 / 200000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_24_9 : Uω (aρ 9) (bρ 9) (280457333 / 200000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_24_10 : Uω (aρ 10) (bρ 10) (280457333 / 200000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_24_11 : Uω (aρ 11) (bρ 11) (280457333 / 200000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_24_12 : Uω (aρ 12) (bρ 12) (280457333 / 200000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_24_13 : Uω (aρ 13) (bρ 13) (280457333 / 200000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_24_14 : Uω (aρ 14) (bρ 14) (280457333 / 200000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_24_15 : Uω (aρ 15) (bρ 15) (280457333 / 200000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_24_16 : Uω (aρ 16) (bρ 16) (280457333 / 200000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_24 : Uρ (280457333 / 200000000000) ≤ -(28391530796819438246561 / 10000000000000000000000)

theorem Zeta5Irrational.U_25_1 : Uω (aρ 1) (bρ 1) (6519108259 / 4000000000000) ≤ -(27066132270492516043287 / 5000000000000000000000)

theorem Zeta5Irrational.U_25_2 : Uω (aρ 2) (bρ 2) (6519108259 / 4000000000000) ≤ -(52730540587954460599153 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_25 : Uρ (6519108259 / 4000000000000) ≤ -(14208726599741697552523 / 5000000000000000000000)

theorem Zeta5Irrational.U_26_1 : Uω (aρ 1) (bρ 1) (3714534929 / 2000000000000) ≤ -(13676747820096012817053 / 2500000000000000000000)

theorem Zeta5Irrational.U_26_2 : Uω (aρ 2) (bρ 2) (3714534929 / 2000000000000) ≤ -(26776440993766361792693 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_26 : Uρ (3714534929 / 2000000000000) ≤ -(28447732623893462494161 / 10000000000000000000000)

theorem Zeta5Irrational.U_27_1 : Uω (aρ 1) (bρ 1) (8339031457 / 4000000000000) ≤ -(55324376016046487597617 / 10000000000000000000000)

theorem Zeta5Irrational.U_27_2 : Uω (aρ 2) (bρ 2) (8339031457 / 4000000000000) ≤ -(10926753652502540317131 / 2000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_27 : Uρ (8339031457 / 4000000000000) ≤ -(5697216077868329425469 / 2000000000000000000000)

theorem Zeta5Irrational.U_28_1 : Uω (aρ 1) (bρ 1) (289031033 / 125000000000) ≤ -(27996295164352877284557 / 5000000000000000000000)

theorem Zeta5Irrational.U_28_2 : Uω (aρ 2) (bρ 2) (289031033 / 125000000000) ≤ -(57268912150832389796717 / 10000000000000000000000)

theorem Zeta5Irrational.U_28_3 : Uω (aρ 3) (bρ 3) (289031033 / 125000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_28_4 : Uω (aρ 4) (bρ 4) (289031033 / 125000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_28_5 : Uω (aρ 5) (bρ 5) (289031033 / 125000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_28_6 : Uω (aρ 6) (bρ 6) (289031033 / 125000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_28_7 : Uω (aρ 7) (bρ 7) (289031033 / 125000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_28_8 : Uω (aρ 8) (bρ 8) (289031033 / 125000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_28_9 : Uω (aρ 9) (bρ 9) (289031033 / 125000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_28_10 : Uω (aρ 10) (bρ 10) (289031033 / 125000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_28_11 : Uω (aρ 11) (bρ 11) (289031033 / 125000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_28_12 : Uω (aρ 12) (bρ 12) (289031033 / 125000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_28_13 : Uω (aρ 13) (bρ 13) (289031033 / 125000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_28_14 : Uω (aρ 14) (bρ 14) (289031033 / 125000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

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

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

theorem Zeta5Irrational.U_28 : Uρ (289031033 / 125000000000) ≤ -(7142692332734663141767 / 2500000000000000000000)

theorem Zeta5Irrational.U_29_1 : Uω (aρ 1) (bρ 1) (124379927 / 40000000000) ≤ -(14737682003414632220873 / 2500000000000000000000)

theorem Zeta5Irrational.U_29_2 : Uω (aρ 2) (bρ 2) (124379927 / 40000000000) ≤ -(57268912150832389796717 / 10000000000000000000000)

theorem Zeta5Irrational.U_29_3 : Uω (aρ 3) (bρ 3) (124379927 / 40000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_29_4 : Uω (aρ 4) (bρ 4) (124379927 / 40000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_29_5 : Uω (aρ 5) (bρ 5) (124379927 / 40000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_29_6 : Uω (aρ 6) (bρ 6) (124379927 / 40000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_29_7 : Uω (aρ 7) (bρ 7) (124379927 / 40000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_29_8 : Uω (aρ 8) (bρ 8) (124379927 / 40000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_29_9 : Uω (aρ 9) (bρ 9) (124379927 / 40000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_29_10 : Uω (aρ 10) (bρ 10) (124379927 / 40000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_29_11 : Uω (aρ 11) (bρ 11) (124379927 / 40000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_29_12 : Uω (aρ 12) (bρ 12) (124379927 / 40000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_29_13 : Uω (aρ 13) (bρ 13) (124379927 / 40000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_29_14 : Uω (aρ 14) (bρ 14) (124379927 / 40000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_29_15 : Uω (aρ 15) (bρ 15) (124379927 / 40000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_29_16 : Uω (aρ 16) (bρ 16) (124379927 / 40000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_29 : Uρ (124379927 / 40000000000) ≤ -(893808622258701750129 / 312500000000000000000)

theorem Zeta5Irrational.U_30_1 : Uω (aρ 1) (bρ 1) (7016246261 / 2000000000000) ≤ -(1910848611840935650757 / 312500000000000000000)

theorem Zeta5Irrational.U_30_2 : Uω (aρ 2) (bρ 2) (7016246261 / 2000000000000) ≤ -(57268912150832389796717 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_30 : Uρ (7016246261 / 2000000000000) ≤ -(1789060791099578778267 / 625000000000000000000)

theorem Zeta5Irrational.U_35_1 : Uω (aρ 1) (bρ 1) (19572466643 / 2000000000000) ≤ -(5896789100911232295581 / 1000000000000000000000)

theorem Zeta5Irrational.U_35_2 : Uω (aρ 2) (bρ 2) (19572466643 / 2000000000000) ≤ -(57268912150832389796717 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_35 : Uρ (19572466643 / 2000000000000) ≤ -(14301028195703943639221 / 5000000000000000000000)

theorem Zeta5Irrational.U_36_1 : Uω (aρ 1) (bρ 1) (40732008867 / 4000000000000) ≤ -(28671312100952179027439 / 5000000000000000000000)

theorem Zeta5Irrational.U_36_2 : Uω (aρ 2) (bρ 2) (40732008867 / 4000000000000) ≤ -(57268912150832389796717 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_36 : Uρ (40732008867 / 4000000000000) ≤ -(3573120717747316300783 / 1250000000000000000000)

theorem Zeta5Irrational.U_37_1 : Uω (aρ 1) (bρ 1) (1322471389 / 125000000000) ≤ -(437620085001547802181 / 78125000000000000000)

theorem Zeta5Irrational.U_37_2 : Uω (aρ 2) (bρ 2) (1322471389 / 125000000000) ≤ -(57268912150832389796717 / 10000000000000000000000)

theorem Zeta5Irrational.U_37_3 : Uω (aρ 3) (bρ 3) (1322471389 / 125000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_37_4 : Uω (aρ 4) (bρ 4) (1322471389 / 125000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_37_5 : Uω (aρ 5) (bρ 5) (1322471389 / 125000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_37_6 : Uω (aρ 6) (bρ 6) (1322471389 / 125000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_37_7 : Uω (aρ 7) (bρ 7) (1322471389 / 125000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_37_8 : Uω (aρ 8) (bρ 8) (1322471389 / 125000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_37_9 : Uω (aρ 9) (bρ 9) (1322471389 / 125000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_37_10 : Uω (aρ 10) (bρ 10) (1322471389 / 125000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_37_11 : Uω (aρ 11) (bρ 11) (1322471389 / 125000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_37_12 : Uω (aρ 12) (bρ 12) (1322471389 / 125000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_37_13 : Uω (aρ 13) (bρ 13) (1322471389 / 125000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_37_14 : Uω (aρ 14) (bρ 14) (1322471389 / 125000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

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

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

theorem Zeta5Irrational.U_37 : Uρ (1322471389 / 125000000000) ≤ -(28571008882018903964403 / 10000000000000000000000)

theorem Zeta5Irrational.U_38_1 : Uω (aρ 1) (bρ 1) (4549323561 / 400000000000) ≤ -(53882828561175423362757 / 10000000000000000000000)

theorem Zeta5Irrational.U_38_2 : Uω (aρ 2) (bρ 2) (4549323561 / 400000000000) ≤ -(57268912150832389796717 / 10000000000000000000000)

theorem Zeta5Irrational.U_38_3 : Uω (aρ 3) (bρ 3) (4549323561 / 400000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_38_4 : Uω (aρ 4) (bρ 4) (4549323561 / 400000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_38_5 : Uω (aρ 5) (bρ 5) (4549323561 / 400000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_38_6 : Uω (aρ 6) (bρ 6) (4549323561 / 400000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_38_7 : Uω (aρ 7) (bρ 7) (4549323561 / 400000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_38_8 : Uω (aρ 8) (bρ 8) (4549323561 / 400000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_38_9 : Uω (aρ 9) (bρ 9) (4549323561 / 400000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_38_10 : Uω (aρ 10) (bρ 10) (4549323561 / 400000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_38_11 : Uω (aρ 11) (bρ 11) (4549323561 / 400000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_38_12 : Uω (aρ 12) (bρ 12) (4549323561 / 400000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_38_13 : Uω (aρ 13) (bρ 13) (4549323561 / 400000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_38_14 : Uω (aρ 14) (bρ 14) (4549323561 / 400000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_38_15 : Uω (aρ 15) (bρ 15) (4549323561 / 400000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_38_16 : Uω (aρ 16) (bρ 16) (4549323561 / 400000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_38 : Uρ (4549323561 / 400000000000) ≤ -(142742919640776502841 / 50000000000000000000)

theorem Zeta5Irrational.U_39_1 : Uω (aρ 1) (bρ 1) (12166846693 / 1000000000000) ≤ -(52178850672124585216629 / 10000000000000000000000)

theorem Zeta5Irrational.U_39_2 : Uω (aρ 2) (bρ 2) (12166846693 / 1000000000000) ≤ -(57268912150832389796717 / 10000000000000000000000)

theorem Zeta5Irrational.U_39_3 : Uω (aρ 3) (bρ 3) (12166846693 / 1000000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_39_4 : Uω (aρ 4) (bρ 4) (12166846693 / 1000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_39 : Uρ (12166846693 / 1000000000000) ≤ -(5706133116954878622153 / 2000000000000000000000)