Certified arcsine potential bounds (U53)

theorem Zeta5Irrational.U_640_1 : Uω (aρ 1) (bρ 1) (11854766575033 / 16000000000000) ≤ -(617209565778762565663 / 2000000000000000000000)

theorem Zeta5Irrational.U_640_2 : Uω (aρ 2) (bρ 2) (11854766575033 / 16000000000000) ≤ -(1559315139434144244523 / 5000000000000000000000)

theorem Zeta5Irrational.U_640_3 : Uω (aρ 3) (bρ 3) (11854766575033 / 16000000000000) ≤ -(796020581195767598923 / 2500000000000000000000)

theorem Zeta5Irrational.U_640_4 : Uω (aρ 4) (bρ 4) (11854766575033 / 16000000000000) ≤ -(3293641379290378129919 / 10000000000000000000000)

theorem Zeta5Irrational.U_640_5 : Uω (aρ 5) (bρ 5) (11854766575033 / 16000000000000) ≤ -(3462554103321312357713 / 10000000000000000000000)

theorem Zeta5Irrational.U_640_6 : Uω (aρ 6) (bρ 6) (11854766575033 / 16000000000000) ≤ -(1854629608987680224327 / 5000000000000000000000)

theorem Zeta5Irrational.U_640_7 : Uω (aρ 7) (bρ 7) (11854766575033 / 16000000000000) ≤ -(4054556366412365688859 / 10000000000000000000000)

theorem Zeta5Irrational.U_640_8 : Uω (aρ 8) (bρ 8) (11854766575033 / 16000000000000) ≤ -(141276713247013046609 / 312500000000000000000)

theorem Zeta5Irrational.U_640_9 : Uω (aρ 9) (bρ 9) (11854766575033 / 16000000000000) ≤ -(160361986765208395623 / 312500000000000000000)

theorem Zeta5Irrational.U_640_10 : Uω (aρ 10) (bρ 10) (11854766575033 / 16000000000000) ≤ -(1477721945264326746369 / 2500000000000000000000)

theorem Zeta5Irrational.U_640_11 : Uω (aρ 11) (bρ 11) (11854766575033 / 16000000000000) ≤ -(430240760642288933031 / 625000000000000000000)

theorem Zeta5Irrational.U_640_12 : Uω (aρ 12) (bρ 12) (11854766575033 / 16000000000000) ≤ -(4038902029818474039807 / 5000000000000000000000)

theorem Zeta5Irrational.U_640_13 : Uω (aρ 13) (bρ 13) (11854766575033 / 16000000000000) ≤ -(9526396211055741483633 / 10000000000000000000000)

theorem Zeta5Irrational.U_640_14 : Uω (aρ 14) (bρ 14) (11854766575033 / 16000000000000) ≤ -(11283870676060941852289 / 10000000000000000000000)

theorem Zeta5Irrational.U_640_15 : Uω (aρ 15) (bρ 15) (11854766575033 / 16000000000000) ≤ -(3376112697703459964891 / 2500000000000000000000)

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

theorem Zeta5Irrational.U_640 : Uρ (11854766575033 / 16000000000000) ≤ -(1074206850063200334523 / 2000000000000000000000)

theorem Zeta5Irrational.U_641_1 : Uω (aρ 1) (bρ 1) (23740009868623 / 32000000000000) ≤ -(3073089068670948228763 / 10000000000000000000000)

theorem Zeta5Irrational.U_641_2 : Uω (aρ 2) (bρ 2) (23740009868623 / 32000000000000) ≤ -(3105629036471363676813 / 10000000000000000000000)

theorem Zeta5Irrational.U_641_3 : Uω (aρ 3) (bρ 3) (23740009868623 / 32000000000000) ≤ -(1585497554256626544711 / 5000000000000000000000)

theorem Zeta5Irrational.U_641_4 : Uω (aρ 4) (bρ 4) (23740009868623 / 32000000000000) ≤ -(3280408326324041502759 / 10000000000000000000000)

theorem Zeta5Irrational.U_641_5 : Uω (aρ 5) (bρ 5) (23740009868623 / 32000000000000) ≤ -(1724545680045968091771 / 5000000000000000000000)

theorem Zeta5Irrational.U_641_6 : Uω (aρ 6) (bρ 6) (23740009868623 / 32000000000000) ≤ -(3695450016234095153087 / 10000000000000000000000)

theorem Zeta5Irrational.U_641_7 : Uω (aρ 7) (bρ 7) (23740009868623 / 32000000000000) ≤ -(808047810240227746469 / 2000000000000000000000)

theorem Zeta5Irrational.U_641_8 : Uω (aρ 8) (bρ 8) (23740009868623 / 32000000000000) ≤ -(4505804715333577953633 / 10000000000000000000000)

theorem Zeta5Irrational.U_641_9 : Uω (aρ 9) (bρ 9) (23740009868623 / 32000000000000) ≤ -(5115482859176546188077 / 10000000000000000000000)

