Certified arcsine potential bounds (U00)

theorem Zeta5Irrational.U_0_1 : Uω (aρ 1) (bρ 1) 0 ≤ -(12712663703508542025099 / 2500000000000000000000)

theorem Zeta5Irrational.U_0_2 : Uω (aρ 2) (bρ 2) 0 ≤ -(1962983986998948336949 / 400000000000000000000)

theorem Zeta5Irrational.U_0_3 : Uω (aρ 3) (bρ 3) 0 ≤ -(46267520391835680481277 / 10000000000000000000000)

theorem Zeta5Irrational.U_0_4 : Uω (aρ 4) (bρ 4) 0 ≤ -(5359553913723040081263 / 1250000000000000000000)

theorem Zeta5Irrational.U_0_5 : Uω (aρ 5) (bρ 5) 0 ≤ -(39275139978819449528723 / 10000000000000000000000)

theorem Zeta5Irrational.U_0_6 : Uω (aρ 6) (bρ 6) 0 ≤ -(7143339604213661208809 / 2000000000000000000000)

theorem Zeta5Irrational.U_0_7 : Uω (aρ 7) (bρ 7) 0 ≤ -(32351824960621028314427 / 10000000000000000000000)

theorem Zeta5Irrational.U_0_8 : Uω (aρ 8) (bρ 8) 0 ≤ -(7315709960795885799737 / 2500000000000000000000)

theorem Zeta5Irrational.U_0_9 : Uω (aρ 9) (bρ 9) 0 ≤ -(13245699571552860366621 / 5000000000000000000000)

theorem Zeta5Irrational.U_0_10 : Uω (aρ 10) (bρ 10) 0 ≤ -(4811289393237367803367 / 2000000000000000000000)

theorem Zeta5Irrational.U_0_11 : Uω (aρ 11) (bρ 11) 0 ≤ -(21964674985840736154593 / 10000000000000000000000)

theorem Zeta5Irrational.U_0_12 : Uω (aρ 12) (bρ 12) 0 ≤ -(4043272987456227879851 / 2000000000000000000000)

theorem Zeta5Irrational.U_0_13 : Uω (aρ 13) (bρ 13) 0 ≤ -(4702168270076774782451 / 2500000000000000000000)

theorem Zeta5Irrational.U_0_14 : Uω (aρ 14) (bρ 14) 0 ≤ -(2217195343887504332233 / 1250000000000000000000)

theorem Zeta5Irrational.U_0_15 : Uω (aρ 15) (bρ 15) 0 ≤ -(16999000975580328413317 / 10000000000000000000000)

theorem Zeta5Irrational.U_0_16 : Uω (aρ 16) (bρ 16) 0 ≤ -(1036850562756824007821 / 625000000000000000000)

theorem Zeta5Irrational.U_0 : Uρ 0 ≤ -(27385656762631359502577 / 10000000000000000000000)

theorem Zeta5Irrational.U_1_1 : Uω (aρ 1) (bρ 1) (7174131 / 200000000000) ≤ -(50911373318893302541507 / 10000000000000000000000)

theorem Zeta5Irrational.U_1_2 : Uω (aρ 2) (bρ 2) (7174131 / 200000000000) ≤ -(49135098078763348601453 / 10000000000000000000000)

theorem Zeta5Irrational.U_1_3 : Uω (aρ 3) (bρ 3) (7174131 / 200000000000) ≤ -(46327645463733161241931 / 10000000000000000000000)

theorem Zeta5Irrational.U_1_4 : Uω (aρ 4) (bρ 4) (7174131 / 200000000000) ≤ -(42936065490516840879561 / 10000000000000000000000)

theorem Zeta5Irrational.U_1_5 : Uω (aρ 5) (bρ 5) (7174131 / 200000000000) ≤ -(7866842272424100993973 / 2000000000000000000000)

theorem Zeta5Irrational.U_1_6 : Uω (aρ 6) (bρ 6) (7174131 / 200000000000) ≤ -(1431007411209519275791 / 400000000000000000000)

