Certified arcsine potential bounds (U39)

theorem Zeta5Irrational.U_472_1 : Uω (aρ 1) (bρ 1) (33714943315019 / 64000000000000) ≤ -(3266333803415444261449 / 5000000000000000000000)

theorem Zeta5Irrational.U_472_2 : Uω (aρ 2) (bρ 2) (33714943315019 / 64000000000000) ≤ -(3289393613990012216949 / 5000000000000000000000)

theorem Zeta5Irrational.U_472_3 : Uω (aρ 3) (bρ 3) (33714943315019 / 64000000000000) ≤ -(3335860642552980259753 / 5000000000000000000000)

theorem Zeta5Irrational.U_472_4 : Uω (aρ 4) (bρ 4) (33714943315019 / 64000000000000) ≤ -(853520683420242002753 / 1250000000000000000000)

theorem Zeta5Irrational.U_472_5 : Uω (aρ 5) (bρ 5) (33714943315019 / 64000000000000) ≤ -(3535812079804980335119 / 5000000000000000000000)

theorem Zeta5Irrational.U_472_6 : Uω (aρ 6) (bρ 6) (33714943315019 / 64000000000000) ≤ -(743247428260968271397 / 1000000000000000000000)

theorem Zeta5Irrational.U_472_7 : Uω (aρ 7) (bρ 7) (33714943315019 / 64000000000000) ≤ -(397457265176319725381 / 500000000000000000000)

theorem Zeta5Irrational.U_472_8 : Uω (aρ 8) (bρ 8) (33714943315019 / 64000000000000) ≤ -(8671834233232153227217 / 10000000000000000000000)

theorem Zeta5Irrational.U_472_9 : Uω (aρ 9) (bρ 9) (33714943315019 / 64000000000000) ≤ -(1209062573808391051687 / 1250000000000000000000)

theorem Zeta5Irrational.U_472_10 : Uω (aρ 10) (bρ 10) (33714943315019 / 64000000000000) ≤ -(11074084550028256930173 / 10000000000000000000000)

theorem Zeta5Irrational.U_472_11 : Uω (aρ 11) (bρ 11) (33714943315019 / 64000000000000) ≤ -(263285150516408844729 / 200000000000000000000)