theorem Zeta5Irrational.U_641_10 : Uω (aρ 10) (bρ 10) (23740009868623 / 32000000000000) ≤ -(736658945086993470021 / 1250000000000000000000)

theorem Zeta5Irrational.U_641_11 : Uω (aρ 11) (bρ 11) (23740009868623 / 32000000000000) ≤ -(6864003581606836853937 / 10000000000000000000000)

theorem Zeta5Irrational.U_641_12 : Uω (aρ 12) (bρ 12) (23740009868623 / 32000000000000) ≤ -(4027263637795985554169 / 5000000000000000000000)

theorem Zeta5Irrational.U_641_13 : Uω (aρ 13) (bρ 13) (23740009868623 / 32000000000000) ≤ -(9497441751319171954421 / 10000000000000000000000)

theorem Zeta5Irrational.U_641_14 : Uω (aρ 14) (bρ 14) (23740009868623 / 32000000000000) ≤ -(1124404824568891011653 / 1000000000000000000000)

theorem Zeta5Irrational.U_641_15 : Uω (aρ 15) (bρ 15) (23740009868623 / 32000000000000) ≤ -(13434819948548071133851 / 10000000000000000000000)

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

theorem Zeta5Irrational.U_641 : Uρ (23740009868623 / 32000000000000) ≤ -(2676446975214992581051 / 5000000000000000000000)

theorem Zeta5Irrational.U_642_1 : Uω (aρ 1) (bρ 1) (1188524329359 / 1600000000000) ≤ -(3060147079763797147191 / 10000000000000000000000)

theorem Zeta5Irrational.U_642_2 : Uω (aρ 2) (bρ 2) (1188524329359 / 1600000000000) ≤ -(3092644676025192306147 / 10000000000000000000000)

theorem Zeta5Irrational.U_642_3 : Uω (aρ 3) (bρ 3) (1188524329359 / 1600000000000) ≤ -(3157924999766053070299 / 10000000000000000000000)

theorem Zeta5Irrational.U_642_4 : Uω (aρ 4) (bρ 4) (1188524329359 / 1600000000000) ≤ -(1633596384335385696813 / 5000000000000000000000)

theorem Zeta5Irrational.U_642_5 : Uω (aρ 5) (bρ 5) (1188524329359 / 1600000000000) ≤ -(1717823368121241994069 / 5000000000000000000000)

theorem Zeta5Irrational.U_642_6 : Uω (aρ 6) (bρ 6) (1188524329359 / 1600000000000) ≤ -(736331981307432108431 / 2000000000000000000000)

theorem Zeta5Irrational.U_642_7 : Uω (aρ 7) (bρ 7) (1188524329359 / 1600000000000) ≤ -(805188464903322653011 / 2000000000000000000000)

theorem Zeta5Irrational.U_642_8 : Uω (aρ 8) (bρ 8) (1188524329359 / 1600000000000) ≤ -(4490777505587620117577 / 10000000000000000000000)

theorem Zeta5Irrational.U_642_9 : Uω (aρ 9) (bρ 9) (1188524329359 / 1600000000000) ≤ -(2549704341422734584063 / 5000000000000000000000)

theorem Zeta5Irrational.U_642_10 : Uω (aρ 10) (bρ 10) (1188524329359 / 1600000000000) ≤ -(5875687868970487449787 / 10000000000000000000000)

theorem Zeta5Irrational.U_642_11 : Uω (aρ 11) (bρ 11) (1188524329359 / 1600000000000) ≤ -(3422099036893664444543 / 5000000000000000000000)

theorem Zeta5Irrational.U_642_12 : Uω (aρ 12) (bρ 12) (1188524329359 / 1600000000000) ≤ -(31372321582058323511 / 39062500000000000000)

theorem Zeta5Irrational.U_642_13 : Uω (aρ 13) (bρ 13) (1188524329359 / 1600000000000) ≤ -(4734299912291785360331 / 5000000000000000000000)

theorem Zeta5Irrational.U_642_14 : Uω (aρ 14) (bρ 14) (1188524329359 / 1600000000000) ≤ -(2240898948388567398827 / 2000000000000000000000)

theorem Zeta5Irrational.U_642_15 : Uω (aρ 15) (bρ 15) (1188524329359 / 1600000000000) ≤ -(13366510929828003237353 / 10000000000000000000000)

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

theorem Zeta5Irrational.U_642 : Uρ (1188524329359 / 1600000000000) ≤ -(666854306635595554443 / 1250000000000000000000)

theorem Zeta5Irrational.U_643_1 : Uω (aρ 1) (bρ 1) (23800963305737 / 32000000000000) ≤ -(1523610909408552015951 / 5000000000000000000000)

