Certified arcsine potential bounds (U46)

theorem Zeta5Irrational.U_556_1 : Uω (aρ 1) (bρ 1) (10146313901169 / 16000000000000) ≤ -(291065728968855683219 / 625000000000000000000)

theorem Zeta5Irrational.U_556_2 : Uω (aρ 2) (bρ 2) (10146313901169 / 16000000000000) ≤ -(2347610491870088450017 / 5000000000000000000000)

theorem Zeta5Irrational.U_556_3 : Uω (aρ 3) (bρ 3) (10146313901169 / 16000000000000) ≤ -(4771994197900481931239 / 10000000000000000000000)

theorem Zeta5Irrational.U_556_4 : Uω (aρ 4) (bρ 4) (10146313901169 / 16000000000000) ≤ -(2450401313667920874891 / 5000000000000000000000)

theorem Zeta5Irrational.U_556_5 : Uω (aρ 5) (bρ 5) (10146313901169 / 16000000000000) ≤ -(1275037682980197292503 / 2500000000000000000000)

theorem Zeta5Irrational.U_556_6 : Uω (aρ 6) (bρ 6) (10146313901169 / 16000000000000) ≤ -(5393044761434235189473 / 10000000000000000000000)

theorem Zeta5Irrational.U_556_7 : Uω (aρ 7) (bρ 7) (10146313901169 / 16000000000000) ≤ -(362920054805424530923 / 625000000000000000000)

theorem Zeta5Irrational.U_556_8 : Uω (aρ 8) (bρ 8) (10146313901169 / 16000000000000) ≤ -(6373060435506251966543 / 10000000000000000000000)

theorem Zeta5Irrational.U_556_9 : Uω (aρ 9) (bρ 9) (10146313901169 / 16000000000000) ≤ -(1426088610888638727831 / 2000000000000000000000)

theorem Zeta5Irrational.U_556_10 : Uω (aρ 10) (bρ 10) (10146313901169 / 16000000000000) ≤ -(508060006594250466711 / 625000000000000000000)

theorem Zeta5Irrational.U_556_11 : Uω (aρ 11) (bρ 11) (10146313901169 / 16000000000000) ≤ -(1180631375359092244143 / 1250000000000000000000)

theorem Zeta5Irrational.U_556_12 : Uω (aρ 12) (bρ 12) (10146313901169 / 16000000000000) ≤ -(11231330514346018154391 / 10000000000000000000000)

