Certified arcsine potential bounds (U14)

theorem Zeta5Irrational.U_172_1 : Uω (aρ 1) (bρ 1) (730852490563 / 6400000000000) ≤ -(22281181472692134742863 / 10000000000000000000000)

theorem Zeta5Irrational.U_172_2 : Uω (aρ 2) (bρ 2) (730852490563 / 6400000000000) ≤ -(11256214960041973685579 / 5000000000000000000000)

theorem Zeta5Irrational.U_172_3 : Uω (aρ 3) (bρ 3) (730852490563 / 6400000000000) ≤ -(1149991614237294033779 / 500000000000000000000)

theorem Zeta5Irrational.U_172_4 : Uω (aρ 4) (bρ 4) (730852490563 / 6400000000000) ≤ -(11948772902721880539821 / 5000000000000000000000)

theorem Zeta5Irrational.U_172_5 : Uω (aρ 5) (bρ 5) (730852490563 / 6400000000000) ≤ -(199755328482226702363 / 78125000000000000000)

theorem Zeta5Irrational.U_172_6 : Uω (aρ 6) (bρ 6) (730852490563 / 6400000000000) ≤ -(1840780699148846481243 / 625000000000000000000)

theorem Zeta5Irrational.U_172_7 : Uω (aρ 7) (bρ 7) (730852490563 / 6400000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_172 : Uρ (730852490563 / 6400000000000) ≤ -(23044230349968969239773 / 10000000000000000000000)

theorem Zeta5Irrational.U_173_1 : Uω (aρ 1) (bρ 1) (7330947250417 / 64000000000000) ≤ -(22248708993169244456213 / 10000000000000000000000)

theorem Zeta5Irrational.U_173_2 : Uω (aρ 2) (bρ 2) (7330947250417 / 64000000000000) ≤ -(22479171954322094534041 / 10000000000000000000000)

theorem Zeta5Irrational.U_173_3 : Uω (aρ 3) (bρ 3) (7330947250417 / 64000000000000) ≤ -(22964821159010354163667 / 10000000000000000000000)

theorem Zeta5Irrational.U_173_4 : Uω (aρ 4) (bρ 4) (7330947250417 / 64000000000000) ≤ -(23858911651480393246513 / 10000000000000000000000)

theorem Zeta5Irrational.U_173_5 : Uω (aρ 5) (bρ 5) (7330947250417 / 64000000000000) ≤ -(204172253072514234181 / 80000000000000000000)

theorem Zeta5Irrational.U_173_6 : Uω (aρ 6) (bρ 6) (7330947250417 / 64000000000000) ≤ -(5873488781927654282487 / 2000000000000000000000)

theorem Zeta5Irrational.U_173_7 : Uω (aρ 7) (bρ 7) (7330947250417 / 64000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_173 : Uρ (7330947250417 / 64000000000000) ≤ -(23029193766167760068613 / 10000000000000000000000)

theorem Zeta5Irrational.U_174_1 : Uω (aρ 1) (bρ 1) (1838342398801 / 16000000000000) ≤ -(888653665905254274529 / 400000000000000000000)

theorem Zeta5Irrational.U_174_2 : Uω (aρ 2) (bρ 2) (1838342398801 / 16000000000000) ≤ -(22446024440442051456091 / 10000000000000000000000)

theorem Zeta5Irrational.U_174_3 : Uω (aρ 3) (bρ 3) (1838342398801 / 16000000000000) ≤ -(22929933076480730785293 / 10000000000000000000000)

theorem Zeta5Irrational.U_174_4 : Uω (aρ 4) (bρ 4) (1838342398801 / 16000000000000) ≤ -(4764085982108051921477 / 2000000000000000000000)

theorem Zeta5Irrational.U_174_5 : Uω (aρ 5) (bρ 5) (1838342398801 / 16000000000000) ≤ -(12737311347516656082539 / 5000000000000000000000)

theorem Zeta5Irrational.U_174_6 : Uω (aρ 6) (bρ 6) (1838342398801 / 16000000000000) ≤ -(29283508847027304206383 / 10000000000000000000000)

theorem Zeta5Irrational.U_174_7 : Uω (aρ 7) (bρ 7) (1838342398801 / 16000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_174 : Uρ (1838342398801 / 16000000000000) ≤ -(23014280091458413181989 / 10000000000000000000000)

theorem Zeta5Irrational.U_175_1 : Uω (aρ 1) (bρ 1) (3699107142389 / 32000000000000) ≤ -(22151919650023756881351 / 10000000000000000000000)

theorem Zeta5Irrational.U_175_2 : Uω (aρ 2) (bρ 2) (3699107142389 / 32000000000000) ≤ -(11190028922637405674731 / 5000000000000000000000)

theorem Zeta5Irrational.U_175_3 : Uω (aρ 3) (bρ 3) (3699107142389 / 32000000000000) ≤ -(11430261289115545831809 / 5000000000000000000000)

theorem Zeta5Irrational.U_175_4 : Uω (aρ 4) (bρ 4) (3699107142389 / 32000000000000) ≤ -(23743918776680516836079 / 10000000000000000000000)

theorem Zeta5Irrational.U_175_5 : Uω (aρ 5) (bρ 5) (3699107142389 / 32000000000000) ≤ -(5076303731562824760583 / 2000000000000000000000)

theorem Zeta5Irrational.U_175_6 : Uω (aρ 6) (bρ 6) (3699107142389 / 32000000000000) ≤ -(14559415015712096654269 / 5000000000000000000000)

theorem Zeta5Irrational.U_175_7 : Uω (aρ 7) (bρ 7) (3699107142389 / 32000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_175_8 : Uω (aρ 8) (bρ 8) (3699107142389 / 32000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_175_9 : Uω (aρ 9) (bρ 9) (3699107142389 / 32000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_175_10 : Uω (aρ 10) (bρ 10) (3699107142389 / 32000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_175_11 : Uω (aρ 11) (bρ 11) (3699107142389 / 32000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_175_12 : Uω (aρ 12) (bρ 12) (3699107142389 / 32000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_175 : Uρ (3699107142389 / 32000000000000) ≤ -(11492404364136263761547 / 5000000000000000000000)

theorem Zeta5Irrational.U_176_1 : Uω (aρ 1) (bρ 1) (465191185897 / 4000000000000) ≤ -(22087910127931218969373 / 10000000000000000000000)

theorem Zeta5Irrational.U_176_2 : Uω (aρ 2) (bρ 2) (465191185897 / 4000000000000) ≤ -(5578631090169752076037 / 2500000000000000000000)

theorem Zeta5Irrational.U_176_3 : Uω (aρ 3) (bρ 3) (465191185897 / 4000000000000) ≤ -(22791593955763525787333 / 10000000000000000000000)

theorem Zeta5Irrational.U_176_4 : Uω (aρ 4) (bρ 4) (465191185897 / 4000000000000) ≤ -(23668002770991622080457 / 10000000000000000000000)

theorem Zeta5Irrational.U_176_5 : Uω (aρ 5) (bρ 5) (465191185897 / 4000000000000) ≤ -(6322337309009206611799 / 2500000000000000000000)

theorem Zeta5Irrational.U_176_6 : Uω (aρ 6) (bρ 6) (465191185897 / 4000000000000) ≤ -(2895818328965296759049 / 1000000000000000000000)

theorem Zeta5Irrational.U_176_7 : Uω (aρ 7) (bρ 7) (465191185897 / 4000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_176 : Uρ (465191185897 / 4000000000000) ≤ -(22955792340828882002671 / 10000000000000000000000)

theorem Zeta5Irrational.U_177_1 : Uω (aρ 1) (bρ 1) (3743951831963 / 32000000000000) ≤ -(11012153915808991134077 / 5000000000000000000000)

theorem Zeta5Irrational.U_177_2 : Uω (aρ 2) (bρ 2) (3743951831963 / 32000000000000) ≤ -(22249418326153667549627 / 10000000000000000000000)

theorem Zeta5Irrational.U_177_3 : Uω (aρ 3) (bρ 3) (3743951831963 / 32000000000000) ≤ -(1136157025908839802787 / 500000000000000000000)

theorem Zeta5Irrational.U_177_4 : Uω (aρ 4) (bρ 4) (3743951831963 / 32000000000000) ≤ -(5898168123465075345177 / 2500000000000000000000)

theorem Zeta5Irrational.U_177_5 : Uω (aρ 5) (bρ 5) (3743951831963 / 32000000000000) ≤ -(25198094437116484192507 / 10000000000000000000000)

theorem Zeta5Irrational.U_177_6 : Uω (aρ 6) (bρ 6) (3743951831963 / 32000000000000) ≤ -(14400662417436316917723 / 5000000000000000000000)

theorem Zeta5Irrational.U_177_7 : Uω (aρ 7) (bρ 7) (3743951831963 / 32000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_177_8 : Uω (aρ 8) (bρ 8) (3743951831963 / 32000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_177_9 : Uω (aρ 9) (bρ 9) (3743951831963 / 32000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_177_10 : Uω (aρ 10) (bρ 10) (3743951831963 / 32000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_177_11 : Uω (aρ 11) (bρ 11) (3743951831963 / 32000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_177_12 : Uω (aρ 12) (bρ 12) (3743951831963 / 32000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_177 : Uρ (3743951831963 / 32000000000000) ≤ -(716475289508359637971 / 312500000000000000000)

theorem Zeta5Irrational.U_178_1 : Uω (aρ 1) (bρ 1) (15065496707 / 128000000000) ≤ -(21961107610964149289349 / 10000000000000000000000)

theorem Zeta5Irrational.U_178_2 : Uω (aρ 2) (bρ 2) (15065496707 / 128000000000) ≤ -(5546183547911107213653 / 2500000000000000000000)

theorem Zeta5Irrational.U_178_3 : Uω (aρ 3) (bρ 3) (15065496707 / 128000000000) ≤ -(5663788928473910630479 / 2500000000000000000000)

theorem Zeta5Irrational.U_178_4 : Uω (aρ 4) (bρ 4) (15065496707 / 128000000000) ≤ -(23517918771318664380059 / 10000000000000000000000)

theorem Zeta5Irrational.U_178_5 : Uω (aρ 5) (bρ 5) (15065496707 / 128000000000) ≤ -(6276933735209036880089 / 2500000000000000000000)

theorem Zeta5Irrational.U_178_6 : Uω (aρ 6) (bρ 6) (15065496707 / 128000000000) ≤ -(572960694532787081867 / 200000000000000000000)

theorem Zeta5Irrational.U_178_7 : Uω (aρ 7) (bρ 7) (15065496707 / 128000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_178_8 : Uω (aρ 8) (bρ 8) (15065496707 / 128000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_178_9 : Uω (aρ 9) (bρ 9) (15065496707 / 128000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_178_10 : Uω (aρ 10) (bρ 10) (15065496707 / 128000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_178_11 : Uω (aρ 11) (bρ 11) (15065496707 / 128000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_178_12 : Uω (aρ 12) (bρ 12) (15065496707 / 128000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_178_13 : Uω (aρ 13) (bρ 13) (15065496707 / 128000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_178_14 : Uω (aρ 14) (bρ 14) (15065496707 / 128000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_178_15 : Uω (aρ 15) (bρ 15) (15065496707 / 128000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_178_16 : Uω (aρ 16) (bρ 16) (15065496707 / 128000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_178 : Uρ (15065496707 / 128000000000) ≤ -(22899039784404335583777 / 10000000000000000000000)

theorem Zeta5Irrational.U_179_1 : Uω (aρ 1) (bρ 1) (3788796521537 / 32000000000000) ≤ -(5474576103240136115701 / 2500000000000000000000)

theorem Zeta5Irrational.U_179_2 : Uω (aρ 2) (bρ 2) (3788796521537 / 32000000000000) ≤ -(11060233257341866518873 / 5000000000000000000000)

theorem Zeta5Irrational.U_179_3 : Uω (aρ 3) (bρ 3) (3788796521537 / 32000000000000) ≤ -(2258763312680448441801 / 1000000000000000000000)

theorem Zeta5Irrational.U_179_4 : Uω (aρ 4) (bρ 4) (3788796521537 / 32000000000000) ≤ -(468874652954865998573 / 200000000000000000000)

theorem Zeta5Irrational.U_179_5 : Uω (aρ 5) (bρ 5) (3788796521537 / 32000000000000) ≤ -(2501825206824387380069 / 1000000000000000000000)

theorem Zeta5Irrational.U_179_6 : Uω (aρ 6) (bρ 6) (3788796521537 / 32000000000000) ≤ -(14249056853658479258529 / 5000000000000000000000)

theorem Zeta5Irrational.U_179_7 : Uω (aρ 7) (bρ 7) (3788796521537 / 32000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_179_8 : Uω (aρ 8) (bρ 8) (3788796521537 / 32000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_179_9 : Uω (aρ 9) (bρ 9) (3788796521537 / 32000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_179_10 : Uω (aρ 10) (bρ 10) (3788796521537 / 32000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_179_11 : Uω (aρ 11) (bρ 11) (3788796521537 / 32000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_179_12 : Uω (aρ 12) (bρ 12) (3788796521537 / 32000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_179 : Uρ (3788796521537 / 32000000000000) ≤ -(11435632942680119457883 / 5000000000000000000000)

theorem Zeta5Irrational.U_180_1 : Uω (aρ 1) (bρ 1) (952804716581 / 8000000000000) ≤ -(5458973319820460563247 / 2500000000000000000000)

theorem Zeta5Irrational.U_180_2 : Uω (aρ 2) (bρ 2) (952804716581 / 8000000000000) ≤ -(11028304978811575276189 / 5000000000000000000000)

theorem Zeta5Irrational.U_180_3 : Uω (aρ 3) (bρ 3) (952804716581 / 8000000000000) ≤ -(11260283236257531228509 / 5000000000000000000000)

theorem Zeta5Irrational.U_180_4 : Uω (aρ 4) (bρ 4) (952804716581 / 8000000000000) ≤ -(23370105378852098455103 / 10000000000000000000000)

theorem Zeta5Irrational.U_180_5 : Uω (aρ 5) (bρ 5) (952804716581 / 8000000000000) ≤ -(99718511009526859259 / 40000000000000000000)

theorem Zeta5Irrational.U_180_6 : Uω (aρ 6) (bρ 6) (952804716581 / 8000000000000) ≤ -(7087845139958546029759 / 2500000000000000000000)

theorem Zeta5Irrational.U_180_7 : Uω (aρ 7) (bρ 7) (952804716581 / 8000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_180_8 : Uω (aρ 8) (bρ 8) (952804716581 / 8000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_180_9 : Uω (aρ 9) (bρ 9) (952804716581 / 8000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_180_10 : Uω (aρ 10) (bρ 10) (952804716581 / 8000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_180_11 : Uω (aρ 11) (bρ 11) (952804716581 / 8000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_180_12 : Uω (aρ 12) (bρ 12) (952804716581 / 8000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_180_13 : Uω (aρ 13) (bρ 13) (952804716581 / 8000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

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

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

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

theorem Zeta5Irrational.U_180 : Uρ (952804716581 / 8000000000000) ≤ -(5710967759615853715893 / 2500000000000000000000)

theorem Zeta5Irrational.U_181_1 : Uω (aρ 1) (bρ 1) (3833641211111 / 32000000000000) ≤ -(21773869343935046491781 / 10000000000000000000000)

theorem Zeta5Irrational.U_181_2 : Uω (aρ 2) (bρ 2) (3833641211111 / 32000000000000) ≤ -(21993159284954283541103 / 10000000000000000000000)

theorem Zeta5Irrational.U_181_3 : Uω (aρ 3) (bρ 3) (3833641211111 / 32000000000000) ≤ -(11226974797381275692259 / 5000000000000000000000)

theorem Zeta5Irrational.U_181_4 : Uω (aρ 4) (bρ 4) (3833641211111 / 32000000000000) ≤ -(1164851421249206849263 / 500000000000000000000)

theorem Zeta5Irrational.U_181_5 : Uω (aρ 5) (bρ 5) (3833641211111 / 32000000000000) ≤ -(24841844510715917490201 / 10000000000000000000000)

theorem Zeta5Irrational.U_181_6 : Uω (aρ 6) (bρ 6) (3833641211111 / 32000000000000) ≤ -(28207669885361066139551 / 10000000000000000000000)

theorem Zeta5Irrational.U_181_7 : Uω (aρ 7) (bρ 7) (3833641211111 / 32000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_181_8 : Uω (aρ 8) (bρ 8) (3833641211111 / 32000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_181_9 : Uω (aρ 9) (bρ 9) (3833641211111 / 32000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_181_10 : Uω (aρ 10) (bρ 10) (3833641211111 / 32000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_181_11 : Uω (aρ 11) (bρ 11) (3833641211111 / 32000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_181_12 : Uω (aρ 12) (bρ 12) (3833641211111 / 32000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_181 : Uρ (3833641211111 / 32000000000000) ≤ -(22816840024414922085761 / 10000000000000000000000)

theorem Zeta5Irrational.U_182_1 : Uω (aρ 1) (bρ 1) (1928031777949 / 16000000000000) ≤ -(542805695774513738577 / 250000000000000000000)

theorem Zeta5Irrational.U_182_2 : Uω (aρ 2) (bρ 2) (1928031777949 / 16000000000000) ≤ -(10965054680357433308143 / 5000000000000000000000)

theorem Zeta5Irrational.U_182_3 : Uω (aρ 3) (bρ 3) (1928031777949 / 16000000000000) ≤ -(22387776461924809992277 / 10000000000000000000000)

theorem Zeta5Irrational.U_182_4 : Uω (aρ 4) (bρ 4) (1928031777949 / 16000000000000) ≤ -(11612246722324450860351 / 5000000000000000000000)

theorem Zeta5Irrational.U_182_5 : Uω (aρ 5) (bρ 5) (1928031777949 / 16000000000000) ≤ -(6188721354787161308899 / 2500000000000000000000)

theorem Zeta5Irrational.U_182_6 : Uω (aρ 6) (bρ 6) (1928031777949 / 16000000000000) ≤ -(14033415111008318688351 / 5000000000000000000000)

theorem Zeta5Irrational.U_182_7 : Uω (aρ 7) (bρ 7) (1928031777949 / 16000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_182 : Uρ (1928031777949 / 16000000000000) ≤ -(11395079391242920398171 / 5000000000000000000000)

theorem Zeta5Irrational.U_183_1 : Uω (aρ 1) (bρ 1) (121903382671 / 1000000000000) ≤ -(431801468111400782417 / 200000000000000000000)

theorem Zeta5Irrational.U_183_2 : Uω (aρ 2) (bρ 2) (121903382671 / 1000000000000) ≤ -(10902595848206565310453 / 5000000000000000000000)

theorem Zeta5Irrational.U_183_3 : Uω (aρ 3) (bρ 3) (121903382671 / 1000000000000) ≤ -(5564184476913954951537 / 2500000000000000000000)

theorem Zeta5Irrational.U_183_4 : Uω (aρ 4) (bρ 4) (121903382671 / 1000000000000) ≤ -(23081016992543017206069 / 10000000000000000000000)

theorem Zeta5Irrational.U_183_5 : Uω (aρ 5) (bρ 5) (121903382671 / 1000000000000) ≤ -(196666997090944639807 / 80000000000000000000)

theorem Zeta5Irrational.U_183_6 : Uω (aρ 6) (bρ 6) (121903382671 / 1000000000000) ≤ -(27793218382762658487643 / 10000000000000000000000)

theorem Zeta5Irrational.U_183_7 : Uω (aρ 7) (bρ 7) (121903382671 / 1000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_183_8 : Uω (aρ 8) (bρ 8) (121903382671 / 1000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_183_9 : Uω (aρ 9) (bρ 9) (121903382671 / 1000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_183_10 : Uω (aρ 10) (bρ 10) (121903382671 / 1000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_183_11 : Uω (aρ 11) (bρ 11) (121903382671 / 1000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_183_12 : Uω (aρ 12) (bρ 12) (121903382671 / 1000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_183 : Uρ (121903382671 / 1000000000000) ≤ -(22737794411188599503227 / 10000000000000000000000)