Certified arcsine potential bounds (U01)

theorem Zeta5Irrational.U_12_1 : Uω (aρ 1) (bρ 1) (496117379 / 2000000000000) ≤ -(51279014775995128440791 / 10000000000000000000000)

theorem Zeta5Irrational.U_12_2 : Uω (aρ 2) (bρ 2) (496117379 / 2000000000000) ≤ -(3094041904103170921061 / 625000000000000000000)

theorem Zeta5Irrational.U_12_3 : Uω (aρ 3) (bρ 3) (496117379 / 2000000000000) ≤ -(23350817492635683984117 / 5000000000000000000000)

theorem Zeta5Irrational.U_12_4 : Uω (aρ 4) (bρ 4) (496117379 / 2000000000000) ≤ -(8663759421672724895473 / 2000000000000000000000)

theorem Zeta5Irrational.U_12_5 : Uω (aρ 5) (bρ 5) (496117379 / 2000000000000) ≤ -(39733556029110319524967 / 10000000000000000000000)

theorem Zeta5Irrational.U_12_6 : Uω (aρ 6) (bρ 6) (496117379 / 2000000000000) ≤ -(36207282453746924592843 / 10000000000000000000000)

theorem Zeta5Irrational.U_12_7 : Uω (aρ 7) (bρ 7) (496117379 / 2000000000000) ≤ -(32923939525185939772853 / 10000000000000000000000)

