Certified arcsine potential bounds (U48)

theorem Zeta5Irrational.U_580_1 : Uω (aρ 1) (bρ 1) (43290236447347 / 64000000000000) ≤ -(4005405391022337117569 / 10000000000000000000000)

theorem Zeta5Irrational.U_580_2 : Uω (aρ 2) (bρ 2) (43290236447347 / 64000000000000) ≤ -(2020574381616309005321 / 5000000000000000000000)

theorem Zeta5Irrational.U_580_3 : Uω (aρ 3) (bρ 3) (43290236447347 / 64000000000000) ≤ -(4113002484966424445947 / 10000000000000000000000)

theorem Zeta5Irrational.U_580_4 : Uω (aρ 4) (bρ 4) (43290236447347 / 64000000000000) ≤ -(1058358803653668769017 / 2500000000000000000000)

theorem Zeta5Irrational.U_580_5 : Uω (aρ 5) (bρ 5) (43290236447347 / 64000000000000) ≤ -(220975577212004283547 / 500000000000000000000)

theorem Zeta5Irrational.U_580_6 : Uω (aρ 6) (bρ 6) (43290236447347 / 64000000000000) ≤ -(4692195289343839263543 / 10000000000000000000000)

theorem Zeta5Irrational.U_580_7 : Uω (aρ 7) (bρ 7) (43290236447347 / 64000000000000) ≤ -(5075794398165442137843 / 10000000000000000000000)

theorem Zeta5Irrational.U_580_8 : Uω (aρ 8) (bρ 8) (43290236447347 / 64000000000000) ≤ -(1399444218052103159183 / 2500000000000000000000)

theorem Zeta5Irrational.U_580_9 : Uω (aρ 9) (bρ 9) (43290236447347 / 64000000000000) ≤ -(6289329057577266237567 / 10000000000000000000000)

theorem Zeta5Irrational.U_580_10 : Uω (aρ 10) (bρ 10) (43290236447347 / 64000000000000) ≤ -(7187502901981604046617 / 10000000000000000000000)

theorem Zeta5Irrational.U_580_11 : Uω (aρ 11) (bρ 11) (43290236447347 / 64000000000000) ≤ -(8341281510819861628441 / 10000000000000000000000)

theorem Zeta5Irrational.U_580_12 : Uω (aρ 12) (bρ 12) (43290236447347 / 64000000000000) ≤ -(4914793623665919405137 / 5000000000000000000000)

theorem Zeta5Irrational.U_580_13 : Uω (aρ 13) (bρ 13) (43290236447347 / 64000000000000) ≤ -(11831206847900431713959 / 10000000000000000000000)

theorem Zeta5Irrational.U_580_14 : Uω (aρ 14) (bρ 14) (43290236447347 / 64000000000000) ≤ -(7628136779712544570147 / 5000000000000000000000)

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

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

theorem Zeta5Irrational.U_580 : Uρ (43290236447347 / 64000000000000) ≤ -(837778362582075301389 / 1250000000000000000000)

theorem Zeta5Irrational.U_581_1 : Uω (aρ 1) (bρ 1) (2708884727561 / 4000000000000) ≤ -(3993303889330489471621 / 10000000000000000000000)

theorem Zeta5Irrational.U_581_2 : Uω (aρ 2) (bρ 2) (2708884727561 / 4000000000000) ≤ -(4029003710659338433683 / 10000000000000000000000)

theorem Zeta5Irrational.U_581_3 : Uω (aρ 3) (bρ 3) (2708884727561 / 4000000000000) ≤ -(4100769167401937979183 / 10000000000000000000000)

theorem Zeta5Irrational.U_581_4 : Uω (aρ 4) (bρ 4) (2708884727561 / 4000000000000) ≤ -(4221051777138668487973 / 10000000000000000000000)

theorem Zeta5Irrational.U_581_5 : Uω (aρ 5) (bρ 5) (2708884727561 / 4000000000000) ≤ -(4406890640283341706941 / 10000000000000000000000)

theorem Zeta5Irrational.U_581_6 : Uω (aρ 6) (bρ 6) (2708884727561 / 4000000000000) ≤ -(292450859203226838757 / 625000000000000000000)

theorem Zeta5Irrational.U_581_7 : Uω (aρ 7) (bρ 7) (2708884727561 / 4000000000000) ≤ -(2531139197092148791153 / 5000000000000000000000)

