Certified arcsine potential bounds (U38)

theorem Zeta5Irrational.U_460_1 : Uω (aρ 1) (bρ 1) (245862249367 / 500000000000) ≤ -(3615234313927837667861 / 5000000000000000000000)

theorem Zeta5Irrational.U_460_2 : Uω (aρ 2) (bρ 2) (245862249367 / 500000000000) ≤ -(7279955839745068222781 / 10000000000000000000000)

theorem Zeta5Irrational.U_460_3 : Uω (aρ 3) (bρ 3) (245862249367 / 500000000000) ≤ -(1475950658839148611197 / 2000000000000000000000)

theorem Zeta5Irrational.U_460_4 : Uω (aρ 4) (bρ 4) (245862249367 / 500000000000) ≤ -(3773995427686548841721 / 5000000000000000000000)

theorem Zeta5Irrational.U_460_5 : Uω (aρ 5) (bρ 5) (245862249367 / 500000000000) ≤ -(1249668051570219817 / 1600000000000000000)

theorem Zeta5Irrational.U_460_6 : Uω (aρ 6) (bρ 6) (245862249367 / 500000000000) ≤ -(512555580040854648039 / 625000000000000000000)

theorem Zeta5Irrational.U_460_7 : Uω (aρ 7) (bρ 7) (245862249367 / 500000000000) ≤ -(4381688364844639488627 / 5000000000000000000000)

theorem Zeta5Irrational.U_460_8 : Uω (aρ 8) (bρ 8) (245862249367 / 500000000000) ≤ -(9557973728229765291131 / 10000000000000000000000)

theorem Zeta5Irrational.U_460_9 : Uω (aρ 9) (bρ 9) (245862249367 / 500000000000) ≤ -(1334631757746133575117 / 1250000000000000000000)

theorem Zeta5Irrational.U_460_10 : Uω (aρ 10) (bρ 10) (245862249367 / 500000000000) ≤ -(12296988295501843449263 / 10000000000000000000000)

