Certified arcsine potential bounds (U51)

theorem Zeta5Irrational.U_616_1 : Uω (aρ 1) (bρ 1) (11489045952349 / 16000000000000) ≤ -(106318913346585029177 / 312500000000000000000)

theorem Zeta5Irrational.U_616_2 : Uω (aρ 2) (bρ 2) (11489045952349 / 16000000000000) ≤ -(3435841602808840498403 / 10000000000000000000000)

theorem Zeta5Irrational.U_616_3 : Uω (aρ 3) (bρ 3) (11489045952349 / 16000000000000) ≤ -(3503427083001394159311 / 10000000000000000000000)

theorem Zeta5Irrational.U_616_4 : Uω (aρ 4) (bρ 4) (11489045952349 / 16000000000000) ≤ -(904151680374748223911 / 2500000000000000000000)

theorem Zeta5Irrational.U_616_5 : Uω (aρ 5) (bρ 5) (11489045952349 / 16000000000000) ≤ -(3791226089629521932043 / 10000000000000000000000)

theorem Zeta5Irrational.U_616_6 : Uω (aρ 6) (bρ 6) (11489045952349 / 16000000000000) ≤ -(202327453614113887511 / 500000000000000000000)

theorem Zeta5Irrational.U_616_7 : Uω (aρ 7) (bρ 7) (11489045952349 / 16000000000000) ≤ -(2202253901422898501509 / 5000000000000000000000)

theorem Zeta5Irrational.U_616_8 : Uω (aρ 8) (bρ 8) (11489045952349 / 16000000000000) ≤ -(4889116153186919824119 / 10000000000000000000000)

theorem Zeta5Irrational.U_616_9 : Uω (aρ 9) (bρ 9) (11489045952349 / 16000000000000) ≤ -(1105240842738283865227 / 2000000000000000000000)

theorem Zeta5Irrational.U_616_10 : Uω (aρ 10) (bρ 10) (11489045952349 / 16000000000000) ≤ -(6343775738609869476143 / 10000000000000000000000)

theorem Zeta5Irrational.U_616_11 : Uω (aρ 11) (bρ 11) (11489045952349 / 16000000000000) ≤ -(3686848114669659335923 / 5000000000000000000000)

theorem Zeta5Irrational.U_616_12 : Uω (aρ 12) (bρ 12) (11489045952349 / 16000000000000) ≤ -(4328354908750573873291 / 5000000000000000000000)

theorem Zeta5Irrational.U_616_13 : Uω (aρ 13) (bρ 13) (11489045952349 / 16000000000000) ≤ -(10258168058087591677167 / 10000000000000000000000)

theorem Zeta5Irrational.U_616_14 : Uω (aρ 14) (bρ 14) (11489045952349 / 16000000000000) ≤ -(6167965695391489451341 / 5000000000000000000000)

theorem Zeta5Irrational.U_616_15 : Uω (aρ 15) (bρ 15) (11489045952349 / 16000000000000) ≤ -(16171439084303750819383 / 10000000000000000000000)

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

theorem Zeta5Irrational.U_616 : Uρ (11489045952349 / 16000000000000) ≤ -(292500798363171186281 / 500000000000000000000)

theorem Zeta5Irrational.U_617_1 : Uω (aρ 1) (bρ 1) (4601713724651 / 6400000000000) ≤ -(847207624102700801571 / 2500000000000000000000)

theorem Zeta5Irrational.U_617_2 : Uω (aρ 2) (bρ 2) (4601713724651 / 6400000000000) ≤ -(3422421599130554510801 / 10000000000000000000000)

theorem Zeta5Irrational.U_617_3 : Uω (aρ 3) (bρ 3) (4601713724651 / 6400000000000) ≤ -(109059856659853529079 / 312500000000000000000)

theorem Zeta5Irrational.U_617_4 : Uω (aρ 4) (bρ 4) (4601713724651 / 6400000000000) ≤ -(3602939422167406557651 / 10000000000000000000000)

theorem Zeta5Irrational.U_617_5 : Uω (aρ 5) (bρ 5) (4601713724651 / 6400000000000) ≤ -(1888656661307937322841 / 5000000000000000000000)

theorem Zeta5Irrational.U_617_6 : Uω (aρ 6) (bρ 6) (4601713724651 / 6400000000000) ≤ -(1008066302970724523623 / 2500000000000000000000)

theorem Zeta5Irrational.U_617_7 : Uω (aρ 7) (bρ 7) (4601713724651 / 6400000000000) ≤ -(1097419455511665411643 / 2500000000000000000000)

theorem Zeta5Irrational.U_617_8 : Uω (aρ 8) (bρ 8) (4601713724651 / 6400000000000) ≤ -(2436747227048758859281 / 5000000000000000000000)

