Certified arcsine potential bounds (U42)

theorem Zeta5Irrational.U_508_1 : Uω (aρ 1) (bρ 1) (17856057682947 / 32000000000000) ≤ -(5950243241019627244583 / 10000000000000000000000)

theorem Zeta5Irrational.U_508_2 : Uω (aρ 2) (bρ 2) (17856057682947 / 32000000000000) ≤ -(1498432447403128669001 / 2500000000000000000000)

theorem Zeta5Irrational.U_508_3 : Uω (aρ 3) (bρ 3) (17856057682947 / 32000000000000) ≤ -(3040652460816649757537 / 5000000000000000000000)

theorem Zeta5Irrational.U_508_4 : Uω (aρ 4) (bρ 4) (17856057682947 / 32000000000000) ≤ -(3114282215668375516407 / 5000000000000000000000)

theorem Zeta5Irrational.U_508_5 : Uω (aρ 5) (bρ 5) (17856057682947 / 32000000000000) ≤ -(645730810402355959231 / 1000000000000000000000)

theorem Zeta5Irrational.U_508_6 : Uω (aρ 6) (bρ 6) (17856057682947 / 32000000000000) ≤ -(271814105316008456471 / 400000000000000000000)

theorem Zeta5Irrational.U_508_7 : Uω (aρ 7) (bρ 7) (17856057682947 / 32000000000000) ≤ -(7277132358554394793971 / 10000000000000000000000)

theorem Zeta5Irrational.U_508_8 : Uω (aρ 8) (bρ 8) (17856057682947 / 32000000000000) ≤ -(7946056761336366334497 / 10000000000000000000000)

theorem Zeta5Irrational.U_508_9 : Uω (aρ 9) (bρ 9) (17856057682947 / 32000000000000) ≤ -(1772195515441329619083 / 2000000000000000000000)

theorem Zeta5Irrational.U_508_10 : Uω (aρ 10) (bρ 10) (17856057682947 / 32000000000000) ≤ -(10114145609446987792001 / 10000000000000000000000)

theorem Zeta5Irrational.U_508_11 : Uω (aρ 11) (bρ 11) (17856057682947 / 32000000000000) ≤ -(1189203117663709979711 / 1000000000000000000000)

