Certified arcsine potential bounds (U10)

theorem Zeta5Irrational.U_124_1 : Uω (aρ 1) (bρ 1) (9605987655299 / 128000000000000) ≤ -(13399246969653145294021 / 5000000000000000000000)

theorem Zeta5Irrational.U_124_2 : Uω (aρ 2) (bρ 2) (9605987655299 / 128000000000000) ≤ -(27171986109213034869943 / 10000000000000000000000)

theorem Zeta5Irrational.U_124_3 : Uω (aρ 3) (bρ 3) (9605987655299 / 128000000000000) ≤ -(13994837736555882275651 / 5000000000000000000000)

theorem Zeta5Irrational.U_124_4 : Uω (aρ 4) (bρ 4) (9605987655299 / 128000000000000) ≤ -(14819930885633522672703 / 5000000000000000000000)

theorem Zeta5Irrational.U_124_5 : Uω (aρ 5) (bρ 5) (9605987655299 / 128000000000000) ≤ -(16906927768461829373233 / 5000000000000000000000)

theorem Zeta5Irrational.U_124_6 : Uω (aρ 6) (bρ 6) (9605987655299 / 128000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_124_7 : Uω (aρ 7) (bρ 7) (9605987655299 / 128000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_124_8 : Uω (aρ 8) (bρ 8) (9605987655299 / 128000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_124_9 : Uω (aρ 9) (bρ 9) (9605987655299 / 128000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_124_10 : Uω (aρ 10) (bρ 10) (9605987655299 / 128000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_124_11 : Uω (aρ 11) (bρ 11) (9605987655299 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_124_12 : Uω (aρ 12) (bρ 12) (9605987655299 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_124 : Uρ (9605987655299 / 128000000000000) ≤ -(24940524488693670762209 / 10000000000000000000000)

theorem Zeta5Irrational.U_125_1 : Uω (aρ 1) (bρ 1) (481980880181 / 6400000000000) ≤ -(6690059962646030184617 / 2500000000000000000000)

theorem Zeta5Irrational.U_125_2 : Uω (aρ 2) (bρ 2) (481980880181 / 6400000000000) ≤ -(1085287861694982018329 / 400000000000000000000)

theorem Zeta5Irrational.U_125_3 : Uω (aρ 3) (bρ 3) (481980880181 / 6400000000000) ≤ -(6986543959626957316373 / 2500000000000000000000)

theorem Zeta5Irrational.U_125_4 : Uω (aρ 4) (bρ 4) (481980880181 / 6400000000000) ≤ -(1849188452354571814583 / 625000000000000000000)

theorem Zeta5Irrational.U_125_5 : Uω (aρ 5) (bρ 5) (481980880181 / 6400000000000) ≤ -(33714249304541786608363 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_125 : Uρ (481980880181 / 6400000000000) ≤ -(12463564729009360759451 / 5000000000000000000000)

theorem Zeta5Irrational.U_126_1 : Uω (aρ 1) (bρ 1) (9673247551941 / 128000000000000) ≤ -(26722131641032751290407 / 10000000000000000000000)

theorem Zeta5Irrational.U_126_2 : Uω (aρ 2) (bρ 2) (9673247551941 / 128000000000000) ≤ -(3386570678593159343237 / 1250000000000000000000)

theorem Zeta5Irrational.U_126_3 : Uω (aρ 3) (bρ 3) (9673247551941 / 128000000000000) ≤ -(697571708901889533809 / 250000000000000000000)

theorem Zeta5Irrational.U_126_4 : Uω (aρ 4) (bρ 4) (9673247551941 / 128000000000000) ≤ -(2953446897992292134223 / 1000000000000000000000)

theorem Zeta5Irrational.U_126_5 : Uω (aρ 5) (bρ 5) (9673247551941 / 128000000000000) ≤ -(6723237936362052732691 / 2000000000000000000000)

theorem Zeta5Irrational.U_126_6 : Uω (aρ 6) (bρ 6) (9673247551941 / 128000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_126_7 : Uω (aρ 7) (bρ 7) (9673247551941 / 128000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_126_8 : Uω (aρ 8) (bρ 8) (9673247551941 / 128000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_126_9 : Uω (aρ 9) (bρ 9) (9673247551941 / 128000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_126_10 : Uω (aρ 10) (bρ 10) (9673247551941 / 128000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_126_11 : Uω (aρ 11) (bρ 11) (9673247551941 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_126_12 : Uω (aρ 12) (bρ 12) (9673247551941 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_126 : Uρ (9673247551941 / 128000000000000) ≤ -(6228468283187341352323 / 2500000000000000000000)

theorem Zeta5Irrational.U_127_1 : Uω (aρ 1) (bρ 1) (4853438750131 / 64000000000000) ≤ -(2668416820153121014947 / 1000000000000000000000)

theorem Zeta5Irrational.U_127_2 : Uω (aρ 2) (bρ 2) (4853438750131 / 64000000000000) ≤ -(13526545752678102531631 / 5000000000000000000000)

theorem Zeta5Irrational.U_127_3 : Uω (aρ 3) (bρ 3) (4853438750131 / 64000000000000) ≤ -(1392987565165561452741 / 500000000000000000000)

theorem Zeta5Irrational.U_127_4 : Uω (aρ 4) (bρ 4) (4853438750131 / 64000000000000) ≤ -(14741109681724341615633 / 5000000000000000000000)

theorem Zeta5Irrational.U_127_5 : Uω (aρ 5) (bρ 5) (4853438750131 / 64000000000000) ≤ -(33519615797620916311619 / 10000000000000000000000)

theorem Zeta5Irrational.U_127_6 : Uω (aρ 6) (bρ 6) (4853438750131 / 64000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_127_7 : Uω (aρ 7) (bρ 7) (4853438750131 / 64000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_127_8 : Uω (aρ 8) (bρ 8) (4853438750131 / 64000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_127_9 : Uω (aρ 9) (bρ 9) (4853438750131 / 64000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_127_10 : Uω (aρ 10) (bρ 10) (4853438750131 / 64000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_127_11 : Uω (aρ 11) (bρ 11) (4853438750131 / 64000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_127_12 : Uω (aρ 12) (bρ 12) (4853438750131 / 64000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_127 : Uρ (4853438750131 / 64000000000000) ≤ -(24900750976102301112917 / 10000000000000000000000)

theorem Zeta5Irrational.U_128_1 : Uω (aρ 1) (bρ 1) (1221767174613 / 16000000000000) ≤ -(5321734251810154824021 / 2000000000000000000000)

theorem Zeta5Irrational.U_128_2 : Uω (aρ 2) (bρ 2) (1221767174613 / 16000000000000) ≤ -(26974610252730626450719 / 10000000000000000000000)

theorem Zeta5Irrational.U_128_3 : Uω (aρ 3) (bρ 3) (1221767174613 / 16000000000000) ≤ -(27774081713696468351641 / 10000000000000000000000)

theorem Zeta5Irrational.U_128_4 : Uω (aρ 4) (bρ 4) (1221767174613 / 16000000000000) ≤ -(14689297930419472306447 / 5000000000000000000000)

theorem Zeta5Irrational.U_128_5 : Uω (aρ 5) (bρ 5) (1221767174613 / 16000000000000) ≤ -(33330701080104509943517 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_128 : Uρ (1221767174613 / 16000000000000) ≤ -(24874892383294093360151 / 10000000000000000000000)

theorem Zeta5Irrational.U_129_1 : Uω (aρ 1) (bρ 1) (4920698646773 / 64000000000000) ≤ -(26533740398960545318349 / 10000000000000000000000)

theorem Zeta5Irrational.U_129_2 : Uω (aρ 2) (bρ 2) (4920698646773 / 64000000000000) ≤ -(26896742978634930657697 / 10000000000000000000000)

theorem Zeta5Irrational.U_129_3 : Uω (aρ 3) (bρ 3) (4920698646773 / 64000000000000) ≤ -(27689153753963773397029 / 10000000000000000000000)

theorem Zeta5Irrational.U_129_4 : Uω (aρ 4) (bρ 4) (4920698646773 / 64000000000000) ≤ -(14638058503645561336247 / 5000000000000000000000)

theorem Zeta5Irrational.U_129_5 : Uω (aρ 5) (bρ 5) (4920698646773 / 64000000000000) ≤ -(8286772710427584474673 / 2500000000000000000000)

theorem Zeta5Irrational.U_129_6 : Uω (aρ 6) (bρ 6) (4920698646773 / 64000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_129_7 : Uω (aρ 7) (bρ 7) (4920698646773 / 64000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_129_8 : Uω (aρ 8) (bρ 8) (4920698646773 / 64000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_129_9 : Uω (aρ 9) (bρ 9) (4920698646773 / 64000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_129_10 : Uω (aρ 10) (bρ 10) (4920698646773 / 64000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_129_11 : Uω (aρ 11) (bρ 11) (4920698646773 / 64000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_129_12 : Uω (aρ 12) (bρ 12) (4920698646773 / 64000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_129 : Uρ (4920698646773 / 64000000000000) ≤ -(12424761255821240445021 / 5000000000000000000000)

theorem Zeta5Irrational.U_130_1 : Uω (aρ 1) (bρ 1) (2477164297547 / 32000000000000) ≤ -(5291873437976526183487 / 2000000000000000000000)

theorem Zeta5Irrational.U_130_2 : Uω (aρ 2) (bρ 2) (2477164297547 / 32000000000000) ≤ -(26819480107653810847137 / 10000000000000000000000)

theorem Zeta5Irrational.U_130_3 : Uω (aρ 3) (bρ 3) (2477164297547 / 32000000000000) ≤ -(13802477227999504398421 / 5000000000000000000000)

theorem Zeta5Irrational.U_130_4 : Uω (aρ 4) (bρ 4) (2477164297547 / 32000000000000) ≤ -(5834951221022183615197 / 2000000000000000000000)

theorem Zeta5Irrational.U_130_5 : Uω (aρ 5) (bρ 5) (2477164297547 / 32000000000000) ≤ -(8242104744242823723913 / 2500000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_130 : Uρ (2477164297547 / 32000000000000) ≤ -(24824613604535232933069 / 10000000000000000000000)

theorem Zeta5Irrational.U_131_1 : Uω (aρ 1) (bρ 1) (997591708683 / 12800000000000) ≤ -(26385543387535192161299 / 10000000000000000000000)

theorem Zeta5Irrational.U_131_2 : Uω (aρ 2) (bρ 2) (997591708683 / 12800000000000) ≤ -(1069712491504947096903 / 400000000000000000000)

theorem Zeta5Irrational.U_131_3 : Uω (aρ 3) (bρ 3) (997591708683 / 12800000000000) ≤ -(27521471202141578539429 / 10000000000000000000000)

theorem Zeta5Irrational.U_131_4 : Uω (aρ 4) (bρ 4) (997591708683 / 12800000000000) ≤ -(1453724371476601447869 / 500000000000000000000)

theorem Zeta5Irrational.U_131_5 : Uω (aρ 5) (bρ 5) (997591708683 / 12800000000000) ≤ -(32794360034669585926951 / 10000000000000000000000)

theorem Zeta5Irrational.U_131_6 : Uω (aρ 6) (bρ 6) (997591708683 / 12800000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_131_7 : Uω (aρ 7) (bρ 7) (997591708683 / 12800000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_131_8 : Uω (aρ 8) (bρ 8) (997591708683 / 12800000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_131_9 : Uω (aρ 9) (bρ 9) (997591708683 / 12800000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_131_10 : Uω (aρ 10) (bρ 10) (997591708683 / 12800000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_131_11 : Uω (aρ 11) (bρ 11) (997591708683 / 12800000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_131_12 : Uω (aρ 12) (bρ 12) (997591708683 / 12800000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_131_13 : Uω (aρ 13) (bρ 13) (997591708683 / 12800000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_131_14 : Uω (aρ 14) (bρ 14) (997591708683 / 12800000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

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

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

theorem Zeta5Irrational.U_131 : Uρ (997591708683 / 12800000000000) ≤ -(49600281584509713859 / 20000000000000000000)

theorem Zeta5Irrational.U_132_1 : Uω (aρ 1) (bρ 1) (627698561467 / 8000000000000) ≤ -(5262452185846792494703 / 2000000000000000000000)

theorem Zeta5Irrational.U_132_2 : Uω (aρ 2) (bρ 2) (627698561467 / 8000000000000) ≤ -(6666682595679150360093 / 2500000000000000000000)

theorem Zeta5Irrational.U_132_3 : Uω (aρ 3) (bρ 3) (627698561467 / 8000000000000) ≤ -(3429836462828796430307 / 1250000000000000000000)

theorem Zeta5Irrational.U_132_4 : Uω (aρ 4) (bρ 4) (627698561467 / 8000000000000) ≤ -(28975286180128640663519 / 10000000000000000000000)

theorem Zeta5Irrational.U_132_5 : Uω (aρ 5) (bρ 5) (627698561467 / 8000000000000) ≤ -(32624623126546358520591 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_132 : Uρ (627698561467 / 8000000000000) ≤ -(24776081667392410080527 / 10000000000000000000000)

theorem Zeta5Irrational.U_133_1 : Uω (aρ 1) (bρ 1) (5055218440057 / 64000000000000) ≤ -(5247902385718883216969 / 2000000000000000000000)

theorem Zeta5Irrational.U_133_2 : Uω (aρ 2) (bρ 2) (5055218440057 / 64000000000000) ≤ -(5318245093358236445799 / 2000000000000000000000)

theorem Zeta5Irrational.U_133_3 : Uω (aρ 3) (bρ 3) (5055218440057 / 64000000000000) ≤ -(27356603986588711129289 / 10000000000000000000000)

theorem Zeta5Irrational.U_133_4 : Uω (aρ 4) (bρ 4) (5055218440057 / 64000000000000) ≤ -(14438564217655403680117 / 5000000000000000000000)

theorem Zeta5Irrational.U_133_5 : Uω (aρ 5) (bρ 5) (5055218440057 / 64000000000000) ≤ -(4057368370546522140043 / 1250000000000000000000)

theorem Zeta5Irrational.U_133_6 : Uω (aρ 6) (bρ 6) (5055218440057 / 64000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_133_7 : Uω (aρ 7) (bρ 7) (5055218440057 / 64000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_133_8 : Uω (aρ 8) (bρ 8) (5055218440057 / 64000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_133_9 : Uω (aρ 9) (bρ 9) (5055218440057 / 64000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_133_10 : Uω (aρ 10) (bρ 10) (5055218440057 / 64000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_133_11 : Uω (aρ 11) (bρ 11) (5055218440057 / 64000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_133_12 : Uω (aρ 12) (bρ 12) (5055218440057 / 64000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_133 : Uρ (5055218440057 / 64000000000000) ≤ -(24752415938931362015277 / 10000000000000000000000)

theorem Zeta5Irrational.U_134_1 : Uω (aρ 1) (bρ 1) (2544424194189 / 32000000000000) ≤ -(26167288670425871360889 / 10000000000000000000000)

theorem Zeta5Irrational.U_134_2 : Uω (aρ 2) (bρ 2) (2544424194189 / 32000000000000) ≤ -(26516288816997824638059 / 10000000000000000000000)

theorem Zeta5Irrational.U_134_3 : Uω (aρ 3) (bρ 3) (2544424194189 / 32000000000000) ≤ -(2727519639092246926631 / 1000000000000000000000)

theorem Zeta5Irrational.U_134_4 : Uω (aρ 4) (bρ 4) (2544424194189 / 32000000000000) ≤ -(28779991109665995308087 / 10000000000000000000000)

theorem Zeta5Irrational.U_134_5 : Uω (aρ 5) (bρ 5) (2544424194189 / 32000000000000) ≤ -(16148547889847596668857 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_134 : Uρ (2544424194189 / 32000000000000) ≤ -(6182281286838750952367 / 2500000000000000000000)

theorem Zeta5Irrational.U_135_1 : Uω (aρ 1) (bρ 1) (5122478336699 / 64000000000000) ≤ -(13047791802904571252103 / 5000000000000000000000)

theorem Zeta5Irrational.U_135_2 : Uω (aρ 2) (bρ 2) (5122478336699 / 64000000000000) ≤ -(13220955953813518373719 / 5000000000000000000000)

theorem Zeta5Irrational.U_135_3 : Uω (aρ 3) (bρ 3) (5122478336699 / 64000000000000) ≤ -(13597228774851769235177 / 5000000000000000000000)

theorem Zeta5Irrational.U_135_4 : Uω (aρ 4) (bρ 4) (5122478336699 / 64000000000000) ≤ -(7170962978482870943403 / 2500000000000000000000)

theorem Zeta5Irrational.U_135_5 : Uω (aρ 5) (bρ 5) (5122478336699 / 64000000000000) ≤ -(6427771188288008699121 / 2000000000000000000000)

theorem Zeta5Irrational.U_135_6 : Uω (aρ 6) (bρ 6) (5122478336699 / 64000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_135_7 : Uω (aρ 7) (bρ 7) (5122478336699 / 64000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_135_8 : Uω (aρ 8) (bρ 8) (5122478336699 / 64000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_135_9 : Uω (aρ 9) (bρ 9) (5122478336699 / 64000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_135_10 : Uω (aρ 10) (bρ 10) (5122478336699 / 64000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_135_11 : Uω (aρ 11) (bρ 11) (5122478336699 / 64000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_135_12 : Uω (aρ 12) (bρ 12) (5122478336699 / 64000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_135 : Uρ (5122478336699 / 64000000000000) ≤ -(3088274053514358657371 / 1250000000000000000000)