Certified arcsine potential bounds (U06)

theorem Zeta5Irrational.U_76_1 : Uω (aρ 1) (bρ 1) (143369216701 / 4000000000000) ≤ -(17644447654831053876417 / 5000000000000000000000)

theorem Zeta5Irrational.U_76_2 : Uω (aρ 2) (bρ 2) (143369216701 / 4000000000000) ≤ -(36262016923645122436277 / 10000000000000000000000)

theorem Zeta5Irrational.U_76_3 : Uω (aρ 3) (bρ 3) (143369216701 / 4000000000000) ≤ -(38888475953383457362861 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_76 : Uρ (143369216701 / 4000000000000) ≤ -(27212905725500611600959 / 10000000000000000000000)

theorem Zeta5Irrational.U_77_1 : Uω (aρ 1) (bρ 1) (75729457731 / 2000000000000) ≤ -(17310558705766996086987 / 5000000000000000000000)

theorem Zeta5Irrational.U_77_2 : Uω (aρ 2) (bρ 2) (75729457731 / 2000000000000) ≤ -(17759863104573821333591 / 5000000000000000000000)

theorem Zeta5Irrational.U_77_3 : Uω (aρ 3) (bρ 3) (75729457731 / 2000000000000) ≤ -(1893432330977563126623 / 500000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_77 : Uρ (75729457731 / 2000000000000) ≤ -(5428044264104939481293 / 2000000000000000000000)

theorem Zeta5Irrational.U_78_1 : Uω (aρ 1) (bρ 1) (20954789123 / 500000000000) ≤ -(16703211212357127756093 / 5000000000000000000000)

theorem Zeta5Irrational.U_78_2 : Uω (aρ 2) (bρ 2) (20954789123 / 500000000000) ≤ -(8546436382655285391233 / 2500000000000000000000)

theorem Zeta5Irrational.U_78_3 : Uω (aρ 3) (bρ 3) (20954789123 / 500000000000) ≤ -(36129596021937323314463 / 10000000000000000000000)

theorem Zeta5Irrational.U_78_4 : Uω (aρ 4) (bρ 4) (20954789123 / 500000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_78_5 : Uω (aρ 5) (bρ 5) (20954789123 / 500000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_78_6 : Uω (aρ 6) (bρ 6) (20954789123 / 500000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_78_7 : Uω (aρ 7) (bρ 7) (20954789123 / 500000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_78_8 : Uω (aρ 8) (bρ 8) (20954789123 / 500000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_78_9 : Uω (aρ 9) (bρ 9) (20954789123 / 500000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_78_10 : Uω (aρ 10) (bρ 10) (20954789123 / 500000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_78_11 : Uω (aρ 11) (bρ 11) (20954789123 / 500000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_78_12 : Uω (aρ 12) (bρ 12) (20954789123 / 500000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_78_13 : Uω (aρ 13) (bρ 13) (20954789123 / 500000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_78_14 : Uω (aρ 14) (bρ 14) (20954789123 / 500000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_78_15 : Uω (aρ 15) (bρ 15) (20954789123 / 500000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_78_16 : Uω (aρ 16) (bρ 16) (20954789123 / 500000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_78 : Uρ (20954789123 / 500000000000) ≤ -(27013468316499378362551 / 10000000000000000000000)

theorem Zeta5Irrational.U_79_1 : Uω (aρ 1) (bρ 1) (694494763253 / 16000000000000) ≤ -(8248019133811670168773 / 2500000000000000000000)

theorem Zeta5Irrational.U_79_2 : Uω (aρ 2) (bρ 2) (694494763253 / 16000000000000) ≤ -(33734931655425398758109 / 10000000000000000000000)

theorem Zeta5Irrational.U_79_3 : Uω (aρ 3) (bρ 3) (694494763253 / 16000000000000) ≤ -(17781582814941265651163 / 5000000000000000000000)

theorem Zeta5Irrational.U_79_4 : Uω (aρ 4) (bρ 4) (694494763253 / 16000000000000) ≤ -(2625083115715732209859 / 625000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_79 : Uρ (694494763253 / 16000000000000) ≤ -(2675052424918429982301 / 1000000000000000000000)

theorem Zeta5Irrational.U_80_1 : Uω (aρ 1) (bρ 1) (1412931037823 / 32000000000000) ≤ -(6558236691624471248019 / 2000000000000000000000)

theorem Zeta5Irrational.U_80_2 : Uω (aρ 2) (bρ 2) (1412931037823 / 32000000000000) ≤ -(33517056778454642676983 / 10000000000000000000000)

theorem Zeta5Irrational.U_80_3 : Uω (aρ 3) (bρ 3) (1412931037823 / 32000000000000) ≤ -(27572364292843690767 / 7812500000000000000)

theorem Zeta5Irrational.U_80_4 : Uω (aρ 4) (bρ 4) (1412931037823 / 32000000000000) ≤ -(20580854203499261973059 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_80 : Uρ (1412931037823 / 32000000000000) ≤ -(13340752815781598529229 / 5000000000000000000000)

theorem Zeta5Irrational.U_81_1 : Uω (aρ 1) (bρ 1) (71843627457 / 1600000000000) ≤ -(3259425568664305827969 / 1000000000000000000000)

theorem Zeta5Irrational.U_81_2 : Uω (aρ 2) (bρ 2) (71843627457 / 1600000000000) ≤ -(6660781429157999445921 / 2000000000000000000000)

theorem Zeta5Irrational.U_81_3 : Uω (aρ 3) (bρ 3) (71843627457 / 1600000000000) ≤ -(35029836476419809769441 / 10000000000000000000000)

theorem Zeta5Irrational.U_81_4 : Uω (aρ 4) (bρ 4) (71843627457 / 1600000000000) ≤ -(8091999804594550308781 / 2000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_81 : Uρ (71843627457 / 1600000000000) ≤ -(5324205551757644520397 / 2000000000000000000000)

theorem Zeta5Irrational.U_82_1 : Uω (aρ 1) (bρ 1) (2897686609597 / 64000000000000) ≤ -(32497230363190579783231 / 10000000000000000000000)

theorem Zeta5Irrational.U_82_2 : Uω (aρ 2) (bρ 2) (2897686609597 / 64000000000000) ≤ -(6639808015630789086519 / 2000000000000000000000)

theorem Zeta5Irrational.U_82_3 : Uω (aρ 3) (bρ 3) (2897686609597 / 64000000000000) ≤ -(87253003056903595321 / 25000000000000000000)

theorem Zeta5Irrational.U_82_4 : Uω (aρ 4) (bρ 4) (2897686609597 / 64000000000000) ≤ -(20072167163996576495227 / 5000000000000000000000)

theorem Zeta5Irrational.U_82_5 : Uω (aρ 5) (bρ 5) (2897686609597 / 64000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_82 : Uρ (2897686609597 / 64000000000000) ≤ -(6648255242717957936621 / 2500000000000000000000)

theorem Zeta5Irrational.U_83_1 : Uω (aρ 1) (bρ 1) (1460814060457 / 32000000000000) ≤ -(8100284844802228771499 / 2500000000000000000000)

theorem Zeta5Irrational.U_83_2 : Uω (aρ 2) (bρ 2) (1460814060457 / 32000000000000) ≤ -(4136909867612453369687 / 1250000000000000000000)

theorem Zeta5Irrational.U_83_3 : Uω (aρ 3) (bρ 3) (1460814060457 / 32000000000000) ≤ -(34774333175818615317637 / 10000000000000000000000)

theorem Zeta5Irrational.U_83_4 : Uω (aρ 4) (bρ 4) (1460814060457 / 32000000000000) ≤ -(19923513604471120193173 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_83 : Uρ (1460814060457 / 32000000000000) ≤ -(26566200964288256233641 / 10000000000000000000000)

theorem Zeta5Irrational.U_84_1 : Uω (aρ 1) (bρ 1) (2945569632231 / 64000000000000) ≤ -(16152982436976417664993 / 5000000000000000000000)

theorem Zeta5Irrational.U_84_2 : Uω (aρ 2) (bρ 2) (2945569632231 / 64000000000000) ≤ -(16496300146835009040687 / 5000000000000000000000)

theorem Zeta5Irrational.U_84_3 : Uω (aρ 3) (bρ 3) (2945569632231 / 64000000000000) ≤ -(34649181056232259045777 / 10000000000000000000000)

theorem Zeta5Irrational.U_84_4 : Uω (aρ 4) (bρ 4) (2945569632231 / 64000000000000) ≤ -(494567863174717687381 / 125000000000000000000)

theorem Zeta5Irrational.U_84_5 : Uω (aρ 5) (bρ 5) (2945569632231 / 64000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_84 : Uρ (2945569632231 / 64000000000000) ≤ -(26540410498328256391827 / 10000000000000000000000)

theorem Zeta5Irrational.U_85_1 : Uω (aρ 1) (bρ 1) (742377785887 / 16000000000000) ≤ -(16105844747499819637607 / 5000000000000000000000)

theorem Zeta5Irrational.U_85_2 : Uω (aρ 2) (bρ 2) (742377785887 / 16000000000000) ≤ -(8222745361049200402393 / 2500000000000000000000)

theorem Zeta5Irrational.U_85_3 : Uω (aρ 3) (bρ 3) (742377785887 / 16000000000000) ≤ -(17262847949594570677381 / 5000000000000000000000)

theorem Zeta5Irrational.U_85_4 : Uω (aρ 4) (bρ 4) (742377785887 / 16000000000000) ≤ -(7859495672749720896173 / 2000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_85 : Uρ (742377785887 / 16000000000000) ≤ -(6628881657870160769053 / 2500000000000000000000)

theorem Zeta5Irrational.U_86_1 : Uω (aρ 1) (bρ 1) (598690530973 / 12800000000000) ≤ -(16059148189551546355899 / 5000000000000000000000)

theorem Zeta5Irrational.U_86_2 : Uω (aρ 2) (bρ 2) (598690530973 / 12800000000000) ≤ -(1024700013012026515809 / 312500000000000000000)

theorem Zeta5Irrational.U_86_3 : Uω (aρ 3) (bρ 3) (598690530973 / 12800000000000) ≤ -(6880766185247015737031 / 2000000000000000000000)

theorem Zeta5Irrational.U_86_4 : Uω (aρ 4) (bρ 4) (598690530973 / 12800000000000) ≤ -(39041532706513693929033 / 10000000000000000000000)

theorem Zeta5Irrational.U_86_5 : Uω (aρ 5) (bρ 5) (598690530973 / 12800000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_86_6 : Uω (aρ 6) (bρ 6) (598690530973 / 12800000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_86_7 : Uω (aρ 7) (bρ 7) (598690530973 / 12800000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_86_8 : Uω (aρ 8) (bρ 8) (598690530973 / 12800000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_86_9 : Uω (aρ 9) (bρ 9) (598690530973 / 12800000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_86_10 : Uω (aρ 10) (bρ 10) (598690530973 / 12800000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_86_11 : Uω (aρ 11) (bρ 11) (598690530973 / 12800000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_86_12 : Uω (aρ 12) (bρ 12) (598690530973 / 12800000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_86_13 : Uω (aρ 13) (bρ 13) (598690530973 / 12800000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_86_14 : Uω (aρ 14) (bρ 14) (598690530973 / 12800000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_86_15 : Uω (aρ 15) (bρ 15) (598690530973 / 12800000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_86_16 : Uω (aρ 16) (bρ 16) (598690530973 / 12800000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_86 : Uρ (598690530973 / 12800000000000) ≤ -(26491450933863278184387 / 10000000000000000000000)

theorem Zeta5Irrational.U_87_1 : Uω (aρ 1) (bρ 1) (1508697083091 / 32000000000000) ≤ -(6405153826788440415589 / 2000000000000000000000)

theorem Zeta5Irrational.U_87_2 : Uω (aρ 2) (bρ 2) (1508697083091 / 32000000000000) ≤ -(6538167184020175693239 / 2000000000000000000000)

theorem Zeta5Irrational.U_87_3 : Uω (aρ 3) (bρ 3) (1508697083091 / 32000000000000) ≤ -(34283541402370319659499 / 10000000000000000000000)

theorem Zeta5Irrational.U_87_4 : Uω (aρ 4) (bρ 4) (1508697083091 / 32000000000000) ≤ -(1551850317616410832219 / 400000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_87 : Uρ (1508697083091 / 32000000000000) ≤ -(3308512879034082580067 / 1250000000000000000000)