Certified arcsine potential bounds (U19)

theorem Zeta5Irrational.U_232_1 : Uω (aρ 1) (bρ 1) (345431490187 / 2000000000000) ≤ -(1121390443150977258413 / 625000000000000000000)

theorem Zeta5Irrational.U_232_2 : Uω (aρ 2) (bρ 2) (345431490187 / 2000000000000) ≤ -(113060024226724001509 / 62500000000000000000)

theorem Zeta5Irrational.U_232_3 : Uω (aρ 3) (bρ 3) (345431490187 / 2000000000000) ≤ -(3678749652860036091943 / 2000000000000000000000)

theorem Zeta5Irrational.U_232_4 : Uω (aρ 4) (bρ 4) (345431490187 / 2000000000000) ≤ -(18929844191670132660891 / 10000000000000000000000)

theorem Zeta5Irrational.U_232_5 : Uω (aρ 5) (bρ 5) (345431490187 / 2000000000000) ≤ -(4959139442762577320171 / 2500000000000000000000)

theorem Zeta5Irrational.U_232_6 : Uω (aρ 6) (bρ 6) (345431490187 / 2000000000000) ≤ -(5352071603001420085127 / 2500000000000000000000)

theorem Zeta5Irrational.U_232_7 : Uω (aρ 7) (bρ 7) (345431490187 / 2000000000000) ≤ -(1539303126159486415141 / 625000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_232 : Uρ (345431490187 / 2000000000000) ≤ -(20620488410529718411491 / 10000000000000000000000)

theorem Zeta5Irrational.U_233_1 : Uω (aρ 1) (bρ 1) (5583683878263 / 32000000000000) ≤ -(17836081128313023247777 / 10000000000000000000000)

theorem Zeta5Irrational.U_233_2 : Uω (aρ 2) (bρ 2) (5583683878263 / 32000000000000) ≤ -(17981834645297691005227 / 10000000000000000000000)

theorem Zeta5Irrational.U_233_3 : Uω (aρ 3) (bρ 3) (5583683878263 / 32000000000000) ≤ -(3656510475313698243173 / 2000000000000000000000)

theorem Zeta5Irrational.U_233_4 : Uω (aρ 4) (bρ 4) (5583683878263 / 32000000000000) ≤ -(2351524134012850285883 / 1250000000000000000000)

theorem Zeta5Irrational.U_233_5 : Uω (aρ 5) (bρ 5) (5583683878263 / 32000000000000) ≤ -(9853302452241801719929 / 5000000000000000000000)

theorem Zeta5Irrational.U_233_6 : Uω (aρ 6) (bρ 6) (5583683878263 / 32000000000000) ≤ -(425033657159668721931 / 200000000000000000000)

theorem Zeta5Irrational.U_233_7 : Uω (aρ 7) (bρ 7) (5583683878263 / 32000000000000) ≤ -(24379726540844704730177 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_233 : Uρ (5583683878263 / 32000000000000) ≤ -(10281055425697362557601 / 5000000000000000000000)

theorem Zeta5Irrational.U_234_1 : Uω (aρ 1) (bρ 1) (2820231956767 / 16000000000000) ≤ -(4432757645883601178647 / 2500000000000000000000)

theorem Zeta5Irrational.U_234_2 : Uω (aρ 2) (bρ 2) (2820231956767 / 16000000000000) ≤ -(17875215342854461799939 / 10000000000000000000000)

theorem Zeta5Irrational.U_234_3 : Uω (aρ 3) (bρ 3) (2820231956767 / 16000000000000) ≤ -(9086291413154191049523 / 5000000000000000000000)

theorem Zeta5Irrational.U_234_4 : Uω (aρ 4) (bρ 4) (2820231956767 / 16000000000000) ≤ -(4673980589084799832807 / 2500000000000000000000)

theorem Zeta5Irrational.U_234_5 : Uω (aρ 5) (bρ 5) (2820231956767 / 16000000000000) ≤ -(19578364916448394077517 / 10000000000000000000000)

theorem Zeta5Irrational.U_234_6 : Uω (aρ 6) (bρ 6) (2820231956767 / 16000000000000) ≤ -(21097707582265118210857 / 10000000000000000000000)

theorem Zeta5Irrational.U_234_7 : Uω (aρ 7) (bρ 7) (2820231956767 / 16000000000000) ≤ -(24139057684859532006813 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_234 : Uρ (2820231956767 / 16000000000000) ≤ -(20504954889210252469137 / 10000000000000000000000)

theorem Zeta5Irrational.U_235_1 : Uω (aρ 1) (bρ 1) (1139448789761 / 6400000000000) ≤ -(17627072259042377358077 / 10000000000000000000000)

theorem Zeta5Irrational.U_235_2 : Uω (aρ 2) (bρ 2) (1139448789761 / 6400000000000) ≤ -(17769721669487918798127 / 10000000000000000000000)

theorem Zeta5Irrational.U_235_3 : Uω (aρ 3) (bρ 3) (1139448789761 / 6400000000000) ≤ -(18063812784732552797297 / 10000000000000000000000)

theorem Zeta5Irrational.U_235_4 : Uω (aρ 4) (bρ 4) (1139448789761 / 6400000000000) ≤ -(18580999749485371987611 / 10000000000000000000000)

theorem Zeta5Irrational.U_235_5 : Uω (aρ 5) (bρ 5) (1139448789761 / 6400000000000) ≤ -(19451792096157150090147 / 10000000000000000000000)

theorem Zeta5Irrational.U_235_6 : Uω (aρ 6) (bρ 6) (1139448789761 / 6400000000000) ≤ -(20946267287668847085137 / 10000000000000000000000)

theorem Zeta5Irrational.U_235_7 : Uω (aρ 7) (bρ 7) (1139448789761 / 6400000000000) ≤ -(23906163545953218465999 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_235 : Uρ (1139448789761 / 6400000000000) ≤ -(1278059270240595681709 / 625000000000000000000)

theorem Zeta5Irrational.U_236_1 : Uω (aρ 1) (bρ 1) (1438505996019 / 8000000000000) ≤ -(3504836734814087840143 / 2000000000000000000000)

theorem Zeta5Irrational.U_236_2 : Uω (aρ 2) (bρ 2) (1438505996019 / 8000000000000) ≤ -(8832665044234793364127 / 5000000000000000000000)

theorem Zeta5Irrational.U_236_3 : Uω (aρ 3) (bρ 3) (1438505996019 / 8000000000000) ≤ -(561131759258713630229 / 312500000000000000000)

theorem Zeta5Irrational.U_236_4 : Uω (aρ 4) (bρ 4) (1438505996019 / 8000000000000) ≤ -(18467394086119095410203 / 10000000000000000000000)

theorem Zeta5Irrational.U_236_5 : Uω (aρ 5) (bρ 5) (1438505996019 / 8000000000000) ≤ -(19326842580294766154441 / 10000000000000000000000)

theorem Zeta5Irrational.U_236_6 : Uω (aρ 6) (bρ 6) (1438505996019 / 8000000000000) ≤ -(4159454768142052679751 / 2000000000000000000000)

theorem Zeta5Irrational.U_236_7 : Uω (aρ 7) (bρ 7) (1438505996019 / 8000000000000) ≤ -(23680451252261213551871 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_236 : Uρ (1438505996019 / 8000000000000) ≤ -(815761080340562607109 / 400000000000000000000)

theorem Zeta5Irrational.U_237_1 : Uω (aρ 1) (bρ 1) (2933792027309 / 16000000000000) ≤ -(216519115091196781593 / 125000000000000000000)

theorem Zeta5Irrational.U_237_2 : Uω (aρ 2) (bρ 2) (2933792027309 / 16000000000000) ≤ -(545617583817240004993 / 312500000000000000000)

theorem Zeta5Irrational.U_237_3 : Uω (aρ 3) (bρ 3) (2933792027309 / 16000000000000) ≤ -(17744444299101173343339 / 10000000000000000000000)

theorem Zeta5Irrational.U_237_4 : Uω (aρ 4) (bρ 4) (2933792027309 / 16000000000000) ≤ -(18244014263751742130657 / 10000000000000000000000)

theorem Zeta5Irrational.U_237_5 : Uω (aρ 5) (bρ 5) (2933792027309 / 16000000000000) ≤ -(9540823325732590924141 / 5000000000000000000000)

theorem Zeta5Irrational.U_237_6 : Uω (aρ 6) (bρ 6) (2933792027309 / 16000000000000) ≤ -(20506298475419563252639 / 10000000000000000000000)

theorem Zeta5Irrational.U_237_7 : Uω (aρ 7) (bρ 7) (2933792027309 / 16000000000000) ≤ -(2906068668546487972029 / 1250000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_237 : Uρ (2933792027309 / 16000000000000) ≤ -(10143608103708137941839 / 5000000000000000000000)

theorem Zeta5Irrational.U_238_1 : Uω (aρ 1) (bρ 1) (149528603129 / 800000000000) ≤ -(17122900589309473870993 / 10000000000000000000000)

theorem Zeta5Irrational.U_238_2 : Uω (aρ 2) (bρ 2) (149528603129 / 800000000000) ≤ -(8629169461557259480653 / 5000000000000000000000)

theorem Zeta5Irrational.U_238_3 : Uω (aρ 3) (bρ 3) (149528603129 / 800000000000) ≤ -(3507415055125305177593 / 2000000000000000000000)

theorem Zeta5Irrational.U_238_4 : Uω (aρ 4) (bρ 4) (149528603129 / 800000000000) ≤ -(3605110847146402910907 / 2000000000000000000000)

theorem Zeta5Irrational.U_238_5 : Uω (aρ 5) (bρ 5) (149528603129 / 800000000000) ≤ -(9421229765333016833399 / 5000000000000000000000)

theorem Zeta5Irrational.U_238_6 : Uω (aρ 6) (bρ 6) (149528603129 / 800000000000) ≤ -(20224165771428923170819 / 10000000000000000000000)

theorem Zeta5Irrational.U_238_7 : Uω (aρ 7) (bρ 7) (149528603129 / 800000000000) ≤ -(22839854558538710203403 / 10000000000000000000000)

theorem Zeta5Irrational.U_238_8 : Uω (aρ 8) (bρ 8) (149528603129 / 800000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_238_9 : Uω (aρ 9) (bρ 9) (149528603129 / 800000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_238_10 : Uω (aρ 10) (bρ 10) (149528603129 / 800000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_238_11 : Uω (aρ 11) (bρ 11) (149528603129 / 800000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_238_12 : Uω (aρ 12) (bρ 12) (149528603129 / 800000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_238_13 : Uω (aρ 13) (bρ 13) (149528603129 / 800000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_238_14 : Uω (aρ 14) (bρ 14) (149528603129 / 800000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_238_15 : Uω (aρ 15) (bρ 15) (149528603129 / 800000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_238_16 : Uω (aρ 16) (bρ 16) (149528603129 / 800000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_238 : Uρ (149528603129 / 800000000000) ≤ -(10092063400161778436219 / 5000000000000000000000)

theorem Zeta5Irrational.U_239_1 : Uω (aρ 1) (bρ 1) (3047352097851 / 16000000000000) ≤ -(423203524096555888311 / 250000000000000000000)

theorem Zeta5Irrational.U_239_2 : Uω (aρ 2) (bρ 2) (3047352097851 / 16000000000000) ≤ -(17060894951251626070951 / 10000000000000000000000)

theorem Zeta5Irrational.U_239_3 : Uω (aρ 3) (bρ 3) (3047352097851 / 16000000000000) ≤ -(3466785886107343843369 / 2000000000000000000000)

theorem Zeta5Irrational.U_239_4 : Uω (aρ 4) (bρ 4) (3047352097851 / 16000000000000) ≤ -(17811800359939854210869 / 10000000000000000000000)

theorem Zeta5Irrational.U_239_5 : Uω (aρ 5) (bρ 5) (3047352097851 / 16000000000000) ≤ -(9304493713255353838983 / 5000000000000000000000)

theorem Zeta5Irrational.U_239_6 : Uω (aρ 6) (bρ 6) (3047352097851 / 16000000000000) ≤ -(19950321207062330984031 / 10000000000000000000000)

theorem Zeta5Irrational.U_239_7 : Uω (aρ 7) (bρ 7) (3047352097851 / 16000000000000) ≤ -(22451573375701112560891 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_239 : Uρ (3047352097851 / 16000000000000) ≤ -(20084431088609508863849 / 10000000000000000000000)

theorem Zeta5Irrational.U_240_1 : Uω (aρ 1) (bρ 1) (1552066066561 / 8000000000000) ≤ -(3347420493572264953999 / 2000000000000000000000)

theorem Zeta5Irrational.U_240_2 : Uω (aρ 2) (bρ 2) (1552066066561 / 8000000000000) ≤ -(4216819111011872001949 / 2500000000000000000000)

theorem Zeta5Irrational.U_240_3 : Uω (aρ 3) (bρ 3) (1552066066561 / 8000000000000) ≤ -(3426967557250234145729 / 2000000000000000000000)

theorem Zeta5Irrational.U_240_4 : Uω (aρ 4) (bρ 4) (1552066066561 / 8000000000000) ≤ -(1100159544436690800209 / 625000000000000000000)

theorem Zeta5Irrational.U_240_5 : Uω (aρ 5) (bρ 5) (1552066066561 / 8000000000000) ≤ -(18380957992918669968001 / 10000000000000000000000)

theorem Zeta5Irrational.U_240_6 : Uω (aρ 6) (bρ 6) (1552066066561 / 8000000000000) ≤ -(3936852661578481560173 / 2000000000000000000000)

theorem Zeta5Irrational.U_240_7 : Uω (aρ 7) (bρ 7) (1552066066561 / 8000000000000) ≤ -(5520357822357195670947 / 2500000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_240 : Uρ (1552066066561 / 8000000000000) ≤ -(4996963179176144483103 / 2500000000000000000000)

theorem Zeta5Irrational.U_241_1 : Uω (aρ 1) (bρ 1) (201105762729 / 1000000000000) ≤ -(8182819195849925653851 / 5000000000000000000000)

theorem Zeta5Irrational.U_241_2 : Uω (aρ 2) (bρ 2) (201105762729 / 1000000000000) ≤ -(16490941930067749877633 / 10000000000000000000000)

theorem Zeta5Irrational.U_241_3 : Uω (aρ 3) (bρ 3) (201105762729 / 1000000000000) ≤ -(3349638049019418963313 / 2000000000000000000000)

theorem Zeta5Irrational.U_241_4 : Uω (aρ 4) (bρ 4) (201105762729 / 1000000000000) ≤ -(8598419076450674071003 / 5000000000000000000000)

theorem Zeta5Irrational.U_241_5 : Uω (aρ 5) (bρ 5) (201105762729 / 1000000000000) ≤ -(17940232793488732042317 / 10000000000000000000000)

theorem Zeta5Irrational.U_241_6 : Uω (aρ 6) (bρ 6) (201105762729 / 1000000000000) ≤ -(19173727179049642941211 / 10000000000000000000000)

theorem Zeta5Irrational.U_241_7 : Uω (aρ 7) (bρ 7) (201105762729 / 1000000000000) ≤ -(21388339142901952282833 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_241 : Uρ (201105762729 / 1000000000000) ≤ -(19803133250419148341029 / 10000000000000000000000)

theorem Zeta5Irrational.U_242_1 : Uω (aρ 1) (bρ 1) (3251812320751 / 16000000000000) ≤ -(16256672346253327359079 / 10000000000000000000000)

theorem Zeta5Irrational.U_242_2 : Uω (aρ 2) (bρ 2) (3251812320751 / 16000000000000) ≤ -(16380582927889856239697 / 10000000000000000000000)

theorem Zeta5Irrational.U_242_3 : Uω (aρ 3) (bρ 3) (3251812320751 / 16000000000000) ≤ -(8317443114412870681471 / 5000000000000000000000)

theorem Zeta5Irrational.U_242_4 : Uω (aρ 4) (bρ 4) (3251812320751 / 16000000000000) ≤ -(17078105971949760117981 / 10000000000000000000000)

theorem Zeta5Irrational.U_242_5 : Uω (aρ 5) (bρ 5) (3251812320751 / 16000000000000) ≤ -(17811592507555697950333 / 10000000000000000000000)

theorem Zeta5Irrational.U_242_6 : Uω (aρ 6) (bρ 6) (3251812320751 / 16000000000000) ≤ -(9512788988564780394523 / 5000000000000000000000)

theorem Zeta5Irrational.U_242_7 : Uω (aρ 7) (bρ 7) (3251812320751 / 16000000000000) ≤ -(21190996519392976753163 / 10000000000000000000000)

theorem Zeta5Irrational.U_242_8 : Uω (aρ 8) (bρ 8) (3251812320751 / 16000000000000) ≤ -(13927889747717311336039 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_242 : Uρ (3251812320751 / 16000000000000) ≤ -(2445977526242332705763 / 1250000000000000000000)

theorem Zeta5Irrational.U_243_1 : Uω (aρ 1) (bρ 1) (1642966218919 / 8000000000000) ≤ -(16148880970392734533323 / 10000000000000000000000)

theorem Zeta5Irrational.U_243_2 : Uω (aρ 2) (bρ 2) (1642966218919 / 8000000000000) ≤ -(16271429224111498996607 / 10000000000000000000000)

theorem Zeta5Irrational.U_243_3 : Uω (aρ 3) (bρ 3) (1642966218919 / 8000000000000) ≤ -(16522854212519461836571 / 10000000000000000000000)

theorem Zeta5Irrational.U_243_4 : Uω (aρ 4) (bρ 4) (1642966218919 / 8000000000000) ≤ -(16960775844740112262383 / 10000000000000000000000)

theorem Zeta5Irrational.U_243_5 : Uω (aρ 5) (bρ 5) (1642966218919 / 8000000000000) ≤ -(8842308310589361790873 / 5000000000000000000000)

theorem Zeta5Irrational.U_243_6 : Uω (aρ 6) (bρ 6) (1642966218919 / 8000000000000) ≤ -(3775942473366500779873 / 2000000000000000000000)

theorem Zeta5Irrational.U_243_7 : Uω (aρ 7) (bρ 7) (1642966218919 / 8000000000000) ≤ -(20998210011066161697331 / 10000000000000000000000)

theorem Zeta5Irrational.U_243_8 : Uω (aρ 8) (bρ 8) (1642966218919 / 8000000000000) ≤ -(270088395415343064811 / 100000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_243 : Uρ (1642966218919 / 8000000000000) ≤ -(19440334361737891654043 / 10000000000000000000000)