theorem Zeta5Irrational.U_12_8 : Uω (aρ 8) (bρ 8) (496117379 / 2000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_12_9 : Uω (aρ 9) (bρ 9) (496117379 / 2000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_12_10 : Uω (aρ 10) (bρ 10) (496117379 / 2000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_12_11 : Uω (aρ 11) (bρ 11) (496117379 / 2000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_12_12 : Uω (aρ 12) (bρ 12) (496117379 / 2000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_12_13 : Uω (aρ 13) (bρ 13) (496117379 / 2000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_12_14 : Uω (aρ 14) (bρ 14) (496117379 / 2000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_12_15 : Uω (aρ 15) (bρ 15) (496117379 / 2000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_12_16 : Uω (aρ 16) (bρ 16) (496117379 / 2000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_12 : Uρ (496117379 / 2000000000000) ≤ -(27776595649486878085457 / 10000000000000000000000)

theorem Zeta5Irrational.U_13_1 : Uω (aρ 1) (bρ 1) (283911191 / 1000000000000) ≤ -(25671310519013681683207 / 5000000000000000000000)

theorem Zeta5Irrational.U_13_2 : Uω (aρ 2) (bρ 2) (283911191 / 1000000000000) ≤ -(9913844635044356752717 / 2000000000000000000000)

theorem Zeta5Irrational.U_13_3 : Uω (aρ 3) (bρ 3) (283911191 / 1000000000000) ≤ -(46768288274873095600687 / 10000000000000000000000)

theorem Zeta5Irrational.U_13_4 : Uω (aρ 4) (bρ 4) (283911191 / 1000000000000) ≤ -(5423700856563990487439 / 1250000000000000000000)

theorem Zeta5Irrational.U_13_5 : Uω (aρ 5) (bρ 5) (283911191 / 1000000000000) ≤ -(39812819146312822009509 / 10000000000000000000000)

theorem Zeta5Irrational.U_13_6 : Uω (aρ 6) (bρ 6) (283911191 / 1000000000000) ≤ -(18153609865494868493647 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_13 : Uρ (283911191 / 1000000000000) ≤ -(5565255693326323982243 / 2000000000000000000000)

theorem Zeta5Irrational.U_14_1 : Uω (aρ 1) (bρ 1) (170058951 / 500000000000) ≤ -(5144324067033277739057 / 1000000000000000000000)

theorem Zeta5Irrational.U_14_2 : Uω (aρ 2) (bρ 2) (170058951 / 500000000000) ≤ -(496717399318518904317 / 100000000000000000000)

theorem Zeta5Irrational.U_14_3 : Uω (aρ 3) (bρ 3) (170058951 / 500000000000) ≤ -(1875002690401424918243 / 400000000000000000000)

theorem Zeta5Irrational.U_14_4 : Uω (aρ 4) (bρ 4) (170058951 / 500000000000) ≤ -(5438137640616013885629 / 1250000000000000000000)

theorem Zeta5Irrational.U_14_5 : Uω (aρ 5) (bρ 5) (170058951 / 500000000000) ≤ -(39947577872317960521831 / 10000000000000000000000)

theorem Zeta5Irrational.U_14_6 : Uω (aρ 6) (bρ 6) (170058951 / 500000000000) ≤ -(36504445610949767396391 / 10000000000000000000000)

theorem Zeta5Irrational.U_14_7 : Uω (aρ 7) (bρ 7) (170058951 / 500000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_14_8 : Uω (aρ 8) (bρ 8) (170058951 / 500000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_14 : Uρ (170058951 / 500000000000) ≤ -(13933261935333362960321 / 5000000000000000000000)

theorem Zeta5Irrational.U_15_1 : Uω (aρ 1) (bρ 1) (396324613 / 1000000000000) ≤ -(10308997249903148058101 / 2000000000000000000000)

theorem Zeta5Irrational.U_15_2 : Uω (aρ 2) (bρ 2) (396324613 / 1000000000000) ≤ -(24887961647494144053291 / 5000000000000000000000)

theorem Zeta5Irrational.U_15_3 : Uω (aρ 3) (bρ 3) (396324613 / 1000000000000) ≤ -(11746208074433576911541 / 2500000000000000000000)

theorem Zeta5Irrational.U_15_4 : Uω (aρ 4) (bρ 4) (396324613 / 1000000000000) ≤ -(43626843011011594664449 / 10000000000000000000000)

theorem Zeta5Irrational.U_15_5 : Uω (aρ 5) (bρ 5) (396324613 / 1000000000000) ≤ -(20049749814838098711663 / 5000000000000000000000)

theorem Zeta5Irrational.U_15_6 : Uω (aρ 6) (bρ 6) (396324613 / 1000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_15 : Uρ (396324613 / 1000000000000) ≤ -(27930518333896095285283 / 10000000000000000000000)

theorem Zeta5Irrational.U_16_1 : Uω (aρ 1) (bρ 1) (974522519 / 2000000000000) ≤ -(51712055896552965688933 / 10000000000000000000000)

theorem Zeta5Irrational.U_16_2 : Uω (aρ 2) (bρ 2) (974522519 / 2000000000000) ≤ -(49948197000145039205691 / 10000000000000000000000)

theorem Zeta5Irrational.U_16_3 : Uω (aρ 3) (bρ 3) (974522519 / 2000000000000) ≤ -(11792350042914402417241 / 2500000000000000000000)

theorem Zeta5Irrational.U_16_4 : Uω (aρ 4) (bρ 4) (974522519 / 2000000000000) ≤ -(219200189839688302473 / 50000000000000000000)

theorem Zeta5Irrational.U_16_5 : Uω (aρ 5) (bρ 5) (974522519 / 2000000000000) ≤ -(808167918466123975469 / 200000000000000000000)

theorem Zeta5Irrational.U_16_6 : Uω (aρ 6) (bρ 6) (974522519 / 2000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_16_7 : Uω (aρ 7) (bρ 7) (974522519 / 2000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_16_8 : Uω (aρ 8) (bρ 8) (974522519 / 2000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_16_9 : Uω (aρ 9) (bρ 9) (974522519 / 2000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_16_10 : Uω (aρ 10) (bρ 10) (974522519 / 2000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_16_11 : Uω (aρ 11) (bρ 11) (974522519 / 2000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_16_12 : Uω (aρ 12) (bρ 12) (974522519 / 2000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_16_13 : Uω (aρ 13) (bρ 13) (974522519 / 2000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_16_14 : Uω (aρ 14) (bρ 14) (974522519 / 2000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_16_15 : Uω (aρ 15) (bρ 15) (974522519 / 2000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_16_16 : Uω (aρ 16) (bρ 16) (974522519 / 2000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_16 : Uρ (974522519 / 2000000000000) ≤ -(27979010994860448204283 / 10000000000000000000000)

theorem Zeta5Irrational.U_17_1 : Uω (aρ 1) (bρ 1) (289098953 / 500000000000) ≤ -(1037645395330397781579 / 200000000000000000000)

theorem Zeta5Irrational.U_17_2 : Uω (aρ 2) (bρ 2) (289098953 / 500000000000) ≤ -(50125360529440552437197 / 10000000000000000000000)

theorem Zeta5Irrational.U_17_3 : Uω (aρ 3) (bρ 3) (289098953 / 500000000000) ≤ -(47363740868116265483369 / 10000000000000000000000)

theorem Zeta5Irrational.U_17_4 : Uω (aρ 4) (bρ 4) (289098953 / 500000000000) ≤ -(11019964131301389298539 / 2500000000000000000000)

theorem Zeta5Irrational.U_17_5 : Uω (aρ 5) (bρ 5) (289098953 / 500000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_17_6 : Uω (aρ 6) (bρ 6) (289098953 / 500000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_17_7 : Uω (aρ 7) (bρ 7) (289098953 / 500000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_17_8 : Uω (aρ 8) (bρ 8) (289098953 / 500000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_17 : Uρ (289098953 / 500000000000) ≤ -(14029924784689781065817 / 5000000000000000000000)

theorem Zeta5Irrational.U_18_1 : Uω (aρ 1) (bρ 1) (729961631 / 1000000000000) ≤ -(52173705525642853674791 / 10000000000000000000000)

theorem Zeta5Irrational.U_18_2 : Uω (aρ 2) (bρ 2) (729961631 / 1000000000000) ≤ -(157603058690652939389 / 31250000000000000000)

theorem Zeta5Irrational.U_18_3 : Uω (aρ 3) (bρ 3) (729961631 / 1000000000000) ≤ -(5964321618170938271907 / 1250000000000000000000)

theorem Zeta5Irrational.U_18_4 : Uω (aρ 4) (bρ 4) (729961631 / 1000000000000) ≤ -(44582338407334756483981 / 10000000000000000000000)

theorem Zeta5Irrational.U_18_5 : Uω (aρ 5) (bρ 5) (729961631 / 1000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_18_6 : Uω (aρ 6) (bρ 6) (729961631 / 1000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_18 : Uρ (729961631 / 1000000000000) ≤ -(1124651582364191246041 / 400000000000000000000)

theorem Zeta5Irrational.U_19_1 : Uω (aρ 1) (bρ 1) (1611686987 / 2000000000000) ≤ -(26161527144129535042071 / 5000000000000000000000)

theorem Zeta5Irrational.U_19_2 : Uω (aρ 2) (bρ 2) (1611686987 / 2000000000000) ≤ -(10118588778586567237301 / 2000000000000000000000)

theorem Zeta5Irrational.U_19_3 : Uω (aρ 3) (bρ 3) (1611686987 / 2000000000000) ≤ -(47905346243074077148493 / 10000000000000000000000)

theorem Zeta5Irrational.U_19_4 : Uω (aρ 4) (bρ 4) (1611686987 / 2000000000000) ≤ -(8987625693749818873013 / 2000000000000000000000)

theorem Zeta5Irrational.U_19_5 : Uω (aρ 5) (bρ 5) (1611686987 / 2000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_19_6 : Uω (aρ 6) (bρ 6) (1611686987 / 2000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_19_7 : Uω (aρ 7) (bρ 7) (1611686987 / 2000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_19_8 : Uω (aρ 8) (bρ 8) (1611686987 / 2000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_19_9 : Uω (aρ 9) (bρ 9) (1611686987 / 2000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_19_10 : Uω (aρ 10) (bρ 10) (1611686987 / 2000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_19_11 : Uω (aρ 11) (bρ 11) (1611686987 / 2000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_19_12 : Uω (aρ 12) (bρ 12) (1611686987 / 2000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_19_13 : Uω (aρ 13) (bρ 13) (1611686987 / 2000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_19_14 : Uω (aρ 14) (bρ 14) (1611686987 / 2000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_19_15 : Uω (aρ 15) (bρ 15) (1611686987 / 2000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_19_16 : Uω (aρ 16) (bρ 16) (1611686987 / 2000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_19 : Uρ (1611686987 / 2000000000000) ≤ -(1126058948715908662283 / 400000000000000000000)

theorem Zeta5Irrational.U_20_1 : Uω (aρ 1) (bρ 1) (220431339 / 250000000000) ≤ -(10494988835400103718169 / 2000000000000000000000)

theorem Zeta5Irrational.U_20_2 : Uω (aρ 2) (bρ 2) (220431339 / 250000000000) ≤ -(50757420127736585768143 / 10000000000000000000000)

theorem Zeta5Irrational.U_20_3 : Uω (aρ 3) (bρ 3) (220431339 / 250000000000) ≤ -(24054501625710163523737 / 5000000000000000000000)

theorem Zeta5Irrational.U_20_4 : Uω (aρ 4) (bρ 4) (220431339 / 250000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_20_5 : Uω (aρ 5) (bρ 5) (220431339 / 250000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_20_6 : Uω (aρ 6) (bρ 6) (220431339 / 250000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_20_7 : Uω (aρ 7) (bρ 7) (220431339 / 250000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_20 : Uρ (220431339 / 250000000000) ≤ -(7054177370793323835461 / 2500000000000000000000)

theorem Zeta5Irrational.U_21_1 : Uω (aρ 1) (bρ 1) (4047462733 / 4000000000000) ≤ -(329635258503986697477 / 62500000000000000000)

theorem Zeta5Irrational.U_21_2 : Uω (aρ 2) (bρ 2) (4047462733 / 4000000000000) ≤ -(25525528995361187317657 / 5000000000000000000000)

theorem Zeta5Irrational.U_21_3 : Uω (aρ 3) (bρ 3) (4047462733 / 4000000000000) ≤ -(48497352170934822805119 / 10000000000000000000000)

theorem Zeta5Irrational.U_21_4 : Uω (aρ 4) (bρ 4) (4047462733 / 4000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_21_5 : Uω (aρ 5) (bρ 5) (4047462733 / 4000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_21_6 : Uω (aρ 6) (bρ 6) (4047462733 / 4000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_21 : Uρ (4047462733 / 4000000000000) ≤ -(28244841495459020605873 / 10000000000000000000000)

theorem Zeta5Irrational.U_22_1 : Uω (aρ 1) (bρ 1) (2284012021 / 2000000000000) ≤ -(2650831856230185575557 / 500000000000000000000)

theorem Zeta5Irrational.U_22_2 : Uω (aρ 2) (bρ 2) (2284012021 / 2000000000000) ≤ -(51361201358950362094901 / 10000000000000000000000)

theorem Zeta5Irrational.U_22_3 : Uω (aρ 3) (bρ 3) (2284012021 / 2000000000000) ≤ -(979184520167902038687 / 200000000000000000000)

theorem Zeta5Irrational.U_22_4 : Uω (aρ 4) (bρ 4) (2284012021 / 2000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_22_5 : Uω (aρ 5) (bρ 5) (2284012021 / 2000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_22_6 : Uω (aρ 6) (bρ 6) (2284012021 / 2000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_22_7 : Uω (aρ 7) (bρ 7) (2284012021 / 2000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_22_8 : Uω (aρ 8) (bρ 8) (2284012021 / 2000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_22_9 : Uω (aρ 9) (bρ 9) (2284012021 / 2000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_22_10 : Uω (aρ 10) (bρ 10) (2284012021 / 2000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_22_11 : Uω (aρ 11) (bρ 11) (2284012021 / 2000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_22_12 : Uω (aρ 12) (bρ 12) (2284012021 / 2000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_22_13 : Uω (aρ 13) (bρ 13) (2284012021 / 2000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_22_14 : Uω (aρ 14) (bρ 14) (2284012021 / 2000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_22_15 : Uω (aρ 15) (bρ 15) (2284012021 / 2000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_22_16 : Uω (aρ 16) (bρ 16) (2284012021 / 2000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_22 : Uρ (2284012021 / 2000000000000) ≤ -(2827670396385794487423 / 1000000000000000000000)

theorem Zeta5Irrational.U_23_1 : Uω (aρ 1) (bρ 1) (5088585351 / 4000000000000) ≤ -(26650264330778109932447 / 5000000000000000000000)

theorem Zeta5Irrational.U_23_2 : Uω (aρ 2) (bρ 2) (5088585351 / 4000000000000) ≤ -(206762531076714809157 / 40000000000000000000)

theorem Zeta5Irrational.U_23_3 : Uω (aρ 3) (bρ 3) (5088585351 / 4000000000000) ≤ -(49562765747407728412987 / 10000000000000000000000)

theorem Zeta5Irrational.U_23_4 : Uω (aρ 4) (bρ 4) (5088585351 / 4000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_23_5 : Uω (aρ 5) (bρ 5) (5088585351 / 4000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_23_6 : Uω (aρ 6) (bρ 6) (5088585351 / 4000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_23 : Uρ (5088585351 / 4000000000000) ≤ -(14157655382134504069693 / 5000000000000000000000)