theorem Zeta5Irrational.U_643_2 : Uω (aρ 2) (bρ 2) (23800963305737 / 32000000000000) ≤ -(1539838576871448098047 / 5000000000000000000000)

theorem Zeta5Irrational.U_643_3 : Uω (aρ 3) (bρ 3) (23800963305737 / 32000000000000) ≤ -(628974390773593105421 / 2000000000000000000000)

theorem Zeta5Irrational.U_643_4 : Uω (aρ 4) (bρ 4) (23800963305737 / 32000000000000) ≤ -(813498665028040558633 / 2500000000000000000000)

theorem Zeta5Irrational.U_643_5 : Uω (aρ 5) (bρ 5) (23800963305737 / 32000000000000) ≤ -(1711110091506825365049 / 5000000000000000000000)

theorem Zeta5Irrational.U_643_6 : Uω (aρ 6) (bρ 6) (23800963305737 / 32000000000000) ≤ -(3667888836031086007881 / 10000000000000000000000)

theorem Zeta5Irrational.U_643_7 : Uω (aρ 7) (bρ 7) (23800963305737 / 32000000000000) ≤ -(501458265861246567413 / 1250000000000000000000)

theorem Zeta5Irrational.U_643_8 : Uω (aρ 8) (bρ 8) (23800963305737 / 32000000000000) ≤ -(4475773124241223698507 / 10000000000000000000000)

theorem Zeta5Irrational.U_643_9 : Uω (aρ 9) (bρ 9) (23800963305737 / 32000000000000) ≤ -(1270840239499814070163 / 2500000000000000000000)

theorem Zeta5Irrational.U_643_10 : Uω (aρ 10) (bρ 10) (23800963305737 / 32000000000000) ≤ -(292906829020823116481 / 500000000000000000000)

theorem Zeta5Irrational.U_643_11 : Uω (aρ 11) (bρ 11) (23800963305737 / 32000000000000) ≤ -(106631803823411271099 / 156250000000000000000)

theorem Zeta5Irrational.U_643_12 : Uω (aρ 12) (bρ 12) (23800963305737 / 32000000000000) ≤ -(1601632961928138856129 / 2000000000000000000000)

theorem Zeta5Irrational.U_643_13 : Uω (aρ 13) (bρ 13) (23800963305737 / 32000000000000) ≤ -(4719934683011539956371 / 5000000000000000000000)

theorem Zeta5Irrational.U_643_14 : Uω (aρ 14) (bρ 14) (23800963305737 / 32000000000000) ≤ -(2791301348886200293647 / 2500000000000000000000)

theorem Zeta5Irrational.U_643_15 : Uω (aρ 15) (bρ 15) (23800963305737 / 32000000000000) ≤ -(13299454215022681784837 / 10000000000000000000000)

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

theorem Zeta5Irrational.U_643 : Uρ (23800963305737 / 32000000000000) ≤ -(5316853278250076301219 / 10000000000000000000000)

theorem Zeta5Irrational.U_644_1 : Uω (aρ 1) (bρ 1) (11915720012147 / 16000000000000) ≤ -(3034313242643511466231 / 10000000000000000000000)

theorem Zeta5Irrational.U_644_2 : Uω (aρ 2) (bρ 2) (11915720012147 / 16000000000000) ≤ -(766681606501934609241 / 2500000000000000000000)

theorem Zeta5Irrational.U_644_3 : Uω (aρ 3) (bρ 3) (11915720012147 / 16000000000000) ≤ -(3131835926320268809229 / 10000000000000000000000)

theorem Zeta5Irrational.U_644_4 : Uω (aρ 4) (bρ 4) (11915720012147 / 16000000000000) ≤ -(810203488653197127289 / 2500000000000000000000)

theorem Zeta5Irrational.U_644_5 : Uω (aρ 5) (bρ 5) (11915720012147 / 16000000000000) ≤ -(852202912960722596749 / 2500000000000000000000)

theorem Zeta5Irrational.U_644_6 : Uω (aρ 6) (bρ 6) (11915720012147 / 16000000000000) ≤ -(3654136752082123200103 / 10000000000000000000000)

theorem Zeta5Irrational.U_644_7 : Uω (aρ 7) (bρ 7) (11915720012147 / 16000000000000) ≤ -(3997410399111135964581 / 10000000000000000000000)

theorem Zeta5Irrational.U_644_8 : Uω (aρ 8) (bρ 8) (11915720012147 / 16000000000000) ≤ -(178431660047890653203 / 400000000000000000000)

theorem Zeta5Irrational.U_644_9 : Uω (aρ 9) (bρ 9) (11915720012147 / 16000000000000) ≤ -(633417449450731358873 / 1250000000000000000000)

theorem Zeta5Irrational.U_644_10 : Uω (aρ 10) (bρ 10) (11915720012147 / 16000000000000) ≤ -(2920308785161509705411 / 5000000000000000000000)