theorem Zeta5Irrational.U_581_8 : Uω (aρ 8) (bρ 8) (2708884727561 / 4000000000000) ≤ -(5583477732194065256547 / 10000000000000000000000)

theorem Zeta5Irrational.U_581_9 : Uω (aρ 9) (bρ 9) (2708884727561 / 4000000000000) ≤ -(1568469855154944946347 / 2500000000000000000000)

theorem Zeta5Irrational.U_581_10 : Uω (aρ 10) (bρ 10) (2708884727561 / 4000000000000) ≤ -(7170328599460265511283 / 10000000000000000000000)

theorem Zeta5Irrational.U_581_11 : Uω (aρ 11) (bρ 11) (2708884727561 / 4000000000000) ≤ -(8321398900107086323937 / 10000000000000000000000)

theorem Zeta5Irrational.U_581_12 : Uω (aρ 12) (bρ 12) (2708884727561 / 4000000000000) ≤ -(39220117818480693483 / 40000000000000000000)

theorem Zeta5Irrational.U_581_13 : Uω (aρ 13) (bρ 13) (2708884727561 / 4000000000000) ≤ -(11796635347326533752359 / 10000000000000000000000)

theorem Zeta5Irrational.U_581_14 : Uω (aρ 14) (bρ 14) (2708884727561 / 4000000000000) ≤ -(1516831959140549096717 / 1000000000000000000000)

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

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

theorem Zeta5Irrational.U_581 : Uρ (2708884727561 / 4000000000000) ≤ -(41775748645483768217 / 62500000000000000000)

theorem Zeta5Irrational.U_582_1 : Uω (aρ 1) (bρ 1) (8678814966921 / 12800000000000) ≤ -(497652126834867869363 / 1250000000000000000000)

theorem Zeta5Irrational.U_582_2 : Uω (aρ 2) (bρ 2) (8678814966921 / 12800000000000) ≤ -(4016873391124482683507 / 10000000000000000000000)

theorem Zeta5Irrational.U_582_3 : Uω (aρ 3) (bρ 3) (8678814966921 / 12800000000000) ≤ -(4088550799468137633081 / 10000000000000000000000)

theorem Zeta5Irrational.U_582_4 : Uω (aρ 4) (bρ 4) (8678814966921 / 12800000000000) ≤ -(4208683663139425892631 / 10000000000000000000000)

theorem Zeta5Irrational.U_582_5 : Uω (aρ 5) (bρ 5) (8678814966921 / 12800000000000) ≤ -(549285708176747111411 / 1250000000000000000000)

theorem Zeta5Irrational.U_582_6 : Uω (aρ 6) (bρ 6) (8678814966921 / 12800000000000) ≤ -(466624908802661578893 / 1000000000000000000000)

theorem Zeta5Irrational.U_582_7 : Uω (aρ 7) (bρ 7) (8678814966921 / 12800000000000) ≤ -(631097595537542197029 / 1250000000000000000000)

theorem Zeta5Irrational.U_582_8 : Uω (aρ 8) (bρ 8) (8678814966921 / 12800000000000) ≤ -(1392299831538579844629 / 2500000000000000000000)

theorem Zeta5Irrational.U_582_9 : Uω (aρ 9) (bρ 9) (8678814966921 / 12800000000000) ≤ -(6258454383988677137099 / 10000000000000000000000)

theorem Zeta5Irrational.U_582_10 : Uω (aρ 10) (bρ 10) (8678814966921 / 12800000000000) ≤ -(447074103633723834573 / 625000000000000000000)

theorem Zeta5Irrational.U_582_11 : Uω (aρ 11) (bρ 11) (8678814966921 / 12800000000000) ≤ -(518847554900022932309 / 625000000000000000000)

theorem Zeta5Irrational.U_582_12 : Uω (aρ 12) (bρ 12) (8678814966921 / 12800000000000) ≤ -(9780547872498677856713 / 10000000000000000000000)

theorem Zeta5Irrational.U_582_13 : Uω (aρ 13) (bρ 13) (8678814966921 / 12800000000000) ≤ -(5881127756237673751163 / 5000000000000000000000)

theorem Zeta5Irrational.U_582_14 : Uω (aρ 14) (bρ 14) (8678814966921 / 12800000000000) ≤ -(3770781227787045933889 / 2500000000000000000000)

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

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

theorem Zeta5Irrational.U_582 : Uρ (8678814966921 / 12800000000000) ≤ -(1333233638414966829353 / 2000000000000000000000)