theorem Zeta5Irrational.U_617_9 : Uω (aρ 9) (bρ 9) (4601713724651 / 6400000000000) ≤ -(1377359600808868290677 / 2500000000000000000000)

theorem Zeta5Irrational.U_617_10 : Uω (aρ 10) (bρ 10) (4601713724651 / 6400000000000) ≤ -(158133477903931247259 / 250000000000000000000)

theorem Zeta5Irrational.U_617_11 : Uω (aρ 11) (bρ 11) (4601713724651 / 6400000000000) ≤ -(3676374418941192739521 / 5000000000000000000000)

theorem Zeta5Irrational.U_617_12 : Uω (aρ 12) (bρ 12) (4601713724651 / 6400000000000) ≤ -(431588493602501169943 / 500000000000000000000)

theorem Zeta5Irrational.U_617_13 : Uω (aρ 13) (bρ 13) (4601713724651 / 6400000000000) ≤ -(10226142048473857112987 / 10000000000000000000000)

theorem Zeta5Irrational.U_617_14 : Uω (aρ 14) (bρ 14) (4601713724651 / 6400000000000) ≤ -(12287712213345314582721 / 10000000000000000000000)

theorem Zeta5Irrational.U_617_15 : Uω (aρ 15) (bρ 15) (4601713724651 / 6400000000000) ≤ -(15939995460286118426859 / 10000000000000000000000)

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

theorem Zeta5Irrational.U_617 : Uρ (4601713724651 / 6400000000000) ≤ -(728229669929658414691 / 1250000000000000000000)

theorem Zeta5Irrational.U_618_1 : Uω (aρ 1) (bρ 1) (5759761335453 / 8000000000000) ≤ -(337547363029600780631 / 1000000000000000000000)

theorem Zeta5Irrational.U_618_2 : Uω (aρ 2) (bρ 2) (5759761335453 / 8000000000000) ≤ -(3409019581723940330361 / 10000000000000000000000)

theorem Zeta5Irrational.U_618_3 : Uω (aρ 3) (bρ 3) (5759761335453 / 8000000000000) ≤ -(173821098891361459987 / 500000000000000000000)

theorem Zeta5Irrational.U_618_4 : Uω (aρ 4) (bρ 4) (5759761335453 / 8000000000000) ≤ -(179464539245497928923 / 500000000000000000000)

theorem Zeta5Irrational.U_618_5 : Uω (aρ 5) (bρ 5) (5759761335453 / 8000000000000) ≤ -(940854976778895516571 / 2500000000000000000000)

theorem Zeta5Irrational.U_618_6 : Uω (aρ 6) (bρ 6) (5759761335453 / 8000000000000) ≤ -(803600356250984112259 / 2000000000000000000000)

theorem Zeta5Irrational.U_618_7 : Uω (aρ 7) (bρ 7) (5759761335453 / 8000000000000) ≤ -(2187434969384649431987 / 5000000000000000000000)

theorem Zeta5Irrational.U_618_8 : Uω (aρ 8) (bρ 8) (5759761335453 / 8000000000000) ≤ -(1214474362038736148431 / 2500000000000000000000)

theorem Zeta5Irrational.U_618_9 : Uω (aρ 9) (bρ 9) (5759761335453 / 8000000000000) ≤ -(1373175357305435607103 / 2500000000000000000000)

theorem Zeta5Irrational.U_618_10 : Uω (aρ 10) (bρ 10) (5759761335453 / 8000000000000) ≤ -(3153469138497098411407 / 5000000000000000000000)

theorem Zeta5Irrational.U_618_11 : Uω (aρ 11) (bρ 11) (5759761335453 / 8000000000000) ≤ -(7331849876332865554959 / 10000000000000000000000)

theorem Zeta5Irrational.U_618_12 : Uω (aρ 12) (bρ 12) (5759761335453 / 8000000000000) ≤ -(8606904707458635042521 / 10000000000000000000000)

theorem Zeta5Irrational.U_618_13 : Uω (aρ 13) (bρ 13) (5759761335453 / 8000000000000) ≤ -(2038852069256468634701 / 2000000000000000000000)

theorem Zeta5Irrational.U_618_14 : Uω (aρ 14) (bρ 14) (5759761335453 / 8000000000000) ≤ -(3059985522729845712219 / 2500000000000000000000)

theorem Zeta5Irrational.U_618_15 : Uω (aρ 15) (bρ 15) (5759761335453 / 8000000000000) ≤ -(15745009285213127229491 / 10000000000000000000000)

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

theorem Zeta5Irrational.U_618 : Uρ (5759761335453 / 8000000000000) ≤ -(580282206778786842289 / 1000000000000000000000)