theorem Zeta5Irrational.U_644_11 : Uω (aρ 11) (bρ 11) (11915720012147 / 16000000000000) ≤ -(3402357746865413340039 / 5000000000000000000000)

theorem Zeta5Irrational.U_644_12 : Uω (aρ 12) (bρ 12) (11915720012147 / 16000000000000) ≤ -(3992539167654871337849 / 5000000000000000000000)

theorem Zeta5Irrational.U_644_13 : Uω (aρ 13) (bρ 13) (11915720012147 / 16000000000000) ≤ -(9411249327571361579049 / 10000000000000000000000)

theorem Zeta5Irrational.U_644_14 : Uω (aρ 14) (bρ 14) (11915720012147 / 16000000000000) ≤ -(5563087789113514828389 / 5000000000000000000000)

theorem Zeta5Irrational.U_644_15 : Uω (aρ 15) (bρ 15) (11915720012147 / 16000000000000) ≤ -(13233586213666000565321 / 10000000000000000000000)

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

theorem Zeta5Irrational.U_644 : Uρ (11915720012147 / 16000000000000) ≤ -(2649474067190841539383 / 5000000000000000000000)

theorem Zeta5Irrational.U_645_1 : Uω (aρ 1) (bρ 1) (746637295669 / 1000000000000) ≤ -(1504272986350256580489 / 5000000000000000000000)

theorem Zeta5Irrational.U_645_2 : Uω (aρ 2) (bρ 2) (746637295669 / 1000000000000) ≤ -(3040875180557327393003 / 10000000000000000000000)

theorem Zeta5Irrational.U_645_3 : Uω (aρ 3) (bρ 3) (746637295669 / 1000000000000) ≤ -(388226843643701977613 / 1250000000000000000000)

theorem Zeta5Irrational.U_645_4 : Uω (aρ 4) (bρ 4) (746637295669 / 1000000000000) ≤ -(1607252284779575578089 / 5000000000000000000000)

theorem Zeta5Irrational.U_645_5 : Uω (aρ 5) (bρ 5) (746637295669 / 1000000000000) ≤ -(3382048462402861285543 / 10000000000000000000000)

theorem Zeta5Irrational.U_645_6 : Uω (aρ 6) (bρ 6) (746637295669 / 1000000000000) ≤ -(3626689334411872943689 / 10000000000000000000000)

theorem Zeta5Irrational.U_645_7 : Uω (aρ 7) (bρ 7) (746637295669 / 1000000000000) ≤ -(496120014692653319329 / 1250000000000000000000)

theorem Zeta5Irrational.U_645_8 : Uω (aρ 8) (bρ 8) (746637295669 / 1000000000000) ≤ -(4430896251256838405569 / 10000000000000000000000)

theorem Zeta5Irrational.U_645_9 : Uω (aρ 9) (bρ 9) (746637295669 / 1000000000000) ≤ -(2517687802170217421033 / 5000000000000000000000)

theorem Zeta5Irrational.U_645_10 : Uω (aρ 10) (bρ 10) (746637295669 / 1000000000000) ≤ -(2902837945202620132743 / 5000000000000000000000)

theorem Zeta5Irrational.U_645_11 : Uω (aρ 11) (bρ 11) (746637295669 / 1000000000000) ≤ -(1691350707796066750917 / 2500000000000000000000)

theorem Zeta5Irrational.U_645_12 : Uω (aρ 12) (bρ 12) (746637295669 / 1000000000000) ≤ -(3969546476480306766289 / 5000000000000000000000)

theorem Zeta5Irrational.U_645_13 : Uω (aρ 13) (bρ 13) (746637295669 / 1000000000000) ≤ -(935433640031612922849 / 1000000000000000000000)

theorem Zeta5Irrational.U_645_14 : Uω (aρ 14) (bρ 14) (746637295669 / 1000000000000) ≤ -(1104887668831840048521 / 1000000000000000000000)

theorem Zeta5Irrational.U_645_15 : Uω (aρ 15) (bρ 15) (746637295669 / 1000000000000) ≤ -(6552593809832138435991 / 5000000000000000000000)

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

theorem Zeta5Irrational.U_645 : Uρ (746637295669 / 1000000000000) ≤ -(5263357591767758389913 / 10000000000000000000000)

theorem Zeta5Irrational.U_646_1 : Uω (aρ 1) (bρ 1) (765809953469387 / 1024000000000000) ≤ -(2992023359028118615229 / 10000000000000000000000)

theorem Zeta5Irrational.U_646_2 : Uω (aρ 2) (bρ 2) (765809953469387 / 1024000000000000) ≤ -(3024298834984676636863 / 10000000000000000000000)

theorem Zeta5Irrational.U_646_3 : Uω (aρ 3) (bρ 3) (765809953469387 / 1024000000000000) ≤ -(3089129675859665067647 / 10000000000000000000000)

