Certified arcsine potential bounds (U41)

theorem Zeta5Irrational.U_496_1 : Uω (aρ 1) (bρ 1) (4364155818193 / 8000000000000) ≤ -(6179158631021010828439 / 10000000000000000000000)

theorem Zeta5Irrational.U_496_2 : Uω (aρ 2) (bρ 2) (4364155818193 / 8000000000000) ≤ -(6223661486905342670339 / 10000000000000000000000)

theorem Zeta5Irrational.U_496_3 : Uω (aρ 3) (bρ 3) (4364155818193 / 8000000000000) ≤ -(1578326067291152192927 / 2500000000000000000000)

theorem Zeta5Irrational.U_496_4 : Uω (aρ 4) (bρ 4) (4364155818193 / 8000000000000) ≤ -(6464105087964167300301 / 10000000000000000000000)

theorem Zeta5Irrational.U_496_5 : Uω (aρ 5) (bρ 5) (4364155818193 / 8000000000000) ≤ -(6698515862953343862829 / 10000000000000000000000)

theorem Zeta5Irrational.U_496_6 : Uω (aρ 6) (bρ 6) (4364155818193 / 8000000000000) ≤ -(7045327077678014554961 / 10000000000000000000000)

theorem Zeta5Irrational.U_496_7 : Uω (aρ 7) (bρ 7) (4364155818193 / 8000000000000) ≤ -(1508095917026171862497 / 2000000000000000000000)

theorem Zeta5Irrational.U_496_8 : Uω (aρ 8) (bρ 8) (4364155818193 / 8000000000000) ≤ -(514369428705734080287 / 625000000000000000000)

theorem Zeta5Irrational.U_496_9 : Uω (aρ 9) (bρ 9) (4364155818193 / 8000000000000) ≤ -(9177266539706387383039 / 10000000000000000000000)

theorem Zeta5Irrational.U_496_10 : Uω (aρ 10) (bρ 10) (4364155818193 / 8000000000000) ≤ -(10485693084161377691493 / 10000000000000000000000)

theorem Zeta5Irrational.U_496_11 : Uω (aρ 11) (bρ 11) (4364155818193 / 8000000000000) ≤ -(193366462786153684599 / 156250000000000000000)