theorem Zeta5Irrational.U_619_1 : Uω (aρ 1) (bρ 1) (23069522060369 / 32000000000000) ≤ -(840533645271613096197 / 2500000000000000000000)

theorem Zeta5Irrational.U_619_2 : Uω (aρ 2) (bρ 2) (23069522060369 / 32000000000000) ≤ -(1697817751219501552147 / 5000000000000000000000)

theorem Zeta5Irrational.U_619_3 : Uω (aρ 3) (bρ 3) (23069522060369 / 32000000000000) ≤ -(3462946727979391038407 / 10000000000000000000000)

theorem Zeta5Irrational.U_619_4 : Uω (aρ 4) (bρ 4) (23069522060369 / 32000000000000) ≤ -(3575660758809798843429 / 10000000000000000000000)

theorem Zeta5Irrational.U_619_5 : Uω (aρ 5) (bρ 5) (23069522060369 / 32000000000000) ≤ -(3749545789310065404481 / 10000000000000000000000)

theorem Zeta5Irrational.U_619_6 : Uω (aρ 6) (bρ 6) (23069522060369 / 32000000000000) ≤ -(4003758721882345394807 / 10000000000000000000000)

theorem Zeta5Irrational.U_619_7 : Uω (aρ 7) (bρ 7) (23069522060369 / 32000000000000) ≤ -(872016817370518790959 / 2000000000000000000000)

theorem Zeta5Irrational.U_619_8 : Uω (aρ 8) (bρ 8) (23069522060369 / 32000000000000) ≤ -(4842325056394238771433 / 10000000000000000000000)

theorem Zeta5Irrational.U_619_9 : Uω (aρ 9) (bρ 9) (23069522060369 / 32000000000000) ≤ -(5475993190011855433897 / 10000000000000000000000)

theorem Zeta5Irrational.U_619_10 : Uω (aρ 10) (bρ 10) (23069522060369 / 32000000000000) ≤ -(6288573075515474583353 / 10000000000000000000000)

theorem Zeta5Irrational.U_619_11 : Uω (aρ 11) (bρ 11) (23069522060369 / 32000000000000) ≤ -(1827749775245038889841 / 2500000000000000000000)

theorem Zeta5Irrational.U_619_12 : Uω (aρ 12) (bρ 12) (23069522060369 / 32000000000000) ≤ -(343284552296869609383 / 400000000000000000000)

theorem Zeta5Irrational.U_619_13 : Uω (aρ 13) (bρ 13) (23069522060369 / 32000000000000) ≤ -(1016252133793236407923 / 1000000000000000000000)

theorem Zeta5Irrational.U_619_14 : Uω (aρ 14) (bρ 14) (23069522060369 / 32000000000000) ≤ -(12192609767079604075557 / 10000000000000000000000)

theorem Zeta5Irrational.U_619_15 : Uω (aρ 15) (bρ 15) (23069522060369 / 32000000000000) ≤ -(3893334229564846221071 / 2500000000000000000000)

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

theorem Zeta5Irrational.U_619 : Uρ (23069522060369 / 32000000000000) ≤ -(5780568999489780155329 / 10000000000000000000000)

theorem Zeta5Irrational.U_620_1 : Uω (aρ 1) (bρ 1) (11549999389463 / 16000000000000) ≤ -(133952532052508978969 / 400000000000000000000)

theorem Zeta5Irrational.U_620_2 : Uω (aρ 2) (bρ 2) (11549999389463 / 16000000000000) ≤ -(3382269313318846887479 / 10000000000000000000000)

theorem Zeta5Irrational.U_620_3 : Uω (aρ 3) (bρ 3) (11549999389463 / 16000000000000) ≤ -(1724744807306295194459 / 5000000000000000000000)

theorem Zeta5Irrational.U_620_4 : Uω (aρ 4) (bρ 4) (11549999389463 / 16000000000000) ≤ -(1781024646579131442769 / 5000000000000000000000)

theorem Zeta5Irrational.U_620_5 : Uω (aρ 5) (bρ 5) (11549999389463 / 16000000000000) ≤ -(233480682225324909683 / 625000000000000000000)

theorem Zeta5Irrational.U_620_6 : Uω (aρ 6) (bρ 6) (11549999389463 / 16000000000000) ≤ -(124672999234403041657 / 312500000000000000000)

theorem Zeta5Irrational.U_620_7 : Uω (aρ 7) (bρ 7) (11549999389463 / 16000000000000) ≤ -(543165025054239187137 / 1250000000000000000000)

theorem Zeta5Irrational.U_620_8 : Uω (aρ 8) (bρ 8) (11549999389463 / 16000000000000) ≤ -(2413388600116685197157 / 5000000000000000000000)