theorem Zeta5Irrational.U_646_4 : Uω (aρ 4) (bρ 4) (765809953469387 / 1024000000000000) ≤ -(3197635102305245452937 / 10000000000000000000000)

theorem Zeta5Irrational.U_646_5 : Uω (aρ 5) (bρ 5) (765809953469387 / 1024000000000000) ≤ -(3364888680715927873629 / 10000000000000000000000)

theorem Zeta5Irrational.U_646_6 : Uω (aρ 6) (bρ 6) (765809953469387 / 1024000000000000) ≤ -(902272973128295129753 / 2500000000000000000000)

theorem Zeta5Irrational.U_646_7 : Uω (aρ 7) (bρ 7) (765809953469387 / 1024000000000000) ≤ -(3950721346605848420679 / 10000000000000000000000)

theorem Zeta5Irrational.U_646_8 : Uω (aρ 8) (bρ 8) (765809953469387 / 1024000000000000) ≤ -(1102933434446520637007 / 2500000000000000000000)

theorem Zeta5Irrational.U_646_9 : Uω (aρ 9) (bρ 9) (765809953469387 / 1024000000000000) ≤ -(5014891254244500333307 / 10000000000000000000000)

theorem Zeta5Irrational.U_646_10 : Uω (aρ 10) (bρ 10) (765809953469387 / 1024000000000000) ≤ -(2891645207438468629941 / 5000000000000000000000)

theorem Zeta5Irrational.U_646_11 : Uω (aρ 11) (bρ 11) (765809953469387 / 1024000000000000) ≤ -(6740230160113358478249 / 10000000000000000000000)

theorem Zeta5Irrational.U_646_12 : Uω (aρ 12) (bρ 12) (765809953469387 / 1024000000000000) ≤ -(3954837198590898932649 / 5000000000000000000000)

theorem Zeta5Irrational.U_646_13 : Uω (aρ 13) (bρ 13) (765809953469387 / 1024000000000000) ≤ -(9317992342333403447889 / 10000000000000000000000)

theorem Zeta5Irrational.U_646_14 : Uω (aρ 14) (bρ 14) (765809953469387 / 1024000000000000) ≤ -(10999728173947622292111 / 10000000000000000000000)

theorem Zeta5Irrational.U_646_15 : Uω (aρ 15) (bρ 15) (765809953469387 / 1024000000000000) ≤ -(3256218652869368476347 / 2500000000000000000000)

theorem Zeta5Irrational.U_646_16 : Uω (aρ 16) (bρ 16) (765809953469387 / 1024000000000000) ≤ -(3195214162855050481337 / 2000000000000000000000)

theorem Zeta5Irrational.U_646 : Uρ (765809953469387 / 1024000000000000) ≤ -(2617905894506130104443 / 5000000000000000000000)

theorem Zeta5Irrational.U_647_1 : Uω (aρ 1) (bρ 1) (383531658086859 / 512000000000000) ≤ -(2975528000166417994777 / 10000000000000000000000)

theorem Zeta5Irrational.U_647_2 : Uω (aρ 2) (bρ 2) (383531658086859 / 512000000000000) ≤ -(3007749922533249645921 / 10000000000000000000000)

theorem Zeta5Irrational.U_647_3 : Uω (aρ 3) (bρ 3) (383531658086859 / 512000000000000) ≤ -(3072472399178550156159 / 10000000000000000000000)

theorem Zeta5Irrational.U_647_4 : Uω (aρ 4) (bρ 4) (383531658086859 / 512000000000000) ≤ -(3180794056339040181553 / 10000000000000000000000)

theorem Zeta5Irrational.U_647_5 : Uω (aρ 5) (bρ 5) (383531658086859 / 512000000000000) ≤ -(1673879162526766033253 / 5000000000000000000000)

theorem Zeta5Irrational.U_647_6 : Uω (aρ 6) (bρ 6) (383531658086859 / 512000000000000) ≤ -(1795762720630881838427 / 5000000000000000000000)

theorem Zeta5Irrational.U_647_7 : Uω (aρ 7) (bρ 7) (383531658086859 / 512000000000000) ≤ -(983128992591838766227 / 2500000000000000000000)

theorem Zeta5Irrational.U_647_8 : Uω (aρ 8) (bρ 8) (383531658086859 / 512000000000000) ≤ -(4392608322960627458259 / 10000000000000000000000)

theorem Zeta5Irrational.U_647_9 : Uω (aρ 9) (bρ 9) (383531658086859 / 512000000000000) ≤ -(998889964806808706123 / 2000000000000000000000)

theorem Zeta5Irrational.U_647_10 : Uω (aρ 10) (bρ 10) (383531658086859 / 512000000000000) ≤ -(5760957383230505686231 / 10000000000000000000000)

theorem Zeta5Irrational.U_647_11 : Uω (aρ 11) (bρ 11) (383531658086859 / 512000000000000) ≤ -(3357563293086641684171 / 5000000000000000000000)

