Certified arcsine potential bounds (U07)

theorem Zeta5Irrational.U_88_1 : Uω (aρ 1) (bρ 1) (3041335677499 / 64000000000000) ≤ -(31934091820714900994499 / 10000000000000000000000)

theorem Zeta5Irrational.U_88_2 : Uω (aρ 2) (bρ 2) (3041335677499 / 64000000000000) ≤ -(254627088457477178169 / 78125000000000000000)

theorem Zeta5Irrational.U_88_3 : Uω (aρ 3) (bρ 3) (3041335677499 / 64000000000000) ≤ -(34164784516352722640813 / 10000000000000000000000)

theorem Zeta5Irrational.U_88_4 : Uω (aρ 4) (bρ 4) (3041335677499 / 64000000000000) ≤ -(1928027625307929110733 / 500000000000000000000)

theorem Zeta5Irrational.U_88_5 : Uω (aρ 5) (bρ 5) (3041335677499 / 64000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_88_6 : Uω (aρ 6) (bρ 6) (3041335677499 / 64000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_88 : Uρ (3041335677499 / 64000000000000) ≤ -(826419256172916514983 / 312500000000000000000)

theorem Zeta5Irrational.U_89_1 : Uω (aρ 1) (bρ 1) (191579824301 / 4000000000000) ≤ -(796081223438251080513 / 250000000000000000000)

theorem Zeta5Irrational.U_89_2 : Uω (aρ 2) (bρ 2) (191579824301 / 4000000000000) ≤ -(6498934924237707349841 / 2000000000000000000000)

theorem Zeta5Irrational.U_89_3 : Uω (aρ 3) (bρ 3) (191579824301 / 4000000000000) ≤ -(17023759633831421878791 / 5000000000000000000000)

theorem Zeta5Irrational.U_89_4 : Uω (aρ 4) (bρ 4) (191579824301 / 4000000000000) ≤ -(19166747049474907076563 / 5000000000000000000000)

theorem Zeta5Irrational.U_89_5 : Uω (aρ 5) (bρ 5) (191579824301 / 4000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_89_6 : Uω (aρ 6) (bρ 6) (191579824301 / 4000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_89_7 : Uω (aρ 7) (bρ 7) (191579824301 / 4000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_89_8 : Uω (aρ 8) (bρ 8) (191579824301 / 4000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_89_9 : Uω (aρ 9) (bρ 9) (191579824301 / 4000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_89_10 : Uω (aρ 10) (bρ 10) (191579824301 / 4000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_89_11 : Uω (aρ 11) (bρ 11) (191579824301 / 4000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_89_12 : Uω (aρ 12) (bρ 12) (191579824301 / 4000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_89_13 : Uω (aρ 13) (bρ 13) (191579824301 / 4000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_89_14 : Uω (aρ 14) (bρ 14) (191579824301 / 4000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_89_15 : Uω (aρ 15) (bρ 15) (191579824301 / 4000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_89_16 : Uω (aρ 16) (bρ 16) (191579824301 / 4000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_89 : Uρ (191579824301 / 4000000000000) ≤ -(26423334234748999464827 / 10000000000000000000000)

theorem Zeta5Irrational.U_90_1 : Uω (aρ 1) (bρ 1) (3089218700133 / 64000000000000) ≤ -(31753225403554109637937 / 10000000000000000000000)

theorem Zeta5Irrational.U_90_2 : Uω (aρ 2) (bρ 2) (3089218700133 / 64000000000000) ≤ -(16199019208965554918851 / 5000000000000000000000)

theorem Zeta5Irrational.U_90_3 : Uω (aρ 3) (bρ 3) (3089218700133 / 64000000000000) ≤ -(6786341272376926062427 / 2000000000000000000000)

theorem Zeta5Irrational.U_90_4 : Uω (aρ 4) (bρ 4) (3089218700133 / 64000000000000) ≤ -(9528575281149508014001 / 2500000000000000000000)

theorem Zeta5Irrational.U_90_5 : Uω (aρ 5) (bρ 5) (3089218700133 / 64000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_90_6 : Uω (aρ 6) (bρ 6) (3089218700133 / 64000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_90 : Uρ (3089218700133 / 64000000000000) ≤ -(13200904617235475791283 / 5000000000000000000000)

theorem Zeta5Irrational.U_91_1 : Uω (aρ 1) (bρ 1) (62263204229 / 1280000000000) ≤ -(1583200327193589922537 / 500000000000000000000)

theorem Zeta5Irrational.U_91_2 : Uω (aρ 2) (bρ 2) (62263204229 / 1280000000000) ≤ -(16151169947406386751941 / 5000000000000000000000)

theorem Zeta5Irrational.U_91_3 : Uω (aρ 3) (bρ 3) (62263204229 / 1280000000000) ≤ -(1056790878554544750231 / 312500000000000000000)

theorem Zeta5Irrational.U_91_4 : Uω (aρ 4) (bρ 4) (62263204229 / 1280000000000) ≤ -(37902304216173367332429 / 10000000000000000000000)

theorem Zeta5Irrational.U_91_5 : Uω (aρ 5) (bρ 5) (62263204229 / 1280000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_91_6 : Uω (aρ 6) (bρ 6) (62263204229 / 1280000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_91_7 : Uω (aρ 7) (bρ 7) (62263204229 / 1280000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_91_8 : Uω (aρ 8) (bρ 8) (62263204229 / 1280000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_91_9 : Uω (aρ 9) (bρ 9) (62263204229 / 1280000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_91_10 : Uω (aρ 10) (bρ 10) (62263204229 / 1280000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_91_11 : Uω (aρ 11) (bρ 11) (62263204229 / 1280000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_91_12 : Uω (aρ 12) (bρ 12) (62263204229 / 1280000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_91_13 : Uω (aρ 13) (bρ 13) (62263204229 / 1280000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_91_14 : Uω (aρ 14) (bρ 14) (62263204229 / 1280000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_91_15 : Uω (aρ 15) (bρ 15) (62263204229 / 1280000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_91_16 : Uω (aρ 16) (bρ 16) (62263204229 / 1280000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_91 : Uρ (62263204229 / 1280000000000) ≤ -(412199998590688327739 / 156250000000000000000)

theorem Zeta5Irrational.U_92_1 : Uω (aρ 1) (bρ 1) (3137101722767 / 64000000000000) ≤ -(31575578075022150256599 / 10000000000000000000000)

theorem Zeta5Irrational.U_92_2 : Uω (aρ 2) (bρ 2) (3137101722767 / 64000000000000) ≤ -(16103780395389085637527 / 5000000000000000000000)

theorem Zeta5Irrational.U_92_3 : Uω (aρ 3) (bρ 3) (3137101722767 / 64000000000000) ≤ -(33704288357139015076803 / 10000000000000000000000)

theorem Zeta5Irrational.U_92_4 : Uω (aρ 4) (bρ 4) (3137101722767 / 64000000000000) ≤ -(18848462387150699761219 / 5000000000000000000000)

theorem Zeta5Irrational.U_92_5 : Uω (aρ 5) (bρ 5) (3137101722767 / 64000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_92_6 : Uω (aρ 6) (bρ 6) (3137101722767 / 64000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_92 : Uρ (3137101722767 / 64000000000000) ≤ -(13180135171331573725517 / 5000000000000000000000)

theorem Zeta5Irrational.U_93_1 : Uω (aρ 1) (bρ 1) (790260808521 / 16000000000000) ≤ -(31487926091174342905069 / 10000000000000000000000)

theorem Zeta5Irrational.U_93_2 : Uω (aρ 2) (bρ 2) (790260808521 / 16000000000000) ≤ -(32113683379671497832899 / 10000000000000000000000)

theorem Zeta5Irrational.U_93_3 : Uω (aρ 3) (bρ 3) (790260808521 / 16000000000000) ≤ -(1679630618076205600743 / 500000000000000000000)

theorem Zeta5Irrational.U_93_4 : Uω (aρ 4) (bρ 4) (790260808521 / 16000000000000) ≤ -(18748829261004226629189 / 5000000000000000000000)

theorem Zeta5Irrational.U_93_5 : Uω (aρ 5) (bρ 5) (790260808521 / 16000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_93_6 : Uω (aρ 6) (bρ 6) (790260808521 / 16000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_93 : Uρ (790260808521 / 16000000000000) ≤ -(26340189022211827785901 / 10000000000000000000000)

theorem Zeta5Irrational.U_94_1 : Uω (aρ 1) (bρ 1) (3184984745401 / 64000000000000) ≤ -(15700518525454701202457 / 5000000000000000000000)

theorem Zeta5Irrational.U_94_2 : Uω (aρ 2) (bρ 2) (3184984745401 / 64000000000000) ≤ -(32020690449308287470393 / 10000000000000000000000)

theorem Zeta5Irrational.U_94_3 : Uω (aρ 3) (bρ 3) (3184984745401 / 64000000000000) ≤ -(6696449350830705340347 / 2000000000000000000000)

theorem Zeta5Irrational.U_94_4 : Uω (aρ 4) (bρ 4) (3184984745401 / 64000000000000) ≤ -(37304062711062346239319 / 10000000000000000000000)

theorem Zeta5Irrational.U_94_5 : Uω (aρ 5) (bρ 5) (3184984745401 / 64000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_94_6 : Uω (aρ 6) (bρ 6) (3184984745401 / 64000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_94 : Uρ (3184984745401 / 64000000000000) ≤ -(6580132024030622994311 / 2500000000000000000000)

theorem Zeta5Irrational.U_95_1 : Uω (aρ 1) (bρ 1) (1604463128359 / 32000000000000) ≤ -(31314897764576203369223 / 10000000000000000000000)

theorem Zeta5Irrational.U_95_2 : Uω (aρ 2) (bρ 2) (1604463128359 / 32000000000000) ≤ -(1995535330098219433187 / 625000000000000000000)

theorem Zeta5Irrational.U_95_3 : Uω (aρ 3) (bρ 3) (1604463128359 / 32000000000000) ≤ -(33373159447642545139733 / 10000000000000000000000)

theorem Zeta5Irrational.U_95_4 : Uω (aρ 4) (bρ 4) (1604463128359 / 32000000000000) ≤ -(37115746034298764438831 / 10000000000000000000000)

theorem Zeta5Irrational.U_95_5 : Uω (aρ 5) (bρ 5) (1604463128359 / 32000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_95_6 : Uω (aρ 6) (bρ 6) (1604463128359 / 32000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_95 : Uρ (1604463128359 / 32000000000000) ≤ -(1643828923725105092647 / 625000000000000000000)

theorem Zeta5Irrational.U_96_1 : Uω (aρ 1) (bρ 1) (646573553607 / 12800000000000) ≤ -(31229495382192123462893 / 10000000000000000000000)

theorem Zeta5Irrational.U_96_2 : Uω (aρ 2) (bρ 2) (646573553607 / 12800000000000) ≤ -(31837291633471834828943 / 10000000000000000000000)

theorem Zeta5Irrational.U_96_3 : Uω (aρ 3) (bρ 3) (646573553607 / 12800000000000) ≤ -(33265319572434076398587 / 10000000000000000000000)

theorem Zeta5Irrational.U_96_4 : Uω (aρ 4) (bρ 4) (646573553607 / 12800000000000) ≤ -(18466180287477100611297 / 5000000000000000000000)

theorem Zeta5Irrational.U_96_5 : Uω (aρ 5) (bρ 5) (646573553607 / 12800000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_96_6 : Uω (aρ 6) (bρ 6) (646573553607 / 12800000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_96 : Uρ (646573553607 / 12800000000000) ≤ -(328529636040277536627 / 125000000000000000000)

theorem Zeta5Irrational.U_97_1 : Uω (aρ 1) (bρ 1) (407101159919 / 8000000000000) ≤ -(31144817381860143498661 / 10000000000000000000000)

theorem Zeta5Irrational.U_97_2 : Uω (aρ 2) (bρ 2) (407101159919 / 8000000000000) ≤ -(1984178357444751687497 / 625000000000000000000)

theorem Zeta5Irrational.U_97_3 : Uω (aρ 3) (bρ 3) (407101159919 / 8000000000000) ≤ -(3315869741376076852277 / 1000000000000000000000)

theorem Zeta5Irrational.U_97_4 : Uω (aρ 4) (bρ 4) (407101159919 / 8000000000000) ≤ -(36753595311212100745499 / 10000000000000000000000)

theorem Zeta5Irrational.U_97_5 : Uω (aρ 5) (bρ 5) (407101159919 / 8000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_97_6 : Uω (aρ 6) (bρ 6) (407101159919 / 8000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_97 : Uρ (407101159919 / 8000000000000) ≤ -(26263832431500510068899 / 10000000000000000000000)

theorem Zeta5Irrational.U_98_1 : Uω (aρ 1) (bρ 1) (1652346150993 / 32000000000000) ≤ -(15488793007051782660579 / 5000000000000000000000)

theorem Zeta5Irrational.U_98_2 : Uω (aρ 2) (bρ 2) (1652346150993 / 32000000000000) ≤ -(789210603282412178031 / 250000000000000000000)

theorem Zeta5Irrational.U_98_3 : Uω (aρ 3) (bρ 3) (1652346150993 / 32000000000000) ≤ -(32948992811289585472047 / 10000000000000000000000)

theorem Zeta5Irrational.U_98_4 : Uω (aρ 4) (bρ 4) (1652346150993 / 32000000000000) ≤ -(9102208735492745651249 / 2500000000000000000000)

theorem Zeta5Irrational.U_98_5 : Uω (aρ 5) (bρ 5) (1652346150993 / 32000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_98_6 : Uω (aρ 6) (bρ 6) (1652346150993 / 32000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_98 : Uρ (1652346150993 / 32000000000000) ≤ -(26227745217472389991977 / 10000000000000000000000)

theorem Zeta5Irrational.U_99_1 : Uω (aρ 1) (bρ 1) (167628766231 / 3200000000000) ≤ -(30813109637784336635283 / 10000000000000000000000)

theorem Zeta5Irrational.U_99_2 : Uω (aρ 2) (bρ 2) (167628766231 / 3200000000000) ≤ -(31393158740030300939493 / 10000000000000000000000)

theorem Zeta5Irrational.U_99_3 : Uω (aρ 3) (bρ 3) (167628766231 / 3200000000000) ≤ -(8185957218103774495557 / 2500000000000000000000)

theorem Zeta5Irrational.U_99_4 : Uω (aρ 4) (bρ 4) (167628766231 / 3200000000000) ≤ -(9019883879209497377887 / 2500000000000000000000)

theorem Zeta5Irrational.U_99_5 : Uω (aρ 5) (bρ 5) (167628766231 / 3200000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_99_6 : Uω (aρ 6) (bρ 6) (167628766231 / 3200000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_99_7 : Uω (aρ 7) (bρ 7) (167628766231 / 3200000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_99_8 : Uω (aρ 8) (bρ 8) (167628766231 / 3200000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_99_9 : Uω (aρ 9) (bρ 9) (167628766231 / 3200000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_99_10 : Uω (aρ 10) (bρ 10) (167628766231 / 3200000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_99_11 : Uω (aρ 11) (bρ 11) (167628766231 / 3200000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_99_12 : Uω (aρ 12) (bρ 12) (167628766231 / 3200000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_99_13 : Uω (aρ 13) (bρ 13) (167628766231 / 3200000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_99_14 : Uω (aρ 14) (bρ 14) (167628766231 / 3200000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_99_15 : Uω (aρ 15) (bρ 15) (167628766231 / 3200000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_99_16 : Uω (aρ 16) (bρ 16) (167628766231 / 3200000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_99 : Uρ (167628766231 / 3200000000000) ≤ -(3274109383884848166437 / 1250000000000000000000)