theorem Zeta5Irrational.U_620_9 : Uω (aρ 9) (bρ 9) (11549999389463 / 16000000000000) ≤ -(1364828396129223884731 / 2500000000000000000000)

theorem Zeta5Irrational.U_620_10 : Uω (aρ 10) (bρ 10) (11549999389463 / 16000000000000) ≤ -(3135121683520498290713 / 5000000000000000000000)

theorem Zeta5Irrational.U_620_11 : Uω (aρ 11) (bρ 11) (11549999389463 / 16000000000000) ≤ -(3645098135037624419509 / 5000000000000000000000)

theorem Zeta5Irrational.U_620_12 : Uω (aρ 12) (bρ 12) (11549999389463 / 16000000000000) ≤ -(8557396661480946125929 / 10000000000000000000000)

theorem Zeta5Irrational.U_620_13 : Uω (aρ 13) (bρ 13) (11549999389463 / 16000000000000) ≤ -(506546171996047407941 / 500000000000000000000)

theorem Zeta5Irrational.U_620_14 : Uω (aρ 14) (bρ 14) (11549999389463 / 16000000000000) ≤ -(12145704453235629212067 / 10000000000000000000000)

theorem Zeta5Irrational.U_620_15 : Uω (aρ 15) (bρ 15) (11549999389463 / 16000000000000) ≤ -(15418235905060781715109 / 10000000000000000000000)

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

theorem Zeta5Irrational.U_620 : Uρ (11549999389463 / 16000000000000) ≤ -(71985901044622510087 / 125000000000000000000)

theorem Zeta5Irrational.U_621_1 : Uω (aρ 1) (bρ 1) (23130475497483 / 32000000000000) ≤ -(667101948738974140143 / 2000000000000000000000)

theorem Zeta5Irrational.U_621_2 : Uω (aρ 2) (bρ 2) (23130475497483 / 32000000000000) ≤ -(3368920966598643556611 / 10000000000000000000000)

theorem Zeta5Irrational.U_621_3 : Uω (aρ 3) (bρ 3) (23130475497483 / 32000000000000) ≤ -(214753161810318558973 / 625000000000000000000)

theorem Zeta5Irrational.U_621_4 : Uω (aρ 4) (bρ 4) (23130475497483 / 32000000000000) ≤ -(709691267490747128891 / 2000000000000000000000)

theorem Zeta5Irrational.U_621_5 : Uω (aρ 5) (bρ 5) (23130475497483 / 32000000000000) ≤ -(3721855232630060188191 / 10000000000000000000000)

theorem Zeta5Irrational.U_621_6 : Uω (aρ 6) (bρ 6) (23130475497483 / 32000000000000) ≤ -(1987666742048291147841 / 5000000000000000000000)

theorem Zeta5Irrational.U_621_7 : Uω (aρ 7) (bρ 7) (23130475497483 / 32000000000000) ≤ -(4330578213947306030187 / 10000000000000000000000)

theorem Zeta5Irrational.U_621_8 : Uω (aρ 8) (bρ 8) (23130475497483 / 32000000000000) ≤ -(4811253801470739519341 / 10000000000000000000000)

theorem Zeta5Irrational.U_621_9 : Uω (aρ 9) (bρ 9) (23130475497483 / 32000000000000) ≤ -(1360665628048339499749 / 2500000000000000000000)

theorem Zeta5Irrational.U_621_10 : Uω (aρ 10) (bρ 10) (23130475497483 / 32000000000000) ≤ -(1562987251951932787287 / 2500000000000000000000)

theorem Zeta5Irrational.U_621_11 : Uω (aρ 11) (bρ 11) (23130475497483 / 32000000000000) ≤ -(726944114380871616587 / 1000000000000000000000)

theorem Zeta5Irrational.U_621_12 : Uω (aρ 12) (bρ 12) (23130475497483 / 32000000000000) ≤ -(8532752764931727160707 / 10000000000000000000000)

theorem Zeta5Irrational.U_621_13 : Uω (aρ 13) (bρ 13) (23130475497483 / 32000000000000) ≤ -(5049732549018707484119 / 5000000000000000000000)

theorem Zeta5Irrational.U_621_14 : Uω (aρ 14) (bρ 14) (23130475497483 / 32000000000000) ≤ -(12099215801753549008383 / 10000000000000000000000)

theorem Zeta5Irrational.U_621_15 : Uω (aρ 15) (bρ 15) (23130475497483 / 32000000000000) ≤ -(1909462497718683193977 / 1250000000000000000000)

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

theorem Zeta5Irrational.U_621 : Uρ (23130475497483 / 32000000000000) ≤ -(1147521724675301463431 / 2000000000000000000000)