theorem Zeta5Irrational.U_647_12 : Uω (aρ 12) (bρ 12) (383531658086859 / 512000000000000) ≤ -(1970089311762010817417 / 2500000000000000000000)

theorem Zeta5Irrational.U_647_13 : Uω (aρ 13) (bρ 13) (383531658086859 / 512000000000000) ≤ -(1856364708443179756327 / 2000000000000000000000)

theorem Zeta5Irrational.U_647_14 : Uω (aρ 14) (bρ 14) (383531658086859 / 512000000000000) ≤ -(10950977982772224991237 / 10000000000000000000000)

theorem Zeta5Irrational.U_647_15 : Uω (aρ 15) (bρ 15) (383531658086859 / 512000000000000) ≤ -(80913513290171031217 / 62500000000000000000)

theorem Zeta5Irrational.U_647_16 : Uω (aρ 16) (bρ 16) (383531658086859 / 512000000000000) ≤ -(7820519683689689857467 / 5000000000000000000000)

theorem Zeta5Irrational.U_647 : Uρ (383531658086859 / 512000000000000) ≤ -(5211206336518075658923 / 10000000000000000000000)

theorem Zeta5Irrational.U_648_1 : Uω (aρ 1) (bρ 1) (768316678878049 / 1024000000000000) ≤ -(1479529903173407912513 / 5000000000000000000000)

theorem Zeta5Irrational.U_648_2 : Uω (aρ 2) (bρ 2) (768316678878049 / 1024000000000000) ≤ -(1495614176274166129169 / 5000000000000000000000)

theorem Zeta5Irrational.U_648_3 : Uω (aρ 3) (bρ 3) (768316678878049 / 1024000000000000) ≤ -(1527921413315886781817 / 5000000000000000000000)

theorem Zeta5Irrational.U_648_4 : Uω (aρ 4) (bρ 4) (768316678878049 / 1024000000000000) ≤ -(1581990668008304209843 / 5000000000000000000000)

theorem Zeta5Irrational.U_648_5 : Uω (aρ 5) (bρ 5) (768316678878049 / 1024000000000000) ≤ -(3330657294562922625271 / 10000000000000000000000)

theorem Zeta5Irrational.U_648_6 : Uω (aρ 6) (bρ 6) (768316678878049 / 1024000000000000) ≤ -(714797974284375681511 / 2000000000000000000000)

theorem Zeta5Irrational.U_648_7 : Uω (aρ 7) (bρ 7) (768316678878049 / 1024000000000000) ≤ -(489292983258718903463 / 1250000000000000000000)

theorem Zeta5Irrational.U_648_8 : Uω (aρ 8) (bρ 8) (768316678878049 / 1024000000000000) ≤ -(4373519861695254145247 / 10000000000000000000000)

theorem Zeta5Irrational.U_648_9 : Uω (aρ 9) (bρ 9) (768316678878049 / 1024000000000000) ≤ -(2487025564965771604759 / 5000000000000000000000)

theorem Zeta5Irrational.U_648_10 : Uω (aρ 10) (bρ 10) (768316678878049 / 1024000000000000) ≤ -(1434669134801156281813 / 2500000000000000000000)

theorem Zeta5Irrational.U_648_11 : Uω (aρ 11) (bρ 11) (768316678878049 / 1024000000000000) ≤ -(3345045850188347560643 / 5000000000000000000000)

theorem Zeta5Irrational.U_648_12 : Uω (aρ 12) (bρ 12) (768316678878049 / 1024000000000000) ≤ -(245348147203090920197 / 312500000000000000000)

theorem Zeta5Irrational.U_648_13 : Uω (aρ 13) (bρ 13) (768316678878049 / 1024000000000000) ≤ -(9245827955184049930021 / 10000000000000000000000)

theorem Zeta5Irrational.U_648_14 : Uω (aρ 14) (bρ 14) (768316678878049 / 1024000000000000) ≤ -(10902617715487759439317 / 10000000000000000000000)

theorem Zeta5Irrational.U_648_15 : Uω (aρ 15) (bρ 15) (768316678878049 / 1024000000000000) ≤ -(12868962730306120814047 / 10000000000000000000000)

theorem Zeta5Irrational.U_648_16 : Uω (aρ 16) (bρ 16) (768316678878049 / 1024000000000000) ≤ -(3076834627347482851323 / 2000000000000000000000)

theorem Zeta5Irrational.U_648 : Uρ (768316678878049 / 1024000000000000) ≤ -(1037435107378750881219 / 2000000000000000000000)

theorem Zeta5Irrational.U_649_1 : Uω (aρ 1) (bρ 1) (38478502079119 / 51200000000000) ≤ -(1471309344121746862427 / 5000000000000000000000)

