Certified arcsine potential bounds (U05)

theorem Zeta5Irrational.U_64_1 : Uω (aρ 1) (bρ 1) (944711264583 / 32000000000000) ≤ -(18860822371165874400701 / 5000000000000000000000)

theorem Zeta5Irrational.U_64_2 : Uω (aρ 2) (bρ 2) (944711264583 / 32000000000000) ≤ -(19517893536797811818607 / 5000000000000000000000)

theorem Zeta5Irrational.U_64_3 : Uω (aρ 3) (bρ 3) (944711264583 / 32000000000000) ≤ -(21660038294705195113549 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_64 : Uρ (944711264583 / 32000000000000) ≤ -(5502100664475844411457 / 2000000000000000000000)

theorem Zeta5Irrational.U_65_1 : Uω (aρ 1) (bρ 1) (59550060209 / 2000000000000) ≤ -(37612010995240153131751 / 10000000000000000000000)

theorem Zeta5Irrational.U_65_2 : Uω (aρ 2) (bρ 2) (59550060209 / 2000000000000) ≤ -(7781591291438441479693 / 2000000000000000000000)

theorem Zeta5Irrational.U_65_3 : Uω (aρ 3) (bρ 3) (59550060209 / 2000000000000) ≤ -(43079747104388786598999 / 10000000000000000000000)

theorem Zeta5Irrational.U_65_4 : Uω (aρ 4) (bρ 4) (59550060209 / 2000000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_65_5 : Uω (aρ 5) (bρ 5) (59550060209 / 2000000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_65_6 : Uω (aρ 6) (bρ 6) (59550060209 / 2000000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_65 : Uρ (59550060209 / 2000000000000) ≤ -(13747632336952287678791 / 5000000000000000000000)

theorem Zeta5Irrational.U_66_1 : Uω (aρ 1) (bρ 1) (192178132421 / 6400000000000) ≤ -(37503573233468039420779 / 10000000000000000000000)

theorem Zeta5Irrational.U_66_2 : Uω (aρ 2) (bρ 2) (192178132421 / 6400000000000) ≤ -(4847727796490385371113 / 1250000000000000000000)

theorem Zeta5Irrational.U_66_3 : Uω (aρ 3) (bρ 3) (192178132421 / 6400000000000) ≤ -(42847853324868564028227 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_66 : Uρ (192178132421 / 6400000000000) ≤ -(13740225391654598492339 / 5000000000000000000000)

theorem Zeta5Irrational.U_67_1 : Uω (aρ 1) (bρ 1) (484490180433 / 16000000000000) ≤ -(37396305496047393699967 / 10000000000000000000000)

theorem Zeta5Irrational.U_67_2 : Uω (aρ 2) (bρ 2) (484490180433 / 16000000000000) ≤ -(19328669154765280711259 / 5000000000000000000000)

theorem Zeta5Irrational.U_67_3 : Uω (aρ 3) (bρ 3) (484490180433 / 16000000000000) ≤ -(1704947106755531654199 / 400000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_67 : Uρ (484490180433 / 16000000000000) ≤ -(27466029197992934502529 / 10000000000000000000000)

theorem Zeta5Irrational.U_68_1 : Uω (aρ 1) (bρ 1) (977070059627 / 32000000000000) ≤ -(37290182662862082118669 / 10000000000000000000000)

theorem Zeta5Irrational.U_68_2 : Uω (aρ 2) (bρ 2) (977070059627 / 32000000000000) ≤ -(19267229861265618418229 / 5000000000000000000000)

theorem Zeta5Irrational.U_68_3 : Uω (aρ 3) (bρ 3) (977070059627 / 32000000000000) ≤ -(42406599719954955895771 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_68 : Uρ (977070059627 / 32000000000000) ≤ -(27451971703722815927747 / 10000000000000000000000)

theorem Zeta5Irrational.U_69_1 : Uω (aρ 1) (bρ 1) (246289939597 / 8000000000000) ≤ -(37185180418532968481481 / 10000000000000000000000)

theorem Zeta5Irrational.U_69_2 : Uω (aρ 2) (bρ 2) (246289939597 / 8000000000000) ≤ -(4801642989010586665173 / 1250000000000000000000)

theorem Zeta5Irrational.U_69_3 : Uω (aρ 3) (bρ 3) (246289939597 / 8000000000000) ≤ -(10549019659401938900341 / 2500000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_69 : Uρ (246289939597 / 8000000000000) ≤ -(27438253565757300111681 / 10000000000000000000000)

theorem Zeta5Irrational.U_70_1 : Uω (aρ 1) (bρ 1) (100133915591 / 3200000000000) ≤ -(7395688851059352324481 / 2000000000000000000000)

theorem Zeta5Irrational.U_70_2 : Uω (aρ 2) (bρ 2) (100133915591 / 3200000000000) ≤ -(3817503845189056183093 / 1000000000000000000000)

theorem Zeta5Irrational.U_70_3 : Uω (aρ 3) (bρ 3) (100133915591 / 3200000000000) ≤ -(2612053898144625343839 / 625000000000000000000)

theorem Zeta5Irrational.U_70_4 : Uω (aρ 4) (bρ 4) (100133915591 / 3200000000000) ≤ -(11449496158609380585237 / 2500000000000000000000)

theorem Zeta5Irrational.U_70_5 : Uω (aρ 5) (bρ 5) (100133915591 / 3200000000000) ≤ -(20577364119368339121527 / 5000000000000000000000)

theorem Zeta5Irrational.U_70_6 : Uω (aρ 6) (bρ 6) (100133915591 / 3200000000000) ≤ -(3698074464695343529243 / 1000000000000000000000)

theorem Zeta5Irrational.U_70_7 : Uω (aρ 7) (bρ 7) (100133915591 / 3200000000000) ≤ -(33239459906384759787341 / 10000000000000000000000)

theorem Zeta5Irrational.U_70_8 : Uω (aρ 8) (bρ 8) (100133915591 / 3200000000000) ≤ -(14956372202312055299661 / 5000000000000000000000)

theorem Zeta5Irrational.U_70_9 : Uω (aρ 9) (bρ 9) (100133915591 / 3200000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_70_10 : Uω (aρ 10) (bρ 10) (100133915591 / 3200000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_70_11 : Uω (aρ 11) (bρ 11) (100133915591 / 3200000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_70_12 : Uω (aρ 12) (bρ 12) (100133915591 / 3200000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_70_13 : Uω (aρ 13) (bρ 13) (100133915591 / 3200000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_70_14 : Uω (aρ 14) (bρ 14) (100133915591 / 3200000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_70_15 : Uω (aρ 15) (bρ 15) (100133915591 / 3200000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_70_16 : Uω (aρ 16) (bρ 16) (100133915591 / 3200000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_70 : Uρ (100133915591 / 3200000000000) ≤ -(685293759890628417919 / 250000000000000000000)

theorem Zeta5Irrational.U_71_1 : Uω (aρ 1) (bρ 1) (127189819179 / 4000000000000) ≤ -(18387958661588722880311 / 5000000000000000000000)

theorem Zeta5Irrational.U_71_2 : Uω (aρ 2) (bρ 2) (127189819179 / 4000000000000) ≤ -(7588542707518441531123 / 2000000000000000000000)

theorem Zeta5Irrational.U_71_3 : Uω (aρ 3) (bρ 3) (127189819179 / 4000000000000) ≤ -(1656433616878713809077 / 400000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_71 : Uρ (127189819179 / 4000000000000) ≤ -(13693185907714144032147 / 5000000000000000000000)

theorem Zeta5Irrational.U_72_1 : Uω (aρ 1) (bρ 1) (516848975477 / 16000000000000) ≤ -(36577430804916419226009 / 10000000000000000000000)

theorem Zeta5Irrational.U_72_2 : Uω (aρ 2) (bρ 2) (516848975477 / 16000000000000) ≤ -(9428971103386477538939 / 2500000000000000000000)

theorem Zeta5Irrational.U_72_3 : Uω (aρ 3) (bρ 3) (516848975477 / 16000000000000) ≤ -(41047467247559701779401 / 10000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_72 : Uρ (516848975477 / 16000000000000) ≤ -(273619983663501507283 / 100000000000000000000)

theorem Zeta5Irrational.U_73_1 : Uω (aρ 1) (bρ 1) (262469337119 / 8000000000000) ≤ -(1455313035456262498261 / 400000000000000000000)

theorem Zeta5Irrational.U_73_2 : Uω (aρ 2) (bρ 2) (262469337119 / 8000000000000) ≤ -(9373571884890926660439 / 2500000000000000000000)

theorem Zeta5Irrational.U_73_3 : Uω (aρ 3) (bρ 3) (262469337119 / 8000000000000) ≤ -(8140134214423032915029 / 2000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_73 : Uρ (262469337119 / 8000000000000) ≤ -(27338531661035234682497 / 10000000000000000000000)

theorem Zeta5Irrational.U_74_1 : Uω (aρ 1) (bρ 1) (6763975897 / 200000000000) ≤ -(36004671011973596596201 / 10000000000000000000000)

theorem Zeta5Irrational.U_74_2 : Uω (aρ 2) (bρ 2) (6763975897 / 200000000000) ≤ -(18532915025022758161627 / 5000000000000000000000)

theorem Zeta5Irrational.U_74_3 : Uω (aρ 3) (bρ 3) (6763975897 / 200000000000) ≤ -(801004622320808228037 / 200000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_74 : Uρ (6763975897 / 200000000000) ≤ -(27294001523746580880381 / 10000000000000000000000)

theorem Zeta5Irrational.U_75_1 : Uω (aρ 1) (bρ 1) (278648734641 / 8000000000000) ≤ -(35640354467824444665873 / 10000000000000000000000)

theorem Zeta5Irrational.U_75_2 : Uω (aρ 2) (bρ 2) (278648734641 / 8000000000000) ≤ -(36655583055019159093507 / 10000000000000000000000)

theorem Zeta5Irrational.U_75_3 : Uω (aρ 3) (bρ 3) (278648734641 / 8000000000000) ≤ -(19724394162041300263193 / 5000000000000000000000)

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_75 : Uρ (278648734641 / 8000000000000) ≤ -(27252257261802753728461 / 10000000000000000000000)