theorem Zeta5Irrational.U_622_1 : Uω (aρ 1) (bρ 1) (579023805401 / 800000000000) ≤ -(664444772228277286747 / 2000000000000000000000)

theorem Zeta5Irrational.U_622_2 : Uω (aρ 2) (bρ 2) (579023805401 / 800000000000) ≤ -(1677795207352304648309 / 5000000000000000000000)

theorem Zeta5Irrational.U_622_3 : Uω (aρ 3) (bρ 3) (579023805401 / 800000000000) ≤ -(3422629602471597769299 / 10000000000000000000000)

theorem Zeta5Irrational.U_622_4 : Uω (aρ 4) (bρ 4) (579023805401 / 800000000000) ≤ -(17674409207002628977 / 50000000000000000000)

theorem Zeta5Irrational.U_622_5 : Uω (aρ 5) (bρ 5) (579023805401 / 800000000000) ≤ -(23175241795223090519 / 62500000000000000000)

theorem Zeta5Irrational.U_622_6 : Uω (aρ 6) (bρ 6) (579023805401 / 800000000000) ≤ -(1980575594952124207391 / 5000000000000000000000)

theorem Zeta5Irrational.U_622_7 : Uω (aρ 7) (bρ 7) (579023805401 / 800000000000) ≤ -(4315858062121709975551 / 10000000000000000000000)

theorem Zeta5Irrational.U_622_8 : Uω (aρ 8) (bρ 8) (579023805401 / 800000000000) ≤ -(119893869557067372297 / 250000000000000000000)

theorem Zeta5Irrational.U_622_9 : Uω (aρ 9) (bρ 9) (579023805401 / 800000000000) ≤ -(5426039873039151492967 / 10000000000000000000000)

theorem Zeta5Irrational.U_622_10 : Uω (aρ 10) (bρ 10) (579023805401 / 800000000000) ≤ -(6233689854961697792241 / 10000000000000000000000)

theorem Zeta5Irrational.U_622_11 : Uω (aρ 11) (bρ 11) (579023805401 / 800000000000) ≤ -(906091685536126654847 / 1250000000000000000000)

theorem Zeta5Irrational.U_622_12 : Uω (aρ 12) (bρ 12) (579023805401 / 800000000000) ≤ -(1063522702341544572123 / 1250000000000000000000)

theorem Zeta5Irrational.U_622_13 : Uω (aρ 13) (bρ 13) (579023805401 / 800000000000) ≤ -(10068144786604213098637 / 10000000000000000000000)

theorem Zeta5Irrational.U_622_14 : Uω (aρ 14) (bρ 14) (579023805401 / 800000000000) ≤ -(753320867564564560021 / 625000000000000000000)

theorem Zeta5Irrational.U_622_15 : Uω (aρ 15) (bρ 15) (579023805401 / 800000000000) ≤ -(15143118237455441992627 / 10000000000000000000000)

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

theorem Zeta5Irrational.U_622 : Uρ (579023805401 / 800000000000) ≤ -(1429174612416460317899 / 2500000000000000000000)

theorem Zeta5Irrational.U_623_1 : Uω (aρ 1) (bρ 1) (23191428934597 / 32000000000000) ≤ -(3308955606748218408403 / 10000000000000000000000)

theorem Zeta5Irrational.U_623_2 : Uω (aρ 2) (bρ 2) (23191428934597 / 32000000000000) ≤ -(835569402563246451051 / 2500000000000000000000)

theorem Zeta5Irrational.U_623_3 : Uω (aρ 3) (bρ 3) (23191428934597 / 32000000000000) ≤ -(3409226606762139118281 / 10000000000000000000000)

theorem Zeta5Irrational.U_623_4 : Uω (aρ 4) (bρ 4) (23191428934597 / 32000000000000) ≤ -(3521325754907749846863 / 10000000000000000000000)

theorem Zeta5Irrational.U_623_5 : Uω (aρ 5) (bρ 5) (23191428934597 / 32000000000000) ≤ -(461780153311734872569 / 1250000000000000000000)

theorem Zeta5Irrational.U_623_6 : Uω (aρ 6) (bρ 6) (23191428934597 / 32000000000000) ≤ -(3946989035406164734171 / 10000000000000000000000)

theorem Zeta5Irrational.U_623_7 : Uω (aρ 7) (bρ 7) (23191428934597 / 32000000000000) ≤ -(4301159679979176426909 / 10000000000000000000000)

theorem Zeta5Irrational.U_623_8 : Uω (aρ 8) (bρ 8) (23191428934597 / 32000000000000) ≤ -(4780280065221076428117 / 10000000000000000000000)