theorem Zeta5Irrational.U_460_11 : Uω (aρ 11) (bρ 11) (245862249367 / 500000000000) ≤ -(14931666246709073635179 / 10000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_460 : Uρ (245862249367 / 500000000000) ≤ -(1097728741781144235151 / 1000000000000000000000)

theorem Zeta5Irrational.U_461_1 : Uω (aρ 1) (bρ 1) (494373098487 / 1000000000000) ≤ -(1435207381605281826913 / 2000000000000000000000)

theorem Zeta5Irrational.U_461_2 : Uω (aρ 2) (bρ 2) (494373098487 / 1000000000000) ≤ -(3612626362959643324813 / 5000000000000000000000)

theorem Zeta5Irrational.U_461_3 : Uω (aρ 3) (bρ 3) (494373098487 / 1000000000000) ≤ -(732449666129835809591 / 1000000000000000000000)

theorem Zeta5Irrational.U_461_4 : Uω (aρ 4) (bρ 4) (494373098487 / 1000000000000) ≤ -(7491781848650053319527 / 10000000000000000000000)

theorem Zeta5Irrational.U_461_5 : Uω (aρ 5) (bρ 5) (494373098487 / 1000000000000) ≤ -(387634025740016904203 / 500000000000000000000)

theorem Zeta5Irrational.U_461_6 : Uω (aρ 6) (bρ 6) (494373098487 / 1000000000000) ≤ -(814073901128552071001 / 1000000000000000000000)

theorem Zeta5Irrational.U_461_7 : Uω (aρ 7) (bρ 7) (494373098487 / 1000000000000) ≤ -(8699483085173201573619 / 10000000000000000000000)

theorem Zeta5Irrational.U_461_8 : Uω (aρ 8) (bρ 8) (494373098487 / 1000000000000) ≤ -(9488147633802443083583 / 10000000000000000000000)

theorem Zeta5Irrational.U_461_9 : Uω (aρ 9) (bρ 9) (494373098487 / 1000000000000) ≤ -(10597289264973965425953 / 10000000000000000000000)

theorem Zeta5Irrational.U_461_10 : Uω (aρ 10) (bρ 10) (494373098487 / 1000000000000) ≤ -(609912108571579113853 / 500000000000000000000)

theorem Zeta5Irrational.U_461_11 : Uω (aρ 11) (bρ 11) (494373098487 / 1000000000000) ≤ -(1847555945715342408171 / 1250000000000000000000)

theorem Zeta5Irrational.U_461_12 : Uω (aρ 12) (bρ 12) (494373098487 / 1000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_461_13 : Uω (aρ 13) (bρ 13) (494373098487 / 1000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_461_14 : Uω (aρ 14) (bρ 14) (494373098487 / 1000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_461_15 : Uω (aρ 15) (bρ 15) (494373098487 / 1000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_461_16 : Uω (aρ 16) (bρ 16) (494373098487 / 1000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_461 : Uρ (494373098487 / 1000000000000) ≤ -(682607457176087644829 / 625000000000000000000)

theorem Zeta5Irrational.U_462_1 : Uω (aρ 1) (bρ 1) (1553192807 / 3125000000) ≤ -(3560949935065535102229 / 5000000000000000000000)

theorem Zeta5Irrational.U_462_2 : Uω (aρ 2) (bρ 2) (1553192807 / 3125000000) ≤ -(3585423627245885930571 / 5000000000000000000000)

theorem Zeta5Irrational.U_462_3 : Uω (aρ 3) (bρ 3) (1553192807 / 3125000000) ≤ -(1817385944381576922393 / 2500000000000000000000)

theorem Zeta5Irrational.U_462_4 : Uω (aρ 4) (bρ 4) (1553192807 / 3125000000) ≤ -(1487177463258952670079 / 2000000000000000000000)

theorem Zeta5Irrational.U_462_5 : Uω (aρ 5) (bρ 5) (1553192807 / 3125000000) ≤ -(7695268068651840452393 / 10000000000000000000000)

theorem Zeta5Irrational.U_462_6 : Uω (aρ 6) (bρ 6) (1553192807 / 3125000000) ≤ -(8080950627273355186921 / 10000000000000000000000)

theorem Zeta5Irrational.U_462_7 : Uω (aρ 7) (bρ 7) (1553192807 / 3125000000) ≤ -(8636001089211850716229 / 10000000000000000000000)

theorem Zeta5Irrational.U_462_8 : Uω (aρ 8) (bρ 8) (1553192807 / 3125000000) ≤ -(9418822182081979184731 / 10000000000000000000000)

theorem Zeta5Irrational.U_462_9 : Uω (aρ 9) (bρ 9) (1553192807 / 3125000000) ≤ -(10518204729532456955793 / 10000000000000000000000)

theorem Zeta5Irrational.U_462_10 : Uω (aρ 10) (bρ 10) (1553192807 / 3125000000) ≤ -(2420128375275408177111 / 2000000000000000000000)

theorem Zeta5Irrational.U_462_11 : Uω (aρ 11) (bρ 11) (1553192807 / 3125000000) ≤ -(1829093014460264202961 / 1250000000000000000000)

theorem Zeta5Irrational.U_462_12 : Uω (aρ 12) (bρ 12) (1553192807 / 3125000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_462_13 : Uω (aρ 13) (bρ 13) (1553192807 / 3125000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_462_14 : Uω (aρ 14) (bρ 14) (1553192807 / 3125000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_462_15 : Uω (aρ 15) (bρ 15) (1553192807 / 3125000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_462_16 : Uω (aρ 16) (bρ 16) (1553192807 / 3125000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_462 : Uρ (1553192807 / 3125000000) ≤ -(5433380228379890830107 / 5000000000000000000000)

theorem Zeta5Irrational.U_463_1 : Uω (aρ 1) (bρ 1) (499670297993 / 1000000000000) ≤ -(7068054340607733583047 / 10000000000000000000000)

theorem Zeta5Irrational.U_463_2 : Uω (aρ 2) (bρ 2) (499670297993 / 1000000000000) ≤ -(889592025465360876981 / 1250000000000000000000)

theorem Zeta5Irrational.U_463_3 : Uω (aρ 3) (bρ 3) (499670297993 / 1000000000000) ≤ -(3607445660313601547497 / 5000000000000000000000)

theorem Zeta5Irrational.U_463_4 : Uω (aρ 4) (bρ 4) (499670297993 / 1000000000000) ≤ -(59042430046709734459 / 80000000000000000000)

theorem Zeta5Irrational.U_463_5 : Uω (aρ 5) (bρ 5) (499670297993 / 1000000000000) ≤ -(7638184170449427090801 / 10000000000000000000000)

theorem Zeta5Irrational.U_463_6 : Uω (aρ 6) (bρ 6) (499670297993 / 1000000000000) ≤ -(125336246465165303943 / 156250000000000000000)

theorem Zeta5Irrational.U_463_7 : Uω (aρ 7) (bρ 7) (499670297993 / 1000000000000) ≤ -(2143231349051881482137 / 2500000000000000000000)

theorem Zeta5Irrational.U_463_8 : Uω (aρ 8) (bρ 8) (499670297993 / 1000000000000) ≤ -(9349990018013522406539 / 10000000000000000000000)

theorem Zeta5Irrational.U_463_9 : Uω (aρ 9) (bρ 9) (499670297993 / 1000000000000) ≤ -(10439788165175504274949 / 10000000000000000000000)

theorem Zeta5Irrational.U_463_10 : Uω (aρ 10) (bρ 10) (499670297993 / 1000000000000) ≤ -(12004157409170647831141 / 10000000000000000000000)

theorem Zeta5Irrational.U_463_11 : Uω (aρ 11) (bρ 11) (499670297993 / 1000000000000) ≤ -(7244175858108899826303 / 5000000000000000000000)

theorem Zeta5Irrational.U_463_12 : Uω (aρ 12) (bρ 12) (499670297993 / 1000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_463_13 : Uω (aρ 13) (bρ 13) (499670297993 / 1000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_463_14 : Uω (aρ 14) (bρ 14) (499670297993 / 1000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_463_15 : Uω (aρ 15) (bρ 15) (499670297993 / 1000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_463_16 : Uω (aρ 16) (bρ 16) (499670297993 / 1000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_463 : Uρ (499670297993 / 1000000000000) ≤ -(10812388899080794907653 / 10000000000000000000000)

theorem Zeta5Irrational.U_464_1 : Uω (aρ 1) (bρ 1) (504967497499 / 1000000000000) ≤ -(3480612683152575500467 / 5000000000000000000000)

theorem Zeta5Irrational.U_464_2 : Uω (aρ 2) (bρ 2) (504967497499 / 1000000000000) ≤ -(7009384736248986284349 / 10000000000000000000000)

theorem Zeta5Irrational.U_464_3 : Uω (aρ 3) (bρ 3) (504967497499 / 1000000000000) ≤ -(7106474668395118534257 / 10000000000000000000000)

theorem Zeta5Irrational.U_464_4 : Uω (aρ 4) (bρ 4) (504967497499 / 1000000000000) ≤ -(3635027915338646864123 / 5000000000000000000000)

theorem Zeta5Irrational.U_464_5 : Uω (aρ 5) (bρ 5) (504967497499 / 1000000000000) ≤ -(300999483591545481661 / 400000000000000000000)

theorem Zeta5Irrational.U_464_6 : Uω (aρ 6) (bρ 6) (504967497499 / 1000000000000) ≤ -(987964203752296207611 / 1250000000000000000000)

theorem Zeta5Irrational.U_464_7 : Uω (aρ 7) (bρ 7) (504967497499 / 1000000000000) ≤ -(168959441163534356641 / 200000000000000000000)

theorem Zeta5Irrational.U_464_8 : Uω (aρ 8) (bρ 8) (504967497499 / 1000000000000) ≤ -(9213776955017311777019 / 10000000000000000000000)

theorem Zeta5Irrational.U_464_9 : Uω (aρ 9) (bρ 9) (504967497499 / 1000000000000) ≤ -(5142455757492057291689 / 5000000000000000000000)

theorem Zeta5Irrational.U_464_10 : Uω (aρ 10) (bρ 10) (504967497499 / 1000000000000) ≤ -(11814422219193978853499 / 10000000000000000000000)

theorem Zeta5Irrational.U_464_11 : Uω (aρ 11) (bρ 11) (504967497499 / 1000000000000) ≤ -(7104388521796205094697 / 5000000000000000000000)

theorem Zeta5Irrational.U_464_12 : Uω (aρ 12) (bρ 12) (504967497499 / 1000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_464_13 : Uω (aρ 13) (bρ 13) (504967497499 / 1000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_464_14 : Uω (aρ 14) (bρ 14) (504967497499 / 1000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_464_15 : Uω (aρ 15) (bρ 15) (504967497499 / 1000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_464_16 : Uω (aρ 16) (bρ 16) (504967497499 / 1000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_464 : Uρ (504967497499 / 1000000000000) ≤ -(10705328196259241107531 / 10000000000000000000000)

theorem Zeta5Irrational.U_465_1 : Uω (aρ 1) (bρ 1) (102052939401 / 200000000000) ≤ -(685552559971335199247 / 1000000000000000000000)

theorem Zeta5Irrational.U_465_2 : Uω (aρ 2) (bρ 2) (102052939401 / 200000000000) ≤ -(6903173572969198641041 / 10000000000000000000000)

theorem Zeta5Irrational.U_465_3 : Uω (aρ 3) (bρ 3) (102052939401 / 200000000000) ≤ -(3499610595096664125941 / 5000000000000000000000)

theorem Zeta5Irrational.U_465_4 : Uω (aρ 4) (bρ 4) (102052939401 / 200000000000) ≤ -(7161011195376077060239 / 10000000000000000000000)

theorem Zeta5Irrational.U_465_5 : Uω (aρ 5) (bρ 5) (102052939401 / 200000000000) ≤ -(3706530023605786136097 / 5000000000000000000000)

theorem Zeta5Irrational.U_465_6 : Uω (aρ 6) (bρ 6) (102052939401 / 200000000000) ≤ -(311491491184998294687 / 400000000000000000000)

theorem Zeta5Irrational.U_465_7 : Uω (aρ 7) (bρ 7) (102052939401 / 200000000000) ≤ -(66596658834443514293 / 80000000000000000000)

theorem Zeta5Irrational.U_465_8 : Uω (aρ 8) (bρ 8) (102052939401 / 200000000000) ≤ -(4539726412331190736867 / 5000000000000000000000)

theorem Zeta5Irrational.U_465_9 : Uω (aρ 9) (bρ 9) (102052939401 / 200000000000) ≤ -(5066283857032743146991 / 5000000000000000000000)

theorem Zeta5Irrational.U_465_10 : Uω (aρ 10) (bρ 10) (102052939401 / 200000000000) ≤ -(11628820653098059451003 / 10000000000000000000000)

theorem Zeta5Irrational.U_465_11 : Uω (aρ 11) (bρ 11) (102052939401 / 200000000000) ≤ -(871277070376627645763 / 625000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_465 : Uρ (102052939401 / 200000000000) ≤ -(80874574167903463 / 76293945312500000)

theorem Zeta5Irrational.U_466_1 : Uω (aρ 1) (bρ 1) (515561896511 / 1000000000000) ≤ -(843866426616583228107 / 1250000000000000000000)

theorem Zeta5Irrational.U_466_2 : Uω (aρ 2) (bρ 2) (515561896511 / 1000000000000) ≤ -(6798078736206332217349 / 10000000000000000000000)

theorem Zeta5Irrational.U_466_3 : Uω (aρ 3) (bρ 3) (515561896511 / 1000000000000) ≤ -(430819136700830867653 / 625000000000000000000)

theorem Zeta5Irrational.U_466_4 : Uω (aρ 4) (bρ 4) (515561896511 / 1000000000000) ≤ -(3526571922133105569901 / 5000000000000000000000)

theorem Zeta5Irrational.U_466_5 : Uω (aρ 5) (bρ 5) (515561896511 / 1000000000000) ≤ -(3651187397247562346277 / 5000000000000000000000)

theorem Zeta5Irrational.U_466_6 : Uω (aρ 6) (bρ 6) (515561896511 / 1000000000000) ≤ -(7672208592147029240361 / 10000000000000000000000)

theorem Zeta5Irrational.U_466_7 : Uω (aρ 7) (bρ 7) (515561896511 / 1000000000000) ≤ -(4101358559010733619021 / 5000000000000000000000)

theorem Zeta5Irrational.U_466_8 : Uω (aρ 8) (bρ 8) (515561896511 / 1000000000000) ≤ -(1789392884586392307439 / 2000000000000000000000)

theorem Zeta5Irrational.U_466_9 : Uω (aρ 9) (bρ 9) (515561896511 / 1000000000000) ≤ -(9982670117907299539191 / 10000000000000000000000)

theorem Zeta5Irrational.U_466_10 : Uω (aρ 10) (bρ 10) (515561896511 / 1000000000000) ≤ -(715447111252919705633 / 625000000000000000000)

theorem Zeta5Irrational.U_466_11 : Uω (aρ 11) (bρ 11) (515561896511 / 1000000000000) ≤ -(13682238889552235011001 / 10000000000000000000000)

theorem Zeta5Irrational.U_466_12 : Uω (aρ 12) (bρ 12) (515561896511 / 1000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_466_13 : Uω (aρ 13) (bρ 13) (515561896511 / 1000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_466_14 : Uω (aρ 14) (bρ 14) (515561896511 / 1000000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_466_15 : Uω (aρ 15) (bρ 15) (515561896511 / 1000000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_466_16 : Uω (aρ 16) (bρ 16) (515561896511 / 1000000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_466 : Uρ (515561896511 / 1000000000000) ≤ -(10497454876210826800467 / 10000000000000000000000)

theorem Zeta5Irrational.U_467_1 : Uω (aρ 1) (bρ 1) (16577867570387 / 32000000000000) ≤ -(1340402996119632497453 / 2000000000000000000000)

theorem Zeta5Irrational.U_467_2 : Uω (aρ 2) (bρ 2) (16577867570387 / 32000000000000) ≤ -(107982879792002849 / 160000000000000000)

theorem Zeta5Irrational.U_467_3 : Uω (aρ 3) (bρ 3) (16577867570387 / 32000000000000) ≤ -(1710871032282440537927 / 2500000000000000000000)

theorem Zeta5Irrational.U_467_4 : Uω (aρ 4) (bρ 4) (16577867570387 / 32000000000000) ≤ -(3501354518816356370809 / 5000000000000000000000)

theorem Zeta5Irrational.U_467_5 : Uω (aρ 5) (bρ 5) (16577867570387 / 32000000000000) ≤ -(7250633714693489879047 / 10000000000000000000000)

theorem Zeta5Irrational.U_467_6 : Uω (aρ 6) (bρ 6) (16577867570387 / 32000000000000) ≤ -(380921630778540381131 / 500000000000000000000)

theorem Zeta5Irrational.U_467_7 : Uω (aρ 7) (bρ 7) (16577867570387 / 32000000000000) ≤ -(1629160430370876043877 / 2000000000000000000000)

theorem Zeta5Irrational.U_467_8 : Uω (aρ 8) (bρ 8) (16577867570387 / 32000000000000) ≤ -(4442573536579649517609 / 5000000000000000000000)

theorem Zeta5Irrational.U_467_9 : Uω (aρ 9) (bρ 9) (16577867570387 / 32000000000000) ≤ -(4956425418371077082301 / 5000000000000000000000)

theorem Zeta5Irrational.U_467_10 : Uω (aρ 10) (bρ 10) (16577867570387 / 32000000000000) ≤ -(5681424454436483179861 / 5000000000000000000000)

theorem Zeta5Irrational.U_467_11 : Uω (aρ 11) (bρ 11) (16577867570387 / 32000000000000) ≤ -(13563808816514087504783 / 10000000000000000000000)

theorem Zeta5Irrational.U_467_12 : Uω (aρ 12) (bρ 12) (16577867570387 / 32000000000000) ≤ -(2387382650451925792207 / 1250000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_467 : Uρ (16577867570387 / 32000000000000) ≤ -(10351760659059680238169 / 10000000000000000000000)

theorem Zeta5Irrational.U_468_1 : Uω (aρ 1) (bρ 1) (8328877226211 / 16000000000000) ≤ -(3326668334306610783819 / 5000000000000000000000)

theorem Zeta5Irrational.U_468_2 : Uω (aρ 2) (bρ 2) (8328877226211 / 16000000000000) ≤ -(6700021636373269278519 / 10000000000000000000000)

theorem Zeta5Irrational.U_468_3 : Uω (aρ 3) (bρ 3) (8328877226211 / 16000000000000) ≤ -(6794107161476389452203 / 10000000000000000000000)

theorem Zeta5Irrational.U_468_4 : Uω (aρ 4) (bρ 4) (8328877226211 / 16000000000000) ≤ -(695252753712603288749 / 1000000000000000000000)

theorem Zeta5Irrational.U_468_5 : Uω (aρ 5) (bρ 5) (8328877226211 / 16000000000000) ≤ -(1439831914742107004137 / 2000000000000000000000)

theorem Zeta5Irrational.U_468_6 : Uω (aρ 6) (bρ 6) (8328877226211 / 16000000000000) ≤ -(1512989178853868331933 / 2000000000000000000000)

theorem Zeta5Irrational.U_468_7 : Uω (aρ 7) (bρ 7) (8328877226211 / 16000000000000) ≤ -(8089213548594952910653 / 10000000000000000000000)

theorem Zeta5Irrational.U_468_8 : Uω (aρ 8) (bρ 8) (8328877226211 / 16000000000000) ≤ -(8823720942157960686819 / 10000000000000000000000)

theorem Zeta5Irrational.U_468_9 : Uω (aρ 9) (bρ 9) (8328877226211 / 16000000000000) ≤ -(9843548329673441358901 / 10000000000000000000000)

theorem Zeta5Irrational.U_468_10 : Uω (aρ 10) (bρ 10) (8328877226211 / 16000000000000) ≤ -(1409919848820797437973 / 1250000000000000000000)

theorem Zeta5Irrational.U_468_11 : Uω (aρ 11) (bρ 11) (8328877226211 / 16000000000000) ≤ -(13447342272511465768649 / 10000000000000000000000)

theorem Zeta5Irrational.U_468_12 : Uω (aρ 12) (bρ 12) (8328877226211 / 16000000000000) ≤ -(18524580292131774241723 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_468 : Uρ (8328877226211 / 16000000000000) ≤ -(1026390100268947894541 / 1000000000000000000000)

theorem Zeta5Irrational.U_469_1 : Uω (aρ 1) (bρ 1) (16737641334457 / 32000000000000) ≤ -(1651223542470804826287 / 2500000000000000000000)

theorem Zeta5Irrational.U_469_2 : Uω (aρ 2) (bρ 2) (16737641334457 / 32000000000000) ≤ -(1330270268776452498909 / 2000000000000000000000)

theorem Zeta5Irrational.U_469_3 : Uω (aρ 3) (bρ 3) (16737641334457 / 32000000000000) ≤ -(337248643719215027449 / 500000000000000000000)

theorem Zeta5Irrational.U_469_4 : Uω (aρ 4) (bρ 4) (16737641334457 / 32000000000000) ≤ -(3451298405747701115753 / 5000000000000000000000)

theorem Zeta5Irrational.U_469_5 : Uω (aρ 5) (bρ 5) (16737641334457 / 32000000000000) ≤ -(7147949625221588208791 / 10000000000000000000000)

theorem Zeta5Irrational.U_469_6 : Uω (aρ 6) (bρ 6) (16737641334457 / 32000000000000) ≤ -(3755872658039831526277 / 5000000000000000000000)

theorem Zeta5Irrational.U_469_7 : Uω (aρ 7) (bρ 7) (16737641334457 / 32000000000000) ≤ -(8032947538949810997407 / 10000000000000000000000)

theorem Zeta5Irrational.U_469_8 : Uω (aρ 8) (bρ 8) (16737641334457 / 32000000000000) ≤ -(8762680969486746709881 / 10000000000000000000000)

theorem Zeta5Irrational.U_469_9 : Uω (aρ 9) (bρ 9) (16737641334457 / 32000000000000) ≤ -(9774754545064592874979 / 10000000000000000000000)

theorem Zeta5Irrational.U_469_10 : Uω (aρ 10) (bρ 10) (16737641334457 / 32000000000000) ≤ -(2799166476393955032353 / 2500000000000000000000)

theorem Zeta5Irrational.U_469_11 : Uω (aρ 11) (bρ 11) (16737641334457 / 32000000000000) ≤ -(3333189941798207716189 / 2500000000000000000000)

theorem Zeta5Irrational.U_469_12 : Uω (aρ 12) (bρ 12) (16737641334457 / 32000000000000) ≤ -(18084834061631598644507 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_469 : Uρ (16737641334457 / 32000000000000) ≤ -(5092959469832835324207 / 5000000000000000000000)

theorem Zeta5Irrational.U_470_1 : Uω (aρ 1) (bρ 1) (33555169550949 / 64000000000000) ≤ -(1316152127732697187741 / 2000000000000000000000)

theorem Zeta5Irrational.U_470_2 : Uω (aρ 2) (bρ 2) (33555169550949 / 64000000000000) ≤ -(1656776186842113214311 / 2500000000000000000000)

theorem Zeta5Irrational.U_470_3 : Uω (aρ 3) (bρ 3) (33555169550949 / 64000000000000) ≤ -(6720495992657626363703 / 10000000000000000000000)

theorem Zeta5Irrational.U_470_4 : Uω (aρ 4) (bρ 4) (33555169550949 / 64000000000000) ≤ -(1719431176382352272803 / 2500000000000000000000)

theorem Zeta5Irrational.U_470_5 : Uω (aρ 5) (bρ 5) (33555169550949 / 64000000000000) ≤ -(3561221438257288238383 / 5000000000000000000000)

theorem Zeta5Irrational.U_470_6 : Uω (aρ 6) (bρ 6) (33555169550949 / 64000000000000) ≤ -(7485251371864224695571 / 10000000000000000000000)

theorem Zeta5Irrational.U_470_7 : Uω (aρ 7) (bρ 7) (33555169550949 / 64000000000000) ≤ -(8004934346840263548131 / 10000000000000000000000)

theorem Zeta5Irrational.U_470_8 : Uω (aρ 8) (bρ 8) (33555169550949 / 64000000000000) ≤ -(2183076059643294649347 / 2500000000000000000000)

theorem Zeta5Irrational.U_470_9 : Uω (aρ 9) (bρ 9) (33555169550949 / 64000000000000) ≤ -(9740545961313508592881 / 10000000000000000000000)

theorem Zeta5Irrational.U_470_10 : Uω (aρ 10) (bρ 10) (33555169550949 / 64000000000000) ≤ -(139445163964400578137 / 125000000000000000000)

theorem Zeta5Irrational.U_470_11 : Uω (aρ 11) (bρ 11) (33555169550949 / 64000000000000) ≤ -(13276151640471082417553 / 10000000000000000000000)

theorem Zeta5Irrational.U_470_12 : Uω (aρ 12) (bρ 12) (33555169550949 / 64000000000000) ≤ -(17893176801322932681187 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_470 : Uρ (33555169550949 / 64000000000000) ≤ -(1014905945163655209177 / 1000000000000000000000)

theorem Zeta5Irrational.U_471_1 : Uω (aρ 1) (bρ 1) (4204382054123 / 8000000000000) ≤ -(6556685210681737118977 / 10000000000000000000000)

theorem Zeta5Irrational.U_471_2 : Uω (aρ 2) (bρ 2) (4204382054123 / 8000000000000) ≤ -(6602916803099730944047 / 10000000000000000000000)

theorem Zeta5Irrational.U_471_3 : Uω (aρ 3) (bρ 3) (4204382054123 / 8000000000000) ≤ -(1339215778672726434163 / 2000000000000000000000)

theorem Zeta5Irrational.U_471_4 : Uω (aρ 4) (bρ 4) (4204382054123 / 8000000000000) ≤ -(6852914359553545011063 / 10000000000000000000000)

theorem Zeta5Irrational.U_471_5 : Uω (aρ 5) (bρ 5) (4204382054123 / 8000000000000) ≤ -(7097001165159826073773 / 10000000000000000000000)

theorem Zeta5Irrational.U_471_6 : Uω (aρ 6) (bρ 6) (4204382054123 / 8000000000000) ≤ -(3729413909532381592127 / 5000000000000000000000)

theorem Zeta5Irrational.U_471_7 : Uω (aρ 7) (bρ 7) (4204382054123 / 8000000000000) ≤ -(15580078944028729029 / 19531250000000000000)

theorem Zeta5Irrational.U_471_8 : Uω (aρ 8) (bρ 8) (4204382054123 / 8000000000000) ≤ -(8702022194771938875817 / 10000000000000000000000)

theorem Zeta5Irrational.U_471_9 : Uω (aρ 9) (bρ 9) (4204382054123 / 8000000000000) ≤ -(9706461627251655129437 / 10000000000000000000000)

theorem Zeta5Irrational.U_471_10 : Uω (aρ 10) (bρ 10) (4204382054123 / 8000000000000) ≤ -(2778688335021342273317 / 2500000000000000000000)

theorem Zeta5Irrational.U_471_11 : Uω (aρ 11) (bρ 11) (4204382054123 / 8000000000000) ≤ -(6609993535840864133789 / 5000000000000000000000)

theorem Zeta5Irrational.U_471_12 : Uω (aρ 12) (bρ 12) (4204382054123 / 8000000000000) ≤ -(3542999804663610854087 / 2000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_471 : Uρ (4204382054123 / 8000000000000) ≤ -(79009721845316621653 / 78125000000000000000)