Certified arcsine potential bounds (U23)

theorem Zeta5Irrational.U_280_1 : Uω (aρ 1) (bρ 1) (7424867802851 / 32000000000000) ≤ -(595649490681648873547 / 400000000000000000000)

theorem Zeta5Irrational.U_280_2 : Uω (aρ 2) (bρ 2) (7424867802851 / 32000000000000) ≤ -(14998978531214893129037 / 10000000000000000000000)

theorem Zeta5Irrational.U_280_3 : Uω (aρ 3) (bρ 3) (7424867802851 / 32000000000000) ≤ -(3804810672586354525097 / 2500000000000000000000)

theorem Zeta5Irrational.U_280_4 : Uω (aρ 4) (bρ 4) (7424867802851 / 32000000000000) ≤ -(15600250780916396574767 / 10000000000000000000000)

theorem Zeta5Irrational.U_280_5 : Uω (aρ 5) (bρ 5) (7424867802851 / 32000000000000) ≤ -(16221992242274015104961 / 10000000000000000000000)

theorem Zeta5Irrational.U_280_6 : Uω (aρ 6) (bρ 6) (7424867802851 / 32000000000000) ≤ -(17223054302843945077151 / 10000000000000000000000)

theorem Zeta5Irrational.U_280_7 : Uω (aρ 7) (bρ 7) (7424867802851 / 32000000000000) ≤ -(3779062541338344784579 / 2000000000000000000000)

