Certified arcsine potential bounds (U35)

theorem Zeta5Irrational.U_424_1 : Uω (aρ 1) (bρ 1) (1810630609509 / 4000000000000) ≤ -(8069783430186067276137 / 10000000000000000000000)

theorem Zeta5Irrational.U_424_2 : Uω (aρ 2) (bρ 2) (1810630609509 / 4000000000000) ≤ -(1624730430815369043297 / 2000000000000000000000)

theorem Zeta5Irrational.U_424_3 : Uω (aρ 3) (bρ 3) (1810630609509 / 4000000000000) ≤ -(4116197784770404230469 / 5000000000000000000000)

theorem Zeta5Irrational.U_424_4 : Uω (aρ 4) (bρ 4) (1810630609509 / 4000000000000) ≤ -(8416056233038239239309 / 10000000000000000000000)

theorem Zeta5Irrational.U_424_5 : Uω (aρ 5) (bρ 5) (1810630609509 / 4000000000000) ≤ -(8703446256895322532487 / 10000000000000000000000)

theorem Zeta5Irrational.U_424_6 : Uω (aρ 6) (bρ 6) (1810630609509 / 4000000000000) ≤ -(2283303540356153156021 / 2500000000000000000000)

theorem Zeta5Irrational.U_424_7 : Uω (aρ 7) (bρ 7) (1810630609509 / 4000000000000) ≤ -(2439356390886610766343 / 2500000000000000000000)

theorem Zeta5Irrational.U_424_8 : Uω (aρ 8) (bρ 8) (1810630609509 / 4000000000000) ≤ -(10651370252152340611 / 10000000000000000000)

theorem Zeta5Irrational.U_424_9 : Uω (aρ 9) (bρ 9) (1810630609509 / 4000000000000) ≤ -(1194174976479651820651 / 1000000000000000000000)

theorem Zeta5Irrational.U_424_10 : Uω (aρ 10) (bρ 10) (1810630609509 / 4000000000000) ≤ -(13910766432101367482929 / 10000000000000000000000)