theorem Zeta5Irrational.U_1_7 : Uω (aρ 7) (bρ 7) (7174131 / 200000000000) ≤ -(40512196593284858497 / 12500000000000000000)

theorem Zeta5Irrational.U_1_8 : Uω (aρ 8) (bρ 8) (7174131 / 200000000000) ≤ -(14660146048277734861007 / 5000000000000000000000)

theorem Zeta5Irrational.U_1_9 : Uω (aρ 9) (bρ 9) (7174131 / 200000000000) ≤ -(5309696547214735406207 / 2000000000000000000000)

theorem Zeta5Irrational.U_1_10 : Uω (aρ 10) (bρ 10) (7174131 / 200000000000) ≤ -(24113296642670996497633 / 10000000000000000000000)

theorem Zeta5Irrational.U_1_11 : Uω (aρ 11) (bρ 11) (7174131 / 200000000000) ≤ -(5505358080027453352527 / 2500000000000000000000)

theorem Zeta5Irrational.U_1_12 : Uω (aρ 12) (bρ 12) (7174131 / 200000000000) ≤ -(10136579785760210337841 / 5000000000000000000000)

theorem Zeta5Irrational.U_1_13 : Uω (aρ 13) (bρ 13) (7174131 / 200000000000) ≤ -(75462414402452552303 / 40000000000000000000)

theorem Zeta5Irrational.U_1_14 : Uω (aρ 14) (bρ 14) (7174131 / 200000000000) ≤ -(8897340153662197454051 / 5000000000000000000000)

theorem Zeta5Irrational.U_1_15 : Uω (aρ 15) (bρ 15) (7174131 / 200000000000) ≤ -(8528150055396143754779 / 5000000000000000000000)

theorem Zeta5Irrational.U_1_16 : Uω (aρ 16) (bρ 16) (7174131 / 200000000000) ≤ -(16647030518034101616959 / 10000000000000000000000)

theorem Zeta5Irrational.U_1 : Uρ (7174131 / 200000000000) ≤ -(27439164557690169188743 / 10000000000000000000000)

theorem Zeta5Irrational.U_2_1 : Uω (aρ 1) (bρ 1) (21522393 / 400000000000) ≤ -(25470941903623612969977 / 5000000000000000000000)

theorem Zeta5Irrational.U_2_2 : Uω (aρ 2) (bρ 2) (21522393 / 400000000000) ≤ -(49165552758527775040867 / 10000000000000000000000)

theorem Zeta5Irrational.U_2_3 : Uω (aρ 3) (bρ 3) (21522393 / 400000000000) ≤ -(46358019844614904236579 / 10000000000000000000000)

theorem Zeta5Irrational.U_2_4 : Uω (aρ 4) (bρ 4) (21522393 / 400000000000) ≤ -(2148318328187890160217 / 500000000000000000000)

theorem Zeta5Irrational.U_2_5 : Uω (aρ 5) (bρ 5) (21522393 / 400000000000) ≤ -(19682243075206791475787 / 5000000000000000000000)

theorem Zeta5Irrational.U_2_6 : Uω (aρ 6) (bρ 6) (21522393 / 400000000000) ≤ -(35805525469465709732703 / 10000000000000000000000)

theorem Zeta5Irrational.U_2_7 : Uω (aρ 7) (bρ 7) (21522393 / 400000000000) ≤ -(2027518787259263390593 / 625000000000000000000)

theorem Zeta5Irrational.U_2_8 : Uω (aρ 8) (bρ 8) (21522393 / 400000000000) ≤ -(183445131700844988143 / 62500000000000000000)

theorem Zeta5Irrational.U_2_9 : Uω (aρ 9) (bρ 9) (21522393 / 400000000000) ≤ -(13290010338352078837471 / 5000000000000000000000)

theorem Zeta5Irrational.U_2_10 : Uω (aρ 10) (bρ 10) (21522393 / 400000000000) ≤ -(24145699467680874899253 / 10000000000000000000000)

