Certified arcsine potential bounds (U13)

theorem Zeta5Irrational.U_160_1 : Uω (aρ 1) (bρ 1) (3519728384093 / 32000000000000) ≤ -(22679308077571814145547 / 10000000000000000000000)

theorem Zeta5Irrational.U_160_2 : Uω (aρ 2) (bρ 2) (3519728384093 / 32000000000000) ≤ -(22920417791434948469573 / 10000000000000000000000)

theorem Zeta5Irrational.U_160_3 : Uω (aρ 3) (bρ 3) (3519728384093 / 32000000000000) ≤ -(23429892300799022833847 / 10000000000000000000000)

theorem Zeta5Irrational.U_160_4 : Uω (aρ 4) (bρ 4) (3519728384093 / 32000000000000) ≤ -(24373512065536270100317 / 10000000000000000000000)

theorem Zeta5Irrational.U_160_5 : Uω (aρ 5) (bρ 5) (3519728384093 / 32000000000000) ≤ -(26154357087978048520417 / 10000000000000000000000)

theorem Zeta5Irrational.U_160_6 : Uω (aρ 6) (bρ 6) (3519728384093 / 32000000000000) ≤ -(30576880569535722827721 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_160 : Uρ (3519728384093 / 32000000000000) ≤ -(23235726291618061649999 / 10000000000000000000000)

theorem Zeta5Irrational.U_161_1 : Uω (aρ 1) (bρ 1) (7061879112973 / 64000000000000) ≤ -(22645518540262755321593 / 10000000000000000000000)

theorem Zeta5Irrational.U_161_2 : Uω (aρ 2) (bρ 2) (7061879112973 / 64000000000000) ≤ -(22885774473786439499311 / 10000000000000000000000)

theorem Zeta5Irrational.U_161_3 : Uω (aρ 3) (bρ 3) (7061879112973 / 64000000000000) ≤ -(4678666681552500330723 / 2000000000000000000000)

theorem Zeta5Irrational.U_161_4 : Uω (aρ 4) (bρ 4) (7061879112973 / 64000000000000) ≤ -(12166473716122874792837 / 5000000000000000000000)

theorem Zeta5Irrational.U_161_5 : Uω (aρ 5) (bρ 5) (7061879112973 / 64000000000000) ≤ -(26104083312985725933909 / 10000000000000000000000)

theorem Zeta5Irrational.U_161_6 : Uω (aρ 6) (bρ 6) (7061879112973 / 64000000000000) ≤ -(30474581016948763726831 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_161 : Uρ (7061879112973 / 64000000000000) ≤ -(725589995154055185789 / 312500000000000000000)

theorem Zeta5Irrational.U_162_1 : Uω (aρ 1) (bρ 1) (44276884111 / 400000000000) ≤ -(22611842825845109650421 / 10000000000000000000000)

theorem Zeta5Irrational.U_162_2 : Uω (aρ 2) (bρ 2) (44276884111 / 400000000000) ≤ -(5712812751008120059167 / 2500000000000000000000)

theorem Zeta5Irrational.U_162_3 : Uω (aρ 3) (bρ 3) (44276884111 / 400000000000) ≤ -(364951699124394211791 / 156250000000000000000)

theorem Zeta5Irrational.U_162_4 : Uω (aρ 4) (bρ 4) (44276884111 / 400000000000) ≤ -(12146275602580457198217 / 5000000000000000000000)

theorem Zeta5Irrational.U_162_5 : Uω (aρ 5) (bρ 5) (44276884111 / 400000000000) ≤ -(26054086950097842529433 / 10000000000000000000000)

theorem Zeta5Irrational.U_162_6 : Uω (aρ 6) (bρ 6) (44276884111 / 400000000000) ≤ -(7593519709594403117721 / 2500000000000000000000)

theorem Zeta5Irrational.U_162_7 : Uω (aρ 7) (bρ 7) (44276884111 / 400000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_162_8 : Uω (aρ 8) (bρ 8) (44276884111 / 400000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_162_9 : Uω (aρ 9) (bρ 9) (44276884111 / 400000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_162_10 : Uω (aρ 10) (bρ 10) (44276884111 / 400000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_162_11 : Uω (aρ 11) (bρ 11) (44276884111 / 400000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_162_12 : Uω (aρ 12) (bρ 12) (44276884111 / 400000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_162_13 : Uω (aρ 13) (bρ 13) (44276884111 / 400000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_162_14 : Uω (aρ 14) (bρ 14) (44276884111 / 400000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_162_15 : Uω (aρ 15) (bρ 15) (44276884111 / 400000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_162_16 : Uω (aρ 16) (bρ 16) (44276884111 / 400000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_162 : Uρ (44276884111 / 400000000000) ≤ -(1450138413038403161583 / 625000000000000000000)

theorem Zeta5Irrational.U_163_1 : Uω (aρ 1) (bρ 1) (7106723802547 / 64000000000000) ≤ -(2822285021227761372561 / 1250000000000000000000)

theorem Zeta5Irrational.U_163_2 : Uω (aρ 2) (bρ 2) (7106723802547 / 64000000000000) ≤ -(22816846554124106986407 / 10000000000000000000000)

theorem Zeta5Irrational.U_163_3 : Uω (aρ 3) (bρ 3) (7106723802547 / 64000000000000) ≤ -(23320617319657831171039 / 10000000000000000000000)

theorem Zeta5Irrational.U_163_4 : Uω (aρ 4) (bρ 4) (7106723802547 / 64000000000000) ≤ -(24252321955188649295791 / 10000000000000000000000)

theorem Zeta5Irrational.U_163_5 : Uω (aρ 5) (bρ 5) (7106723802547 / 64000000000000) ≤ -(26004364686440584843293 / 10000000000000000000000)

theorem Zeta5Irrational.U_163_6 : Uω (aρ 6) (bρ 6) (7106723802547 / 64000000000000) ≤ -(15137646071887000568089 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_163 : Uρ (7106723802547 / 64000000000000) ≤ -(23185723736921093732363 / 10000000000000000000000)

theorem Zeta5Irrational.U_164_1 : Uω (aρ 1) (bρ 1) (3564573073667 / 32000000000000) ≤ -(4508965963075115482201 / 2000000000000000000000)

theorem Zeta5Irrational.U_164_2 : Uω (aρ 2) (bρ 2) (3564573073667 / 32000000000000) ≤ -(2278256030458170454529 / 1000000000000000000000)

theorem Zeta5Irrational.U_164_3 : Uω (aρ 3) (bρ 3) (3564573073667 / 32000000000000) ≤ -(23284458156104073445189 / 10000000000000000000000)

theorem Zeta5Irrational.U_164_4 : Uω (aρ 4) (bρ 4) (3564573073667 / 32000000000000) ≤ -(2421225827178593245939 / 1000000000000000000000)

theorem Zeta5Irrational.U_164_5 : Uω (aρ 5) (bρ 5) (3564573073667 / 32000000000000) ≤ -(5190982654415919228157 / 2000000000000000000000)

theorem Zeta5Irrational.U_164_6 : Uω (aρ 6) (bρ 6) (3564573073667 / 32000000000000) ≤ -(30178145148616695910741 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_164 : Uρ (3564573073667 / 32000000000000) ≤ -(23169400871890508402437 / 10000000000000000000000)

theorem Zeta5Irrational.U_165_1 : Uω (aρ 1) (bρ 1) (7151568492121 / 64000000000000) ≤ -(225114910132635713543 / 100000000000000000000)

theorem Zeta5Irrational.U_165_2 : Uω (aρ 2) (bρ 2) (7151568492121 / 64000000000000) ≤ -(11374195722188479028337 / 5000000000000000000000)

theorem Zeta5Irrational.U_165_3 : Uω (aρ 3) (bρ 3) (7151568492121 / 64000000000000) ≤ -(23248430285377622815949 / 10000000000000000000000)

theorem Zeta5Irrational.U_165_4 : Uω (aρ 4) (bρ 4) (7151568492121 / 64000000000000) ≤ -(24172358762633393102107 / 10000000000000000000000)

theorem Zeta5Irrational.U_165_5 : Uω (aρ 5) (bρ 5) (7151568492121 / 64000000000000) ≤ -(25905729518360809311063 / 10000000000000000000000)

theorem Zeta5Irrational.U_165_6 : Uω (aρ 6) (bρ 6) (7151568492121 / 64000000000000) ≤ -(30082567552000849825557 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_165 : Uρ (7151568492121 / 64000000000000) ≤ -(11576620047079105469959 / 5000000000000000000000)

theorem Zeta5Irrational.U_166_1 : Uω (aρ 1) (bρ 1) (1793497709227 / 16000000000000) ≤ -(22478263021719406875639 / 10000000000000000000000)

theorem Zeta5Irrational.U_166_2 : Uω (aρ 2) (bρ 2) (1793497709227 / 16000000000000) ≤ -(181714713366534310893 / 80000000000000000000)

theorem Zeta5Irrational.U_166_3 : Uω (aρ 3) (bρ 3) (1793497709227 / 16000000000000) ≤ -(2901566593777723928731 / 1250000000000000000000)

theorem Zeta5Irrational.U_166_4 : Uω (aρ 4) (bρ 4) (1793497709227 / 16000000000000) ≤ -(12066311026658035428937 / 5000000000000000000000)

theorem Zeta5Irrational.U_166_5 : Uω (aρ 5) (bρ 5) (1793497709227 / 16000000000000) ≤ -(12928405148153663752511 / 5000000000000000000000)

theorem Zeta5Irrational.U_166_6 : Uω (aρ 6) (bρ 6) (1793497709227 / 16000000000000) ≤ -(14994246997006309491453 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_166 : Uρ (1793497709227 / 16000000000000) ≤ -(4627447176003051539293 / 2000000000000000000000)

theorem Zeta5Irrational.U_167_1 : Uω (aρ 1) (bρ 1) (1439282636339 / 12800000000000) ≤ -(22445145106352584507421 / 10000000000000000000000)

theorem Zeta5Irrational.U_167_2 : Uω (aρ 2) (bρ 2) (1439282636339 / 12800000000000) ≤ -(2835050336178665111439 / 1250000000000000000000)

theorem Zeta5Irrational.U_167_3 : Uω (aρ 3) (bρ 3) (1439282636339 / 12800000000000) ≤ -(2317676460388831441057 / 1000000000000000000000)

theorem Zeta5Irrational.U_167_4 : Uω (aρ 4) (bρ 4) (1439282636339 / 12800000000000) ≤ -(24093046787011313355059 / 10000000000000000000000)

theorem Zeta5Irrational.U_167_5 : Uω (aρ 5) (bρ 5) (1439282636339 / 12800000000000) ≤ -(6452038133767527073457 / 2500000000000000000000)

theorem Zeta5Irrational.U_167_6 : Uω (aρ 6) (bρ 6) (1439282636339 / 12800000000000) ≤ -(29895863580366005101939 / 10000000000000000000000)

theorem Zeta5Irrational.U_167_7 : Uω (aρ 7) (bρ 7) (1439282636339 / 12800000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_167_8 : Uω (aρ 8) (bρ 8) (1439282636339 / 12800000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_167_9 : Uω (aρ 9) (bρ 9) (1439282636339 / 12800000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_167 : Uρ (1439282636339 / 12800000000000) ≤ -(11560691531889299496159 / 5000000000000000000000)

theorem Zeta5Irrational.U_168_1 : Uω (aρ 1) (bρ 1) (3609417763241 / 32000000000000) ≤ -(22412136540051290770829 / 10000000000000000000000)

theorem Zeta5Irrational.U_168_2 : Uω (aρ 2) (bρ 2) (3609417763241 / 32000000000000) ≤ -(22646581213851753936333 / 10000000000000000000000)

theorem Zeta5Irrational.U_168_3 : Uω (aρ 3) (bρ 3) (3609417763241 / 32000000000000) ≤ -(23141124909983015902357 / 10000000000000000000000)

theorem Zeta5Irrational.U_168_4 : Uω (aρ 4) (bρ 4) (3609417763241 / 32000000000000) ≤ -(12026815812091775261959 / 5000000000000000000000)

theorem Zeta5Irrational.U_168_5 : Uω (aρ 5) (bρ 5) (3609417763241 / 32000000000000) ≤ -(12879876610215081971411 / 5000000000000000000000)

theorem Zeta5Irrational.U_168_6 : Uω (aρ 6) (bρ 6) (3609417763241 / 32000000000000) ≤ -(7451154866094100783241 / 2500000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_168 : Uρ (3609417763241 / 32000000000000) ≤ -(2310567680468791145093 / 1000000000000000000000)

theorem Zeta5Irrational.U_169_1 : Uω (aρ 1) (bρ 1) (7241257871269 / 64000000000000) ≤ -(22379236602886479923973 / 10000000000000000000000)

theorem Zeta5Irrational.U_169_2 : Uω (aρ 2) (bρ 2) (7241257871269 / 64000000000000) ≤ -(22612873965720201807563 / 10000000000000000000000)

theorem Zeta5Irrational.U_169_3 : Uω (aρ 3) (bρ 3) (7241257871269 / 64000000000000) ≤ -(23105612742314276111357 / 10000000000000000000000)

theorem Zeta5Irrational.U_169_4 : Uω (aρ 4) (bρ 4) (7241257871269 / 64000000000000) ≤ -(24014375242285785827619 / 10000000000000000000000)

theorem Zeta5Irrational.U_169_5 : Uω (aρ 5) (bρ 5) (7241257871269 / 64000000000000) ≤ -(25711609393350256228287 / 10000000000000000000000)

theorem Zeta5Irrational.U_169_6 : Uω (aρ 6) (bρ 6) (7241257871269 / 64000000000000) ≤ -(29714708478032058836987 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_169 : Uρ (7241257871269 / 64000000000000) ≤ -(23090112557678937190821 / 10000000000000000000000)

theorem Zeta5Irrational.U_170_1 : Uω (aρ 1) (bρ 1) (907960027007 / 8000000000000) ≤ -(1396652786376097337059 / 625000000000000000000)

theorem Zeta5Irrational.U_170_2 : Uω (aρ 2) (bρ 2) (907960027007 / 8000000000000) ≤ -(22579280174561325422027 / 10000000000000000000000)

theorem Zeta5Irrational.U_170_3 : Uω (aρ 3) (bρ 3) (907960027007 / 8000000000000) ≤ -(4614045436948869884133 / 2000000000000000000000)

theorem Zeta5Irrational.U_170_4 : Uω (aρ 4) (bρ 4) (907960027007 / 8000000000000) ≤ -(1498454770966725311139 / 625000000000000000000)

theorem Zeta5Irrational.U_170_5 : Uω (aρ 5) (bρ 5) (907960027007 / 8000000000000) ≤ -(12831859074287055078487 / 5000000000000000000000)

theorem Zeta5Irrational.U_170_6 : Uω (aρ 6) (bρ 6) (907960027007 / 8000000000000) ≤ -(29626080805288577062113 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_170 : Uρ (907960027007 / 8000000000000) ≤ -(23074686047490937971453 / 10000000000000000000000)

theorem Zeta5Irrational.U_171_1 : Uω (aρ 1) (bρ 1) (7286102560843 / 64000000000000) ≤ -(2789219971449951260491 / 1250000000000000000000)

theorem Zeta5Irrational.U_171_2 : Uω (aρ 2) (bρ 2) (7286102560843 / 64000000000000) ≤ -(11272899538842934213803 / 5000000000000000000000)

theorem Zeta5Irrational.U_171_3 : Uω (aρ 3) (bρ 3) (7286102560843 / 64000000000000) ≤ -(23034967331043341839631 / 10000000000000000000000)

theorem Zeta5Irrational.U_171_4 : Uω (aρ 4) (bρ 4) (7286102560843 / 64000000000000) ≤ -(11968166807144784725189 / 5000000000000000000000)

theorem Zeta5Irrational.U_171_5 : Uω (aρ 5) (bρ 5) (7286102560843 / 64000000000000) ≤ -(25616076633271137021301 / 10000000000000000000000)

theorem Zeta5Irrational.U_171_6 : Uω (aρ 6) (bρ 6) (7286102560843 / 64000000000000) ≤ -(29538689691821717904251 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_171 : Uρ (7286102560843 / 64000000000000) ≤ -(4611878649130685497723 / 2000000000000000000000)