theorem Zeta5Irrational.U_623_9 : Uω (aρ 9) (bρ 9) (23191428934597 / 32000000000000) ≤ -(5409445567589630971793 / 10000000000000000000000)

theorem Zeta5Irrational.U_623_10 : Uω (aρ 10) (bρ 10) (23191428934597 / 32000000000000) ≤ -(6215465766550052784111 / 10000000000000000000000)

theorem Zeta5Irrational.U_623_11 : Uω (aρ 11) (bρ 11) (23191428934597 / 32000000000000) ≤ -(903509131940136337699 / 1250000000000000000000)

theorem Zeta5Irrational.U_623_12 : Uω (aρ 12) (bρ 12) (23191428934597 / 32000000000000) ≤ -(848368272941469264369 / 1000000000000000000000)

theorem Zeta5Irrational.U_623_13 : Uω (aρ 13) (bρ 13) (23191428934597 / 32000000000000) ≤ -(5018480503871485516127 / 5000000000000000000000)

theorem Zeta5Irrational.U_623_14 : Uω (aρ 14) (bρ 14) (23191428934597 / 32000000000000) ≤ -(12007449152369101586589 / 10000000000000000000000)

theorem Zeta5Irrational.U_623_15 : Uω (aρ 15) (bρ 15) (23191428934597 / 32000000000000) ≤ -(15018676704649794032253 / 10000000000000000000000)

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

theorem Zeta5Irrational.U_623 : Uρ (23191428934597 / 32000000000000) ≤ -(5696085690247323872273 / 10000000000000000000000)

theorem Zeta5Irrational.U_624_1 : Uω (aρ 1) (bρ 1) (11610952826577 / 16000000000000) ≤ -(3295704933797769085771 / 10000000000000000000000)

theorem Zeta5Irrational.U_624_2 : Uω (aρ 2) (bρ 2) (11610952826577 / 16000000000000) ≤ -(665796501209805653239 / 2000000000000000000000)

theorem Zeta5Irrational.U_624_3 : Uω (aρ 3) (bρ 3) (11610952826577 / 16000000000000) ≤ -(3395841553661085159127 / 10000000000000000000000)

theorem Zeta5Irrational.U_624_4 : Uω (aρ 4) (bρ 4) (11610952826577 / 16000000000000) ≤ -(3507788028088219534127 / 10000000000000000000000)

theorem Zeta5Irrational.U_624_5 : Uω (aρ 5) (bρ 5) (11610952826577 / 16000000000000) ≤ -(3680462797695905282609 / 10000000000000000000000)

theorem Zeta5Irrational.U_624_6 : Uω (aρ 6) (bρ 6) (11610952826577 / 16000000000000) ≤ -(1966423481665302052459 / 5000000000000000000000)

theorem Zeta5Irrational.U_624_7 : Uω (aρ 7) (bρ 7) (11610952826577 / 16000000000000) ≤ -(2143241501416554488787 / 5000000000000000000000)

theorem Zeta5Irrational.U_624_8 : Uω (aρ 8) (bρ 8) (11610952826577 / 16000000000000) ≤ -(4764829573210770707701 / 10000000000000000000000)

theorem Zeta5Irrational.U_624_9 : Uω (aρ 9) (bρ 9) (11610952826577 / 16000000000000) ≤ -(5392879496913676081697 / 10000000000000000000000)

theorem Zeta5Irrational.U_624_10 : Uω (aρ 10) (bρ 10) (11610952826577 / 16000000000000) ≤ -(1549319150378315990693 / 2500000000000000000000)

theorem Zeta5Irrational.U_624_11 : Uω (aρ 11) (bρ 11) (11610952826577 / 16000000000000) ≤ -(7207459623385319839303 / 10000000000000000000000)

theorem Zeta5Irrational.U_624_12 : Uω (aρ 12) (bρ 12) (11610952826577 / 16000000000000) ≤ -(1691851121799353991287 / 2000000000000000000000)

theorem Zeta5Irrational.U_624_13 : Uω (aρ 13) (bρ 13) (11610952826577 / 16000000000000) ≤ -(2501478072666182089101 / 2500000000000000000000)

theorem Zeta5Irrational.U_624_14 : Uω (aρ 14) (bρ 14) (11610952826577 / 16000000000000) ≤ -(11962152448444704526753 / 10000000000000000000000)

theorem Zeta5Irrational.U_624_15 : Uω (aρ 15) (bρ 15) (11610952826577 / 16000000000000) ≤ -(14901054336295950917693 / 10000000000000000000000)

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

theorem Zeta5Irrational.U_624 : Uρ (11610952826577 / 16000000000000) ≤ -(2837864753785064472951 / 5000000000000000000000)

