Certified arcsine potential bounds (U34)

theorem Zeta5Irrational.U_412_1 : Uω (aρ 1) (bρ 1) (441401103427 / 1000000000000) ≤ -(8325295657190344060219 / 10000000000000000000000)

theorem Zeta5Irrational.U_412_2 : Uω (aρ 2) (bρ 2) (441401103427 / 1000000000000) ≤ -(335222984107915235267 / 400000000000000000000)

theorem Zeta5Irrational.U_412_3 : Uω (aρ 3) (bρ 3) (441401103427 / 1000000000000) ≤ -(8492201232119775677881 / 10000000000000000000000)

theorem Zeta5Irrational.U_412_4 : Uω (aρ 4) (bρ 4) (441401103427 / 1000000000000) ≤ -(4340422539223208551097 / 5000000000000000000000)

theorem Zeta5Irrational.U_412_5 : Uω (aρ 5) (bρ 5) (441401103427 / 1000000000000) ≤ -(4488166174250952639887 / 5000000000000000000000)

theorem Zeta5Irrational.U_412_6 : Uω (aρ 6) (bρ 6) (441401103427 / 1000000000000) ≤ -(470947097206575796623 / 500000000000000000000)

theorem Zeta5Irrational.U_412_7 : Uω (aρ 7) (bρ 7) (441401103427 / 1000000000000) ≤ -(10063552978277690335471 / 10000000000000000000000)

theorem Zeta5Irrational.U_412_8 : Uω (aρ 8) (bρ 8) (441401103427 / 1000000000000) ≤ -(274774647827680332549 / 250000000000000000000)

theorem Zeta5Irrational.U_412_9 : Uω (aρ 9) (bρ 9) (441401103427 / 1000000000000) ≤ -(1234130017850107135807 / 1000000000000000000000)

theorem Zeta5Irrational.U_412_10 : Uω (aρ 10) (bρ 10) (441401103427 / 1000000000000) ≤ -(14443658687485022068619 / 10000000000000000000000)