theorem Zeta5Irrational.U_424_11 : Uω (aρ 11) (bρ 11) (1810630609509 / 4000000000000) ≤ -(8909444894819806137933 / 5000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_424 : Uρ (1810630609509 / 4000000000000) ≤ -(11891711587405053258781 / 10000000000000000000000)

theorem Zeta5Irrational.U_425_1 : Uω (aρ 1) (bρ 1) (906639604631 / 2000000000000) ≤ -(4027477348275718747337 / 5000000000000000000000)

theorem Zeta5Irrational.U_425_2 : Uω (aρ 2) (bρ 2) (906639604631 / 2000000000000) ≤ -(4054371351793893970459 / 5000000000000000000000)

theorem Zeta5Irrational.U_425_3 : Uω (aρ 3) (bρ 3) (906639604631 / 2000000000000) ≤ -(8217321149963825466591 / 10000000000000000000000)

theorem Zeta5Irrational.U_425_4 : Uω (aρ 4) (bρ 4) (906639604631 / 2000000000000) ≤ -(4200348437088783331463 / 5000000000000000000000)

theorem Zeta5Irrational.U_425_5 : Uω (aρ 5) (bρ 5) (906639604631 / 2000000000000) ≤ -(8687624402469212596989 / 10000000000000000000000)

theorem Zeta5Irrational.U_425_6 : Uω (aρ 6) (bρ 6) (906639604631 / 2000000000000) ≤ -(1139582518123484126347 / 1250000000000000000000)

theorem Zeta5Irrational.U_425_7 : Uω (aρ 7) (bρ 7) (906639604631 / 2000000000000) ≤ -(1947942394458633086619 / 2000000000000000000000)

theorem Zeta5Irrational.U_425_8 : Uω (aρ 8) (bρ 8) (906639604631 / 2000000000000) ≤ -(10631763071366856419741 / 10000000000000000000000)

theorem Zeta5Irrational.U_425_9 : Uω (aρ 9) (bρ 9) (906639604631 / 2000000000000) ≤ -(11918788004198888387561 / 10000000000000000000000)

theorem Zeta5Irrational.U_425_10 : Uω (aρ 10) (bρ 10) (906639604631 / 2000000000000) ≤ -(3470132493185344546727 / 2500000000000000000000)

theorem Zeta5Irrational.U_425_11 : Uω (aρ 11) (bρ 11) (906639604631 / 2000000000000) ≤ -(221910297290179888531 / 125000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_425 : Uρ (906639604631 / 2000000000000) ≤ -(11874116246818642659339 / 10000000000000000000000)

theorem Zeta5Irrational.U_426_1 : Uω (aρ 1) (bρ 1) (363185561803 / 800000000000) ≤ -(1608029583970223099703 / 2000000000000000000000)

theorem Zeta5Irrational.U_426_2 : Uω (aρ 2) (bρ 2) (363185561803 / 800000000000) ≤ -(252932982861302534687 / 312500000000000000000)

theorem Zeta5Irrational.U_426_3 : Uω (aρ 3) (bρ 3) (363185561803 / 800000000000) ≤ -(4101134714336247887123 / 5000000000000000000000)

theorem Zeta5Irrational.U_426_4 : Uω (aρ 4) (bρ 4) (363185561803 / 800000000000) ≤ -(8385361096703903811737 / 10000000000000000000000)

theorem Zeta5Irrational.U_426_5 : Uω (aρ 5) (bρ 5) (363185561803 / 800000000000) ≤ -(541989226078443513091 / 625000000000000000000)

theorem Zeta5Irrational.U_426_6 : Uω (aρ 6) (bρ 6) (363185561803 / 800000000000) ≤ -(2275033423792574258343 / 2500000000000000000000)

theorem Zeta5Irrational.U_426_7 : Uω (aρ 7) (bρ 7) (363185561803 / 800000000000) ≤ -(1215253784585170195443 / 1250000000000000000000)

theorem Zeta5Irrational.U_426_8 : Uω (aρ 8) (bρ 8) (363185561803 / 800000000000) ≤ -(2122439182815299947461 / 2000000000000000000000)

theorem Zeta5Irrational.U_426_9 : Uω (aρ 9) (bρ 9) (363185561803 / 800000000000) ≤ -(2973971066903655038759 / 2500000000000000000000)

theorem Zeta5Irrational.U_426_10 : Uω (aρ 10) (bρ 10) (363185561803 / 800000000000) ≤ -(1731301202107627005709 / 1250000000000000000000)

theorem Zeta5Irrational.U_426_11 : Uω (aρ 11) (bρ 11) (363185561803 / 800000000000) ≤ -(17687769941311851423913 / 10000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_426 : Uρ (363185561803 / 800000000000) ≤ -(11856629194172474159109 / 10000000000000000000000)

theorem Zeta5Irrational.U_427_1 : Uω (aρ 1) (bρ 1) (28415256387 / 62500000000) ≤ -(2006340758789207906781 / 2500000000000000000000)

theorem Zeta5Irrational.U_427_2 : Uω (aρ 2) (bρ 2) (28415256387 / 62500000000) ≤ -(1615798066397558523171 / 2000000000000000000000)

theorem Zeta5Irrational.U_427_3 : Uω (aρ 3) (bρ 3) (28415256387 / 62500000000) ≤ -(818724033738776100043 / 1000000000000000000000)

theorem Zeta5Irrational.U_427_4 : Uω (aρ 4) (bρ 4) (28415256387 / 62500000000) ≤ -(1046256103529695111109 / 1250000000000000000000)

theorem Zeta5Irrational.U_427_5 : Uω (aρ 5) (bρ 5) (28415256387 / 62500000000) ≤ -(2164013955424430799831 / 2500000000000000000000)

theorem Zeta5Irrational.U_427_6 : Uω (aρ 6) (bρ 6) (28415256387 / 62500000000) ≤ -(9083634719625875003053 / 10000000000000000000000)

theorem Zeta5Irrational.U_427_7 : Uω (aρ 7) (bρ 7) (28415256387 / 62500000000) ≤ -(4852190180007776394843 / 5000000000000000000000)

theorem Zeta5Irrational.U_427_8 : Uω (aρ 8) (bρ 8) (28415256387 / 62500000000) ≤ -(10592668610642755392833 / 10000000000000000000000)

theorem Zeta5Irrational.U_427_9 : Uω (aρ 9) (bρ 9) (28415256387 / 62500000000) ≤ -(5936519118310741301741 / 5000000000000000000000)

theorem Zeta5Irrational.U_427_10 : Uω (aρ 10) (bρ 10) (28415256387 / 62500000000) ≤ -(3455101075548872166831 / 2500000000000000000000)

theorem Zeta5Irrational.U_427_11 : Uω (aρ 11) (bρ 11) (28415256387 / 62500000000) ≤ -(8811842877035075998573 / 5000000000000000000000)

theorem Zeta5Irrational.U_427_12 : Uω (aρ 12) (bρ 12) (28415256387 / 62500000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_427_13 : Uω (aρ 13) (bρ 13) (28415256387 / 62500000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_427_14 : Uω (aρ 14) (bρ 14) (28415256387 / 62500000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_427_15 : Uω (aρ 15) (bρ 15) (28415256387 / 62500000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_427_16 : Uω (aρ 16) (bρ 16) (28415256387 / 62500000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_427 : Uρ (28415256387 / 62500000000) ≤ -(11839246909114969195289 / 10000000000000000000000)

theorem Zeta5Irrational.U_428_1 : Uω (aρ 1) (bρ 1) (1821225008521 / 4000000000000) ≤ -(8010599977827891867547 / 10000000000000000000000)

theorem Zeta5Irrational.U_428_2 : Uω (aρ 2) (bρ 2) (1821225008521 / 4000000000000) ≤ -(1612829455829885220953 / 2000000000000000000000)

theorem Zeta5Irrational.U_428_3 : Uω (aρ 3) (bρ 3) (1821225008521 / 4000000000000) ≤ -(2043058452034576909719 / 2500000000000000000000)

theorem Zeta5Irrational.U_428_4 : Uω (aρ 4) (bρ 4) (1821225008521 / 4000000000000) ≤ -(4177379998365973504417 / 5000000000000000000000)

theorem Zeta5Irrational.U_428_5 : Uω (aρ 5) (bρ 5) (1821225008521 / 4000000000000) ≤ -(8640308936621060834287 / 10000000000000000000000)

theorem Zeta5Irrational.U_428_6 : Uω (aρ 6) (bρ 6) (1821225008521 / 4000000000000) ≤ -(9067163126475235429003 / 10000000000000000000000)

theorem Zeta5Irrational.U_428_7 : Uω (aρ 7) (bρ 7) (1821225008521 / 4000000000000) ≤ -(9686762106250244520731 / 10000000000000000000000)

theorem Zeta5Irrational.U_428_8 : Uω (aρ 8) (bρ 8) (1821225008521 / 4000000000000) ≤ -(10573180992541647374207 / 10000000000000000000000)

theorem Zeta5Irrational.U_428_9 : Uω (aρ 9) (bρ 9) (1821225008521 / 4000000000000) ≤ -(11850249595588193161761 / 10000000000000000000000)

theorem Zeta5Irrational.U_428_10 : Uω (aρ 10) (bρ 10) (1821225008521 / 4000000000000) ≤ -(6895256495096437908121 / 5000000000000000000000)

theorem Zeta5Irrational.U_428_11 : Uω (aρ 11) (bρ 11) (1821225008521 / 4000000000000) ≤ -(3512106326516641677623 / 2000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_428 : Uρ (1821225008521 / 4000000000000) ≤ -(2364393220857954377449 / 2000000000000000000000)

theorem Zeta5Irrational.U_429_1 : Uω (aρ 1) (bρ 1) (911936804137 / 2000000000000) ≤ -(7995858683509481005467 / 10000000000000000000000)

theorem Zeta5Irrational.U_429_2 : Uω (aρ 2) (bρ 2) (911936804137 / 2000000000000) ≤ -(251541444613192942879 / 312500000000000000000)

theorem Zeta5Irrational.U_429_3 : Uω (aρ 3) (bρ 3) (911936804137 / 2000000000000) ≤ -(4078624886629356679157 / 5000000000000000000000)

theorem Zeta5Irrational.U_429_4 : Uω (aρ 4) (bρ 4) (911936804137 / 2000000000000) ≤ -(8339494530471527057847 / 10000000000000000000000)

theorem Zeta5Irrational.U_429_5 : Uω (aρ 5) (bρ 5) (911936804137 / 2000000000000) ≤ -(8624586883225874612507 / 10000000000000000000000)

theorem Zeta5Irrational.U_429_6 : Uω (aρ 6) (bρ 6) (911936804137 / 2000000000000) ≤ -(4525359412151244814811 / 5000000000000000000000)

theorem Zeta5Irrational.U_429_7 : Uω (aρ 7) (bρ 7) (911936804137 / 2000000000000) ≤ -(1933835079997006956291 / 2000000000000000000000)

theorem Zeta5Irrational.U_429_8 : Uω (aρ 8) (bρ 8) (911936804137 / 2000000000000) ≤ -(5276866446176848011757 / 5000000000000000000000)

theorem Zeta5Irrational.U_429_9 : Uω (aρ 9) (bρ 9) (911936804137 / 2000000000000) ≤ -(5913759015820159389253 / 5000000000000000000000)

theorem Zeta5Irrational.U_429_10 : Uω (aρ 10) (bρ 10) (911936804137 / 2000000000000) ≤ -(1720091831909998787893 / 1250000000000000000000)

theorem Zeta5Irrational.U_429_11 : Uω (aρ 11) (bρ 11) (911936804137 / 2000000000000) ≤ -(17498270634776701115959 / 10000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_429 : Uρ (911936804137 / 2000000000000) ≤ -(11804783702785120325837 / 10000000000000000000000)

theorem Zeta5Irrational.U_430_1 : Uω (aρ 1) (bρ 1) (1826522208027 / 4000000000000) ≤ -(3990569544065491910013 / 5000000000000000000000)

theorem Zeta5Irrational.U_430_2 : Uω (aρ 2) (bρ 2) (1826522208027 / 4000000000000) ≤ -(1004315889034024038327 / 1250000000000000000000)

theorem Zeta5Irrational.U_430_3 : Uω (aρ 3) (bρ 3) (1826522208027 / 4000000000000) ≤ -(8142288165387616772923 / 10000000000000000000000)

theorem Zeta5Irrational.U_430_4 : Uω (aρ 4) (bρ 4) (1826522208027 / 4000000000000) ≤ -(4162126179034898229433 / 5000000000000000000000)

theorem Zeta5Irrational.U_430_5 : Uω (aρ 5) (bρ 5) (1826522208027 / 4000000000000) ≤ -(2152222395771836180129 / 2500000000000000000000)

theorem Zeta5Irrational.U_430_6 : Uω (aρ 6) (bρ 6) (1826522208027 / 4000000000000) ≤ -(9034301722152087805031 / 10000000000000000000000)

theorem Zeta5Irrational.U_430_7 : Uω (aρ 7) (bρ 7) (1826522208027 / 4000000000000) ≤ -(2412905031614942433679 / 2500000000000000000000)

theorem Zeta5Irrational.U_430_8 : Uω (aρ 8) (bρ 8) (1826522208027 / 4000000000000) ≤ -(2633581035938500616407 / 2500000000000000000000)

theorem Zeta5Irrational.U_430_9 : Uω (aρ 9) (bρ 9) (1826522208027 / 4000000000000) ≤ -(11804843234626741708411 / 10000000000000000000000)

theorem Zeta5Irrational.U_430_10 : Uω (aρ 10) (bρ 10) (1826522208027 / 4000000000000) ≤ -(13731068287134637534901 / 10000000000000000000000)

theorem Zeta5Irrational.U_430_11 : Uω (aρ 11) (bρ 11) (1826522208027 / 4000000000000) ≤ -(17436868223522066249077 / 10000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_430 : Uρ (1826522208027 / 4000000000000) ≤ -(5893848409619263390529 / 5000000000000000000000)

theorem Zeta5Irrational.U_431_1 : Uω (aρ 1) (bρ 1) (91458540389 / 200000000000) ≤ -(7966441127904307519531 / 10000000000000000000000)

theorem Zeta5Irrational.U_431_2 : Uω (aρ 2) (bρ 2) (91458540389 / 200000000000) ≤ -(4009874934127237774067 / 5000000000000000000000)

theorem Zeta5Irrational.U_431_3 : Uω (aρ 3) (bρ 3) (91458540389 / 200000000000) ≤ -(4063674458732947917093 / 5000000000000000000000)

theorem Zeta5Irrational.U_431_4 : Uω (aρ 4) (bρ 4) (91458540389 / 200000000000) ≤ -(1661806681693453128021 / 2000000000000000000000)

theorem Zeta5Irrational.U_431_5 : Uω (aρ 5) (bρ 5) (91458540389 / 200000000000) ≤ -(8593216958152678828791 / 10000000000000000000000)

theorem Zeta5Irrational.U_431_6 : Uω (aρ 6) (bρ 6) (91458540389 / 200000000000) ≤ -(9017911729525724670809 / 10000000000000000000000)

theorem Zeta5Irrational.U_431_7 : Uω (aρ 7) (bρ 7) (91458540389 / 200000000000) ≤ -(38536384686198961727 / 40000000000000000000)

theorem Zeta5Irrational.U_431_8 : Uω (aρ 8) (bρ 8) (91458540389 / 200000000000) ≤ -(10514954581502450073807 / 10000000000000000000000)

theorem Zeta5Irrational.U_431_9 : Uω (aρ 9) (bρ 9) (91458540389 / 200000000000) ≤ -(5891112448543313736457 / 5000000000000000000000)

theorem Zeta5Irrational.U_431_10 : Uω (aρ 10) (bρ 10) (91458540389 / 200000000000) ≤ -(13701512890367255710259 / 10000000000000000000000)

theorem Zeta5Irrational.U_431_11 : Uω (aρ 11) (bρ 11) (91458540389 / 200000000000) ≤ -(17376292052470984479999 / 10000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_431 : Uρ (91458540389 / 200000000000) ≤ -(2942675685726804811747 / 2500000000000000000000)

theorem Zeta5Irrational.U_432_1 : Uω (aρ 1) (bρ 1) (1831819407533 / 4000000000000) ≤ -(7951764739322229786499 / 10000000000000000000000)

theorem Zeta5Irrational.U_432_2 : Uω (aρ 2) (bρ 2) (1831819407533 / 4000000000000) ≤ -(1000624303876394457959 / 1250000000000000000000)

theorem Zeta5Irrational.U_432_3 : Uω (aρ 3) (bρ 3) (1831819407533 / 4000000000000) ≤ -(31689187354433060421 / 39062500000000000000)

theorem Zeta5Irrational.U_432_4 : Uω (aρ 4) (bρ 4) (1831819407533 / 4000000000000) ≤ -(8293837610929466732469 / 10000000000000000000000)

theorem Zeta5Irrational.U_432_5 : Uω (aρ 5) (bρ 5) (1831819407533 / 4000000000000) ≤ -(4288784465369381867481 / 5000000000000000000000)

theorem Zeta5Irrational.U_432_6 : Uω (aρ 6) (bρ 6) (1831819407533 / 4000000000000) ≤ -(2250387189094811231179 / 2500000000000000000000)

theorem Zeta5Irrational.U_432_7 : Uω (aρ 7) (bρ 7) (1831819407533 / 4000000000000) ≤ -(4808301710880464751429 / 5000000000000000000000)

theorem Zeta5Irrational.U_432_8 : Uω (aρ 8) (bρ 8) (1831819407533 / 4000000000000) ≤ -(10495624041434001507059 / 10000000000000000000000)

theorem Zeta5Irrational.U_432_9 : Uω (aρ 9) (bρ 9) (1831819407533 / 4000000000000) ≤ -(2939915678554231113423 / 2500000000000000000000)

theorem Zeta5Irrational.U_432_10 : Uω (aρ 10) (bρ 10) (1831819407533 / 4000000000000) ≤ -(13672067484211088375381 / 10000000000000000000000)

theorem Zeta5Irrational.U_432_11 : Uω (aρ 11) (bρ 11) (1831819407533 / 4000000000000) ≤ -(8658255887911272410519 / 5000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_432 : Uρ (1831819407533 / 4000000000000) ≤ -(2938449730656911494861 / 2500000000000000000000)

theorem Zeta5Irrational.U_433_1 : Uω (aρ 1) (bρ 1) (917234003643 / 2000000000000) ≤ -(1587421971831349571987 / 2000000000000000000000)

theorem Zeta5Irrational.U_433_2 : Uω (aρ 2) (bρ 2) (917234003643 / 2000000000000) ≤ -(998782592033725802447 / 1250000000000000000000)

theorem Zeta5Irrational.U_433_3 : Uω (aρ 3) (bρ 3) (917234003643 / 2000000000000) ≤ -(8097537234734476602597 / 10000000000000000000000)

theorem Zeta5Irrational.U_433_4 : Uω (aρ 4) (bρ 4) (917234003643 / 2000000000000) ≤ -(8278664895044969696437 / 10000000000000000000000)

theorem Zeta5Irrational.U_433_5 : Uω (aρ 5) (bρ 5) (917234003643 / 2000000000000) ≤ -(4280972711764913015427 / 5000000000000000000000)

theorem Zeta5Irrational.U_433_6 : Uω (aρ 6) (bρ 6) (917234003643 / 2000000000000) ≤ -(8985212713119600161899 / 10000000000000000000000)

theorem Zeta5Irrational.U_433_7 : Uω (aρ 7) (bρ 7) (917234003643 / 2000000000000) ≤ -(2399785441056326483251 / 2500000000000000000000)

theorem Zeta5Irrational.U_433_8 : Uω (aρ 8) (bρ 8) (917234003643 / 2000000000000) ≤ -(1309541545056140365681 / 1250000000000000000000)

theorem Zeta5Irrational.U_433_9 : Uω (aρ 9) (bρ 9) (917234003643 / 2000000000000) ≤ -(11737156383840359370543 / 10000000000000000000000)

theorem Zeta5Irrational.U_433_10 : Uω (aρ 10) (bρ 10) (917234003643 / 2000000000000) ≤ -(6821365551110305732887 / 5000000000000000000000)

theorem Zeta5Irrational.U_433_11 : Uω (aρ 11) (bρ 11) (917234003643 / 2000000000000) ≤ -(8628749439416123003623 / 5000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_433 : Uρ (917234003643 / 2000000000000) ≤ -(2934245738353066200817 / 2500000000000000000000)

theorem Zeta5Irrational.U_434_1 : Uω (aρ 1) (bρ 1) (1837116607039 / 4000000000000) ≤ -(3961238212228721508109 / 5000000000000000000000)

theorem Zeta5Irrational.U_434_2 : Uω (aρ 2) (bρ 2) (1837116607039 / 4000000000000) ≤ -(7975548720041766875749 / 10000000000000000000000)

theorem Zeta5Irrational.U_434_3 : Uω (aρ 3) (bρ 3) (1837116607039 / 4000000000000) ≤ -(4041332333650775896749 / 5000000000000000000000)

theorem Zeta5Irrational.U_434_4 : Uω (aρ 4) (bρ 4) (1837116607039 / 4000000000000) ≤ -(4131757595361709041687 / 5000000000000000000000)

theorem Zeta5Irrational.U_434_5 : Uω (aρ 5) (bρ 5) (1837116607039 / 4000000000000) ≤ -(1709269271915022459983 / 2000000000000000000000)

theorem Zeta5Irrational.U_434_6 : Uω (aρ 6) (bρ 6) (1837116607039 / 4000000000000) ≤ -(8968903510601811328087 / 10000000000000000000000)

theorem Zeta5Irrational.U_434_7 : Uω (aρ 7) (bρ 7) (1837116607039 / 4000000000000) ≤ -(4790855543348075876977 / 5000000000000000000000)

theorem Zeta5Irrational.U_434_8 : Uω (aρ 8) (bρ 8) (1837116607039 / 4000000000000) ≤ -(10457079376504312439157 / 10000000000000000000000)

theorem Zeta5Irrational.U_434_9 : Uω (aρ 9) (bρ 9) (1837116607039 / 4000000000000) ≤ -(2928676401593483871823 / 2500000000000000000000)

theorem Zeta5Irrational.U_434_10 : Uω (aρ 10) (bρ 10) (1837116607039 / 4000000000000) ≤ -(13613502791977963723017 / 10000000000000000000000)

theorem Zeta5Irrational.U_434_11 : Uω (aρ 11) (bρ 11) (1837116607039 / 4000000000000) ≤ -(3439845305272605237621 / 2000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_434 : Uρ (1837116607039 / 4000000000000) ≤ -(1172025256447057801947 / 1000000000000000000000)

theorem Zeta5Irrational.U_435_1 : Uω (aρ 1) (bρ 1) (229970650849 / 500000000000) ≤ -(3953932186274931808203 / 5000000000000000000000)

theorem Zeta5Irrational.U_435_2 : Uω (aρ 2) (bρ 2) (229970650849 / 500000000000) ≤ -(1592171663724093181691 / 2000000000000000000000)

theorem Zeta5Irrational.U_435_3 : Uω (aρ 3) (bρ 3) (229970650849 / 500000000000) ≤ -(1008476774321000244151 / 1250000000000000000000)

theorem Zeta5Irrational.U_435_4 : Uω (aρ 4) (bρ 4) (229970650849 / 500000000000) ≤ -(1031048553524197032573 / 1250000000000000000000)

theorem Zeta5Irrational.U_435_5 : Uω (aρ 5) (bρ 5) (229970650849 / 500000000000) ≤ -(8530771662286591006543 / 10000000000000000000000)

theorem Zeta5Irrational.U_435_6 : Uω (aρ 6) (bρ 6) (229970650849 / 500000000000) ≤ -(8952621060125969732773 / 10000000000000000000000)

theorem Zeta5Irrational.U_435_7 : Uω (aρ 7) (bρ 7) (229970650849 / 500000000000) ≤ -(9564311277543446347187 / 10000000000000000000000)

theorem Zeta5Irrational.U_435_8 : Uω (aρ 8) (bρ 8) (229970650849 / 500000000000) ≤ -(10437864928602727238181 / 10000000000000000000000)

theorem Zeta5Irrational.U_435_9 : Uω (aρ 9) (bρ 9) (229970650849 / 500000000000) ≤ -(11692310084797909684141 / 10000000000000000000000)

theorem Zeta5Irrational.U_435_10 : Uω (aρ 10) (bρ 10) (229970650849 / 500000000000) ≤ -(13584381614807102870191 / 10000000000000000000000)

theorem Zeta5Irrational.U_435_11 : Uω (aρ 11) (bρ 11) (229970650849 / 500000000000) ≤ -(1714166942718427090193 / 1000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_435 : Uρ (229970650849 / 500000000000) ≤ -(1170360560847339253183 / 1000000000000000000000)