Certified arcsine potential bounds (U03)

theorem Zeta5Irrational.U_40_1 : Uω (aρ 1) (bρ 1) (3068199571 / 200000000000) ≤ -(47437922514341080202681 / 10000000000000000000000)

theorem Zeta5Irrational.U_40_2 : Uω (aρ 2) (bρ 2) (3068199571 / 200000000000) ≤ -(57268912150832389796717 / 10000000000000000000000)

theorem Zeta5Irrational.U_40_3 : Uω (aρ 3) (bρ 3) (3068199571 / 200000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_40_4 : Uω (aρ 4) (bρ 4) (3068199571 / 200000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_40_5 : Uω (aρ 5) (bρ 5) (3068199571 / 200000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_40_6 : Uω (aρ 6) (bρ 6) (3068199571 / 200000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_40_7 : Uω (aρ 7) (bρ 7) (3068199571 / 200000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_40_8 : Uω (aρ 8) (bρ 8) (3068199571 / 200000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_40_9 : Uω (aρ 9) (bρ 9) (3068199571 / 200000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_40_10 : Uω (aρ 10) (bρ 10) (3068199571 / 200000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_40_11 : Uω (aρ 11) (bρ 11) (3068199571 / 200000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_40_12 : Uω (aρ 12) (bρ 12) (3068199571 / 200000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_40_13 : Uω (aρ 13) (bρ 13) (3068199571 / 200000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_40_14 : Uω (aρ 14) (bρ 14) (3068199571 / 200000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_40_15 : Uω (aρ 15) (bρ 15) (3068199571 / 200000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_40_16 : Uω (aρ 16) (bρ 16) (3068199571 / 200000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_40 : Uρ (3068199571 / 200000000000) ≤ -(28480811898748750448173 / 10000000000000000000000)

theorem Zeta5Irrational.U_41_1 : Uω (aρ 1) (bρ 1) (255845148549 / 16000000000000) ≤ -(23352264455452045399363 / 5000000000000000000000)

theorem Zeta5Irrational.U_41_2 : Uω (aρ 2) (bρ 2) (255845148549 / 16000000000000) ≤ -(2113612623409580587049 / 400000000000000000000)

theorem Zeta5Irrational.U_41_3 : Uω (aρ 3) (bρ 3) (255845148549 / 16000000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_41_4 : Uω (aρ 4) (bρ 4) (255845148549 / 16000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_41_5 : Uω (aρ 5) (bρ 5) (255845148549 / 16000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_41_6 : Uω (aρ 6) (bρ 6) (255845148549 / 16000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_41_7 : Uω (aρ 7) (bρ 7) (255845148549 / 16000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_41_8 : Uω (aρ 8) (bρ 8) (255845148549 / 16000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_41 : Uρ (255845148549 / 16000000000000) ≤ -(14171290695500939233193 / 5000000000000000000000)

theorem Zeta5Irrational.U_42_1 : Uω (aρ 1) (bρ 1) (133117165709 / 8000000000000) ≤ -(23011512008219083613497 / 5000000000000000000000)

theorem Zeta5Irrational.U_42_2 : Uω (aρ 2) (bρ 2) (133117165709 / 8000000000000) ≤ -(51055078142581221338421 / 10000000000000000000000)

theorem Zeta5Irrational.U_42_3 : Uω (aρ 3) (bρ 3) (133117165709 / 8000000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_42_4 : Uω (aρ 4) (bρ 4) (133117165709 / 8000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_42_5 : Uω (aρ 5) (bρ 5) (133117165709 / 8000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_42_6 : Uω (aρ 6) (bρ 6) (133117165709 / 8000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_42_7 : Uω (aρ 7) (bρ 7) (133117165709 / 8000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_42_8 : Uω (aρ 8) (bρ 8) (133117165709 / 8000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_42 : Uρ (133117165709 / 8000000000000) ≤ -(14141400455464355101593 / 5000000000000000000000)

theorem Zeta5Irrational.U_43_1 : Uω (aρ 1) (bρ 1) (108571569141 / 6400000000000) ≤ -(22849732727431537692483 / 5000000000000000000000)

theorem Zeta5Irrational.U_43_2 : Uω (aρ 2) (bρ 2) (108571569141 / 6400000000000) ≤ -(5034826491214142248959 / 1000000000000000000000)

theorem Zeta5Irrational.U_43_3 : Uω (aρ 3) (bρ 3) (108571569141 / 6400000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_43_4 : Uω (aρ 4) (bρ 4) (108571569141 / 6400000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_43_5 : Uω (aρ 5) (bρ 5) (108571569141 / 6400000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_43_6 : Uω (aρ 6) (bρ 6) (108571569141 / 6400000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_43_7 : Uω (aρ 7) (bρ 7) (108571569141 / 6400000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_43_8 : Uω (aρ 8) (bρ 8) (108571569141 / 6400000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_43_9 : Uω (aρ 9) (bρ 9) (108571569141 / 6400000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_43_10 : Uω (aρ 10) (bρ 10) (108571569141 / 6400000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_43_11 : Uω (aρ 11) (bρ 11) (108571569141 / 6400000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_43_12 : Uω (aρ 12) (bρ 12) (108571569141 / 6400000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_43_13 : Uω (aρ 13) (bρ 13) (108571569141 / 6400000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_43_14 : Uω (aρ 14) (bρ 14) (108571569141 / 6400000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

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

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

theorem Zeta5Irrational.U_43 : Uρ (108571569141 / 6400000000000) ≤ -(5651713497111691966977 / 2000000000000000000000)

theorem Zeta5Irrational.U_44_1 : Uω (aρ 1) (bρ 1) (276623514287 / 16000000000000) ≤ -(45386349211403757950859 / 10000000000000000000000)

theorem Zeta5Irrational.U_44_2 : Uω (aρ 2) (bρ 2) (276623514287 / 16000000000000) ≤ -(49716311348467284244491 / 10000000000000000000000)

theorem Zeta5Irrational.U_44_3 : Uω (aρ 3) (bρ 3) (276623514287 / 16000000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_44_4 : Uω (aρ 4) (bρ 4) (276623514287 / 16000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_44_5 : Uω (aρ 5) (bρ 5) (276623514287 / 16000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_44_6 : Uω (aρ 6) (bρ 6) (276623514287 / 16000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_44_7 : Uω (aρ 7) (bρ 7) (276623514287 / 16000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_44_8 : Uω (aρ 8) (bρ 8) (276623514287 / 16000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_44 : Uρ (276623514287 / 16000000000000) ≤ -(14118325055929443477217 / 5000000000000000000000)

theorem Zeta5Irrational.U_45_1 : Uω (aρ 1) (bρ 1) (563636211443 / 32000000000000) ≤ -(45083004919660055486503 / 10000000000000000000000)

theorem Zeta5Irrational.U_45_2 : Uω (aρ 2) (bρ 2) (563636211443 / 32000000000000) ≤ -(9828288768212480750473 / 2000000000000000000000)

theorem Zeta5Irrational.U_45_3 : Uω (aρ 3) (bρ 3) (563636211443 / 32000000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_45_4 : Uω (aρ 4) (bρ 4) (563636211443 / 32000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_45_5 : Uω (aρ 5) (bρ 5) (563636211443 / 32000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_45_6 : Uω (aρ 6) (bρ 6) (563636211443 / 32000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_45_7 : Uω (aρ 7) (bρ 7) (563636211443 / 32000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_45_8 : Uω (aρ 8) (bρ 8) (563636211443 / 32000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_45 : Uρ (563636211443 / 32000000000000) ≤ -(28216517921339449947509 / 10000000000000000000000)

theorem Zeta5Irrational.U_46_1 : Uω (aρ 1) (bρ 1) (71753174289 / 4000000000000) ≤ -(44788826203166347861371 / 10000000000000000000000)

theorem Zeta5Irrational.U_46_2 : Uω (aρ 2) (bρ 2) (71753174289 / 4000000000000) ≤ -(24306011407961759067497 / 5000000000000000000000)

theorem Zeta5Irrational.U_46_3 : Uω (aρ 3) (bρ 3) (71753174289 / 4000000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_46_4 : Uω (aρ 4) (bρ 4) (71753174289 / 4000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_46_5 : Uω (aρ 5) (bρ 5) (71753174289 / 4000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_46_6 : Uω (aρ 6) (bρ 6) (71753174289 / 4000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_46_7 : Uω (aρ 7) (bρ 7) (71753174289 / 4000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_46_8 : Uω (aρ 8) (bρ 8) (71753174289 / 4000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_46 : Uρ (71753174289 / 4000000000000) ≤ -(1762363843694816057143 / 625000000000000000000)

theorem Zeta5Irrational.U_47_1 : Uω (aρ 1) (bρ 1) (584414577181 / 32000000000000) ≤ -(4450326262908179514767 / 1000000000000000000000)

theorem Zeta5Irrational.U_47_2 : Uω (aρ 2) (bρ 2) (584414577181 / 32000000000000) ≤ -(48119922953915799270603 / 10000000000000000000000)

theorem Zeta5Irrational.U_47_3 : Uω (aρ 3) (bρ 3) (584414577181 / 32000000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_47_4 : Uω (aρ 4) (bρ 4) (584414577181 / 32000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_47_5 : Uω (aρ 5) (bρ 5) (584414577181 / 32000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_47_6 : Uω (aρ 6) (bρ 6) (584414577181 / 32000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_47_7 : Uω (aρ 7) (bρ 7) (584414577181 / 32000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_47_8 : Uω (aρ 8) (bρ 8) (584414577181 / 32000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_47 : Uρ (584414577181 / 32000000000000) ≤ -(14090157794893601635931 / 5000000000000000000000)

theorem Zeta5Irrational.U_48_1 : Uω (aρ 1) (bρ 1) (11896075201 / 640000000000) ≤ -(44225812907642607522863 / 10000000000000000000000)

theorem Zeta5Irrational.U_48_2 : Uω (aρ 2) (bρ 2) (11896075201 / 640000000000) ≤ -(47659199379596186942369 / 10000000000000000000000)

theorem Zeta5Irrational.U_48_3 : Uω (aρ 3) (bρ 3) (11896075201 / 640000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_48_4 : Uω (aρ 4) (bρ 4) (11896075201 / 640000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_48_5 : Uω (aρ 5) (bρ 5) (11896075201 / 640000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_48_6 : Uω (aρ 6) (bρ 6) (11896075201 / 640000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_48_7 : Uω (aρ 7) (bρ 7) (11896075201 / 640000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_48_8 : Uω (aρ 8) (bρ 8) (11896075201 / 640000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_48_9 : Uω (aρ 9) (bρ 9) (11896075201 / 640000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_48_10 : Uω (aρ 10) (bρ 10) (11896075201 / 640000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_48_11 : Uω (aρ 11) (bρ 11) (11896075201 / 640000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_48_12 : Uω (aρ 12) (bρ 12) (11896075201 / 640000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_48_13 : Uω (aρ 13) (bρ 13) (11896075201 / 640000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_48_14 : Uω (aρ 14) (bρ 14) (11896075201 / 640000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_48_15 : Uω (aρ 15) (bρ 15) (11896075201 / 640000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_48_16 : Uω (aρ 16) (bρ 16) (11896075201 / 640000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_48 : Uρ (11896075201 / 640000000000) ≤ -(28163819716178893923457 / 10000000000000000000000)

theorem Zeta5Irrational.U_49_1 : Uω (aρ 1) (bρ 1) (605192942919 / 32000000000000) ≤ -(21978009554983345102107 / 5000000000000000000000)

theorem Zeta5Irrational.U_49_2 : Uω (aρ 2) (bρ 2) (605192942919 / 32000000000000) ≤ -(47225342930112879030383 / 10000000000000000000000)

theorem Zeta5Irrational.U_49_3 : Uω (aρ 3) (bρ 3) (605192942919 / 32000000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_49_4 : Uω (aρ 4) (bρ 4) (605192942919 / 32000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_49_5 : Uω (aρ 5) (bρ 5) (605192942919 / 32000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_49_6 : Uω (aρ 6) (bρ 6) (605192942919 / 32000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_49_7 : Uω (aρ 7) (bρ 7) (605192942919 / 32000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_49_8 : Uω (aρ 8) (bρ 8) (605192942919 / 32000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_49 : Uρ (605192942919 / 32000000000000) ≤ -(28148196170031691353311 / 10000000000000000000000)

theorem Zeta5Irrational.U_50_1 : Uω (aρ 1) (bρ 1) (153895531447 / 8000000000000) ≤ -(10923365431073482723193 / 2500000000000000000000)

theorem Zeta5Irrational.U_50_2 : Uω (aρ 2) (bρ 2) (153895531447 / 8000000000000) ≤ -(182870446791635865959 / 39062500000000000000)

theorem Zeta5Irrational.U_50_3 : Uω (aρ 3) (bρ 3) (153895531447 / 8000000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_50_4 : Uω (aρ 4) (bρ 4) (153895531447 / 8000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_50_5 : Uω (aρ 5) (bρ 5) (153895531447 / 8000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_50_6 : Uω (aρ 6) (bρ 6) (153895531447 / 8000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_50_7 : Uω (aρ 7) (bρ 7) (153895531447 / 8000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_50_8 : Uω (aρ 8) (bρ 8) (153895531447 / 8000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_50 : Uρ (153895531447 / 8000000000000) ≤ -(28133336822199640692941 / 10000000000000000000000)

theorem Zeta5Irrational.U_51_1 : Uω (aρ 1) (bρ 1) (318180245763 / 16000000000000) ≤ -(21594272656989974022877 / 5000000000000000000000)

theorem Zeta5Irrational.U_51_2 : Uω (aρ 2) (bρ 2) (318180245763 / 16000000000000) ≤ -(9210627822742137523341 / 2000000000000000000000)

theorem Zeta5Irrational.U_51_3 : Uω (aρ 3) (bρ 3) (318180245763 / 16000000000000) ≤ -(25512130211755314637529 / 5000000000000000000000)

theorem Zeta5Irrational.U_51_4 : Uω (aρ 4) (bρ 4) (318180245763 / 16000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_51_5 : Uω (aρ 5) (bρ 5) (318180245763 / 16000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_51_6 : Uω (aρ 6) (bρ 6) (318180245763 / 16000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_51_7 : Uω (aρ 7) (bρ 7) (318180245763 / 16000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_51_8 : Uω (aρ 8) (bρ 8) (318180245763 / 16000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_51 : Uρ (318180245763 / 16000000000000) ≤ -(7026394710499350942541 / 2500000000000000000000)