Certified arcsine potential bounds (U09)

theorem Zeta5Irrational.U_112_1 : Uω (aρ 1) (bρ 1) (4517139266921 / 64000000000000) ≤ -(5494454591738893614821 / 2000000000000000000000)

theorem Zeta5Irrational.U_112_2 : Uω (aρ 2) (bρ 2) (4517139266921 / 64000000000000) ≤ -(27873954405000162249769 / 10000000000000000000000)

theorem Zeta5Irrational.U_112_3 : Uω (aρ 3) (bρ 3) (4517139266921 / 64000000000000) ≤ -(179752256073111659559 / 62500000000000000000)

theorem Zeta5Irrational.U_112_4 : Uω (aρ 4) (bρ 4) (4517139266921 / 64000000000000) ≤ -(15294047642102670013741 / 5000000000000000000000)

theorem Zeta5Irrational.U_112_5 : Uω (aρ 5) (bρ 5) (4517139266921 / 64000000000000) ≤ -(35834287293306577019241 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_112 : Uρ (4517139266921 / 64000000000000) ≤ -(25196063800726208672673 / 10000000000000000000000)

theorem Zeta5Irrational.U_113_1 : Uω (aρ 1) (bρ 1) (2275384607621 / 32000000000000) ≤ -(27390605922888495679481 / 10000000000000000000000)

theorem Zeta5Irrational.U_113_2 : Uω (aρ 2) (bρ 2) (2275384607621 / 32000000000000) ≤ -(13894376027202381802373 / 5000000000000000000000)

theorem Zeta5Irrational.U_113_3 : Uω (aρ 3) (bρ 3) (2275384607621 / 32000000000000) ≤ -(14333238409323982707187 / 5000000000000000000000)

theorem Zeta5Irrational.U_113_4 : Uω (aρ 4) (bρ 4) (2275384607621 / 32000000000000) ≤ -(15235650232966056679897 / 5000000000000000000000)

theorem Zeta5Irrational.U_113_5 : Uω (aρ 5) (bρ 5) (2275384607621 / 32000000000000) ≤ -(17776807122822487646779 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_113 : Uρ (2275384607621 / 32000000000000) ≤ -(5032497630608943774487 / 2000000000000000000000)

theorem Zeta5Irrational.U_114_1 : Uω (aρ 1) (bρ 1) (4584399163563 / 64000000000000) ≤ -(853425029583273381449 / 312500000000000000000)

theorem Zeta5Irrational.U_114_2 : Uω (aρ 2) (bρ 2) (4584399163563 / 64000000000000) ≤ -(13852136729366462766811 / 5000000000000000000000)

theorem Zeta5Irrational.U_114_3 : Uω (aρ 3) (bρ 3) (4584399163563 / 64000000000000) ≤ -(3571685737350867667193 / 1250000000000000000000)

theorem Zeta5Irrational.U_114_4 : Uω (aρ 4) (bρ 4) (4584399163563 / 64000000000000) ≤ -(30355984291079358506601 / 10000000000000000000000)

theorem Zeta5Irrational.U_114_5 : Uω (aρ 5) (bρ 5) (4584399163563 / 64000000000000) ≤ -(8821912704169286925593 / 2500000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_114 : Uρ (4584399163563 / 64000000000000) ≤ -(25130080728420120270839 / 10000000000000000000000)

theorem Zeta5Irrational.U_115_1 : Uω (aρ 1) (bρ 1) (1154507277971 / 16000000000000) ≤ -(13614623686929618077151 / 5000000000000000000000)

theorem Zeta5Irrational.U_115_2 : Uω (aρ 2) (bρ 2) (1154507277971 / 16000000000000) ≤ -(27620506355407504983373 / 10000000000000000000000)

theorem Zeta5Irrational.U_115_3 : Uω (aρ 3) (bρ 3) (1154507277971 / 16000000000000) ≤ -(28481371009729646648441 / 10000000000000000000000)

theorem Zeta5Irrational.U_115_4 : Uω (aρ 4) (bρ 4) (1154507277971 / 16000000000000) ≤ -(15121053377842898206551 / 5000000000000000000000)

theorem Zeta5Irrational.U_115_5 : Uω (aρ 5) (bρ 5) (1154507277971 / 16000000000000) ≤ -(8758616067257419857111 / 2500000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_115 : Uρ (1154507277971 / 16000000000000) ≤ -(25098704554830257436931 / 10000000000000000000000)

theorem Zeta5Irrational.U_116_1 : Uω (aρ 1) (bρ 1) (930331812041 / 12800000000000) ≤ -(6787383700929643976333 / 2500000000000000000000)

theorem Zeta5Irrational.U_116_2 : Uω (aρ 2) (bρ 2) (930331812041 / 12800000000000) ≤ -(3442179850001808571531 / 1250000000000000000000)

theorem Zeta5Irrational.U_116_3 : Uω (aρ 3) (bρ 3) (930331812041 / 12800000000000) ≤ -(14195057725500391424769 / 5000000000000000000000)

theorem Zeta5Irrational.U_116_4 : Uω (aρ 4) (bρ 4) (930331812041 / 12800000000000) ≤ -(30129629557487540673771 / 10000000000000000000000)

theorem Zeta5Irrational.U_116_5 : Uω (aρ 5) (bρ 5) (930331812041 / 12800000000000) ≤ -(34792515104179698616019 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_116 : Uρ (930331812041 / 12800000000000) ≤ -(25068249941190760208499 / 10000000000000000000000)

theorem Zeta5Irrational.U_117_1 : Uω (aρ 1) (bρ 1) (2342644504263 / 32000000000000) ≤ -(13535226541398232719239 / 5000000000000000000000)

theorem Zeta5Irrational.U_117_2 : Uω (aρ 2) (bρ 2) (2342644504263 / 32000000000000) ≤ -(6863764786365759850067 / 2500000000000000000000)

theorem Zeta5Irrational.U_117_3 : Uω (aρ 3) (bρ 3) (2342644504263 / 32000000000000) ≤ -(14149851502271592942073 / 5000000000000000000000)

theorem Zeta5Irrational.U_117_4 : Uω (aρ 4) (bρ 4) (2342644504263 / 32000000000000) ≤ -(30018515996535756825573 / 10000000000000000000000)

theorem Zeta5Irrational.U_117_5 : Uω (aρ 5) (bρ 5) (2342644504263 / 32000000000000) ≤ -(34560553073273099210261 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_117 : Uρ (2342644504263 / 32000000000000) ≤ -(1001545091634398708323 / 400000000000000000000)

theorem Zeta5Irrational.U_118_1 : Uω (aρ 1) (bρ 1) (9404207965373 / 128000000000000) ≤ -(6757786420885346854021 / 2500000000000000000000)

theorem Zeta5Irrational.U_118_2 : Uω (aρ 2) (bρ 2) (9404207965373 / 128000000000000) ≤ -(1096564948833060777743 / 400000000000000000000)

theorem Zeta5Irrational.U_118_3 : Uω (aρ 3) (bρ 3) (9404207965373 / 128000000000000) ≤ -(110370343779415330577 / 39062500000000000000)

theorem Zeta5Irrational.U_118_4 : Uω (aρ 4) (bρ 4) (9404207965373 / 128000000000000) ≤ -(1198538381065681381673 / 400000000000000000000)

theorem Zeta5Irrational.U_118_5 : Uω (aρ 5) (bρ 5) (9404207965373 / 128000000000000) ≤ -(34447987663370110448543 / 10000000000000000000000)

theorem Zeta5Irrational.U_118_6 : Uω (aρ 6) (bρ 6) (9404207965373 / 128000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_118_7 : Uω (aρ 7) (bρ 7) (9404207965373 / 128000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_118 : Uρ (9404207965373 / 128000000000000) ≤ -(625602605153547579439 / 250000000000000000000)

theorem Zeta5Irrational.U_119_1 : Uω (aρ 1) (bρ 1) (4718918956847 / 64000000000000) ≤ -(26991992297169125119499 / 10000000000000000000000)

theorem Zeta5Irrational.U_119_2 : Uω (aρ 2) (bρ 2) (4718918956847 / 64000000000000) ≤ -(27373356034580663451179 / 10000000000000000000000)

theorem Zeta5Irrational.U_119_3 : Uω (aρ 3) (bρ 3) (4718918956847 / 64000000000000) ≤ -(28210117915897178442261 / 10000000000000000000000)

theorem Zeta5Irrational.U_119_4 : Uω (aρ 4) (bρ 4) (4718918956847 / 64000000000000) ≤ -(29908730883182997431499 / 10000000000000000000000)

theorem Zeta5Irrational.U_119_5 : Uω (aρ 5) (bρ 5) (4718918956847 / 64000000000000) ≤ -(34337546103835562865811 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_119 : Uρ (4718918956847 / 64000000000000) ≤ -(1563110136778042269237 / 625000000000000000000)

theorem Zeta5Irrational.U_120_1 : Uω (aρ 1) (bρ 1) (1894293572403 / 25600000000000) ≤ -(26952991720637376599691 / 10000000000000000000000)

theorem Zeta5Irrational.U_120_2 : Uω (aρ 2) (bρ 2) (1894293572403 / 25600000000000) ≤ -(13666377355402748850127 / 5000000000000000000000)

theorem Zeta5Irrational.U_120_3 : Uω (aρ 3) (bρ 3) (1894293572403 / 25600000000000) ≤ -(28165630829855142778867 / 10000000000000000000000)

theorem Zeta5Irrational.U_120_4 : Uω (aρ 4) (bρ 4) (1894293572403 / 25600000000000) ≤ -(5970865177888741761793 / 2000000000000000000000)

theorem Zeta5Irrational.U_120_5 : Uω (aρ 5) (bρ 5) (1894293572403 / 25600000000000) ≤ -(3422912528271636769997 / 1000000000000000000000)

theorem Zeta5Irrational.U_120_6 : Uω (aρ 6) (bρ 6) (1894293572403 / 25600000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_120_7 : Uω (aρ 7) (bρ 7) (1894293572403 / 25600000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_120_8 : Uω (aρ 8) (bρ 8) (1894293572403 / 25600000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_120_9 : Uω (aρ 9) (bρ 9) (1894293572403 / 25600000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_120_10 : Uω (aρ 10) (bρ 10) (1894293572403 / 25600000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_120_11 : Uω (aρ 11) (bρ 11) (1894293572403 / 25600000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_120_12 : Uω (aρ 12) (bρ 12) (1894293572403 / 25600000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_120_13 : Uω (aρ 13) (bρ 13) (1894293572403 / 25600000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_120_14 : Uω (aρ 14) (bρ 14) (1894293572403 / 25600000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_120_15 : Uω (aρ 15) (bρ 15) (1894293572403 / 25600000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_120_16 : Uω (aρ 16) (bρ 16) (1894293572403 / 25600000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_120 : Uρ (1894293572403 / 25600000000000) ≤ -(24995593741306154908533 / 10000000000000000000000)

theorem Zeta5Irrational.U_121_1 : Uω (aρ 1) (bρ 1) (297034306573 / 4000000000000) ≤ -(6728535691238731355147 / 2500000000000000000000)

theorem Zeta5Irrational.U_121_2 : Uω (aρ 2) (bρ 2) (297034306573 / 4000000000000) ≤ -(3411539798815513981353 / 1250000000000000000000)

theorem Zeta5Irrational.U_121_3 : Uω (aρ 3) (bρ 3) (297034306573 / 4000000000000) ≤ -(7030336219103306552713 / 2500000000000000000000)

theorem Zeta5Irrational.U_121_4 : Uω (aρ 4) (bρ 4) (297034306573 / 4000000000000) ≤ -(3725030056597356522343 / 1250000000000000000000)

theorem Zeta5Irrational.U_121_5 : Uω (aρ 5) (bρ 5) (297034306573 / 4000000000000) ≤ -(682452605272557036629 / 200000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_121 : Uρ (297034306573 / 4000000000000) ≤ -(24981591939352846305661 / 10000000000000000000000)

theorem Zeta5Irrational.U_122_1 : Uω (aρ 1) (bρ 1) (9538727758657 / 128000000000000) ≤ -(26875444254963523057139 / 10000000000000000000000)

theorem Zeta5Irrational.U_122_2 : Uω (aρ 2) (bρ 2) (9538727758657 / 128000000000000) ≤ -(27252045731424229280841 / 10000000000000000000000)

theorem Zeta5Irrational.U_122_3 : Uω (aρ 3) (bρ 3) (9538727758657 / 128000000000000) ≤ -(28077258208867713837771 / 10000000000000000000000)

theorem Zeta5Irrational.U_122_4 : Uω (aρ 4) (bρ 4) (9538727758657 / 128000000000000) ≤ -(14873235281136487034493 / 5000000000000000000000)

theorem Zeta5Irrational.U_122_5 : Uω (aρ 5) (bρ 5) (9538727758657 / 128000000000000) ≤ -(6803594680306818344917 / 2000000000000000000000)

theorem Zeta5Irrational.U_122_6 : Uω (aρ 6) (bρ 6) (9538727758657 / 128000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_122_7 : Uω (aρ 7) (bρ 7) (9538727758657 / 128000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_122 : Uρ (9538727758657 / 128000000000000) ≤ -(6241937591781720172913 / 2500000000000000000000)

theorem Zeta5Irrational.U_123_1 : Uω (aρ 1) (bρ 1) (4786178853489 / 64000000000000) ≤ -(5367379005824790420369 / 2000000000000000000000)

theorem Zeta5Irrational.U_123_2 : Uω (aρ 2) (bρ 2) (4786178853489 / 64000000000000) ≤ -(27211935407585621453431 / 10000000000000000000000)

theorem Zeta5Irrational.U_123_3 : Uω (aρ 3) (bρ 3) (4786178853489 / 64000000000000) ≤ -(14016684503152133467349 / 5000000000000000000000)

theorem Zeta5Irrational.U_123_4 : Uω (aρ 4) (bρ 4) (4786178853489 / 64000000000000) ≤ -(29693012286484085391417 / 10000000000000000000000)

theorem Zeta5Irrational.U_123_5 : Uω (aρ 5) (bρ 5) (4786178853489 / 64000000000000) ≤ -(16957536789013437420659 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_123 : Uρ (4786178853489 / 64000000000000) ≤ -(311925788326356217817 / 125000000000000000000)