Certified arcsine potential bounds (U27)

theorem Zeta5Irrational.U_328_1 : Uω (aρ 1) (bρ 1) (38285721908981 / 128000000000000) ≤ -(12287712377373996090711 / 10000000000000000000000)

theorem Zeta5Irrational.U_328_2 : Uω (aρ 2) (bρ 2) (38285721908981 / 128000000000000) ≤ -(6185166194462050153967 / 5000000000000000000000)

theorem Zeta5Irrational.U_328_3 : Uω (aρ 3) (bρ 3) (38285721908981 / 128000000000000) ≤ -(12538237532450347374363 / 10000000000000000000000)

theorem Zeta5Irrational.U_328_4 : Uω (aρ 4) (bρ 4) (38285721908981 / 128000000000000) ≤ -(12825392018479425605597 / 10000000000000000000000)

theorem Zeta5Irrational.U_328_5 : Uω (aρ 5) (bρ 5) (38285721908981 / 128000000000000) ≤ -(6642254426029126533917 / 5000000000000000000000)

theorem Zeta5Irrational.U_328_6 : Uω (aρ 6) (bρ 6) (38285721908981 / 128000000000000) ≤ -(13996590595477121154087 / 10000000000000000000000)

theorem Zeta5Irrational.U_328_7 : Uω (aρ 7) (bρ 7) (38285721908981 / 128000000000000) ≤ -(7549480253947935622409 / 5000000000000000000000)

theorem Zeta5Irrational.U_328_8 : Uω (aρ 8) (bρ 8) (38285721908981 / 128000000000000) ≤ -(16884873835296377582209 / 10000000000000000000000)

theorem Zeta5Irrational.U_328_9 : Uω (aρ 9) (bρ 9) (38285721908981 / 128000000000000) ≤ -(4090660677271729170247 / 2000000000000000000000)

