Certified arcsine potential bounds (U47)

theorem Zeta5Irrational.U_568_1 : Uω (aρ 1) (bρ 1) (5245138462927 / 8000000000000) ≤ -(4320296992729446895061 / 10000000000000000000000)

theorem Zeta5Irrational.U_568_2 : Uω (aρ 2) (bρ 2) (5245138462927 / 8000000000000) ≤ -(2178596304860126658363 / 5000000000000000000000)

theorem Zeta5Irrational.U_568_3 : Uω (aρ 3) (bρ 3) (5245138462927 / 8000000000000) ≤ -(553922780094374103553 / 1250000000000000000000)

theorem Zeta5Irrational.U_568_4 : Uω (aρ 4) (bρ 4) (5245138462927 / 8000000000000) ≤ -(36446318800435169751 / 80000000000000000000)

theorem Zeta5Irrational.U_568_5 : Uω (aρ 5) (bρ 5) (5245138462927 / 8000000000000) ≤ -(1187039758133659573379 / 2500000000000000000000)

theorem Zeta5Irrational.U_568_6 : Uω (aρ 6) (bρ 6) (5245138462927 / 8000000000000) ≤ -(5030412153596103091251 / 10000000000000000000000)

theorem Zeta5Irrational.U_568_7 : Uω (aρ 7) (bρ 7) (5245138462927 / 8000000000000) ≤ -(5428221581310503912809 / 10000000000000000000000)

theorem Zeta5Irrational.U_568_8 : Uω (aρ 8) (bρ 8) (5245138462927 / 8000000000000) ≤ -(597109085408817176559 / 1000000000000000000000)

theorem Zeta5Irrational.U_568_9 : Uω (aρ 9) (bρ 9) (5245138462927 / 8000000000000) ≤ -(3346738440394695985477 / 5000000000000000000000)

theorem Zeta5Irrational.U_568_10 : Uω (aρ 10) (bρ 10) (5245138462927 / 8000000000000) ≤ -(7638238555624362940643 / 10000000000000000000000)

theorem Zeta5Irrational.U_568_11 : Uω (aρ 11) (bρ 11) (5245138462927 / 8000000000000) ≤ -(2216547990186434725099 / 2500000000000000000000)

theorem Zeta5Irrational.U_568_12 : Uω (aρ 12) (bρ 12) (5245138462927 / 8000000000000) ≤ -(2621534172356183131653 / 2500000000000000000000)