theorem Zeta5Irrational.U_2_11 : Uω (aρ 11) (bρ 11) (21522393 / 400000000000) ≤ -(22054972789443236367197 / 10000000000000000000000)

theorem Zeta5Irrational.U_2_12 : Uω (aρ 12) (bρ 12) (21522393 / 400000000000) ≤ -(20308097898670736143723 / 10000000000000000000000)

theorem Zeta5Irrational.U_2_13 : Uω (aρ 13) (bρ 13) (21522393 / 400000000000) ≤ -(18902136129446577859961 / 10000000000000000000000)

theorem Zeta5Irrational.U_2_14 : Uω (aρ 14) (bρ 14) (21522393 / 400000000000) ≤ -(17832860086660498318657 / 10000000000000000000000)

theorem Zeta5Irrational.U_2_15 : Uω (aρ 15) (bρ 15) (21522393 / 400000000000) ≤ -(17095939417607986453457 / 10000000000000000000000)

theorem Zeta5Irrational.U_2_16 : Uω (aρ 16) (bρ 16) (21522393 / 400000000000) ≤ -(4171908594379160841333 / 2500000000000000000000)

theorem Zeta5Irrational.U_2 : Uρ (21522393 / 400000000000) ≤ -(27469213456810556512581 / 10000000000000000000000)

theorem Zeta5Irrational.U_3_1 : Uω (aρ 1) (bρ 1) (7174131 / 100000000000) ≤ -(50972496086807483658427 / 10000000000000000000000)

theorem Zeta5Irrational.U_3_2 : Uω (aρ 2) (bρ 2) (7174131 / 100000000000) ≤ -(49196146549098639705941 / 10000000000000000000000)

theorem Zeta5Irrational.U_3_3 : Uω (aρ 3) (bρ 3) (7174131 / 100000000000) ≤ -(11597151895750616494561 / 2500000000000000000000)

theorem Zeta5Irrational.U_3_4 : Uω (aρ 4) (bρ 4) (7174131 / 100000000000) ≤ -(429970042250669996509 / 100000000000000000000)

theorem Zeta5Irrational.U_3_5 : Uω (aρ 5) (bρ 5) (7174131 / 100000000000) ≤ -(9848821862142350549383 / 2500000000000000000000)

theorem Zeta5Irrational.U_3_6 : Uω (aρ 6) (bρ 6) (7174131 / 100000000000) ≤ -(17918336888719840156369 / 5000000000000000000000)

theorem Zeta5Irrational.U_3_7 : Uω (aρ 7) (bρ 7) (7174131 / 100000000000) ≤ -(32472061297251956228297 / 10000000000000000000000)

theorem Zeta5Irrational.U_3_8 : Uω (aρ 8) (bρ 8) (7174131 / 100000000000) ≤ -(14691979007557547771577 / 5000000000000000000000)

theorem Zeta5Irrational.U_3_9 : Uω (aρ 9) (bρ 9) (7174131 / 100000000000) ≤ -(26614221306142328686011 / 10000000000000000000000)

theorem Zeta5Irrational.U_3_10 : Uω (aρ 10) (bρ 10) (7174131 / 100000000000) ≤ -(24182014718027931878799 / 10000000000000000000000)

theorem Zeta5Irrational.U_3_11 : Uω (aρ 11) (bρ 11) (7174131 / 100000000000) ≤ -(22094280725116768354743 / 10000000000000000000000)

theorem Zeta5Irrational.U_3_12 : Uω (aρ 12) (bρ 12) (7174131 / 100000000000) ≤ -(20351605328285829232061 / 10000000000000000000000)

theorem Zeta5Irrational.U_3_13 : Uω (aρ 13) (bρ 13) (7174131 / 100000000000) ≤ -(18951542575309468805869 / 10000000000000000000000)

theorem Zeta5Irrational.U_3_14 : Uω (aρ 14) (bρ 14) (7174131 / 100000000000) ≤ -(4472659389032352227177 / 2500000000000000000000)

theorem Zeta5Irrational.U_3_15 : Uω (aρ 15) (bρ 15) (7174131 / 100000000000) ≤ -(17165962668190914916479 / 10000000000000000000000)