theorem Zeta5Irrational.U_412_11 : Uω (aρ 11) (bρ 11) (441401103427 / 1000000000000) ≤ -(19162436512716292548947 / 10000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_412 : Uρ (441401103427 / 1000000000000) ≤ -(6106371938425516455039 / 5000000000000000000000)

theorem Zeta5Irrational.U_413_1 : Uω (aρ 1) (bρ 1) (885450806607 / 2000000000000) ≤ -(829489431824442098373 / 1000000000000000000000)

theorem Zeta5Irrational.U_413_2 : Uω (aρ 2) (bρ 2) (885450806607 / 2000000000000) ≤ -(417500176740119125927 / 500000000000000000000)

theorem Zeta5Irrational.U_413_3 : Uω (aρ 3) (bρ 3) (885450806607 / 2000000000000) ≤ -(1692256610190248951243 / 2000000000000000000000)

theorem Zeta5Irrational.U_413_4 : Uω (aρ 4) (bρ 4) (885450806607 / 2000000000000) ≤ -(1729865328848618984599 / 2000000000000000000000)

theorem Zeta5Irrational.U_413_5 : Uω (aρ 5) (bρ 5) (885450806607 / 2000000000000) ≤ -(8943837665525954089233 / 10000000000000000000000)

theorem Zeta5Irrational.U_413_6 : Uω (aρ 6) (bρ 6) (885450806607 / 2000000000000) ≤ -(9384896663309727471479 / 10000000000000000000000)

theorem Zeta5Irrational.U_413_7 : Uω (aρ 7) (bρ 7) (885450806607 / 2000000000000) ≤ -(10027038309970569596151 / 10000000000000000000000)

theorem Zeta5Irrational.U_413_8 : Uω (aρ 8) (bρ 8) (885450806607 / 2000000000000) ≤ -(10950399669358784600239 / 10000000000000000000000)

theorem Zeta5Irrational.U_413_9 : Uω (aρ 9) (bρ 9) (885450806607 / 2000000000000) ≤ -(6146682270563129851507 / 5000000000000000000000)

theorem Zeta5Irrational.U_413_10 : Uω (aρ 10) (bρ 10) (885450806607 / 2000000000000) ≤ -(3594754308831076809627 / 2500000000000000000000)

theorem Zeta5Irrational.U_413_11 : Uω (aρ 11) (bρ 11) (885450806607 / 2000000000000) ≤ -(18974596681744203262247 / 10000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_413 : Uρ (885450806607 / 2000000000000) ≤ -(1217216813364887052379 / 1000000000000000000000)

theorem Zeta5Irrational.U_414_1 : Uω (aρ 1) (bρ 1) (22202485159 / 50000000000) ≤ -(8264585124940494284273 / 10000000000000000000000)

theorem Zeta5Irrational.U_414_2 : Uω (aρ 2) (bρ 2) (22202485159 / 50000000000) ≤ -(8319525651625783148213 / 10000000000000000000000)

theorem Zeta5Irrational.U_414_3 : Uω (aρ 3) (bρ 3) (22202485159 / 50000000000) ≤ -(4215230103394798454407 / 5000000000000000000000)

theorem Zeta5Irrational.U_414_4 : Uω (aρ 4) (bρ 4) (22202485159 / 50000000000) ≤ -(8617907356384918787213 / 10000000000000000000000)

theorem Zeta5Irrational.U_414_5 : Uω (aρ 5) (bρ 5) (22202485159 / 50000000000) ≤ -(8911448565837778337919 / 10000000000000000000000)

theorem Zeta5Irrational.U_414_6 : Uω (aρ 6) (bρ 6) (22202485159 / 50000000000) ≤ -(9350967824237916076221 / 10000000000000000000000)

theorem Zeta5Irrational.U_414_7 : Uω (aρ 7) (bρ 7) (22202485159 / 50000000000) ≤ -(4995329531900420707149 / 5000000000000000000000)

theorem Zeta5Irrational.U_414_8 : Uω (aρ 8) (bρ 8) (22202485159 / 50000000000) ≤ -(10909985018713567947419 / 10000000000000000000000)

theorem Zeta5Irrational.U_414_9 : Uω (aρ 9) (bρ 9) (22202485159 / 50000000000) ≤ -(191338797200200775319 / 156250000000000000000)

theorem Zeta5Irrational.U_414_10 : Uω (aρ 10) (bρ 10) (22202485159 / 50000000000) ≤ -(286298355615774617203 / 200000000000000000000)

theorem Zeta5Irrational.U_414_11 : Uω (aρ 11) (bρ 11) (22202485159 / 50000000000) ≤ -(3759439815845592521937 / 2000000000000000000000)

theorem Zeta5Irrational.U_414_12 : Uω (aρ 12) (bρ 12) (22202485159 / 50000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_414_13 : Uω (aρ 13) (bρ 13) (22202485159 / 50000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_414_14 : Uω (aρ 14) (bρ 14) (22202485159 / 50000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_414_15 : Uω (aρ 15) (bρ 15) (22202485159 / 50000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_414_16 : Uω (aρ 16) (bρ 16) (22202485159 / 50000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_414 : Uρ (22202485159 / 50000000000) ≤ -(485301670043732980539 / 400000000000000000000)

theorem Zeta5Irrational.U_415_1 : Uω (aρ 1) (bρ 1) (890748006113 / 2000000000000) ≤ -(2058591880093690254427 / 2500000000000000000000)

theorem Zeta5Irrational.U_415_2 : Uω (aρ 2) (bρ 2) (890748006113 / 2000000000000) ≤ -(4144570193375825698037 / 5000000000000000000000)

theorem Zeta5Irrational.U_415_3 : Uω (aρ 3) (bρ 3) (890748006113 / 2000000000000) ≤ -(4199866056630123266719 / 5000000000000000000000)

theorem Zeta5Irrational.U_415_4 : Uω (aρ 4) (bρ 4) (890748006113 / 2000000000000) ≤ -(8586586592335453971777 / 10000000000000000000000)

theorem Zeta5Irrational.U_415_5 : Uω (aρ 5) (bρ 5) (890748006113 / 2000000000000) ≤ -(34684235794435448991 / 39062500000000000000)

theorem Zeta5Irrational.U_415_6 : Uω (aρ 6) (bρ 6) (890748006113 / 2000000000000) ≤ -(4658577313435840435391 / 5000000000000000000000)

theorem Zeta5Irrational.U_415_7 : Uω (aρ 7) (bρ 7) (890748006113 / 2000000000000) ≤ -(9954414220290087389677 / 10000000000000000000000)

theorem Zeta5Irrational.U_415_8 : Uω (aρ 8) (bρ 8) (890748006113 / 2000000000000) ≤ -(5434870227411690620931 / 5000000000000000000000)

theorem Zeta5Irrational.U_415_9 : Uω (aρ 9) (bρ 9) (890748006113 / 2000000000000) ≤ -(12198252685595503436989 / 10000000000000000000000)

theorem Zeta5Irrational.U_415_10 : Uω (aρ 10) (bρ 10) (890748006113 / 2000000000000) ≤ -(1781418685494105864799 / 1250000000000000000000)

theorem Zeta5Irrational.U_415_11 : Uω (aρ 11) (bρ 11) (890748006113 / 2000000000000) ≤ -(9314361252783403192807 / 5000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_415 : Uρ (890748006113 / 2000000000000) ≤ -(12093743108271133476063 / 10000000000000000000000)

theorem Zeta5Irrational.U_416_1 : Uω (aρ 1) (bρ 1) (446698302933 / 1000000000000) ≤ -(8204240952676966510493 / 10000000000000000000000)

theorem Zeta5Irrational.U_416_2 : Uω (aρ 2) (bρ 2) (446698302933 / 1000000000000) ≤ -(1032355897364107694117 / 1250000000000000000000)

theorem Zeta5Irrational.U_416_3 : Uω (aρ 3) (bρ 3) (446698302933 / 1000000000000) ≤ -(8369098189383941263791 / 10000000000000000000000)

theorem Zeta5Irrational.U_416_4 : Uω (aρ 4) (bρ 4) (446698302933 / 1000000000000) ≤ -(8555363735410042263653 / 10000000000000000000000)

theorem Zeta5Irrational.U_416_5 : Uω (aρ 5) (bρ 5) (446698302933 / 1000000000000) ≤ -(884698437876299503827 / 1000000000000000000000)

theorem Zeta5Irrational.U_416_6 : Uω (aρ 6) (bρ 6) (446698302933 / 1000000000000) ≤ -(9283456279446531117199 / 10000000000000000000000)

theorem Zeta5Irrational.U_416_7 : Uω (aρ 7) (bρ 7) (446698302933 / 1000000000000) ≤ -(2479575692907522664859 / 2500000000000000000000)

theorem Zeta5Irrational.U_416_8 : Uω (aρ 8) (bρ 8) (446698302933 / 1000000000000) ≤ -(2165932898364507387119 / 2000000000000000000000)

theorem Zeta5Irrational.U_416_9 : Uω (aρ 9) (bρ 9) (446698302933 / 1000000000000) ≤ -(12151070657503466858303 / 10000000000000000000000)

theorem Zeta5Irrational.U_416_10 : Uω (aρ 10) (bρ 10) (446698302933 / 1000000000000) ≤ -(3547075465469153810511 / 2500000000000000000000)

theorem Zeta5Irrational.U_416_11 : Uω (aρ 11) (bρ 11) (446698302933 / 1000000000000) ≤ -(738719378596878066367 / 400000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_416 : Uρ (446698302933 / 1000000000000) ≤ -(1506959668461532668943 / 1250000000000000000000)

theorem Zeta5Irrational.U_417_1 : Uω (aρ 1) (bρ 1) (896045205619 / 2000000000000) ≤ -(2043551218737480737427 / 2500000000000000000000)

theorem Zeta5Irrational.U_417_2 : Uω (aρ 2) (bρ 2) (896045205619 / 2000000000000) ≤ -(2057161367982340828791 / 2500000000000000000000)

theorem Zeta5Irrational.U_417_3 : Uω (aρ 3) (bρ 3) (896045205619 / 2000000000000) ≤ -(833855785951075132007 / 1000000000000000000000)

theorem Zeta5Irrational.U_417_4 : Uω (aρ 4) (bρ 4) (896045205619 / 2000000000000) ≤ -(1704847634940521090967 / 2000000000000000000000)

theorem Zeta5Irrational.U_417_5 : Uω (aρ 5) (bρ 5) (896045205619 / 2000000000000) ≤ -(1101863492402909633239 / 1250000000000000000000)

theorem Zeta5Irrational.U_417_6 : Uω (aρ 6) (bρ 6) (896045205619 / 2000000000000) ≤ -(9249871998363191376847 / 10000000000000000000000)

theorem Zeta5Irrational.U_417_7 : Uω (aρ 7) (bρ 7) (896045205619 / 2000000000000) ≤ -(494116186075126798691 / 500000000000000000000)

theorem Zeta5Irrational.U_417_8 : Uω (aρ 8) (bρ 8) (896045205619 / 2000000000000) ≤ -(10789755663946743181419 / 10000000000000000000000)

theorem Zeta5Irrational.U_417_9 : Uω (aρ 9) (bρ 9) (896045205619 / 2000000000000) ≤ -(756508381948669364161 / 625000000000000000000)

theorem Zeta5Irrational.U_417_10 : Uω (aρ 10) (bρ 10) (896045205619 / 2000000000000) ≤ -(2825152954444311047283 / 2000000000000000000000)

theorem Zeta5Irrational.U_417_11 : Uω (aρ 11) (bρ 11) (896045205619 / 2000000000000) ≤ -(3662808807969156807193 / 2000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_417 : Uρ (896045205619 / 2000000000000) ≤ -(2403653742116277630583 / 2000000000000000000000)

theorem Zeta5Irrational.U_418_1 : Uω (aρ 1) (bρ 1) (1794739010991 / 4000000000000) ≤ -(326368824010608195853 / 400000000000000000000)

theorem Zeta5Irrational.U_418_2 : Uω (aρ 2) (bρ 2) (1794739010991 / 4000000000000) ≤ -(4106789379413987168301 / 5000000000000000000000)

theorem Zeta5Irrational.U_418_3 : Uω (aρ 3) (bρ 3) (1794739010991 / 4000000000000) ≤ -(8323322613875938862681 / 10000000000000000000000)

theorem Zeta5Irrational.U_418_4 : Uω (aρ 4) (bρ 4) (1794739010991 / 4000000000000) ≤ -(8508711691084804030819 / 10000000000000000000000)

theorem Zeta5Irrational.U_418_5 : Uω (aρ 5) (bρ 5) (1794739010991 / 4000000000000) ≤ -(2199727085099057476111 / 2500000000000000000000)

theorem Zeta5Irrational.U_418_6 : Uω (aρ 6) (bρ 6) (1794739010991 / 4000000000000) ≤ -(4616561195014913821701 / 5000000000000000000000)

theorem Zeta5Irrational.U_418_7 : Uω (aρ 7) (bρ 7) (1794739010991 / 4000000000000) ≤ -(4932191768818572964023 / 5000000000000000000000)

theorem Zeta5Irrational.U_418_8 : Uω (aρ 8) (bρ 8) (1794739010991 / 4000000000000) ≤ -(2153972694606828066529 / 2000000000000000000000)

theorem Zeta5Irrational.U_418_9 : Uω (aρ 9) (bρ 9) (1794739010991 / 4000000000000) ≤ -(12080757024811163845657 / 10000000000000000000000)

theorem Zeta5Irrational.U_418_10 : Uω (aρ 10) (bρ 10) (1794739010991 / 4000000000000) ≤ -(14094684596889839880361 / 10000000000000000000000)

theorem Zeta5Irrational.U_418_11 : Uω (aρ 11) (bρ 11) (1794739010991 / 4000000000000) ≤ -(18239378751248439378963 / 10000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_418 : Uρ (1794739010991 / 4000000000000) ≤ -(599989554116664840691 / 500000000000000000000)

theorem Zeta5Irrational.U_419_1 : Uω (aρ 1) (bρ 1) (224673451343 / 500000000000) ≤ -(2036064686302483332461 / 2500000000000000000000)

theorem Zeta5Irrational.U_419_2 : Uω (aρ 2) (bρ 2) (224673451343 / 500000000000) ≤ -(8198534714646879541903 / 10000000000000000000000)

theorem Zeta5Irrational.U_419_3 : Uω (aρ 3) (bρ 3) (224673451343 / 500000000000) ≤ -(4154055276627529415703 / 5000000000000000000000)

theorem Zeta5Irrational.U_419_4 : Uω (aρ 4) (bρ 4) (224673451343 / 500000000000) ≤ -(53082558156334955823 / 62500000000000000000)

theorem Zeta5Irrational.U_419_5 : Uω (aρ 5) (bρ 5) (224673451343 / 500000000000) ≤ -(2195733594623203264179 / 2500000000000000000000)

theorem Zeta5Irrational.U_419_6 : Uω (aρ 6) (bρ 6) (224673451343 / 500000000000) ≤ -(92164010080748980551 / 100000000000000000000)

theorem Zeta5Irrational.U_419_7 : Uω (aρ 7) (bρ 7) (224673451343 / 500000000000) ≤ -(9846476084902234316057 / 10000000000000000000000)

theorem Zeta5Irrational.U_419_8 : Uω (aρ 8) (bρ 8) (224673451343 / 500000000000) ≤ -(2687503131290268703811 / 2500000000000000000000)

theorem Zeta5Irrational.U_419_9 : Uω (aρ 9) (bρ 9) (224673451343 / 500000000000) ≤ -(1507180034067428396347 / 1250000000000000000000)

theorem Zeta5Irrational.U_419_10 : Uω (aρ 10) (bρ 10) (224673451343 / 500000000000) ≤ -(7031864198912791906271 / 5000000000000000000000)

theorem Zeta5Irrational.U_419_11 : Uω (aρ 11) (bρ 11) (224673451343 / 500000000000) ≤ -(9083068948402617052851 / 5000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_419 : Uρ (224673451343 / 500000000000) ≤ -(2396291097251474981877 / 2000000000000000000000)

theorem Zeta5Irrational.U_420_1 : Uω (aρ 1) (bρ 1) (1800036210497 / 4000000000000) ≤ -(4064659621397125910963 / 5000000000000000000000)

theorem Zeta5Irrational.U_420_2 : Uω (aρ 2) (bρ 2) (1800036210497 / 4000000000000) ≤ -(4091756635633582914549 / 5000000000000000000000)

theorem Zeta5Irrational.U_420_3 : Uω (aρ 3) (bρ 3) (1800036210497 / 4000000000000) ≤ -(8292921607161953238429 / 10000000000000000000000)

theorem Zeta5Irrational.U_420_4 : Uω (aρ 4) (bρ 4) (1800036210497 / 4000000000000) ≤ -(1059716367714879467071 / 1250000000000000000000)

theorem Zeta5Irrational.U_420_5 : Uω (aρ 5) (bρ 5) (1800036210497 / 4000000000000) ≤ -(1753397194246807411647 / 2000000000000000000000)

theorem Zeta5Irrational.U_420_6 : Uω (aρ 6) (bρ 6) (1800036210497 / 4000000000000) ≤ -(183994155135901900949 / 200000000000000000000)

theorem Zeta5Irrational.U_420_7 : Uω (aρ 7) (bρ 7) (1800036210497 / 4000000000000) ≤ -(9828601241911390730523 / 10000000000000000000000)

theorem Zeta5Irrational.U_420_8 : Uω (aρ 8) (bρ 8) (1800036210497 / 4000000000000) ≤ -(1073020264259629767199 / 1000000000000000000000)

theorem Zeta5Irrational.U_420_9 : Uω (aρ 9) (bρ 9) (1800036210497 / 4000000000000) ≤ -(12034183515403065078679 / 10000000000000000000000)

theorem Zeta5Irrational.U_420_10 : Uω (aρ 10) (bρ 10) (1800036210497 / 4000000000000) ≤ -(561315799852319578607 / 400000000000000000000)

theorem Zeta5Irrational.U_420_11 : Uω (aρ 11) (bρ 11) (1800036210497 / 4000000000000) ≤ -(18094246652620039559979 / 10000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_420 : Uρ (1800036210497 / 4000000000000) ≤ -(5981627919399893279119 / 5000000000000000000000)

theorem Zeta5Irrational.U_421_1 : Uω (aρ 1) (bρ 1) (7210739241 / 16000000000) ≤ -(8114402026328109846991 / 10000000000000000000000)

theorem Zeta5Irrational.U_421_2 : Uω (aρ 2) (bρ 2) (7210739241 / 16000000000) ≤ -(4084257180438267317039 / 5000000000000000000000)

theorem Zeta5Irrational.U_421_3 : Uω (aρ 3) (bρ 3) (7210739241 / 16000000000) ≤ -(8277755705431535785367 / 10000000000000000000000)

theorem Zeta5Irrational.U_421_4 : Uω (aρ 4) (bρ 4) (7210739241 / 16000000000) ≤ -(67698212214232369843 / 80000000000000000000)

theorem Zeta5Irrational.U_421_5 : Uω (aρ 5) (bρ 5) (7210739241 / 16000000000) ≤ -(8751063036737577972069 / 10000000000000000000000)

theorem Zeta5Irrational.U_421_6 : Uω (aρ 6) (bρ 6) (7210739241 / 16000000000) ≤ -(2295760635244161997167 / 2500000000000000000000)

theorem Zeta5Irrational.U_421_7 : Uω (aρ 7) (bρ 7) (7210739241 / 16000000000) ≤ -(306586215248868418239 / 312500000000000000000)

theorem Zeta5Irrational.U_421_8 : Uω (aρ 8) (bρ 8) (7210739241 / 16000000000) ≤ -(1338804206099587571027 / 1250000000000000000000)

theorem Zeta5Irrational.U_421_9 : Uω (aρ 9) (bρ 9) (7210739241 / 16000000000) ≤ -(12010986417487087268443 / 10000000000000000000000)

theorem Zeta5Irrational.U_421_10 : Uω (aρ 10) (bρ 10) (7210739241 / 16000000000) ≤ -(350054580804219201741 / 250000000000000000000)

theorem Zeta5Irrational.U_421_11 : Uω (aρ 11) (bρ 11) (7210739241 / 16000000000) ≤ -(4505909143362031622123 / 2500000000000000000000)

theorem Zeta5Irrational.U_421_12 : Uω (aρ 12) (bρ 12) (7210739241 / 16000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_421_13 : Uω (aρ 13) (bρ 13) (7210739241 / 16000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_421_14 : Uω (aρ 14) (bρ 14) (7210739241 / 16000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_421_15 : Uω (aρ 15) (bρ 15) (7210739241 / 16000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_421_16 : Uω (aρ 16) (bρ 16) (7210739241 / 16000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_421 : Uρ (7210739241 / 16000000000) ≤ -(11945186561807156496291 / 10000000000000000000000)

theorem Zeta5Irrational.U_422_1 : Uω (aρ 1) (bρ 1) (1805333410003 / 4000000000000) ≤ -(2024876757354868561347 / 2500000000000000000000)

theorem Zeta5Irrational.U_422_2 : Uω (aρ 2) (bρ 2) (1805333410003 / 4000000000000) ≤ -(1630707583193492241937 / 2000000000000000000000)

theorem Zeta5Irrational.U_422_3 : Uω (aρ 3) (bρ 3) (1805333410003 / 4000000000000) ≤ -(4131306389108922398569 / 5000000000000000000000)

theorem Zeta5Irrational.U_422_4 : Uω (aρ 4) (bρ 4) (1805333410003 / 4000000000000) ≤ -(8446845986117236546949 / 10000000000000000000000)

theorem Zeta5Irrational.U_422_5 : Uω (aρ 5) (bρ 5) (1805333410003 / 4000000000000) ≤ -(8735165493515219476671 / 10000000000000000000000)

theorem Zeta5Irrational.U_422_6 : Uω (aρ 6) (bρ 6) (1805333410003 / 4000000000000) ≤ -(9166405265891975863527 / 10000000000000000000000)

theorem Zeta5Irrational.U_422_7 : Uω (aρ 7) (bρ 7) (1805333410003 / 4000000000000) ≤ -(4896474451519480225219 / 5000000000000000000000)

theorem Zeta5Irrational.U_422_8 : Uω (aρ 8) (bρ 8) (1805333410003 / 4000000000000) ≤ -(10690705368396436709341 / 10000000000000000000000)

theorem Zeta5Irrational.U_422_9 : Uω (aρ 9) (bρ 9) (1805333410003 / 4000000000000) ≤ -(5993924322941902594337 / 5000000000000000000000)

theorem Zeta5Irrational.U_422_10 : Uω (aρ 10) (bρ 10) (1805333410003 / 4000000000000) ≤ -(2794318392676469736287 / 2000000000000000000000)

theorem Zeta5Irrational.U_422_11 : Uω (aρ 11) (bρ 11) (1805333410003 / 4000000000000) ≤ -(3590848971023895272907 / 2000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_422 : Uρ (1805333410003 / 4000000000000) ≤ -(11927242524291849257171 / 10000000000000000000000)

theorem Zeta5Irrational.U_423_1 : Uω (aρ 1) (bρ 1) (451995502439 / 1000000000000) ≤ -(4042317092986279800841 / 5000000000000000000000)

theorem Zeta5Irrational.U_423_2 : Uω (aρ 2) (bρ 2) (451995502439 / 1000000000000) ≤ -(4069291934667686941101 / 5000000000000000000000)

theorem Zeta5Irrational.U_423_3 : Uω (aρ 3) (bρ 3) (451995502439 / 1000000000000) ≤ -(4123746377996051450701 / 5000000000000000000000)

theorem Zeta5Irrational.U_423_4 : Uω (aρ 4) (bρ 4) (451995502439 / 1000000000000) ≤ -(4215719623000383988557 / 5000000000000000000000)

theorem Zeta5Irrational.U_423_5 : Uω (aρ 5) (bρ 5) (451995502439 / 1000000000000) ≤ -(1743858652094064989949 / 2000000000000000000000)

theorem Zeta5Irrational.U_423_6 : Uω (aρ 6) (bρ 6) (451995502439 / 1000000000000) ≤ -(914979583729635317381 / 1000000000000000000000)

theorem Zeta5Irrational.U_423_7 : Uω (aρ 7) (bρ 7) (451995502439 / 1000000000000) ≤ -(9775171167791601484043 / 10000000000000000000000)

theorem Zeta5Irrational.U_423_8 : Uω (aρ 8) (bρ 8) (451995502439 / 1000000000000) ≤ -(1067101762719614924343 / 1000000000000000000000)

theorem Zeta5Irrational.U_423_9 : Uω (aρ 9) (bρ 9) (451995502439 / 1000000000000) ≤ -(239295397413106100289 / 200000000000000000000)

theorem Zeta5Irrational.U_423_10 : Uω (aρ 10) (bρ 10) (451995502439 / 1000000000000) ≤ -(6970560032833848866531 / 5000000000000000000000)

theorem Zeta5Irrational.U_423_11 : Uω (aρ 11) (bρ 11) (451995502439 / 1000000000000) ≤ -(4471503425795417789409 / 2500000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_423 : Uρ (451995502439 / 1000000000000) ≤ -(744338687036184402011 / 625000000000000000000)