Certified arcsine potential bounds (U28)

theorem Zeta5Irrational.U_340_1 : Uω (aρ 1) (bρ 1) (200369118629 / 640000000000) ≤ -(369418863686504577121 / 312500000000000000000)

theorem Zeta5Irrational.U_340_2 : Uω (aρ 2) (bρ 2) (200369118629 / 640000000000) ≤ -(5950098832509869832131 / 5000000000000000000000)

theorem Zeta5Irrational.U_340_3 : Uω (aρ 3) (bρ 3) (200369118629 / 640000000000) ≤ -(1507522950055079918221 / 1250000000000000000000)

theorem Zeta5Irrational.U_340_4 : Uω (aρ 4) (bρ 4) (200369118629 / 640000000000) ≤ -(616666543212505308213 / 500000000000000000000)

theorem Zeta5Irrational.U_340_5 : Uω (aρ 5) (bρ 5) (200369118629 / 640000000000) ≤ -(3192188962342959562939 / 2500000000000000000000)

theorem Zeta5Irrational.U_340_6 : Uω (aρ 6) (bρ 6) (200369118629 / 640000000000) ≤ -(13440584727778944987359 / 10000000000000000000000)

theorem Zeta5Irrational.U_340_7 : Uω (aρ 7) (bρ 7) (200369118629 / 640000000000) ≤ -(7235321489269726734981 / 5000000000000000000000)

theorem Zeta5Irrational.U_340_8 : Uω (aρ 8) (bρ 8) (200369118629 / 640000000000) ≤ -(8052373851717295670201 / 5000000000000000000000)

theorem Zeta5Irrational.U_340_9 : Uω (aρ 9) (bρ 9) (200369118629 / 640000000000) ≤ -(19129132475187687634013 / 10000000000000000000000)

