Certified arcsine potential bounds (U15)

theorem Zeta5Irrational.U_184_1 : Uω (aρ 1) (bρ 1) (1972876467523 / 16000000000000) ≤ -(10734696757160727232713 / 5000000000000000000000)

theorem Zeta5Irrational.U_184_2 : Uω (aρ 2) (bρ 2) (1972876467523 / 16000000000000) ≤ -(10840908887218247258763 / 5000000000000000000000)

theorem Zeta5Irrational.U_184_3 : Uω (aρ 3) (bρ 3) (1972876467523 / 16000000000000) ≤ -(11063702462299722560483 / 5000000000000000000000)

theorem Zeta5Irrational.U_184_4 : Uω (aρ 4) (bρ 4) (1972876467523 / 16000000000000) ≤ -(22939613024631683193711 / 10000000000000000000000)

theorem Zeta5Irrational.U_184_5 : Uω (aρ 5) (bρ 5) (1972876467523 / 16000000000000) ≤ -(4882994056373813382959 / 2000000000000000000000)

theorem Zeta5Irrational.U_184_6 : Uω (aρ 6) (bρ 6) (1972876467523 / 16000000000000) ≤ -(13764778325010343518127 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_184 : Uρ (1972876467523 / 16000000000000) ≤ -(11343342076695662676383 / 5000000000000000000000)

theorem Zeta5Irrational.U_185_1 : Uω (aρ 1) (bρ 1) (199529881231 / 1600000000000) ≤ -(4270030594954638318783 / 2000000000000000000000)

theorem Zeta5Irrational.U_185_2 : Uω (aρ 2) (bρ 2) (199529881231 / 1600000000000) ≤ -(21559949844423918091557 / 10000000000000000000000)

theorem Zeta5Irrational.U_185_3 : Uω (aρ 3) (bρ 3) (199529881231 / 1600000000000) ≤ -(21999733418108408918803 / 10000000000000000000000)

theorem Zeta5Irrational.U_185_4 : Uω (aρ 4) (bρ 4) (199529881231 / 1600000000000) ≤ -(22800221341664611774923 / 10000000000000000000000)

theorem Zeta5Irrational.U_185_5 : Uω (aρ 5) (bρ 5) (199529881231 / 1600000000000) ≤ -(24249554734050633766169 / 10000000000000000000000)

theorem Zeta5Irrational.U_185_6 : Uω (aρ 6) (bρ 6) (199529881231 / 1600000000000) ≤ -(5454999569515305561689 / 2000000000000000000000)

theorem Zeta5Irrational.U_185_7 : Uω (aρ 7) (bρ 7) (199529881231 / 1600000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_185_8 : Uω (aρ 8) (bρ 8) (199529881231 / 1600000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_185_9 : Uω (aρ 9) (bρ 9) (199529881231 / 1600000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_185_10 : Uω (aρ 10) (bρ 10) (199529881231 / 1600000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_185_11 : Uω (aρ 11) (bρ 11) (199529881231 / 1600000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_185_12 : Uω (aρ 12) (bρ 12) (199529881231 / 1600000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_185_13 : Uω (aρ 13) (bρ 13) (199529881231 / 1600000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_185_14 : Uω (aρ 14) (bρ 14) (199529881231 / 1600000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_185_15 : Uω (aρ 15) (bρ 15) (199529881231 / 1600000000000) ≤ -(268788866070650094343 / 156250000000000000000)

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

theorem Zeta5Irrational.U_185 : Uρ (199529881231 / 1600000000000) ≤ -(2829593273725598213717 / 1250000000000000000000)

theorem Zeta5Irrational.U_186_1 : Uω (aρ 1) (bρ 1) (2017721157097 / 16000000000000) ≤ -(2654039731137533813037 / 1250000000000000000000)

theorem Zeta5Irrational.U_186_2 : Uω (aρ 2) (bρ 2) (2017721157097 / 16000000000000) ≤ -(4287910305227927671211 / 2000000000000000000000)

theorem Zeta5Irrational.U_186_3 : Uω (aρ 3) (bρ 3) (2017721157097 / 16000000000000) ≤ -(21873680991519987290401 / 10000000000000000000000)

theorem Zeta5Irrational.U_186_4 : Uω (aρ 4) (bρ 4) (2017721157097 / 16000000000000) ≤ -(22662784376969185616087 / 10000000000000000000000)

theorem Zeta5Irrational.U_186_5 : Uω (aρ 5) (bρ 5) (2017721157097 / 16000000000000) ≤ -(4817403452281815741051 / 2000000000000000000000)

theorem Zeta5Irrational.U_186_6 : Uω (aρ 6) (bρ 6) (2017721157097 / 16000000000000) ≤ -(27028809110634695454701 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_186 : Uρ (2017721157097 / 16000000000000) ≤ -(5646977118127164902371 / 2500000000000000000000)

theorem Zeta5Irrational.U_187_1 : Uω (aρ 1) (bρ 1) (510035875471 / 4000000000000) ≤ -(10557927693038472750489 / 5000000000000000000000)

theorem Zeta5Irrational.U_187_2 : Uω (aρ 2) (bρ 2) (510035875471 / 4000000000000) ≤ -(21320587743862525124249 / 10000000000000000000000)

theorem Zeta5Irrational.U_187_3 : Uω (aρ 3) (bρ 3) (510035875471 / 4000000000000) ≤ -(4349841371920999492129 / 2000000000000000000000)

theorem Zeta5Irrational.U_187_4 : Uω (aρ 4) (bρ 4) (510035875471 / 4000000000000) ≤ -(28159058803363137901 / 12500000000000000000)

theorem Zeta5Irrational.U_187_5 : Uω (aρ 5) (bρ 5) (510035875471 / 4000000000000) ≤ -(11963626737311393197339 / 5000000000000000000000)

theorem Zeta5Irrational.U_187_6 : Uω (aρ 6) (bρ 6) (510035875471 / 4000000000000) ≤ -(13395175617456387926221 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_187 : Uρ (510035875471 / 4000000000000) ≤ -(22540107043114398128433 / 10000000000000000000000)

theorem Zeta5Irrational.U_188_1 : Uω (aρ 1) (bρ 1) (1042494095729 / 8000000000000) ≤ -(2088692305103148942643 / 1000000000000000000000)

theorem Zeta5Irrational.U_188_2 : Uω (aρ 2) (bρ 2) (1042494095729 / 8000000000000) ≤ -(5271707410071795261109 / 2500000000000000000000)

theorem Zeta5Irrational.U_188_3 : Uω (aρ 3) (bρ 3) (1042494095729 / 8000000000000) ≤ -(4300967582928605563113 / 2000000000000000000000)

theorem Zeta5Irrational.U_188_4 : Uω (aρ 4) (bρ 4) (1042494095729 / 8000000000000) ≤ -(22261662463063795315849 / 10000000000000000000000)

theorem Zeta5Irrational.U_188_5 : Uω (aρ 5) (bρ 5) (1042494095729 / 8000000000000) ≤ -(23615658202251705360119 / 10000000000000000000000)

theorem Zeta5Irrational.U_188_6 : Uω (aρ 6) (bρ 6) (1042494095729 / 8000000000000) ≤ -(329180582000059646687 / 125000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_188 : Uρ (1042494095729 / 8000000000000) ≤ -(22447390042549224808151 / 10000000000000000000000)

theorem Zeta5Irrational.U_189_1 : Uω (aρ 1) (bρ 1) (266229110129 / 2000000000000) ≤ -(20663115692318653602647 / 10000000000000000000000)

theorem Zeta5Irrational.U_189_2 : Uω (aρ 2) (bρ 2) (266229110129 / 2000000000000) ≤ -(20858418761046195439279 / 10000000000000000000000)

theorem Zeta5Irrational.U_189_3 : Uω (aρ 3) (bρ 3) (266229110129 / 2000000000000) ≤ -(4253265914535006292877 / 2000000000000000000000)

theorem Zeta5Irrational.U_189_4 : Uω (aρ 4) (bρ 4) (266229110129 / 2000000000000) ≤ -(22003071308913592837197 / 10000000000000000000000)

theorem Zeta5Irrational.U_189_5 : Uω (aρ 5) (bρ 5) (266229110129 / 2000000000000) ≤ -(11657021536339170325913 / 5000000000000000000000)

theorem Zeta5Irrational.U_189_6 : Uω (aρ 6) (bρ 6) (266229110129 / 2000000000000) ≤ -(25903511253721066404459 / 10000000000000000000000)

theorem Zeta5Irrational.U_189_7 : Uω (aρ 7) (bρ 7) (266229110129 / 2000000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_189_8 : Uω (aρ 8) (bρ 8) (266229110129 / 2000000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_189_9 : Uω (aρ 9) (bρ 9) (266229110129 / 2000000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_189_10 : Uω (aρ 10) (bρ 10) (266229110129 / 2000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_189_11 : Uω (aρ 11) (bρ 11) (266229110129 / 2000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_189_12 : Uω (aρ 12) (bρ 12) (266229110129 / 2000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_189_13 : Uω (aρ 13) (bρ 13) (266229110129 / 2000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_189_14 : Uω (aρ 14) (bρ 14) (266229110129 / 2000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_189_15 : Uω (aρ 15) (bρ 15) (266229110129 / 2000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_189_16 : Uω (aρ 16) (bρ 16) (266229110129 / 2000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_189 : Uρ (266229110129 / 2000000000000) ≤ -(11179100805596847419571 / 5000000000000000000000)

theorem Zeta5Irrational.U_190_1 : Uω (aρ 1) (bρ 1) (110976113009 / 800000000000) ≤ -(20229992373945278136929 / 10000000000000000000000)

theorem Zeta5Irrational.U_190_2 : Uω (aρ 2) (bρ 2) (110976113009 / 800000000000) ≤ -(20416696451517995856967 / 10000000000000000000000)

theorem Zeta5Irrational.U_190_3 : Uω (aρ 3) (bρ 3) (110976113009 / 800000000000) ≤ -(2080581013886745405213 / 1000000000000000000000)

theorem Zeta5Irrational.U_190_4 : Uω (aρ 4) (bρ 4) (110976113009 / 800000000000) ≤ -(21505438446981235916047 / 10000000000000000000000)

theorem Zeta5Irrational.U_190_5 : Uω (aρ 5) (bρ 5) (110976113009 / 800000000000) ≤ -(4547642411201558481751 / 2000000000000000000000)

theorem Zeta5Irrational.U_190_6 : Uω (aρ 6) (bρ 6) (110976113009 / 800000000000) ≤ -(25105050925041415667209 / 10000000000000000000000)

theorem Zeta5Irrational.U_190_7 : Uω (aρ 7) (bρ 7) (110976113009 / 800000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_190_8 : Uω (aρ 8) (bρ 8) (110976113009 / 800000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_190_9 : Uω (aρ 9) (bρ 9) (110976113009 / 800000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_190_10 : Uω (aρ 10) (bρ 10) (110976113009 / 800000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_190_11 : Uω (aρ 11) (bρ 11) (110976113009 / 800000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_190_12 : Uω (aρ 12) (bρ 12) (110976113009 / 800000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_190_13 : Uω (aρ 13) (bρ 13) (110976113009 / 800000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_190_14 : Uω (aρ 14) (bρ 14) (110976113009 / 800000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_190_15 : Uω (aρ 15) (bρ 15) (110976113009 / 800000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_190_16 : Uω (aρ 16) (bρ 16) (110976113009 / 800000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_190 : Uρ (110976113009 / 800000000000) ≤ -(11094580622395912739221 / 5000000000000000000000)

theorem Zeta5Irrational.U_191_1 : Uω (aρ 1) (bρ 1) (72162863729 / 500000000000) ≤ -(19814855621105804326481 / 10000000000000000000000)

theorem Zeta5Irrational.U_191_2 : Uω (aρ 2) (bρ 2) (72162863729 / 500000000000) ≤ -(19993685957203362780097 / 10000000000000000000000)

theorem Zeta5Irrational.U_191_3 : Uω (aρ 3) (bρ 3) (72162863729 / 500000000000) ≤ -(10182830255675675289117 / 5000000000000000000000)

theorem Zeta5Irrational.U_191_4 : Uω (aρ 4) (bρ 4) (72162863729 / 500000000000) ≤ -(2628969020630553055031 / 1250000000000000000000)

theorem Zeta5Irrational.U_191_5 : Uω (aρ 5) (bρ 5) (72162863729 / 500000000000) ≤ -(22195271732922818939507 / 10000000000000000000000)

theorem Zeta5Irrational.U_191_6 : Uω (aρ 6) (bρ 6) (72162863729 / 500000000000) ≤ -(24376790840821149583193 / 10000000000000000000000)

theorem Zeta5Irrational.U_191_7 : Uω (aρ 7) (bρ 7) (72162863729 / 500000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_191_8 : Uω (aρ 8) (bρ 8) (72162863729 / 500000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_191_9 : Uω (aρ 9) (bρ 9) (72162863729 / 500000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_191_10 : Uω (aρ 10) (bρ 10) (72162863729 / 500000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_191_11 : Uω (aρ 11) (bρ 11) (72162863729 / 500000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_191_12 : Uω (aρ 12) (bρ 12) (72162863729 / 500000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_191_13 : Uω (aρ 13) (bρ 13) (72162863729 / 500000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_191_14 : Uω (aρ 14) (bρ 14) (72162863729 / 500000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_191_15 : Uω (aρ 15) (bρ 15) (72162863729 / 500000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_191_16 : Uω (aρ 16) (bρ 16) (72162863729 / 500000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_191 : Uρ (72162863729 / 500000000000) ≤ -(22030937450651269436371 / 10000000000000000000000)

theorem Zeta5Irrational.U_192_1 : Uω (aρ 1) (bρ 1) (4675203313927 / 32000000000000) ≤ -(787478463849348170387 / 400000000000000000000)

theorem Zeta5Irrational.U_192_2 : Uω (aρ 2) (bρ 2) (4675203313927 / 32000000000000) ≤ -(19863436151075893595487 / 10000000000000000000000)

theorem Zeta5Irrational.U_192_3 : Uω (aρ 3) (bρ 3) (4675203313927 / 32000000000000) ≤ -(4046059230732191981441 / 2000000000000000000000)

theorem Zeta5Irrational.U_192_4 : Uω (aρ 4) (bρ 4) (4675203313927 / 32000000000000) ≤ -(20886435181837476410703 / 10000000000000000000000)

theorem Zeta5Irrational.U_192_5 : Uω (aρ 5) (bρ 5) (4675203313927 / 32000000000000) ≤ -(22029650929542333847147 / 10000000000000000000000)

theorem Zeta5Irrational.U_192_6 : Uω (aρ 6) (bρ 6) (4675203313927 / 32000000000000) ≤ -(19326993602285207127 / 8000000000000000000)

theorem Zeta5Irrational.U_192_7 : Uω (aρ 7) (bρ 7) (4675203313927 / 32000000000000) ≤ -(969506853701683875103 / 312500000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_192 : Uρ (4675203313927 / 32000000000000) ≤ -(21794875057781414112513 / 10000000000000000000000)

theorem Zeta5Irrational.U_193_1 : Uω (aρ 1) (bρ 1) (2365991674599 / 16000000000000) ≤ -(19560682890171164556221 / 10000000000000000000000)

theorem Zeta5Irrational.U_193_2 : Uω (aρ 2) (bρ 2) (2365991674599 / 16000000000000) ≤ -(394697258427317257959 / 200000000000000000000)

theorem Zeta5Irrational.U_193_3 : Uω (aρ 3) (bρ 3) (2365991674599 / 16000000000000) ≤ -(2512093407885480065093 / 1250000000000000000000)

theorem Zeta5Irrational.U_193_4 : Uω (aρ 4) (bρ 4) (2365991674599 / 16000000000000) ≤ -(10371614014328306359131 / 5000000000000000000000)

theorem Zeta5Irrational.U_193_5 : Uω (aρ 5) (bρ 5) (2365991674599 / 16000000000000) ≤ -(5466711720418222399723 / 2500000000000000000000)

theorem Zeta5Irrational.U_193_6 : Uω (aρ 6) (bρ 6) (2365991674599 / 16000000000000) ≤ -(23946103601804326428943 / 10000000000000000000000)

theorem Zeta5Irrational.U_193_7 : Uω (aρ 7) (bρ 7) (2365991674599 / 16000000000000) ≤ -(752824408466949677751 / 250000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_193 : Uρ (2365991674599 / 16000000000000) ≤ -(21670353188008540621837 / 10000000000000000000000)

theorem Zeta5Irrational.U_194_1 : Uω (aρ 1) (bρ 1) (4788763384469 / 32000000000000) ≤ -(3887195840299343045543 / 2000000000000000000000)

theorem Zeta5Irrational.U_194_2 : Uω (aρ 2) (bρ 2) (4788763384469 / 32000000000000) ≤ -(1960792360803155468861 / 1000000000000000000000)

theorem Zeta5Irrational.U_194_3 : Uω (aρ 3) (bρ 3) (4788763384469 / 32000000000000) ≤ -(19964965591887264809447 / 10000000000000000000000)

theorem Zeta5Irrational.U_194_4 : Uω (aρ 4) (bρ 4) (4788763384469 / 32000000000000) ≤ -(20602069529176842578973 / 10000000000000000000000)

theorem Zeta5Irrational.U_194_5 : Uω (aρ 5) (bρ 5) (4788763384469 / 32000000000000) ≤ -(21706761635276424051639 / 10000000000000000000000)

theorem Zeta5Irrational.U_194_6 : Uω (aρ 6) (bρ 6) (4788763384469 / 32000000000000) ≤ -(4747716261870926325079 / 2000000000000000000000)

theorem Zeta5Irrational.U_194_7 : Uω (aρ 7) (bρ 7) (4788763384469 / 32000000000000) ≤ -(14708997966031985063453 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_194 : Uρ (4788763384469 / 32000000000000) ≤ -(10782516787768049362653 / 5000000000000000000000)

theorem Zeta5Irrational.U_195_1 : Uω (aρ 1) (bρ 1) (9634306804209 / 64000000000000) ≤ -(1210887862743762534847 / 625000000000000000000)

theorem Zeta5Irrational.U_195_2 : Uω (aρ 2) (bρ 2) (9634306804209 / 64000000000000) ≤ -(977252689052743997793 / 500000000000000000000)

theorem Zeta5Irrational.U_195_3 : Uω (aρ 3) (bρ 3) (9634306804209 / 64000000000000) ≤ -(9949861454974666734381 / 5000000000000000000000)

theorem Zeta5Irrational.U_195_4 : Uω (aρ 4) (bρ 4) (9634306804209 / 64000000000000) ≤ -(20532240139569703071389 / 10000000000000000000000)

theorem Zeta5Irrational.U_195_5 : Uω (aρ 5) (bρ 5) (9634306804209 / 64000000000000) ≤ -(21627709382413351683267 / 10000000000000000000000)

theorem Zeta5Irrational.U_195_6 : Uω (aρ 6) (bρ 6) (9634306804209 / 64000000000000) ≤ -(5909163429288754127091 / 2500000000000000000000)

theorem Zeta5Irrational.U_195_7 : Uω (aρ 7) (bρ 7) (9634306804209 / 64000000000000) ≤ -(2911592179000382039081 / 1000000000000000000000)

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_195 : Uρ (9634306804209 / 64000000000000) ≤ -(21516535824810612976769 / 10000000000000000000000)