theorem Zeta5Irrational.U_496_12 : Uω (aρ 12) (bρ 12) (4364155818193 / 8000000000000) ≤ -(1964224768782355217967 / 1250000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_496 : Uρ (4364155818193 / 8000000000000) ≤ -(480610621488243035319 / 500000000000000000000)

theorem Zeta5Irrational.U_497_1 : Uω (aρ 1) (bρ 1) (69906379973123 / 128000000000000) ≤ -(6167587546193927183517 / 10000000000000000000000)

theorem Zeta5Irrational.U_497_2 : Uω (aρ 2) (bρ 2) (69906379973123 / 128000000000000) ≤ -(6212038459828908181177 / 10000000000000000000000)

theorem Zeta5Irrational.U_497_3 : Uω (aρ 3) (bρ 3) (69906379973123 / 128000000000000) ≤ -(6153882366540572167 / 9765625000000000000)

theorem Zeta5Irrational.U_497_4 : Uω (aρ 4) (bρ 4) (69906379973123 / 128000000000000) ≤ -(6452195255314039757353 / 10000000000000000000000)

theorem Zeta5Irrational.U_497_5 : Uω (aρ 5) (bρ 5) (69906379973123 / 128000000000000) ≤ -(668631600941429284913 / 1000000000000000000000)

theorem Zeta5Irrational.U_497_6 : Uω (aρ 6) (bρ 6) (69906379973123 / 128000000000000) ≤ -(6867849691752660767 / 9765625000000000000)

theorem Zeta5Irrational.U_497_7 : Uω (aρ 7) (bρ 7) (69906379973123 / 128000000000000) ≤ -(7527144268936852965187 / 10000000000000000000000)

theorem Zeta5Irrational.U_497_8 : Uω (aρ 8) (bρ 8) (69906379973123 / 128000000000000) ≤ -(513470005995439371749 / 625000000000000000000)

theorem Zeta5Irrational.U_497_9 : Uω (aρ 9) (bρ 9) (69906379973123 / 128000000000000) ≤ -(366447935732025427061 / 400000000000000000000)

theorem Zeta5Irrational.U_497_10 : Uω (aρ 10) (bρ 10) (69906379973123 / 128000000000000) ≤ -(1308342692389497524921 / 1250000000000000000000)

theorem Zeta5Irrational.U_497_11 : Uω (aρ 11) (bρ 11) (69906379973123 / 128000000000000) ≤ -(3087635739603101573631 / 2500000000000000000000)

theorem Zeta5Irrational.U_497_12 : Uω (aρ 12) (bρ 12) (69906379973123 / 128000000000000) ≤ -(3133047669711312742019 / 2000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_497 : Uρ (69906379973123 / 128000000000000) ≤ -(2399471840990113090949 / 2500000000000000000000)

theorem Zeta5Irrational.U_498_1 : Uω (aρ 1) (bρ 1) (34993133427579 / 64000000000000) ≤ -(6156029835042409091741 / 10000000000000000000000)

theorem Zeta5Irrational.U_498_2 : Uω (aρ 2) (bρ 2) (34993133427579 / 64000000000000) ≤ -(1550107231884159405343 / 2500000000000000000000)

theorem Zeta5Irrational.U_498_3 : Uω (aρ 3) (bρ 3) (34993133427579 / 64000000000000) ≤ -(1257972112255709486683 / 2000000000000000000000)

theorem Zeta5Irrational.U_498_4 : Uω (aρ 4) (bρ 4) (34993133427579 / 64000000000000) ≤ -(6440299601029007882821 / 10000000000000000000000)

theorem Zeta5Irrational.U_498_5 : Uω (aρ 5) (bρ 5) (34993133427579 / 64000000000000) ≤ -(6674131051530196510577 / 10000000000000000000000)

theorem Zeta5Irrational.U_498_6 : Uω (aρ 6) (bρ 6) (34993133427579 / 64000000000000) ≤ -(438752821916816559511 / 625000000000000000000)

theorem Zeta5Irrational.U_498_7 : Uω (aρ 7) (bρ 7) (34993133427579 / 64000000000000) ≤ -(7513826920613636684123 / 10000000000000000000000)

theorem Zeta5Irrational.U_498_8 : Uω (aρ 8) (bρ 8) (34993133427579 / 64000000000000) ≤ -(2050287639504809022989 / 2500000000000000000000)

theorem Zeta5Irrational.U_498_9 : Uω (aρ 9) (bρ 9) (34993133427579 / 64000000000000) ≤ -(9145157522639751445491 / 10000000000000000000000)

theorem Zeta5Irrational.U_498_10 : Uω (aρ 10) (bρ 10) (34993133427579 / 64000000000000) ≤ -(10447830492519363594599 / 10000000000000000000000)

theorem Zeta5Irrational.U_498_11 : Uω (aρ 11) (bρ 11) (34993133427579 / 64000000000000) ≤ -(12325713800658735169931 / 10000000000000000000000)

theorem Zeta5Irrational.U_498_12 : Uω (aρ 12) (bρ 12) (34993133427579 / 64000000000000) ≤ -(7808599520102826369753 / 5000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_498 : Uρ (34993133427579 / 64000000000000) ≤ -(383344754671723342871 / 400000000000000000000)

theorem Zeta5Irrational.U_499_1 : Uω (aρ 1) (bρ 1) (70066153737193 / 128000000000000) ≤ -(3072242733343819264019 / 5000000000000000000000)

theorem Zeta5Irrational.U_499_2 : Uω (aρ 2) (bρ 2) (70066153737193 / 128000000000000) ≤ -(6188832858726643796807 / 10000000000000000000000)

theorem Zeta5Irrational.U_499_3 : Uω (aρ 3) (bρ 3) (70066153737193 / 128000000000000) ≤ -(6278159290806943346951 / 10000000000000000000000)

theorem Zeta5Irrational.U_499_4 : Uω (aρ 4) (bρ 4) (70066153737193 / 128000000000000) ≤ -(6428418091365539699 / 10000000000000000000)

theorem Zeta5Irrational.U_499_5 : Uω (aρ 5) (bρ 5) (70066153737193 / 128000000000000) ≤ -(832745119112230134817 / 1250000000000000000000)

theorem Zeta5Irrational.U_499_6 : Uω (aρ 6) (bρ 6) (70066153737193 / 128000000000000) ≤ -(3503714117845335411479 / 5000000000000000000000)

theorem Zeta5Irrational.U_499_7 : Uω (aρ 7) (bρ 7) (70066153737193 / 128000000000000) ≤ -(937565936406325238339 / 1250000000000000000000)

theorem Zeta5Irrational.U_499_8 : Uω (aρ 8) (bρ 8) (70066153737193 / 128000000000000) ≤ -(1637360436293184612359 / 2000000000000000000000)

theorem Zeta5Irrational.U_499_9 : Uω (aρ 9) (bρ 9) (70066153737193 / 128000000000000) ≤ -(4564571915178486632409 / 5000000000000000000000)

theorem Zeta5Irrational.U_499_10 : Uω (aρ 10) (bρ 10) (70066153737193 / 128000000000000) ≤ -(2607239938261753790789 / 2500000000000000000000)

theorem Zeta5Irrational.U_499_11 : Uω (aρ 11) (bρ 11) (70066153737193 / 128000000000000) ≤ -(6150482750929794706883 / 5000000000000000000000)

theorem Zeta5Irrational.U_499_12 : Uω (aρ 12) (bρ 12) (70066153737193 / 128000000000000) ≤ -(15569664912888544190381 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_499 : Uρ (70066153737193 / 128000000000000) ≤ -(9569405765138696291859 / 10000000000000000000000)

theorem Zeta5Irrational.U_500_1 : Uω (aρ 1) (bρ 1) (17536510154807 / 32000000000000) ≤ -(6132954410357619226903 / 10000000000000000000000)

theorem Zeta5Irrational.U_500_2 : Uω (aρ 2) (bρ 2) (17536510154807 / 32000000000000) ≤ -(6177250222205826174879 / 10000000000000000000000)

theorem Zeta5Irrational.U_500_3 : Uω (aρ 3) (bρ 3) (17536510154807 / 32000000000000) ≤ -(195827240620468206163 / 312500000000000000000)

theorem Zeta5Irrational.U_500_4 : Uω (aρ 4) (bρ 4) (17536510154807 / 32000000000000) ≤ -(3208275346350256311827 / 5000000000000000000000)

theorem Zeta5Irrational.U_500_5 : Uω (aρ 5) (bρ 5) (17536510154807 / 32000000000000) ≤ -(831225709655945375553 / 1250000000000000000000)

theorem Zeta5Irrational.U_500_6 : Uω (aρ 6) (bρ 6) (17536510154807 / 32000000000000) ≤ -(6994827298646218981741 / 10000000000000000000000)

theorem Zeta5Irrational.U_500_7 : Uω (aρ 7) (bρ 7) (17536510154807 / 32000000000000) ≤ -(7487245932138787324571 / 10000000000000000000000)

theorem Zeta5Irrational.U_500_8 : Uω (aρ 8) (bρ 8) (17536510154807 / 32000000000000) ≤ -(4086237451230692446593 / 5000000000000000000000)

theorem Zeta5Irrational.U_500_9 : Uω (aρ 9) (bρ 9) (17536510154807 / 32000000000000) ≤ -(2278289304907380917197 / 2500000000000000000000)

theorem Zeta5Irrational.U_500_10 : Uω (aρ 10) (bρ 10) (17536510154807 / 32000000000000) ≤ -(10410129130832395465343 / 10000000000000000000000)

theorem Zeta5Irrational.U_500_11 : Uω (aρ 11) (bρ 11) (17536510154807 / 32000000000000) ≤ -(12276297427255723426533 / 10000000000000000000000)

theorem Zeta5Irrational.U_500_12 : Uω (aρ 12) (bρ 12) (17536510154807 / 32000000000000) ≤ -(3880655349478368086291 / 2500000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_500 : Uρ (17536510154807 / 32000000000000) ≤ -(382209877564364374023 / 400000000000000000000)

theorem Zeta5Irrational.U_501_1 : Uω (aρ 1) (bρ 1) (35152907191649 / 64000000000000) ≤ -(1527483027803754788683 / 2500000000000000000000)

theorem Zeta5Irrational.U_501_2 : Uω (aρ 2) (bρ 2) (35152907191649 / 64000000000000) ≤ -(3077062560900137648367 / 5000000000000000000000)

theorem Zeta5Irrational.U_501_3 : Uω (aρ 3) (bρ 3) (35152907191649 / 64000000000000) ≤ -(6243137428800446165823 / 10000000000000000000000)

theorem Zeta5Irrational.U_501_4 : Uω (aρ 4) (bρ 4) (35152907191649 / 64000000000000) ≤ -(3196429047235951039163 / 5000000000000000000000)

theorem Zeta5Irrational.U_501_5 : Uω (aρ 5) (bρ 5) (35152907191649 / 64000000000000) ≤ -(3312769725239216942567 / 5000000000000000000000)

theorem Zeta5Irrational.U_501_6 : Uω (aρ 6) (bρ 6) (35152907191649 / 64000000000000) ≤ -(6969673196046202864671 / 10000000000000000000000)

theorem Zeta5Irrational.U_501_7 : Uω (aρ 7) (bρ 7) (35152907191649 / 64000000000000) ≤ -(746073623083452947819 / 1000000000000000000000)

theorem Zeta5Irrational.U_501_8 : Uω (aρ 8) (bρ 8) (35152907191649 / 64000000000000) ≤ -(4071941691674149917709 / 5000000000000000000000)

theorem Zeta5Irrational.U_501_9 : Uω (aρ 9) (bρ 9) (35152907191649 / 64000000000000) ≤ -(4540632429122172497341 / 5000000000000000000000)

theorem Zeta5Irrational.U_501_10 : Uω (aρ 10) (bρ 10) (35152907191649 / 64000000000000) ≤ -(2074517497181400129451 / 2000000000000000000000)

theorem Zeta5Irrational.U_501_11 : Uω (aρ 11) (bρ 11) (35152907191649 / 64000000000000) ≤ -(1222719945283823425943 / 1000000000000000000000)

theorem Zeta5Irrational.U_501_12 : Uω (aρ 12) (bρ 12) (35152907191649 / 64000000000000) ≤ -(15429951354170808899491 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_501 : Uρ (35152907191649 / 64000000000000) ≤ -(1190885984971035254361 / 1250000000000000000000)

theorem Zeta5Irrational.U_502_1 : Uω (aρ 1) (bρ 1) (8808198518421 / 16000000000000) ≤ -(304348134677823892373 / 500000000000000000000)

theorem Zeta5Irrational.U_502_2 : Uω (aρ 2) (bρ 2) (8808198518421 / 16000000000000) ≤ -(3065526689465984201931 / 5000000000000000000000)

theorem Zeta5Irrational.U_502_3 : Uω (aρ 3) (bρ 3) (8808198518421 / 16000000000000) ≤ -(3109928746905706661603 / 5000000000000000000000)

theorem Zeta5Irrational.U_502_4 : Uω (aρ 4) (bρ 4) (8808198518421 / 16000000000000) ≤ -(1592305384936174259601 / 2500000000000000000000)

theorem Zeta5Irrational.U_502_5 : Uω (aρ 5) (bρ 5) (8808198518421 / 16000000000000) ≤ -(6601332083711793922337 / 10000000000000000000000)

theorem Zeta5Irrational.U_502_6 : Uω (aρ 6) (bρ 6) (8808198518421 / 16000000000000) ≤ -(6944582519792693022809 / 10000000000000000000000)

theorem Zeta5Irrational.U_502_7 : Uω (aρ 7) (bρ 7) (8808198518421 / 16000000000000) ≤ -(7434297431019868095343 / 10000000000000000000000)

theorem Zeta5Irrational.U_502_8 : Uω (aρ 8) (bρ 8) (8808198518421 / 16000000000000) ≤ -(1014421937012309681831 / 1250000000000000000000)

theorem Zeta5Irrational.U_502_9 : Uω (aρ 9) (bρ 9) (8808198518421 / 16000000000000) ≤ -(4524739837311758777763 / 5000000000000000000000)

theorem Zeta5Irrational.U_502_10 : Uω (aρ 10) (bρ 10) (8808198518421 / 16000000000000) ≤ -(5167602033692465113331 / 5000000000000000000000)

theorem Zeta5Irrational.U_502_11 : Uω (aρ 11) (bρ 11) (8808198518421 / 16000000000000) ≤ -(1522301870274884627343 / 1250000000000000000000)

theorem Zeta5Irrational.U_502_12 : Uω (aρ 12) (bρ 12) (8808198518421 / 16000000000000) ≤ -(1917385680481320352707 / 1250000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_502 : Uρ (8808198518421 / 16000000000000) ≤ -(189982673360871353711 / 200000000000000000000)

theorem Zeta5Irrational.U_503_1 : Uω (aρ 1) (bρ 1) (35312680955719 / 64000000000000) ≤ -(6064045915001829464321 / 10000000000000000000000)

theorem Zeta5Irrational.U_503_2 : Uω (aρ 2) (bρ 2) (35312680955719 / 64000000000000) ≤ -(1221606949584324856063 / 2000000000000000000000)

theorem Zeta5Irrational.U_503_3 : Uω (aρ 3) (bρ 3) (35312680955719 / 64000000000000) ≤ -(3098315821178827396319 / 5000000000000000000000)

theorem Zeta5Irrational.U_503_4 : Uω (aρ 4) (bρ 4) (35312680955719 / 64000000000000) ≤ -(634564076381066350629 / 1000000000000000000000)

theorem Zeta5Irrational.U_503_5 : Uω (aρ 5) (bρ 5) (35312680955719 / 64000000000000) ≤ -(3288591645766013384659 / 5000000000000000000000)

theorem Zeta5Irrational.U_503_6 : Uω (aρ 6) (bρ 6) (35312680955719 / 64000000000000) ≤ -(6919554951870387697571 / 10000000000000000000000)

theorem Zeta5Irrational.U_503_7 : Uω (aρ 7) (bρ 7) (35312680955719 / 64000000000000) ≤ -(7407929150169422584079 / 10000000000000000000000)

theorem Zeta5Irrational.U_503_8 : Uω (aρ 8) (bρ 8) (35312680955719 / 64000000000000) ≤ -(8086950740760240682239 / 10000000000000000000000)

theorem Zeta5Irrational.U_503_9 : Uω (aρ 9) (bρ 9) (35312680955719 / 64000000000000) ≤ -(4508900456673071142313 / 5000000000000000000000)

theorem Zeta5Irrational.U_503_10 : Uω (aρ 10) (bρ 10) (35312680955719 / 64000000000000) ≤ -(5148988703631236251007 / 5000000000000000000000)

theorem Zeta5Irrational.U_503_11 : Uω (aρ 11) (bρ 11) (35312680955719 / 64000000000000) ≤ -(2425987833100888042973 / 2000000000000000000000)

theorem Zeta5Irrational.U_503_12 : Uω (aρ 12) (bρ 12) (35312680955719 / 64000000000000) ≤ -(15249929318392561796379 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_503 : Uρ (35312680955719 / 64000000000000) ≤ -(947137693861291331499 / 1000000000000000000000)

theorem Zeta5Irrational.U_504_1 : Uω (aρ 1) (bρ 1) (17696283918877 / 32000000000000) ≤ -(60411815348335259041 / 100000000000000000000)

theorem Zeta5Irrational.U_504_2 : Uω (aρ 2) (bρ 2) (17696283918877 / 32000000000000) ≤ -(3042534492391497808847 / 5000000000000000000000)

theorem Zeta5Irrational.U_504_3 : Uω (aρ 3) (bρ 3) (17696283918877 / 32000000000000) ≤ -(6173459623665779297577 / 10000000000000000000000)

theorem Zeta5Irrational.U_504_4 : Uω (aρ 4) (bρ 4) (17696283918877 / 32000000000000) ≤ -(1580528875958493533667 / 2500000000000000000000)

theorem Zeta5Irrational.U_504_5 : Uω (aρ 5) (bρ 5) (17696283918877 / 32000000000000) ≤ -(6553092790598556143351 / 10000000000000000000000)

theorem Zeta5Irrational.U_504_6 : Uω (aρ 6) (bρ 6) (17696283918877 / 32000000000000) ≤ -(3447295084451065829983 / 5000000000000000000000)

theorem Zeta5Irrational.U_504_7 : Uω (aρ 7) (bρ 7) (17696283918877 / 32000000000000) ≤ -(3690815504439367221797 / 5000000000000000000000)

theorem Zeta5Irrational.U_504_8 : Uω (aρ 8) (bρ 8) (17696283918877 / 32000000000000) ≤ -(1007326077744263590559 / 1250000000000000000000)

theorem Zeta5Irrational.U_504_9 : Uω (aρ 9) (bρ 9) (17696283918877 / 32000000000000) ≤ -(1123278478412851818853 / 1250000000000000000000)

theorem Zeta5Irrational.U_504_10 : Uω (aρ 10) (bρ 10) (17696283918877 / 32000000000000) ≤ -(10260906059422783887687 / 10000000000000000000000)

theorem Zeta5Irrational.U_504_11 : Uω (aρ 11) (bρ 11) (17696283918877 / 32000000000000) ≤ -(755110462113986613171 / 625000000000000000000)

theorem Zeta5Irrational.U_504_12 : Uω (aρ 12) (bρ 12) (17696283918877 / 32000000000000) ≤ -(1516239665633792455279 / 1000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_504 : Uρ (17696283918877 / 32000000000000) ≤ -(1180476362959208691143 / 1250000000000000000000)

theorem Zeta5Irrational.U_505_1 : Uω (aρ 1) (bρ 1) (35472454719789 / 64000000000000) ≤ -(6018369313981465330427 / 10000000000000000000000)

theorem Zeta5Irrational.U_505_2 : Uω (aρ 2) (bρ 2) (35472454719789 / 64000000000000) ≤ -(6062155847207341966241 / 10000000000000000000000)

theorem Zeta5Irrational.U_505_3 : Uω (aρ 3) (bρ 3) (35472454719789 / 64000000000000) ≤ -(384396324293936033753 / 625000000000000000000)

theorem Zeta5Irrational.U_505_4 : Uω (aρ 4) (bρ 4) (35472454719789 / 64000000000000) ≤ -(6298645498833575554591 / 10000000000000000000000)

theorem Zeta5Irrational.U_505_5 : Uω (aρ 5) (bρ 5) (35472454719789 / 64000000000000) ≤ -(6529060299625747032463 / 10000000000000000000000)

theorem Zeta5Irrational.U_505_6 : Uω (aρ 6) (bρ 6) (35472454719789 / 64000000000000) ≤ -(858710982215112154227 / 1250000000000000000000)

theorem Zeta5Irrational.U_505_7 : Uω (aρ 7) (bρ 7) (35472454719789 / 64000000000000) ≤ -(58843221046640534947 / 80000000000000000000)

theorem Zeta5Irrational.U_505_8 : Uω (aρ 8) (bρ 8) (35472454719789 / 64000000000000) ≤ -(2007587162204019625203 / 2500000000000000000000)

theorem Zeta5Irrational.U_505_9 : Uω (aρ 9) (bρ 9) (35472454719789 / 64000000000000) ≤ -(8954759677569814852371 / 10000000000000000000000)

theorem Zeta5Irrational.U_505_10 : Uω (aρ 10) (bρ 10) (35472454719789 / 64000000000000) ≤ -(255599714979519626207 / 250000000000000000000)

theorem Zeta5Irrational.U_505_11 : Uω (aρ 11) (bρ 11) (35472454719789 / 64000000000000) ≤ -(6016947547431752205949 / 5000000000000000000000)

theorem Zeta5Irrational.U_505_12 : Uω (aρ 12) (bρ 12) (35472454719789 / 64000000000000) ≤ -(1884551029486662392393 / 1250000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_505 : Uρ (35472454719789 / 64000000000000) ≤ -(9416429288524211005069 / 10000000000000000000000)

theorem Zeta5Irrational.U_506_1 : Uω (aρ 1) (bρ 1) (1111010675057 / 2000000000000) ≤ -(59956090150079933539 / 100000000000000000000)

theorem Zeta5Irrational.U_506_2 : Uω (aρ 2) (bρ 2) (1111010675057 / 2000000000000) ≤ -(6039295094548093923991 / 10000000000000000000000)

theorem Zeta5Irrational.U_506_3 : Uω (aρ 3) (bρ 3) (1111010675057 / 2000000000000) ≤ -(6127276090160940364943 / 10000000000000000000000)

theorem Zeta5Irrational.U_506_4 : Uω (aρ 4) (bρ 4) (1111010675057 / 2000000000000) ≤ -(3137615244832883098359 / 5000000000000000000000)

theorem Zeta5Irrational.U_506_5 : Uω (aρ 5) (bρ 5) (1111010675057 / 2000000000000) ≤ -(6505085539363036308551 / 10000000000000000000000)

theorem Zeta5Irrational.U_506_6 : Uω (aρ 6) (bρ 6) (1111010675057 / 2000000000000) ≤ -(6844847704947540843917 / 10000000000000000000000)

theorem Zeta5Irrational.U_506_7 : Uω (aρ 7) (bρ 7) (1111010675057 / 2000000000000) ≤ -(3664621821379332739513 / 5000000000000000000000)

theorem Zeta5Irrational.U_506_8 : Uω (aρ 8) (bρ 8) (1111010675057 / 2000000000000) ≤ -(4001085167470894044969 / 5000000000000000000000)

theorem Zeta5Irrational.U_506_9 : Uω (aρ 9) (bρ 9) (1111010675057 / 2000000000000) ≤ -(35693582933142942329 / 40000000000000000000)

theorem Zeta5Irrational.U_506_10 : Uω (aρ 10) (bρ 10) (1111010675057 / 2000000000000) ≤ -(10187223622840232274999 / 10000000000000000000000)

theorem Zeta5Irrational.U_506_11 : Uω (aρ 11) (bρ 11) (1111010675057 / 2000000000000) ≤ -(5993158914446563252359 / 5000000000000000000000)

theorem Zeta5Irrational.U_506_12 : Uω (aρ 12) (bρ 12) (1111010675057 / 2000000000000) ≤ -(14991891141000413337327 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_506 : Uρ (1111010675057 / 2000000000000) ≤ -(9389226274504482798993 / 10000000000000000000000)

theorem Zeta5Irrational.U_507_1 : Uω (aρ 1) (bρ 1) (35632228483859 / 64000000000000) ≤ -(373306275130817100621 / 625000000000000000000)

theorem Zeta5Irrational.U_507_2 : Uω (aρ 2) (bρ 2) (35632228483859 / 64000000000000) ≤ -(3008243243902837444081 / 5000000000000000000000)

theorem Zeta5Irrational.U_507_3 : Uω (aρ 3) (bρ 3) (35632228483859 / 64000000000000) ≤ -(6104264082439977002931 / 10000000000000000000000)

theorem Zeta5Irrational.U_507_4 : Uω (aρ 4) (bρ 4) (35632228483859 / 64000000000000) ≤ -(6251870219006976036533 / 10000000000000000000000)

theorem Zeta5Irrational.U_507_5 : Uω (aρ 5) (bρ 5) (35632228483859 / 64000000000000) ≤ -(6481168232575320061883 / 10000000000000000000000)

theorem Zeta5Irrational.U_507_6 : Uω (aρ 6) (bρ 6) (35632228483859 / 64000000000000) ≤ -(3410034699783073694907 / 5000000000000000000000)

theorem Zeta5Irrational.U_507_7 : Uω (aρ 7) (bρ 7) (35632228483859 / 64000000000000) ≤ -(1460630734883897880289 / 2000000000000000000000)

theorem Zeta5Irrational.U_507_8 : Uω (aρ 8) (bρ 8) (35632228483859 / 64000000000000) ≤ -(3987036599165787142513 / 5000000000000000000000)

theorem Zeta5Irrational.U_507_9 : Uω (aρ 9) (bρ 9) (35632228483859 / 64000000000000) ≤ -(8892135271530491175893 / 10000000000000000000000)

theorem Zeta5Irrational.U_507_10 : Uω (aρ 10) (bρ 10) (35632228483859 / 64000000000000) ≤ -(5075304873631269541131 / 5000000000000000000000)

theorem Zeta5Irrational.U_507_11 : Uω (aρ 11) (bρ 11) (35632228483859 / 64000000000000) ≤ -(11939031264853494913149 / 10000000000000000000000)

theorem Zeta5Irrational.U_507_12 : Uω (aρ 12) (bρ 12) (35632228483859 / 64000000000000) ≤ -(2981755615627733624033 / 2000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_507 : Uρ (35632228483859 / 64000000000000) ≤ -(1170274556345986861049 / 1250000000000000000000)