theorem Zeta5Irrational.U_340_10 : Uω (aρ 10) (bρ 10) (200369118629 / 640000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_340_11 : Uω (aρ 11) (bρ 11) (200369118629 / 640000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_340_12 : Uω (aρ 12) (bρ 12) (200369118629 / 640000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_340_13 : Uω (aρ 13) (bρ 13) (200369118629 / 640000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_340_14 : Uω (aρ 14) (bρ 14) (200369118629 / 640000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_340_15 : Uω (aρ 15) (bρ 15) (200369118629 / 640000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_340_16 : Uω (aρ 16) (bρ 16) (200369118629 / 640000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_340 : Uρ (200369118629 / 640000000000) ≤ -(3956263075367200025727 / 2500000000000000000000)

theorem Zeta5Irrational.U_341_1 : Uω (aρ 1) (bρ 1) (10096199488703 / 32000000000000) ≤ -(11742480570451772639849 / 10000000000000000000000)

theorem Zeta5Irrational.U_341_2 : Uω (aρ 2) (bρ 2) (10096199488703 / 32000000000000) ≤ -(11820645091192290518187 / 10000000000000000000000)

theorem Zeta5Irrational.U_341_3 : Uω (aρ 3) (bρ 3) (10096199488703 / 32000000000000) ≤ -(11979329423253933029181 / 10000000000000000000000)

theorem Zeta5Irrational.U_341_4 : Uω (aρ 4) (bρ 4) (10096199488703 / 32000000000000) ≤ -(12250179083177582271047 / 10000000000000000000000)

theorem Zeta5Irrational.U_341_5 : Uω (aρ 5) (bρ 5) (10096199488703 / 32000000000000) ≤ -(2536346345276691305741 / 2000000000000000000000)

theorem Zeta5Irrational.U_341_6 : Uω (aρ 6) (bρ 6) (10096199488703 / 32000000000000) ≤ -(13347023103751467493021 / 10000000000000000000000)

theorem Zeta5Irrational.U_341_7 : Uω (aρ 7) (bρ 7) (10096199488703 / 32000000000000) ≤ -(1795684838138299536907 / 1250000000000000000000)

theorem Zeta5Irrational.U_341_8 : Uω (aρ 8) (bρ 8) (10096199488703 / 32000000000000) ≤ -(1996986356463040772307 / 1250000000000000000000)

theorem Zeta5Irrational.U_341_9 : Uω (aρ 9) (bρ 9) (10096199488703 / 32000000000000) ≤ -(18924646561087487775289 / 10000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_341 : Uρ (10096199488703 / 32000000000000) ≤ -(15761808112806890583937 / 10000000000000000000000)

theorem Zeta5Irrational.U_342_1 : Uω (aρ 1) (bρ 1) (2543485761489 / 8000000000000) ≤ -(11664175534405795398607 / 10000000000000000000000)

theorem Zeta5Irrational.U_342_2 : Uω (aρ 2) (bρ 2) (2543485761489 / 8000000000000) ≤ -(5870860263786756796371 / 5000000000000000000000)

theorem Zeta5Irrational.U_342_3 : Uω (aρ 3) (bρ 3) (2543485761489 / 8000000000000) ≤ -(2974781067166648350813 / 2500000000000000000000)

theorem Zeta5Irrational.U_342_4 : Uω (aρ 4) (bρ 4) (2543485761489 / 8000000000000) ≤ -(6083857343180408154369 / 5000000000000000000000)

theorem Zeta5Irrational.U_342_5 : Uω (aρ 5) (bρ 5) (2543485761489 / 8000000000000) ≤ -(12595463419058547117867 / 10000000000000000000000)

theorem Zeta5Irrational.U_342_6 : Uω (aρ 6) (bρ 6) (2543485761489 / 8000000000000) ≤ -(6627172050807757955697 / 5000000000000000000000)

theorem Zeta5Irrational.U_342_7 : Uω (aρ 7) (bρ 7) (2543485761489 / 8000000000000) ≤ -(14261459727060855781449 / 10000000000000000000000)

theorem Zeta5Irrational.U_342_8 : Uω (aρ 8) (bρ 8) (2543485761489 / 8000000000000) ≤ -(990555338418671925963 / 625000000000000000000)

theorem Zeta5Irrational.U_342_9 : Uω (aρ 9) (bρ 9) (2543485761489 / 8000000000000) ≤ -(4681560142880333083387 / 2500000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_342 : Uρ (2543485761489 / 8000000000000) ≤ -(15699576321583142466967 / 10000000000000000000000)

theorem Zeta5Irrational.U_343_1 : Uω (aρ 1) (bρ 1) (10251686603209 / 32000000000000) ≤ -(5793239462649911037 / 5000000000000000000)

theorem Zeta5Irrational.U_343_2 : Uω (aρ 2) (bρ 2) (10251686603209 / 32000000000000) ≤ -(2332682826846300534697 / 2000000000000000000000)

theorem Zeta5Irrational.U_343_3 : Uω (aρ 3) (bρ 3) (10251686603209 / 32000000000000) ≤ -(2954889447974945029483 / 2500000000000000000000)

theorem Zeta5Irrational.U_343_4 : Uω (aρ 4) (bρ 4) (10251686603209 / 32000000000000) ≤ -(6042963187737180019357 / 5000000000000000000000)

theorem Zeta5Irrational.U_343_5 : Uω (aρ 5) (bρ 5) (10251686603209 / 32000000000000) ≤ -(12509937826887110023689 / 10000000000000000000000)

theorem Zeta5Irrational.U_343_6 : Uω (aρ 6) (bρ 6) (10251686603209 / 32000000000000) ≤ -(13162530945191651836923 / 10000000000000000000000)

theorem Zeta5Irrational.U_343_7 : Uω (aρ 7) (bρ 7) (10251686603209 / 32000000000000) ≤ -(14158560319631239190253 / 10000000000000000000000)

theorem Zeta5Irrational.U_343_8 : Uω (aρ 8) (bρ 8) (10251686603209 / 32000000000000) ≤ -(15723673450207903387083 / 10000000000000000000000)

theorem Zeta5Irrational.U_343_9 : Uω (aρ 9) (bρ 9) (10251686603209 / 32000000000000) ≤ -(741338966521064763589 / 400000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_343 : Uρ (10251686603209 / 32000000000000) ≤ -(7819153509420200613333 / 5000000000000000000000)

theorem Zeta5Irrational.U_344_1 : Uω (aρ 1) (bρ 1) (5164715080231 / 16000000000000) ≤ -(2301876272154925326387 / 2000000000000000000000)

theorem Zeta5Irrational.U_344_2 : Uω (aρ 2) (bρ 2) (5164715080231 / 16000000000000) ≤ -(11585716300751941489211 / 10000000000000000000000)

theorem Zeta5Irrational.U_344_3 : Uω (aρ 3) (bρ 3) (5164715080231 / 16000000000000) ≤ -(11740619893739643235129 / 10000000000000000000000)

theorem Zeta5Irrational.U_344_4 : Uω (aρ 4) (bρ 4) (5164715080231 / 16000000000000) ≤ -(240096062582495861523 / 200000000000000000000)

theorem Zeta5Irrational.U_344_5 : Uω (aρ 5) (bρ 5) (5164715080231 / 16000000000000) ≤ -(6212571094579826978127 / 5000000000000000000000)

theorem Zeta5Irrational.U_344_6 : Uω (aρ 6) (bρ 6) (5164715080231 / 16000000000000) ≤ -(13071567339577674235373 / 10000000000000000000000)

theorem Zeta5Irrational.U_344_7 : Uω (aρ 7) (bρ 7) (5164715080231 / 16000000000000) ≤ -(14056755646450440234437 / 10000000000000000000000)

theorem Zeta5Irrational.U_344_8 : Uω (aρ 8) (bρ 8) (5164715080231 / 16000000000000) ≤ -(195002498657717841121 / 125000000000000000000)

theorem Zeta5Irrational.U_344_9 : Uω (aρ 9) (bρ 9) (5164715080231 / 16000000000000) ≤ -(3669191631964464684769 / 2000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_344 : Uρ (5164715080231 / 16000000000000) ≤ -(3115591048149674882067 / 2000000000000000000000)

theorem Zeta5Irrational.U_345_1 : Uω (aρ 1) (bρ 1) (1310614659371 / 4000000000000) ≤ -(11356946906342816493083 / 10000000000000000000000)

theorem Zeta5Irrational.U_345_2 : Uω (aρ 2) (bρ 2) (1310614659371 / 4000000000000) ≤ -(11432108977075101674191 / 10000000000000000000000)

theorem Zeta5Irrational.U_345_3 : Uω (aρ 3) (bρ 3) (1310614659371 / 4000000000000) ≤ -(5792295309103324570207 / 5000000000000000000000)

theorem Zeta5Irrational.U_345_4 : Uω (aρ 4) (bρ 4) (1310614659371 / 4000000000000) ≤ -(11844509075501430543993 / 10000000000000000000000)

theorem Zeta5Irrational.U_345_5 : Uω (aρ 5) (bρ 5) (1310614659371 / 4000000000000) ≤ -(2451538272676043922751 / 2000000000000000000000)

theorem Zeta5Irrational.U_345_6 : Uω (aρ 6) (bρ 6) (1310614659371 / 4000000000000) ≤ -(50359866786970237563 / 39062500000000000000)

theorem Zeta5Irrational.U_345_7 : Uω (aρ 7) (bρ 7) (1310614659371 / 4000000000000) ≤ -(3464083838632482367617 / 2500000000000000000000)

theorem Zeta5Irrational.U_345_8 : Uω (aρ 8) (bρ 8) (1310614659371 / 4000000000000) ≤ -(7679130478477478291329 / 5000000000000000000000)

theorem Zeta5Irrational.U_345_9 : Uω (aρ 9) (bρ 9) (1310614659371 / 4000000000000) ≤ -(449633250021974099083 / 250000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_345 : Uρ (1310614659371 / 4000000000000) ≤ -(15459844878657915384769 / 10000000000000000000000)

theorem Zeta5Irrational.U_346_1 : Uω (aρ 1) (bρ 1) (5320202194737 / 16000000000000) ≤ -(1400850162952081230453 / 1250000000000000000000)

theorem Zeta5Irrational.U_346_2 : Uω (aρ 2) (bρ 2) (5320202194737 / 16000000000000) ≤ -(11280826001053343395199 / 10000000000000000000000)

theorem Zeta5Irrational.U_346_3 : Uω (aρ 3) (bρ 3) (5320202194737 / 16000000000000) ≤ -(228619205476329618989 / 200000000000000000000)

theorem Zeta5Irrational.U_346_4 : Uω (aρ 4) (bρ 4) (5320202194737 / 16000000000000) ≤ -(11686749560023923541033 / 10000000000000000000000)

theorem Zeta5Irrational.U_346_5 : Uω (aρ 5) (bρ 5) (5320202194737 / 16000000000000) ≤ -(12093015219054816054701 / 10000000000000000000000)

theorem Zeta5Irrational.U_346_6 : Uω (aρ 6) (bρ 6) (5320202194737 / 16000000000000) ≤ -(6357949180291555523893 / 5000000000000000000000)

theorem Zeta5Irrational.U_346_7 : Uω (aρ 7) (bρ 7) (5320202194737 / 16000000000000) ≤ -(6830008200364275306877 / 5000000000000000000000)

theorem Zeta5Irrational.U_346_8 : Uω (aρ 8) (bρ 8) (5320202194737 / 16000000000000) ≤ -(7561339280388101403409 / 5000000000000000000000)

theorem Zeta5Irrational.U_346_9 : Uω (aρ 9) (bρ 9) (5320202194737 / 16000000000000) ≤ -(2756562137920207449 / 1562500000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_346 : Uρ (5320202194737 / 16000000000000) ≤ -(15344959851341678360121 / 10000000000000000000000)

theorem Zeta5Irrational.U_347_1 : Uω (aρ 1) (bρ 1) (539794575199 / 1600000000000) ≤ -(5529438415241096726837 / 5000000000000000000000)

theorem Zeta5Irrational.U_347_2 : Uω (aρ 2) (bρ 2) (539794575199 / 1600000000000) ≤ -(2782949515805895480333 / 2500000000000000000000)

theorem Zeta5Irrational.U_347_3 : Uω (aρ 3) (bρ 3) (539794575199 / 1600000000000) ≤ -(2819914039390198190657 / 2500000000000000000000)

theorem Zeta5Irrational.U_347_4 : Uω (aρ 4) (bρ 4) (539794575199 / 1600000000000) ≤ -(1153144550858087381687 / 1000000000000000000000)

theorem Zeta5Irrational.U_347_5 : Uω (aρ 5) (bρ 5) (539794575199 / 1600000000000) ≤ -(1193102277038038876959 / 1000000000000000000000)

theorem Zeta5Irrational.U_347_6 : Uω (aρ 6) (bρ 6) (539794575199 / 1600000000000) ≤ -(6271384959581393181183 / 5000000000000000000000)

theorem Zeta5Irrational.U_347_7 : Uω (aρ 7) (bρ 7) (539794575199 / 1600000000000) ≤ -(2693525626556395372243 / 2000000000000000000000)

theorem Zeta5Irrational.U_347_8 : Uω (aρ 8) (bρ 8) (539794575199 / 1600000000000) ≤ -(14893097731127274734401 / 10000000000000000000000)

theorem Zeta5Irrational.U_347_9 : Uω (aρ 9) (bρ 9) (539794575199 / 1600000000000) ≤ -(17314042422240819869213 / 10000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_347 : Uρ (539794575199 / 1600000000000) ≤ -(7616529524551265616913 / 5000000000000000000000)

theorem Zeta5Irrational.U_348_1 : Uω (aρ 1) (bρ 1) (5475689309243 / 16000000000000) ≤ -(2728277181692807866107 / 2500000000000000000000)

theorem Zeta5Irrational.U_348_2 : Uω (aρ 2) (bρ 2) (5475689309243 / 16000000000000) ≤ -(10984958909324133836937 / 10000000000000000000000)

theorem Zeta5Irrational.U_348_3 : Uω (aρ 3) (bρ 3) (5475689309243 / 16000000000000) ≤ -(1113060882446734250669 / 1000000000000000000000)

theorem Zeta5Irrational.U_348_4 : Uω (aρ 4) (bρ 4) (5475689309243 / 16000000000000) ≤ -(5689260749156044347883 / 5000000000000000000000)

theorem Zeta5Irrational.U_348_5 : Uω (aρ 5) (bρ 5) (5475689309243 / 16000000000000) ≤ -(470865098371135128527 / 400000000000000000000)

theorem Zeta5Irrational.U_348_6 : Uω (aρ 6) (bρ 6) (5475689309243 / 16000000000000) ≤ -(12372631891703963693447 / 10000000000000000000000)

theorem Zeta5Irrational.U_348_7 : Uω (aρ 7) (bρ 7) (5475689309243 / 16000000000000) ≤ -(6639505332453721451779 / 5000000000000000000000)

theorem Zeta5Irrational.U_348_8 : Uω (aρ 8) (bρ 8) (5475689309243 / 16000000000000) ≤ -(14669194304964489016403 / 10000000000000000000000)

theorem Zeta5Irrational.U_348_9 : Uω (aρ 9) (bρ 9) (5475689309243 / 16000000000000) ≤ -(2124984692148639207169 / 1250000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_348 : Uρ (5475689309243 / 16000000000000) ≤ -(15123935587556814908631 / 10000000000000000000000)

theorem Zeta5Irrational.U_349_1 : Uω (aρ 1) (bρ 1) (86772388539 / 250000000000) ≤ -(2692358756001912750639 / 2500000000000000000000)

theorem Zeta5Irrational.U_349_2 : Uω (aρ 2) (bρ 2) (86772388539 / 250000000000) ≤ -(2710061290822971316719 / 2500000000000000000000)

theorem Zeta5Irrational.U_349_3 : Uω (aρ 3) (bρ 3) (86772388539 / 250000000000) ≤ -(2745937973915816665167 / 2500000000000000000000)

theorem Zeta5Irrational.U_349_4 : Uω (aρ 4) (bρ 4) (86772388539 / 250000000000) ≤ -(1403488191972210064163 / 1250000000000000000000)

theorem Zeta5Irrational.U_349_5 : Uω (aρ 5) (bρ 5) (86772388539 / 250000000000) ≤ -(181480419862451201021 / 156250000000000000000)

theorem Zeta5Irrational.U_349_6 : Uω (aρ 6) (bρ 6) (86772388539 / 250000000000) ≤ -(488215251642030165167 / 400000000000000000000)

theorem Zeta5Irrational.U_349_7 : Uω (aρ 7) (bρ 7) (86772388539 / 250000000000) ≤ -(3273503492390745150533 / 2500000000000000000000)

theorem Zeta5Irrational.U_349_8 : Uω (aρ 8) (bρ 8) (86772388539 / 250000000000) ≤ -(3612667828037066073951 / 2500000000000000000000)

theorem Zeta5Irrational.U_349_9 : Uω (aρ 9) (bρ 9) (86772388539 / 250000000000) ≤ -(16698172633618705145123 / 10000000000000000000000)

theorem Zeta5Irrational.U_349_10 : Uω (aρ 10) (bρ 10) (86772388539 / 250000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_349_11 : Uω (aρ 11) (bρ 11) (86772388539 / 250000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_349 : Uρ (86772388539 / 250000000000) ≤ -(3754352408588390882517 / 2500000000000000000000)

theorem Zeta5Irrational.U_350_1 : Uω (aρ 1) (bρ 1) (11190582883251 / 32000000000000) ≤ -(10692924948722708581073 / 10000000000000000000000)

theorem Zeta5Irrational.U_350_2 : Uω (aρ 2) (bρ 2) (11190582883251 / 32000000000000) ≤ -(5381593741458052326591 / 5000000000000000000000)

theorem Zeta5Irrational.U_350_3 : Uω (aρ 3) (bρ 3) (11190582883251 / 32000000000000) ≤ -(10905566206672627143071 / 10000000000000000000000)

theorem Zeta5Irrational.U_350_4 : Uω (aρ 4) (bρ 4) (11190582883251 / 32000000000000) ≤ -(11147742773399472978853 / 10000000000000000000000)

theorem Zeta5Irrational.U_350_5 : Uω (aρ 5) (bρ 5) (11190582883251 / 32000000000000) ≤ -(5765646633728764278609 / 5000000000000000000000)

theorem Zeta5Irrational.U_350_6 : Uω (aρ 6) (bρ 6) (11190582883251 / 32000000000000) ≤ -(12116491871022092607709 / 10000000000000000000000)

theorem Zeta5Irrational.U_350_7 : Uω (aρ 7) (bρ 7) (11190582883251 / 32000000000000) ≤ -(12995858129784667405647 / 10000000000000000000000)

theorem Zeta5Irrational.U_350_8 : Uω (aρ 8) (bρ 8) (11190582883251 / 32000000000000) ≤ -(7167573149467358629037 / 5000000000000000000000)

theorem Zeta5Irrational.U_350_9 : Uω (aρ 9) (bρ 9) (11190582883251 / 32000000000000) ≤ -(8270243481336133218047 / 5000000000000000000000)

theorem Zeta5Irrational.U_350_10 : Uω (aρ 10) (bρ 10) (11190582883251 / 32000000000000) ≤ -(2271398553081343851221 / 1000000000000000000000)

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

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

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

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

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

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

theorem Zeta5Irrational.U_350 : Uρ (11190582883251 / 32000000000000) ≤ -(14812819820006037121807 / 10000000000000000000000)

theorem Zeta5Irrational.U_351_1 : Uω (aρ 1) (bρ 1) (1127430003351 / 3200000000000) ≤ -(2123399165295955899713 / 2000000000000000000000)

theorem Zeta5Irrational.U_351_2 : Uω (aρ 2) (bρ 2) (1127430003351 / 3200000000000) ≤ -(2671679790056744699741 / 2500000000000000000000)

theorem Zeta5Irrational.U_351_3 : Uω (aρ 3) (bρ 3) (1127430003351 / 3200000000000) ≤ -(10827987472984737147193 / 10000000000000000000000)

theorem Zeta5Irrational.U_351_4 : Uω (aρ 4) (bρ 4) (1127430003351 / 3200000000000) ≤ -(5534109374562723863797 / 5000000000000000000000)

theorem Zeta5Irrational.U_351_5 : Uω (aρ 5) (bρ 5) (1127430003351 / 3200000000000) ≤ -(2862133506329783265521 / 2500000000000000000000)

theorem Zeta5Irrational.U_351_6 : Uω (aρ 6) (bρ 6) (1127430003351 / 3200000000000) ≤ -(6014198225391302158967 / 5000000000000000000000)

theorem Zeta5Irrational.U_351_7 : Uω (aρ 7) (bρ 7) (1127430003351 / 3200000000000) ≤ -(50385507542380392039 / 39062500000000000000)

theorem Zeta5Irrational.U_351_8 : Uω (aρ 8) (bρ 8) (1127430003351 / 3200000000000) ≤ -(2844212325531341812721 / 2000000000000000000000)

theorem Zeta5Irrational.U_351_9 : Uω (aρ 9) (bρ 9) (1127430003351 / 3200000000000) ≤ -(4096481844382657276603 / 2500000000000000000000)

theorem Zeta5Irrational.U_351_10 : Uω (aρ 10) (bρ 10) (1127430003351 / 3200000000000) ≤ -(219985771669146987571 / 100000000000000000000)

theorem Zeta5Irrational.U_351_11 : Uω (aρ 11) (bρ 11) (1127430003351 / 3200000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_351_12 : Uω (aρ 12) (bρ 12) (1127430003351 / 3200000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_351_13 : Uω (aρ 13) (bρ 13) (1127430003351 / 3200000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_351_14 : Uω (aρ 14) (bρ 14) (1127430003351 / 3200000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_351_15 : Uω (aρ 15) (bρ 15) (1127430003351 / 3200000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_351_16 : Uω (aρ 16) (bρ 16) (1127430003351 / 3200000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_351 : Uρ (1127430003351 / 3200000000000) ≤ -(14696020735188019821327 / 10000000000000000000000)