theorem Zeta5Irrational.U_472_12 : Uω (aρ 12) (bρ 12) (33714943315019 / 64000000000000) ≤ -(3509569916371714106323 / 2000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_472 : Uρ (33714943315019 / 64000000000000) ≤ -(10078300210227161819509 / 10000000000000000000000)

theorem Zeta5Irrational.U_473_1 : Uω (aρ 1) (bρ 1) (16897415098527 / 32000000000000) ≤ -(6508707550010153423257 / 10000000000000000000000)

theorem Zeta5Irrational.U_473_2 : Uω (aρ 2) (bρ 2) (16897415098527 / 32000000000000) ≤ -(3277357870479055754481 / 5000000000000000000000)

theorem Zeta5Irrational.U_473_3 : Uω (aρ 3) (bρ 3) (16897415098527 / 32000000000000) ≤ -(830927859826774090171 / 1250000000000000000000)

theorem Zeta5Irrational.U_473_4 : Uω (aρ 4) (bρ 4) (16897415098527 / 32000000000000) ≤ -(6803477725022190286487 / 10000000000000000000000)

theorem Zeta5Irrational.U_473_5 : Uω (aρ 5) (bρ 5) (16897415098527 / 32000000000000) ≤ -(704631153085188042397 / 1000000000000000000000)

theorem Zeta5Irrational.U_473_6 : Uω (aρ 6) (bρ 6) (16897415098527 / 32000000000000) ≤ -(7406190390433035913379 / 10000000000000000000000)

theorem Zeta5Irrational.U_473_7 : Uω (aρ 7) (bρ 7) (16897415098527 / 32000000000000) ≤ -(7921368550378337604691 / 10000000000000000000000)

theorem Zeta5Irrational.U_473_8 : Uω (aρ 8) (bρ 8) (16897415098527 / 32000000000000) ≤ -(4320869877513572204633 / 5000000000000000000000)

theorem Zeta5Irrational.U_473_9 : Uω (aρ 9) (bρ 9) (16897415098527 / 32000000000000) ≤ -(1927732381998579928349 / 2000000000000000000000)

theorem Zeta5Irrational.U_473_10 : Uω (aρ 10) (bρ 10) (16897415098527 / 32000000000000) ≤ -(11033604756957846854013 / 10000000000000000000000)

theorem Zeta5Irrational.U_473_11 : Uω (aρ 11) (bρ 11) (16897415098527 / 32000000000000) ≤ -(262179094799017356733 / 200000000000000000000)

theorem Zeta5Irrational.U_473_12 : Uω (aρ 12) (bρ 12) (16897415098527 / 32000000000000) ≤ -(17389943031897199826591 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_473 : Uρ (16897415098527 / 32000000000000) ≤ -(1255512523990723562393 / 1250000000000000000000)

theorem Zeta5Irrational.U_474_1 : Uω (aρ 1) (bρ 1) (33874717079089 / 64000000000000) ≤ -(25939219060423466283 / 40000000000000000000)

theorem Zeta5Irrational.U_474_2 : Uω (aρ 2) (bρ 2) (33874717079089 / 64000000000000) ≤ -(1306140412601594962099 / 2000000000000000000000)

theorem Zeta5Irrational.U_474_3 : Uω (aρ 3) (bρ 3) (33874717079089 / 64000000000000) ≤ -(3311591693361606929099 / 5000000000000000000000)

theorem Zeta5Irrational.U_474_4 : Uω (aρ 4) (bρ 4) (33874717079089 / 64000000000000) ≤ -(677885083085293050957 / 1000000000000000000000)

theorem Zeta5Irrational.U_474_5 : Uω (aρ 5) (bρ 5) (33874717079089 / 64000000000000) ≤ -(28084251809523764379 / 40000000000000000000)

theorem Zeta5Irrational.U_474_6 : Uω (aρ 6) (bρ 6) (33874717079089 / 64000000000000) ≤ -(1475995154688466043879 / 2000000000000000000000)

theorem Zeta5Irrational.U_474_7 : Uω (aρ 7) (bρ 7) (33874717079089 / 64000000000000) ≤ -(7893669714757767057957 / 10000000000000000000000)

theorem Zeta5Irrational.U_474_8 : Uω (aρ 8) (bρ 8) (33874717079089 / 64000000000000) ≤ -(8611738167075583192321 / 10000000000000000000000)

theorem Zeta5Irrational.U_474_9 : Uω (aρ 9) (bρ 9) (33874717079089 / 64000000000000) ≤ -(9604944656117145227967 / 10000000000000000000000)

theorem Zeta5Irrational.U_474_10 : Uω (aρ 10) (bρ 10) (33874717079089 / 64000000000000) ≤ -(5496656002181523759141 / 5000000000000000000000)

theorem Zeta5Irrational.U_474_11 : Uω (aρ 11) (bρ 11) (33874717079089 / 64000000000000) ≤ -(13054070711118162002301 / 10000000000000000000000)

theorem Zeta5Irrational.U_474_12 : Uω (aρ 12) (bρ 12) (33874717079089 / 64000000000000) ≤ -(17239930913919872437509 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_474 : Uρ (33874717079089 / 64000000000000) ≤ -(2002109681776138421131 / 2000000000000000000000)

theorem Zeta5Irrational.U_475_1 : Uω (aρ 1) (bρ 1) (8488650990281 / 16000000000000) ≤ -(6460958978972525251067 / 10000000000000000000000)

theorem Zeta5Irrational.U_475_2 : Uω (aρ 2) (bρ 2) (8488650990281 / 16000000000000) ≤ -(3253372958554693937133 / 5000000000000000000000)

theorem Zeta5Irrational.U_475_3 : Uω (aρ 3) (bρ 3) (8488650990281 / 16000000000000) ≤ -(1649750631088205402597 / 2500000000000000000000)

theorem Zeta5Irrational.U_475_4 : Uω (aρ 4) (bρ 4) (8488650990281 / 16000000000000) ≤ -(3377142242700800895389 / 5000000000000000000000)

theorem Zeta5Irrational.U_475_5 : Uω (aρ 5) (bρ 5) (8488650990281 / 16000000000000) ≤ -(1748969525043867698289 / 2500000000000000000000)

theorem Zeta5Irrational.U_475_6 : Uω (aρ 6) (bρ 6) (8488650990281 / 16000000000000) ≤ -(3676915032743383951457 / 5000000000000000000000)

theorem Zeta5Irrational.U_475_7 : Uω (aρ 7) (bρ 7) (8488650990281 / 16000000000000) ≤ -(7866048355351224914357 / 10000000000000000000000)

theorem Zeta5Irrational.U_475_8 : Uω (aρ 8) (bρ 8) (8488650990281 / 16000000000000) ≤ -(858182888206397318407 / 1000000000000000000000)

theorem Zeta5Irrational.U_475_9 : Uω (aρ 9) (bρ 9) (8488650990281 / 16000000000000) ≤ -(2392836977549402281269 / 2500000000000000000000)

theorem Zeta5Irrational.U_475_10 : Uω (aρ 10) (bρ 10) (8488650990281 / 16000000000000) ≤ -(10953204368456377232327 / 10000000000000000000000)

theorem Zeta5Irrational.U_475_11 : Uω (aρ 11) (bρ 11) (8488650990281 / 16000000000000) ≤ -(3249899421236699954177 / 2500000000000000000000)

theorem Zeta5Irrational.U_475_12 : Uω (aρ 12) (bρ 12) (8488650990281 / 16000000000000) ≤ -(854838257289714201947 / 500000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_475 : Uρ (8488650990281 / 16000000000000) ≤ -(9977570086192114256609 / 10000000000000000000000)

theorem Zeta5Irrational.U_476_1 : Uω (aρ 1) (bρ 1) (34034490843159 / 64000000000000) ≤ -(6437169920414059672691 / 10000000000000000000000)

theorem Zeta5Irrational.U_476_2 : Uω (aρ 2) (bρ 2) (34034490843159 / 64000000000000) ≤ -(6482847028228737411169 / 10000000000000000000000)

theorem Zeta5Irrational.U_476_3 : Uω (aρ 3) (bρ 3) (34034490843159 / 64000000000000) ≤ -(6574880008487592758289 / 10000000000000000000000)

theorem Zeta5Irrational.U_476_4 : Uω (aρ 4) (bρ 4) (34034490843159 / 64000000000000) ≤ -(105152787365977387829 / 156250000000000000000)

theorem Zeta5Irrational.U_476_5 : Uω (aρ 5) (bρ 5) (34034490843159 / 64000000000000) ≤ -(1742689163167899786689 / 2500000000000000000000)

theorem Zeta5Irrational.U_476_6 : Uω (aρ 6) (bρ 6) (34034490843159 / 64000000000000) ≤ -(7327752903325907666223 / 10000000000000000000000)

theorem Zeta5Irrational.U_476_7 : Uω (aρ 7) (bρ 7) (34034490843159 / 64000000000000) ≤ -(244953251082135055187 / 312500000000000000000)

theorem Zeta5Irrational.U_476_8 : Uω (aρ 8) (bρ 8) (34034490843159 / 64000000000000) ≤ -(855201131837044779203 / 1000000000000000000000)

theorem Zeta5Irrational.U_476_9 : Uω (aρ 9) (bρ 9) (34034490843159 / 64000000000000) ≤ -(190757415289597866371 / 200000000000000000000)

theorem Zeta5Irrational.U_476_10 : Uω (aρ 10) (bρ 10) (34034490843159 / 64000000000000) ≤ -(10913279957409600345849 / 10000000000000000000000)

theorem Zeta5Irrational.U_476_11 : Uω (aρ 11) (bρ 11) (34034490843159 / 64000000000000) ≤ -(6472764072437904424893 / 5000000000000000000000)

theorem Zeta5Irrational.U_476_12 : Uω (aρ 12) (bρ 12) (34034490843159 / 64000000000000) ≤ -(16959611872217714546673 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_476 : Uρ (34034490843159 / 64000000000000) ≤ -(62156909653359306433 / 62500000000000000000)

theorem Zeta5Irrational.U_477_1 : Uω (aρ 1) (bρ 1) (17057188862597 / 32000000000000) ≤ -(1603359330041331640883 / 2500000000000000000000)

theorem Zeta5Irrational.U_477_2 : Uω (aρ 2) (bρ 2) (17057188862597 / 32000000000000) ≤ -(6459005123300066603403 / 10000000000000000000000)

theorem Zeta5Irrational.U_477_3 : Uω (aρ 3) (bρ 3) (17057188862597 / 32000000000000) ≤ -(1310163111631396293071 / 2000000000000000000000)

theorem Zeta5Irrational.U_477_4 : Uω (aρ 4) (bρ 4) (17057188862597 / 32000000000000) ≤ -(6705332253855386408567 / 10000000000000000000000)

theorem Zeta5Irrational.U_477_5 : Uω (aρ 5) (bρ 5) (17057188862597 / 32000000000000) ≤ -(3472849145369206145161 / 5000000000000000000000)

theorem Zeta5Irrational.U_477_6 : Uω (aρ 6) (bρ 6) (17057188862597 / 32000000000000) ≤ -(7301743926598747382951 / 10000000000000000000000)

theorem Zeta5Irrational.U_477_7 : Uω (aρ 7) (bρ 7) (17057188862597 / 32000000000000) ≤ -(1562207263759628217761 / 2000000000000000000000)

theorem Zeta5Irrational.U_477_8 : Uω (aρ 8) (bρ 8) (17057188862597 / 32000000000000) ≤ -(8522284899989832254591 / 10000000000000000000000)

theorem Zeta5Irrational.U_477_9 : Uω (aρ 9) (bρ 9) (17057188862597 / 32000000000000) ≤ -(950451232191955561317 / 1000000000000000000000)

theorem Zeta5Irrational.U_477_10 : Uω (aρ 10) (bρ 10) (17057188862597 / 32000000000000) ≤ -(10873536910612324331361 / 10000000000000000000000)

theorem Zeta5Irrational.U_477_11 : Uω (aρ 11) (bρ 11) (17057188862597 / 32000000000000) ≤ -(12891854801988329159687 / 10000000000000000000000)

theorem Zeta5Irrational.U_477_12 : Uω (aρ 12) (bρ 12) (17057188862597 / 32000000000000) ≤ -(2103474338028338746597 / 1250000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_477 : Uρ (17057188862597 / 32000000000000) ≤ -(2478276551493754470733 / 2500000000000000000000)

theorem Zeta5Irrational.U_478_1 : Uω (aρ 1) (bρ 1) (34194264607229 / 64000000000000) ≤ -(6389760910873824690131 / 10000000000000000000000)

theorem Zeta5Irrational.U_478_2 : Uω (aρ 2) (bρ 2) (34194264607229 / 64000000000000) ≤ -(6435219931206354359771 / 10000000000000000000000)

theorem Zeta5Irrational.U_478_3 : Uω (aρ 3) (bρ 3) (34194264607229 / 64000000000000) ≤ -(6526808894415663314091 / 10000000000000000000000)

theorem Zeta5Irrational.U_478_4 : Uω (aρ 4) (bρ 4) (34194264607229 / 64000000000000) ≤ -(1670236444950892870231 / 2500000000000000000000)

theorem Zeta5Irrational.U_478_5 : Uω (aρ 5) (bρ 5) (34194264607229 / 64000000000000) ≤ -(3460351350126436706987 / 5000000000000000000000)

theorem Zeta5Irrational.U_478_6 : Uω (aρ 6) (bρ 6) (34194264607229 / 64000000000000) ≤ -(7275802777793215124253 / 10000000000000000000000)

theorem Zeta5Irrational.U_478_7 : Uω (aρ 7) (bρ 7) (34194264607229 / 64000000000000) ≤ -(194591119444156857651 / 250000000000000000000)

theorem Zeta5Irrational.U_478_8 : Uω (aρ 8) (bρ 8) (34194264607229 / 64000000000000) ≤ -(8492649056459973840639 / 10000000000000000000000)

theorem Zeta5Irrational.U_478_9 : Uω (aρ 9) (bρ 9) (34194264607229 / 64000000000000) ≤ -(9471271696007942156663 / 10000000000000000000000)

theorem Zeta5Irrational.U_478_10 : Uω (aρ 10) (bρ 10) (34194264607229 / 64000000000000) ≤ -(5416986698976334785817 / 5000000000000000000000)

theorem Zeta5Irrational.U_478_11 : Uω (aρ 11) (bρ 11) (34194264607229 / 64000000000000) ≤ -(12838570585395820165127 / 10000000000000000000000)

theorem Zeta5Irrational.U_478_12 : Uω (aρ 12) (bρ 12) (34194264607229 / 64000000000000) ≤ -(4175188987432682907409 / 2500000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_478 : Uρ (34194264607229 / 64000000000000) ≤ -(123519148321299201723 / 125000000000000000000)

theorem Zeta5Irrational.U_479_1 : Uω (aρ 1) (bρ 1) (68468416096493 / 128000000000000) ≤ -(637794369480791432831 / 1000000000000000000000)

theorem Zeta5Irrational.U_479_2 : Uω (aρ 2) (bρ 2) (68468416096493 / 128000000000000) ≤ -(321167425913844597629 / 500000000000000000000)

theorem Zeta5Irrational.U_479_3 : Uω (aρ 3) (bρ 3) (68468416096493 / 128000000000000) ≤ -(1302965429178912640407 / 2000000000000000000000)

theorem Zeta5Irrational.U_479_4 : Uω (aρ 4) (bρ 4) (68468416096493 / 128000000000000) ≤ -(3334387412826117338583 / 5000000000000000000000)

theorem Zeta5Irrational.U_479_5 : Uω (aρ 5) (bρ 5) (68468416096493 / 128000000000000) ≤ -(276329133748210301077 / 400000000000000000000)

theorem Zeta5Irrational.U_479_6 : Uω (aρ 6) (bρ 6) (68468416096493 / 128000000000000) ≤ -(7262857527910127196811 / 10000000000000000000000)

theorem Zeta5Irrational.U_479_7 : Uω (aρ 7) (bρ 7) (68468416096493 / 128000000000000) ≤ -(7769977439395536664309 / 10000000000000000000000)

theorem Zeta5Irrational.U_479_8 : Uω (aρ 8) (bρ 8) (68468416096493 / 128000000000000) ≤ -(8477864923492468921267 / 10000000000000000000000)

theorem Zeta5Irrational.U_479_9 : Uω (aρ 9) (bρ 9) (68468416096493 / 128000000000000) ≤ -(9454695290100289161531 / 10000000000000000000000)

theorem Zeta5Irrational.U_479_10 : Uω (aρ 10) (bρ 10) (68468416096493 / 128000000000000) ≤ -(10814258403181725422127 / 10000000000000000000000)

theorem Zeta5Irrational.U_479_11 : Uω (aρ 11) (bρ 11) (68468416096493 / 128000000000000) ≤ -(12812072247175655142927 / 10000000000000000000000)

theorem Zeta5Irrational.U_479_12 : Uω (aρ 12) (bρ 12) (68468416096493 / 128000000000000) ≤ -(16638879770636086593247 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_479 : Uρ (68468416096493 / 128000000000000) ≤ -(2466473327665301070027 / 2500000000000000000000)

theorem Zeta5Irrational.U_480_1 : Uω (aρ 1) (bρ 1) (2142134468079 / 4000000000000) ≤ -(10185824683330590031 / 16000000000000000000)

theorem Zeta5Irrational.U_480_2 : Uω (aρ 2) (bρ 2) (2142134468079 / 4000000000000) ≤ -(1602872795690252040067 / 2500000000000000000000)

theorem Zeta5Irrational.U_480_3 : Uω (aρ 3) (bρ 3) (2142134468079 / 4000000000000) ≤ -(6502859740324113881097 / 10000000000000000000000)

theorem Zeta5Irrational.U_480_4 : Uω (aρ 4) (bρ 4) (2142134468079 / 4000000000000) ≤ -(6656618678513322478103 / 10000000000000000000000)

theorem Zeta5Irrational.U_480_5 : Uω (aρ 5) (bρ 5) (2142134468079 / 4000000000000) ≤ -(21549279880243073947 / 31250000000000000000)

theorem Zeta5Irrational.U_480_6 : Uω (aρ 6) (bρ 6) (2142134468079 / 4000000000000) ≤ -(7249929102216071350707 / 10000000000000000000000)

theorem Zeta5Irrational.U_480_7 : Uω (aρ 7) (bρ 7) (2142134468079 / 4000000000000) ≤ -(7756328985092475948893 / 10000000000000000000000)

theorem Zeta5Irrational.U_480_8 : Uω (aρ 8) (bρ 8) (2142134468079 / 4000000000000) ≤ -(8463103222789283762703 / 10000000000000000000000)

theorem Zeta5Irrational.U_480_9 : Uω (aρ 9) (bρ 9) (2142134468079 / 4000000000000) ≤ -(4719074005300819373633 / 5000000000000000000000)

theorem Zeta5Irrational.U_480_10 : Uω (aρ 10) (bρ 10) (2142134468079 / 4000000000000) ≤ -(10794587619119258863077 / 10000000000000000000000)

theorem Zeta5Irrational.U_480_11 : Uω (aρ 11) (bρ 11) (2142134468079 / 4000000000000) ≤ -(12785668633140302686513 / 10000000000000000000000)

theorem Zeta5Irrational.U_480_12 : Uω (aρ 12) (bρ 12) (2142134468079 / 4000000000000) ≤ -(8289014659856279049473 / 5000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_480 : Uρ (2142134468079 / 4000000000000) ≤ -(2462587192580934883643 / 2500000000000000000000)

theorem Zeta5Irrational.U_481_1 : Uω (aρ 1) (bρ 1) (68628189860563 / 128000000000000) ≤ -(635435107480579353849 / 1000000000000000000000)

theorem Zeta5Irrational.U_481_2 : Uω (aρ 2) (bρ 2) (68628189860563 / 128000000000000) ≤ -(799955986413626136757 / 1250000000000000000000)

theorem Zeta5Irrational.U_481_3 : Uω (aρ 3) (bρ 3) (68628189860563 / 128000000000000) ≤ -(6490906643397133693603 / 10000000000000000000000)

theorem Zeta5Irrational.U_481_4 : Uω (aρ 4) (bρ 4) (68628189860563 / 128000000000000) ≤ -(6644477302373994372467 / 10000000000000000000000)

theorem Zeta5Irrational.U_481_5 : Uω (aρ 5) (bρ 5) (68628189860563 / 128000000000000) ≤ -(6883326315246774074947 / 10000000000000000000000)

theorem Zeta5Irrational.U_481_6 : Uω (aρ 6) (bρ 6) (68628189860563 / 128000000000000) ≤ -(7237017456809963206417 / 10000000000000000000000)

theorem Zeta5Irrational.U_481_7 : Uω (aρ 7) (bρ 7) (68628189860563 / 128000000000000) ≤ -(7742699362116177004641 / 10000000000000000000000)

theorem Zeta5Irrational.U_481_8 : Uω (aρ 8) (bρ 8) (68628189860563 / 128000000000000) ≤ -(33793455538278231109 / 40000000000000000000)

theorem Zeta5Irrational.U_481_9 : Uω (aρ 9) (bρ 9) (68628189860563 / 128000000000000) ≤ -(9421629749586235676443 / 10000000000000000000000)

theorem Zeta5Irrational.U_481_10 : Uω (aρ 10) (bρ 10) (68628189860563 / 128000000000000) ≤ -(10774960825271525424907 / 10000000000000000000000)

theorem Zeta5Irrational.U_481_11 : Uω (aρ 11) (bρ 11) (68628189860563 / 128000000000000) ≤ -(6379679458388677789959 / 5000000000000000000000)

theorem Zeta5Irrational.U_481_12 : Uω (aρ 12) (bρ 12) (68628189860563 / 128000000000000) ≤ -(3303631472747489113263 / 2000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_481 : Uρ (68628189860563 / 128000000000000) ≤ -(4917447403195761472373 / 5000000000000000000000)

theorem Zeta5Irrational.U_482_1 : Uω (aρ 1) (bρ 1) (34354038371299 / 64000000000000) ≤ -(3171287802603740539783 / 5000000000000000000000)

theorem Zeta5Irrational.U_482_2 : Uω (aρ 2) (bρ 2) (34354038371299 / 64000000000000) ≤ -(159695465267239470827 / 250000000000000000000)

theorem Zeta5Irrational.U_482_3 : Uω (aρ 3) (bρ 3) (34354038371299 / 64000000000000) ≤ -(1619741955232353905561 / 2500000000000000000000)

theorem Zeta5Irrational.U_482_4 : Uω (aρ 4) (bρ 4) (34354038371299 / 64000000000000) ≤ -(6632350661352732514341 / 10000000000000000000000)

theorem Zeta5Irrational.U_482_5 : Uω (aρ 5) (bρ 5) (34354038371299 / 64000000000000) ≤ -(3435449282817292923889 / 5000000000000000000000)

theorem Zeta5Irrational.U_482_6 : Uω (aρ 6) (bρ 6) (34354038371299 / 64000000000000) ≤ -(3612061273981600181139 / 5000000000000000000000)

theorem Zeta5Irrational.U_482_7 : Uω (aρ 7) (bρ 7) (34354038371299 / 64000000000000) ≤ -(7729088517948928495677 / 10000000000000000000000)

theorem Zeta5Irrational.U_482_8 : Uω (aρ 8) (bρ 8) (34354038371299 / 64000000000000) ≤ -(4216823419692748033009 / 5000000000000000000000)

theorem Zeta5Irrational.U_482_9 : Uω (aρ 9) (bρ 9) (34354038371299 / 64000000000000) ≤ -(2351285099938865213181 / 2500000000000000000000)

theorem Zeta5Irrational.U_482_10 : Uω (aρ 10) (bρ 10) (34354038371299 / 64000000000000) ≤ -(84026389085341504191 / 78125000000000000000)

theorem Zeta5Irrational.U_482_11 : Uω (aρ 11) (bρ 11) (34354038371299 / 64000000000000) ≤ -(2546628456716178291753 / 2000000000000000000000)

theorem Zeta5Irrational.U_482_12 : Uω (aρ 12) (bρ 12) (34354038371299 / 64000000000000) ≤ -(16459220212367328245369 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_482 : Uρ (34354038371299 / 64000000000000) ≤ -(9819528231062824967897 / 10000000000000000000000)

theorem Zeta5Irrational.U_483_1 : Uω (aρ 1) (bρ 1) (68787963624633 / 128000000000000) ≤ -(6330813985629369780369 / 10000000000000000000000)

theorem Zeta5Irrational.U_483_2 : Uω (aρ 2) (bρ 2) (68787963624633 / 128000000000000) ≤ -(3188001653894608997351 / 5000000000000000000000)

theorem Zeta5Irrational.U_483_3 : Uω (aρ 3) (bρ 3) (68787963624633 / 128000000000000) ≤ -(3233521619429571196959 / 5000000000000000000000)

theorem Zeta5Irrational.U_483_4 : Uω (aρ 4) (bρ 4) (68787963624633 / 128000000000000) ≤ -(6620238719698710557651 / 10000000000000000000000)

theorem Zeta5Irrational.U_483_5 : Uω (aρ 5) (bρ 5) (68787963624633 / 128000000000000) ≤ -(3429243137104443273827 / 5000000000000000000000)

theorem Zeta5Irrational.U_483_6 : Uω (aρ 6) (bρ 6) (68787963624633 / 128000000000000) ≤ -(7211244332118761894243 / 10000000000000000000000)

theorem Zeta5Irrational.U_483_7 : Uω (aρ 7) (bρ 7) (68787963624633 / 128000000000000) ≤ -(3857748200147473405413 / 5000000000000000000000)

theorem Zeta5Irrational.U_483_8 : Uω (aρ 8) (bρ 8) (68787963624633 / 128000000000000) ≤ -(210473800453005356507 / 250000000000000000000)

theorem Zeta5Irrational.U_483_9 : Uω (aρ 9) (bρ 9) (68787963624633 / 128000000000000) ≤ -(2347169963608201734619 / 2500000000000000000000)

theorem Zeta5Irrational.U_483_10 : Uω (aρ 10) (bρ 10) (68787963624633 / 128000000000000) ≤ -(10735838335119840614069 / 10000000000000000000000)

theorem Zeta5Irrational.U_483_11 : Uω (aρ 11) (bρ 11) (68787963624633 / 128000000000000) ≤ -(12707017930806615344121 / 10000000000000000000000)

theorem Zeta5Irrational.U_483_12 : Uω (aρ 12) (bρ 12) (68787963624633 / 128000000000000) ≤ -(3280235471263865683437 / 2000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_483 : Uρ (68787963624633 / 128000000000000) ≤ -(980424608155701660297 / 1000000000000000000000)