theorem Zeta5Irrational.U_280_8 : Uω (aρ 8) (bρ 8) (7424867802851 / 32000000000000) ≤ -(11127371186098035850237 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_280 : Uρ (7424867802851 / 32000000000000) ≤ -(18424120970672703313979 / 10000000000000000000000)

theorem Zeta5Irrational.U_281_1 : Uω (aρ 1) (bρ 1) (3729493959969 / 16000000000000) ≤ -(14844077893084188706087 / 10000000000000000000000)

theorem Zeta5Irrational.U_281_2 : Uω (aρ 2) (bρ 2) (3729493959969 / 16000000000000) ≤ -(7475650471701528025081 / 5000000000000000000000)

theorem Zeta5Irrational.U_281_3 : Uω (aρ 3) (bρ 3) (3729493959969 / 16000000000000) ≤ -(15170478598639876278171 / 10000000000000000000000)

theorem Zeta5Irrational.U_281_4 : Uω (aρ 4) (bρ 4) (3729493959969 / 16000000000000) ≤ -(3109903348603568808439 / 2000000000000000000000)

theorem Zeta5Irrational.U_281_5 : Uω (aρ 5) (bρ 5) (3729493959969 / 16000000000000) ≤ -(16167772839817462190979 / 10000000000000000000000)

theorem Zeta5Irrational.U_281_6 : Uω (aρ 6) (bρ 6) (3729493959969 / 16000000000000) ≤ -(858119665204360662129 / 500000000000000000000)

theorem Zeta5Irrational.U_281_7 : Uω (aρ 7) (bρ 7) (3729493959969 / 16000000000000) ≤ -(3764166476338037308167 / 2000000000000000000000)

theorem Zeta5Irrational.U_281_8 : Uω (aρ 8) (bρ 8) (3729493959969 / 16000000000000) ≤ -(885200539449577683937 / 400000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_281 : Uρ (3729493959969 / 16000000000000) ≤ -(18391299973504200398809 / 10000000000000000000000)

theorem Zeta5Irrational.U_282_1 : Uω (aρ 1) (bρ 1) (299724321481 / 1280000000000) ≤ -(1849642486269237145517 / 1250000000000000000000)

theorem Zeta5Irrational.U_282_2 : Uω (aρ 2) (bρ 2) (299724321481 / 1280000000000) ≤ -(14903849687665541604669 / 10000000000000000000000)

theorem Zeta5Irrational.U_282_3 : Uω (aρ 3) (bρ 3) (299724321481 / 1280000000000) ≤ -(3024390301891908800277 / 2000000000000000000000)

theorem Zeta5Irrational.U_282_4 : Uω (aρ 4) (bρ 4) (299724321481 / 1280000000000) ≤ -(193738000068022755659 / 125000000000000000000)

theorem Zeta5Irrational.U_282_5 : Uω (aρ 5) (bρ 5) (299724321481 / 1280000000000) ≤ -(402846244571714183917 / 250000000000000000000)

theorem Zeta5Irrational.U_282_6 : Uω (aρ 6) (bρ 6) (299724321481 / 1280000000000) ≤ -(17102112138147452632809 / 10000000000000000000000)

theorem Zeta5Irrational.U_282_7 : Uω (aρ 7) (bρ 7) (299724321481 / 1280000000000) ≤ -(1171685462072131543447 / 625000000000000000000)

theorem Zeta5Irrational.U_282_8 : Uω (aρ 8) (bρ 8) (299724321481 / 1280000000000) ≤ -(11003813586334001811501 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_282 : Uρ (299724321481 / 1280000000000) ≤ -(18358822832970896564511 / 10000000000000000000000)

theorem Zeta5Irrational.U_283_1 : Uω (aρ 1) (bρ 1) (29403234977 / 125000000000) ≤ -(14750421189550824741283 / 10000000000000000000000)

theorem Zeta5Irrational.U_283_2 : Uω (aρ 2) (bρ 2) (29403234977 / 125000000000) ≤ -(7428311312201253933377 / 5000000000000000000000)

theorem Zeta5Irrational.U_283_3 : Uω (aρ 3) (bρ 3) (29403234977 / 125000000000) ≤ -(7536829563360700704481 / 5000000000000000000000)

theorem Zeta5Irrational.U_283_4 : Uω (aρ 4) (bρ 4) (29403234977 / 125000000000) ≤ -(1931102244940006175991 / 1250000000000000000000)

theorem Zeta5Irrational.U_283_5 : Uω (aρ 5) (bρ 5) (29403234977 / 125000000000) ≤ -(16060219807321465949653 / 10000000000000000000000)

theorem Zeta5Irrational.U_283_6 : Uω (aρ 6) (bρ 6) (29403234977 / 125000000000) ≤ -(8521102954091416726939 / 5000000000000000000000)

theorem Zeta5Irrational.U_283_7 : Uω (aρ 7) (bρ 7) (29403234977 / 125000000000) ≤ -(18673706669854913901521 / 10000000000000000000000)

theorem Zeta5Irrational.U_283_8 : Uω (aρ 8) (bρ 8) (29403234977 / 125000000000) ≤ -(21887473556177965593987 / 10000000000000000000000)

theorem Zeta5Irrational.U_283_9 : Uω (aρ 9) (bρ 9) (29403234977 / 125000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_283_10 : Uω (aρ 10) (bρ 10) (29403234977 / 125000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_283_11 : Uω (aρ 11) (bρ 11) (29403234977 / 125000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_283_12 : Uω (aρ 12) (bρ 12) (29403234977 / 125000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_283_13 : Uω (aρ 13) (bρ 13) (29403234977 / 125000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_283_14 : Uω (aρ 14) (bρ 14) (29403234977 / 125000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_283_15 : Uω (aρ 15) (bρ 15) (29403234977 / 125000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_283_16 : Uω (aρ 16) (bρ 16) (29403234977 / 125000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_283 : Uρ (29403234977 / 125000000000) ≤ -(3665335590052395257373 / 2000000000000000000000)

theorem Zeta5Irrational.U_284_1 : Uω (aρ 1) (bρ 1) (7561348271199 / 32000000000000) ≤ -(2940783950288045734059 / 2000000000000000000000)

theorem Zeta5Irrational.U_284_2 : Uω (aρ 2) (bρ 2) (7561348271199 / 32000000000000) ≤ -(7404808822111749557067 / 5000000000000000000000)

theorem Zeta5Irrational.U_284_3 : Uω (aρ 3) (bρ 3) (7561348271199 / 32000000000000) ≤ -(15025599187597887615541 / 10000000000000000000000)

theorem Zeta5Irrational.U_284_4 : Uω (aρ 4) (bρ 4) (7561348271199 / 32000000000000) ≤ -(15398848036234854074413 / 10000000000000000000000)

theorem Zeta5Irrational.U_284_5 : Uω (aρ 5) (bρ 5) (7561348271199 / 32000000000000) ≤ -(3201375940674537947543 / 2000000000000000000000)

theorem Zeta5Irrational.U_284_6 : Uω (aρ 6) (bρ 6) (7561348271199 / 32000000000000) ≤ -(16982669814435490042889 / 10000000000000000000000)

theorem Zeta5Irrational.U_284_7 : Uω (aρ 7) (bρ 7) (7561348271199 / 32000000000000) ≤ -(18601039457942155663267 / 10000000000000000000000)

theorem Zeta5Irrational.U_284_8 : Uω (aρ 8) (bρ 8) (7561348271199 / 32000000000000) ≤ -(5442362793886692937687 / 2500000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_284 : Uρ (7561348271199 / 32000000000000) ≤ -(9147427256802812168183 / 5000000000000000000000)

theorem Zeta5Irrational.U_285_1 : Uω (aρ 1) (bρ 1) (3797734194143 / 16000000000000) ≤ -(3664408391079400055809 / 2500000000000000000000)

theorem Zeta5Irrational.U_285_2 : Uω (aρ 2) (bρ 2) (3797734194143 / 16000000000000) ≤ -(461338520855661178501 / 312500000000000000000)

theorem Zeta5Irrational.U_285_3 : Uω (aρ 3) (bρ 3) (3797734194143 / 16000000000000) ≤ -(14977769461876843290263 / 10000000000000000000000)

theorem Zeta5Irrational.U_285_4 : Uω (aρ 4) (bρ 4) (3797734194143 / 16000000000000) ≤ -(7674563852708070316761 / 5000000000000000000000)

theorem Zeta5Irrational.U_285_5 : Uω (aρ 5) (bρ 5) (3797734194143 / 16000000000000) ≤ -(3190765262861868759431 / 2000000000000000000000)

theorem Zeta5Irrational.U_285_6 : Uω (aρ 6) (bρ 6) (3797734194143 / 16000000000000) ≤ -(8461749575806555752881 / 5000000000000000000000)

theorem Zeta5Irrational.U_285_7 : Uω (aρ 7) (bρ 7) (3797734194143 / 16000000000000) ≤ -(18528955308340390514393 / 10000000000000000000000)

theorem Zeta5Irrational.U_285_8 : Uω (aρ 8) (bρ 8) (3797734194143 / 16000000000000) ≤ -(21653466102551587295531 / 10000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_285 : Uρ (3797734194143 / 16000000000000) ≤ -(18263342418928709501953 / 10000000000000000000000)

theorem Zeta5Irrational.U_286_1 : Uω (aρ 1) (bρ 1) (383185431123 / 1600000000000) ≤ -(728284951777396434499 / 500000000000000000000)

theorem Zeta5Irrational.U_286_2 : Uω (aρ 2) (bρ 2) (383185431123 / 1600000000000) ≤ -(14669914549627046428131 / 10000000000000000000000)

theorem Zeta5Irrational.U_286_3 : Uω (aρ 3) (bρ 3) (383185431123 / 1600000000000) ≤ -(1488279188913710560159 / 1000000000000000000000)

theorem Zeta5Irrational.U_286_4 : Uω (aρ 4) (bρ 4) (383185431123 / 1600000000000) ≤ -(7625212945029603857267 / 5000000000000000000000)

theorem Zeta5Irrational.U_286_5 : Uω (aρ 5) (bρ 5) (383185431123 / 1600000000000) ≤ -(1981070914050747589499 / 1250000000000000000000)

theorem Zeta5Irrational.U_286_6 : Uω (aρ 6) (bρ 6) (383185431123 / 1600000000000) ≤ -(16806235754814884325851 / 10000000000000000000000)

theorem Zeta5Irrational.U_286_7 : Uω (aρ 7) (bρ 7) (383185431123 / 1600000000000) ≤ -(18386495852461762688133 / 10000000000000000000000)

theorem Zeta5Irrational.U_286_8 : Uω (aρ 8) (bρ 8) (383185431123 / 1600000000000) ≤ -(2678408166937960326061 / 1250000000000000000000)

theorem Zeta5Irrational.U_286_9 : Uω (aρ 9) (bρ 9) (383185431123 / 1600000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_286_10 : Uω (aρ 10) (bρ 10) (383185431123 / 1600000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_286_11 : Uω (aρ 11) (bρ 11) (383185431123 / 1600000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_286_12 : Uω (aρ 12) (bρ 12) (383185431123 / 1600000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_286_13 : Uω (aρ 13) (bρ 13) (383185431123 / 1600000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_286_14 : Uω (aρ 14) (bρ 14) (383185431123 / 1600000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_286_15 : Uω (aρ 15) (bρ 15) (383185431123 / 1600000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_286_16 : Uω (aρ 16) (bρ 16) (383185431123 / 1600000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_286 : Uρ (383185431123 / 1600000000000) ≤ -(3640242994400076007859 / 2000000000000000000000)

theorem Zeta5Irrational.U_287_1 : Uω (aρ 1) (bρ 1) (3865974428317 / 16000000000000) ≤ -(7237301029131155242153 / 5000000000000000000000)

theorem Zeta5Irrational.U_287_2 : Uω (aρ 2) (bρ 2) (3865974428317 / 16000000000000) ≤ -(3644463051331309478819 / 2500000000000000000000)

theorem Zeta5Irrational.U_287_3 : Uω (aρ 3) (bρ 3) (3865974428317 / 16000000000000) ≤ -(2957741839148582854709 / 2000000000000000000000)

theorem Zeta5Irrational.U_287_4 : Uω (aρ 4) (bρ 4) (3865974428317 / 16000000000000) ≤ -(378817325494630744883 / 250000000000000000000)

theorem Zeta5Irrational.U_287_5 : Uω (aρ 5) (bρ 5) (3865974428317 / 16000000000000) ≤ -(3936104641443346695053 / 2500000000000000000000)

theorem Zeta5Irrational.U_287_6 : Uω (aρ 6) (bρ 6) (3865974428317 / 16000000000000) ≤ -(8345189935393049647993 / 5000000000000000000000)

theorem Zeta5Irrational.U_287_7 : Uω (aρ 7) (bρ 7) (3865974428317 / 16000000000000) ≤ -(18246250365212857194421 / 10000000000000000000000)

theorem Zeta5Irrational.U_287_8 : Uω (aρ 8) (bρ 8) (3865974428317 / 16000000000000) ≤ -(1060412185914542412997 / 500000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_287 : Uρ (3865974428317 / 16000000000000) ≤ -(9070113256560938488283 / 5000000000000000000000)

theorem Zeta5Irrational.U_288_1 : Uω (aρ 1) (bρ 1) (975023636351 / 4000000000000) ≤ -(7192163754279661846917 / 5000000000000000000000)

theorem Zeta5Irrational.U_288_2 : Uω (aρ 2) (bρ 2) (975023636351 / 4000000000000) ≤ -(7243315004429613191293 / 5000000000000000000000)

theorem Zeta5Irrational.U_288_3 : Uω (aρ 3) (bρ 3) (975023636351 / 4000000000000) ≤ -(14695504652313017170091 / 10000000000000000000000)

theorem Zeta5Irrational.U_288_4 : Uω (aρ 4) (bρ 4) (975023636351 / 4000000000000) ≤ -(15055910174395545613739 / 10000000000000000000000)

theorem Zeta5Irrational.U_288_5 : Uω (aρ 5) (bρ 5) (975023636351 / 4000000000000) ≤ -(7820678307979677280879 / 5000000000000000000000)

theorem Zeta5Irrational.U_288_6 : Uω (aρ 6) (bρ 6) (975023636351 / 4000000000000) ≤ -(8287948505380436413979 / 5000000000000000000000)

theorem Zeta5Irrational.U_288_7 : Uω (aρ 7) (bρ 7) (975023636351 / 4000000000000) ≤ -(2263518134952506017373 / 1250000000000000000000)

theorem Zeta5Irrational.U_288_8 : Uω (aρ 8) (bρ 8) (975023636351 / 4000000000000) ≤ -(5248963545902056685773 / 2500000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_288 : Uρ (975023636351 / 4000000000000) ≤ -(1130019727831504586083 / 625000000000000000000)

theorem Zeta5Irrational.U_289_1 : Uω (aρ 1) (bρ 1) (3934214662491 / 16000000000000) ≤ -(2858972133708537061617 / 2000000000000000000000)

theorem Zeta5Irrational.U_289_2 : Uω (aρ 2) (bρ 2) (3934214662491 / 16000000000000) ≤ -(3599058189717142384657 / 2500000000000000000000)

theorem Zeta5Irrational.U_289_3 : Uω (aρ 3) (bρ 3) (3934214662491 / 16000000000000) ≤ -(7301580997444027247323 / 5000000000000000000000)

theorem Zeta5Irrational.U_289_4 : Uω (aρ 4) (bρ 4) (3934214662491 / 16000000000000) ≤ -(1496005898479066858877 / 1000000000000000000000)

theorem Zeta5Irrational.U_289_5 : Uω (aρ 5) (bρ 5) (3934214662491 / 16000000000000) ≤ -(3884839687161393204871 / 2500000000000000000000)

theorem Zeta5Irrational.U_289_6 : Uω (aρ 6) (bρ 6) (3934214662491 / 16000000000000) ≤ -(16462753974742707140679 / 10000000000000000000000)

theorem Zeta5Irrational.U_289_7 : Uω (aρ 7) (bρ 7) (3934214662491 / 16000000000000) ≤ -(17972110093080970712811 / 10000000000000000000000)

theorem Zeta5Irrational.U_289_8 : Uω (aρ 8) (bρ 8) (3934214662491 / 16000000000000) ≤ -(519740407477164840823 / 250000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_289 : Uρ (3934214662491 / 16000000000000) ≤ -(1126339213224684761437 / 625000000000000000000)

theorem Zeta5Irrational.U_290_1 : Uω (aρ 1) (bρ 1) (1984167389789 / 8000000000000) ≤ -(14206187211916833637463 / 10000000000000000000000)

theorem Zeta5Irrational.U_290_2 : Uω (aρ 2) (bρ 2) (1984167389789 / 8000000000000) ≤ -(14306645663022064867043 / 10000000000000000000000)

theorem Zeta5Irrational.U_290_3 : Uω (aρ 3) (bρ 3) (1984167389789 / 8000000000000) ≤ -(1813958175975205347013 / 1250000000000000000000)

theorem Zeta5Irrational.U_290_4 : Uω (aρ 4) (bρ 4) (1984167389789 / 8000000000000) ≤ -(92907010073051215021 / 62500000000000000000)

theorem Zeta5Irrational.U_290_5 : Uω (aρ 5) (bρ 5) (1984167389789 / 8000000000000) ≤ -(15438402962172249138387 / 10000000000000000000000)

theorem Zeta5Irrational.U_290_6 : Uω (aρ 6) (bρ 6) (1984167389789 / 8000000000000) ≤ -(4087729696628356463639 / 2500000000000000000000)

theorem Zeta5Irrational.U_290_7 : Uω (aρ 7) (bρ 7) (1984167389789 / 8000000000000) ≤ -(1783807909004666494059 / 1000000000000000000000)

theorem Zeta5Irrational.U_290_8 : Uω (aρ 8) (bρ 8) (1984167389789 / 8000000000000) ≤ -(1286819084048231859999 / 625000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_290 : Uρ (1984167389789 / 8000000000000) ≤ -(8981756148083042841929 / 5000000000000000000000)

theorem Zeta5Irrational.U_291_1 : Uω (aρ 1) (bρ 1) (504571876719 / 2000000000000) ≤ -(3507791254907928832507 / 2500000000000000000000)

theorem Zeta5Irrational.U_291_2 : Uω (aρ 2) (bρ 2) (504571876719 / 2000000000000) ≤ -(7064922361463546649243 / 5000000000000000000000)

theorem Zeta5Irrational.U_291_3 : Uω (aρ 3) (bρ 3) (504571876719 / 2000000000000) ≤ -(14331149326100729740711 / 10000000000000000000000)

theorem Zeta5Irrational.U_291_4 : Uω (aρ 4) (bρ 4) (504571876719 / 2000000000000) ≤ -(14677919486345039845707 / 10000000000000000000000)

theorem Zeta5Irrational.U_291_5 : Uω (aρ 5) (bρ 5) (504571876719 / 2000000000000) ≤ -(3047906602216523433211 / 2000000000000000000000)

theorem Zeta5Irrational.U_291_6 : Uω (aρ 6) (bρ 6) (504571876719 / 2000000000000) ≤ -(2016381225759584278767 / 1250000000000000000000)

theorem Zeta5Irrational.U_291_7 : Uω (aρ 7) (bρ 7) (504571876719 / 2000000000000) ≤ -(8787890108594326096779 / 5000000000000000000000)

theorem Zeta5Irrational.U_291_8 : Uω (aρ 8) (bρ 8) (504571876719 / 2000000000000) ≤ -(20203793397973935609921 / 10000000000000000000000)

theorem Zeta5Irrational.U_291_9 : Uω (aρ 9) (bρ 9) (504571876719 / 2000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_291_10 : Uω (aρ 10) (bρ 10) (504571876719 / 2000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_291_11 : Uω (aρ 11) (bρ 11) (504571876719 / 2000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_291_12 : Uω (aρ 12) (bρ 12) (504571876719 / 2000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_291_13 : Uω (aρ 13) (bρ 13) (504571876719 / 2000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_291_14 : Uω (aρ 14) (bρ 14) (504571876719 / 2000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_291_15 : Uω (aρ 15) (bρ 15) (504571876719 / 2000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_291_16 : Uω (aρ 16) (bρ 16) (504571876719 / 2000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_291 : Uρ (504571876719 / 2000000000000) ≤ -(8925212957824183781139 / 5000000000000000000000)