Documentation

LeanPool.Zeta5Irrational.Table.U52

Certified arcsine potential bounds (U52) #

source
theorem Zeta5Irrational.U_628_1 :
Uω (aρ 1) (bρ 1) (11671906263691 / 16000000000000) ≤ -(3242877128542114788709 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_628_2 :
Uω (aρ 2) (bρ 2) (11671906263691 / 16000000000000) ≤ -(1637989077187245085489 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_628_3 :
Uω (aρ 3) (bρ 3) (11671906263691 / 16000000000000) ≤ -(3342479810571222740781 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_628_4 :
Uω (aρ 4) (bρ 4) (11671906263691 / 16000000000000) ≤ -(3453819726866507349207 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_628_5 :
Uω (aρ 5) (bρ 5) (11671906263691 / 16000000000000) ≤ -(3625538355383480504909 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_628_6 :
Uω (aρ 6) (bρ 6) (11671906263691 / 16000000000000) ≤ -(193823918117542028053 / 500000000000000000000)
source
theorem Zeta5Irrational.U_628_7 :
Uω (aρ 7) (bρ 7) (11671906263691 / 16000000000000) ≤ -(132124751893165640127 / 312500000000000000000)
source
theorem Zeta5Irrational.U_628_8 :
Uω (aρ 8) (bρ 8) (11671906263691 / 16000000000000) ≤ -(4703268327102192686097 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_628_9 :
Uω (aρ 9) (bρ 9) (11671906263691 / 16000000000000) ≤ -(5326895601779464101117 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_628_10 :
Uω (aρ 10) (bρ 10) (11671906263691 / 16000000000000) ≤ -(3062433192379457887933 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_628_11 :
Uω (aρ 11) (bρ 11) (11671906263691 / 16000000000000) ≤ -(7125471243255631514223 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_628_12 :
Uω (aρ 12) (bρ 12) (11671906263691 / 16000000000000) ≤ -(8362255243951402653027 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_628_13 :
Uω (aρ 13) (bρ 13) (11671906263691 / 16000000000000) ≤ -(9883039534702144509293 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_628_14 :
Uω (aρ 14) (bρ 14) (11671906263691 / 16000000000000) ≤ -(589233722447172838279 / 500000000000000000000)
source
theorem Zeta5Irrational.U_628_15 :
Uω (aρ 15) (bρ 15) (11671906263691 / 16000000000000) ≤ -(7240890309318723000821 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_628_16 :
Uω (aρ 16) (bρ 16) (11671906263691 / 16000000000000) ≤ -(419641552645073499393 / 250000000000000000000)
source
theorem Zeta5Irrational.U_628 :
Uρ (11671906263691 / 16000000000000) ≤ -(1399085531536063093099 / 2500000000000000000000)
source
theorem Zeta5Irrational.U_629_1 :
Uω (aρ 1) (bρ 1) (23374289245939 / 32000000000000) ≤ -(645942733699712492987 / 2000000000000000000000)
source
theorem Zeta5Irrational.U_629_2 :
Uω (aρ 2) (bρ 2) (23374289245939 / 32000000000000) ≤ -(815692712508334048631 / 2500000000000000000000)
source
theorem Zeta5Irrational.U_629_3 :
Uω (aρ 3) (bρ 3) (23374289245939 / 32000000000000) ≤ -(832295938651579155123 / 2500000000000000000000)
source
theorem Zeta5Irrational.U_629_4 :
Uω (aρ 4) (bρ 4) (23374289245939 / 32000000000000) ≤ -(3440373057157870478887 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_629_5 :
Uω (aρ 5) (bρ 5) (23374289245939 / 32000000000000) ≤ -(722370860654510914959 / 2000000000000000000000)
source
theorem Zeta5Irrational.U_629_6 :
Uω (aρ 6) (bρ 6) (23374289245939 / 32000000000000) ≤ -(965608962956098136493 / 2500000000000000000000)
source
theorem Zeta5Irrational.U_629_7 :
Uω (aρ 7) (bρ 7) (23374289245939 / 32000000000000) ≤ -(105335573704855377237 / 250000000000000000000)
source
theorem Zeta5Irrational.U_629_8 :
Uω (aρ 8) (bρ 8) (23374289245939 / 32000000000000) ≤ -(4687937817110196890423 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_629_9 :
Uω (aρ 9) (bρ 9) (23374289245939 / 32000000000000) ≤ -(5310469239407437719787 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_629_10 :
Uω (aρ 10) (bρ 10) (23374289245939 / 32000000000000) ≤ -(3053424875716178132791 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_629_11 :
Uω (aρ 11) (bρ 11) (23374289245939 / 32000000000000) ≤ -(1421017869337593465473 / 2000000000000000000000)
source
theorem Zeta5Irrational.U_629_12 :
Uω (aρ 12) (bρ 12) (23374289245939 / 32000000000000) ≤ -(833817983441931326163 / 1000000000000000000000)
source
theorem Zeta5Irrational.U_629_13 :
Uω (aρ 13) (bρ 13) (23374289245939 / 32000000000000) ≤ -(12315806207499133563 / 12500000000000000000)
source
theorem Zeta5Irrational.U_629_14 :
Uω (aρ 14) (bρ 14) (23374289245939 / 32000000000000) ≤ -(469647681200431082067 / 400000000000000000000)
source
theorem Zeta5Irrational.U_629_15 :
Uω (aρ 15) (bρ 15) (23374289245939 / 32000000000000) ≤ -(14386903830489276582459 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_629_16 :
Uω (aρ 16) (bρ 16) (23374289245939 / 32000000000000) ≤ -(419641552645073499393 / 250000000000000000000)
source
theorem Zeta5Irrational.U_629 :
Uρ (23374289245939 / 32000000000000) ≤ -(5576914744225668371273 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_630_1 :
Uω (aρ 1) (bρ 1) (1462797872781 / 2000000000000) ≤ -(3216567513452919317099 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_630_2 :
Uω (aρ 2) (bρ 2) (1462797872781 / 2000000000000) ≤ -(1624790483342472992419 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_630_3 :
Uω (aρ 3) (bρ 3) (1462797872781 / 2000000000000) ≤ -(1657952678109447268993 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_630_4 :
Uω (aρ 4) (bρ 4) (1462797872781 / 2000000000000) ≤ -(3426944452015668801577 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_630_5 :
Uω (aρ 5) (bρ 5) (1462797872781 / 2000000000000) ≤ -(1799094485697806630207 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_630_6 :
Uω (aρ 6) (bρ 6) (1462797872781 / 2000000000000) ≤ -(38484130851782445057 / 100000000000000000000)
source
theorem Zeta5Irrational.U_630_7 :
Uω (aρ 7) (bρ 7) (1462797872781 / 2000000000000) ≤ -(524859394838169808527 / 1250000000000000000000)
source
theorem Zeta5Irrational.U_630_8 :
Uω (aρ 8) (bρ 8) (1462797872781 / 2000000000000) ≤ -(4672631077418728873253 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_630_9 :
Uω (aρ 9) (bρ 9) (1462797872781 / 2000000000000) ≤ -(529407052921083357707 / 1000000000000000000000)
source
theorem Zeta5Irrational.U_630_10 :
Uω (aρ 10) (bρ 10) (1462797872781 / 2000000000000) ≤ -(3044433606727779236829 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_630_11 :
Uω (aρ 11) (bρ 11) (1462797872781 / 2000000000000) ≤ -(7084753080275469726601 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_630_12 :
Uω (aρ 12) (bρ 12) (1462797872781 / 2000000000000) ≤ -(1662834675285439792897 / 2000000000000000000000)
source
theorem Zeta5Irrational.U_630_13 :
Uω (aρ 13) (bρ 13) (1462797872781 / 2000000000000) ≤ -(9822377166288816452343 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_630_14 :
Uω (aρ 14) (bρ 14) (1462797872781 / 2000000000000) ≤ -(5849024699973716311919 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_630_15 :
Uω (aρ 15) (bρ 15) (1462797872781 / 2000000000000) ≤ -(7147600066389320593217 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_630_16 :
Uω (aρ 16) (bρ 16) (1462797872781 / 2000000000000) ≤ -(419641552645073499393 / 250000000000000000000)
source
theorem Zeta5Irrational.U_630 :
Uρ (1462797872781 / 2000000000000) ≤ -(5557629648906738505043 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_631_1 :
Uω (aρ 1) (bρ 1) (23435242683053 / 32000000000000) ≤ -(3203438617965511292341 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_631_2 :
Uω (aρ 2) (bρ 2) (23435242683053 / 32000000000000) ≤ -(3236408458429937679207 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_631_3 :
Uω (aρ 3) (bρ 3) (23435242683053 / 32000000000000) ≤ -(132105782742592253447 / 400000000000000000000)
source
theorem Zeta5Irrational.U_631_4 :
Uω (aρ 4) (bρ 4) (23435242683053 / 32000000000000) ≤ -(3413533862948097198867 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_631_5 :
Uω (aρ 5) (bρ 5) (23435242683053 / 32000000000000) ≤ -(3584542308547022505337 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_631_6 :
Uω (aρ 6) (bρ 6) (23435242683053 / 32000000000000) ≤ -(3834410006823929320503 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_631_7 :
Uω (aρ 7) (bρ 7) (23435242683053 / 32000000000000) ≤ -(836869725883868706071 / 2000000000000000000000)
source
theorem Zeta5Irrational.U_631_8 :
Uω (aρ 8) (bρ 8) (23435242683053 / 32000000000000) ≤ -(931469606699471203557 / 2000000000000000000000)
source
theorem Zeta5Irrational.U_631_9 :
Uω (aρ 9) (bρ 9) (23435242683053 / 32000000000000) ≤ -(5277699375886241265793 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_631_10 :
Uω (aρ 10) (bρ 10) (23435242683053 / 32000000000000) ≤ -(758864829476275798249 / 1250000000000000000000)
source
theorem Zeta5Irrational.U_631_11 :
Uω (aρ 11) (bρ 11) (23435242683053 / 32000000000000) ≤ -(7064462222460948975133 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_631_12 :
Uω (aρ 12) (bρ 12) (23435242683053 / 32000000000000) ≤ -(8290235418091904679413 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_631_13 :
Uω (aρ 13) (bρ 13) (23435242683053 / 32000000000000) ≤ -(9792234836373217187103 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_631_14 :
Uω (aρ 14) (bρ 14) (23435242683053 / 32000000000000) ≤ -(2913809875003440331781 / 2500000000000000000000)
source
theorem Zeta5Irrational.U_631_15 :
Uω (aρ 15) (bρ 15) (23435242683053 / 32000000000000) ≤ -(221974656099820521723 / 156250000000000000000)
source
theorem Zeta5Irrational.U_631_16 :
Uω (aρ 16) (bρ 16) (23435242683053 / 32000000000000) ≤ -(419641552645073499393 / 250000000000000000000)
source
theorem Zeta5Irrational.U_631 :
Uρ (23435242683053 / 32000000000000) ≤ -(86538710522970460249 / 156250000000000000000)
source
theorem Zeta5Irrational.U_632_1 :
Uω (aρ 1) (bρ 1) (2346571940161 / 3200000000000) ≤ -(1595163468387701664069 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_632_2 :
Uω (aρ 2) (bρ 2) (2346571940161 / 3200000000000) ≤ -(3223253279550098399567 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_632_3 :
Uω (aρ 3) (bρ 3) (2346571940161 / 3200000000000) ≤ -(3289401344986094540583 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_632_4 :
Uω (aρ 4) (bρ 4) (2346571940161 / 3200000000000) ≤ -(680028248331685089271 / 2000000000000000000000)
source
theorem Zeta5Irrational.U_632_5 :
Uω (aρ 5) (bρ 5) (2346571940161 / 3200000000000) ≤ -(1785457131865592913579 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_632_6 :
Uω (aρ 6) (bρ 6) (2346571940161 / 3200000000000) ≤ -(1910213280704012408157 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_632_7 :
Uω (aρ 7) (bρ 7) (2346571940161 / 3200000000000) ≤ -(4169843297918505665339 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_632_8 :
Uω (aρ 8) (bρ 8) (2346571940161 / 3200000000000) ≤ -(2321044305584939681371 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_632_9 :
Uω (aρ 9) (bρ 9) (2346571940161 / 3200000000000) ≤ -(5261355684633632966319 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_632_10 :
Uω (aρ 10) (bρ 10) (2346571940161 / 3200000000000) ≤ -(6053003884311726330449 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_632_11 :
Uω (aρ 11) (bρ 11) (2346571940161 / 3200000000000) ≤ -(7044216553404438458349 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_632_12 :
Uω (aρ 12) (bρ 12) (2346571940161 / 3200000000000) ≤ -(4133182756188624599249 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_632_13 :
Uω (aρ 13) (bρ 13) (2346571940161 / 3200000000000) ≤ -(9762216699229738464429 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_632_14 :
Uω (aρ 14) (bρ 14) (2346571940161 / 3200000000000) ≤ -(11612755515422022468479 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_632_15 :
Uω (aρ 15) (bρ 15) (2346571940161 / 3200000000000) ≤ -(2824037625449027245121 / 2000000000000000000000)
source
theorem Zeta5Irrational.U_632_16 :
Uω (aρ 16) (bρ 16) (2346571940161 / 3200000000000) ≤ -(419641552645073499393 / 250000000000000000000)
source
theorem Zeta5Irrational.U_632 :
Uρ (2346571940161 / 3200000000000) ≤ -(5519450151378080841463 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_633_1 :
Uω (aρ 1) (bρ 1) (23496196120167 / 32000000000000) ≤ -(1588616212399733649147 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_633_2 :
Uω (aρ 2) (bρ 2) (23496196120167 / 32000000000000) ≤ -(3210115384507427481169 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_633_3 :
Uω (aρ 3) (bρ 3) (23496196120167 / 32000000000000) ≤ -(131047025560400143257 / 400000000000000000000)
source
theorem Zeta5Irrational.U_633_4 :
Uω (aρ 4) (bρ 4) (23496196120167 / 32000000000000) ≤ -(846691635010987255199 / 2500000000000000000000)
source
theorem Zeta5Irrational.U_633_5 :
Uω (aρ 5) (bρ 5) (23496196120167 / 32000000000000) ≤ -(3557304786161391909607 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_633_6 :
Uω (aρ 6) (bρ 6) (23496196120167 / 32000000000000) ≤ -(3806462693810826226399 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_633_7 :
Uω (aρ 7) (bρ 7) (23496196120167 / 32000000000000) ≤ -(2077679551030624965963 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_633_8 :
Uω (aρ 8) (bρ 8) (23496196120167 / 32000000000000) ≤ -(4626852736612063300721 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_633_9 :
Uω (aρ 9) (bρ 9) (23496196120167 / 32000000000000) ≤ -(5245039361152753413503 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_633_10 :
Uω (aρ 10) (bρ 10) (23496196120167 / 32000000000000) ≤ -(1508780706400550594719 / 2500000000000000000000)
source
theorem Zeta5Irrational.U_633_11 :
Uω (aρ 11) (bρ 11) (23496196120167 / 32000000000000) ≤ -(219500495467645514591 / 312500000000000000000)
source
theorem Zeta5Irrational.U_633_12 :
Uω (aρ 12) (bρ 12) (23496196120167 / 32000000000000) ≤ -(1030320402127628943133 / 1250000000000000000000)
source
theorem Zeta5Irrational.U_633_13 :
Uω (aρ 13) (bρ 13) (23496196120167 / 32000000000000) ≤ -(304135046858737321201 / 312500000000000000000)
source
theorem Zeta5Irrational.U_633_14 :
Uω (aρ 14) (bρ 14) (23496196120167 / 32000000000000) ≤ -(11570590863640125216681 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_633_15 :
Uω (aρ 15) (bρ 15) (23496196120167 / 32000000000000) ≤ -(7018207705648636198711 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_633_16 :
Uω (aρ 16) (bρ 16) (23496196120167 / 32000000000000) ≤ -(419641552645073499393 / 250000000000000000000)
source
theorem Zeta5Irrational.U_633 :
Uρ (23496196120167 / 32000000000000) ≤ -(5500540668506838355503 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_634_1 :
Uω (aρ 1) (bρ 1) (5881668209681 / 8000000000000) ≤ -(3164155037131447097627 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_634_2 :
Uω (aρ 2) (bρ 2) (5881668209681 / 8000000000000) ≤ -(3196994727943193935909 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_634_3 :
Uω (aρ 3) (bρ 3) (5881668209681 / 8000000000000) ≤ -(163148370217400263421 / 500000000000000000000)
source
theorem Zeta5Irrational.U_634_4 :
Uω (aρ 4) (bρ 4) (5881668209681 / 8000000000000) ≤ -(3373409710194953931207 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_634_5 :
Uω (aρ 5) (bρ 5) (5881668209681 / 8000000000000) ≤ -(3543713825258676462001 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_634_6 :
Uω (aρ 6) (bρ 6) (5881668209681 / 8000000000000) ≤ -(3792518349145028688873 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_634_7 :
Uω (aρ 7) (bρ 7) (5881668209681 / 8000000000000) ≤ -(1035223994995105045411 / 2500000000000000000000)
source
theorem Zeta5Irrational.U_634_8 :
Uω (aρ 8) (bρ 8) (5881668209681 / 8000000000000) ≤ -(4611640336349390814731 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_634_9 :
Uω (aρ 9) (bρ 9) (5881668209681 / 8000000000000) ≤ -(5228750311639540664367 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_634_10 :
Uω (aρ 10) (bρ 10) (5881668209681 / 8000000000000) ≤ -(6017275327143369276991 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_634_11 :
Uω (aρ 11) (bρ 11) (5881668209681 / 8000000000000) ≤ -(437741244417544630727 / 625000000000000000000)
source
theorem Zeta5Irrational.U_634_12 :
Uω (aρ 12) (bρ 12) (5881668209681 / 8000000000000) ≤ -(4109414047231730727419 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_634_13 :
Uω (aρ 13) (bρ 13) (5881668209681 / 8000000000000) ≤ -(1940509600574714462243 / 2000000000000000000000)
source
theorem Zeta5Irrational.U_634_14 :
Uω (aρ 14) (bρ 14) (5881668209681 / 8000000000000) ≤ -(90068274870373059033 / 78125000000000000000)
source
theorem Zeta5Irrational.U_634_15 :
Uω (aρ 15) (bρ 15) (5881668209681 / 8000000000000) ≤ -(13954872639935423773157 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_634_16 :
Uω (aρ 16) (bρ 16) (5881668209681 / 8000000000000) ≤ -(419641552645073499393 / 250000000000000000000)
source
theorem Zeta5Irrational.U_634 :
Uρ (5881668209681 / 8000000000000) ≤ -(2740871436653137694881 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_635_1 :
Uω (aρ 1) (bρ 1) (23557149557281 / 32000000000000) ≤ -(630218945808207475073 / 2000000000000000000000)
source
theorem Zeta5Irrational.U_635_2 :
Uω (aρ 2) (bρ 2) (23557149557281 / 32000000000000) ≤ -(636778252935398947851 / 2000000000000000000000)
source
theorem Zeta5Irrational.U_635_3 :
Uω (aρ 3) (bρ 3) (23557149557281 / 32000000000000) ≤ -(649955318978965030579 / 2000000000000000000000)
source
theorem Zeta5Irrational.U_635_4 :
Uω (aρ 4) (bρ 4) (23557149557281 / 32000000000000) ≤ -(672014140878737271299 / 2000000000000000000000)
source
theorem Zeta5Irrational.U_635_5 :
Uω (aρ 5) (bρ 5) (23557149557281 / 32000000000000) ≤ -(882535332662672776061 / 2500000000000000000000)
source
theorem Zeta5Irrational.U_635_6 :
Uω (aρ 6) (bρ 6) (23557149557281 / 32000000000000) ≤ -(1889296736377210212201 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_635_7 :
Uω (aρ 7) (bρ 7) (23557149557281 / 32000000000000) ≤ -(82529077401633511151 / 200000000000000000000)
source
theorem Zeta5Irrational.U_635_8 :
Uω (aρ 8) (bρ 8) (23557149557281 / 32000000000000) ≤ -(1149112834313707893071 / 2500000000000000000000)
source
theorem Zeta5Irrational.U_635_9 :
Uω (aρ 9) (bρ 9) (23557149557281 / 32000000000000) ≤ -(2606244221391287807851 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_635_10 :
Uω (aρ 10) (bρ 10) (23557149557281 / 32000000000000) ≤ -(1499865314302420498799 / 2500000000000000000000)
source
theorem Zeta5Irrational.U_635_11 :
Uω (aρ 11) (bρ 11) (23557149557281 / 32000000000000) ≤ -(6983748505754081904723 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_635_12 :
Uω (aρ 12) (bρ 12) (23557149557281 / 32000000000000) ≤ -(1639031942355393550651 / 2000000000000000000000)
source
theorem Zeta5Irrational.U_635_13 :
Uω (aρ 13) (bρ 13) (23557149557281 / 32000000000000) ≤ -(4836447497896644797437 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_635_14 :
Uω (aρ 14) (bρ 14) (23557149557281 / 32000000000000) ≤ -(11487194324412495821493 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_635_15 :
Uω (aρ 15) (bρ 15) (23557149557281 / 32000000000000) ≤ -(346884892714684572593 / 250000000000000000000)
source
theorem Zeta5Irrational.U_635_16 :
Uω (aρ 16) (bρ 16) (23557149557281 / 32000000000000) ≤ -(419641552645073499393 / 250000000000000000000)
source
theorem Zeta5Irrational.U_635 :
Uρ (23557149557281 / 32000000000000) ≤ -(109261026582514005137 / 200000000000000000000)
source
theorem Zeta5Irrational.U_636_1 :
Uω (aρ 1) (bρ 1) (11793813137919 / 16000000000000) ≤ -(627610291194593107191 / 2000000000000000000000)
source
theorem Zeta5Irrational.U_636_2 :
Uω (aρ 2) (bρ 2) (11793813137919 / 16000000000000) ≤ -(634160989941164399659 / 2000000000000000000000)
source
theorem Zeta5Irrational.U_636_3 :
Uω (aρ 3) (bρ 3) (11793813137919 / 16000000000000) ≤ -(1618301582363736978203 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_636_4 :
Uω (aρ 4) (bρ 4) (11793813137919 / 16000000000000) ≤ -(1673374737556661780137 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_636_5 :
Uω (aρ 5) (bρ 5) (11793813137919 / 16000000000000) ≤ -(3516587252170573535409 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_636_6 :
Uω (aρ 6) (bρ 6) (11793813137919 / 16000000000000) ≤ -(470586001276572675323 / 1250000000000000000000)
source
theorem Zeta5Irrational.U_636_7 :
Uω (aρ 7) (bρ 7) (11793813137919 / 16000000000000) ≤ -(822406542208375767147 / 2000000000000000000000)
source
theorem Zeta5Irrational.U_636_8 :
Uω (aρ 8) (bρ 8) (11793813137919 / 16000000000000) ≤ -(4581285666546628779379 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_636_9 :
Uω (aρ 9) (bρ 9) (11793813137919 / 16000000000000) ≤ -(5196253661759570077241 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_636_10 :
Uω (aρ 10) (bρ 10) (11793813137919 / 16000000000000) ≤ -(5981680484881463733891 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_636_11 :
Uω (aρ 11) (bρ 11) (11793813137919 / 16000000000000) ≤ -(278547257081232514053 / 400000000000000000000)
source
theorem Zeta5Irrational.U_636_12 :
Uω (aρ 12) (bρ 12) (11793813137919 / 16000000000000) ≤ -(817155764059736202051 / 1000000000000000000000)
source
theorem Zeta5Irrational.U_636_13 :
Uω (aρ 13) (bρ 13) (11793813137919 / 16000000000000) ≤ -(9643361284767544950333 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_636_14 :
Uω (aρ 14) (bρ 14) (11793813137919 / 16000000000000) ≤ -(457838013503125911517 / 400000000000000000000)
source
theorem Zeta5Irrational.U_636_15 :
Uω (aρ 15) (bρ 15) (11793813137919 / 16000000000000) ≤ -(6898919903209831485569 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_636_16 :
Uω (aρ 16) (bρ 16) (11793813137919 / 16000000000000) ≤ -(419641552645073499393 / 250000000000000000000)
source
theorem Zeta5Irrational.U_636 :
Uρ (11793813137919 / 16000000000000) ≤ -(5444461197856341892419 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_637_1 :
Uω (aρ 1) (bρ 1) (4723620598879 / 6400000000000) ≤ -(195314073346629939723 / 625000000000000000000)
source
theorem Zeta5Irrational.U_637_2 :
Uω (aρ 2) (bρ 2) (4723620598879 / 6400000000000) ≤ -(25261885905625078749 / 80000000000000000000)
source
theorem Zeta5Irrational.U_637_3 :
Uω (aρ 3) (bρ 3) (4723620598879 / 6400000000000) ≤ -(3223447068104290737667 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_637_4 :
Uω (aρ 4) (bρ 4) (4723620598879 / 6400000000000) ≤ -(166672298750848071597 / 500000000000000000000)
source
theorem Zeta5Irrational.U_637_5 :
Uω (aρ 5) (bρ 5) (4723620598879 / 6400000000000) ≤ -(3503051539855834598479 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_637_6 :
Uω (aρ 6) (bρ 6) (4723620598879 / 6400000000000) ≤ -(750160381464319673849 / 2000000000000000000000)
source
theorem Zeta5Irrational.U_637_7 :
Uω (aρ 7) (bρ 7) (4723620598879 / 6400000000000) ≤ -(1024408110451874314823 / 2500000000000000000000)
source
theorem Zeta5Irrational.U_637_8 :
Uω (aρ 8) (bρ 8) (4723620598879 / 6400000000000) ≤ -(2283071625893052422273 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_637_9 :
Uω (aρ 9) (bρ 9) (4723620598879 / 6400000000000) ≤ -(647505734529234841183 / 1250000000000000000000)
source
theorem Zeta5Irrational.U_637_10 :
Uω (aρ 10) (bρ 10) (4723620598879 / 6400000000000) ≤ -(2981966440019059832977 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_637_11 :
Uω (aρ 11) (bρ 11) (4723620598879 / 6400000000000) ≤ -(1388731692596799573783 / 2000000000000000000000)
source
theorem Zeta5Irrational.U_637_12 :
Uω (aρ 12) (bρ 12) (4723620598879 / 6400000000000) ≤ -(4074010728528158471861 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_637_13 :
Uω (aρ 13) (bρ 13) (4723620598879 / 6400000000000) ≤ -(2403486424000805781369 / 2500000000000000000000)
source
theorem Zeta5Irrational.U_637_14 :
Uω (aρ 14) (bρ 14) (4723620598879 / 6400000000000) ≤ -(11405001465921323028451 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_637_15 :
Uω (aρ 15) (bρ 15) (4723620598879 / 6400000000000) ≤ -(857629773117390833237 / 625000000000000000000)
source
theorem Zeta5Irrational.U_637_16 :
Uω (aρ 16) (bρ 16) (4723620598879 / 6400000000000) ≤ -(419641552645073499393 / 250000000000000000000)
source
theorem Zeta5Irrational.U_637 :
Uρ (4723620598879 / 6400000000000) ≤ -(339123009167877599779 / 625000000000000000000)
source
theorem Zeta5Irrational.U_638_1 :
Uω (aρ 1) (bρ 1) (2956072464119 / 4000000000000) ≤ -(622403167510487586771 / 2000000000000000000000)
source
theorem Zeta5Irrational.U_638_2 :
Uω (aρ 2) (bρ 2) (2956072464119 / 4000000000000) ≤ -(1572341792758970059237 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_638_3 :
Uω (aρ 3) (bρ 3) (2956072464119 / 4000000000000) ≤ -(802577064865997302589 / 2500000000000000000000)
source
theorem Zeta5Irrational.U_638_4 :
Uω (aρ 4) (bρ 4) (2956072464119 / 4000000000000) ≤ -(20751000980978739367 / 62500000000000000000)
source
theorem Zeta5Irrational.U_638_5 :
Uω (aρ 5) (bρ 5) (2956072464119 / 4000000000000) ≤ -(872383535986811447349 / 2500000000000000000000)
source
theorem Zeta5Irrational.U_638_6 :
Uω (aρ 6) (bρ 6) (2956072464119 / 4000000000000) ≤ -(3736935110110778650981 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_638_7 :
Uω (aρ 7) (bρ 7) (2956072464119 / 4000000000000) ≤ -(81665060031860360223 / 200000000000000000000)
source
theorem Zeta5Irrational.U_638_8 :
Uω (aρ 8) (bρ 8) (2956072464119 / 4000000000000) ≤ -(1137756005218871002723 / 2500000000000000000000)
source
theorem Zeta5Irrational.U_638_9 :
Uω (aρ 9) (bρ 9) (2956072464119 / 4000000000000) ≤ -(1290966248587763081941 / 2500000000000000000000)
source
theorem Zeta5Irrational.U_638_10 :
Uω (aρ 10) (bρ 10) (2956072464119 / 4000000000000) ≤ -(2973109156675716891163 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_638_11 :
Uω (aρ 11) (bρ 11) (2956072464119 / 4000000000000) ≤ -(6923679406295921670647 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_638_12 :
Uω (aρ 12) (bρ 12) (2956072464119 / 4000000000000) ≤ -(4062275370857562616801 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_638_13 :
Uω (aρ 13) (bρ 13) (2956072464119 / 4000000000000) ≤ -(2396161768732546289149 / 2500000000000000000000)
source
theorem Zeta5Irrational.U_638_14 :
Uω (aρ 14) (bρ 14) (2956072464119 / 4000000000000) ≤ -(11364342135936268109407 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_638_15 :
Uω (aρ 15) (bρ 15) (2956072464119 / 4000000000000) ≤ -(13647990650442621606171 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_638_16 :
Uω (aρ 16) (bρ 16) (2956072464119 / 4000000000000) ≤ -(419641552645073499393 / 250000000000000000000)
source
theorem Zeta5Irrational.U_638 :
Uρ (2956072464119 / 4000000000000) ≤ -(675946034224267949889 / 1250000000000000000000)
source
theorem Zeta5Irrational.U_639_1 :
Uω (aρ 1) (bρ 1) (23679056431509 / 32000000000000) ≤ -(3099023403956418114027 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_639_2 :
Uω (aρ 2) (bρ 2) (23679056431509 / 32000000000000) ≤ -(3131648447173872218449 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_639_3 :
Uω (aρ 3) (bρ 3) (23679056431509 / 32000000000000) ≤ -(3197186693424707257857 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_639_4 :
Uω (aρ 4) (bρ 4) (23679056431509 / 32000000000000) ≤ -(3306891973972135931103 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_639_5 :
Uω (aρ 5) (bρ 5) (23679056431509 / 32000000000000) ≤ -(54313047107620936833 / 156250000000000000000)
source
theorem Zeta5Irrational.U_639_6 :
Uω (aρ 6) (bρ 6) (23679056431509 / 32000000000000) ≤ -(3723087564835383075901 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_639_7 :
Uω (aρ 7) (bρ 7) (23679056431509 / 32000000000000) ≤ -(2034447164939685717283 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_639_8 :
Uω (aρ 8) (bρ 8) (23679056431509 / 32000000000000) ≤ -(2267963951027866300151 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_639_9 :
Uω (aρ 9) (bρ 9) (23679056431509 / 32000000000000) ≤ -(5147710924735413315221 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_639_10 :
Uω (aρ 10) (bρ 10) (23679056431509 / 32000000000000) ≤ -(2964268328139464888913 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_639_11 :
Uω (aρ 11) (bρ 11) (23679056431509 / 32000000000000) ≤ -(6903744043443189821783 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_639_12 :
Uω (aρ 12) (bρ 12) (23679056431509 / 32000000000000) ≤ -(4050572539749861997181 / 5000000000000000000000)
source
theorem Zeta5Irrational.U_639_13 :
Uω (aρ 13) (bρ 13) (23679056431509 / 32000000000000) ≤ -(1194433035719959725449 / 1250000000000000000000)
source
theorem Zeta5Irrational.U_639_14 :
Uω (aρ 14) (bρ 14) (23679056431509 / 32000000000000) ≤ -(11323966949471001526601 / 10000000000000000000000)
source
theorem Zeta5Irrational.U_639_15 :
Uω (aρ 15) (bρ 15) (23679056431509 / 32000000000000) ≤ -(3393869927754534575737 / 2500000000000000000000)
source
theorem Zeta5Irrational.U_639_16 :
Uω (aρ 16) (bρ 16) (23679056431509 / 32000000000000) ≤ -(419641552645073499393 / 250000000000000000000)
source
theorem Zeta5Irrational.U_639 :
Uρ (23679056431509 / 32000000000000) ≤ -(2694629023050604486451 / 5000000000000000000000)