theorem Zeta5Irrational.U_328_10 : Uω (aρ 10) (bρ 10) (38285721908981 / 128000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_328_11 : Uω (aρ 11) (bρ 11) (38285721908981 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_328_12 : Uω (aρ 12) (bρ 12) (38285721908981 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_328_13 : Uω (aρ 13) (bρ 13) (38285721908981 / 128000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_328_14 : Uω (aρ 14) (bρ 14) (38285721908981 / 128000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_328_15 : Uω (aρ 15) (bρ 15) (38285721908981 / 128000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_328_16 : Uω (aρ 16) (bρ 16) (38285721908981 / 128000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_328 : Uρ (38285721908981 / 128000000000000) ≤ -(16211642204940930669019 / 10000000000000000000000)

theorem Zeta5Irrational.U_329_1 : Uω (aρ 1) (bρ 1) (19181732733117 / 64000000000000) ≤ -(6133489718462708656097 / 5000000000000000000000)

theorem Zeta5Irrational.U_329_2 : Uω (aρ 2) (bρ 2) (19181732733117 / 64000000000000) ≤ -(12349425391609171288573 / 10000000000000000000000)

theorem Zeta5Irrational.U_329_3 : Uω (aρ 3) (bρ 3) (19181732733117 / 64000000000000) ≤ -(6258484975339397372699 / 5000000000000000000000)

theorem Zeta5Irrational.U_329_4 : Uω (aρ 4) (bρ 4) (19181732733117 / 64000000000000) ≤ -(640174279668968429527 / 500000000000000000000)

theorem Zeta5Irrational.U_329_5 : Uω (aρ 5) (bρ 5) (19181732733117 / 64000000000000) ≤ -(13261518716286128424891 / 10000000000000000000000)

theorem Zeta5Irrational.U_329_6 : Uω (aρ 6) (bρ 6) (19181732733117 / 64000000000000) ≤ -(13971749560585366629263 / 10000000000000000000000)

theorem Zeta5Irrational.U_329_7 : Uω (aρ 7) (bρ 7) (19181732733117 / 64000000000000) ≤ -(15070760978440686554333 / 10000000000000000000000)

theorem Zeta5Irrational.U_329_8 : Uω (aρ 8) (bρ 8) (19181732733117 / 64000000000000) ≤ -(2106182354807468528861 / 1250000000000000000000)

theorem Zeta5Irrational.U_329_9 : Uω (aρ 9) (bρ 9) (19181732733117 / 64000000000000) ≤ -(20389268512107521157571 / 10000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_329 : Uρ (19181732733117 / 64000000000000) ≤ -(16193895444089082419773 / 10000000000000000000000)

theorem Zeta5Irrational.U_330_1 : Uω (aρ 1) (bρ 1) (38441209023487 / 128000000000000) ≤ -(61231446973232137127 / 50000000000000000000)

theorem Zeta5Irrational.U_330_2 : Uω (aρ 2) (bρ 2) (38441209023487 / 128000000000000) ≤ -(12328562024288774376437 / 10000000000000000000000)

theorem Zeta5Irrational.U_330_3 : Uω (aρ 3) (bρ 3) (38441209023487 / 128000000000000) ≤ -(3123936886171363010597 / 2500000000000000000000)

theorem Zeta5Irrational.U_330_4 : Uω (aρ 4) (bρ 4) (38441209023487 / 128000000000000) ≤ -(1278162718286327350039 / 1000000000000000000000)

theorem Zeta5Irrational.U_330_5 : Uω (aρ 5) (bρ 5) (38441209023487 / 128000000000000) ≤ -(3309645428236645038509 / 2500000000000000000000)

theorem Zeta5Irrational.U_330_6 : Uω (aρ 6) (bρ 6) (38441209023487 / 128000000000000) ≤ -(2789394265029026856113 / 2000000000000000000000)

theorem Zeta5Irrational.U_330_7 : Uω (aρ 7) (bρ 7) (38441209023487 / 128000000000000) ≤ -(15042645037382581962017 / 10000000000000000000000)

theorem Zeta5Irrational.U_330_8 : Uω (aρ 8) (bρ 8) (38441209023487 / 128000000000000) ≤ -(67256754094232746029 / 40000000000000000000)

theorem Zeta5Irrational.U_330_9 : Uω (aρ 9) (bρ 9) (38441209023487 / 128000000000000) ≤ -(5081483772522509532501 / 2500000000000000000000)

theorem Zeta5Irrational.U_330_10 : Uω (aρ 10) (bρ 10) (38441209023487 / 128000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_330_11 : Uω (aρ 11) (bρ 11) (38441209023487 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_330_12 : Uω (aρ 12) (bρ 12) (38441209023487 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_330_13 : Uω (aρ 13) (bρ 13) (38441209023487 / 128000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_330_14 : Uω (aρ 14) (bρ 14) (38441209023487 / 128000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_330_15 : Uω (aρ 15) (bρ 15) (38441209023487 / 128000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_330_16 : Uω (aρ 16) (bρ 16) (38441209023487 / 128000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_330 : Uρ (38441209023487 / 128000000000000) ≤ -(8088122799333122230017 / 5000000000000000000000)

theorem Zeta5Irrational.U_331_1 : Uω (aρ 1) (bρ 1) (1925947629037 / 6400000000000) ≤ -(6112821036688579436813 / 5000000000000000000000)

theorem Zeta5Irrational.U_331_2 : Uω (aρ 2) (bρ 2) (1925947629037 / 6400000000000) ≤ -(12307742105197329123461 / 10000000000000000000000)

theorem Zeta5Irrational.U_331_3 : Uω (aρ 3) (bρ 3) (1925947629037 / 6400000000000) ≤ -(3118642530695954496121 / 2500000000000000000000)

theorem Zeta5Irrational.U_331_4 : Uω (aρ 4) (bρ 4) (1925947629037 / 6400000000000) ≤ -(12759816576347544304649 / 10000000000000000000000)

theorem Zeta5Irrational.U_331_5 : Uω (aρ 5) (bρ 5) (1925947629037 / 6400000000000) ≤ -(2643139519038542533491 / 2000000000000000000000)

theorem Zeta5Irrational.U_331_6 : Uω (aρ 6) (bρ 6) (1925947629037 / 6400000000000) ≤ -(2784451113250624090057 / 2000000000000000000000)

theorem Zeta5Irrational.U_331_7 : Uω (aρ 7) (bρ 7) (1925947629037 / 6400000000000) ≤ -(15014612166085188211901 / 10000000000000000000000)

theorem Zeta5Irrational.U_331_8 : Uω (aρ 8) (bρ 8) (1925947629037 / 6400000000000) ≤ -(2097382695647042841857 / 1250000000000000000000)

theorem Zeta5Irrational.U_331_9 : Uω (aρ 9) (bρ 9) (1925947629037 / 6400000000000) ≤ -(20263283021367291826911 / 10000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_331 : Uρ (1925947629037 / 6400000000000) ≤ -(8079345331240174625109 / 5000000000000000000000)

theorem Zeta5Irrational.U_332_1 : Uω (aρ 1) (bρ 1) (19337219847623 / 64000000000000) ≤ -(6092237445347728784389 / 5000000000000000000000)

theorem Zeta5Irrational.U_332_2 : Uω (aρ 2) (bρ 2) (19337219847623 / 64000000000000) ≤ -(12266231890298508999037 / 10000000000000000000000)

theorem Zeta5Irrational.U_332_3 : Uω (aρ 3) (bρ 3) (19337219847623 / 64000000000000) ≤ -(6216174735296002445103 / 5000000000000000000000)

theorem Zeta5Irrational.U_332_4 : Uω (aρ 4) (bρ 4) (19337219847623 / 64000000000000) ≤ -(12716337939900776348663 / 10000000000000000000000)

theorem Zeta5Irrational.U_332_5 : Uω (aρ 5) (bρ 5) (19337219847623 / 64000000000000) ≤ -(3292521759420410891227 / 2500000000000000000000)

theorem Zeta5Irrational.U_332_6 : Uω (aρ 6) (bρ 6) (19337219847623 / 64000000000000) ≤ -(6936505099560823511611 / 5000000000000000000000)

theorem Zeta5Irrational.U_332_7 : Uω (aρ 7) (bρ 7) (19337219847623 / 64000000000000) ≤ -(14958793583244939740179 / 10000000000000000000000)

theorem Zeta5Irrational.U_332_8 : Uω (aρ 8) (bρ 8) (19337219847623 / 64000000000000) ≤ -(8354616257164736756719 / 5000000000000000000000)

theorem Zeta5Irrational.U_332_9 : Uω (aρ 9) (bρ 9) (19337219847623 / 64000000000000) ≤ -(5034986812783164747793 / 2500000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_332 : Uρ (19337219847623 / 64000000000000) ≤ -(16123857921615760857801 / 10000000000000000000000)

theorem Zeta5Irrational.U_333_1 : Uω (aρ 1) (bρ 1) (4853740851219 / 16000000000000) ≤ -(2428695298668879795403 / 2000000000000000000000)

theorem Zeta5Irrational.U_333_2 : Uω (aρ 2) (bρ 2) (4853740851219 / 16000000000000) ≤ -(6112446657647581372819 / 5000000000000000000000)

theorem Zeta5Irrational.U_333_3 : Uω (aρ 3) (bρ 3) (4853740851219 / 16000000000000) ≤ -(12390306484797001658741 / 10000000000000000000000)

theorem Zeta5Irrational.U_333_4 : Uω (aρ 4) (bρ 4) (4853740851219 / 16000000000000) ≤ -(6336524013436370123083 / 5000000000000000000000)

theorem Zeta5Irrational.U_333_5 : Uω (aρ 5) (bρ 5) (4853740851219 / 16000000000000) ≤ -(13124685103260900577841 / 10000000000000000000000)

theorem Zeta5Irrational.U_333_6 : Uω (aρ 6) (bρ 6) (4853740851219 / 16000000000000) ≤ -(1728001366084479726809 / 1250000000000000000000)

theorem Zeta5Irrational.U_333_7 : Uω (aρ 7) (bρ 7) (4853740851219 / 16000000000000) ≤ -(7451650589987120200889 / 5000000000000000000000)

theorem Zeta5Irrational.U_333_8 : Uω (aρ 8) (bρ 8) (4853740851219 / 16000000000000) ≤ -(16639961469023081417581 / 10000000000000000000000)

theorem Zeta5Irrational.U_333_9 : Uω (aρ 9) (bρ 9) (4853740851219 / 16000000000000) ≤ -(2502389798007060102871 / 1250000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_333 : Uρ (4853740851219 / 16000000000000) ≤ -(2011172851470674920769 / 1250000000000000000000)

theorem Zeta5Irrational.U_334_1 : Uω (aρ 1) (bρ 1) (19492706962129 / 64000000000000) ≤ -(12102645502884357136123 / 10000000000000000000000)

theorem Zeta5Irrational.U_334_2 : Uω (aρ 2) (bρ 2) (19492706962129 / 64000000000000) ≤ -(6091862483132022743739 / 5000000000000000000000)

theorem Zeta5Irrational.U_334_3 : Uω (aρ 3) (bρ 3) (19492706962129 / 64000000000000) ≤ -(12348439675099821250339 / 10000000000000000000000)

theorem Zeta5Irrational.U_334_4 : Uω (aρ 4) (bρ 4) (19492706962129 / 64000000000000) ≤ -(6314972600848446314769 / 5000000000000000000000)

theorem Zeta5Irrational.U_334_5 : Uω (aρ 5) (bρ 5) (19492706962129 / 64000000000000) ≤ -(13079489878329665778293 / 10000000000000000000000)

theorem Zeta5Irrational.U_334_6 : Uω (aρ 6) (bρ 6) (19492706962129 / 64000000000000) ≤ -(13775255255809352500289 / 10000000000000000000000)

theorem Zeta5Irrational.U_334_7 : Uω (aρ 7) (bρ 7) (19492706962129 / 64000000000000) ≤ -(7424065491729029942457 / 5000000000000000000000)

theorem Zeta5Irrational.U_334_8 : Uω (aρ 8) (bρ 8) (19492706962129 / 64000000000000) ≤ -(16571238508300731484711 / 10000000000000000000000)

theorem Zeta5Irrational.U_334_9 : Uω (aρ 9) (bρ 9) (19492706962129 / 64000000000000) ≤ -(9950333064951701404441 / 5000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_334 : Uρ (19492706962129 / 64000000000000) ≤ -(8027626034599468880467 / 5000000000000000000000)

theorem Zeta5Irrational.U_335_1 : Uω (aρ 1) (bρ 1) (9785225259691 / 32000000000000) ≤ -(12061980557693874766859 / 10000000000000000000000)

theorem Zeta5Irrational.U_335_2 : Uω (aρ 2) (bρ 2) (9785225259691 / 32000000000000) ≤ -(1517840680835718813187 / 1250000000000000000000)

theorem Zeta5Irrational.U_335_3 : Uω (aρ 3) (bρ 3) (9785225259691 / 32000000000000) ≤ -(6153373784945376044151 / 5000000000000000000000)

theorem Zeta5Irrational.U_335_4 : Uω (aρ 4) (bρ 4) (9785225259691 / 32000000000000) ≤ -(12587027850031739223471 / 10000000000000000000000)

theorem Zeta5Irrational.U_335_5 : Uω (aρ 5) (bρ 5) (9785225259691 / 32000000000000) ≤ -(814656217230021947263 / 625000000000000000000)

theorem Zeta5Irrational.U_335_6 : Uω (aρ 6) (bρ 6) (9785225259691 / 32000000000000) ≤ -(1372674072760321762727 / 1000000000000000000000)

theorem Zeta5Irrational.U_335_7 : Uω (aρ 7) (bρ 7) (9785225259691 / 32000000000000) ≤ -(7396639548000137332547 / 5000000000000000000000)

theorem Zeta5Irrational.U_335_8 : Uω (aρ 8) (bρ 8) (9785225259691 / 32000000000000) ≤ -(1031440874701677454237 / 625000000000000000000)

theorem Zeta5Irrational.U_335_9 : Uω (aρ 9) (bρ 9) (9785225259691 / 32000000000000) ≤ -(19784471231578686300367 / 10000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_335 : Uρ (9785225259691 / 32000000000000) ≤ -(8010726722061475591077 / 5000000000000000000000)

theorem Zeta5Irrational.U_336_1 : Uω (aρ 1) (bρ 1) (3929638815327 / 12800000000000) ≤ -(12021480312697159223583 / 10000000000000000000000)

theorem Zeta5Irrational.U_336_2 : Uω (aρ 2) (bρ 2) (3929638815327 / 12800000000000) ≤ -(3025473344290043015187 / 2500000000000000000000)

theorem Zeta5Irrational.U_336_3 : Uω (aρ 3) (bρ 3) (3929638815327 / 12800000000000) ≤ -(3066307178984472565569 / 2500000000000000000000)

theorem Zeta5Irrational.U_336_4 : Uω (aρ 4) (bρ 4) (3929638815327 / 12800000000000) ≤ -(12544294378394242768849 / 10000000000000000000000)

theorem Zeta5Irrational.U_336_5 : Uω (aρ 5) (bρ 5) (3929638815327 / 12800000000000) ≤ -(2597942406802438394041 / 2000000000000000000000)

theorem Zeta5Irrational.U_336_6 : Uω (aρ 6) (bρ 6) (3929638815327 / 12800000000000) ≤ -(6839232463065716702293 / 5000000000000000000000)

theorem Zeta5Irrational.U_336_7 : Uω (aρ 7) (bρ 7) (3929638815327 / 12800000000000) ≤ -(7369370846539389318947 / 5000000000000000000000)

theorem Zeta5Irrational.U_336_8 : Uω (aρ 8) (bρ 8) (3929638815327 / 12800000000000) ≤ -(16435398565581580107231 / 10000000000000000000000)

theorem Zeta5Irrational.U_336_9 : Uω (aρ 9) (bρ 9) (3929638815327 / 12800000000000) ≤ -(19670424193114000292823 / 10000000000000000000000)

theorem Zeta5Irrational.U_336_10 : Uω (aρ 10) (bρ 10) (3929638815327 / 12800000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_336_11 : Uω (aρ 11) (bρ 11) (3929638815327 / 12800000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_336_12 : Uω (aρ 12) (bρ 12) (3929638815327 / 12800000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_336_13 : Uω (aρ 13) (bρ 13) (3929638815327 / 12800000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_336_14 : Uω (aρ 14) (bρ 14) (3929638815327 / 12800000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_336_15 : Uω (aρ 15) (bρ 15) (3929638815327 / 12800000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_336_16 : Uω (aρ 16) (bρ 16) (3929638815327 / 12800000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_336 : Uρ (3929638815327 / 12800000000000) ≤ -(15987975586230920657997 / 10000000000000000000000)

theorem Zeta5Irrational.U_337_1 : Uω (aρ 1) (bρ 1) (616435551059 / 2000000000000) ≤ -(11981143439097091459783 / 10000000000000000000000)

theorem Zeta5Irrational.U_337_2 : Uω (aρ 2) (bρ 2) (616435551059 / 2000000000000) ≤ -(12061227395127781664123 / 10000000000000000000000)

theorem Zeta5Irrational.U_337_3 : Uω (aρ 3) (bρ 3) (616435551059 / 2000000000000) ≤ -(12223881678082135699073 / 10000000000000000000000)

theorem Zeta5Irrational.U_337_4 : Uω (aρ 4) (bρ 4) (616435551059 / 2000000000000) ≤ -(3125435803450280365889 / 2500000000000000000000)

theorem Zeta5Irrational.U_337_5 : Uω (aρ 5) (bρ 5) (616435551059 / 2000000000000) ≤ -(2589025143491211693361 / 2000000000000000000000)

theorem Zeta5Irrational.U_337_6 : Uω (aρ 6) (bρ 6) (616435551059 / 2000000000000) ≤ -(13630425470284692729279 / 10000000000000000000000)

theorem Zeta5Irrational.U_337_7 : Uω (aρ 7) (bρ 7) (616435551059 / 2000000000000) ≤ -(14684515021464761878583 / 10000000000000000000000)

theorem Zeta5Irrational.U_337_8 : Uω (aρ 8) (bρ 8) (616435551059 / 2000000000000) ≤ -(4092065779282799140011 / 2500000000000000000000)

theorem Zeta5Irrational.U_337_9 : Uω (aρ 9) (bρ 9) (616435551059 / 2000000000000) ≤ -(9779212095280143712081 / 5000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_337 : Uρ (616435551059 / 2000000000000) ≤ -(7977403973744688773817 / 5000000000000000000000)

theorem Zeta5Irrational.U_338_1 : Uω (aρ 1) (bρ 1) (19803681191141 / 64000000000000) ≤ -(46644408687943654039 / 39062500000000000000)

theorem Zeta5Irrational.U_338_2 : Uω (aρ 2) (bρ 2) (19803681191141 / 64000000000000) ≤ -(12020726154596521413683 / 10000000000000000000000)

theorem Zeta5Irrational.U_338_3 : Uω (aρ 3) (bρ 3) (19803681191141 / 64000000000000) ≤ -(2436541007787700471499 / 2000000000000000000000)

theorem Zeta5Irrational.U_338_4 : Uω (aρ 4) (bρ 4) (19803681191141 / 64000000000000) ≤ -(6229686401708916302631 / 5000000000000000000000)

theorem Zeta5Irrational.U_338_5 : Uω (aρ 5) (bρ 5) (19803681191141 / 64000000000000) ≤ -(12900738715110178474141 / 10000000000000000000000)

theorem Zeta5Irrational.U_338_6 : Uω (aρ 6) (bρ 6) (19803681191141 / 64000000000000) ≤ -(2716524003002969505043 / 2000000000000000000000)

theorem Zeta5Irrational.U_338_7 : Uω (aρ 7) (bρ 7) (19803681191141 / 64000000000000) ≤ -(14630595397403589959339 / 10000000000000000000000)

theorem Zeta5Irrational.U_338_8 : Uω (aρ 8) (bρ 8) (19803681191141 / 64000000000000) ≤ -(16301638799438157530459 / 10000000000000000000000)

theorem Zeta5Irrational.U_338_9 : Uω (aρ 9) (bρ 9) (19803681191141 / 64000000000000) ≤ -(9724189067304602339073 / 5000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_338 : Uρ (19803681191141 / 64000000000000) ≤ -(15921940698173401965557 / 10000000000000000000000)

theorem Zeta5Irrational.U_339_1 : Uω (aρ 1) (bρ 1) (9940712374197 / 32000000000000) ≤ -(5950477285363575388391 / 5000000000000000000000)

theorem Zeta5Irrational.U_339_2 : Uω (aρ 2) (bρ 2) (9940712374197 / 32000000000000) ≤ -(5990194162937124877343 / 5000000000000000000000)

theorem Zeta5Irrational.U_339_3 : Uω (aρ 3) (bρ 3) (9940712374197 / 32000000000000) ≤ -(6070848699301788378207 / 5000000000000000000000)

theorem Zeta5Irrational.U_339_4 : Uω (aρ 4) (bρ 4) (9940712374197 / 32000000000000) ≤ -(1552147701776885039179 / 1250000000000000000000)

theorem Zeta5Irrational.U_339_5 : Uω (aρ 5) (bρ 5) (9940712374197 / 32000000000000) ≤ -(6428274620293240149007 / 5000000000000000000000)

theorem Zeta5Irrational.U_339_6 : Uω (aρ 6) (bρ 6) (9940712374197 / 32000000000000) ≤ -(13535046250598920676661 / 10000000000000000000000)

theorem Zeta5Irrational.U_339_7 : Uω (aρ 7) (bρ 7) (9940712374197 / 32000000000000) ≤ -(91106120030342734303 / 62500000000000000000)

theorem Zeta5Irrational.U_339_8 : Uω (aρ 8) (bρ 8) (9940712374197 / 32000000000000) ≤ -(16235517004178202317679 / 10000000000000000000000)

theorem Zeta5Irrational.U_339_9 : Uω (aρ 9) (bρ 9) (9940712374197 / 32000000000000) ≤ -(19340199859860171901071 / 10000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_339 : Uρ (9940712374197 / 32000000000000) ≤ -(127114917233107029293 / 80000000000000000000)