theorem Zeta5Irrational.U_583_1 : Uω (aρ 1) (bρ 1) (21722997014117 / 32000000000000) ≤ -(1984572365875415154351 / 5000000000000000000000)

theorem Zeta5Irrational.U_583_2 : Uω (aρ 2) (bρ 2) (21722997014117 / 32000000000000) ≤ -(4004757768924670619983 / 10000000000000000000000)

theorem Zeta5Irrational.U_583_3 : Uω (aρ 3) (bρ 3) (21722997014117 / 32000000000000) ≤ -(815269468933069742969 / 2000000000000000000000)

theorem Zeta5Irrational.U_583_4 : Uω (aρ 4) (bρ 4) (21722997014117 / 32000000000000) ≤ -(2098165417361143833627 / 5000000000000000000000)

theorem Zeta5Irrational.U_583_5 : Uω (aρ 5) (bρ 5) (21722997014117 / 32000000000000) ≤ -(4381696579422479512909 / 10000000000000000000000)

theorem Zeta5Irrational.U_583_6 : Uω (aρ 6) (bρ 6) (21722997014117 / 32000000000000) ≤ -(4653301267676273408001 / 10000000000000000000000)

theorem Zeta5Irrational.U_583_7 : Uω (aρ 7) (bρ 7) (21722997014117 / 32000000000000) ≤ -(1258825364568131694757 / 2500000000000000000000)

theorem Zeta5Irrational.U_583_8 : Uω (aρ 8) (bρ 8) (21722997014117 / 32000000000000) ≤ -(1388735398284956359487 / 2500000000000000000000)

theorem Zeta5Irrational.U_583_9 : Uω (aρ 9) (bρ 9) (21722997014117 / 32000000000000) ≤ -(6243053867070716944753 / 10000000000000000000000)

theorem Zeta5Irrational.U_583_10 : Uω (aρ 10) (bρ 10) (21722997014117 / 32000000000000) ≤ -(7136073956947920528813 / 10000000000000000000000)

theorem Zeta5Irrational.U_583_11 : Uω (aρ 11) (bρ 11) (21722997014117 / 32000000000000) ≤ -(8281767224600949070467 / 10000000000000000000000)

theorem Zeta5Irrational.U_583_12 : Uω (aρ 12) (bρ 12) (21722997014117 / 32000000000000) ≤ -(9756141941200541419451 / 10000000000000000000000)

theorem Zeta5Irrational.U_583_13 : Uω (aρ 13) (bρ 13) (21722997014117 / 32000000000000) ≤ -(586403229508580354881 / 500000000000000000000)

theorem Zeta5Irrational.U_583_14 : Uω (aρ 14) (bρ 14) (21722997014117 / 32000000000000) ≤ -(3000090141854125438813 / 2000000000000000000000)

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

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

theorem Zeta5Irrational.U_583 : Uρ (21722997014117 / 32000000000000) ≤ -(3324180630720396764653 / 5000000000000000000000)

theorem Zeta5Irrational.U_584_1 : Uω (aρ 1) (bρ 1) (43497913221863 / 64000000000000) ≤ -(3957087005357036086949 / 10000000000000000000000)

theorem Zeta5Irrational.U_584_2 : Uω (aρ 2) (bρ 2) (43497913221863 / 64000000000000) ≤ -(1996328404243077264093 / 5000000000000000000000)

theorem Zeta5Irrational.U_584_3 : Uω (aρ 3) (bρ 3) (43497913221863 / 64000000000000) ≤ -(4064158766627427001413 / 10000000000000000000000)

theorem Zeta5Irrational.U_584_4 : Uω (aρ 4) (bρ 4) (43497913221863 / 64000000000000) ≤ -(167359730165322291151 / 400000000000000000000)

theorem Zeta5Irrational.U_584_5 : Uω (aρ 5) (bρ 5) (43497913221863 / 64000000000000) ≤ -(4369123342251587632137 / 10000000000000000000000)

theorem Zeta5Irrational.U_584_6 : Uω (aρ 6) (bρ 6) (43497913221863 / 64000000000000) ≤ -(1160092560595083378649 / 2500000000000000000000)

theorem Zeta5Irrational.U_584_7 : Uω (aρ 7) (bρ 7) (43497913221863 / 64000000000000) ≤ -(5021840426067032372317 / 10000000000000000000000)

