Certified arcsine potential bounds (U36)

theorem Zeta5Irrational.U_436_1 : Uω (aρ 1) (bρ 1) (368482761309 / 800000000000) ≤ -(7893273641033907831537 / 10000000000000000000000)

theorem Zeta5Irrational.U_436_2 : Uω (aρ 2) (bρ 2) (368482761309 / 800000000000) ≤ -(3973094734289888371921 / 5000000000000000000000)

theorem Zeta5Irrational.U_436_3 : Uω (aρ 3) (bρ 3) (368482761309 / 800000000000) ≤ -(8052985750959086163193 / 10000000000000000000000)

theorem Zeta5Irrational.U_436_4 : Uω (aρ 4) (bρ 4) (368482761309 / 800000000000) ≤ -(8233284538001393696237 / 10000000000000000000000)

theorem Zeta5Irrational.U_436_5 : Uω (aρ 5) (bρ 5) (368482761309 / 800000000000) ≤ -(2128805313859165745199 / 2500000000000000000000)

theorem Zeta5Irrational.U_436_6 : Uω (aρ 6) (bρ 6) (368482761309 / 800000000000) ≤ -(4468182636717128945429 / 5000000000000000000000)

theorem Zeta5Irrational.U_436_7 : Uω (aρ 7) (bρ 7) (368482761309 / 800000000000) ≤ -(9546942225749288231573 / 10000000000000000000000)

theorem Zeta5Irrational.U_436_8 : Uω (aρ 8) (bρ 8) (368482761309 / 800000000000) ≤ -(2083737771356987306073 / 2000000000000000000000)

theorem Zeta5Irrational.U_436_9 : Uω (aρ 9) (bρ 9) (368482761309 / 800000000000) ≤ -(18234327382226959179 / 15625000000000000000)

theorem Zeta5Irrational.U_436_10 : Uω (aρ 10) (bρ 10) (368482761309 / 800000000000) ≤ -(6777683322747721136581 / 5000000000000000000000)

