Certified arcsine potential bounds (U17)

theorem Zeta5Irrational.U_208_1 : Uω (aρ 1) (bρ 1) (634082945103 / 4000000000000) ≤ -(18834775819919365320531 / 10000000000000000000000)

theorem Zeta5Irrational.U_208_2 : Uω (aρ 2) (bρ 2) (634082945103 / 4000000000000) ≤ -(18996351001129505770501 / 10000000000000000000000)

theorem Zeta5Irrational.U_208_3 : Uω (aρ 3) (bρ 3) (634082945103 / 4000000000000) ≤ -(19331004852514832193709 / 10000000000000000000000)

theorem Zeta5Irrational.U_208_4 : Uω (aρ 4) (bρ 4) (634082945103 / 4000000000000) ≤ -(19925043404826570845423 / 10000000000000000000000)

theorem Zeta5Irrational.U_208_5 : Uω (aρ 5) (bρ 5) (634082945103 / 4000000000000) ≤ -(2618004087800691493427 / 1250000000000000000000)

theorem Zeta5Irrational.U_208_6 : Uω (aρ 6) (bρ 6) (634082945103 / 4000000000000) ≤ -(22769024589857949647633 / 10000000000000000000000)

theorem Zeta5Irrational.U_208_7 : Uω (aρ 7) (bρ 7) (634082945103 / 4000000000000) ≤ -(27059794013414673404811 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_208 : Uρ (634082945103 / 4000000000000) ≤ -(21144826167404248198697 / 10000000000000000000000)

theorem Zeta5Irrational.U_209_1 : Uω (aρ 1) (bρ 1) (20347434278567 / 128000000000000) ≤ -(9402822015822657623339 / 5000000000000000000000)

theorem Zeta5Irrational.U_209_2 : Uω (aρ 2) (bρ 2) (20347434278567 / 128000000000000) ≤ -(18966733481316253290297 / 10000000000000000000000)

theorem Zeta5Irrational.U_209_3 : Uω (aρ 3) (bρ 3) (20347434278567 / 128000000000000) ≤ -(19300341465000340110197 / 10000000000000000000000)

theorem Zeta5Irrational.U_209_4 : Uω (aρ 4) (bρ 4) (20347434278567 / 128000000000000) ≤ -(3978475927905370941629 / 2000000000000000000000)

theorem Zeta5Irrational.U_209_5 : Uω (aρ 5) (bρ 5) (20347434278567 / 128000000000000) ≤ -(5226858955032555311931 / 2500000000000000000000)

theorem Zeta5Irrational.U_209_6 : Uω (aρ 6) (bρ 6) (20347434278567 / 128000000000000) ≤ -(22723231852291062307257 / 10000000000000000000000)

theorem Zeta5Irrational.U_209_7 : Uω (aρ 7) (bρ 7) (20347434278567 / 128000000000000) ≤ -(26966981408494280424653 / 10000000000000000000000)

theorem Zeta5Irrational.U_209_8 : Uω (aρ 8) (bρ 8) (20347434278567 / 128000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_209_9 : Uω (aρ 9) (bρ 9) (20347434278567 / 128000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_209_10 : Uω (aρ 10) (bρ 10) (20347434278567 / 128000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_209_11 : Uω (aρ 11) (bρ 11) (20347434278567 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_209_12 : Uω (aρ 12) (bρ 12) (20347434278567 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_209_13 : Uω (aρ 13) (bρ 13) (20347434278567 / 128000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_209_14 : Uω (aρ 14) (bρ 14) (20347434278567 / 128000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_209_15 : Uω (aρ 15) (bρ 15) (20347434278567 / 128000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_209_16 : Uω (aρ 16) (bρ 16) (20347434278567 / 128000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_209 : Uρ (20347434278567 / 128000000000000) ≤ -(5281603793154777291613 / 2500000000000000000000)

theorem Zeta5Irrational.U_210_1 : Uω (aρ 1) (bρ 1) (10202107156919 / 64000000000000) ≤ -(18776596874758489166257 / 10000000000000000000000)

theorem Zeta5Irrational.U_210_2 : Uω (aρ 2) (bρ 2) (10202107156919 / 64000000000000) ≤ -(9468601752239696732103 / 5000000000000000000000)

theorem Zeta5Irrational.U_210_3 : Uω (aρ 3) (bρ 3) (10202107156919 / 64000000000000) ≤ -(19269772143215850917411 / 10000000000000000000000)

theorem Zeta5Irrational.U_210_4 : Uω (aρ 4) (bρ 4) (10202107156919 / 64000000000000) ≤ -(124123896360046046919 / 62500000000000000000)

theorem Zeta5Irrational.U_210_5 : Uω (aρ 5) (bρ 5) (10202107156919 / 64000000000000) ≤ -(20870977099919409056433 / 10000000000000000000000)

theorem Zeta5Irrational.U_210_6 : Uω (aρ 6) (bρ 6) (10202107156919 / 64000000000000) ≤ -(11338836658656259650589 / 5000000000000000000000)

theorem Zeta5Irrational.U_210_7 : Uω (aρ 7) (bρ 7) (10202107156919 / 64000000000000) ≤ -(13437846207618377346453 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_210 : Uρ (10202107156919 / 64000000000000) ≤ -(5277043811099700677133 / 2500000000000000000000)

theorem Zeta5Irrational.U_211_1 : Uω (aρ 1) (bρ 1) (20460994349109 / 128000000000000) ≤ -(9373816929443217670237 / 5000000000000000000000)

theorem Zeta5Irrational.U_211_2 : Uω (aρ 2) (bρ 2) (20460994349109 / 128000000000000) ≤ -(1890776055414610494797 / 1000000000000000000000)

theorem Zeta5Irrational.U_211_3 : Uω (aρ 3) (bρ 3) (20460994349109 / 128000000000000) ≤ -(19239296309802124964013 / 10000000000000000000000)

theorem Zeta5Irrational.U_211_4 : Uω (aρ 4) (bρ 4) (20460994349109 / 128000000000000) ≤ -(4956843506365323570481 / 2500000000000000000000)

theorem Zeta5Irrational.U_211_5 : Uω (aρ 5) (bρ 5) (20460994349109 / 128000000000000) ≤ -(10417327733948295803493 / 5000000000000000000000)

theorem Zeta5Irrational.U_211_6 : Uω (aρ 6) (bρ 6) (20460994349109 / 128000000000000) ≤ -(5658086589788000643379 / 2500000000000000000000)

theorem Zeta5Irrational.U_211_7 : Uω (aρ 7) (bρ 7) (20460994349109 / 128000000000000) ≤ -(6696465406727953716517 / 2500000000000000000000)

theorem Zeta5Irrational.U_211_8 : Uω (aρ 8) (bρ 8) (20460994349109 / 128000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_211_9 : Uω (aρ 9) (bρ 9) (20460994349109 / 128000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_211_10 : Uω (aρ 10) (bρ 10) (20460994349109 / 128000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_211_11 : Uω (aρ 11) (bρ 11) (20460994349109 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_211_12 : Uω (aρ 12) (bρ 12) (20460994349109 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_211_13 : Uω (aρ 13) (bρ 13) (20460994349109 / 128000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_211_14 : Uω (aρ 14) (bρ 14) (20460994349109 / 128000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_211_15 : Uω (aρ 15) (bρ 15) (20460994349109 / 128000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_211_16 : Uω (aρ 16) (bρ 16) (20460994349109 / 128000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_211 : Uρ (20460994349109 / 128000000000000) ≤ -(4218020092928001477611 / 2000000000000000000000)

theorem Zeta5Irrational.U_212_1 : Uω (aρ 1) (bρ 1) (1025888719219 / 6400000000000) ≤ -(9359377248953476493289 / 5000000000000000000000)

theorem Zeta5Irrational.U_212_2 : Uω (aρ 2) (bρ 2) (1025888719219 / 6400000000000) ≤ -(943920205920242897763 / 500000000000000000000)

theorem Zeta5Irrational.U_212_3 : Uω (aρ 3) (bρ 3) (1025888719219 / 6400000000000) ≤ -(19208913392717338753281 / 10000000000000000000000)

theorem Zeta5Irrational.U_212_4 : Uω (aρ 4) (bρ 4) (1025888719219 / 6400000000000) ≤ -(791801230265439478831 / 400000000000000000000)

theorem Zeta5Irrational.U_212_5 : Uω (aρ 5) (bρ 5) (1025888719219 / 6400000000000) ≤ -(20798469863029981377397 / 10000000000000000000000)

theorem Zeta5Irrational.U_212_6 : Uω (aρ 6) (bρ 6) (1025888719219 / 6400000000000) ≤ -(2823406049901683619027 / 1250000000000000000000)

theorem Zeta5Irrational.U_212_7 : Uω (aρ 7) (bρ 7) (1025888719219 / 6400000000000) ≤ -(26697428239469773735417 / 10000000000000000000000)

theorem Zeta5Irrational.U_212_8 : Uω (aρ 8) (bρ 8) (1025888719219 / 6400000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_212_9 : Uω (aρ 9) (bρ 9) (1025888719219 / 6400000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_212_10 : Uω (aρ 10) (bρ 10) (1025888719219 / 6400000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_212_11 : Uω (aρ 11) (bρ 11) (1025888719219 / 6400000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_212_12 : Uω (aρ 12) (bρ 12) (1025888719219 / 6400000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_212_13 : Uω (aρ 13) (bρ 13) (1025888719219 / 6400000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_212_14 : Uω (aρ 14) (bρ 14) (1025888719219 / 6400000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_212_15 : Uω (aρ 15) (bρ 15) (1025888719219 / 6400000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_212_16 : Uω (aρ 16) (bρ 16) (1025888719219 / 6400000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_212 : Uρ (1025888719219 / 6400000000000) ≤ -(5268046327809099390991 / 2500000000000000000000)

theorem Zeta5Irrational.U_213_1 : Uω (aρ 1) (bρ 1) (20574554419651 / 128000000000000) ≤ -(18689958309899125630867 / 10000000000000000000000)

theorem Zeta5Irrational.U_213_2 : Uω (aρ 2) (bρ 2) (20574554419651 / 128000000000000) ≤ -(294517713903934530317 / 156250000000000000000)

theorem Zeta5Irrational.U_213_3 : Uω (aρ 3) (bρ 3) (20574554419651 / 128000000000000) ≤ -(19178622825171756382173 / 10000000000000000000000)

theorem Zeta5Irrational.U_213_4 : Uω (aρ 4) (bρ 4) (20574554419651 / 128000000000000) ≤ -(988139645586834072963 / 500000000000000000000)

theorem Zeta5Irrational.U_213_5 : Uω (aρ 5) (bρ 5) (20574554419651 / 128000000000000) ≤ -(5190604809880666183443 / 2500000000000000000000)

theorem Zeta5Irrational.U_213_6 : Uω (aρ 6) (bρ 6) (20574554419651 / 128000000000000) ≤ -(11271188452447671165599 / 5000000000000000000000)

theorem Zeta5Irrational.U_213_7 : Uω (aρ 7) (bρ 7) (20574554419651 / 128000000000000) ≤ -(2661033560846422827913 / 1000000000000000000000)

theorem Zeta5Irrational.U_213_8 : Uω (aρ 8) (bρ 8) (20574554419651 / 128000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_213_9 : Uω (aρ 9) (bρ 9) (20574554419651 / 128000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_213_10 : Uω (aρ 10) (bρ 10) (20574554419651 / 128000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_213_11 : Uω (aρ 11) (bρ 11) (20574554419651 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_213_12 : Uω (aρ 12) (bρ 12) (20574554419651 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_213_13 : Uω (aρ 13) (bρ 13) (20574554419651 / 128000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_213_14 : Uω (aρ 14) (bρ 14) (20574554419651 / 128000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_213_15 : Uω (aρ 15) (bρ 15) (20574554419651 / 128000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_213_16 : Uω (aρ 16) (bρ 16) (20574554419651 / 128000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_213 : Uρ (20574554419651 / 128000000000000) ≤ -(21054424620542273751667 / 10000000000000000000000)

theorem Zeta5Irrational.U_214_1 : Uω (aρ 1) (bρ 1) (10315667227461 / 64000000000000) ≤ -(18661244817095025294763 / 10000000000000000000000)

theorem Zeta5Irrational.U_214_2 : Uω (aρ 2) (bρ 2) (10315667227461 / 64000000000000) ≤ -(4704987191384496238617 / 2500000000000000000000)

theorem Zeta5Irrational.U_214_3 : Uω (aρ 3) (bρ 3) (10315667227461 / 64000000000000) ≤ -(19148424045563445068967 / 10000000000000000000000)

theorem Zeta5Irrational.U_214_4 : Uω (aρ 4) (bρ 4) (10315667227461 / 64000000000000) ≤ -(1973065979833186243353 / 1000000000000000000000)

theorem Zeta5Irrational.U_214_5 : Uω (aρ 5) (bρ 5) (10315667227461 / 64000000000000) ≤ -(10363251278104916277097 / 5000000000000000000000)

theorem Zeta5Irrational.U_214_6 : Uω (aρ 6) (bρ 6) (10315667227461 / 64000000000000) ≤ -(703054043389017050231 / 312500000000000000000)

theorem Zeta5Irrational.U_214_7 : Uω (aρ 7) (bρ 7) (10315667227461 / 64000000000000) ≤ -(13262265429716689337577 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_214 : Uρ (10315667227461 / 64000000000000) ≤ -(21036813553478639506113 / 10000000000000000000000)

theorem Zeta5Irrational.U_215_1 : Uω (aρ 1) (bρ 1) (20688114490193 / 128000000000000) ≤ -(18632613545832130859089 / 10000000000000000000000)

theorem Zeta5Irrational.U_215_2 : Uω (aρ 2) (bρ 2) (20688114490193 / 128000000000000) ≤ -(18790848846917232790029 / 10000000000000000000000)

theorem Zeta5Irrational.U_215_3 : Uω (aρ 3) (bρ 3) (20688114490193 / 128000000000000) ≤ -(19118316497414914090889 / 10000000000000000000000)

theorem Zeta5Irrational.U_215_4 : Uω (aρ 4) (bρ 4) (20688114490193 / 128000000000000) ≤ -(19698630730860232821229 / 10000000000000000000000)

theorem Zeta5Irrational.U_215_5 : Uω (aρ 5) (bρ 5) (20688114490193 / 128000000000000) ≤ -(20690718791954763536791 / 10000000000000000000000)

theorem Zeta5Irrational.U_215_6 : Uω (aρ 6) (bρ 6) (20688114490193 / 128000000000000) ≤ -(22453303405870982867681 / 10000000000000000000000)

theorem Zeta5Irrational.U_215_7 : Uω (aρ 7) (bρ 7) (20688114490193 / 128000000000000) ≤ -(6609991136014297365741 / 2500000000000000000000)

theorem Zeta5Irrational.U_215_8 : Uω (aρ 8) (bρ 8) (20688114490193 / 128000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_215_9 : Uω (aρ 9) (bρ 9) (20688114490193 / 128000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_215_10 : Uω (aρ 10) (bρ 10) (20688114490193 / 128000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_215_11 : Uω (aρ 11) (bρ 11) (20688114490193 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_215_12 : Uω (aρ 12) (bρ 12) (20688114490193 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_215_13 : Uω (aρ 13) (bρ 13) (20688114490193 / 128000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_215_14 : Uω (aρ 14) (bρ 14) (20688114490193 / 128000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_215_15 : Uω (aρ 15) (bρ 15) (20688114490193 / 128000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_215_16 : Uω (aρ 16) (bρ 16) (20688114490193 / 128000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_215 : Uρ (20688114490193 / 128000000000000) ≤ -(21019347567321569209947 / 10000000000000000000000)

theorem Zeta5Irrational.U_216_1 : Uω (aρ 1) (bρ 1) (2593111815683 / 16000000000000) ≤ -(744162561060257032513 / 400000000000000000000)

theorem Zeta5Irrational.U_216_2 : Uω (aρ 2) (bρ 2) (2593111815683 / 16000000000000) ≤ -(18761833439794934696371 / 10000000000000000000000)

theorem Zeta5Irrational.U_216_3 : Uω (aρ 3) (bρ 3) (2593111815683 / 16000000000000) ≤ -(19088299629310782092179 / 10000000000000000000000)

theorem Zeta5Irrational.U_216_4 : Uω (aρ 4) (bρ 4) (2593111815683 / 16000000000000) ≤ -(393334100610784337877 / 200000000000000000000)

theorem Zeta5Irrational.U_216_5 : Uω (aρ 5) (bρ 5) (2593111815683 / 16000000000000) ≤ -(20655066935054398764263 / 10000000000000000000000)

theorem Zeta5Irrational.U_216_6 : Uω (aρ 6) (bρ 6) (2593111815683 / 16000000000000) ≤ -(22409096555836940562381 / 10000000000000000000000)

theorem Zeta5Irrational.U_216_7 : Uω (aρ 7) (bρ 7) (2593111815683 / 16000000000000) ≤ -(3294573791959917824413 / 1250000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_216 : Uρ (2593111815683 / 16000000000000) ≤ -(10501011194519760065581 / 5000000000000000000000)

theorem Zeta5Irrational.U_217_1 : Uω (aρ 1) (bρ 1) (4160334912147 / 25600000000000) ≤ -(18575595793526144554733 / 10000000000000000000000)

theorem Zeta5Irrational.U_217_2 : Uω (aρ 2) (bρ 2) (4160334912147 / 25600000000000) ≤ -(9366451027138736003651 / 5000000000000000000000)

theorem Zeta5Irrational.U_217_3 : Uω (aρ 3) (bρ 3) (4160334912147 / 25600000000000) ≤ -(19058372894836346185957 / 10000000000000000000000)

theorem Zeta5Irrational.U_217_4 : Uω (aρ 4) (bρ 4) (4160334912147 / 25600000000000) ≤ -(490872050631875603417 / 250000000000000000000)

theorem Zeta5Irrational.U_217_5 : Uω (aρ 5) (bρ 5) (4160334912147 / 25600000000000) ≤ -(20619545985646205896543 / 10000000000000000000000)

theorem Zeta5Irrational.U_217_6 : Uω (aρ 6) (bρ 6) (4160334912147 / 25600000000000) ≤ -(22365106478660146974889 / 10000000000000000000000)

theorem Zeta5Irrational.U_217_7 : Uω (aρ 7) (bρ 7) (4160334912147 / 25600000000000) ≤ -(26274364758818529627057 / 10000000000000000000000)

theorem Zeta5Irrational.U_217_8 : Uω (aρ 8) (bρ 8) (4160334912147 / 25600000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_217_9 : Uω (aρ 9) (bρ 9) (4160334912147 / 25600000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_217_10 : Uω (aρ 10) (bρ 10) (4160334912147 / 25600000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_217_11 : Uω (aρ 11) (bρ 11) (4160334912147 / 25600000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_217_12 : Uω (aρ 12) (bρ 12) (4160334912147 / 25600000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_217_13 : Uω (aρ 13) (bρ 13) (4160334912147 / 25600000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_217_14 : Uω (aρ 14) (bρ 14) (4160334912147 / 25600000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_217_15 : Uω (aρ 15) (bρ 15) (4160334912147 / 25600000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_217_16 : Uω (aρ 16) (bρ 16) (4160334912147 / 25600000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_217 : Uρ (4160334912147 / 25600000000000) ≤ -(4196966798483047930983 / 2000000000000000000000)

theorem Zeta5Irrational.U_218_1 : Uω (aρ 1) (bρ 1) (10429227298003 / 64000000000000) ≤ -(18547208385266200982007 / 10000000000000000000000)

theorem Zeta5Irrational.U_218_2 : Uω (aρ 2) (bρ 2) (10429227298003 / 64000000000000) ≤ -(3740810840944483037073 / 2000000000000000000000)

theorem Zeta5Irrational.U_218_3 : Uω (aρ 3) (bρ 3) (10429227298003 / 64000000000000) ≤ -(19028535752517117294929 / 10000000000000000000000)

theorem Zeta5Irrational.U_218_4 : Uω (aρ 4) (bρ 4) (10429227298003 / 64000000000000) ≤ -(19603161049574197177753 / 10000000000000000000000)

theorem Zeta5Irrational.U_218_5 : Uω (aρ 5) (bρ 5) (10429227298003 / 64000000000000) ≤ -(4116830991103902289863 / 2000000000000000000000)

theorem Zeta5Irrational.U_218_6 : Uω (aρ 6) (bρ 6) (10429227298003 / 64000000000000) ≤ -(2790166356911144784423 / 1250000000000000000000)

theorem Zeta5Irrational.U_218_7 : Uω (aρ 7) (bρ 7) (10429227298003 / 64000000000000) ≤ -(2619324694814019901359 / 1000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_218 : Uρ (10429227298003 / 64000000000000) ≤ -(20967778577491089068771 / 10000000000000000000000)

theorem Zeta5Irrational.U_219_1 : Uω (aρ 1) (bρ 1) (20915234631277 / 128000000000000) ≤ -(4629725336005811571373 / 2500000000000000000000)

theorem Zeta5Irrational.U_219_2 : Uω (aρ 2) (bρ 2) (20915234631277 / 128000000000000) ≤ -(2334411176211178011403 / 1250000000000000000000)

theorem Zeta5Irrational.U_219_3 : Uω (aρ 3) (bρ 3) (20915234631277 / 128000000000000) ≤ -(18998787665759244029903 / 10000000000000000000000)

theorem Zeta5Irrational.U_219_4 : Uω (aρ 4) (bρ 4) (20915234631277 / 128000000000000) ≤ -(19571541444456643283281 / 10000000000000000000000)

theorem Zeta5Irrational.U_219_5 : Uω (aρ 5) (bρ 5) (20915234631277 / 128000000000000) ≤ -(821955714717225692007 / 400000000000000000000)

theorem Zeta5Irrational.U_219_6 : Uω (aρ 6) (bρ 6) (20915234631277 / 128000000000000) ≤ -(44555534812667741173 / 20000000000000000000)

theorem Zeta5Irrational.U_219_7 : Uω (aρ 7) (bρ 7) (20915234631277 / 128000000000000) ≤ -(13056599216528297659903 / 5000000000000000000000)

theorem Zeta5Irrational.U_219_8 : Uω (aρ 8) (bρ 8) (20915234631277 / 128000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_219_9 : Uω (aρ 9) (bρ 9) (20915234631277 / 128000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_219_10 : Uω (aρ 10) (bρ 10) (20915234631277 / 128000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_219_11 : Uω (aρ 11) (bρ 11) (20915234631277 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_219_12 : Uω (aρ 12) (bρ 12) (20915234631277 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_219_13 : Uω (aρ 13) (bρ 13) (20915234631277 / 128000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_219_14 : Uω (aρ 14) (bρ 14) (20915234631277 / 128000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_219_15 : Uω (aρ 15) (bρ 15) (20915234631277 / 128000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_219_16 : Uω (aρ 16) (bρ 16) (20915234631277 / 128000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_219 : Uρ (20915234631277 / 128000000000000) ≤ -(20950852552191954841159 / 10000000000000000000000)