theorem Zeta5Irrational.U_625_1 : Uω (aρ 1) (bρ 1) (23252382371711 / 32000000000000) ≤ -(3282471795757911769263 / 10000000000000000000000)

theorem Zeta5Irrational.U_625_2 : Uω (aρ 2) (bρ 2) (23252382371711 / 32000000000000) ≤ -(1657852527543002467351 / 5000000000000000000000)

theorem Zeta5Irrational.U_625_3 : Uω (aρ 3) (bρ 3) (23252382371711 / 32000000000000) ≤ -(845618598796519162513 / 2500000000000000000000)

theorem Zeta5Irrational.U_625_4 : Uω (aρ 4) (bρ 4) (23252382371711 / 32000000000000) ≤ -(3494268611257336033207 / 10000000000000000000000)

theorem Zeta5Irrational.U_625_5 : Uω (aρ 5) (bρ 5) (23252382371711 / 32000000000000) ≤ -(458337918543920478139 / 1250000000000000000000)

theorem Zeta5Irrational.U_625_6 : Uω (aρ 6) (bρ 6) (23252382371711 / 32000000000000) ≤ -(3918724916650439724693 / 10000000000000000000000)

theorem Zeta5Irrational.U_625_7 : Uω (aρ 7) (bρ 7) (23252382371711 / 32000000000000) ≤ -(4271827966286515829487 / 10000000000000000000000)

theorem Zeta5Irrational.U_625_8 : Uω (aρ 8) (bρ 8) (23252382371711 / 32000000000000) ≤ -(2374701614773647720401 / 5000000000000000000000)

theorem Zeta5Irrational.U_625_9 : Uω (aρ 9) (bρ 9) (23252382371711 / 32000000000000) ≤ -(5376341562609795843151 / 10000000000000000000000)

theorem Zeta5Irrational.U_625_10 : Uω (aρ 10) (bρ 10) (23252382371711 / 32000000000000) ≤ -(6179122219677369954149 / 10000000000000000000000)

theorem Zeta5Irrational.U_625_11 : Uω (aρ 11) (bρ 11) (23252382371711 / 32000000000000) ≤ -(7186892955616715097121 / 10000000000000000000000)

theorem Zeta5Irrational.U_625_12 : Uω (aρ 12) (bρ 12) (23252382371711 / 32000000000000) ≤ -(8434899774897159942441 / 10000000000000000000000)

theorem Zeta5Irrational.U_625_13 : Uω (aρ 13) (bρ 13) (23252382371711 / 32000000000000) ≤ -(2493749297745844288991 / 2500000000000000000000)

theorem Zeta5Irrational.U_625_14 : Uω (aρ 14) (bρ 14) (23252382371711 / 32000000000000) ≤ -(11917234953315698604143 / 10000000000000000000000)

theorem Zeta5Irrational.U_625_15 : Uω (aρ 15) (bρ 15) (23252382371711 / 32000000000000) ≤ -(739462680758528667917 / 500000000000000000000)

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

theorem Zeta5Irrational.U_625 : Uρ (23252382371711 / 32000000000000) ≤ -(1413899734414673350401 / 2500000000000000000000)

theorem Zeta5Irrational.U_626_1 : Uω (aρ 1) (bρ 1) (5820714772567 / 8000000000000) ≤ -(3269256146281007372917 / 10000000000000000000000)

theorem Zeta5Irrational.U_626_2 : Uω (aρ 2) (bρ 2) (5820714772567 / 8000000000000) ≤ -(3302445210544198461269 / 10000000000000000000000)

theorem Zeta5Irrational.U_626_3 : Uω (aρ 3) (bρ 3) (5820714772567 / 8000000000000) ≤ -(842281270886748966641 / 2500000000000000000000)

theorem Zeta5Irrational.U_626_4 : Uω (aρ 4) (bρ 4) (5820714772567 / 8000000000000) ≤ -(3480767454931998022547 / 10000000000000000000000)

theorem Zeta5Irrational.U_626_5 : Uω (aρ 5) (bρ 5) (5820714772567 / 8000000000000) ≤ -(3652962826186939902803 / 10000000000000000000000)

theorem Zeta5Irrational.U_626_6 : Uω (aρ 6) (bρ 6) (5820714772567 / 8000000000000) ≤ -(1952311419290875189301 / 5000000000000000000000)

theorem Zeta5Irrational.U_626_7 : Uω (aρ 7) (bρ 7) (5820714772567 / 8000000000000) ≤ -(4257194506230267187757 / 10000000000000000000000)

theorem Zeta5Irrational.U_626_8 : Uω (aρ 8) (bρ 8) (5820714772567 / 8000000000000) ≤ -(4734000957894396568091 / 10000000000000000000000)

