Certified arcsine potential bounds (U21)

theorem Zeta5Irrational.U_256_1 : Uω (aρ 1) (bρ 1) (6947186163633 / 32000000000000) ≤ -(15575944573125605674177 / 10000000000000000000000)

theorem Zeta5Irrational.U_256_2 : Uω (aρ 2) (bρ 2) (6947186163633 / 32000000000000) ≤ -(245179764752538628203 / 156250000000000000000)

theorem Zeta5Irrational.U_256_3 : Uω (aρ 3) (bρ 3) (6947186163633 / 32000000000000) ≤ -(995512258233638353213 / 625000000000000000000)

theorem Zeta5Irrational.U_256_4 : Uω (aρ 4) (bρ 4) (6947186163633 / 32000000000000) ≤ -(8169553275997104438517 / 5000000000000000000000)

theorem Zeta5Irrational.U_256_5 : Uω (aρ 5) (bρ 5) (6947186163633 / 32000000000000) ≤ -(136113189584853233173 / 80000000000000000000)

theorem Zeta5Irrational.U_256_6 : Uω (aρ 6) (bρ 6) (6947186163633 / 32000000000000) ≤ -(18115189220547125073919 / 10000000000000000000000)

theorem Zeta5Irrational.U_256_7 : Uω (aρ 7) (bρ 7) (6947186163633 / 32000000000000) ≤ -(10004865974050945407887 / 5000000000000000000000)