theorem Zeta5Irrational.U_556_13 : Uω (aρ 13) (bρ 13) (10146313901169 / 16000000000000) ≤ -(14003623676628956738161 / 10000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_556 : Uρ (10146313901169 / 16000000000000) ≤ -(7616476006420413902031 / 10000000000000000000000)

theorem Zeta5Irrational.U_557_1 : Uω (aρ 1) (bρ 1) (40654048209613 / 64000000000000) ≤ -(2319970927352704056403 / 5000000000000000000000)

theorem Zeta5Irrational.U_557_2 : Uω (aρ 2) (bρ 2) (40654048209613 / 64000000000000) ≤ -(1169511351196875418163 / 2500000000000000000000)

theorem Zeta5Irrational.U_557_3 : Uω (aρ 3) (bρ 3) (40654048209613 / 64000000000000) ≤ -(4754685173399231974649 / 10000000000000000000000)

theorem Zeta5Irrational.U_557_4 : Uω (aρ 4) (bρ 4) (40654048209613 / 64000000000000) ≤ -(2441633089450279375213 / 5000000000000000000000)

theorem Zeta5Irrational.U_557_5 : Uω (aρ 5) (bρ 5) (40654048209613 / 64000000000000) ≤ -(5082253326313264360587 / 10000000000000000000000)

theorem Zeta5Irrational.U_557_6 : Uω (aρ 6) (bρ 6) (40654048209613 / 64000000000000) ≤ -(5374596265478078590309 / 10000000000000000000000)

theorem Zeta5Irrational.U_557_7 : Uω (aρ 7) (bρ 7) (40654048209613 / 64000000000000) ≤ -(2893724476532077899517 / 5000000000000000000000)

theorem Zeta5Irrational.U_557_8 : Uω (aρ 8) (bρ 8) (40654048209613 / 64000000000000) ≤ -(6352566579593873370831 / 10000000000000000000000)

theorem Zeta5Irrational.U_557_9 : Uω (aρ 9) (bρ 9) (40654048209613 / 64000000000000) ≤ -(177702947989476951683 / 250000000000000000000)

theorem Zeta5Irrational.U_557_10 : Uω (aρ 10) (bρ 10) (40654048209613 / 64000000000000) ≤ -(253243698688492737057 / 312500000000000000000)

theorem Zeta5Irrational.U_557_11 : Uω (aρ 11) (bρ 11) (40654048209613 / 64000000000000) ≤ -(9415166918186793190237 / 10000000000000000000000)

theorem Zeta5Irrational.U_557_12 : Uω (aρ 12) (bρ 12) (40654048209613 / 64000000000000) ≤ -(11192235148967130137221 / 10000000000000000000000)

theorem Zeta5Irrational.U_557_13 : Uω (aρ 13) (bρ 13) (40654048209613 / 64000000000000) ≤ -(6967750135136901165281 / 5000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_557 : Uρ (40654048209613 / 64000000000000) ≤ -(7594649789318552314463 / 10000000000000000000000)

theorem Zeta5Irrational.U_558_1 : Uω (aρ 1) (bρ 1) (814456816291 / 1280000000000) ≤ -(4622861270707890117367 / 10000000000000000000000)

theorem Zeta5Irrational.U_558_2 : Uω (aρ 2) (bρ 2) (814456816291 / 1280000000000) ≤ -(4660899276902082966911 / 10000000000000000000000)

theorem Zeta5Irrational.U_558_3 : Uω (aρ 3) (bρ 3) (814456816291 / 1280000000000) ≤ -(4737406063087016598307 / 10000000000000000000000)

theorem Zeta5Irrational.U_558_4 : Uω (aρ 4) (bρ 4) (814456816291 / 1280000000000) ≤ -(4865760446468570302513 / 10000000000000000000000)

theorem Zeta5Irrational.U_558_5 : Uω (aρ 5) (bρ 5) (814456816291 / 1280000000000) ≤ -(2532193971103932224791 / 5000000000000000000000)

theorem Zeta5Irrational.U_558_6 : Uω (aρ 6) (bρ 6) (814456816291 / 1280000000000) ≤ -(1339045465924501048353 / 2500000000000000000000)

theorem Zeta5Irrational.U_558_7 : Uω (aρ 7) (bρ 7) (814456816291 / 1280000000000) ≤ -(2884107202550171195271 / 5000000000000000000000)

theorem Zeta5Irrational.U_558_8 : Uω (aρ 8) (bρ 8) (814456816291 / 1280000000000) ≤ -(633211539617910829051 / 1000000000000000000000)

theorem Zeta5Irrational.U_558_9 : Uω (aρ 9) (bρ 9) (814456816291 / 1280000000000) ≤ -(3542922206328462858359 / 5000000000000000000000)

theorem Zeta5Irrational.U_558_10 : Uω (aρ 10) (bρ 10) (814456816291 / 1280000000000) ≤ -(1009838093136397352783 / 1250000000000000000000)

theorem Zeta5Irrational.U_558_11 : Uω (aρ 11) (bρ 11) (814456816291 / 1280000000000) ≤ -(9385386513549517948139 / 10000000000000000000000)

theorem Zeta5Irrational.U_558_12 : Uω (aρ 12) (bρ 12) (814456816291 / 1280000000000) ≤ -(11153347910153076889553 / 10000000000000000000000)

theorem Zeta5Irrational.U_558_13 : Uω (aρ 13) (bρ 13) (814456816291 / 1280000000000) ≤ -(13868348245627295984087 / 10000000000000000000000)

theorem Zeta5Irrational.U_558_14 : Uω (aρ 14) (bρ 14) (814456816291 / 1280000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_558_15 : Uω (aρ 15) (bρ 15) (814456816291 / 1280000000000) ≤ -(268788866070650094343 / 156250000000000000000)

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

theorem Zeta5Irrational.U_558 : Uρ (814456816291 / 1280000000000) ≤ -(1893232505862725806829 / 2500000000000000000000)

theorem Zeta5Irrational.U_559_1 : Uω (aρ 1) (bρ 1) (40791633419487 / 64000000000000) ≤ -(2302904905921185912749 / 5000000000000000000000)

theorem Zeta5Irrational.U_559_2 : Uω (aρ 2) (bρ 2) (40791633419487 / 64000000000000) ≤ -(580472812406440178227 / 1250000000000000000000)

theorem Zeta5Irrational.U_559_3 : Uω (aρ 3) (bρ 3) (40791633419487 / 64000000000000) ≤ -(472015676372460509977 / 1000000000000000000000)

theorem Zeta5Irrational.U_559_4 : Uω (aρ 4) (bρ 4) (40791633419487 / 64000000000000) ≤ -(151508916330217477677 / 312500000000000000000)

theorem Zeta5Irrational.U_559_5 : Uω (aρ 5) (bρ 5) (40791633419487 / 64000000000000) ≤ -(5046554465058193984063 / 10000000000000000000000)

theorem Zeta5Irrational.U_559_6 : Uω (aρ 6) (bρ 6) (40791633419487 / 64000000000000) ≤ -(533780142986120744697 / 1000000000000000000000)

theorem Zeta5Irrational.U_559_7 : Uω (aρ 7) (bρ 7) (40791633419487 / 64000000000000) ≤ -(5749017087125469562931 / 10000000000000000000000)

theorem Zeta5Irrational.U_559_8 : Uω (aρ 8) (bρ 8) (40791633419487 / 64000000000000) ≤ -(631170670481372951783 / 1000000000000000000000)

theorem Zeta5Irrational.U_559_9 : Uω (aρ 9) (bρ 9) (40791633419487 / 64000000000000) ≤ -(353181114344393088867 / 500000000000000000000)

theorem Zeta5Irrational.U_559_10 : Uω (aρ 10) (bρ 10) (40791633419487 / 64000000000000) ≤ -(402683943645360927051 / 500000000000000000000)

theorem Zeta5Irrational.U_559_11 : Uω (aρ 11) (bρ 11) (40791633419487 / 64000000000000) ≤ -(146182952791553937827 / 156250000000000000000)

theorem Zeta5Irrational.U_559_12 : Uω (aρ 12) (bρ 12) (40791633419487 / 64000000000000) ≤ -(11114666087772948681293 / 10000000000000000000000)

theorem Zeta5Irrational.U_559_13 : Uω (aρ 13) (bρ 13) (40791633419487 / 64000000000000) ≤ -(13802130104783206082597 / 10000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_559 : Uρ (40791633419487 / 64000000000000) ≤ -(3775657065764696745661 / 5000000000000000000000)

theorem Zeta5Irrational.U_560_1 : Uω (aρ 1) (bρ 1) (5107553253053 / 8000000000000) ≤ -(2294393689475535923337 / 5000000000000000000000)

theorem Zeta5Irrational.U_560_2 : Uω (aρ 2) (bρ 2) (5107553253053 / 8000000000000) ≤ -(4626694971520392917771 / 10000000000000000000000)

theorem Zeta5Irrational.U_560_3 : Uω (aρ 3) (bρ 3) (5107553253053 / 8000000000000) ≤ -(940587434521278228623 / 2000000000000000000000)

theorem Zeta5Irrational.U_560_4 : Uω (aρ 4) (bρ 4) (5107553253053 / 8000000000000) ≤ -(1207710175071547666761 / 2500000000000000000000)

theorem Zeta5Irrational.U_560_5 : Uω (aρ 5) (bρ 5) (5107553253053 / 8000000000000) ≤ -(251437639046613927597 / 500000000000000000000)

theorem Zeta5Irrational.U_560_6 : Uω (aρ 6) (bρ 6) (5107553253053 / 8000000000000) ≤ -(5319454838437104841271 / 10000000000000000000000)

theorem Zeta5Irrational.U_560_7 : Uω (aρ 7) (bρ 7) (5107553253053 / 8000000000000) ≤ -(2864928427064339415983 / 5000000000000000000000)

theorem Zeta5Irrational.U_560_8 : Uω (aρ 8) (bρ 8) (5107553253053 / 8000000000000) ≤ -(6291340326210612036741 / 10000000000000000000000)

theorem Zeta5Irrational.U_560_9 : Uω (aρ 9) (bρ 9) (5107553253053 / 8000000000000) ≤ -(7041451297304985064883 / 10000000000000000000000)

theorem Zeta5Irrational.U_560_10 : Uω (aρ 10) (bρ 10) (5107553253053 / 8000000000000) ≤ -(4014360175648586768127 / 5000000000000000000000)

theorem Zeta5Irrational.U_560_11 : Uω (aρ 11) (bρ 11) (5107553253053 / 8000000000000) ≤ -(932613351350855815937 / 1000000000000000000000)

theorem Zeta5Irrational.U_560_12 : Uω (aρ 12) (bρ 12) (5107553253053 / 8000000000000) ≤ -(2769046757582107150309 / 2500000000000000000000)

theorem Zeta5Irrational.U_560_13 : Uω (aρ 13) (bρ 13) (5107553253053 / 8000000000000) ≤ -(13736810718800869438119 / 10000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_560 : Uρ (5107553253053 / 8000000000000) ≤ -(1505959936281701094027 / 2000000000000000000000)

theorem Zeta5Irrational.U_561_1 : Uω (aρ 1) (bρ 1) (20499005617149 / 32000000000000) ≤ -(2277414598492095836739 / 5000000000000000000000)

theorem Zeta5Irrational.U_561_2 : Uω (aρ 2) (bρ 2) (20499005617149 / 32000000000000) ≤ -(4592607267118482431659 / 10000000000000000000000)

theorem Zeta5Irrational.U_561_3 : Uω (aρ 3) (bρ 3) (20499005617149 / 32000000000000) ≤ -(4668586706926270342089 / 10000000000000000000000)

theorem Zeta5Irrational.U_561_4 : Uω (aρ 4) (bρ 4) (20499005617149 / 32000000000000) ≤ -(479604253574241296943 / 1000000000000000000000)

theorem Zeta5Irrational.U_561_5 : Uω (aρ 5) (bρ 5) (20499005617149 / 32000000000000) ≤ -(4993244339069595102151 / 10000000000000000000000)

theorem Zeta5Irrational.U_561_6 : Uω (aρ 6) (bρ 6) (20499005617149 / 32000000000000) ≤ -(5282862684184516705617 / 10000000000000000000000)

theorem Zeta5Irrational.U_561_7 : Uω (aρ 7) (bρ 7) (20499005617149 / 32000000000000) ≤ -(1138329413456083984391 / 2000000000000000000000)

theorem Zeta5Irrational.U_561_8 : Uω (aρ 8) (bρ 8) (20499005617149 / 32000000000000) ≤ -(6250733795887733386939 / 10000000000000000000000)

theorem Zeta5Irrational.U_561_9 : Uω (aρ 9) (bρ 9) (20499005617149 / 32000000000000) ≤ -(3498630877915021785957 / 5000000000000000000000)

theorem Zeta5Irrational.U_561_10 : Uω (aρ 10) (bρ 10) (20499005617149 / 32000000000000) ≤ -(3989501908388574488219 / 5000000000000000000000)

theorem Zeta5Irrational.U_561_11 : Uω (aρ 11) (bρ 11) (20499005617149 / 32000000000000) ≤ -(4633642821382275522129 / 5000000000000000000000)

theorem Zeta5Irrational.U_561_12 : Uω (aρ 12) (bρ 12) (20499005617149 / 32000000000000) ≤ -(10999826886831738863463 / 10000000000000000000000)

theorem Zeta5Irrational.U_561_13 : Uω (aρ 13) (bρ 13) (20499005617149 / 32000000000000) ≤ -(1701092299087291908943 / 1250000000000000000000)

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

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

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

theorem Zeta5Irrational.U_561 : Uρ (20499005617149 / 32000000000000) ≤ -(1497413207056877704401 / 2000000000000000000000)

theorem Zeta5Irrational.U_562_1 : Uω (aρ 1) (bρ 1) (10283899111043 / 16000000000000) ≤ -(565123242699242190631 / 1250000000000000000000)

theorem Zeta5Irrational.U_562_2 : Uω (aρ 2) (bρ 2) (10283899111043 / 16000000000000) ≤ -(227931768568958541353 / 500000000000000000000)

theorem Zeta5Irrational.U_562_3 : Uω (aρ 3) (bρ 3) (10283899111043 / 16000000000000) ≤ -(4634353854935592034951 / 10000000000000000000000)

theorem Zeta5Irrational.U_562_4 : Uω (aρ 4) (bρ 4) (10283899111043 / 16000000000000) ≤ -(74396329823126201829 / 156250000000000000000)

theorem Zeta5Irrational.U_562_5 : Uω (aρ 5) (bρ 5) (10283899111043 / 16000000000000) ≤ -(4957861717286478519223 / 10000000000000000000000)

theorem Zeta5Irrational.U_562_6 : Uω (aρ 6) (bρ 6) (10283899111043 / 16000000000000) ≤ -(5246404410543003654287 / 10000000000000000000000)

theorem Zeta5Irrational.U_562_7 : Uω (aρ 7) (bρ 7) (10283899111043 / 16000000000000) ≤ -(282679195069658106583 / 500000000000000000000)

theorem Zeta5Irrational.U_562_8 : Uω (aρ 8) (bρ 8) (10283899111043 / 16000000000000) ≤ -(621029439375479713257 / 1000000000000000000000)

theorem Zeta5Irrational.U_562_9 : Uω (aρ 9) (bρ 9) (10283899111043 / 16000000000000) ≤ -(6953273864243853381139 / 10000000000000000000000)

theorem Zeta5Irrational.U_562_10 : Uω (aρ 10) (bρ 10) (10283899111043 / 16000000000000) ≤ -(7929552090284195248573 / 10000000000000000000000)

theorem Zeta5Irrational.U_562_11 : Uω (aρ 11) (bρ 11) (10283899111043 / 16000000000000) ≤ -(92088367002658787047 / 100000000000000000000)

theorem Zeta5Irrational.U_562_12 : Uω (aρ 12) (bρ 12) (10283899111043 / 16000000000000) ≤ -(5462123687277067907423 / 5000000000000000000000)

theorem Zeta5Irrational.U_562_13 : Uω (aρ 13) (bρ 13) (10283899111043 / 16000000000000) ≤ -(13483890514746875546159 / 10000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_562 : Uρ (10283899111043 / 16000000000000) ≤ -(3722356053754804569431 / 5000000000000000000000)

theorem Zeta5Irrational.U_563_1 : Uω (aρ 1) (bρ 1) (20636590827023 / 32000000000000) ≤ -(1121814209373083173601 / 2500000000000000000000)

theorem Zeta5Irrational.U_563_2 : Uω (aρ 2) (bρ 2) (20636590827023 / 32000000000000) ≤ -(565597312504274044621 / 1250000000000000000000)

theorem Zeta5Irrational.U_563_3 : Uω (aρ 3) (bρ 3) (20636590827023 / 32000000000000) ≤ -(184009512553182304903 / 400000000000000000000)

theorem Zeta5Irrational.U_563_4 : Uω (aρ 4) (bρ 4) (20636590827023 / 32000000000000) ≤ -(1181701895927001116443 / 2500000000000000000000)

theorem Zeta5Irrational.U_563_5 : Uω (aρ 5) (bρ 5) (20636590827023 / 32000000000000) ≤ -(4922604025803230328569 / 10000000000000000000000)

theorem Zeta5Irrational.U_563_6 : Uω (aρ 6) (bρ 6) (20636590827023 / 32000000000000) ≤ -(2605039519011009743847 / 5000000000000000000000)

theorem Zeta5Irrational.U_563_7 : Uω (aρ 7) (bρ 7) (20636590827023 / 32000000000000) ≤ -(1123133245324348551683 / 2000000000000000000000)

theorem Zeta5Irrational.U_563_8 : Uω (aρ 8) (bρ 8) (20636590827023 / 32000000000000) ≤ -(6170020726299281010733 / 10000000000000000000000)

theorem Zeta5Irrational.U_563_9 : Uω (aρ 9) (bρ 9) (20636590827023 / 32000000000000) ≤ -(3454742864578543876601 / 5000000000000000000000)

theorem Zeta5Irrational.U_563_10 : Uω (aρ 10) (bρ 10) (20636590827023 / 32000000000000) ≤ -(1576072435054941454207 / 2000000000000000000000)

theorem Zeta5Irrational.U_563_11 : Uω (aρ 11) (bρ 11) (20636590827023 / 32000000000000) ≤ -(9150780638360100323413 / 10000000000000000000000)

theorem Zeta5Irrational.U_563_12 : Uω (aρ 12) (bρ 12) (20636590827023 / 32000000000000) ≤ -(542471460987771583411 / 500000000000000000000)

theorem Zeta5Irrational.U_563_13 : Uω (aρ 13) (bρ 13) (20636590827023 / 32000000000000) ≤ -(2672410650574187809643 / 2000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_563 : Uρ (20636590827023 / 32000000000000) ≤ -(740272258788343837463 / 1000000000000000000000)

theorem Zeta5Irrational.U_564_1 : Uω (aρ 1) (bρ 1) (517634585799 / 800000000000) ≤ -(4453641117210170942821 / 10000000000000000000000)

theorem Zeta5Irrational.U_564_2 : Uω (aρ 2) (bρ 2) (517634585799 / 800000000000) ≤ -(4491035876755540387069 / 10000000000000000000000)

theorem Zeta5Irrational.U_564_3 : Uω (aρ 3) (bρ 3) (517634585799 / 800000000000) ≤ -(4566237788996584143217 / 10000000000000000000000)

theorem Zeta5Irrational.U_564_4 : Uω (aρ 4) (bρ 4) (517634585799 / 800000000000) ≤ -(58654614175999811513 / 125000000000000000000)

theorem Zeta5Irrational.U_564_5 : Uω (aρ 5) (bρ 5) (517634585799 / 800000000000) ≤ -(977494076851752214137 / 2000000000000000000000)

theorem Zeta5Irrational.U_564_6 : Uω (aρ 6) (bρ 6) (517634585799 / 800000000000) ≤ -(5173885597877607211283 / 10000000000000000000000)

theorem Zeta5Irrational.U_564_7 : Uω (aρ 7) (bρ 7) (517634585799 / 800000000000) ≤ -(1394473231557664473619 / 2500000000000000000000)

theorem Zeta5Irrational.U_564_8 : Uω (aρ 8) (bρ 8) (517634585799 / 800000000000) ≤ -(766238927205555868307 / 1250000000000000000000)

theorem Zeta5Irrational.U_564_9 : Uω (aρ 9) (bρ 9) (517634585799 / 800000000000) ≤ -(6865895476826353308691 / 10000000000000000000000)

theorem Zeta5Irrational.U_564_10 : Uω (aρ 10) (bρ 10) (517634585799 / 800000000000) ≤ -(7831431128554380707361 / 10000000000000000000000)

theorem Zeta5Irrational.U_564_11 : Uω (aρ 11) (bρ 11) (517634585799 / 800000000000) ≤ -(9093111557506252195301 / 10000000000000000000000)

theorem Zeta5Irrational.U_564_12 : Uω (aρ 12) (bρ 12) (517634585799 / 800000000000) ≤ -(5387676966162376967213 / 5000000000000000000000)

theorem Zeta5Irrational.U_564_13 : Uω (aρ 13) (bρ 13) (517634585799 / 800000000000) ≤ -(3310758912492028501331 / 2500000000000000000000)

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

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

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

theorem Zeta5Irrational.U_564 : Uρ (517634585799 / 800000000000) ≤ -(3680541795298583111983 / 5000000000000000000000)

theorem Zeta5Irrational.U_565_1 : Uω (aρ 1) (bρ 1) (20774176036897 / 32000000000000) ≤ -(11050345052480570479 / 25000000000000000000)

theorem Zeta5Irrational.U_565_2 : Uω (aρ 2) (bρ 2) (20774176036897 / 32000000000000) ≤ -(4457406733048630161033 / 10000000000000000000000)

theorem Zeta5Irrational.U_565_3 : Uω (aρ 3) (bρ 3) (20774176036897 / 32000000000000) ≤ -(4532352993907169877393 / 10000000000000000000000)

theorem Zeta5Irrational.U_565_4 : Uω (aρ 4) (bρ 4) (20774176036897 / 32000000000000) ≤ -(232902447078791866397 / 500000000000000000000)

theorem Zeta5Irrational.U_565_5 : Uω (aρ 5) (bρ 5) (20774176036897 / 32000000000000) ≤ -(4852459921577938326357 / 10000000000000000000000)

theorem Zeta5Irrational.U_565_6 : Uω (aρ 6) (bρ 6) (20774176036897 / 32000000000000) ≤ -(64222789149440470487 / 125000000000000000000)

theorem Zeta5Irrational.U_565_7 : Uω (aρ 7) (bρ 7) (20774176036897 / 32000000000000) ≤ -(5540262896390538563607 / 10000000000000000000000)

theorem Zeta5Irrational.U_565_8 : Uω (aρ 8) (bρ 8) (20774176036897 / 32000000000000) ≤ -(6089965109248601034731 / 10000000000000000000000)

theorem Zeta5Irrational.U_565_9 : Uω (aρ 9) (bρ 9) (20774176036897 / 32000000000000) ≤ -(213203164631554066227 / 312500000000000000000)

theorem Zeta5Irrational.U_565_10 : Uω (aρ 10) (bρ 10) (20774176036897 / 32000000000000) ≤ -(3891378029483553701593 / 5000000000000000000000)

theorem Zeta5Irrational.U_565_11 : Uω (aρ 11) (bρ 11) (20774176036897 / 32000000000000) ≤ -(9035823701220572399023 / 10000000000000000000000)

theorem Zeta5Irrational.U_565_12 : Uω (aρ 12) (bρ 12) (20774176036897 / 32000000000000) ≤ -(5351001880761519242997 / 5000000000000000000000)

theorem Zeta5Irrational.U_565_13 : Uω (aρ 13) (bρ 13) (20774176036897 / 32000000000000) ≤ -(13126666327036419575017 / 10000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_565 : Uρ (20774176036897 / 32000000000000) ≤ -(457486403617067305977 / 625000000000000000000)

theorem Zeta5Irrational.U_566_1 : Uω (aρ 1) (bρ 1) (10421484320917 / 16000000000000) ≤ -(438674679669422764263 / 1000000000000000000000)

theorem Zeta5Irrational.U_566_2 : Uω (aρ 2) (bρ 2) (10421484320917 / 16000000000000) ≤ -(552986288518407495121 / 1250000000000000000000)

theorem Zeta5Irrational.U_566_3 : Uω (aρ 3) (bρ 3) (10421484320917 / 16000000000000) ≤ -(1124645662501160291839 / 2500000000000000000000)

theorem Zeta5Irrational.U_566_4 : Uω (aρ 4) (bρ 4) (10421484320917 / 16000000000000) ≤ -(4623846196384515435809 / 10000000000000000000000)

theorem Zeta5Irrational.U_566_5 : Uω (aρ 5) (bρ 5) (10421484320917 / 16000000000000) ≤ -(963514355168254296311 / 2000000000000000000000)

theorem Zeta5Irrational.U_566_6 : Uω (aρ 6) (bρ 6) (10421484320917 / 16000000000000) ≤ -(5101890692535526692447 / 10000000000000000000000)

theorem Zeta5Irrational.U_566_7 : Uω (aρ 7) (bρ 7) (10421484320917 / 16000000000000) ≤ -(1375693761494647139359 / 2500000000000000000000)

theorem Zeta5Irrational.U_566_8 : Uω (aρ 8) (bρ 8) (10421484320917 / 16000000000000) ≤ -(3025090229805417688551 / 5000000000000000000000)

theorem Zeta5Irrational.U_566_9 : Uω (aρ 9) (bρ 9) (10421484320917 / 16000000000000) ≤ -(1355860257608270240147 / 2000000000000000000000)

theorem Zeta5Irrational.U_566_10 : Uω (aρ 10) (bρ 10) (10421484320917 / 16000000000000) ≤ -(1933583531531276978283 / 2500000000000000000000)

theorem Zeta5Irrational.U_566_11 : Uω (aρ 11) (bρ 11) (10421484320917 / 16000000000000) ≤ -(140295491425674205323 / 156250000000000000000)

theorem Zeta5Irrational.U_566_12 : Uω (aρ 12) (bρ 12) (10421484320917 / 16000000000000) ≤ -(10629361654901392404073 / 10000000000000000000000)

theorem Zeta5Irrational.U_566_13 : Uω (aρ 13) (bρ 13) (10421484320917 / 16000000000000) ≤ -(13012790773802567949037 / 10000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_566 : Uρ (10421484320917 / 16000000000000) ≤ -(3639403798061565336769 / 5000000000000000000000)

theorem Zeta5Irrational.U_567_1 : Uω (aρ 1) (bρ 1) (20911761246771 / 32000000000000) ≤ -(4353466699681521755969 / 10000000000000000000000)

theorem Zeta5Irrational.U_567_2 : Uω (aρ 2) (bρ 2) (20911761246771 / 32000000000000) ≤ -(4390485848910326832271 / 10000000000000000000000)

theorem Zeta5Irrational.U_567_3 : Uω (aρ 3) (bρ 3) (20911761246771 / 32000000000000) ≤ -(558115748324716916001 / 1250000000000000000000)

theorem Zeta5Irrational.U_567_4 : Uω (aρ 4) (bρ 4) (20911761246771 / 32000000000000) ≤ -(1147440024247301742847 / 2500000000000000000000)

theorem Zeta5Irrational.U_567_5 : Uω (aρ 5) (bρ 5) (20911761246771 / 32000000000000) ≤ -(239140254707843448427 / 500000000000000000000)

theorem Zeta5Irrational.U_567_6 : Uω (aρ 6) (bρ 6) (20911761246771 / 32000000000000) ≤ -(5066087342182747444541 / 10000000000000000000000)

theorem Zeta5Irrational.U_567_7 : Uω (aρ 7) (bρ 7) (20911761246771 / 32000000000000) ≤ -(2732714148191447201139 / 5000000000000000000000)

theorem Zeta5Irrational.U_567_8 : Uω (aρ 8) (bρ 8) (20911761246771 / 32000000000000) ≤ -(6010556143983057996553 / 10000000000000000000000)

theorem Zeta5Irrational.U_567_9 : Uω (aρ 9) (bρ 9) (20911761246771 / 32000000000000) ≤ -(168407343672909906301 / 250000000000000000000)

theorem Zeta5Irrational.U_567_10 : Uω (aρ 10) (bρ 10) (20911761246771 / 32000000000000) ≤ -(1921540634794681486427 / 2500000000000000000000)

theorem Zeta5Irrational.U_567_11 : Uω (aρ 11) (bρ 11) (20911761246771 / 32000000000000) ≤ -(892236932291373259771 / 1000000000000000000000)

theorem Zeta5Irrational.U_567_12 : Uω (aρ 12) (bρ 12) (20911761246771 / 32000000000000) ≤ -(10557411220120595044881 / 10000000000000000000000)

theorem Zeta5Irrational.U_567_13 : Uω (aρ 13) (bρ 13) (20911761246771 / 32000000000000) ≤ -(3225317275922843369361 / 2500000000000000000000)

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

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

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

theorem Zeta5Irrational.U_567 : Uρ (20911761246771 / 32000000000000) ≤ -(7238148340803391625791 / 10000000000000000000000)