Certified arcsine potential bounds (U40)

theorem Zeta5Irrational.U_484_1 : Uω (aρ 1) (bρ 1) (17216962626667 / 32000000000000) ≤ -(49367704558822225637 / 78125000000000000000)

theorem Zeta5Irrational.U_484_2 : Uω (aρ 2) (bρ 2) (17216962626667 / 32000000000000) ≤ -(3182100974805846120097 / 5000000000000000000000)

theorem Zeta5Irrational.U_484_3 : Uω (aρ 3) (bρ 3) (17216962626667 / 32000000000000) ≤ -(129102657264926025039 / 200000000000000000000)

theorem Zeta5Irrational.U_484_4 : Uω (aρ 4) (bρ 4) (17216962626667 / 32000000000000) ≤ -(1652035360447789156013 / 2500000000000000000000)

theorem Zeta5Irrational.U_484_5 : Uω (aρ 5) (bρ 5) (17216962626667 / 32000000000000) ≤ -(1369217880496384891111 / 2000000000000000000000)

theorem Zeta5Irrational.U_484_6 : Uω (aρ 6) (bρ 6) (17216962626667 / 32000000000000) ≤ -(3599191382945151200059 / 5000000000000000000000)

theorem Zeta5Irrational.U_484_7 : Uω (aρ 7) (bρ 7) (17216962626667 / 32000000000000) ≤ -(3850961478539558197473 / 5000000000000000000000)

theorem Zeta5Irrational.U_484_8 : Uω (aρ 8) (bρ 8) (17216962626667 / 32000000000000) ≤ -(8404279351985589500927 / 10000000000000000000000)

theorem Zeta5Irrational.U_484_9 : Uω (aρ 9) (bρ 9) (17216962626667 / 32000000000000) ≤ -(4686124003779445722807 / 5000000000000000000000)

theorem Zeta5Irrational.U_484_10 : Uω (aρ 10) (bρ 10) (17216962626667 / 32000000000000) ≤ -(10716342206642952717589 / 10000000000000000000000)

theorem Zeta5Irrational.U_484_11 : Uω (aρ 11) (bρ 11) (17216962626667 / 32000000000000) ≤ -(6340492533616705606711 / 5000000000000000000000)

