Certified arcsine potential bounds (U18)

theorem Zeta5Irrational.U_220_1 : Uω (aρ 1) (bρ 1) (5243003666637 / 32000000000000) ≤ -(18490674215971361238241 / 10000000000000000000000)

theorem Zeta5Irrational.U_220_2 : Uω (aρ 2) (bρ 2) (5243003666637 / 32000000000000) ≤ -(2330825898986484937893 / 1250000000000000000000)

theorem Zeta5Irrational.U_220_3 : Uω (aρ 3) (bρ 3) (5243003666637 / 32000000000000) ≤ -(9484564051395421285797 / 5000000000000000000000)

theorem Zeta5Irrational.U_220_4 : Uω (aρ 4) (bρ 4) (5243003666637 / 32000000000000) ≤ -(9770011278685046203197 / 5000000000000000000000)

theorem Zeta5Irrational.U_220_5 : Uω (aρ 5) (bρ 5) (5243003666637 / 32000000000000) ≤ -(20513758757421810226879 / 10000000000000000000000)

theorem Zeta5Irrational.U_220_6 : Uω (aρ 6) (bρ 6) (5243003666637 / 32000000000000) ≤ -(22234413891121944816083 / 10000000000000000000000)

theorem Zeta5Irrational.U_220_7 : Uω (aρ 7) (bρ 7) (5243003666637 / 32000000000000) ≤ -(26034182944698725387439 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_220 : Uρ (5243003666637 / 32000000000000) ≤ -(10467026257924661355203 / 5000000000000000000000)

theorem Zeta5Irrational.U_221_1 : Uω (aρ 1) (bρ 1) (21028794701819 / 128000000000000) ≤ -(4615631637779595417191 / 2500000000000000000000)

theorem Zeta5Irrational.U_221_2 : Uω (aρ 2) (bρ 2) (21028794701819 / 128000000000000) ≤ -(465450176953729785337 / 250000000000000000000)

theorem Zeta5Irrational.U_221_3 : Uω (aρ 3) (bρ 3) (21028794701819 / 128000000000000) ≤ -(591861141768881967909 / 312500000000000000000)

theorem Zeta5Irrational.U_221_4 : Uω (aρ 4) (bρ 4) (21028794701819 / 128000000000000) ≤ -(9754301871052985929913 / 5000000000000000000000)

theorem Zeta5Irrational.U_221_5 : Uω (aρ 5) (bρ 5) (21028794701819 / 128000000000000) ≤ -(10239375834821808422919 / 5000000000000000000000)

theorem Zeta5Irrational.U_221_6 : Uω (aρ 6) (bρ 6) (21028794701819 / 128000000000000) ≤ -(887650724271362820473 / 400000000000000000000)

theorem Zeta5Irrational.U_221_7 : Uω (aρ 7) (bρ 7) (21028794701819 / 128000000000000) ≤ -(12978083121240946271847 / 5000000000000000000000)

theorem Zeta5Irrational.U_221_8 : Uω (aρ 8) (bρ 8) (21028794701819 / 128000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_221_9 : Uω (aρ 9) (bρ 9) (21028794701819 / 128000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_221 : Uρ (21028794701819 / 128000000000000) ≤ -(20917375244390658060383 / 10000000000000000000000)

theorem Zeta5Irrational.U_222_1 : Uω (aρ 1) (bρ 1) (2108557473709 / 12800000000000) ≤ -(1843445790326284033331 / 1000000000000000000000)

theorem Zeta5Irrational.U_222_2 : Uω (aρ 2) (bρ 2) (2108557473709 / 12800000000000) ≤ -(18589488599339791797713 / 10000000000000000000000)

theorem Zeta5Irrational.U_222_3 : Uω (aρ 3) (bρ 3) (2108557473709 / 12800000000000) ≤ -(1891007244489895609963 / 1000000000000000000000)

theorem Zeta5Irrational.U_222_4 : Uω (aρ 4) (bρ 4) (2108557473709 / 12800000000000) ≤ -(19477284358716666822331 / 10000000000000000000000)

theorem Zeta5Irrational.U_222_5 : Uω (aρ 5) (bρ 5) (2108557473709 / 12800000000000) ≤ -(20443870661181125243673 / 10000000000000000000000)

theorem Zeta5Irrational.U_222_6 : Uω (aρ 6) (bρ 6) (2108557473709 / 12800000000000) ≤ -(11074163943683477485381 / 5000000000000000000000)

theorem Zeta5Irrational.U_222_7 : Uω (aρ 7) (bρ 7) (2108557473709 / 12800000000000) ≤ -(12939557978942782377787 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_222 : Uρ (2108557473709 / 12800000000000) ≤ -(20900817676992104316193 / 10000000000000000000000)

theorem Zeta5Irrational.U_223_1 : Uω (aρ 1) (bρ 1) (21142354772361 / 128000000000000) ≤ -(1840646782995148303141 / 1000000000000000000000)

theorem Zeta5Irrational.U_223_2 : Uω (aρ 2) (bρ 2) (21142354772361 / 128000000000000) ≤ -(4640262822588700036873 / 2500000000000000000000)

theorem Zeta5Irrational.U_223_3 : Uω (aρ 3) (bρ 3) (21142354772361 / 128000000000000) ≤ -(18880675310025809271703 / 10000000000000000000000)

theorem Zeta5Irrational.U_223_4 : Uω (aρ 4) (bρ 4) (21142354772361 / 128000000000000) ≤ -(19446063773434154064433 / 10000000000000000000000)

theorem Zeta5Irrational.U_223_5 : Uω (aρ 5) (bρ 5) (21142354772361 / 128000000000000) ≤ -(20409114799383380511043 / 10000000000000000000000)

theorem Zeta5Irrational.U_223_6 : Uω (aρ 6) (bρ 6) (21142354772361 / 128000000000000) ≤ -(4421118220594607150783 / 2000000000000000000000)

theorem Zeta5Irrational.U_223_7 : Uω (aρ 7) (bρ 7) (21142354772361 / 128000000000000) ≤ -(25803001453402450152699 / 10000000000000000000000)

theorem Zeta5Irrational.U_223_8 : Uω (aρ 8) (bρ 8) (21142354772361 / 128000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_223_9 : Uω (aρ 9) (bρ 9) (21142354772361 / 128000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_223 : Uρ (21142354772361 / 128000000000000) ≤ -(522109422600521759591 / 250000000000000000000)

theorem Zeta5Irrational.U_224_1 : Uω (aρ 1) (bρ 1) (1324945925477 / 8000000000000) ≤ -(4594638973109356257451 / 2500000000000000000000)

theorem Zeta5Irrational.U_224_2 : Uω (aρ 2) (bρ 2) (1324945925477 / 8000000000000) ≤ -(2316586836256544584097 / 1250000000000000000000)

theorem Zeta5Irrational.U_224_3 : Uω (aρ 3) (bρ 3) (1324945925477 / 8000000000000) ≤ -(2356420577366438601497 / 1250000000000000000000)

theorem Zeta5Irrational.U_224_4 : Uω (aρ 4) (bρ 4) (1324945925477 / 8000000000000) ≤ -(3882988271717983275987 / 2000000000000000000000)

theorem Zeta5Irrational.U_224_5 : Uω (aρ 5) (bρ 5) (1324945925477 / 8000000000000) ≤ -(1018724158109815143011 / 500000000000000000000)

theorem Zeta5Irrational.U_224_6 : Uω (aρ 6) (bρ 6) (1324945925477 / 8000000000000) ≤ -(882522226357036714549 / 400000000000000000000)

theorem Zeta5Irrational.U_224_7 : Uω (aρ 7) (bρ 7) (1324945925477 / 8000000000000) ≤ -(643194842372322635267 / 250000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_224 : Uρ (1324945925477 / 8000000000000) ≤ -(4173610031223508181363 / 2000000000000000000000)

theorem Zeta5Irrational.U_225_1 : Uω (aρ 1) (bρ 1) (10656347439087 / 64000000000000) ≤ -(4580741172024563874411 / 2500000000000000000000)

theorem Zeta5Irrational.U_225_2 : Uω (aρ 2) (bρ 2) (10656347439087 / 64000000000000) ≤ -(9238110895246623312471 / 5000000000000000000000)

theorem Zeta5Irrational.U_225_3 : Uω (aρ 3) (bρ 3) (10656347439087 / 64000000000000) ≤ -(939650026926023325251 / 500000000000000000000)

theorem Zeta5Irrational.U_225_4 : Uω (aρ 4) (bρ 4) (10656347439087 / 64000000000000) ≤ -(9676494279784326839573 / 5000000000000000000000)

theorem Zeta5Irrational.U_225_5 : Uω (aρ 5) (bρ 5) (10656347439087 / 64000000000000) ≤ -(20305588925442651515513 / 10000000000000000000000)

theorem Zeta5Irrational.U_225_6 : Uω (aρ 6) (bρ 6) (10656347439087 / 64000000000000) ≤ -(5494645146109420751617 / 2500000000000000000000)

theorem Zeta5Irrational.U_225_7 : Uω (aρ 7) (bρ 7) (10656347439087 / 64000000000000) ≤ -(12789994806014067070709 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_225 : Uρ (10656347439087 / 64000000000000) ≤ -(1302233018806088858069 / 625000000000000000000)

theorem Zeta5Irrational.U_226_1 : Uω (aρ 1) (bρ 1) (5356563737179 / 32000000000000) ≤ -(71358128331416751623 / 39062500000000000000)

theorem Zeta5Irrational.U_226_2 : Uω (aρ 2) (bρ 2) (5356563737179 / 32000000000000) ≤ -(18420066289172837522877 / 10000000000000000000000)

theorem Zeta5Irrational.U_226_3 : Uω (aρ 3) (bρ 3) (5356563737179 / 32000000000000) ≤ -(18734976189111055348777 / 10000000000000000000000)

theorem Zeta5Irrational.U_226_4 : Uω (aρ 4) (bρ 4) (5356563737179 / 32000000000000) ≤ -(19291421059334564470881 / 10000000000000000000000)

theorem Zeta5Irrational.U_226_5 : Uω (aρ 5) (bρ 5) (5356563737179 / 32000000000000) ≤ -(10118590390140244503249 / 5000000000000000000000)

theorem Zeta5Irrational.U_226_6 : Uω (aρ 6) (bρ 6) (5356563737179 / 32000000000000) ≤ -(175159092645873246921 / 80000000000000000000)

theorem Zeta5Irrational.U_226_7 : Uω (aρ 7) (bρ 7) (5356563737179 / 32000000000000) ≤ -(25435499359157548817667 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_226 : Uρ (5356563737179 / 32000000000000) ≤ -(20803832407117668669149 / 10000000000000000000000)

theorem Zeta5Irrational.U_227_1 : Uω (aρ 1) (bρ 1) (10769907509629 / 64000000000000) ≤ -(9106350502993110805211 / 5000000000000000000000)

theorem Zeta5Irrational.U_227_2 : Uω (aρ 2) (bρ 2) (10769907509629 / 64000000000000) ≤ -(18364224635257561809589 / 10000000000000000000000)

theorem Zeta5Irrational.U_227_3 : Uω (aρ 3) (bρ 3) (10769907509629 / 64000000000000) ≤ -(4669321906570947279869 / 2500000000000000000000)

theorem Zeta5Irrational.U_227_4 : Uω (aρ 4) (bρ 4) (10769907509629 / 64000000000000) ≤ -(9615117024126235910581 / 5000000000000000000000)

theorem Zeta5Irrational.U_227_5 : Uω (aρ 5) (bρ 5) (10769907509629 / 64000000000000) ≤ -(20169251715464789785997 / 10000000000000000000000)

theorem Zeta5Irrational.U_227_6 : Uω (aρ 6) (bρ 6) (10769907509629 / 64000000000000) ≤ -(10905979039386153311897 / 5000000000000000000000)

theorem Zeta5Irrational.U_227_7 : Uω (aρ 7) (bρ 7) (10769907509629 / 64000000000000) ≤ -(25294137832826385335031 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_227 : Uρ (10769907509629 / 64000000000000) ≤ -(4154468893221481873091 / 2000000000000000000000)

theorem Zeta5Irrational.U_228_1 : Uω (aρ 1) (bρ 1) (108266875449 / 640000000000) ≤ -(9079010911160674591103 / 5000000000000000000000)

theorem Zeta5Irrational.U_228_2 : Uω (aρ 2) (bρ 2) (108266875449 / 640000000000) ≤ -(18308693337218033383591 / 10000000000000000000000)

theorem Zeta5Irrational.U_228_3 : Uω (aρ 3) (bρ 3) (108266875449 / 640000000000) ≤ -(18619930974125314054273 / 10000000000000000000000)

theorem Zeta5Irrational.U_228_4 : Uω (aρ 4) (bρ 4) (108266875449 / 640000000000) ≤ -(766776912281108700213 / 400000000000000000000)

theorem Zeta5Irrational.U_228_5 : Uω (aρ 5) (bρ 5) (108266875449 / 640000000000) ≤ -(502544871858661952131 / 250000000000000000000)

theorem Zeta5Irrational.U_228_6 : Uω (aρ 6) (bρ 6) (108266875449 / 640000000000) ≤ -(679055625029343955549 / 312500000000000000000)

theorem Zeta5Irrational.U_228_7 : Uω (aρ 7) (bρ 7) (108266875449 / 640000000000) ≤ -(25155736715238488212441 / 10000000000000000000000)

theorem Zeta5Irrational.U_228_8 : Uω (aρ 8) (bρ 8) (108266875449 / 640000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_228_9 : Uω (aρ 9) (bρ 9) (108266875449 / 640000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_228_10 : Uω (aρ 10) (bρ 10) (108266875449 / 640000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_228_11 : Uω (aρ 11) (bρ 11) (108266875449 / 640000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_228_12 : Uω (aρ 12) (bρ 12) (108266875449 / 640000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_228_13 : Uω (aρ 13) (bρ 13) (108266875449 / 640000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_228_14 : Uω (aρ 14) (bρ 14) (108266875449 / 640000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_228_15 : Uω (aρ 15) (bρ 15) (108266875449 / 640000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_228_16 : Uω (aρ 16) (bρ 16) (108266875449 / 640000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_228 : Uρ (108266875449 / 640000000000) ≤ -(5185311988381454830147 / 2500000000000000000000)

theorem Zeta5Irrational.U_229_1 : Uω (aρ 1) (bρ 1) (10883467580171 / 64000000000000) ≤ -(3620728006182036485219 / 2000000000000000000000)

theorem Zeta5Irrational.U_229_2 : Uω (aρ 2) (bρ 2) (10883467580171 / 64000000000000) ≤ -(18253468961514672487477 / 10000000000000000000000)

theorem Zeta5Irrational.U_229_3 : Uω (aρ 3) (bρ 3) (10883467580171 / 64000000000000) ≤ -(9281451211823238992419 / 5000000000000000000000)

theorem Zeta5Irrational.U_229_4 : Uω (aρ 4) (bρ 4) (10883467580171 / 64000000000000) ≤ -(19108982704437711202299 / 10000000000000000000000)

theorem Zeta5Irrational.U_229_5 : Uω (aρ 5) (bρ 5) (10883467580171 / 64000000000000) ≤ -(5008700887564128370101 / 2500000000000000000000)

theorem Zeta5Irrational.U_229_6 : Uω (aρ 6) (bρ 6) (10883467580171 / 64000000000000) ≤ -(21648337739633651589547 / 10000000000000000000000)

theorem Zeta5Irrational.U_229_7 : Uω (aρ 7) (bρ 7) (10883467580171 / 64000000000000) ≤ -(12510071202273143955923 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_229 : Uρ (10883467580171 / 64000000000000) ≤ -(10355263825737622949503 / 5000000000000000000000)

theorem Zeta5Irrational.U_230_1 : Uω (aρ 1) (bρ 1) (5470123807721 / 32000000000000) ≤ -(18049552413909734351791 / 10000000000000000000000)

theorem Zeta5Irrational.U_230_2 : Uω (aρ 2) (bρ 2) (5470123807721 / 32000000000000) ≤ -(727941925252781587649 / 400000000000000000000)

theorem Zeta5Irrational.U_230_3 : Uω (aρ 3) (bρ 3) (5470123807721 / 32000000000000) ≤ -(9253099115622933870931 / 5000000000000000000000)

theorem Zeta5Irrational.U_230_4 : Uω (aρ 4) (bρ 4) (5470123807721 / 32000000000000) ≤ -(952445459756741781521 / 500000000000000000000)

theorem Zeta5Irrational.U_230_5 : Uω (aρ 5) (bρ 5) (5470123807721 / 32000000000000) ≤ -(19968271182064297647983 / 10000000000000000000000)

theorem Zeta5Irrational.U_230_6 : Uω (aρ 6) (bρ 6) (5470123807721 / 32000000000000) ≤ -(10783808568520747034887 / 5000000000000000000000)

theorem Zeta5Irrational.U_230_7 : Uω (aρ 7) (bρ 7) (5470123807721 / 32000000000000) ≤ -(6221803565729163471369 / 2500000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_230 : Uρ (5470123807721 / 32000000000000) ≤ -(20680169497693025977507 / 10000000000000000000000)

theorem Zeta5Irrational.U_231_1 : Uω (aρ 1) (bρ 1) (10997027650713 / 64000000000000) ≤ -(17995755805428837382471 / 10000000000000000000000)

theorem Zeta5Irrational.U_231_2 : Uω (aρ 2) (bρ 2) (10997027650713 / 64000000000000) ≤ -(4535981881318316691607 / 2500000000000000000000)

theorem Zeta5Irrational.U_231_3 : Uω (aρ 3) (bρ 3) (10997027650713 / 64000000000000) ≤ -(2306226839652172024137 / 1250000000000000000000)

theorem Zeta5Irrational.U_231_4 : Uω (aρ 4) (bρ 4) (10997027650713 / 64000000000000) ≤ -(18989197817517969399161 / 10000000000000000000000)

theorem Zeta5Irrational.U_231_5 : Uω (aρ 5) (bρ 5) (10997027650713 / 64000000000000) ≤ -(19902191349902427008359 / 10000000000000000000000)

theorem Zeta5Irrational.U_231_6 : Uω (aρ 6) (bρ 6) (10997027650713 / 64000000000000) ≤ -(10743802233008661327371 / 5000000000000000000000)

theorem Zeta5Irrational.U_231_7 : Uω (aρ 7) (bρ 7) (10997027650713 / 64000000000000) ≤ -(12378411562319641158947 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_231 : Uρ (10997027650713 / 64000000000000) ≤ -(4130032091383163246483 / 2000000000000000000000)