theorem Zeta5Irrational.U_568_13 : Uω (aρ 13) (bρ 13) (5245138462927 / 8000000000000) ≤ -(12791974179380312102249 / 10000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_568 : Uρ (5245138462927 / 8000000000000) ≤ -(7197794843052013057711 / 10000000000000000000000)

theorem Zeta5Irrational.U_569_1 : Uω (aρ 1) (bρ 1) (10559069530791 / 16000000000000) ≤ -(4254285836572129056119 / 10000000000000000000000)

theorem Zeta5Irrational.U_569_2 : Uω (aρ 2) (bρ 2) (10559069530791 / 16000000000000) ≤ -(4290936846030395396877 / 10000000000000000000000)

theorem Zeta5Irrational.U_569_3 : Uω (aρ 3) (bρ 3) (10559069530791 / 16000000000000) ≤ -(4364630488213829430073 / 10000000000000000000000)

theorem Zeta5Irrational.U_569_4 : Uω (aρ 4) (bρ 4) (10559069530791 / 16000000000000) ≤ -(448819378046638877049 / 1000000000000000000000)

theorem Zeta5Irrational.U_569_5 : Uω (aρ 5) (bρ 5) (10559069530791 / 16000000000000) ≤ -(935845087457148488507 / 2000000000000000000000)

theorem Zeta5Irrational.U_569_6 : Uω (aρ 6) (bρ 6) (10559069530791 / 16000000000000) ≤ -(1239860650579759773883 / 2500000000000000000000)

theorem Zeta5Irrational.U_569_7 : Uω (aρ 7) (bρ 7) (10559069530791 / 16000000000000) ≤ -(535422405003292823967 / 1000000000000000000000)

theorem Zeta5Irrational.U_569_8 : Uω (aρ 8) (bρ 8) (10559069530791 / 16000000000000) ≤ -(589263219909437068171 / 1000000000000000000000)

theorem Zeta5Irrational.U_569_9 : Uω (aρ 9) (bρ 9) (10559069530791 / 16000000000000) ≤ -(826051030152510713157 / 1250000000000000000000)

theorem Zeta5Irrational.U_569_10 : Uω (aρ 10) (bρ 10) (10559069530791 / 16000000000000) ≤ -(7543122663510840268807 / 10000000000000000000000)

theorem Zeta5Irrational.U_569_11 : Uω (aρ 11) (bρ 11) (10559069530791 / 16000000000000) ≤ -(1750982146713054436347 / 2000000000000000000000)

theorem Zeta5Irrational.U_569_12 : Uω (aρ 12) (bρ 12) (10559069530791 / 16000000000000) ≤ -(5172777597921439708851 / 5000000000000000000000)

theorem Zeta5Irrational.U_569_13 : Uω (aρ 13) (bρ 13) (10559069530791 / 16000000000000) ≤ -(393112829726998233739 / 312500000000000000000)

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

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

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

theorem Zeta5Irrational.U_569 : Uρ (10559069530791 / 16000000000000) ≤ -(35589846219897266431 / 50000000000000000000)

theorem Zeta5Irrational.U_570_1 : Uω (aρ 1) (bρ 1) (664241383483 / 1000000000000) ≤ -(4188707574941079792709 / 10000000000000000000000)

theorem Zeta5Irrational.U_570_2 : Uω (aρ 2) (bρ 2) (664241383483 / 1000000000000) ≤ -(4225117198853214904403 / 10000000000000000000000)

theorem Zeta5Irrational.U_570_3 : Uω (aρ 3) (bρ 3) (664241383483 / 1000000000000) ≤ -(429832144022243457453 / 1000000000000000000000)

theorem Zeta5Irrational.U_570_4 : Uω (aρ 4) (bρ 4) (664241383483 / 1000000000000) ≤ -(552631475048740095093 / 1250000000000000000000)

theorem Zeta5Irrational.U_570_5 : Uω (aρ 5) (bρ 5) (664241383483 / 1000000000000) ≤ -(4610764411565489378927 / 10000000000000000000000)

theorem Zeta5Irrational.U_570_6 : Uω (aρ 6) (bρ 6) (664241383483 / 1000000000000) ≤ -(2444487408756060489599 / 5000000000000000000000)

theorem Zeta5Irrational.U_570_7 : Uω (aρ 7) (bρ 7) (664241383483 / 1000000000000) ≤ -(5280774161118552785937 / 10000000000000000000000)

theorem Zeta5Irrational.U_570_8 : Uω (aρ 8) (bρ 8) (664241383483 / 1000000000000) ≤ -(5814794347494712517697 / 10000000000000000000000)

theorem Zeta5Irrational.U_570_9 : Uω (aρ 9) (bρ 9) (664241383483 / 1000000000000) ≤ -(1631020436464782829367 / 2500000000000000000000)

theorem Zeta5Irrational.U_570_10 : Uω (aρ 10) (bρ 10) (664241383483 / 1000000000000) ≤ -(744896543364644492559 / 1000000000000000000000)

theorem Zeta5Irrational.U_570_11 : Uω (aρ 11) (bρ 11) (664241383483 / 1000000000000) ≤ -(4322513676307216232947 / 5000000000000000000000)

theorem Zeta5Irrational.U_570_12 : Uω (aρ 12) (bρ 12) (664241383483 / 1000000000000) ≤ -(10207502320509313781759 / 10000000000000000000000)

theorem Zeta5Irrational.U_570_13 : Uω (aρ 13) (bρ 13) (664241383483 / 1000000000000) ≤ -(6187441800526216948877 / 5000000000000000000000)

theorem Zeta5Irrational.U_570_14 : Uω (aρ 14) (bρ 14) (664241383483 / 1000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_570_15 : Uω (aρ 15) (bρ 15) (664241383483 / 1000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_570_16 : Uω (aρ 16) (bρ 16) (664241383483 / 1000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_570 : Uρ (664241383483 / 1000000000000) ≤ -(1407853005784725932979 / 2000000000000000000000)

theorem Zeta5Irrational.U_571_1 : Uω (aρ 1) (bρ 1) (4261528693017 / 6400000000000) ≤ -(4164072279252109276981 / 10000000000000000000000)

theorem Zeta5Irrational.U_571_2 : Uω (aρ 2) (bρ 2) (4261528693017 / 6400000000000) ≤ -(1050097909525026300293 / 2500000000000000000000)

theorem Zeta5Irrational.U_571_3 : Uω (aρ 3) (bρ 3) (4261528693017 / 6400000000000) ≤ -(4273412884176880161469 / 10000000000000000000000)

theorem Zeta5Irrational.U_571_4 : Uω (aρ 4) (bρ 4) (4261528693017 / 6400000000000) ≤ -(549478980034508885777 / 1250000000000000000000)

theorem Zeta5Irrational.U_571_5 : Uω (aρ 5) (bρ 5) (4261528693017 / 6400000000000) ≤ -(4585051419903753167239 / 10000000000000000000000)

theorem Zeta5Irrational.U_571_6 : Uω (aρ 6) (bρ 6) (4261528693017 / 6400000000000) ≤ -(303907000827735205621 / 625000000000000000000)

theorem Zeta5Irrational.U_571_7 : Uω (aρ 7) (bρ 7) (4261528693017 / 6400000000000) ≤ -(65664971709746093159 / 125000000000000000000)

theorem Zeta5Irrational.U_571_8 : Uω (aρ 8) (bρ 8) (4261528693017 / 6400000000000) ≤ -(1446395180466007862889 / 2500000000000000000000)

theorem Zeta5Irrational.U_571_9 : Uω (aρ 9) (bρ 9) (4261528693017 / 6400000000000) ≤ -(324622520228389607363 / 500000000000000000000)

theorem Zeta5Irrational.U_571_10 : Uω (aρ 10) (bρ 10) (4261528693017 / 6400000000000) ≤ -(1482735833462658137863 / 2000000000000000000000)

theorem Zeta5Irrational.U_571_11 : Uω (aρ 11) (bρ 11) (4261528693017 / 6400000000000) ≤ -(4301958498077105265997 / 5000000000000000000000)

theorem Zeta5Irrational.U_571_12 : Uω (aρ 12) (bρ 12) (4261528693017 / 6400000000000) ≤ -(10156041558459248697277 / 10000000000000000000000)

theorem Zeta5Irrational.U_571_13 : Uω (aρ 13) (bρ 13) (4261528693017 / 6400000000000) ≤ -(614973329293170409787 / 500000000000000000000)

theorem Zeta5Irrational.U_571_14 : Uω (aρ 14) (bρ 14) (4261528693017 / 6400000000000) ≤ -(16967115179877088640491 / 10000000000000000000000)

theorem Zeta5Irrational.U_571_15 : Uω (aρ 15) (bρ 15) (4261528693017 / 6400000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_571_16 : Uω (aρ 16) (bρ 16) (4261528693017 / 6400000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_571 : Uρ (4261528693017 / 6400000000000) ≤ -(435371962683215891223 / 625000000000000000000)

theorem Zeta5Irrational.U_572_1 : Uω (aρ 1) (bρ 1) (10679781329357 / 16000000000000) ≤ -(2069748762339204639219 / 5000000000000000000000)

theorem Zeta5Irrational.U_572_2 : Uω (aρ 2) (bρ 2) (10679781329357 / 16000000000000) ≤ -(4175727064915972273783 / 10000000000000000000000)

theorem Zeta5Irrational.U_572_3 : Uω (aρ 3) (bρ 3) (10679781329357 / 16000000000000) ≤ -(4248566228358807393553 / 10000000000000000000000)

theorem Zeta5Irrational.U_572_4 : Uω (aρ 4) (bρ 4) (10679781329357 / 16000000000000) ≤ -(2185337678456050449133 / 5000000000000000000000)

theorem Zeta5Irrational.U_572_5 : Uω (aρ 5) (bρ 5) (10679781329357 / 16000000000000) ≤ -(2279702231101783945013 / 5000000000000000000000)

theorem Zeta5Irrational.U_572_6 : Uω (aρ 6) (bρ 6) (10679781329357 / 16000000000000) ≤ -(4836119278634238343609 / 10000000000000000000000)

theorem Zeta5Irrational.U_572_7 : Uω (aρ 7) (bρ 7) (10679781329357 / 16000000000000) ≤ -(2612848856110541349761 / 5000000000000000000000)

theorem Zeta5Irrational.U_572_8 : Uω (aρ 8) (bρ 8) (10679781329357 / 16000000000000) ≤ -(5756453563723046984991 / 10000000000000000000000)

theorem Zeta5Irrational.U_572_9 : Uω (aρ 9) (bρ 9) (10679781329357 / 16000000000000) ≤ -(3230461078330779039389 / 5000000000000000000000)

theorem Zeta5Irrational.U_572_10 : Uω (aρ 10) (bρ 10) (10679781329357 / 16000000000000) ≤ -(7378525449464564730863 / 10000000000000000000000)

theorem Zeta5Irrational.U_572_11 : Uω (aρ 11) (bρ 11) (10679781329357 / 16000000000000) ≤ -(4281499084663921275759 / 5000000000000000000000)

theorem Zeta5Irrational.U_572_12 : Uω (aρ 12) (bρ 12) (10679781329357 / 16000000000000) ≤ -(2020984027645203037053 / 2000000000000000000000)

theorem Zeta5Irrational.U_572_13 : Uω (aρ 13) (bρ 13) (10679781329357 / 16000000000000) ≤ -(12225004331939791329417 / 10000000000000000000000)

theorem Zeta5Irrational.U_572_14 : Uω (aρ 14) (bρ 14) (10679781329357 / 16000000000000) ≤ -(16558394140482642990089 / 10000000000000000000000)

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

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

theorem Zeta5Irrational.U_572 : Uρ (10679781329357 / 16000000000000) ≤ -(13837047140647643897 / 20000000000000000000)

theorem Zeta5Irrational.U_573_1 : Uω (aρ 1) (bρ 1) (21411481852343 / 32000000000000) ≤ -(4114983014388123040979 / 10000000000000000000000)

theorem Zeta5Irrational.U_573_2 : Uω (aρ 2) (bρ 2) (21411481852343 / 32000000000000) ≤ -(4151123179164884118219 / 10000000000000000000000)

theorem Zeta5Irrational.U_573_3 : Uω (aρ 3) (bρ 3) (21411481852343 / 32000000000000) ≤ -(1055945291455342745149 / 2500000000000000000000)

theorem Zeta5Irrational.U_573_4 : Uω (aρ 4) (bρ 4) (21411481852343 / 32000000000000) ≤ -(2172791015703680314347 / 5000000000000000000000)

theorem Zeta5Irrational.U_573_5 : Uω (aρ 5) (bρ 5) (21411481852343 / 32000000000000) ≤ -(4533823199721012871099 / 10000000000000000000000)

theorem Zeta5Irrational.U_573_6 : Uω (aρ 6) (bρ 6) (21411481852343 / 32000000000000) ≤ -(4809796242406969208233 / 10000000000000000000000)

theorem Zeta5Irrational.U_573_7 : Uω (aρ 7) (bρ 7) (21411481852343 / 32000000000000) ≤ -(324892103887673495129 / 625000000000000000000)

theorem Zeta5Irrational.U_573_8 : Uω (aρ 8) (bρ 8) (21411481852343 / 32000000000000) ≤ -(5727412354734878097163 / 10000000000000000000000)

theorem Zeta5Irrational.U_573_9 : Uω (aρ 9) (bρ 9) (21411481852343 / 32000000000000) ≤ -(803687038877101364811 / 1250000000000000000000)

theorem Zeta5Irrational.U_573_10 : Uω (aρ 10) (bρ 10) (21411481852343 / 32000000000000) ≤ -(1835875806775894467537 / 2500000000000000000000)

theorem Zeta5Irrational.U_573_11 : Uω (aρ 11) (bρ 11) (21411481852343 / 32000000000000) ≤ -(8522268895539115610217 / 10000000000000000000000)

theorem Zeta5Irrational.U_573_12 : Uω (aρ 12) (bρ 12) (21411481852343 / 32000000000000) ≤ -(10054132744104097026937 / 10000000000000000000000)

theorem Zeta5Irrational.U_573_13 : Uω (aρ 13) (bρ 13) (21411481852343 / 32000000000000) ≤ -(1215146544888570115507 / 1000000000000000000000)

theorem Zeta5Irrational.U_573_14 : Uω (aρ 14) (bρ 14) (21411481852343 / 32000000000000) ≤ -(8122578466833861866631 / 5000000000000000000000)

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

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

theorem Zeta5Irrational.U_573 : Uρ (21411481852343 / 32000000000000) ≤ -(3437741571450890412419 / 5000000000000000000000)

theorem Zeta5Irrational.U_574_1 : Uω (aρ 1) (bρ 1) (5365850261493 / 8000000000000) ≤ -(2045264226863557451219 / 5000000000000000000000)

theorem Zeta5Irrational.U_574_2 : Uω (aρ 2) (bρ 2) (5365850261493 / 8000000000000) ≤ -(206328984146057335773 / 500000000000000000000)

theorem Zeta5Irrational.U_574_3 : Uω (aρ 3) (bρ 3) (5365850261493 / 8000000000000) ≤ -(2099528695947786887917 / 5000000000000000000000)

theorem Zeta5Irrational.U_574_4 : Uω (aρ 4) (bρ 4) (5365850261493 / 8000000000000) ≤ -(4320551547269413483711 / 10000000000000000000000)

theorem Zeta5Irrational.U_574_5 : Uω (aρ 5) (bρ 5) (5365850261493 / 8000000000000) ≤ -(450830729631545839137 / 1000000000000000000000)

theorem Zeta5Irrational.U_574_6 : Uω (aρ 6) (bρ 6) (5365850261493 / 8000000000000) ≤ -(956708507247560145543 / 2000000000000000000000)

theorem Zeta5Irrational.U_574_7 : Uω (aρ 7) (bρ 7) (5365850261493 / 8000000000000) ≤ -(5170925165050416482019 / 10000000000000000000000)

theorem Zeta5Irrational.U_574_8 : Uω (aρ 8) (bρ 8) (5365850261493 / 8000000000000) ≤ -(356153536329907708581 / 625000000000000000000)

theorem Zeta5Irrational.U_574_9 : Uω (aρ 9) (bρ 9) (5365850261493 / 8000000000000) ≤ -(6398172183635422242973 / 10000000000000000000000)

theorem Zeta5Irrational.U_574_10 : Uω (aρ 10) (bρ 10) (5365850261493 / 8000000000000) ≤ -(7308611460365759401711 / 10000000000000000000000)

theorem Zeta5Irrational.U_574_11 : Uω (aρ 11) (bρ 11) (5365850261493 / 8000000000000) ≤ -(8481727231061772560251 / 10000000000000000000000)

theorem Zeta5Irrational.U_574_12 : Uω (aρ 12) (bρ 12) (5365850261493 / 8000000000000) ≤ -(625229637354933601691 / 625000000000000000000)

theorem Zeta5Irrational.U_574_13 : Uω (aρ 13) (bρ 13) (5365850261493 / 8000000000000) ≤ -(12078820249414143656001 / 10000000000000000000000)

theorem Zeta5Irrational.U_574_14 : Uω (aρ 14) (bρ 14) (5365850261493 / 8000000000000) ≤ -(1598140732969455004503 / 1000000000000000000000)

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

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

theorem Zeta5Irrational.U_574 : Uρ (5365850261493 / 8000000000000) ≤ -(3417392158413140254523 / 5000000000000000000000)

theorem Zeta5Irrational.U_575_1 : Uω (aρ 1) (bρ 1) (21515320239601 / 32000000000000) ≤ -(1016533387549429410351 / 2500000000000000000000)

theorem Zeta5Irrational.U_575_2 : Uω (aρ 2) (bρ 2) (21515320239601 / 32000000000000) ≤ -(4102096280447662030521 / 10000000000000000000000)

theorem Zeta5Irrational.U_575_3 : Uω (aρ 3) (bρ 3) (21515320239601 / 32000000000000) ≤ -(4174394604167777532657 / 10000000000000000000000)

theorem Zeta5Irrational.U_575_4 : Uω (aρ 4) (bρ 4) (21515320239601 / 32000000000000) ≤ -(4295583590380036756359 / 10000000000000000000000)

theorem Zeta5Irrational.U_575_5 : Uω (aρ 5) (bρ 5) (21515320239601 / 32000000000000) ≤ -(448285641842292237797 / 1000000000000000000000)

theorem Zeta5Irrational.U_575_6 : Uω (aρ 6) (bρ 6) (21515320239601 / 32000000000000) ≤ -(594669724340460638439 / 1250000000000000000000)

theorem Zeta5Irrational.U_575_7 : Uω (aρ 7) (bρ 7) (21515320239601 / 32000000000000) ≤ -(102873036052304889857 / 200000000000000000000)

theorem Zeta5Irrational.U_575_8 : Uω (aρ 8) (bρ 8) (21515320239601 / 32000000000000) ≤ -(708698216798880485127 / 1250000000000000000000)

theorem Zeta5Irrational.U_575_9 : Uω (aρ 9) (bρ 9) (21515320239601 / 32000000000000) ≤ -(198967159298271784199 / 312500000000000000000)

theorem Zeta5Irrational.U_575_10 : Uω (aρ 10) (bρ 10) (21515320239601 / 32000000000000) ≤ -(290953964891705276277 / 400000000000000000000)

theorem Zeta5Irrational.U_575_11 : Uω (aρ 11) (bρ 11) (21515320239601 / 32000000000000) ≤ -(4220685632138396378261 / 5000000000000000000000)

theorem Zeta5Irrational.U_575_12 : Uω (aρ 12) (bρ 12) (21515320239601 / 32000000000000) ≤ -(9953539452871187747641 / 10000000000000000000000)

theorem Zeta5Irrational.U_575_13 : Uω (aρ 13) (bρ 13) (21515320239601 / 32000000000000) ≤ -(6003520311026841393907 / 5000000000000000000000)

theorem Zeta5Irrational.U_575_14 : Uω (aρ 14) (bρ 14) (21515320239601 / 32000000000000) ≤ -(15749320931358898036187 / 10000000000000000000000)

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

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

theorem Zeta5Irrational.U_575 : Uρ (21515320239601 / 32000000000000) ≤ -(5436506260804101737 / 8000000000000000000)

theorem Zeta5Irrational.U_576_1 : Uω (aρ 1) (bρ 1) (43082559672831 / 64000000000000) ≤ -(2026979189518170120827 / 5000000000000000000000)

theorem Zeta5Irrational.U_576_2 : Uω (aρ 2) (bρ 2) (43082559672831 / 64000000000000) ≤ -(2044938511275047845963 / 5000000000000000000000)

theorem Zeta5Irrational.U_576_3 : Uω (aρ 3) (bρ 3) (43082559672831 / 64000000000000) ≤ -(4162085986235097085897 / 10000000000000000000000)

theorem Zeta5Irrational.U_576_4 : Uω (aρ 4) (bρ 4) (43082559672831 / 64000000000000) ≤ -(4283122962134978443037 / 10000000000000000000000)

theorem Zeta5Irrational.U_576_5 : Uω (aρ 5) (bρ 5) (43082559672831 / 64000000000000) ≤ -(4470155260503364583741 / 10000000000000000000000)

theorem Zeta5Irrational.U_576_6 : Uω (aρ 6) (bρ 6) (43082559672831 / 64000000000000) ≤ -(1186072793078736166699 / 2500000000000000000000)

theorem Zeta5Irrational.U_576_7 : Uω (aρ 7) (bρ 7) (43082559672831 / 64000000000000) ≤ -(128251079179985541609 / 250000000000000000000)

theorem Zeta5Irrational.U_576_8 : Uω (aρ 8) (bρ 8) (43082559672831 / 64000000000000) ≤ -(2827591000309687841803 / 5000000000000000000000)

theorem Zeta5Irrational.U_576_9 : Uω (aρ 9) (bρ 9) (43082559672831 / 64000000000000) ≤ -(3175687617663083390177 / 5000000000000000000000)

theorem Zeta5Irrational.U_576_10 : Uω (aρ 10) (bρ 10) (43082559672831 / 64000000000000) ≤ -(3628258085777660704223 / 5000000000000000000000)

theorem Zeta5Irrational.U_576_11 : Uω (aρ 11) (bρ 11) (43082559672831 / 64000000000000) ≤ -(4210631164367377930677 / 5000000000000000000000)

theorem Zeta5Irrational.U_576_12 : Uω (aρ 12) (bρ 12) (43082559672831 / 64000000000000) ≤ -(7756712472024757971 / 7812500000000000000)

theorem Zeta5Irrational.U_576_13 : Uω (aρ 13) (bρ 13) (43082559672831 / 64000000000000) ≤ -(5985733507685321610093 / 5000000000000000000000)

theorem Zeta5Irrational.U_576_14 : Uω (aρ 14) (bρ 14) (43082559672831 / 64000000000000) ≤ -(15642119863862916581919 / 10000000000000000000000)

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

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

theorem Zeta5Irrational.U_576 : Uρ (43082559672831 / 64000000000000) ≤ -(211765684898012963771 / 312500000000000000000)

theorem Zeta5Irrational.U_577_1 : Uω (aρ 1) (bρ 1) (2156723943323 / 3200000000000) ≤ -(4041798013437740677517 / 10000000000000000000000)

theorem Zeta5Irrational.U_577_2 : Uω (aρ 2) (bρ 2) (2156723943323 / 3200000000000) ≤ -(254854542385908595437 / 625000000000000000000)

theorem Zeta5Irrational.U_577_3 : Uω (aρ 3) (bρ 3) (2156723943323 / 3200000000000) ≤ -(4149792502457496461927 / 10000000000000000000000)

theorem Zeta5Irrational.U_577_4 : Uω (aρ 4) (bρ 4) (2156723943323 / 3200000000000) ≤ -(4270677848971521522911 / 10000000000000000000000)

theorem Zeta5Irrational.U_577_5 : Uω (aρ 5) (bρ 5) (2156723943323 / 3200000000000) ≤ -(4457470235029769292473 / 10000000000000000000000)

theorem Zeta5Irrational.U_577_6 : Uω (aρ 6) (bρ 6) (2156723943323 / 3200000000000) ≤ -(2365620827675887082541 / 5000000000000000000000)

theorem Zeta5Irrational.U_577_7 : Uω (aρ 7) (bρ 7) (2156723943323 / 3200000000000) ≤ -(1279113290058657057013 / 2500000000000000000000)

theorem Zeta5Irrational.U_577_8 : Uω (aρ 8) (bρ 8) (2156723943323 / 3200000000000) ≤ -(1128159861942127147153 / 2000000000000000000000)

theorem Zeta5Irrational.U_577_9 : Uω (aρ 9) (bρ 9) (2156723943323 / 3200000000000) ≤ -(6335826382699116403269 / 10000000000000000000000)

theorem Zeta5Irrational.U_577_10 : Uω (aρ 10) (bρ 10) (2156723943323 / 3200000000000) ≤ -(3619607599305394259193 / 5000000000000000000000)

theorem Zeta5Irrational.U_577_11 : Uω (aρ 11) (bρ 11) (2156723943323 / 3200000000000) ≤ -(4200599557466197558131 / 5000000000000000000000)

theorem Zeta5Irrational.U_577_12 : Uω (aρ 12) (bρ 12) (2156723943323 / 3200000000000) ≤ -(1980744718241945239729 / 2000000000000000000000)

theorem Zeta5Irrational.U_577_13 : Uω (aρ 13) (bρ 13) (2156723943323 / 3200000000000) ≤ -(596804995792744646391 / 500000000000000000000)

theorem Zeta5Irrational.U_577_14 : Uω (aρ 14) (bρ 14) (2156723943323 / 3200000000000) ≤ -(3884938065980386746899 / 2500000000000000000000)

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

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

theorem Zeta5Irrational.U_577 : Uρ (2156723943323 / 3200000000000) ≤ -(6757620034057452785879 / 10000000000000000000000)

theorem Zeta5Irrational.U_578_1 : Uω (aρ 1) (bρ 1) (43186398060089 / 64000000000000) ≤ -(4029652417436910217643 / 10000000000000000000000)

theorem Zeta5Irrational.U_578_2 : Uω (aρ 2) (bρ 2) (43186398060089 / 64000000000000) ≤ -(4065483210959910322499 / 10000000000000000000000)

theorem Zeta5Irrational.U_578_3 : Uω (aρ 3) (bρ 3) (43186398060089 / 64000000000000) ≤ -(4137514115657745432343 / 10000000000000000000000)

theorem Zeta5Irrational.U_578_4 : Uω (aρ 4) (bρ 4) (43186398060089 / 64000000000000) ≤ -(2129124106141065259827 / 5000000000000000000000)

theorem Zeta5Irrational.U_578_5 : Uω (aρ 5) (bρ 5) (43186398060089 / 64000000000000) ≤ -(1111200325254916125143 / 2500000000000000000000)

theorem Zeta5Irrational.U_578_6 : Uω (aρ 6) (bρ 6) (43186398060089 / 64000000000000) ≤ -(1179552299741664472367 / 2500000000000000000000)

theorem Zeta5Irrational.U_578_7 : Uω (aρ 7) (bρ 7) (43186398060089 / 64000000000000) ≤ -(5102881730426360024451 / 10000000000000000000000)

theorem Zeta5Irrational.U_578_8 : Uω (aρ 8) (bρ 8) (43186398060089 / 64000000000000) ≤ -(1125287519865866481021 / 2000000000000000000000)

theorem Zeta5Irrational.U_578_9 : Uω (aρ 9) (bρ 9) (43186398060089 / 64000000000000) ≤ -(6320302456974391084841 / 10000000000000000000000)

theorem Zeta5Irrational.U_578_10 : Uω (aρ 10) (bρ 10) (43186398060089 / 64000000000000) ≤ -(3610973039310716154581 / 5000000000000000000000)

theorem Zeta5Irrational.U_578_11 : Uω (aρ 11) (bρ 11) (43186398060089 / 64000000000000) ≤ -(8381181392621563129199 / 10000000000000000000000)

theorem Zeta5Irrational.U_578_12 : Uω (aρ 12) (bρ 12) (43186398060089 / 64000000000000) ≤ -(9878933738315134485679 / 10000000000000000000000)

theorem Zeta5Irrational.U_578_13 : Uω (aρ 13) (bρ 13) (43186398060089 / 64000000000000) ≤ -(2975234050794647865737 / 2500000000000000000000)

theorem Zeta5Irrational.U_578_14 : Uω (aρ 14) (bρ 14) (43186398060089 / 64000000000000) ≤ -(15441627376211997410399 / 10000000000000000000000)

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

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

theorem Zeta5Irrational.U_578 : Uρ (43186398060089 / 64000000000000) ≤ -(6738960652673771386763 / 10000000000000000000000)

theorem Zeta5Irrational.U_579_1 : Uω (aρ 1) (bρ 1) (21619158626859 / 32000000000000) ≤ -(2008760777599865418403 / 5000000000000000000000)

theorem Zeta5Irrational.U_579_2 : Uω (aρ 2) (bρ 2) (21619158626859 / 32000000000000) ≤ -(506663573084745193583 / 1250000000000000000000)

theorem Zeta5Irrational.U_579_3 : Uω (aρ 3) (bρ 3) (21619158626859 / 32000000000000) ≤ -(4125250788795458835007 / 10000000000000000000000)

theorem Zeta5Irrational.U_579_4 : Uω (aρ 4) (bρ 4) (21619158626859 / 32000000000000) ≤ -(2122917006801633900917 / 5000000000000000000000)

theorem Zeta5Irrational.U_579_5 : Uω (aρ 5) (bρ 5) (21619158626859 / 32000000000000) ≤ -(1108037104411686499443 / 2500000000000000000000)

theorem Zeta5Irrational.U_579_6 : Uω (aρ 6) (bρ 6) (21619158626859 / 32000000000000) ≤ -(4705193758468929470479 / 10000000000000000000000)

theorem Zeta5Irrational.U_579_7 : Uω (aρ 7) (bρ 7) (21619158626859 / 32000000000000) ≤ -(508932882669316172813 / 1000000000000000000000)

theorem Zeta5Irrational.U_579_8 : Uω (aρ 8) (bρ 8) (21619158626859 / 32000000000000) ≤ -(5612096807420582264481 / 10000000000000000000000)

theorem Zeta5Irrational.U_579_9 : Uω (aρ 9) (bρ 9) (21619158626859 / 32000000000000) ≤ -(6304803375883815152733 / 10000000000000000000000)

theorem Zeta5Irrational.U_579_10 : Uω (aρ 10) (bρ 10) (21619158626859 / 32000000000000) ≤ -(1440941737503140562409 / 2000000000000000000000)

theorem Zeta5Irrational.U_579_11 : Uω (aρ 11) (bρ 11) (21619158626859 / 32000000000000) ≤ -(4180604466712982170821 / 5000000000000000000000)

theorem Zeta5Irrational.U_579_12 : Uω (aρ 12) (bρ 12) (21619158626859 / 32000000000000) ≤ -(9854221817320635336431 / 10000000000000000000000)

theorem Zeta5Irrational.U_579_13 : Uω (aρ 13) (bρ 13) (21619158626859 / 32000000000000) ≤ -(741623302233828881753 / 625000000000000000000)

theorem Zeta5Irrational.U_579_14 : Uω (aρ 14) (bρ 14) (21619158626859 / 32000000000000) ≤ -(15347266115033912343549 / 10000000000000000000000)

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

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

theorem Zeta5Irrational.U_579 : Uρ (21619158626859 / 32000000000000) ≤ -(6720502213295018558049 / 10000000000000000000000)