theorem Zeta5Irrational.U_508_12 : Uω (aρ 12) (bρ 12) (17856057682947 / 32000000000000) ≤ -(2965401357108477598221 / 2000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_508 : Uρ (17856057682947 / 32000000000000) ≤ -(9335334772364821229953 / 10000000000000000000000)

theorem Zeta5Irrational.U_509_1 : Uω (aρ 1) (bρ 1) (35792002247929 / 64000000000000) ≤ -(5927637299159037206243 / 10000000000000000000000)

theorem Zeta5Irrational.U_509_2 : Uω (aρ 2) (bρ 2) (35792002247929 / 64000000000000) ≤ -(5971024764218213295379 / 10000000000000000000000)

theorem Zeta5Irrational.U_509_3 : Uω (aρ 3) (bρ 3) (35792002247929 / 64000000000000) ≤ -(6058398365511501288333 / 10000000000000000000000)

theorem Zeta5Irrational.U_509_4 : Uω (aρ 4) (bρ 4) (35792002247929 / 64000000000000) ≤ -(620531287292092823143 / 1000000000000000000000)

theorem Zeta5Irrational.U_509_5 : Uω (aρ 5) (bρ 5) (35792002247929 / 64000000000000) ≤ -(201047027513926073651 / 312500000000000000000)

theorem Zeta5Irrational.U_509_6 : Uω (aρ 6) (bρ 6) (35792002247929 / 64000000000000) ≤ -(1692674274647282850247 / 2500000000000000000000)

theorem Zeta5Irrational.U_509_7 : Uω (aρ 7) (bρ 7) (35792002247929 / 64000000000000) ≤ -(3625589665429885931267 / 5000000000000000000000)

theorem Zeta5Irrational.U_509_8 : Uω (aρ 8) (bρ 8) (35792002247929 / 64000000000000) ≤ -(7918120550604440884439 / 10000000000000000000000)

theorem Zeta5Irrational.U_509_9 : Uω (aρ 9) (bρ 9) (35792002247929 / 64000000000000) ≤ -(220748048573075527627 / 250000000000000000000)

theorem Zeta5Irrational.U_509_10 : Uω (aρ 10) (bρ 10) (35792002247929 / 64000000000000) ≤ -(157466091658155803863 / 156250000000000000000)

theorem Zeta5Irrational.U_509_11 : Uω (aρ 11) (bρ 11) (35792002247929 / 64000000000000) ≤ -(11845313439531267758087 / 10000000000000000000000)

theorem Zeta5Irrational.U_509_12 : Uω (aρ 12) (bρ 12) (35792002247929 / 64000000000000) ≤ -(14746519519992178665709 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_509 : Uρ (35792002247929 / 64000000000000) ≤ -(1861727304759575972879 / 2000000000000000000000)

theorem Zeta5Irrational.U_510_1 : Uω (aρ 1) (bρ 1) (8967972282491 / 16000000000000) ≤ -(5905082345456817827057 / 10000000000000000000000)

theorem Zeta5Irrational.U_510_2 : Uω (aρ 2) (bρ 2) (8967972282491 / 16000000000000) ≤ -(5948371177474891842903 / 10000000000000000000000)

theorem Zeta5Irrational.U_510_3 : Uω (aρ 3) (bρ 3) (8967972282491 / 16000000000000) ≤ -(150888604337680130333 / 250000000000000000000)

theorem Zeta5Irrational.U_510_4 : Uω (aρ 4) (bρ 4) (8967972282491 / 16000000000000) ≤ -(154552882294875529027 / 250000000000000000000)

theorem Zeta5Irrational.U_510_5 : Uω (aρ 5) (bρ 5) (8967972282491 / 16000000000000) ≤ -(100152473289647147279 / 156250000000000000000)

theorem Zeta5Irrational.U_510_6 : Uω (aρ 6) (bρ 6) (8967972282491 / 16000000000000) ≤ -(843262811570624237493 / 1250000000000000000000)

theorem Zeta5Irrational.U_510_7 : Uω (aρ 7) (bρ 7) (8967972282491 / 16000000000000) ≤ -(7225294229954618860193 / 10000000000000000000000)

theorem Zeta5Irrational.U_510_8 : Uω (aρ 8) (bρ 8) (8967972282491 / 16000000000000) ≤ -(1578052819405799303733 / 2000000000000000000000)

theorem Zeta5Irrational.U_510_9 : Uω (aρ 9) (bρ 9) (8967972282491 / 16000000000000) ≤ -(2199741917220122414509 / 2500000000000000000000)

theorem Zeta5Irrational.U_510_10 : Uω (aρ 10) (bρ 10) (8967972282491 / 16000000000000) ≤ -(2510415298336719111113 / 2500000000000000000000)

theorem Zeta5Irrational.U_510_11 : Uω (aρ 11) (bρ 11) (8967972282491 / 16000000000000) ≤ -(11798874026815627584347 / 10000000000000000000000)

theorem Zeta5Irrational.U_510_12 : Uω (aρ 12) (bρ 12) (8967972282491 / 16000000000000) ≤ -(57293994566708123539 / 39062500000000000000)

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

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

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

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

theorem Zeta5Irrational.U_510 : Uρ (8967972282491 / 16000000000000) ≤ -(2320524321799194358933 / 2500000000000000000000)

theorem Zeta5Irrational.U_511_1 : Uω (aρ 1) (bρ 1) (35951776011999 / 64000000000000) ≤ -(5882578150418441128189 / 10000000000000000000000)

theorem Zeta5Irrational.U_511_2 : Uω (aρ 2) (bρ 2) (35951776011999 / 64000000000000) ≤ -(592576879682269358441 / 1000000000000000000000)

theorem Zeta5Irrational.U_511_3 : Uω (aρ 3) (bρ 3) (35951776011999 / 64000000000000) ≤ -(300637105334994580849 / 500000000000000000000)

theorem Zeta5Irrational.U_511_4 : Uω (aρ 4) (bρ 4) (35951776011999 / 64000000000000) ≤ -(6158971437747780164537 / 10000000000000000000000)

theorem Zeta5Irrational.U_511_5 : Uω (aρ 5) (bρ 5) (35951776011999 / 64000000000000) ≤ -(1277213612986815760097 / 2000000000000000000000)

theorem Zeta5Irrational.U_511_6 : Uω (aρ 6) (bρ 6) (35951776011999 / 64000000000000) ≤ -(6721568513029647007487 / 10000000000000000000000)

theorem Zeta5Irrational.U_511_7 : Uω (aρ 7) (bρ 7) (35951776011999 / 64000000000000) ≤ -(359973834867452409587 / 500000000000000000000)

theorem Zeta5Irrational.U_511_8 : Uω (aρ 8) (bρ 8) (35951776011999 / 64000000000000) ≤ -(491405433481033414363 / 625000000000000000000)

theorem Zeta5Irrational.U_511_9 : Uω (aρ 9) (bρ 9) (35951776011999 / 64000000000000) ≤ -(4384057031379989668599 / 5000000000000000000000)

theorem Zeta5Irrational.U_511_10 : Uω (aρ 10) (bρ 10) (35951776011999 / 64000000000000) ≤ -(10005638286124311866309 / 10000000000000000000000)

theorem Zeta5Irrational.U_511_11 : Uω (aρ 11) (bρ 11) (35951776011999 / 64000000000000) ≤ -(11752709006505664412089 / 10000000000000000000000)

theorem Zeta5Irrational.U_511_12 : Uω (aρ 12) (bρ 12) (35951776011999 / 64000000000000) ≤ -(3647296514749162681049 / 2500000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_511 : Uρ (35951776011999 / 64000000000000) ≤ -(9255712914413268703163 / 10000000000000000000000)

theorem Zeta5Irrational.U_512_1 : Uω (aρ 1) (bρ 1) (18015831447017 / 32000000000000) ≤ -(1465031121523832597231 / 2500000000000000000000)

theorem Zeta5Irrational.U_512_2 : Uω (aρ 2) (bρ 2) (18015831447017 / 32000000000000) ≤ -(368951086954716155551 / 625000000000000000000)

theorem Zeta5Irrational.U_512_3 : Uω (aρ 3) (bρ 3) (18015831447017 / 32000000000000) ≤ -(5989991927800893399251 / 10000000000000000000000)

theorem Zeta5Irrational.U_512_4 : Uω (aρ 4) (bρ 4) (18015831447017 / 32000000000000) ≤ -(6135881062304958525311 / 10000000000000000000000)

theorem Zeta5Irrational.U_512_5 : Uω (aρ 5) (bρ 5) (18015831447017 / 32000000000000) ≤ -(318121696809580573499 / 500000000000000000000)

theorem Zeta5Irrational.U_512_6 : Uω (aρ 6) (bρ 6) (18015831447017 / 32000000000000) ≤ -(1674273715108017435577 / 2500000000000000000000)

theorem Zeta5Irrational.U_512_7 : Uω (aρ 7) (bρ 7) (18015831447017 / 32000000000000) ≤ -(7173726377413230075053 / 10000000000000000000000)

theorem Zeta5Irrational.U_512_8 : Uω (aρ 8) (bρ 8) (18015831447017 / 32000000000000) ≤ -(1958697151459010594993 / 2500000000000000000000)

theorem Zeta5Irrational.U_512_9 : Uω (aρ 9) (bρ 9) (18015831447017 / 32000000000000) ≤ -(1747472087922510415983 / 2000000000000000000000)

theorem Zeta5Irrational.U_512_10 : Uω (aρ 10) (bρ 10) (18015831447017 / 32000000000000) ≤ -(9969759858022321014881 / 10000000000000000000000)

theorem Zeta5Irrational.U_512_11 : Uω (aρ 11) (bρ 11) (18015831447017 / 32000000000000) ≤ -(2926703634558700865789 / 2500000000000000000000)

theorem Zeta5Irrational.U_512_12 : Uω (aρ 12) (bρ 12) (18015831447017 / 32000000000000) ≤ -(1814030401212492219359 / 1250000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_512 : Uρ (18015831447017 / 32000000000000) ≤ -(461473975122939147761 / 500000000000000000000)

theorem Zeta5Irrational.U_513_1 : Uω (aρ 1) (bρ 1) (36111549776069 / 64000000000000) ≤ -(2918860563035500800487 / 5000000000000000000000)

theorem Zeta5Irrational.U_513_2 : Uω (aρ 2) (bρ 2) (36111549776069 / 64000000000000) ≤ -(2940358365703278109947 / 5000000000000000000000)

theorem Zeta5Irrational.U_513_3 : Uω (aρ 3) (bρ 3) (36111549776069 / 64000000000000) ≤ -(18647791878558030403 / 31250000000000000000)

theorem Zeta5Irrational.U_513_4 : Uω (aρ 4) (bρ 4) (36111549776069 / 64000000000000) ≤ -(1222568783742651878327 / 2000000000000000000000)

theorem Zeta5Irrational.U_513_5 : Uω (aρ 5) (bρ 5) (36111549776069 / 64000000000000) ≤ -(396178477423036181643 / 625000000000000000000)

theorem Zeta5Irrational.U_513_6 : Uω (aρ 6) (bρ 6) (36111549776069 / 64000000000000) ≤ -(133453624748920267399 / 200000000000000000000)

theorem Zeta5Irrational.U_513_7 : Uω (aρ 7) (bρ 7) (36111549776069 / 64000000000000) ≤ -(7148042917346742296531 / 10000000000000000000000)

theorem Zeta5Irrational.U_513_8 : Uω (aρ 8) (bρ 8) (36111549776069 / 64000000000000) ≤ -(1561433730153791004607 / 2000000000000000000000)

theorem Zeta5Irrational.U_513_9 : Uω (aρ 9) (bρ 9) (36111549776069 / 64000000000000) ≤ -(8706706121751562856749 / 10000000000000000000000)

theorem Zeta5Irrational.U_513_10 : Uω (aρ 10) (bρ 10) (36111549776069 / 64000000000000) ≤ -(9934024640806293113911 / 10000000000000000000000)

theorem Zeta5Irrational.U_513_11 : Uω (aρ 11) (bρ 11) (36111549776069 / 64000000000000) ≤ -(5830593435133916158567 / 5000000000000000000000)

theorem Zeta5Irrational.U_513_12 : Uω (aρ 12) (bρ 12) (36111549776069 / 64000000000000) ≤ -(288727808611259611257 / 200000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_513 : Uρ (36111549776069 / 64000000000000) ≤ -(4601696685902667401401 / 5000000000000000000000)

theorem Zeta5Irrational.U_514_1 : Uω (aρ 1) (bρ 1) (4523929582263 / 8000000000000) ≤ -(290768392272368305341 / 500000000000000000000)

theorem Zeta5Irrational.U_514_2 : Uω (aρ 2) (bρ 2) (4523929582263 / 8000000000000) ≤ -(234330663573394913113 / 400000000000000000000)

theorem Zeta5Irrational.U_514_3 : Uω (aρ 3) (bρ 3) (4523929582263 / 8000000000000) ≤ -(2972323146321819319241 / 5000000000000000000000)

theorem Zeta5Irrational.U_514_4 : Uω (aρ 4) (bρ 4) (4523929582263 / 8000000000000) ≤ -(3044929880962231886749 / 5000000000000000000000)

theorem Zeta5Irrational.U_514_5 : Uω (aρ 5) (bρ 5) (4523929582263 / 8000000000000) ≤ -(6315332909008076166521 / 10000000000000000000000)

theorem Zeta5Irrational.U_514_6 : Uω (aρ 6) (bρ 6) (4523929582263 / 8000000000000) ≤ -(6648327348947931113759 / 10000000000000000000000)

theorem Zeta5Irrational.U_514_7 : Uω (aρ 7) (bρ 7) (4523929582263 / 8000000000000) ≤ -(7122425967148344153303 / 10000000000000000000000)

theorem Zeta5Irrational.U_514_8 : Uω (aρ 8) (bρ 8) (4523929582263 / 8000000000000) ≤ -(3889813308929943655439 / 5000000000000000000000)

theorem Zeta5Irrational.U_514_9 : Uω (aρ 9) (bρ 9) (4523929582263 / 8000000000000) ≤ -(8676150438646844351813 / 10000000000000000000000)

theorem Zeta5Irrational.U_514_10 : Uω (aρ 10) (bρ 10) (4523929582263 / 8000000000000) ≤ -(395937255363209419699 / 400000000000000000000)

theorem Zeta5Irrational.U_514_11 : Uω (aρ 11) (bρ 11) (4523929582263 / 8000000000000) ≤ -(5807911168319489409469 / 5000000000000000000000)

theorem Zeta5Irrational.U_514_12 : Uω (aρ 12) (bρ 12) (4523929582263 / 8000000000000) ≤ -(179519835636495302763 / 125000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_514 : Uρ (4523929582263 / 8000000000000) ≤ -(9177451047149676338567 / 10000000000000000000000)

theorem Zeta5Irrational.U_515_1 : Uω (aρ 1) (bρ 1) (18175605211087 / 32000000000000) ≤ -(2885405315160330269137 / 5000000000000000000000)

theorem Zeta5Irrational.U_515_2 : Uω (aρ 2) (bρ 2) (18175605211087 / 32000000000000) ≤ -(1162703390940672187211 / 2000000000000000000000)

theorem Zeta5Irrational.U_515_3 : Uω (aρ 3) (bρ 3) (18175605211087 / 32000000000000) ≤ -(5899505401803822401993 / 10000000000000000000000)

theorem Zeta5Irrational.U_515_4 : Uω (aρ 4) (bρ 4) (18175605211087 / 32000000000000) ≤ -(6044049436994200835527 / 10000000000000000000000)

theorem Zeta5Irrational.U_515_5 : Uω (aρ 5) (bρ 5) (18175605211087 / 32000000000000) ≤ -(6268453107162976316631 / 10000000000000000000000)

theorem Zeta5Irrational.U_515_6 : Uω (aρ 6) (bρ 6) (18175605211087 / 32000000000000) ≤ -(6599797605804451610419 / 10000000000000000000000)

theorem Zeta5Irrational.U_515_7 : Uω (aρ 7) (bρ 7) (18175605211087 / 32000000000000) ≤ -(7071390210168205466577 / 10000000000000000000000)

theorem Zeta5Irrational.U_515_8 : Uω (aρ 8) (bρ 8) (18175605211087 / 32000000000000) ≤ -(1544954905579950569431 / 2000000000000000000000)

theorem Zeta5Irrational.U_515_9 : Uω (aρ 9) (bρ 9) (18175605211087 / 32000000000000) ≤ -(1723066465949345500237 / 2000000000000000000000)

theorem Zeta5Irrational.U_515_10 : Uω (aρ 10) (bρ 10) (18175605211087 / 32000000000000) ≤ -(2456916459404556892093 / 2500000000000000000000)

theorem Zeta5Irrational.U_515_11 : Uω (aρ 11) (bρ 11) (18175605211087 / 32000000000000) ≤ -(11525868421030432666923 / 10000000000000000000000)

theorem Zeta5Irrational.U_515_12 : Uω (aρ 12) (bρ 12) (18175605211087 / 32000000000000) ≤ -(14214976197084333418893 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_515 : Uρ (18175605211087 / 32000000000000) ≤ -(9125984834938814482263 / 10000000000000000000000)

theorem Zeta5Irrational.U_516_1 : Uω (aρ 1) (bρ 1) (9127746046561 / 16000000000000) ≤ -(572645107138737305937 / 1000000000000000000000)

theorem Zeta5Irrational.U_516_2 : Uω (aρ 2) (bρ 2) (9127746046561 / 16000000000000) ≤ -(5768966694719913615483 / 10000000000000000000000)

theorem Zeta5Irrational.U_516_3 : Uω (aρ 3) (bρ 3) (9127746046561 / 16000000000000) ≤ -(1170913482845522262301 / 2000000000000000000000)

theorem Zeta5Irrational.U_516_4 : Uω (aρ 4) (bρ 4) (9127746046561 / 16000000000000) ≤ -(5998448160638532935769 / 10000000000000000000000)

theorem Zeta5Irrational.U_516_5 : Uω (aρ 5) (bρ 5) (9127746046561 / 16000000000000) ≤ -(6221792458419681924697 / 10000000000000000000000)

theorem Zeta5Irrational.U_516_6 : Uω (aρ 6) (bρ 6) (9127746046561 / 16000000000000) ≤ -(6551503313245521501489 / 10000000000000000000000)

theorem Zeta5Irrational.U_516_7 : Uω (aρ 7) (bρ 7) (9127746046561 / 16000000000000) ≤ -(1755154090330776418639 / 2500000000000000000000)

theorem Zeta5Irrational.U_516_8 : Uω (aρ 8) (bρ 8) (9127746046561 / 16000000000000) ≤ -(7670228793910646247569 / 10000000000000000000000)

theorem Zeta5Irrational.U_516_9 : Uω (aρ 9) (bρ 9) (9127746046561 / 16000000000000) ≤ -(34219603551607253439 / 40000000000000000000)

theorem Zeta5Irrational.U_516_10 : Uω (aρ 10) (bρ 10) (9127746046561 / 16000000000000) ≤ -(9757453559173009449761 / 10000000000000000000000)

theorem Zeta5Irrational.U_516_11 : Uω (aρ 11) (bρ 11) (9127746046561 / 16000000000000) ≤ -(5718462538789883425289 / 5000000000000000000000)

theorem Zeta5Irrational.U_516_12 : Uω (aρ 12) (bρ 12) (9127746046561 / 16000000000000) ≤ -(7036065505652730763057 / 5000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_516 : Uρ (9127746046561 / 16000000000000) ≤ -(453752827101751907257 / 500000000000000000000)

theorem Zeta5Irrational.U_517_1 : Uω (aρ 1) (bρ 1) (18335378975157 / 32000000000000) ≤ -(568228742276248743139 / 1000000000000000000000)

theorem Zeta5Irrational.U_517_2 : Uω (aρ 2) (bρ 2) (18335378975157 / 32000000000000) ≤ -(2862307020290630033483 / 5000000000000000000000)

theorem Zeta5Irrational.U_517_3 : Uω (aρ 3) (bρ 3) (18335378975157 / 32000000000000) ≤ -(1161966102717595133409 / 2000000000000000000000)

theorem Zeta5Irrational.U_517_4 : Uω (aρ 4) (bρ 4) (18335378975157 / 32000000000000) ≤ -(5953054032277824673143 / 10000000000000000000000)

theorem Zeta5Irrational.U_517_5 : Uω (aρ 5) (bρ 5) (18335378975157 / 32000000000000) ≤ -(3087674459787515912569 / 5000000000000000000000)

theorem Zeta5Irrational.U_517_6 : Uω (aρ 6) (bρ 6) (18335378975157 / 32000000000000) ≤ -(1300688437478143619327 / 2000000000000000000000)

theorem Zeta5Irrational.U_517_7 : Uω (aρ 7) (bρ 7) (18335378975157 / 32000000000000) ≤ -(6970101718382483444987 / 10000000000000000000000)

theorem Zeta5Irrational.U_517_8 : Uω (aρ 8) (bρ 8) (18335378975157 / 32000000000000) ≤ -(304639437420347823563 / 400000000000000000000)

theorem Zeta5Irrational.U_517_9 : Uω (aρ 9) (bρ 9) (18335378975157 / 32000000000000) ≤ -(1698970199231094459177 / 2000000000000000000000)

theorem Zeta5Irrational.U_517_10 : Uω (aρ 10) (bρ 10) (18335378975157 / 32000000000000) ≤ -(4843892576607819671637 / 5000000000000000000000)

theorem Zeta5Irrational.U_517_11 : Uω (aρ 11) (bρ 11) (18335378975157 / 32000000000000) ≤ -(2269793160077358042791 / 2000000000000000000000)

theorem Zeta5Irrational.U_517_12 : Uω (aρ 12) (bρ 12) (18335378975157 / 32000000000000) ≤ -(13932802330277890281229 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_517 : Uρ (18335378975157 / 32000000000000) ≤ -(451232209478411826957 / 500000000000000000000)

theorem Zeta5Irrational.U_518_1 : Uω (aρ 1) (bρ 1) (2301908232149 / 4000000000000) ≤ -(704789745198935614057 / 1250000000000000000000)

theorem Zeta5Irrational.U_518_2 : Uω (aρ 2) (bρ 2) (2301908232149 / 4000000000000) ≤ -(568045724692035134871 / 1000000000000000000000)

theorem Zeta5Irrational.U_518_3 : Uω (aρ 3) (bρ 3) (2301908232149 / 4000000000000) ≤ -(5765292907843755640569 / 10000000000000000000000)

theorem Zeta5Irrational.U_518_4 : Uω (aρ 4) (bρ 4) (2301908232149 / 4000000000000) ≤ -(184620786785993711109 / 312500000000000000000)

theorem Zeta5Irrational.U_518_5 : Uω (aρ 5) (bρ 5) (2301908232149 / 4000000000000) ≤ -(1225824095183702422711 / 2000000000000000000000)

theorem Zeta5Irrational.U_518_6 : Uω (aρ 6) (bρ 6) (2301908232149 / 4000000000000) ≤ -(403475748598469510607 / 625000000000000000000)

theorem Zeta5Irrational.U_518_7 : Uω (aρ 7) (bρ 7) (2301908232149 / 4000000000000) ≤ -(6919843623735854358829 / 10000000000000000000000)

theorem Zeta5Irrational.U_518_8 : Uω (aρ 8) (bρ 8) (2301908232149 / 4000000000000) ≤ -(7562042532521178980667 / 10000000000000000000000)

theorem Zeta5Irrational.U_518_9 : Uω (aρ 9) (bρ 9) (2301908232149 / 4000000000000) ≤ -(843517764254758507903 / 1000000000000000000000)

theorem Zeta5Irrational.U_518_10 : Uω (aρ 10) (bρ 10) (2301908232149 / 4000000000000) ≤ -(9618651478160744289729 / 10000000000000000000000)

theorem Zeta5Irrational.U_518_11 : Uω (aρ 11) (bρ 11) (2301908232149 / 4000000000000) ≤ -(2252393043687111150489 / 2000000000000000000000)

theorem Zeta5Irrational.U_518_12 : Uω (aρ 12) (bρ 12) (2301908232149 / 4000000000000) ≤ -(6898383884473223033613 / 5000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_518 : Uρ (2301908232149 / 4000000000000) ≤ -(8974727806232595687023 / 10000000000000000000000)

theorem Zeta5Irrational.U_519_1 : Uω (aρ 1) (bρ 1) (18495152739227 / 32000000000000) ≤ -(2797270493823523605897 / 5000000000000000000000)

theorem Zeta5Irrational.U_519_2 : Uω (aρ 2) (bρ 2) (18495152739227 / 32000000000000) ≤ -(5636494591394130888957 / 10000000000000000000000)

theorem Zeta5Irrational.U_519_3 : Uω (aρ 3) (bρ 3) (18495152739227 / 32000000000000) ≤ -(178779775900266116243 / 312500000000000000000)

theorem Zeta5Irrational.U_519_4 : Uω (aρ 4) (bρ 4) (18495152739227 / 32000000000000) ≤ -(5862879745853656565577 / 10000000000000000000000)

theorem Zeta5Irrational.U_519_5 : Uω (aρ 5) (bρ 5) (18495152739227 / 32000000000000) ≤ -(6083105140703991195419 / 10000000000000000000000)

theorem Zeta5Irrational.U_519_6 : Uω (aρ 6) (bρ 6) (18495152739227 / 32000000000000) ≤ -(3204005232853766005531 / 5000000000000000000000)

theorem Zeta5Irrational.U_519_7 : Uω (aρ 7) (bρ 7) (18495152739227 / 32000000000000) ≤ -(214682482910002087813 / 312500000000000000000)

theorem Zeta5Irrational.U_519_8 : Uω (aρ 8) (bρ 8) (18495152739227 / 32000000000000) ≤ -(3754197611789808260037 / 5000000000000000000000)

theorem Zeta5Irrational.U_519_9 : Uω (aρ 9) (bρ 9) (18495152739227 / 32000000000000) ≤ -(1046984489645930925899 / 1250000000000000000000)

theorem Zeta5Irrational.U_519_10 : Uω (aρ 10) (bρ 10) (18495152739227 / 32000000000000) ≤ -(4775021818429599099321 / 5000000000000000000000)

theorem Zeta5Irrational.U_519_11 : Uω (aρ 11) (bρ 11) (18495152739227 / 32000000000000) ≤ -(11175899028160388580739 / 10000000000000000000000)

theorem Zeta5Irrational.U_519_12 : Uω (aρ 12) (bρ 12) (18495152739227 / 32000000000000) ≤ -(13663827683608571830467 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_519 : Uρ (18495152739227 / 32000000000000) ≤ -(1785057830144805199833 / 2000000000000000000000)