theorem Zeta5Irrational.U_584_8 : Uω (aρ 8) (bρ 8) (43497913221863 / 64000000000000) ≤ -(2770352236236726762283 / 5000000000000000000000)

theorem Zeta5Irrational.U_584_9 : Uω (aρ 9) (bρ 9) (43497913221863 / 64000000000000) ≤ -(6227677789659275289543 / 10000000000000000000000)

theorem Zeta5Irrational.U_584_10 : Uω (aρ 10) (bρ 10) (43497913221863 / 64000000000000) ≤ -(7118993375547906127047 / 10000000000000000000000)

theorem Zeta5Irrational.U_584_11 : Uω (aρ 11) (bρ 11) (43497913221863 / 64000000000000) ≤ -(1652403543875702179933 / 2000000000000000000000)

theorem Zeta5Irrational.U_584_12 : Uω (aρ 12) (bρ 12) (43497913221863 / 64000000000000) ≤ -(9731811107760359174813 / 10000000000000000000000)

theorem Zeta5Irrational.U_584_13 : Uω (aρ 13) (bρ 13) (43497913221863 / 64000000000000) ≤ -(11694059893297898993841 / 10000000000000000000000)

theorem Zeta5Irrational.U_584_14 : Uω (aρ 14) (bρ 14) (43497913221863 / 64000000000000) ≤ -(14920090891057678189429 / 10000000000000000000000)

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

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

theorem Zeta5Irrational.U_584 : Uρ (43497913221863 / 64000000000000) ≤ -(663068958368421010261 / 1000000000000000000000)

theorem Zeta5Irrational.U_585_1 : Uω (aρ 1) (bρ 1) (10887458103873 / 16000000000000) ≤ -(986260950108896607393 / 2500000000000000000000)

theorem Zeta5Irrational.U_585_2 : Uω (aρ 2) (bρ 2) (10887458103873 / 16000000000000) ≤ -(995142618591047904077 / 2500000000000000000000)

theorem Zeta5Irrational.U_585_3 : Uω (aρ 3) (bρ 3) (10887458103873 / 16000000000000) ≤ -(4051985029121106850783 / 10000000000000000000000)

theorem Zeta5Irrational.U_585_4 : Uω (aρ 4) (bρ 4) (10887458103873 / 16000000000000) ≤ -(1042917720939327110799 / 2500000000000000000000)

theorem Zeta5Irrational.U_585_5 : Uω (aρ 5) (bρ 5) (10887458103873 / 16000000000000) ≤ -(4356565913995524418331 / 10000000000000000000000)

theorem Zeta5Irrational.U_585_6 : Uω (aρ 6) (bρ 6) (10887458103873 / 16000000000000) ≤ -(4627455968489878491293 / 10000000000000000000000)

theorem Zeta5Irrational.U_585_7 : Uω (aρ 7) (bρ 7) (10887458103873 / 16000000000000) ≤ -(500839761785607599 / 1000000000000000000)

theorem Zeta5Irrational.U_585_8 : Uω (aρ 8) (bρ 8) (10887458103873 / 16000000000000) ≤ -(2763243951874325661233 / 5000000000000000000000)

theorem Zeta5Irrational.U_585_9 : Uω (aρ 9) (bρ 9) (10887458103873 / 16000000000000) ≤ -(6212326071951551424699 / 10000000000000000000000)

theorem Zeta5Irrational.U_585_10 : Uω (aρ 10) (bρ 10) (10887458103873 / 16000000000000) ≤ -(443871487145641250981 / 625000000000000000000)

theorem Zeta5Irrational.U_585_11 : Uω (aρ 11) (bρ 11) (10887458103873 / 16000000000000) ≤ -(257572254535980578843 / 312500000000000000000)

theorem Zeta5Irrational.U_585_12 : Uω (aρ 12) (bρ 12) (10887458103873 / 16000000000000) ≤ -(9707554825897988957459 / 10000000000000000000000)

theorem Zeta5Irrational.U_585_13 : Uω (aρ 13) (bρ 13) (10887458103873 / 16000000000000) ≤ -(11660238798583253649693 / 10000000000000000000000)

theorem Zeta5Irrational.U_585_14 : Uω (aρ 14) (bρ 14) (10887458103873 / 16000000000000) ≤ -(14841866121726024649593 / 10000000000000000000000)

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

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

theorem Zeta5Irrational.U_585 : Uρ (10887458103873 / 16000000000000) ≤ -(6613144944372741958823 / 10000000000000000000000)