theorem Zeta5Irrational.U_436_11 : Uω (aρ 11) (bρ 11) (368482761309 / 800000000000) ≤ -(8542401856030899137819 / 5000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_436 : Uρ (368482761309 / 800000000000) ≤ -(11687040051905877864877 / 10000000000000000000000)

theorem Zeta5Irrational.U_437_1 : Uω (aρ 1) (bρ 1) (922531203149 / 2000000000000) ≤ -(7878704167782229152803 / 10000000000000000000000)

theorem Zeta5Irrational.U_437_2 : Uω (aρ 2) (bρ 2) (922531203149 / 2000000000000) ≤ -(317261684270894545459 / 400000000000000000000)

theorem Zeta5Irrational.U_437_3 : Uω (aρ 3) (bρ 3) (922531203149 / 2000000000000) ≤ -(4019089635595831755489 / 5000000000000000000000)

theorem Zeta5Irrational.U_437_4 : Uω (aρ 4) (bρ 4) (922531203149 / 2000000000000) ≤ -(256818857844002620983 / 312500000000000000000)

theorem Zeta5Irrational.U_437_5 : Uω (aρ 5) (bρ 5) (922531203149 / 2000000000000) ≤ -(8499695063155904997523 / 10000000000000000000000)

theorem Zeta5Irrational.U_437_6 : Uω (aρ 6) (bρ 6) (922531203149 / 2000000000000) ≤ -(4460068031353997442141 / 5000000000000000000000)

theorem Zeta5Irrational.U_437_7 : Uω (aρ 7) (bρ 7) (922531203149 / 2000000000000) ≤ -(4764801910451678914299 / 5000000000000000000000)

theorem Zeta5Irrational.U_437_8 : Uω (aρ 8) (bρ 8) (922531203149 / 2000000000000) ≤ -(129994387526496953403 / 125000000000000000000)

theorem Zeta5Irrational.U_437_9 : Uω (aρ 9) (bρ 9) (922531203149 / 2000000000000) ≤ -(5823841816935791055419 / 5000000000000000000000)

theorem Zeta5Irrational.U_437_10 : Uω (aρ 10) (bρ 10) (922531203149 / 2000000000000) ≤ -(6763228486011371335239 / 5000000000000000000000)

theorem Zeta5Irrational.U_437_11 : Uω (aρ 11) (bρ 11) (922531203149 / 2000000000000) ≤ -(17028606823962924506891 / 10000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_437 : Uρ (922531203149 / 2000000000000) ≤ -(1167055396637717132097 / 1000000000000000000000)

theorem Zeta5Irrational.U_438_1 : Uω (aρ 1) (bρ 1) (1847711006051 / 4000000000000) ≤ -(7864155890938650200869 / 10000000000000000000000)

theorem Zeta5Irrational.U_438_2 : Uω (aρ 2) (bρ 2) (1847711006051 / 4000000000000) ≤ -(3958458085164027500651 / 5000000000000000000000)

theorem Zeta5Irrational.U_438_3 : Uω (aρ 3) (bρ 3) (1847711006051 / 4000000000000) ≤ -(250731084071014719003 / 312500000000000000000)

theorem Zeta5Irrational.U_438_4 : Uω (aρ 4) (bρ 4) (1847711006051 / 4000000000000) ≤ -(8203145098388216551507 / 10000000000000000000000)

theorem Zeta5Irrational.U_438_5 : Uω (aρ 5) (bρ 5) (1847711006051 / 4000000000000) ≤ -(265131031560338101691 / 312500000000000000000)

theorem Zeta5Irrational.U_438_6 : Uω (aρ 6) (bρ 6) (1847711006051 / 4000000000000) ≤ -(890393334056470965597 / 1000000000000000000000)

theorem Zeta5Irrational.U_438_7 : Uω (aρ 7) (bρ 7) (1847711006051 / 4000000000000) ≤ -(4756147976599214266163 / 5000000000000000000000)

theorem Zeta5Irrational.U_438_8 : Uω (aρ 8) (bρ 8) (1847711006051 / 4000000000000) ≤ -(1297556400836899823467 / 1250000000000000000000)

theorem Zeta5Irrational.U_438_9 : Uω (aρ 9) (bρ 9) (1847711006051 / 4000000000000) ≤ -(11625452123025537848547 / 10000000000000000000000)

theorem Zeta5Irrational.U_438_10 : Uω (aρ 10) (bρ 10) (1847711006051 / 4000000000000) ≤ -(13497651695297014300729 / 10000000000000000000000)

theorem Zeta5Irrational.U_438_11 : Uω (aρ 11) (bρ 11) (1847711006051 / 4000000000000) ≤ -(1060816088683519187111 / 625000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_438 : Uρ (1847711006051 / 4000000000000) ≤ -(582707276038643686991 / 500000000000000000000)

theorem Zeta5Irrational.U_439_1 : Uω (aρ 1) (bρ 1) (462589901451 / 1000000000000) ≤ -(7665653075113846959 / 9765625000000000000)

theorem Zeta5Irrational.U_439_2 : Uω (aρ 2) (bρ 2) (462589901451 / 1000000000000) ≤ -(7902311596652221809187 / 10000000000000000000000)

theorem Zeta5Irrational.U_439_3 : Uω (aρ 3) (bρ 3) (462589901451 / 1000000000000) ≤ -(1601726388699282176059 / 2000000000000000000000)

theorem Zeta5Irrational.U_439_4 : Uω (aρ 4) (bρ 4) (462589901451 / 1000000000000) ≤ -(8188109411627823297001 / 10000000000000000000000)

theorem Zeta5Irrational.U_439_5 : Uω (aρ 5) (bρ 5) (462589901451 / 1000000000000) ≤ -(8468715020601605035629 / 10000000000000000000000)

theorem Zeta5Irrational.U_439_6 : Uω (aρ 6) (bρ 6) (462589901451 / 1000000000000) ≤ -(2221939255013808664823 / 2500000000000000000000)

theorem Zeta5Irrational.U_439_7 : Uω (aρ 7) (bρ 7) (462589901451 / 1000000000000) ≤ -(1186877314178239240791 / 1250000000000000000000)

theorem Zeta5Irrational.U_439_8 : Uω (aρ 8) (bρ 8) (462589901451 / 1000000000000) ≤ -(518069465680476440557 / 500000000000000000000)

theorem Zeta5Irrational.U_439_9 : Uω (aρ 9) (bρ 9) (462589901451 / 1000000000000) ≤ -(11603274705019627962981 / 10000000000000000000000)

theorem Zeta5Irrational.U_439_10 : Uω (aρ 10) (bρ 10) (462589901451 / 1000000000000) ≤ -(13468949928897215958101 / 10000000000000000000000)

theorem Zeta5Irrational.U_439_11 : Uω (aρ 11) (bρ 11) (462589901451 / 1000000000000) ≤ -(16918135276424289182913 / 10000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_439 : Uρ (462589901451 / 1000000000000) ≤ -(1454726621769049927881 / 1250000000000000000000)

theorem Zeta5Irrational.U_440_1 : Uω (aρ 1) (bρ 1) (1853008205557 / 4000000000000) ≤ -(979390335049681997199 / 1250000000000000000000)

theorem Zeta5Irrational.U_440_2 : Uω (aρ 2) (bρ 2) (1853008205557 / 4000000000000) ≤ -(3943864161712085556341 / 5000000000000000000000)

theorem Zeta5Irrational.U_440_3 : Uω (aρ 3) (bρ 3) (1853008205557 / 4000000000000) ≤ -(7993890966444840479467 / 10000000000000000000000)

theorem Zeta5Irrational.U_440_4 : Uω (aρ 4) (bρ 4) (1853008205557 / 4000000000000) ≤ -(4086548161261261473791 / 5000000000000000000000)

theorem Zeta5Irrational.U_440_5 : Uω (aρ 5) (bρ 5) (1853008205557 / 4000000000000) ≤ -(169065220407198884057 / 200000000000000000000)

theorem Zeta5Irrational.U_440_6 : Uω (aρ 6) (bρ 6) (1853008205557 / 4000000000000) ≤ -(8871607014660831809501 / 10000000000000000000000)

theorem Zeta5Irrational.U_440_7 : Uω (aρ 7) (bρ 7) (1853008205557 / 4000000000000) ≤ -(9477771392971459838581 / 10000000000000000000000)

theorem Zeta5Irrational.U_440_8 : Uω (aρ 8) (bρ 8) (1853008205557 / 4000000000000) ≤ -(5171182583481206675893 / 5000000000000000000000)

theorem Zeta5Irrational.U_440_9 : Uω (aρ 9) (bρ 9) (1853008205557 / 4000000000000) ≤ -(11581151095201511045311 / 10000000000000000000000)

theorem Zeta5Irrational.U_440_10 : Uω (aρ 10) (bρ 10) (1853008205557 / 4000000000000) ≤ -(1344035079882253336513 / 1000000000000000000000)

theorem Zeta5Irrational.U_440_11 : Uω (aρ 11) (bρ 11) (1853008205557 / 4000000000000) ≤ -(16863821217932963072499 / 10000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_440 : Uρ (1853008205557 / 4000000000000) ≤ -(11621554669306362988887 / 10000000000000000000000)

theorem Zeta5Irrational.U_441_1 : Uω (aρ 1) (bρ 1) (185565680531 / 400000000000) ≤ -(7820637624329189336659 / 10000000000000000000000)

theorem Zeta5Irrational.U_441_2 : Uω (aρ 2) (bρ 2) (185565680531 / 400000000000) ≤ -(7873166288595550170051 / 10000000000000000000000)

theorem Zeta5Irrational.U_441_3 : Uω (aρ 3) (bρ 3) (185565680531 / 400000000000) ≤ -(3989585847491946285049 / 5000000000000000000000)

theorem Zeta5Irrational.U_441_4 : Uω (aρ 4) (bρ 4) (185565680531 / 400000000000) ≤ -(1631621152635130144881 / 2000000000000000000000)

theorem Zeta5Irrational.U_441_5 : Uω (aρ 5) (bρ 5) (185565680531 / 400000000000) ≤ -(8437830934746810842847 / 10000000000000000000000)

theorem Zeta5Irrational.U_441_6 : Uω (aρ 6) (bρ 6) (185565680531 / 400000000000) ≤ -(2213870809572582147229 / 2500000000000000000000)

theorem Zeta5Irrational.U_441_7 : Uω (aρ 7) (bρ 7) (185565680531 / 400000000000) ≤ -(1182569310476322240769 / 1250000000000000000000)

theorem Zeta5Irrational.U_441_8 : Uω (aρ 8) (bρ 8) (185565680531 / 400000000000) ≤ -(1032337861184616429291 / 1000000000000000000000)

theorem Zeta5Irrational.U_441_9 : Uω (aρ 9) (bρ 9) (185565680531 / 400000000000) ≤ -(11559081011305702915049 / 10000000000000000000000)

theorem Zeta5Irrational.U_441_10 : Uω (aρ 10) (bρ 10) (185565680531 / 400000000000) ≤ -(6705926721624019064597 / 5000000000000000000000)

theorem Zeta5Irrational.U_441_11 : Uω (aρ 11) (bρ 11) (185565680531 / 400000000000) ≤ -(4202524258281721346399 / 2500000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_441 : Uρ (185565680531 / 400000000000) ≤ -(2901342256725090960881 / 2500000000000000000000)

theorem Zeta5Irrational.U_442_1 : Uω (aρ 1) (bρ 1) (1858305405063 / 4000000000000) ≤ -(7806173519924622736079 / 10000000000000000000000)

theorem Zeta5Irrational.U_442_2 : Uω (aρ 2) (bρ 2) (1858305405063 / 4000000000000) ≤ -(3929312715194378892603 / 5000000000000000000000)

theorem Zeta5Irrational.U_442_3 : Uω (aρ 3) (bρ 3) (1858305405063 / 4000000000000) ≤ -(7964474065262793540323 / 10000000000000000000000)

theorem Zeta5Irrational.U_442_4 : Uω (aρ 4) (bρ 4) (1858305405063 / 4000000000000) ≤ -(8143137665996417731169 / 10000000000000000000000)

theorem Zeta5Irrational.U_442_5 : Uω (aρ 5) (bρ 5) (1858305405063 / 4000000000000) ≤ -(8422424689650293239287 / 10000000000000000000000)

theorem Zeta5Irrational.U_442_6 : Uω (aρ 6) (bρ 6) (1858305405063 / 4000000000000) ≤ -(8839385605277294481179 / 10000000000000000000000)

theorem Zeta5Irrational.U_442_7 : Uω (aρ 7) (bρ 7) (1858305405063 / 4000000000000) ≤ -(9443367678504315809701 / 10000000000000000000000)

theorem Zeta5Irrational.U_442_8 : Uω (aρ 8) (bρ 8) (1858305405063 / 4000000000000) ≤ -(10304429494337094953457 / 10000000000000000000000)

theorem Zeta5Irrational.U_442_9 : Uω (aρ 9) (bρ 9) (1858305405063 / 4000000000000) ≤ -(180266627709776947529 / 156250000000000000000)

theorem Zeta5Irrational.U_442_10 : Uω (aρ 10) (bρ 10) (1858305405063 / 4000000000000) ≤ -(6691728506143263926889 / 5000000000000000000000)

theorem Zeta5Irrational.U_442_11 : Uω (aρ 11) (bρ 11) (1858305405063 / 4000000000000) ≤ -(3351389082507226933971 / 2000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_442 : Uρ (1858305405063 / 4000000000000) ≤ -(5794627270070532732099 / 5000000000000000000000)

theorem Zeta5Irrational.U_443_1 : Uω (aρ 1) (bρ 1) (116309625301 / 250000000000) ≤ -(7791730306659998859531 / 10000000000000000000000)

theorem Zeta5Irrational.U_443_2 : Uω (aρ 2) (bρ 2) (116309625301 / 250000000000) ≤ -(7844105687295377049281 / 10000000000000000000000)

theorem Zeta5Irrational.U_443_3 : Uω (aρ 3) (bρ 3) (116309625301 / 250000000000) ≤ -(3974899006856099753251 / 5000000000000000000000)

theorem Zeta5Irrational.U_443_4 : Uω (aρ 4) (bρ 4) (116309625301 / 250000000000) ≤ -(254005998865564480957 / 312500000000000000000)

theorem Zeta5Irrational.U_443_5 : Uω (aρ 5) (bρ 5) (116309625301 / 250000000000) ≤ -(840704221130343153201 / 1000000000000000000000)

theorem Zeta5Irrational.U_443_6 : Uω (aρ 6) (bρ 6) (116309625301 / 250000000000) ≤ -(4411657015188613554371 / 5000000000000000000000)

theorem Zeta5Irrational.U_443_7 : Uω (aρ 7) (bρ 7) (116309625301 / 250000000000) ≤ -(2356552717548743531489 / 2500000000000000000000)

theorem Zeta5Irrational.U_443_8 : Uω (aρ 8) (bρ 8) (116309625301 / 250000000000) ≤ -(2057103532297391134677 / 2000000000000000000000)

theorem Zeta5Irrational.U_443_9 : Uω (aρ 9) (bρ 9) (116309625301 / 250000000000) ≤ -(2303020060797331947437 / 2000000000000000000000)

theorem Zeta5Irrational.U_443_10 : Uω (aρ 10) (bρ 10) (116309625301 / 250000000000) ≤ -(1669395083469542458551 / 1250000000000000000000)

theorem Zeta5Irrational.U_443_11 : Uω (aρ 11) (bρ 11) (116309625301 / 250000000000) ≤ -(4176087471541592210279 / 2500000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_443 : Uρ (116309625301 / 250000000000) ≤ -(5786604884954288602901 / 5000000000000000000000)

theorem Zeta5Irrational.U_444_1 : Uω (aρ 1) (bρ 1) (1863602604569 / 4000000000000) ≤ -(1944326981068361120593 / 2500000000000000000000)

theorem Zeta5Irrational.U_444_2 : Uω (aρ 2) (bρ 2) (1863602604569 / 4000000000000) ≤ -(1565921399614921480789 / 2000000000000000000000)

theorem Zeta5Irrational.U_444_3 : Uω (aρ 3) (bρ 3) (1863602604569 / 4000000000000) ≤ -(7935143477042547934617 / 10000000000000000000000)

theorem Zeta5Irrational.U_444_4 : Uω (aρ 4) (bρ 4) (1863602604569 / 4000000000000) ≤ -(507079286831002569619 / 625000000000000000000)

theorem Zeta5Irrational.U_444_5 : Uω (aρ 5) (bρ 5) (1863602604569 / 4000000000000) ≤ -(4195841713141036618307 / 5000000000000000000000)

theorem Zeta5Irrational.U_444_6 : Uω (aρ 6) (bρ 6) (1863602604569 / 4000000000000) ≤ -(880726842876476855731 / 1000000000000000000000)

theorem Zeta5Irrational.U_444_7 : Uω (aρ 7) (bρ 7) (1863602604569 / 4000000000000) ≤ -(9409083952601855202521 / 10000000000000000000000)

theorem Zeta5Irrational.U_444_8 : Uω (aρ 8) (bρ 8) (1863602604569 / 4000000000000) ≤ -(10266642961314476776443 / 10000000000000000000000)

theorem Zeta5Irrational.U_444_9 : Uω (aρ 9) (bρ 9) (1863602604569 / 4000000000000) ≤ -(5746594563859062553709 / 5000000000000000000000)

theorem Zeta5Irrational.U_444_10 : Uω (aρ 10) (bρ 10) (1863602604569 / 4000000000000) ≤ -(6663481791477497625633 / 5000000000000000000000)

theorem Zeta5Irrational.U_444_11 : Uω (aρ 11) (bρ 11) (1863602604569 / 4000000000000) ≤ -(4163073691847707252589 / 2500000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_444 : Uρ (1863602604569 / 4000000000000) ≤ -(5778616670153065444033 / 5000000000000000000000)

theorem Zeta5Irrational.U_445_1 : Uω (aρ 1) (bρ 1) (933125602161 / 2000000000000) ≤ -(7762906312763454203637 / 10000000000000000000000)

theorem Zeta5Irrational.U_445_2 : Uω (aρ 2) (bρ 2) (933125602161 / 2000000000000) ≤ -(1953782325437929747473 / 2500000000000000000000)

theorem Zeta5Irrational.U_445_3 : Uω (aρ 3) (bρ 3) (933125602161 / 2000000000000) ≤ -(1980127598060602571469 / 2500000000000000000000)

theorem Zeta5Irrational.U_445_4 : Uω (aρ 4) (bρ 4) (933125602161 / 2000000000000) ≤ -(202459186902655127247 / 250000000000000000000)

theorem Zeta5Irrational.U_445_5 : Uω (aρ 5) (bρ 5) (933125602161 / 2000000000000) ≤ -(1675269652300550677949 / 2000000000000000000000)

theorem Zeta5Irrational.U_445_6 : Uω (aρ 6) (bρ 6) (933125602161 / 2000000000000) ≤ -(8791248716030945256763 / 10000000000000000000000)

theorem Zeta5Irrational.U_445_7 : Uω (aρ 7) (bρ 7) (933125602161 / 2000000000000) ≤ -(4695993410008529072567 / 5000000000000000000000)

theorem Zeta5Irrational.U_445_8 : Uω (aρ 8) (bρ 8) (933125602161 / 2000000000000) ≤ -(10247805242797003460311 / 10000000000000000000000)

theorem Zeta5Irrational.U_445_9 : Uω (aρ 9) (bρ 9) (933125602161 / 2000000000000) ≤ -(458853214865105613027 / 400000000000000000000)

theorem Zeta5Irrational.U_445_10 : Uω (aρ 10) (bρ 10) (933125602161 / 2000000000000) ≤ -(13298864942438442631833 / 10000000000000000000000)

theorem Zeta5Irrational.U_445_11 : Uω (aρ 11) (bρ 11) (933125602161 / 2000000000000) ≤ -(3320153020315792050137 / 2000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_445 : Uρ (933125602161 / 2000000000000) ≤ -(5770661967292001257713 / 5000000000000000000000)

theorem Zeta5Irrational.U_446_1 : Uω (aρ 1) (bρ 1) (467887100957 / 1000000000000) ≤ -(966770645457505427377 / 1250000000000000000000)

theorem Zeta5Irrational.U_446_2 : Uω (aρ 2) (bρ 2) (467887100957 / 1000000000000) ≤ -(973279580652723789647 / 1250000000000000000000)

theorem Zeta5Irrational.U_446_3 : Uω (aρ 3) (bρ 3) (467887100957 / 1000000000000) ≤ -(7891308327585915285363 / 10000000000000000000000)

theorem Zeta5Irrational.U_446_4 : Uω (aρ 4) (bρ 4) (467887100957 / 1000000000000) ≤ -(4034315884058882351419 / 5000000000000000000000)

theorem Zeta5Irrational.U_446_5 : Uω (aρ 5) (bρ 5) (467887100957 / 1000000000000) ≤ -(521609281376695497853 / 625000000000000000000)

theorem Zeta5Irrational.U_446_6 : Uω (aρ 6) (bρ 6) (467887100957 / 1000000000000) ≤ -(4379643310814408410447 / 5000000000000000000000)

theorem Zeta5Irrational.U_446_7 : Uω (aρ 7) (bρ 7) (467887100957 / 1000000000000) ≤ -(9357881489879827674907 / 10000000000000000000000)

theorem Zeta5Irrational.U_446_8 : Uω (aρ 8) (bρ 8) (467887100957 / 1000000000000) ≤ -(2042048030275987590759 / 2000000000000000000000)

theorem Zeta5Irrational.U_446_9 : Uω (aρ 9) (bρ 9) (467887100957 / 1000000000000) ≤ -(5713884519621729279943 / 5000000000000000000000)

theorem Zeta5Irrational.U_446_10 : Uω (aρ 10) (bρ 10) (467887100957 / 1000000000000) ≤ -(13242959787489276770681 / 10000000000000000000000)

theorem Zeta5Irrational.U_446_11 : Uω (aρ 11) (bρ 11) (467887100957 / 1000000000000) ≤ -(16499225691449952125427 / 10000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_446 : Uρ (467887100957 / 1000000000000) ≤ -(11509701201381695884397 / 10000000000000000000000)

theorem Zeta5Irrational.U_447_1 : Uω (aρ 1) (bρ 1) (938422801667 / 2000000000000) ≤ -(7705506384488545139841 / 10000000000000000000000)

theorem Zeta5Irrational.U_447_2 : Uω (aρ 2) (bρ 2) (938422801667 / 2000000000000) ≤ -(969678404396364492027 / 1250000000000000000000)

theorem Zeta5Irrational.U_447_3 : Uω (aρ 3) (bρ 3) (938422801667 / 2000000000000) ≤ -(3931095660576254656589 / 5000000000000000000000)

theorem Zeta5Irrational.U_447_4 : Uω (aρ 4) (bρ 4) (938422801667 / 2000000000000) ≤ -(1004873039024965725031 / 1250000000000000000000)

theorem Zeta5Irrational.U_447_5 : Uω (aρ 5) (bρ 5) (938422801667 / 2000000000000) ≤ -(2078810588735672971517 / 2500000000000000000000)

theorem Zeta5Irrational.U_447_6 : Uω (aρ 6) (bρ 6) (938422801667 / 2000000000000) ≤ -(8727427080123200181059 / 10000000000000000000000)

theorem Zeta5Irrational.U_447_7 : Uω (aρ 7) (bρ 7) (938422801667 / 2000000000000) ≤ -(4661947022709255165381 / 5000000000000000000000)

theorem Zeta5Irrational.U_447_8 : Uω (aρ 8) (bρ 8) (938422801667 / 2000000000000) ≤ -(2543205299478635574293 / 2500000000000000000000)

theorem Zeta5Irrational.U_447_9 : Uω (aρ 9) (bρ 9) (938422801667 / 2000000000000) ≤ -(11384414167465334094829 / 10000000000000000000000)

theorem Zeta5Irrational.U_447_10 : Uω (aρ 10) (bρ 10) (938422801667 / 2000000000000) ≤ -(2637487779295076324629 / 2000000000000000000000)

theorem Zeta5Irrational.U_447_11 : Uω (aρ 11) (bρ 11) (938422801667 / 2000000000000) ≤ -(16399624961174716983881 / 10000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_447 : Uρ (938422801667 / 2000000000000) ≤ -(2295666416895180790197 / 2000000000000000000000)