theorem Zeta5Irrational.U_626_9 : Uω (aρ 9) (bρ 9) (5820714772567 / 8000000000000) ≤ -(2679915833401137352107 / 5000000000000000000000)

theorem Zeta5Irrational.U_626_10 : Uω (aρ 10) (bρ 10) (5820714772567 / 8000000000000) ≤ -(6161002481746330224137 / 10000000000000000000000)

theorem Zeta5Irrational.U_626_11 : Uω (aρ 11) (bρ 11) (5820714772567 / 8000000000000) ≤ -(7166372821784453306367 / 10000000000000000000000)

theorem Zeta5Irrational.U_626_12 : Uω (aρ 12) (bρ 12) (5820714772567 / 8000000000000) ≤ -(4205307374925527529399 / 5000000000000000000000)

theorem Zeta5Irrational.U_626_13 : Uω (aρ 13) (bρ 13) (5820714772567 / 8000000000000) ≤ -(497210714502570725607 / 500000000000000000000)

theorem Zeta5Irrational.U_626_14 : Uω (aρ 14) (bρ 14) (5820714772567 / 8000000000000) ≤ -(5936344091881768530959 / 5000000000000000000000)

theorem Zeta5Irrational.U_626_15 : Uω (aρ 15) (bρ 15) (5820714772567 / 8000000000000) ≤ -(14682499387665634183519 / 10000000000000000000000)

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

theorem Zeta5Irrational.U_626 : Uρ (5820714772567 / 8000000000000) ≤ -(5635669807423770572593 / 10000000000000000000000)

theorem Zeta5Irrational.U_627_1 : Uω (aρ 1) (bρ 1) (932533432353 / 1280000000000) ≤ -(3256057939202933221281 / 10000000000000000000000)

theorem Zeta5Irrational.U_627_2 : Uω (aρ 2) (bρ 2) (932533432353 / 1280000000000) ≤ -(3289202925789912456111 / 10000000000000000000000)

theorem Zeta5Irrational.U_627_3 : Uω (aρ 3) (bρ 3) (932533432353 / 1280000000000) ≤ -(671158714228988945661 / 2000000000000000000000)

theorem Zeta5Irrational.U_627_4 : Uω (aρ 4) (bρ 4) (932533432353 / 1280000000000) ≤ -(3467284509829511449131 / 10000000000000000000000)

theorem Zeta5Irrational.U_627_5 : Uω (aρ 5) (bρ 5) (932533432353 / 1280000000000) ≤ -(1819620589572607906299 / 5000000000000000000000)

theorem Zeta5Irrational.U_627_6 : Uω (aρ 6) (bρ 6) (932533432353 / 1280000000000) ≤ -(243158792036402207847 / 625000000000000000000)

theorem Zeta5Irrational.U_627_7 : Uω (aρ 7) (bρ 7) (932533432353 / 1280000000000) ≤ -(4242582558841379302559 / 10000000000000000000000)

theorem Zeta5Irrational.U_627_8 : Uω (aρ 8) (bρ 8) (932533432353 / 1280000000000) ≤ -(4718622682281668301957 / 10000000000000000000000)

theorem Zeta5Irrational.U_627_9 : Uω (aρ 9) (bρ 9) (932533432353 / 1280000000000) ≤ -(2671674856068678912033 / 5000000000000000000000)

theorem Zeta5Irrational.U_627_10 : Uω (aρ 10) (bρ 10) (932533432353 / 1280000000000) ≤ -(1535729312323613446291 / 2500000000000000000000)

theorem Zeta5Irrational.U_627_11 : Uω (aρ 11) (bρ 11) (932533432353 / 1280000000000) ≤ -(3572949496635842197997 / 5000000000000000000000)

theorem Zeta5Irrational.U_627_12 : Uω (aρ 12) (bρ 12) (932533432353 / 1280000000000) ≤ -(262075001932125642291 / 312500000000000000000)

theorem Zeta5Irrational.U_627_13 : Uω (aρ 13) (bρ 13) (932533432353 / 1280000000000) ≤ -(2478390548579272769413 / 2500000000000000000000)

theorem Zeta5Irrational.U_627_14 : Uω (aρ 14) (bρ 14) (932533432353 / 1280000000000) ≤ -(11828503971903031566869 / 10000000000000000000000)

theorem Zeta5Irrational.U_627_15 : Uω (aρ 15) (bρ 15) (932533432353 / 1280000000000) ≤ -(1458017506958502499819 / 1000000000000000000000)

theorem Zeta5Irrational.U_627_16 : Uω (aρ 16) (bρ 16) (932533432353 / 1280000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_627 : Uρ (932533432353 / 1280000000000) ≤ -(5615922790488704981441 / 10000000000000000000000)