theorem Zeta5Irrational.U_256_8 : Uω (aρ 8) (bρ 8) (6947186163633 / 32000000000000) ≤ -(24341894157151895026913 / 10000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_256 : Uρ (6947186163633 / 32000000000000) ≤ -(4732322352294633080727 / 2500000000000000000000)

theorem Zeta5Irrational.U_257_1 : Uω (aρ 1) (bρ 1) (13928492444353 / 64000000000000) ≤ -(15550666034157081233191 / 10000000000000000000000)

theorem Zeta5Irrational.U_257_2 : Uω (aρ 2) (bρ 2) (13928492444353 / 64000000000000) ≤ -(7832963829924780234651 / 5000000000000000000000)

theorem Zeta5Irrational.U_257_3 : Uω (aρ 3) (bρ 3) (13928492444353 / 64000000000000) ≤ -(15901990069294298442933 / 10000000000000000000000)

theorem Zeta5Irrational.U_257_4 : Uω (aρ 4) (bρ 4) (13928492444353 / 64000000000000) ≤ -(16311751804573218956949 / 10000000000000000000000)

theorem Zeta5Irrational.U_257_5 : Uω (aρ 5) (bρ 5) (13928492444353 / 64000000000000) ≤ -(16984732574596841281701 / 10000000000000000000000)

theorem Zeta5Irrational.U_257_6 : Uω (aρ 6) (bρ 6) (13928492444353 / 64000000000000) ≤ -(18081854109771723636757 / 10000000000000000000000)

theorem Zeta5Irrational.U_257_7 : Uω (aρ 7) (bρ 7) (13928492444353 / 64000000000000) ≤ -(19967393221007081062849 / 10000000000000000000000)

theorem Zeta5Irrational.U_257_8 : Uω (aρ 8) (bρ 8) (13928492444353 / 64000000000000) ≤ -(4850434515589518544511 / 2000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_257 : Uρ (13928492444353 / 64000000000000) ≤ -(590917771300687400017 / 312500000000000000000)

theorem Zeta5Irrational.U_258_1 : Uω (aρ 1) (bρ 1) (87266328509 / 400000000000) ≤ -(1552545123916181522009 / 1000000000000000000000)

theorem Zeta5Irrational.U_258_2 : Uω (aρ 2) (bρ 2) (87266328509 / 400000000000) ≤ -(15640415660118783464449 / 10000000000000000000000)

theorem Zeta5Irrational.U_258_3 : Uω (aρ 3) (bρ 3) (87266328509 / 400000000000) ≤ -(15875852624851757203039 / 10000000000000000000000)

theorem Zeta5Irrational.U_258_4 : Uω (aρ 4) (bρ 4) (87266328509 / 400000000000) ≤ -(16284472091276283593661 / 10000000000000000000000)

theorem Zeta5Irrational.U_258_5 : Uω (aρ 5) (bρ 5) (87266328509 / 400000000000) ≤ -(1695540410769040563281 / 1000000000000000000000)

theorem Zeta5Irrational.U_258_6 : Uω (aρ 6) (bρ 6) (87266328509 / 400000000000) ≤ -(18048634909578610900489 / 10000000000000000000000)

theorem Zeta5Irrational.U_258_7 : Uω (aρ 7) (bρ 7) (87266328509 / 400000000000) ≤ -(19925259876362511462543 / 10000000000000000000000)

theorem Zeta5Irrational.U_258_8 : Uω (aρ 8) (bρ 8) (87266328509 / 400000000000) ≤ -(2416399500157657047719 / 1000000000000000000000)

theorem Zeta5Irrational.U_258_9 : Uω (aρ 9) (bρ 9) (87266328509 / 400000000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_258_10 : Uω (aρ 10) (bρ 10) (87266328509 / 400000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_258_11 : Uω (aρ 11) (bρ 11) (87266328509 / 400000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_258_12 : Uω (aρ 12) (bρ 12) (87266328509 / 400000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_258_13 : Uω (aρ 13) (bρ 13) (87266328509 / 400000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_258_14 : Uω (aρ 14) (bρ 14) (87266328509 / 400000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_258_15 : Uω (aρ 15) (bρ 15) (87266328509 / 400000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_258_16 : Uω (aρ 16) (bρ 16) (87266328509 / 400000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_258 : Uρ (87266328509 / 400000000000) ≤ -(9444813483692401198133 / 5000000000000000000000)

theorem Zeta5Irrational.U_259_1 : Uω (aρ 1) (bρ 1) (13996732678527 / 64000000000000) ≤ -(15500299867443468815179 / 10000000000000000000000)

theorem Zeta5Irrational.U_259_2 : Uω (aρ 2) (bρ 2) (13996732678527 / 64000000000000) ≤ -(15614968612387440695619 / 10000000000000000000000)

theorem Zeta5Irrational.U_259_3 : Uω (aρ 3) (bρ 3) (13996732678527 / 64000000000000) ≤ -(15849783439378083627973 / 10000000000000000000000)

theorem Zeta5Irrational.U_259_4 : Uω (aρ 4) (bρ 4) (13996732678527 / 64000000000000) ≤ -(16257266999367032878831 / 10000000000000000000000)

theorem Zeta5Irrational.U_259_5 : Uω (aρ 5) (bρ 5) (13996732678527 / 64000000000000) ≤ -(4231540692110611749079 / 2500000000000000000000)

theorem Zeta5Irrational.U_259_6 : Uω (aρ 6) (bρ 6) (13996732678527 / 64000000000000) ≤ -(9007765390997410364347 / 5000000000000000000000)

theorem Zeta5Irrational.U_259_7 : Uω (aρ 7) (bρ 7) (13996732678527 / 64000000000000) ≤ -(9941664845595572648541 / 5000000000000000000000)

theorem Zeta5Irrational.U_259_8 : Uω (aρ 8) (bρ 8) (13996732678527 / 64000000000000) ≤ -(1203864543957815277543 / 500000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_259 : Uρ (13996732678527 / 64000000000000) ≤ -(18870057686366365844573 / 10000000000000000000000)

theorem Zeta5Irrational.U_260_1 : Uω (aρ 1) (bρ 1) (7015426397807 / 32000000000000) ≤ -(154752116007199462903 / 100000000000000000000)

theorem Zeta5Irrational.U_260_2 : Uω (aρ 2) (bρ 2) (7015426397807 / 32000000000000) ≤ -(1948698273326129675261 / 1250000000000000000000)

theorem Zeta5Irrational.U_260_3 : Uω (aρ 3) (bρ 3) (7015426397807 / 32000000000000) ≤ -(3955945539164048809487 / 2500000000000000000000)

theorem Zeta5Irrational.U_260_4 : Uω (aρ 4) (bρ 4) (7015426397807 / 32000000000000) ≤ -(1623013611952324522931 / 1000000000000000000000)

theorem Zeta5Irrational.U_260_5 : Uω (aρ 5) (bρ 5) (7015426397807 / 32000000000000) ≤ -(16897008032751650925741 / 10000000000000000000000)

theorem Zeta5Irrational.U_260_6 : Uω (aρ 6) (bρ 6) (7015426397807 / 32000000000000) ≤ -(17982540898443015669829 / 10000000000000000000000)

theorem Zeta5Irrational.U_260_7 : Uω (aρ 7) (bρ 7) (7015426397807 / 32000000000000) ≤ -(19841600481412250417977 / 10000000000000000000000)

theorem Zeta5Irrational.U_260_8 : Uω (aρ 8) (bρ 8) (7015426397807 / 32000000000000) ≤ -(959679797350474912757 / 400000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_260 : Uρ (7015426397807 / 32000000000000) ≤ -(18850654729282272068329 / 10000000000000000000000)

theorem Zeta5Irrational.U_261_1 : Uω (aρ 1) (bρ 1) (14064972912701 / 64000000000000) ≤ -(7725093061549607964581 / 5000000000000000000000)

theorem Zeta5Irrational.U_261_2 : Uω (aρ 2) (bρ 2) (14064972912701 / 64000000000000) ≤ -(622570722209901726493 / 400000000000000000000)

theorem Zeta5Irrational.U_261_3 : Uω (aρ 3) (bρ 3) (14064972912701 / 64000000000000) ≤ -(157978484232550097711 / 100000000000000000000)

theorem Zeta5Irrational.U_261_4 : Uω (aρ 4) (bρ 4) (14064972912701 / 64000000000000) ≤ -(506346220181221679599 / 312500000000000000000)

theorem Zeta5Irrational.U_261_5 : Uω (aρ 5) (bρ 5) (14064972912701 / 64000000000000) ≤ -(16867939381300538389631 / 10000000000000000000000)

theorem Zeta5Irrational.U_261_6 : Uω (aρ 6) (bρ 6) (14064972912701 / 64000000000000) ≤ -(17949664439597163688407 / 10000000000000000000000)

theorem Zeta5Irrational.U_261_7 : Uω (aρ 7) (bρ 7) (14064972912701 / 64000000000000) ≤ -(4950017525222746901699 / 2500000000000000000000)

theorem Zeta5Irrational.U_261_8 : Uω (aρ 8) (bρ 8) (14064972912701 / 64000000000000) ≤ -(23908046622860256109079 / 10000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_261 : Uρ (14064972912701 / 64000000000000) ≤ -(18831412410044943318741 / 10000000000000000000000)

theorem Zeta5Irrational.U_262_1 : Uω (aρ 1) (bρ 1) (3524773257447 / 16000000000000) ≤ -(15425223121055442148307 / 10000000000000000000000)

theorem Zeta5Irrational.U_262_2 : Uω (aρ 2) (bρ 2) (3524773257447 / 16000000000000) ≤ -(31078027786503970657 / 20000000000000000000)

theorem Zeta5Irrational.U_262_3 : Uω (aρ 3) (bρ 3) (3524773257447 / 16000000000000) ≤ -(15771981888500432529827 / 10000000000000000000000)

theorem Zeta5Irrational.U_262_4 : Uω (aρ 4) (bρ 4) (3524773257447 / 16000000000000) ≤ -(16176095375587935077251 / 10000000000000000000000)

theorem Zeta5Irrational.U_262_5 : Uω (aρ 5) (bρ 5) (3524773257447 / 16000000000000) ≤ -(3367791259899323997961 / 2000000000000000000000)

theorem Zeta5Irrational.U_262_6 : Uω (aρ 6) (bρ 6) (3524773257447 / 16000000000000) ≤ -(17916900595241057764019 / 10000000000000000000000)

theorem Zeta5Irrational.U_262_7 : Uω (aρ 7) (bρ 7) (3524773257447 / 16000000000000) ≤ -(9879368220258900866009 / 5000000000000000000000)

theorem Zeta5Irrational.U_262_8 : Uω (aρ 8) (bρ 8) (3524773257447 / 16000000000000) ≤ -(11912694834656871134041 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_262 : Uρ (3524773257447 / 16000000000000) ≤ -(18812325424208424567931 / 10000000000000000000000)

theorem Zeta5Irrational.U_263_1 : Uω (aρ 1) (bρ 1) (4522628207 / 20480000000) ≤ -(15400322283405405486297 / 10000000000000000000000)

theorem Zeta5Irrational.U_263_2 : Uω (aρ 2) (bρ 2) (4522628207 / 20480000000) ≤ -(7756911689015681382531 / 5000000000000000000000)

theorem Zeta5Irrational.U_263_3 : Uω (aρ 3) (bρ 3) (4522628207 / 20480000000) ≤ -(7873091102223352406081 / 5000000000000000000000)

theorem Zeta5Irrational.U_263_4 : Uω (aρ 4) (bρ 4) (4522628207 / 20480000000) ≤ -(16149184709585599162011 / 10000000000000000000000)

theorem Zeta5Irrational.U_263_5 : Uω (aρ 5) (bρ 5) (4522628207 / 20480000000) ≤ -(16810058277414486902431 / 10000000000000000000000)

theorem Zeta5Irrational.U_263_6 : Uω (aρ 6) (bρ 6) (4522628207 / 20480000000) ≤ -(1788424856412957003267 / 1000000000000000000000)

theorem Zeta5Irrational.U_263_7 : Uω (aρ 7) (bρ 7) (4522628207 / 20480000000) ≤ -(19717597427316517697399 / 10000000000000000000000)

theorem Zeta5Irrational.U_263_8 : Uω (aρ 8) (bρ 8) (4522628207 / 20480000000) ≤ -(237439716505508975011 / 100000000000000000000)

theorem Zeta5Irrational.U_263_9 : Uω (aρ 9) (bρ 9) (4522628207 / 20480000000) ≤ -(26986659976834617141369 / 10000000000000000000000)

theorem Zeta5Irrational.U_263_10 : Uω (aρ 10) (bρ 10) (4522628207 / 20480000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_263_11 : Uω (aρ 11) (bρ 11) (4522628207 / 20480000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_263_12 : Uω (aρ 12) (bρ 12) (4522628207 / 20480000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_263_13 : Uω (aρ 13) (bρ 13) (4522628207 / 20480000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_263_14 : Uω (aρ 14) (bρ 14) (4522628207 / 20480000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_263_15 : Uω (aρ 15) (bρ 15) (4522628207 / 20480000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_263_16 : Uω (aρ 16) (bρ 16) (4522628207 / 20480000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_263 : Uρ (4522628207 / 20480000000) ≤ -(18793388812557728533729 / 10000000000000000000000)

theorem Zeta5Irrational.U_264_1 : Uω (aρ 1) (bρ 1) (7083666631981 / 32000000000000) ≤ -(7687741650642611239753 / 5000000000000000000000)

theorem Zeta5Irrational.U_264_2 : Uω (aρ 2) (bρ 2) (7083666631981 / 32000000000000) ≤ -(1936087023678734676367 / 1250000000000000000000)

theorem Zeta5Irrational.U_264_3 : Uω (aρ 3) (bρ 3) (7083666631981 / 32000000000000) ≤ -(15720449025848114804897 / 10000000000000000000000)

theorem Zeta5Irrational.U_264_4 : Uω (aρ 4) (bρ 4) (7083666631981 / 32000000000000) ≤ -(8061173325877085877879 / 5000000000000000000000)

theorem Zeta5Irrational.U_264_5 : Uω (aρ 5) (bρ 5) (7083666631981 / 32000000000000) ≤ -(16781244809738776207101 / 10000000000000000000000)

theorem Zeta5Irrational.U_264_6 : Uω (aρ 6) (bρ 6) (7083666631981 / 32000000000000) ≤ -(446292688846316203507 / 250000000000000000000)

theorem Zeta5Irrational.U_264_7 : Uω (aρ 7) (bρ 7) (7083666631981 / 32000000000000) ≤ -(19676651023580034608527 / 10000000000000000000000)

theorem Zeta5Irrational.U_264_8 : Uω (aρ 8) (bρ 8) (7083666631981 / 32000000000000) ≤ -(11831871818659477479103 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_264 : Uρ (7083666631981 / 32000000000000) ≤ -(18774597929083658498267 / 10000000000000000000000)

theorem Zeta5Irrational.U_265_1 : Uω (aρ 1) (bρ 1) (14201453381049 / 64000000000000) ≤ -(76753529340636769929 / 50000000000000000000)

theorem Zeta5Irrational.U_265_2 : Uω (aρ 2) (bρ 2) (14201453381049 / 64000000000000) ≤ -(3092726401940492489023 / 2000000000000000000000)

theorem Zeta5Irrational.U_265_3 : Uω (aρ 3) (bρ 3) (14201453381049 / 64000000000000) ≤ -(15694782010131099692527 / 10000000000000000000000)

theorem Zeta5Irrational.U_265_4 : Uω (aρ 4) (bρ 4) (14201453381049 / 64000000000000) ≤ -(4023895202321576679941 / 2500000000000000000000)

theorem Zeta5Irrational.U_265_5 : Uω (aρ 5) (bρ 5) (14201453381049 / 64000000000000) ≤ -(16752515395708029767003 / 10000000000000000000000)

theorem Zeta5Irrational.U_265_6 : Uω (aρ 6) (bρ 6) (14201453381049 / 64000000000000) ≤ -(17819276780701897823461 / 10000000000000000000000)

theorem Zeta5Irrational.U_265_7 : Uω (aρ 7) (bρ 7) (14201453381049 / 64000000000000) ≤ -(4908973806508137317557 / 2500000000000000000000)

theorem Zeta5Irrational.U_265_8 : Uω (aρ 8) (bρ 8) (14201453381049 / 64000000000000) ≤ -(5896164968722676067157 / 2500000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_265 : Uρ (14201453381049 / 64000000000000) ≤ -(2344493551589127377827 / 1250000000000000000000)

theorem Zeta5Irrational.U_266_1 : Uω (aρ 1) (bρ 1) (1779446687267 / 8000000000000) ≤ -(3831497419909473840719 / 2500000000000000000000)

theorem Zeta5Irrational.U_266_2 : Uω (aρ 2) (bρ 2) (1779446687267 / 8000000000000) ≤ -(15438630523490637756799 / 10000000000000000000000)

theorem Zeta5Irrational.U_266_3 : Uω (aρ 3) (bρ 3) (1779446687267 / 8000000000000) ≤ -(313383616347333776729 / 200000000000000000000)

theorem Zeta5Irrational.U_266_4 : Uω (aρ 4) (bρ 4) (1779446687267 / 8000000000000) ≤ -(16068886792570002071263 / 10000000000000000000000)

theorem Zeta5Irrational.U_266_5 : Uω (aρ 5) (bρ 5) (1779446687267 / 8000000000000) ≤ -(1045241846191213256377 / 625000000000000000000)

theorem Zeta5Irrational.U_266_6 : Uω (aρ 6) (bρ 6) (1779446687267 / 8000000000000) ≤ -(4446738867384939903639 / 2500000000000000000000)

theorem Zeta5Irrational.U_266_7 : Uω (aρ 7) (bρ 7) (1779446687267 / 8000000000000) ≤ -(19595328065017379469913 / 10000000000000000000000)

theorem Zeta5Irrational.U_266_8 : Uω (aρ 8) (bρ 8) (1779446687267 / 8000000000000) ≤ -(2938334687597392326683 / 1250000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_266 : Uρ (1779446687267 / 8000000000000) ≤ -(18737436162268459849223 / 10000000000000000000000)

theorem Zeta5Irrational.U_267_1 : Uω (aρ 1) (bρ 1) (14269693615223 / 64000000000000) ≤ -(3060266886754829329249 / 2000000000000000000000)

theorem Zeta5Irrational.U_267_2 : Uω (aρ 2) (bρ 2) (14269693615223 / 64000000000000) ≤ -(15413691417798657404249 / 10000000000000000000000)

theorem Zeta5Irrational.U_267_3 : Uω (aρ 3) (bρ 3) (14269693615223 / 64000000000000) ≤ -(1955455638780413424699 / 1250000000000000000000)

theorem Zeta5Irrational.U_267_4 : Uω (aρ 4) (bρ 4) (14269693615223 / 64000000000000) ≤ -(8021132107576929851351 / 5000000000000000000000)

theorem Zeta5Irrational.U_267_5 : Uω (aρ 5) (bρ 5) (14269693615223 / 64000000000000) ≤ -(16695306747974266726253 / 10000000000000000000000)

theorem Zeta5Irrational.U_267_6 : Uω (aρ 6) (bρ 6) (14269693615223 / 64000000000000) ≤ -(17754742853671198578557 / 10000000000000000000000)

theorem Zeta5Irrational.U_267_7 : Uω (aρ 7) (bρ 7) (14269693615223 / 64000000000000) ≤ -(9777473801854687953071 / 5000000000000000000000)

theorem Zeta5Irrational.U_267_8 : Uω (aρ 8) (bρ 8) (14269693615223 / 64000000000000) ≤ -(11714878146986777122497 / 5000000000000000000000)

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

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_267 : Uρ (14269693615223 / 64000000000000) ≤ -(18719057314217090473663 / 10000000000000000000000)