theorem Zeta5Irrational.U_3_16 : Uω (aρ 16) (bρ 16) (7174131 / 100000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_3 : Uρ (7174131 / 100000000000) ≤ -(27504182777521718667561 / 10000000000000000000000)

theorem Zeta5Irrational.U_4_1 : Uω (aρ 1) (bρ 1) (14825913 / 200000000000) ≤ -(50976580114456355348677 / 10000000000000000000000)

theorem Zeta5Irrational.U_4_2 : Uω (aρ 2) (bρ 2) (14825913 / 200000000000) ≤ -(1968009239129451754533 / 400000000000000000000)

theorem Zeta5Irrational.U_4_3 : Uω (aρ 3) (bρ 3) (14825913 / 200000000000) ≤ -(46392696947832317425569 / 10000000000000000000000)

theorem Zeta5Irrational.U_4_4 : Uω (aρ 4) (bρ 4) (14825913 / 200000000000) ≤ -(21500554949887790778621 / 5000000000000000000000)

theorem Zeta5Irrational.U_4_5 : Uω (aρ 5) (bρ 5) (14825913 / 200000000000) ≤ -(9849857532743252544909 / 2500000000000000000000)

theorem Zeta5Irrational.U_4_6 : Uω (aρ 6) (bρ 6) (14825913 / 200000000000) ≤ -(17920442983008148696533 / 5000000000000000000000)

theorem Zeta5Irrational.U_4_7 : Uω (aρ 7) (bρ 7) (14825913 / 200000000000) ≤ -(8119097615340380036387 / 2500000000000000000000)

theorem Zeta5Irrational.U_4_8 : Uω (aρ 8) (bρ 8) (14825913 / 200000000000) ≤ -(2938847159611171861641 / 1000000000000000000000)

theorem Zeta5Irrational.U_4_9 : Uω (aρ 9) (bρ 9) (14825913 / 200000000000) ≤ -(26619015513642536754779 / 10000000000000000000000)

theorem Zeta5Irrational.U_4_10 : Uω (aρ 10) (bρ 10) (14825913 / 200000000000) ≤ -(24187231062536165434337 / 10000000000000000000000)

theorem Zeta5Irrational.U_4_11 : Uω (aρ 11) (bρ 11) (14825913 / 200000000000) ≤ -(22100139537083282243419 / 10000000000000000000000)

theorem Zeta5Irrational.U_4_12 : Uω (aρ 12) (bρ 12) (14825913 / 200000000000) ≤ -(20358481952867747024019 / 10000000000000000000000)

theorem Zeta5Irrational.U_4_13 : Uω (aρ 13) (bρ 13) (14825913 / 200000000000) ≤ -(1896017617456667321 / 1000000000000000000)

theorem Zeta5Irrational.U_4_14 : Uω (aρ 14) (bρ 14) (14825913 / 200000000000) ≤ -(8951472576252204766649 / 5000000000000000000000)

theorem Zeta5Irrational.U_4_15 : Uω (aρ 15) (bρ 15) (14825913 / 200000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_4_16 : Uω (aρ 16) (bρ 16) (14825913 / 200000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_4 : Uρ (14825913 / 200000000000) ≤ -(13755063908664878567303 / 5000000000000000000000)

theorem Zeta5Irrational.U_5_1 : Uω (aρ 1) (bρ 1) (78667711 / 1000000000000) ≤ -(50984345571698067906027 / 10000000000000000000000)

theorem Zeta5Irrational.U_5_2 : Uω (aρ 2) (bρ 2) (78667711 / 1000000000000) ≤ -(24603999536613700227217 / 5000000000000000000000)

theorem Zeta5Irrational.U_5_3 : Uω (aρ 3) (bρ 3) (78667711 / 1000000000000) ≤ -(11600119550061847085141 / 2500000000000000000000)

theorem Zeta5Irrational.U_5_4 : Uω (aρ 4) (bρ 4) (78667711 / 1000000000000) ≤ -(10752232140308635873551 / 2500000000000000000000)

theorem Zeta5Irrational.U_5_5 : Uω (aρ 5) (bρ 5) (78667711 / 1000000000000) ≤ -(1231479042758063468317 / 312500000000000000000)

theorem Zeta5Irrational.U_5_6 : Uω (aρ 6) (bρ 6) (78667711 / 1000000000000) ≤ -(17924466660160898289283 / 5000000000000000000000)

theorem Zeta5Irrational.U_5_7 : Uω (aρ 7) (bρ 7) (78667711 / 1000000000000) ≤ -(32484685260499643578059 / 10000000000000000000000)

theorem Zeta5Irrational.U_5_8 : Uω (aρ 8) (bρ 8) (78667711 / 1000000000000) ≤ -(29397157238015419786121 / 10000000000000000000000)

theorem Zeta5Irrational.U_5_9 : Uω (aρ 9) (bρ 9) (78667711 / 1000000000000) ≤ -(13314151100942602912333 / 5000000000000000000000)

theorem Zeta5Irrational.U_5_10 : Uω (aρ 10) (bρ 10) (78667711 / 1000000000000) ≤ -(12098720823673483752803 / 5000000000000000000000)

theorem Zeta5Irrational.U_5_11 : Uω (aρ 11) (bρ 11) (78667711 / 1000000000000) ≤ -(22111813113724319814737 / 10000000000000000000000)

theorem Zeta5Irrational.U_5_12 : Uω (aρ 12) (bρ 12) (78667711 / 1000000000000) ≤ -(20372656090798980590323 / 10000000000000000000000)

theorem Zeta5Irrational.U_5_13 : Uω (aρ 13) (bρ 13) (78667711 / 1000000000000) ≤ -(74138612372821309739 / 39062500000000000000)

theorem Zeta5Irrational.U_5_14 : Uω (aρ 14) (bρ 14) (78667711 / 1000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_5_15 : Uω (aρ 15) (bρ 15) (78667711 / 1000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_5_16 : Uω (aρ 16) (bρ 16) (78667711 / 1000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_5 : Uρ (78667711 / 1000000000000) ≤ -(6880237177330760400461 / 2500000000000000000000)

theorem Zeta5Irrational.U_6_1 : Uω (aρ 1) (bρ 1) (85815639 / 1000000000000) ≤ -(10199318023215378615661 / 2000000000000000000000)

theorem Zeta5Irrational.U_6_2 : Uω (aρ 2) (bρ 2) (85815639 / 1000000000000) ≤ -(49220252785694328798381 / 10000000000000000000000)

theorem Zeta5Irrational.U_6_3 : Uω (aρ 3) (bρ 3) (85815639 / 1000000000000) ≤ -(23206381385399735792023 / 5000000000000000000000)

theorem Zeta5Irrational.U_6_4 : Uω (aρ 4) (bρ 4) (85815639 / 1000000000000) ≤ -(21510644677510011539679 / 5000000000000000000000)

theorem Zeta5Irrational.U_6_5 : Uω (aρ 5) (bρ 5) (85815639 / 1000000000000) ≤ -(315358759639002277023 / 80000000000000000000)

theorem Zeta5Irrational.U_6_6 : Uω (aρ 6) (bρ 6) (85815639 / 1000000000000) ≤ -(35861726381563634540717 / 10000000000000000000000)

theorem Zeta5Irrational.U_6_7 : Uω (aρ 7) (bρ 7) (85815639 / 1000000000000) ≤ -(32497938712340042706679 / 10000000000000000000000)

theorem Zeta5Irrational.U_6_8 : Uω (aρ 8) (bρ 8) (85815639 / 1000000000000) ≤ -(29411142977102807541847 / 10000000000000000000000)

theorem Zeta5Irrational.U_6_9 : Uω (aρ 9) (bρ 9) (85815639 / 1000000000000) ≤ -(6660859717657794390429 / 2500000000000000000000)

theorem Zeta5Irrational.U_6_10 : Uω (aρ 10) (bρ 10) (85815639 / 1000000000000) ≤ -(4842885154875601165287 / 2000000000000000000000)

theorem Zeta5Irrational.U_6_11 : Uω (aρ 11) (bρ 11) (85815639 / 1000000000000) ≤ -(4426395685635096752489 / 2000000000000000000000)

theorem Zeta5Irrational.U_6_12 : Uω (aρ 12) (bρ 12) (85815639 / 1000000000000) ≤ -(5099845272237973435631 / 2500000000000000000000)

theorem Zeta5Irrational.U_6_13 : Uω (aρ 13) (bρ 13) (85815639 / 1000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_6_14 : Uω (aρ 14) (bρ 14) (85815639 / 1000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_6_15 : Uω (aρ 15) (bρ 15) (85815639 / 1000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_6_16 : Uω (aρ 16) (bρ 16) (85815639 / 1000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_6 : Uρ (85815639 / 1000000000000) ≤ -(27537256492584381318183 / 10000000000000000000000)

theorem Zeta5Irrational.U_7_1 : Uω (aρ 1) (bρ 1) (19269871 / 200000000000) ≤ -(25507332223904240133213 / 5000000000000000000000)

theorem Zeta5Irrational.U_7_2 : Uω (aρ 2) (bρ 2) (19269871 / 200000000000) ≤ -(30773969948474174723 / 6250000000000000000)

theorem Zeta5Irrational.U_7_3 : Uω (aρ 3) (bρ 3) (19269871 / 200000000000) ≤ -(23215465152356514085683 / 5000000000000000000000)

theorem Zeta5Irrational.U_7_4 : Uω (aρ 4) (bρ 4) (19269871 / 200000000000) ≤ -(21519804344189444452201 / 5000000000000000000000)

theorem Zeta5Irrational.U_7_5 : Uω (aρ 5) (bρ 5) (19269871 / 200000000000) ≤ -(315507654980808174019 / 80000000000000000000)

theorem Zeta5Irrational.U_7_6 : Uω (aρ 6) (bρ 6) (19269871 / 200000000000) ≤ -(8970212877133828550347 / 2500000000000000000000)

theorem Zeta5Irrational.U_7_7 : Uω (aρ 7) (bρ 7) (19269871 / 200000000000) ≤ -(32517914390293590790913 / 10000000000000000000000)

theorem Zeta5Irrational.U_7_8 : Uω (aρ 8) (bρ 8) (19269871 / 200000000000) ≤ -(5886499166201685248543 / 2000000000000000000000)

theorem Zeta5Irrational.U_7_9 : Uω (aρ 9) (bρ 9) (19269871 / 200000000000) ≤ -(42667279831309115271 / 16000000000000000000)

theorem Zeta5Irrational.U_7_10 : Uω (aρ 10) (bρ 10) (19269871 / 200000000000) ≤ -(606049641346655113191 / 250000000000000000000)

theorem Zeta5Irrational.U_7_11 : Uω (aρ 11) (bρ 11) (19269871 / 200000000000) ≤ -(22167783768353140953257 / 10000000000000000000000)

theorem Zeta5Irrational.U_7_12 : Uω (aρ 12) (bρ 12) (19269871 / 200000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_7_13 : Uω (aρ 13) (bρ 13) (19269871 / 200000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_7_14 : Uω (aρ 14) (bρ 14) (19269871 / 200000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_7_15 : Uω (aρ 15) (bρ 15) (19269871 / 200000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_7_16 : Uω (aρ 16) (bρ 16) (19269871 / 200000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_7 : Uρ (19269871 / 200000000000) ≤ -(6889957110960769864817 / 2500000000000000000000)

theorem Zeta5Irrational.U_8_1 : Uω (aρ 1) (bρ 1) (55761057 / 500000000000) ≤ -(51040761523417755773563 / 10000000000000000000000)

theorem Zeta5Irrational.U_8_2 : Uω (aρ 2) (bρ 2) (55761057 / 500000000000) ≤ -(12316127176026878844577 / 2500000000000000000000)

theorem Zeta5Irrational.U_8_3 : Uω (aρ 3) (bρ 3) (55761057 / 500000000000) ≤ -(46457234677264518279157 / 10000000000000000000000)

theorem Zeta5Irrational.U_8_4 : Uω (aρ 4) (bρ 4) (55761057 / 500000000000) ≤ -(21533108620975871780131 / 5000000000000000000000)

theorem Zeta5Irrational.U_8_5 : Uω (aρ 5) (bρ 5) (55761057 / 500000000000) ≤ -(1578625177908711877893 / 400000000000000000000)

theorem Zeta5Irrational.U_8_6 : Uω (aρ 6) (bρ 6) (55761057 / 500000000000) ≤ -(897725036415218135001 / 250000000000000000000)

theorem Zeta5Irrational.U_8_7 : Uω (aρ 7) (bρ 7) (55761057 / 500000000000) ≤ -(16273851117356851483897 / 5000000000000000000000)

theorem Zeta5Irrational.U_8_8 : Uω (aρ 8) (bρ 8) (55761057 / 500000000000) ≤ -(7366260065742286983877 / 2500000000000000000000)

theorem Zeta5Irrational.U_8_9 : Uω (aρ 9) (bρ 9) (55761057 / 500000000000) ≤ -(26704512040091709661141 / 10000000000000000000000)

theorem Zeta5Irrational.U_8_10 : Uω (aρ 10) (bρ 10) (55761057 / 500000000000) ≤ -(24289887987277840384009 / 10000000000000000000000)

theorem Zeta5Irrational.U_8_11 : Uω (aρ 11) (bρ 11) (55761057 / 500000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_8_12 : Uω (aρ 12) (bρ 12) (55761057 / 500000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_8_13 : Uω (aρ 13) (bρ 13) (55761057 / 500000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_8_14 : Uω (aρ 14) (bρ 14) (55761057 / 500000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_8_15 : Uω (aρ 15) (bρ 15) (55761057 / 500000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_8_16 : Uω (aρ 16) (bρ 16) (55761057 / 500000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_8 : Uρ (55761057 / 500000000000) ≤ -(5517964148274383717247 / 2000000000000000000000)

theorem Zeta5Irrational.U_9_1 : Uω (aρ 1) (bρ 1) (33336783 / 250000000000) ≤ -(10215686268319257150869 / 2000000000000000000000)

theorem Zeta5Irrational.U_9_2 : Uω (aρ 2) (bρ 2) (33336783 / 250000000000) ≤ -(9860463027542453411111 / 2000000000000000000000)

theorem Zeta5Irrational.U_9_3 : Uω (aρ 3) (bρ 3) (33336783 / 250000000000) ≤ -(46495358210023539812961 / 10000000000000000000000)

theorem Zeta5Irrational.U_9_4 : Uω (aρ 4) (bρ 4) (33336783 / 250000000000) ≤ -(21552482231997735895661 / 5000000000000000000000)

theorem Zeta5Irrational.U_9_5 : Uω (aρ 5) (bρ 5) (33336783 / 250000000000) ≤ -(19752753975247025066761 / 5000000000000000000000)

theorem Zeta5Irrational.U_9_6 : Uω (aρ 6) (bρ 6) (33336783 / 250000000000) ≤ -(17975423546595465917579 / 5000000000000000000000)

theorem Zeta5Irrational.U_9_7 : Uω (aρ 7) (bρ 7) (33336783 / 250000000000) ≤ -(6518591326819602089771 / 2000000000000000000000)

theorem Zeta5Irrational.U_9_8 : Uω (aρ 8) (bρ 8) (33336783 / 250000000000) ≤ -(14758258563778426940663 / 5000000000000000000000)

theorem Zeta5Irrational.U_9_9 : Uω (aρ 9) (bρ 9) (33336783 / 250000000000) ≤ -(5353890477833411319021 / 2000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_9 : Uρ (33336783 / 250000000000) ≤ -(6907239882122678168379 / 2500000000000000000000)

theorem Zeta5Irrational.U_10_1 : Uω (aρ 1) (bρ 1) (82548843 / 500000000000) ≤ -(51133510883215947535941 / 10000000000000000000000)

theorem Zeta5Irrational.U_10_2 : Uω (aρ 2) (bρ 2) (82548843 / 500000000000) ≤ -(24678851808854408309657 / 5000000000000000000000)

theorem Zeta5Irrational.U_10_3 : Uω (aρ 3) (bρ 3) (82548843 / 500000000000) ≤ -(5818929893213673684367 / 1250000000000000000000)

theorem Zeta5Irrational.U_10_4 : Uω (aρ 4) (bρ 4) (82548843 / 500000000000) ≤ -(43162374832339657159807 / 10000000000000000000000)

theorem Zeta5Irrational.U_10_5 : Uω (aρ 5) (bρ 5) (82548843 / 500000000000) ≤ -(39565324440062555612331 / 10000000000000000000000)

theorem Zeta5Irrational.U_10_6 : Uω (aρ 6) (bρ 6) (82548843 / 500000000000) ≤ -(36014967106290014530057 / 10000000000000000000000)

theorem Zeta5Irrational.U_10_7 : Uω (aρ 7) (bρ 7) (82548843 / 500000000000) ≤ -(8166283330872021732883 / 2500000000000000000000)

theorem Zeta5Irrational.U_10_8 : Uω (aρ 8) (bρ 8) (82548843 / 500000000000) ≤ -(592129837744490728151 / 200000000000000000000)

theorem Zeta5Irrational.U_10_9 : Uω (aρ 9) (bρ 9) (82548843 / 500000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_10_10 : Uω (aρ 10) (bρ 10) (82548843 / 500000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_10_11 : Uω (aρ 11) (bρ 11) (82548843 / 500000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_10_12 : Uω (aρ 12) (bρ 12) (82548843 / 500000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_10_13 : Uω (aρ 13) (bρ 13) (82548843 / 500000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_10_14 : Uω (aρ 14) (bρ 14) (82548843 / 500000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_10_15 : Uω (aρ 15) (bρ 15) (82548843 / 500000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_10_16 : Uω (aρ 16) (bρ 16) (82548843 / 500000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_10 : Uρ (82548843 / 500000000000) ≤ -(1107174623610650247861 / 400000000000000000000)

theorem Zeta5Irrational.U_11_1 : Uω (aρ 1) (bρ 1) (53051547 / 250000000000) ≤ -(10243169805498114481613 / 2000000000000000000000)

theorem Zeta5Irrational.U_11_2 : Uω (aρ 2) (bρ 2) (53051547 / 250000000000) ≤ -(24720375964658024966207 / 5000000000000000000000)

theorem Zeta5Irrational.U_11_3 : Uω (aρ 3) (bρ 3) (53051547 / 250000000000) ≤ -(46636055244366115624033 / 10000000000000000000000)

theorem Zeta5Irrational.U_11_4 : Uω (aρ 4) (bρ 4) (53051547 / 250000000000) ≤ -(21624996699245277221649 / 5000000000000000000000)

theorem Zeta5Irrational.U_11_5 : Uω (aρ 5) (bρ 5) (53051547 / 250000000000) ≤ -(39658512652531402453443 / 10000000000000000000000)

theorem Zeta5Irrational.U_11_6 : Uω (aρ 6) (bρ 6) (53051547 / 250000000000) ≤ -(18059438196821077208529 / 5000000000000000000000)

theorem Zeta5Irrational.U_11_7 : Uω (aρ 7) (bρ 7) (53051547 / 250000000000) ≤ -(6558653041860765113421 / 2000000000000000000000)

theorem Zeta5Irrational.U_11_8 : Uω (aρ 8) (bρ 8) (53051547 / 250000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_11_9 : Uω (aρ 9) (bρ 9) (53051547 / 250000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_11 : Uρ (53051547 / 250000000000) ≤ -(13871992575163789919237 / 5000000000000000000000)