theorem Zeta5Irrational.U_649_2 : Uω (aρ 2) (bρ 2) (38478502079119 / 51200000000000) ≤ -(2974734034823848649063 / 10000000000000000000000)

theorem Zeta5Irrational.U_649_3 : Uω (aρ 3) (bρ 3) (38478502079119 / 51200000000000) ≤ -(3039240866205603229829 / 10000000000000000000000)

theorem Zeta5Irrational.U_649_4 : Uω (aρ 4) (bρ 4) (38478502079119 / 51200000000000) ≤ -(1573598423088097864679 / 5000000000000000000000)

theorem Zeta5Irrational.U_649_5 : Uω (aρ 5) (bρ 5) (38478502079119 / 51200000000000) ≤ -(82839637222737004547 / 250000000000000000000)

theorem Zeta5Irrational.U_649_6 : Uω (aρ 6) (bρ 6) (38478502079119 / 51200000000000) ≤ -(3556485074335744005427 / 10000000000000000000000)

theorem Zeta5Irrational.U_649_7 : Uω (aρ 7) (bρ 7) (38478502079119 / 51200000000000) ≤ -(3896204911636402043661 / 10000000000000000000000)

theorem Zeta5Irrational.U_649_8 : Uω (aρ 8) (bρ 8) (38478502079119 / 51200000000000) ≤ -(4354468209763952836931 / 10000000000000000000000)

theorem Zeta5Irrational.U_649_9 : Uω (aρ 9) (bρ 9) (38478502079119 / 51200000000000) ≤ -(990738997872693485211 / 2000000000000000000000)

theorem Zeta5Irrational.U_649_10 : Uω (aρ 10) (bρ 10) (38478502079119 / 51200000000000) ≤ -(142911190712137077017 / 250000000000000000000)

theorem Zeta5Irrational.U_649_11 : Uω (aρ 11) (bρ 11) (38478502079119 / 51200000000000) ≤ -(1666281274396531617289 / 2500000000000000000000)

theorem Zeta5Irrational.U_649_12 : Uω (aρ 12) (bρ 12) (38478502079119 / 51200000000000) ≤ -(1955506001388691126887 / 2500000000000000000000)

theorem Zeta5Irrational.U_649_13 : Uω (aρ 13) (bρ 13) (38478502079119 / 51200000000000) ≤ -(9210003576042587965751 / 10000000000000000000000)

theorem Zeta5Irrational.U_649_14 : Uω (aρ 14) (bρ 14) (38478502079119 / 51200000000000) ≤ -(2170927853472496869607 / 2000000000000000000000)

theorem Zeta5Irrational.U_649_15 : Uω (aρ 15) (bρ 15) (38478502079119 / 51200000000000) ≤ -(12793196732551274176083 / 10000000000000000000000)

theorem Zeta5Irrational.U_649_16 : Uω (aρ 16) (bρ 16) (38478502079119 / 51200000000000) ≤ -(758390116236913319073 / 500000000000000000000)

theorem Zeta5Irrational.U_649 : Uρ (38478502079119 / 51200000000000) ≤ -(161359119069458724063 / 312500000000000000000)

theorem Zeta5Irrational.U_650_1 : Uω (aρ 1) (bρ 1) (770823404286711 / 1024000000000000) ≤ -(1463102278485251628801 / 5000000000000000000000)

theorem Zeta5Irrational.U_650_2 : Uω (aρ 2) (bρ 2) (770823404286711 / 1024000000000000) ≤ -(1479133439799703354753 / 5000000000000000000000)

theorem Zeta5Irrational.U_650_3 : Uω (aρ 3) (bρ 3) (770823404286711 / 1024000000000000) ≤ -(1511333213172008917413 / 5000000000000000000000)

theorem Zeta5Irrational.U_650_4 : Uω (aρ 4) (bρ 4) (770823404286711 / 1024000000000000) ≤ -(3130440492134986453193 / 10000000000000000000000)

theorem Zeta5Irrational.U_650_5 : Uω (aρ 5) (bρ 5) (770823404286711 / 1024000000000000) ≤ -(1648271404136584240029 / 5000000000000000000000)

theorem Zeta5Irrational.U_650_6 : Uω (aρ 6) (bρ 6) (770823404286711 / 1024000000000000) ≤ -(1769505470959731984053 / 5000000000000000000000)

theorem Zeta5Irrational.U_650_7 : Uω (aρ 7) (bρ 7) (770823404286711 / 1024000000000000) ≤ -(387809898566500223647 / 1000000000000000000000)

theorem Zeta5Irrational.U_650_8 : Uω (aρ 8) (bρ 8) (770823404286711 / 1024000000000000) ≤ -(867090644758616515783 / 2000000000000000000000)

theorem Zeta5Irrational.U_650_9 : Uω (aρ 9) (bρ 9) (770823404286711 / 1024000000000000) ≤ -(4933381220949565653991 / 10000000000000000000000)