theorem Zeta5Irrational.U_586_1 : Uω (aρ 1) (bρ 1) (43601751609121 / 64000000000000) ≤ -(1966507541025517927749 / 5000000000000000000000)

theorem Zeta5Irrational.U_586_2 : Uω (aρ 2) (bρ 2) (43601751609121 / 64000000000000) ≤ -(158739949249696931061 / 400000000000000000000)

theorem Zeta5Irrational.U_586_3 : Uω (aρ 3) (bρ 3) (43601751609121 / 64000000000000) ≤ -(4039826096045358521497 / 10000000000000000000000)

theorem Zeta5Irrational.U_586_4 : Uω (aρ 4) (bρ 4) (43601751609121 / 64000000000000) ≤ -(1039840921529924137879 / 2500000000000000000000)

theorem Zeta5Irrational.U_586_5 : Uω (aρ 5) (bρ 5) (43601751609121 / 64000000000000) ≤ -(4344024254899230569613 / 10000000000000000000000)

theorem Zeta5Irrational.U_586_6 : Uω (aρ 6) (bρ 6) (43601751609121 / 64000000000000) ≤ -(4614558402526447368687 / 10000000000000000000000)

theorem Zeta5Irrational.U_586_7 : Uω (aρ 7) (bρ 7) (43601751609121 / 64000000000000) ≤ -(998994596803359351861 / 2000000000000000000000)

theorem Zeta5Irrational.U_586_8 : Uω (aρ 8) (bρ 8) (43601751609121 / 64000000000000) ≤ -(2756145913413908321303 / 5000000000000000000000)

theorem Zeta5Irrational.U_586_9 : Uω (aρ 9) (bρ 9) (43601751609121 / 64000000000000) ≤ -(774624829318223816123 / 1250000000000000000000)

theorem Zeta5Irrational.U_586_10 : Uω (aρ 10) (bρ 10) (43601751609121 / 64000000000000) ≤ -(3542462547203858067021 / 5000000000000000000000)

theorem Zeta5Irrational.U_586_11 : Uω (aρ 11) (bρ 11) (43601751609121 / 64000000000000) ≤ -(8222650286067020655741 / 10000000000000000000000)

theorem Zeta5Irrational.U_586_12 : Uω (aρ 12) (bρ 12) (43601751609121 / 64000000000000) ≤ -(591026156976621987 / 610351562500000000)

theorem Zeta5Irrational.U_586_13 : Uω (aρ 13) (bρ 13) (43601751609121 / 64000000000000) ≤ -(11626598744486248832609 / 10000000000000000000000)

theorem Zeta5Irrational.U_586_14 : Uω (aρ 14) (bρ 14) (43601751609121 / 64000000000000) ≤ -(7382809598534463882491 / 5000000000000000000000)

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

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

theorem Zeta5Irrational.U_586 : Uρ (43601751609121 / 64000000000000) ≤ -(329786005827769626429 / 500000000000000000000)

theorem Zeta5Irrational.U_587_1 : Uω (aρ 1) (bρ 1) (174614683211 / 256000000000) ≤ -(1960500407696928441209 / 5000000000000000000000)

theorem Zeta5Irrational.U_587_2 : Uω (aρ 2) (bρ 2) (174614683211 / 256000000000) ≤ -(3956441543932251401597 / 10000000000000000000000)

theorem Zeta5Irrational.U_587_3 : Uω (aρ 3) (bρ 3) (174614683211 / 256000000000) ≤ -(2013840965715370581603 / 5000000000000000000000)

theorem Zeta5Irrational.U_587_4 : Uω (aρ 4) (bρ 4) (174614683211 / 256000000000) ≤ -(4147071623883270545931 / 10000000000000000000000)

theorem Zeta5Irrational.U_587_5 : Uω (aρ 5) (bρ 5) (174614683211 / 256000000000) ≤ -(866299665071521699251 / 2000000000000000000000)

theorem Zeta5Irrational.U_587_6 : Uω (aρ 6) (bρ 6) (174614683211 / 256000000000) ≤ -(4601677501181152033433 / 10000000000000000000000)

theorem Zeta5Irrational.U_587_7 : Uω (aρ 7) (bρ 7) (174614683211 / 256000000000) ≤ -(1245391618782531133827 / 2500000000000000000000)

theorem Zeta5Irrational.U_587_8 : Uω (aρ 8) (bρ 8) (174614683211 / 256000000000) ≤ -(2749058090920340042383 / 5000000000000000000000)