theorem Zeta5Irrational.U_484_12 : Uω (aρ 12) (bρ 12) (17216962626667 / 32000000000000) ≤ -(8171995575870492649569 / 5000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_484 : Uρ (17216962626667 / 32000000000000) ≤ -(9789045597887444270013 / 10000000000000000000000)

theorem Zeta5Irrational.U_485_1 : Uω (aρ 1) (bρ 1) (68947737388703 / 128000000000000) ≤ -(6307332166479452008709 / 10000000000000000000000)

theorem Zeta5Irrational.U_485_2 : Uω (aρ 2) (bρ 2) (68947737388703 / 128000000000000) ≤ -(6352414503277472699569 / 10000000000000000000000)

theorem Zeta5Irrational.U_485_3 : Uω (aρ 3) (bρ 3) (68947737388703 / 128000000000000) ≤ -(644323666027210507003 / 1000000000000000000000)

theorem Zeta5Irrational.U_485_4 : Uω (aρ 4) (bρ 4) (68947737388703 / 128000000000000) ≤ -(1319211758427744412517 / 2000000000000000000000)

theorem Zeta5Irrational.U_485_5 : Uω (aρ 5) (bρ 5) (68947737388703 / 128000000000000) ≤ -(3416853956054903156221 / 5000000000000000000000)

theorem Zeta5Irrational.U_485_6 : Uω (aρ 6) (bρ 6) (68947737388703 / 128000000000000) ≤ -(1437107561212252026653 / 2000000000000000000000)

theorem Zeta5Irrational.U_485_7 : Uω (aρ 7) (bρ 7) (68947737388703 / 128000000000000) ≤ -(7688368136445735574367 / 10000000000000000000000)

theorem Zeta5Irrational.U_485_8 : Uω (aρ 8) (bρ 8) (68947737388703 / 128000000000000) ≤ -(4194814386260065118497 / 5000000000000000000000)

theorem Zeta5Irrational.U_485_9 : Uω (aρ 9) (bρ 9) (68947737388703 / 128000000000000) ≤ -(9355844753686533661381 / 10000000000000000000000)

theorem Zeta5Irrational.U_485_10 : Uω (aρ 10) (bρ 10) (68947737388703 / 128000000000000) ≤ -(1337111150499449144981 / 1250000000000000000000)

theorem Zeta5Irrational.U_485_11 : Uω (aρ 11) (bρ 11) (68947737388703 / 128000000000000) ≤ -(6327521456465553556581 / 5000000000000000000000)

theorem Zeta5Irrational.U_485_12 : Uω (aρ 12) (bρ 12) (68947737388703 / 128000000000000) ≤ -(407190663593972207153 / 250000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_485 : Uρ (68947737388703 / 128000000000000) ≤ -(4886962101695595637819 / 5000000000000000000000)

theorem Zeta5Irrational.U_486_1 : Uω (aρ 1) (bρ 1) (34513812135369 / 64000000000000) ≤ -(786951487770795011317 / 1250000000000000000000)

theorem Zeta5Irrational.U_486_2 : Uω (aρ 2) (bρ 2) (34513812135369 / 64000000000000) ≤ -(792580117002899229761 / 1250000000000000000000)

theorem Zeta5Irrational.U_486_3 : Uω (aρ 3) (bρ 3) (34513812135369 / 64000000000000) ≤ -(6431354596238415003153 / 10000000000000000000000)

theorem Zeta5Irrational.U_486_4 : Uω (aρ 4) (bρ 4) (34513812135369 / 64000000000000) ≤ -(3291995367689427495473 / 5000000000000000000000)

theorem Zeta5Irrational.U_486_5 : Uω (aρ 5) (bρ 5) (34513812135369 / 64000000000000) ≤ -(1705335441222945381761 / 2500000000000000000000)

theorem Zeta5Irrational.U_486_6 : Uω (aρ 6) (bρ 6) (34513812135369 / 64000000000000) ≤ -(1793177352395991703339 / 2500000000000000000000)

theorem Zeta5Irrational.U_486_7 : Uω (aρ 7) (bρ 7) (34513812135369 / 64000000000000) ≤ -(7674831886757274297583 / 10000000000000000000000)

theorem Zeta5Irrational.U_486_8 : Uω (aρ 8) (bρ 8) (34513812135369 / 64000000000000) ≤ -(837500021158687506521 / 1000000000000000000000)

theorem Zeta5Irrational.U_486_9 : Uω (aρ 9) (bρ 9) (34513812135369 / 64000000000000) ≤ -(29185843712424599397 / 31250000000000000000)

theorem Zeta5Irrational.U_486_10 : Uω (aρ 10) (bρ 10) (34513812135369 / 64000000000000) ≤ -(10677479115380574000047 / 10000000000000000000000)

theorem Zeta5Irrational.U_486_11 : Uω (aρ 11) (bρ 11) (34513812135369 / 64000000000000) ≤ -(2525838139806847648551 / 2000000000000000000000)

theorem Zeta5Irrational.U_486_12 : Uω (aρ 12) (bρ 12) (34513812135369 / 64000000000000) ≤ -(16232050823419908826121 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_486 : Uρ (34513812135369 / 64000000000000) ≤ -(1951775897521726186223 / 2000000000000000000000)

theorem Zeta5Irrational.U_487_1 : Uω (aρ 1) (bρ 1) (69107511152773 / 128000000000000) ≤ -(6283905358389822733931 / 10000000000000000000000)

theorem Zeta5Irrational.U_487_2 : Uω (aρ 2) (bρ 2) (69107511152773 / 128000000000000) ≤ -(6328881215201098496097 / 10000000000000000000000)

theorem Zeta5Irrational.U_487_3 : Uω (aρ 3) (bρ 3) (69107511152773 / 128000000000000) ≤ -(1604871659391791879599 / 2500000000000000000000)

theorem Zeta5Irrational.U_487_4 : Uω (aρ 4) (bρ 4) (69107511152773 / 128000000000000) ≤ -(3285968618138589291277 / 5000000000000000000000)

theorem Zeta5Irrational.U_487_5 : Uω (aρ 5) (bρ 5) (69107511152773 / 128000000000000) ≤ -(6808990922769527856703 / 10000000000000000000000)

theorem Zeta5Irrational.U_487_6 : Uω (aρ 6) (bρ 6) (69107511152773 / 128000000000000) ≤ -(7159897533578763198489 / 10000000000000000000000)

theorem Zeta5Irrational.U_487_7 : Uω (aρ 7) (bρ 7) (69107511152773 / 128000000000000) ≤ -(7661314156593136158591 / 10000000000000000000000)

theorem Zeta5Irrational.U_487_8 : Uω (aρ 8) (bρ 8) (69107511152773 / 128000000000000) ≤ -(8360393601371293797627 / 10000000000000000000000)

theorem Zeta5Irrational.U_487_9 : Uω (aρ 9) (bρ 9) (69107511152773 / 128000000000000) ≤ -(932312360618953778177 / 1000000000000000000000)

theorem Zeta5Irrational.U_487_10 : Uω (aρ 10) (bρ 10) (69107511152773 / 128000000000000) ≤ -(10658111730682012403533 / 10000000000000000000000)

theorem Zeta5Irrational.U_487_11 : Uω (aρ 11) (bρ 11) (69107511152773 / 128000000000000) ≤ -(6301713833760821665297 / 5000000000000000000000)

theorem Zeta5Irrational.U_487_12 : Uω (aρ 12) (bρ 12) (69107511152773 / 128000000000000) ≤ -(3235446682644510697477 / 2000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_487 : Uρ (69107511152773 / 128000000000000) ≤ -(974390919117488362389 / 1000000000000000000000)

theorem Zeta5Irrational.U_488_1 : Uω (aρ 1) (bρ 1) (8648424754351 / 16000000000000) ≤ -(62722125030626558607 / 100000000000000000000)

theorem Zeta5Irrational.U_488_2 : Uω (aρ 2) (bρ 2) (8648424754351 / 16000000000000) ≤ -(1263427061655700437097 / 2000000000000000000000)

theorem Zeta5Irrational.U_488_3 : Uω (aρ 3) (bρ 3) (8648424754351 / 16000000000000) ≤ -(6407632750799801970241 / 10000000000000000000000)

theorem Zeta5Irrational.U_488_4 : Uω (aρ 4) (bρ 4) (8648424754351 / 16000000000000) ≤ -(3279949129863435104927 / 5000000000000000000000)

theorem Zeta5Irrational.U_488_5 : Uω (aρ 5) (bρ 5) (8648424754351 / 16000000000000) ≤ -(6796655347826442500329 / 10000000000000000000000)

theorem Zeta5Irrational.U_488_6 : Uω (aρ 6) (bρ 6) (8648424754351 / 16000000000000) ≤ -(3573551067666562741491 / 5000000000000000000000)

theorem Zeta5Irrational.U_488_7 : Uω (aρ 7) (bρ 7) (8648424754351 / 16000000000000) ≤ -(305912595789937330659 / 400000000000000000000)

theorem Zeta5Irrational.U_488_8 : Uω (aρ 8) (bρ 8) (8648424754351 / 16000000000000) ≤ -(8345808874379213789631 / 10000000000000000000000)

theorem Zeta5Irrational.U_488_9 : Uω (aρ 9) (bρ 9) (8648424754351 / 16000000000000) ≤ -(9306805504687874914537 / 10000000000000000000000)

theorem Zeta5Irrational.U_488_10 : Uω (aρ 10) (bρ 10) (8648424754351 / 16000000000000) ≤ -(531939342072332120009 / 500000000000000000000)

theorem Zeta5Irrational.U_488_11 : Uω (aρ 11) (bρ 11) (8648424754351 / 16000000000000) ≤ -(1572219133875210761649 / 1250000000000000000000)

theorem Zeta5Irrational.U_488_12 : Uω (aρ 12) (bρ 12) (8648424754351 / 16000000000000) ≤ -(16123145677231630302739 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_488 : Uρ (8648424754351 / 16000000000000) ≤ -(194580223848825435147 / 200000000000000000000)

theorem Zeta5Irrational.U_489_1 : Uω (aρ 1) (bρ 1) (69267284916843 / 128000000000000) ≤ -(1252106660842020123547 / 2000000000000000000000)

theorem Zeta5Irrational.U_489_2 : Uω (aρ 2) (bρ 2) (69267284916843 / 128000000000000) ≤ -(6305403182837248309091 / 10000000000000000000000)

theorem Zeta5Irrational.U_489_3 : Uω (aρ 3) (bρ 3) (69267284916843 / 128000000000000) ≤ -(3197896451298350055509 / 5000000000000000000000)

theorem Zeta5Irrational.U_489_4 : Uω (aρ 4) (bρ 4) (69267284916843 / 128000000000000) ≤ -(1636968442687012044419 / 2500000000000000000000)

theorem Zeta5Irrational.U_489_5 : Uω (aρ 5) (bρ 5) (69267284916843 / 128000000000000) ≤ -(1696083750571734394177 / 2500000000000000000000)

theorem Zeta5Irrational.U_489_6 : Uω (aρ 6) (bρ 6) (69267284916843 / 128000000000000) ≤ -(22294759913439966139 / 31250000000000000000)

theorem Zeta5Irrational.U_489_7 : Uω (aρ 7) (bρ 7) (69267284916843 / 128000000000000) ≤ -(7634334050232765267451 / 10000000000000000000000)

theorem Zeta5Irrational.U_489_8 : Uω (aρ 8) (bρ 8) (69267284916843 / 128000000000000) ≤ -(4165622981717381617827 / 5000000000000000000000)

theorem Zeta5Irrational.U_489_9 : Uω (aρ 9) (bρ 9) (69267284916843 / 128000000000000) ≤ -(9290515580424209657449 / 10000000000000000000000)

theorem Zeta5Irrational.U_489_10 : Uω (aρ 10) (bρ 10) (69267284916843 / 128000000000000) ≤ -(10619504240865397292307 / 10000000000000000000000)

theorem Zeta5Irrational.U_489_11 : Uω (aρ 11) (bρ 11) (69267284916843 / 128000000000000) ≤ -(12552166172502945745251 / 10000000000000000000000)

theorem Zeta5Irrational.U_489_12 : Uω (aρ 12) (bρ 12) (69267284916843 / 128000000000000) ≤ -(16069760752416665406813 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_489 : Uρ (69267284916843 / 128000000000000) ≤ -(1942836699118080219587 / 2000000000000000000000)

theorem Zeta5Irrational.U_490_1 : Uω (aρ 1) (bρ 1) (34673585899439 / 64000000000000) ≤ -(3124433864984652654599 / 5000000000000000000000)

theorem Zeta5Irrational.U_490_2 : Uω (aρ 2) (bρ 2) (34673585899439 / 64000000000000) ≤ -(15734212016432925827 / 25000000000000000000)

theorem Zeta5Irrational.U_490_3 : Uω (aρ 3) (bρ 3) (34673585899439 / 64000000000000) ≤ -(797995882467076955683 / 1250000000000000000000)

theorem Zeta5Irrational.U_490_4 : Uω (aρ 4) (bρ 4) (34673585899439 / 64000000000000) ≤ -(6535863734487156375171 / 10000000000000000000000)

theorem Zeta5Irrational.U_490_5 : Uω (aρ 5) (bρ 5) (34673585899439 / 64000000000000) ≤ -(3386014924257870962009 / 5000000000000000000000)

theorem Zeta5Irrational.U_490_6 : Uω (aρ 6) (bρ 6) (34673585899439 / 64000000000000) ≤ -(7121560602100884678399 / 10000000000000000000000)

theorem Zeta5Irrational.U_490_7 : Uω (aρ 7) (bρ 7) (34673585899439 / 64000000000000) ≤ -(7620871572269016417851 / 10000000000000000000000)

theorem Zeta5Irrational.U_490_8 : Uω (aρ 8) (bρ 8) (34673585899439 / 64000000000000) ≤ -(2079176200419582819051 / 2500000000000000000000)

theorem Zeta5Irrational.U_490_9 : Uω (aρ 9) (bρ 9) (34673585899439 / 64000000000000) ≤ -(4637126865470083261903 / 5000000000000000000000)

theorem Zeta5Irrational.U_490_10 : Uω (aρ 10) (bρ 10) (34673585899439 / 64000000000000) ≤ -(5300131861877623017487 / 5000000000000000000000)

theorem Zeta5Irrational.U_490_11 : Uω (aρ 11) (bρ 11) (34673585899439 / 64000000000000) ≤ -(12526666245270194488077 / 10000000000000000000000)

theorem Zeta5Irrational.U_490_12 : Uω (aρ 12) (bρ 12) (34673585899439 / 64000000000000) ≤ -(16017053398384051458857 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_490 : Uρ (34673585899439 / 64000000000000) ≤ -(2424856055011437979509 / 2500000000000000000000)

theorem Zeta5Irrational.U_491_1 : Uω (aρ 1) (bρ 1) (69427058680913 / 128000000000000) ≤ -(249488629943552077721 / 400000000000000000000)

theorem Zeta5Irrational.U_491_2 : Uω (aρ 2) (bρ 2) (69427058680913 / 128000000000000) ≤ -(6281980147295564591557 / 10000000000000000000000)

theorem Zeta5Irrational.U_491_3 : Uω (aρ 3) (bρ 3) (69427058680913 / 128000000000000) ≤ -(6372155189116117571223 / 10000000000000000000000)

theorem Zeta5Irrational.U_491_4 : Uω (aρ 4) (bρ 4) (69427058680913 / 128000000000000) ≤ -(3261934058108181114563 / 5000000000000000000000)

theorem Zeta5Irrational.U_491_5 : Uω (aρ 5) (bρ 5) (69427058680913 / 128000000000000) ≤ -(1689934962254301555617 / 2500000000000000000000)

theorem Zeta5Irrational.U_491_6 : Uω (aρ 6) (bρ 6) (69427058680913 / 128000000000000) ≤ -(3554407191258538788113 / 5000000000000000000000)

theorem Zeta5Irrational.U_491_7 : Uω (aρ 7) (bρ 7) (69427058680913 / 128000000000000) ≤ -(7607427410292149149329 / 10000000000000000000000)

theorem Zeta5Irrational.U_491_8 : Uω (aρ 8) (bρ 8) (69427058680913 / 128000000000000) ≤ -(4151092661282270086939 / 5000000000000000000000)

theorem Zeta5Irrational.U_491_9 : Uω (aρ 9) (bρ 9) (69427058680913 / 128000000000000) ≤ -(1157252481795129172497 / 1250000000000000000000)

theorem Zeta5Irrational.U_491_10 : Uω (aρ 10) (bρ 10) (69427058680913 / 128000000000000) ≤ -(165329141977207929739 / 156250000000000000000)

theorem Zeta5Irrational.U_491_11 : Uω (aρ 11) (bρ 11) (69427058680913 / 128000000000000) ≤ -(6250626286282757761457 / 5000000000000000000000)

theorem Zeta5Irrational.U_491_12 : Uω (aρ 12) (bρ 12) (69427058680913 / 128000000000000) ≤ -(1995624982888555183189 / 1250000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_491 : Uρ (69427058680913 / 128000000000000) ≤ -(484236579550365468117 / 500000000000000000000)

theorem Zeta5Irrational.U_492_1 : Uω (aρ 1) (bρ 1) (17376736390737 / 32000000000000) ≤ -(6225577328427986757589 / 10000000000000000000000)

theorem Zeta5Irrational.U_492_2 : Uω (aρ 2) (bρ 2) (17376736390737 / 32000000000000) ≤ -(3135144586463325143691 / 5000000000000000000000)

theorem Zeta5Irrational.U_492_3 : Uω (aρ 3) (bρ 3) (17376736390737 / 32000000000000) ≤ -(6360357257749035855581 / 10000000000000000000000)

theorem Zeta5Irrational.U_492_4 : Uω (aρ 4) (bρ 4) (17376736390737 / 32000000000000) ≤ -(3255943440666472898293 / 5000000000000000000000)

theorem Zeta5Irrational.U_492_5 : Uω (aρ 5) (bρ 5) (17376736390737 / 32000000000000) ≤ -(6747464966434608471673 / 10000000000000000000000)

theorem Zeta5Irrational.U_492_6 : Uω (aρ 6) (bρ 6) (17376736390737 / 32000000000000) ≤ -(1419216894299342846093 / 2000000000000000000000)

theorem Zeta5Irrational.U_492_7 : Uω (aρ 7) (bρ 7) (17376736390737 / 32000000000000) ≤ -(7594001513948014470251 / 10000000000000000000000)

theorem Zeta5Irrational.U_492_8 : Uω (aρ 8) (bρ 8) (17376736390737 / 32000000000000) ≤ -(2071921864965059653457 / 2500000000000000000000)

theorem Zeta5Irrational.U_492_9 : Uω (aρ 9) (bρ 9) (17376736390737 / 32000000000000) ≤ -(9241813849391177808397 / 10000000000000000000000)

theorem Zeta5Irrational.U_492_10 : Uω (aρ 10) (bρ 10) (17376736390737 / 32000000000000) ≤ -(2640477031809797859469 / 2500000000000000000000)

theorem Zeta5Irrational.U_492_11 : Uω (aρ 11) (bρ 11) (17376736390737 / 32000000000000) ≤ -(2495184889494876055977 / 2000000000000000000000)

theorem Zeta5Irrational.U_492_12 : Uω (aρ 12) (bρ 12) (17376736390737 / 32000000000000) ≤ -(1591357776262880250737 / 1000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_492 : Uρ (17376736390737 / 32000000000000) ≤ -(9670103930970074289523 / 10000000000000000000000)

theorem Zeta5Irrational.U_493_1 : Uω (aρ 1) (bρ 1) (69586832444983 / 128000000000000) ≤ -(1553488109489150942229 / 2500000000000000000000)

theorem Zeta5Irrational.U_493_2 : Uω (aρ 2) (bρ 2) (69586832444983 / 128000000000000) ≤ -(6258611851501049440367 / 10000000000000000000000)

theorem Zeta5Irrational.U_493_3 : Uω (aρ 3) (bρ 3) (69586832444983 / 128000000000000) ≤ -(1587143308191476179277 / 2500000000000000000000)

theorem Zeta5Irrational.U_493_4 : Uω (aρ 4) (bρ 4) (69586832444983 / 128000000000000) ≤ -(6499919995358701146053 / 10000000000000000000000)

theorem Zeta5Irrational.U_493_5 : Uω (aρ 5) (bρ 5) (69586832444983 / 128000000000000) ≤ -(1683801290887367162087 / 2500000000000000000000)

theorem Zeta5Irrational.U_493_6 : Uω (aρ 6) (bρ 6) (69586832444983 / 128000000000000) ≤ -(7083370827149970993019 / 10000000000000000000000)

theorem Zeta5Irrational.U_493_7 : Uω (aρ 7) (bρ 7) (69586832444983 / 128000000000000) ≤ -(3790296916546084192099 / 5000000000000000000000)

theorem Zeta5Irrational.U_493_8 : Uω (aρ 8) (bρ 8) (69586832444983 / 128000000000000) ≤ -(8273211147642510212537 / 10000000000000000000000)

theorem Zeta5Irrational.U_493_9 : Uω (aρ 9) (bρ 9) (69586832444983 / 128000000000000) ≤ -(115320445191368720493 / 125000000000000000000)

theorem Zeta5Irrational.U_493_10 : Uω (aρ 10) (bρ 10) (69586832444983 / 128000000000000) ≤ -(10542792645437616091663 / 10000000000000000000000)

theorem Zeta5Irrational.U_493_11 : Uω (aρ 11) (bρ 11) (69586832444983 / 128000000000000) ≤ -(778167573294784877017 / 625000000000000000000)

theorem Zeta5Irrational.U_493_12 : Uω (aρ 12) (bρ 12) (69586832444983 / 128000000000000) ≤ -(15862765972973506168137 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_493 : Uρ (69586832444983 / 128000000000000) ≤ -(1931107930420668247501 / 2000000000000000000000)

theorem Zeta5Irrational.U_494_1 : Uω (aρ 1) (bρ 1) (34833359663509 / 64000000000000) ≤ -(1240468209150847565031 / 2000000000000000000000)

theorem Zeta5Irrational.U_494_2 : Uω (aρ 2) (bρ 2) (34833359663509 / 64000000000000) ≤ -(1561737037791314671991 / 2500000000000000000000)

theorem Zeta5Irrational.U_494_3 : Uω (aρ 3) (bρ 3) (34833359663509 / 64000000000000) ≤ -(792100385176676737587 / 1250000000000000000000)

theorem Zeta5Irrational.U_494_4 : Uω (aρ 4) (bρ 4) (34833359663509 / 64000000000000) ≤ -(3243983711969671616221 / 5000000000000000000000)

theorem Zeta5Irrational.U_494_5 : Uω (aρ 5) (bρ 5) (34833359663509 / 64000000000000) ≤ -(1344592080656173711347 / 2000000000000000000000)

theorem Zeta5Irrational.U_494_6 : Uω (aρ 6) (bρ 6) (34833359663509 / 64000000000000) ≤ -(1767668351937252963239 / 2500000000000000000000)

theorem Zeta5Irrational.U_494_7 : Uω (aρ 7) (bρ 7) (34833359663509 / 64000000000000) ≤ -(3783602158894347139321 / 5000000000000000000000)

theorem Zeta5Irrational.U_494_8 : Uω (aρ 8) (bρ 8) (34833359663509 / 64000000000000) ≤ -(412937816014834911931 / 500000000000000000000)

theorem Zeta5Irrational.U_494_9 : Uω (aρ 9) (bρ 9) (34833359663509 / 64000000000000) ≤ -(920948505196492789883 / 1000000000000000000000)

theorem Zeta5Irrational.U_494_10 : Uω (aρ 10) (bρ 10) (34833359663509 / 64000000000000) ≤ -(10523718442281250153947 / 10000000000000000000000)

theorem Zeta5Irrational.U_494_11 : Uω (aρ 11) (bρ 11) (34833359663509 / 64000000000000) ≤ -(12425522060461687284879 / 10000000000000000000000)

theorem Zeta5Irrational.U_494_12 : Uω (aρ 12) (bρ 12) (34833359663509 / 64000000000000) ≤ -(7906272266414078093663 / 5000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_494 : Uρ (34833359663509 / 64000000000000) ≤ -(9641037249386160701971 / 10000000000000000000000)

theorem Zeta5Irrational.U_495_1 : Uω (aρ 1) (bρ 1) (69746606209053 / 128000000000000) ≤ -(123814862410195933307 / 200000000000000000000)

theorem Zeta5Irrational.U_495_2 : Uω (aρ 2) (bρ 2) (69746606209053 / 128000000000000) ≤ -(3117649020088563942417 / 5000000000000000000000)

theorem Zeta5Irrational.U_495_3 : Uω (aρ 3) (bρ 3) (69746606209053 / 128000000000000) ≤ -(6325046771053860354781 / 10000000000000000000000)

theorem Zeta5Irrational.U_495_4 : Uω (aρ 4) (bρ 4) (69746606209053 / 128000000000000) ≤ -(1619007283210977189607 / 2500000000000000000000)

theorem Zeta5Irrational.U_495_5 : Uω (aρ 5) (bρ 5) (69746606209053 / 128000000000000) ≤ -(6710730648684770959207 / 10000000000000000000000)

theorem Zeta5Irrational.U_495_6 : Uω (aρ 6) (bρ 6) (69746606209053 / 128000000000000) ≤ -(1764498042931787618447 / 2500000000000000000000)

theorem Zeta5Irrational.U_495_7 : Uω (aρ 7) (bρ 7) (69746606209053 / 128000000000000) ≤ -(1888458229577260486051 / 2500000000000000000000)

theorem Zeta5Irrational.U_495_8 : Uω (aρ 8) (bρ 8) (69746606209053 / 128000000000000) ≤ -(4122161456257221488253 / 5000000000000000000000)

theorem Zeta5Irrational.U_495_9 : Uω (aρ 9) (bρ 9) (69746606209053 / 128000000000000) ≤ -(9193362059771989769797 / 10000000000000000000000)

theorem Zeta5Irrational.U_495_10 : Uω (aρ 10) (bρ 10) (69746606209053 / 128000000000000) ≤ -(5252342660226903689753 / 5000000000000000000000)

theorem Zeta5Irrational.U_495_11 : Uω (aρ 11) (bρ 11) (69746606209053 / 128000000000000) ≤ -(2480089286429880528157 / 2000000000000000000000)

theorem Zeta5Irrational.U_495_12 : Uω (aρ 12) (bρ 12) (69746606209053 / 128000000000000) ≤ -(3152578911133758865109 / 2000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_495 : Uρ (69746606209053 / 128000000000000) ≤ -(9626595294409110944959 / 10000000000000000000000)