theorem Zeta5Irrational.U_650_10 : Uω (aρ 10) (bρ 10) (770823404286711 / 1024000000000000) ≤ -(2847135199343223354549 / 5000000000000000000000)

theorem Zeta5Irrational.U_650_11 : Uω (aρ 11) (bρ 11) (770823404286711 / 1024000000000000) ≤ -(1328045275292720239523 / 2000000000000000000000)

theorem Zeta5Irrational.U_650_12 : Uω (aρ 12) (bρ 12) (770823404286711 / 1024000000000000) ≤ -(7793006360136964195467 / 10000000000000000000000)

theorem Zeta5Irrational.U_650_13 : Uω (aρ 13) (bρ 13) (770823404286711 / 1024000000000000) ≤ -(9174348438106759670099 / 10000000000000000000000)

theorem Zeta5Irrational.U_650_14 : Uω (aρ 14) (bρ 14) (770823404286711 / 1024000000000000) ≤ -(10807034813892791887537 / 10000000000000000000000)

theorem Zeta5Irrational.U_650_15 : Uω (aρ 15) (bρ 15) (770823404286711 / 1024000000000000) ≤ -(12718791257063904718547 / 10000000000000000000000)

theorem Zeta5Irrational.U_650_16 : Uω (aρ 16) (bρ 16) (770823404286711 / 1024000000000000) ≤ -(936083213417966146663 / 625000000000000000000)

theorem Zeta5Irrational.U_650 : Uρ (770823404286711 / 1024000000000000) ≤ -(1028013062888184996239 / 2000000000000000000000)

theorem Zeta5Irrational.U_651_1 : Uω (aρ 1) (bρ 1) (386038383495521 / 512000000000000) ≤ -(1454908662039441301187 / 5000000000000000000000)

theorem Zeta5Irrational.U_651_2 : Uω (aρ 2) (bρ 2) (386038383495521 / 512000000000000) ≤ -(2941826797557366372611 / 10000000000000000000000)

theorem Zeta5Irrational.U_651_3 : Uω (aρ 3) (bρ 3) (386038383495521 / 512000000000000) ≤ -(150305970797283732639 / 500000000000000000000)

theorem Zeta5Irrational.U_651_4 : Uω (aρ 4) (bρ 4) (386038383495521 / 512000000000000) ≤ -(3113712179685890930111 / 10000000000000000000000)

theorem Zeta5Irrational.U_651_5 : Uω (aρ 5) (bρ 5) (386038383495521 / 512000000000000) ≤ -(3279529153345017258651 / 10000000000000000000000)

theorem Zeta5Irrational.U_651_6 : Uω (aρ 6) (bρ 6) (386038383495521 / 512000000000000) ≤ -(880391841664744773029 / 2500000000000000000000)

theorem Zeta5Irrational.U_651_7 : Uω (aρ 7) (bρ 7) (386038383495521 / 512000000000000) ≤ -(772005193484518130031 / 2000000000000000000000)

theorem Zeta5Irrational.U_651_8 : Uω (aρ 8) (bρ 8) (386038383495521 / 512000000000000) ≤ -(4316474761254591827999 / 10000000000000000000000)

theorem Zeta5Irrational.U_651_9 : Uω (aρ 9) (bρ 9) (386038383495521 / 512000000000000) ≤ -(2456554822246143235107 / 5000000000000000000000)

theorem Zeta5Irrational.U_651_10 : Uω (aρ 10) (bρ 10) (386038383495521 / 512000000000000) ≤ -(5672144599328013069273 / 10000000000000000000000)

theorem Zeta5Irrational.U_651_11 : Uω (aρ 11) (bρ 11) (386038383495521 / 512000000000000) ≤ -(66153951394211009971 / 100000000000000000000)

theorem Zeta5Irrational.U_651_12 : Uω (aρ 12) (bρ 12) (386038383495521 / 512000000000000) ≤ -(7764087011892156874073 / 10000000000000000000000)

theorem Zeta5Irrational.U_651_13 : Uω (aρ 13) (bρ 13) (386038383495521 / 512000000000000) ≤ -(2284715153041468922039 / 2500000000000000000000)

theorem Zeta5Irrational.U_651_14 : Uω (aρ 14) (bρ 14) (386038383495521 / 512000000000000) ≤ -(10759796797346239902829 / 10000000000000000000000)

theorem Zeta5Irrational.U_651_15 : Uω (aρ 15) (bρ 15) (386038383495521 / 512000000000000) ≤ -(252913589034511244197 / 200000000000000000000)

theorem Zeta5Irrational.U_651_16 : Uω (aρ 16) (bρ 16) (386038383495521 / 512000000000000) ≤ -(7402636371640588000721 / 5000000000000000000000)

theorem Zeta5Irrational.U_651 : Uρ (386038383495521 / 512000000000000) ≤ -(511684876669522631533 / 1000000000000000000000)