theorem Zeta5Irrational.U_587_9 : Uω (aρ 9) (bρ 9) (174614683211 / 256000000000) ≤ -(6181695398438540011231 / 10000000000000000000000)

theorem Zeta5Irrational.U_587_10 : Uω (aρ 10) (bρ 10) (174614683211 / 256000000000) ≤ -(7067937157608990501517 / 10000000000000000000000)

theorem Zeta5Irrational.U_587_11 : Uω (aρ 11) (bρ 11) (174614683211 / 256000000000) ≤ -(1640606385596563904279 / 2000000000000000000000)

theorem Zeta5Irrational.U_587_12 : Uω (aρ 12) (bρ 12) (174614683211 / 256000000000) ≤ -(965926376453343920951 / 1000000000000000000000)

theorem Zeta5Irrational.U_587_13 : Uω (aρ 13) (bρ 13) (174614683211 / 256000000000) ≤ -(724571076822981242243 / 625000000000000000000)

theorem Zeta5Irrational.U_587_14 : Uω (aρ 14) (bρ 14) (174614683211 / 256000000000) ≤ -(7345605697896120243709 / 5000000000000000000000)

theorem Zeta5Irrational.U_587_15 : Uω (aρ 15) (bρ 15) (174614683211 / 256000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_587_16 : Uω (aρ 16) (bρ 16) (174614683211 / 256000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_587 : Uρ (174614683211 / 256000000000) ≤ -(1644602174649657013571 / 2500000000000000000000)

theorem Zeta5Irrational.U_588_1 : Uω (aρ 1) (bρ 1) (43705589996379 / 64000000000000) ≤ -(39090009657798394581 / 100000000000000000000)

theorem Zeta5Irrational.U_588_2 : Uω (aρ 2) (bρ 2) (43705589996379 / 64000000000000) ≤ -(394439887737222588027 / 1000000000000000000000)

theorem Zeta5Irrational.U_588_3 : Uω (aρ 3) (bρ 3) (43705589996379 / 64000000000000) ≤ -(4015552499438766461231 / 10000000000000000000000)

theorem Zeta5Irrational.U_588_4 : Uω (aρ 4) (bρ 4) (43705589996379 / 64000000000000) ≤ -(413479465984879583207 / 1000000000000000000000)

theorem Zeta5Irrational.U_588_5 : Uω (aρ 5) (bρ 5) (43705589996379 / 64000000000000) ≤ -(539873510739345538629 / 1250000000000000000000)

theorem Zeta5Irrational.U_588_6 : Uω (aρ 6) (bρ 6) (43705589996379 / 64000000000000) ≤ -(573601652664223193247 / 1250000000000000000000)

theorem Zeta5Irrational.U_588_7 : Uω (aρ 7) (bρ 7) (43705589996379 / 64000000000000) ≤ -(4968178041979655025511 / 10000000000000000000000)

theorem Zeta5Irrational.U_588_8 : Uω (aρ 8) (bρ 8) (43705589996379 / 64000000000000) ≤ -(2741980454591354062683 / 5000000000000000000000)

theorem Zeta5Irrational.U_588_9 : Uω (aρ 9) (bρ 9) (43705589996379 / 64000000000000) ≤ -(6166416285021924208357 / 10000000000000000000000)

theorem Zeta5Irrational.U_588_10 : Uω (aρ 10) (bρ 10) (43705589996379 / 64000000000000) ≤ -(7050979866472832607387 / 10000000000000000000000)

theorem Zeta5Irrational.U_588_11 : Uω (aρ 11) (bρ 11) (43705589996379 / 64000000000000) ≤ -(8183456858447127867951 / 10000000000000000000000)

theorem Zeta5Irrational.U_588_12 : Uω (aρ 12) (bρ 12) (43705589996379 / 64000000000000) ≤ -(1204403490610925670401 / 1250000000000000000000)

theorem Zeta5Irrational.U_588_13 : Uω (aρ 13) (bρ 13) (43705589996379 / 64000000000000) ≤ -(11559851808548369618159 / 10000000000000000000000)

theorem Zeta5Irrational.U_588_14 : Uω (aρ 14) (bρ 14) (43705589996379 / 64000000000000) ≤ -(1461851957046835182271 / 1000000000000000000000)

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

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

theorem Zeta5Irrational.U_588 : Uρ (43705589996379 / 64000000000000) ≤ -(6561204984838086247927 / 10000000000000000000000)

theorem Zeta5Irrational.U_589_1 : Uω (aρ 1) (bρ 1) (5469688648751 / 8000000000000) ≤ -(1948507749324743187031 / 5000000000000000000000)

theorem Zeta5Irrational.U_589_2 : Uω (aρ 2) (bρ 2) (5469688648751 / 8000000000000) ≤ -(245773168539214552107 / 625000000000000000000)

theorem Zeta5Irrational.U_589_3 : Uω (aρ 3) (bρ 3) (5469688648751 / 8000000000000) ≤ -(2001718882180630828503 / 5000000000000000000000)

theorem Zeta5Irrational.U_589_4 : Uω (aρ 4) (bρ 4) (5469688648751 / 8000000000000) ≤ -(824506551390814758131 / 2000000000000000000000)

theorem Zeta5Irrational.U_589_5 : Uω (aρ 5) (bρ 5) (5469688648751 / 8000000000000) ≤ -(4306493497263263020103 / 10000000000000000000000)

theorem Zeta5Irrational.U_589_6 : Uω (aρ 6) (bρ 6) (5469688648751 / 8000000000000) ≤ -(4575965519951952109527 / 10000000000000000000000)

theorem Zeta5Irrational.U_589_7 : Uω (aρ 7) (bρ 7) (5469688648751 / 8000000000000) ≤ -(1238701908887633955801 / 2500000000000000000000)

theorem Zeta5Irrational.U_589_8 : Uω (aρ 8) (bρ 8) (5469688648751 / 8000000000000) ≤ -(5469825949513502250433 / 10000000000000000000000)

theorem Zeta5Irrational.U_589_9 : Uω (aρ 9) (bρ 9) (5469688648751 / 8000000000000) ≤ -(6151161216080942852501 / 10000000000000000000000)

theorem Zeta5Irrational.U_589_10 : Uω (aρ 10) (bρ 10) (5469688648751 / 8000000000000) ≤ -(7034053104242121893583 / 10000000000000000000000)

theorem Zeta5Irrational.U_589_11 : Uω (aρ 11) (bρ 11) (5469688648751 / 8000000000000) ≤ -(4081962433340292229409 / 5000000000000000000000)

theorem Zeta5Irrational.U_589_12 : Uω (aρ 12) (bρ 12) (5469688648751 / 8000000000000) ≤ -(1201408064539557201607 / 1250000000000000000000)

theorem Zeta5Irrational.U_589_13 : Uω (aρ 13) (bρ 13) (5469688648751 / 8000000000000) ≤ -(11526740094447365904059 / 10000000000000000000000)

theorem Zeta5Irrational.U_589_14 : Uω (aρ 14) (bρ 14) (5469688648751 / 8000000000000) ≤ -(1818429225264942628537 / 1250000000000000000000)

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

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

theorem Zeta5Irrational.U_589 : Uρ (5469688648751 / 8000000000000) ≤ -(818012982659048695281 / 1250000000000000000000)

theorem Zeta5Irrational.U_590_1 : Uω (aρ 1) (bρ 1) (43809428383637 / 64000000000000) ≤ -(1942522189783709894671 / 5000000000000000000000)

theorem Zeta5Irrational.U_590_2 : Uω (aρ 2) (bρ 2) (43809428383637 / 64000000000000) ≤ -(980089241722220861977 / 2500000000000000000000)

theorem Zeta5Irrational.U_590_3 : Uω (aρ 3) (bρ 3) (43809428383637 / 64000000000000) ≤ -(1995668845309871194029 / 5000000000000000000000)

theorem Zeta5Irrational.U_590_4 : Uω (aρ 4) (bρ 4) (43809428383637 / 64000000000000) ≤ -(4110285878273273006483 / 10000000000000000000000)

theorem Zeta5Irrational.U_590_5 : Uω (aρ 5) (bρ 5) (43809428383637 / 64000000000000) ≤ -(4294014520243379947173 / 10000000000000000000000)

theorem Zeta5Irrational.U_590_6 : Uω (aρ 6) (bρ 6) (43809428383637 / 64000000000000) ≤ -(912626870858038316583 / 2000000000000000000000)

theorem Zeta5Irrational.U_590_7 : Uω (aρ 7) (bρ 7) (43809428383637 / 64000000000000) ≤ -(4941455207028364076573 / 10000000000000000000000)

theorem Zeta5Irrational.U_590_8 : Uω (aρ 8) (bρ 8) (43809428383637 / 64000000000000) ≤ -(545571124375522783539 / 1000000000000000000000)

theorem Zeta5Irrational.U_590_9 : Uω (aρ 9) (bρ 9) (43809428383637 / 64000000000000) ≤ -(766991264223849596283 / 1250000000000000000000)

theorem Zeta5Irrational.U_590_10 : Uω (aρ 10) (bρ 10) (43809428383637 / 64000000000000) ≤ -(3508578377429020554659 / 5000000000000000000000)

theorem Zeta5Irrational.U_590_11 : Uω (aρ 11) (bρ 11) (43809428383637 / 64000000000000) ≤ -(8144435743557710104167 / 10000000000000000000000)

theorem Zeta5Irrational.U_590_12 : Uω (aρ 12) (bρ 12) (43809428383637 / 64000000000000) ≤ -(2396843256077924959477 / 2500000000000000000000)

theorem Zeta5Irrational.U_590_13 : Uω (aρ 13) (bρ 13) (43809428383637 / 64000000000000) ≤ -(5746899876398573163821 / 5000000000000000000000)

theorem Zeta5Irrational.U_590_14 : Uω (aρ 14) (bρ 14) (43809428383637 / 64000000000000) ≤ -(14477855490426510840571 / 10000000000000000000000)

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

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

theorem Zeta5Irrational.U_590 : Uρ (43809428383637 / 64000000000000) ≤ -(326355036030635433631 / 500000000000000000000)

theorem Zeta5Irrational.U_591_1 : Uω (aρ 1) (bρ 1) (21930673788633 / 32000000000000) ≤ -(3873087574221783174133 / 10000000000000000000000)

theorem Zeta5Irrational.U_591_2 : Uω (aρ 2) (bρ 2) (21930673788633 / 32000000000000) ≤ -(3908357653472914841141 / 10000000000000000000000)

theorem Zeta5Irrational.U_591_3 : Uω (aρ 3) (bρ 3) (21930673788633 / 32000000000000) ≤ -(497406530345597454679 / 1250000000000000000000)

theorem Zeta5Irrational.U_591_4 : Uω (aρ 4) (bρ 4) (21930673788633 / 32000000000000) ≤ -(512256748377032037619 / 1250000000000000000000)

theorem Zeta5Irrational.U_591_5 : Uω (aρ 5) (bρ 5) (21930673788633 / 32000000000000) ≤ -(2140775557921181468381 / 5000000000000000000000)

theorem Zeta5Irrational.U_591_6 : Uω (aρ 6) (bρ 6) (21930673788633 / 32000000000000) ≤ -(4550319681689112793929 / 10000000000000000000000)

theorem Zeta5Irrational.U_591_7 : Uω (aρ 7) (bρ 7) (21930673788633 / 32000000000000) ≤ -(4928120707798083417323 / 10000000000000000000000)

theorem Zeta5Irrational.U_591_8 : Uω (aρ 8) (bρ 8) (21930673788633 / 32000000000000) ≤ -(272080836654552202981 / 500000000000000000000)

theorem Zeta5Irrational.U_591_9 : Uω (aρ 9) (bρ 9) (21930673788633 / 32000000000000) ≤ -(6120722900714232247101 / 10000000000000000000000)

theorem Zeta5Irrational.U_591_10 : Uω (aρ 10) (bρ 10) (21930673788633 / 32000000000000) ≤ -(7000290702954301500691 / 10000000000000000000000)

theorem Zeta5Irrational.U_591_11 : Uω (aρ 11) (bρ 11) (21930673788633 / 32000000000000) ≤ -(2031247320397186581489 / 2500000000000000000000)

theorem Zeta5Irrational.U_591_12 : Uω (aρ 12) (bρ 12) (21930673788633 / 32000000000000) ≤ -(9563552940403943445557 / 10000000000000000000000)

theorem Zeta5Irrational.U_591_13 : Uω (aρ 13) (bρ 13) (21930673788633 / 32000000000000) ≤ -(2865257125482834296423 / 2500000000000000000000)

theorem Zeta5Irrational.U_591_14 : Uω (aρ 14) (bρ 14) (21930673788633 / 32000000000000) ≤ -(225151496633754432083 / 156250000000000000000)

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

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

theorem Zeta5Irrational.U_591 : Uρ (21930673788633 / 32000000000000) ≤ -(1302038278493546697749 / 2000000000000000000000)