Certified arcsine potential bounds (U37)

theorem Zeta5Irrational.U_448_1 : Uω (aρ 1) (bρ 1) (47053570071 / 100000000000) ≤ -(1919232376114736975373 / 2500000000000000000000)

theorem Zeta5Irrational.U_448_2 : Uω (aρ 2) (bρ 2) (47053570071 / 100000000000) ≤ -(1545740118644833119621 / 2000000000000000000000)

theorem Zeta5Irrational.U_448_3 : Uω (aρ 3) (bρ 3) (47053570071 / 100000000000) ≤ -(391657943934962024627 / 500000000000000000000)

theorem Zeta5Irrational.U_448_4 : Uω (aρ 4) (bρ 4) (47053570071 / 100000000000) ≤ -(8009424585511980867437 / 10000000000000000000000)

theorem Zeta5Irrational.U_448_5 : Uω (aρ 5) (bρ 5) (47053570071 / 100000000000) ≤ -(8284829247633143014031 / 10000000000000000000000)

theorem Zeta5Irrational.U_448_6 : Uω (aρ 6) (bρ 6) (47053570071 / 100000000000) ≤ -(434783471547781231521 / 500000000000000000000)

theorem Zeta5Irrational.U_448_7 : Uω (aρ 7) (bρ 7) (47053570071 / 100000000000) ≤ -(2322505915292548785069 / 2500000000000000000000)

theorem Zeta5Irrational.U_448_8 : Uω (aρ 8) (bρ 8) (47053570071 / 100000000000) ≤ -(5067773603948575405307 / 5000000000000000000000)

theorem Zeta5Irrational.U_448_9 : Uω (aρ 9) (bρ 9) (47053570071 / 100000000000) ≤ -(7088289782332541623 / 6250000000000000000)

theorem Zeta5Irrational.U_448_10 : Uω (aρ 10) (bρ 10) (47053570071 / 100000000000) ≤ -(13132296129856771453691 / 10000000000000000000000)

theorem Zeta5Irrational.U_448_11 : Uω (aρ 11) (bρ 11) (47053570071 / 100000000000) ≤ -(16301865280119978924169 / 10000000000000000000000)

theorem Zeta5Irrational.U_448_12 : Uω (aρ 12) (bρ 12) (47053570071 / 100000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_448_13 : Uω (aρ 13) (bρ 13) (47053570071 / 100000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_448_14 : Uω (aρ 14) (bρ 14) (47053570071 / 100000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_448_15 : Uω (aρ 15) (bρ 15) (47053570071 / 100000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_448_16 : Uω (aρ 16) (bρ 16) (47053570071 / 100000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_448 : Uρ (47053570071 / 100000000000) ≤ -(1430900979261067775189 / 1250000000000000000000)

theorem Zeta5Irrational.U_449_1 : Uω (aρ 1) (bρ 1) (943720001173 / 2000000000000) ≤ -(7648434056806039205791 / 10000000000000000000000)

theorem Zeta5Irrational.U_449_2 : Uω (aρ 2) (bρ 2) (943720001173 / 2000000000000) ≤ -(7700056245118668029321 / 10000000000000000000000)

theorem Zeta5Irrational.U_449_3 : Uω (aρ 3) (bρ 3) (943720001173 / 2000000000000) ≤ -(3902105255140000568633 / 5000000000000000000000)

theorem Zeta5Irrational.U_449_4 : Uω (aρ 4) (bρ 4) (943720001173 / 2000000000000) ≤ -(3989976034925886310423 / 5000000000000000000000)

theorem Zeta5Irrational.U_449_5 : Uω (aρ 5) (bρ 5) (943720001173 / 2000000000000) ≤ -(8254508612734525013499 / 10000000000000000000000)

theorem Zeta5Irrational.U_449_6 : Uω (aρ 6) (bρ 6) (943720001173 / 2000000000000) ≤ -(8664013019972345318039 / 10000000000000000000000)

theorem Zeta5Irrational.U_449_7 : Uω (aρ 7) (bρ 7) (943720001173 / 2000000000000) ≤ -(9256269520445819727293 / 10000000000000000000000)

theorem Zeta5Irrational.U_449_8 : Uω (aρ 8) (bρ 8) (943720001173 / 2000000000000) ≤ -(2524604255347409636449 / 2500000000000000000000)

theorem Zeta5Irrational.U_449_9 : Uω (aρ 9) (bρ 9) (943720001173 / 2000000000000) ≤ -(11298315421504753008881 / 10000000000000000000000)

theorem Zeta5Irrational.U_449_10 : Uω (aρ 10) (bρ 10) (943720001173 / 2000000000000) ≤ -(6538762754409200956687 / 5000000000000000000000)

theorem Zeta5Irrational.U_449_11 : Uω (aρ 11) (bρ 11) (943720001173 / 2000000000000) ≤ -(8102928517530189352599 / 5000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_449 : Uρ (943720001173 / 2000000000000) ≤ -(11416320353268018089979 / 10000000000000000000000)

theorem Zeta5Irrational.U_450_1 : Uω (aρ 1) (bρ 1) (473184300463 / 1000000000000) ≤ -(476251223671478843051 / 625000000000000000000)

theorem Zeta5Irrational.U_450_2 : Uω (aρ 2) (bρ 2) (473184300463 / 1000000000000) ≤ -(3835746860328307421921 / 5000000000000000000000)

theorem Zeta5Irrational.U_450_3 : Uω (aρ 3) (bρ 3) (473184300463 / 1000000000000) ≤ -(971918216274480697521 / 1250000000000000000000)

theorem Zeta5Irrational.U_450_4 : Uω (aρ 4) (bρ 4) (473184300463 / 1000000000000) ≤ -(1987641562899738892589 / 2500000000000000000000)

theorem Zeta5Irrational.U_450_5 : Uω (aρ 5) (bρ 5) (473184300463 / 1000000000000) ≤ -(8224279888071012172189 / 10000000000000000000000)

theorem Zeta5Irrational.U_450_6 : Uω (aρ 6) (bρ 6) (473184300463 / 1000000000000) ≤ -(8632457199341266362179 / 10000000000000000000000)

theorem Zeta5Irrational.U_450_7 : Uω (aρ 7) (bρ 7) (473184300463 / 1000000000000) ≤ -(9222630815204496616637 / 10000000000000000000000)

theorem Zeta5Irrational.U_450_8 : Uω (aρ 8) (bρ 8) (473184300463 / 1000000000000) ≤ -(10061429492772882776433 / 10000000000000000000000)

theorem Zeta5Irrational.U_450_9 : Uω (aρ 9) (bρ 9) (473184300463 / 1000000000000) ≤ -(2813891859876060749109 / 2500000000000000000000)

theorem Zeta5Irrational.U_450_10 : Uω (aρ 10) (bρ 10) (473184300463 / 1000000000000) ≤ -(6511560604696648093569 / 5000000000000000000000)

theorem Zeta5Irrational.U_450_11 : Uω (aρ 11) (bρ 11) (473184300463 / 1000000000000) ≤ -(16111517734219643503701 / 10000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_450 : Uρ (473184300463 / 1000000000000) ≤ -(11385662126578536729411 / 10000000000000000000000)

theorem Zeta5Irrational.U_451_1 : Uω (aρ 1) (bρ 1) (949017200679 / 2000000000000) ≤ -(948960701427451485171 / 1250000000000000000000)

theorem Zeta5Irrational.U_451_2 : Uω (aρ 2) (bρ 2) (949017200679 / 2000000000000) ≤ -(3821506276829465306197 / 5000000000000000000000)

theorem Zeta5Irrational.U_451_3 : Uω (aρ 3) (bρ 3) (949017200679 / 2000000000000) ≤ -(242080126779563267641 / 312500000000000000000)

theorem Zeta5Irrational.U_451_4 : Uω (aρ 4) (bρ 4) (949017200679 / 2000000000000) ≤ -(7921266621662072203433 / 10000000000000000000000)

theorem Zeta5Irrational.U_451_5 : Uω (aρ 5) (bρ 5) (949017200679 / 2000000000000) ≤ -(8194142516591679673101 / 10000000000000000000000)

theorem Zeta5Irrational.U_451_6 : Uω (aρ 6) (bρ 6) (949017200679 / 2000000000000) ≤ -(8601001327470226045849 / 10000000000000000000000)

theorem Zeta5Irrational.U_451_7 : Uω (aρ 7) (bρ 7) (949017200679 / 2000000000000) ≤ -(9189106745930102249407 / 10000000000000000000000)

theorem Zeta5Irrational.U_451_8 : Uω (aρ 8) (bρ 8) (949017200679 / 2000000000000) ≤ -(2506145872626381178453 / 2500000000000000000000)

theorem Zeta5Irrational.U_451_9 : Uω (aρ 9) (bρ 9) (949017200679 / 2000000000000) ≤ -(11213017700970506234207 / 10000000000000000000000)

theorem Zeta5Irrational.U_451_10 : Uω (aρ 10) (bρ 10) (949017200679 / 2000000000000) ≤ -(1296907755686059853951 / 1000000000000000000000)

theorem Zeta5Irrational.U_451_11 : Uω (aρ 11) (bρ 11) (949017200679 / 2000000000000) ≤ -(25630033977972161371 / 16000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_451 : Uρ (949017200679 / 2000000000000) ≤ -(1135522615867193342733 / 1000000000000000000000)

theorem Zeta5Irrational.U_452_1 : Uω (aρ 1) (bρ 1) (59479112527 / 125000000000) ≤ -(1890857924967793981321 / 2500000000000000000000)

theorem Zeta5Irrational.U_452_2 : Uω (aρ 2) (bρ 2) (59479112527 / 125000000000) ≤ -(1522922456383919548857 / 2000000000000000000000)

theorem Zeta5Irrational.U_452_3 : Uω (aρ 3) (bρ 3) (59479112527 / 125000000000) ≤ -(7717865013179724929687 / 10000000000000000000000)

theorem Zeta5Irrational.U_452_4 : Uω (aρ 4) (bρ 4) (59479112527 / 125000000000) ≤ -(7892052675425208535167 / 10000000000000000000000)

theorem Zeta5Irrational.U_452_5 : Uω (aρ 5) (bρ 5) (59479112527 / 125000000000) ≤ -(4082047973154115081541 / 5000000000000000000000)

theorem Zeta5Irrational.U_452_6 : Uω (aρ 6) (bρ 6) (59479112527 / 125000000000) ≤ -(8569644768926593276099 / 10000000000000000000000)

theorem Zeta5Irrational.U_452_7 : Uω (aρ 7) (bρ 7) (59479112527 / 125000000000) ≤ -(9155696521510087946207 / 10000000000000000000000)

theorem Zeta5Irrational.U_452_8 : Uω (aρ 8) (bρ 8) (59479112527 / 125000000000) ≤ -(4993938948443957304859 / 5000000000000000000000)

theorem Zeta5Irrational.U_452_9 : Uω (aρ 9) (bρ 9) (59479112527 / 125000000000) ≤ -(2792666058235790186179 / 2500000000000000000000)

theorem Zeta5Irrational.U_452_10 : Uω (aρ 10) (bρ 10) (59479112527 / 125000000000) ≤ -(12915389020402956627827 / 10000000000000000000000)

theorem Zeta5Irrational.U_452_11 : Uω (aρ 11) (bρ 11) (59479112527 / 125000000000) ≤ -(7963773541683381200579 / 5000000000000000000000)

theorem Zeta5Irrational.U_452_12 : Uω (aρ 12) (bρ 12) (59479112527 / 125000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_452_13 : Uω (aρ 13) (bρ 13) (59479112527 / 125000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_452_14 : Uω (aρ 14) (bρ 14) (59479112527 / 125000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_452_15 : Uω (aρ 15) (bρ 15) (59479112527 / 125000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_452_16 : Uω (aρ 16) (bρ 16) (59479112527 / 125000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_452 : Uρ (59479112527 / 125000000000) ≤ -(2265001184222090608171 / 2000000000000000000000)

theorem Zeta5Irrational.U_453_1 : Uω (aρ 1) (bρ 1) (190862880037 / 400000000000) ≤ -(7535257392981299478961 / 10000000000000000000000)

theorem Zeta5Irrational.U_453_2 : Uω (aρ 2) (bρ 2) (190862880037 / 400000000000) ≤ -(7586292447160640009489 / 10000000000000000000000)

theorem Zeta5Irrational.U_453_3 : Uω (aρ 3) (bρ 3) (190862880037 / 400000000000) ≤ -(3844624062824249615123 / 5000000000000000000000)

theorem Zeta5Irrational.U_453_4 : Uω (aρ 4) (bρ 4) (190862880037 / 400000000000) ≤ -(1572584782539127471169 / 2000000000000000000000)

theorem Zeta5Irrational.U_453_5 : Uω (aρ 5) (bρ 5) (190862880037 / 400000000000) ≤ -(1016767453779209346861 / 1250000000000000000000)

theorem Zeta5Irrational.U_453_6 : Uω (aρ 6) (bρ 6) (190862880037 / 400000000000) ≤ -(8538386894358178531511 / 10000000000000000000000)

theorem Zeta5Irrational.U_453_7 : Uω (aρ 7) (bρ 7) (190862880037 / 400000000000) ≤ -(4561199679558233400381 / 5000000000000000000000)

theorem Zeta5Irrational.U_453_8 : Uω (aρ 8) (bρ 8) (190862880037 / 400000000000) ≤ -(995131160783109617529 / 1000000000000000000000)

theorem Zeta5Irrational.U_453_9 : Uω (aρ 9) (bρ 9) (190862880037 / 400000000000) ≤ -(5564252546781204034449 / 5000000000000000000000)

theorem Zeta5Irrational.U_453_10 : Uω (aρ 10) (bρ 10) (190862880037 / 400000000000) ≤ -(12862050208008657540741 / 10000000000000000000000)

theorem Zeta5Irrational.U_453_11 : Uω (aρ 11) (bρ 11) (190862880037 / 400000000000) ≤ -(3959444980566102260757 / 2500000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_453 : Uρ (190862880037 / 400000000000) ≤ -(705937206632403026211 / 625000000000000000000)

theorem Zeta5Irrational.U_454_1 : Uω (aρ 1) (bρ 1) (478481499969 / 1000000000000) ≤ -(3753581121717678975279 / 5000000000000000000000)

theorem Zeta5Irrational.U_454_2 : Uω (aρ 2) (bρ 2) (478481499969 / 1000000000000) ≤ -(184522768432317577 / 244140625000000000)

theorem Zeta5Irrational.U_454_3 : Uω (aρ 3) (bρ 3) (478481499969 / 1000000000000) ≤ -(7660712925159377773271 / 10000000000000000000000)

theorem Zeta5Irrational.U_454_4 : Uω (aρ 4) (bρ 4) (478481499969 / 1000000000000) ≤ -(156677596753044379399 / 200000000000000000000)

theorem Zeta5Irrational.U_454_5 : Uω (aρ 5) (bρ 5) (478481499969 / 1000000000000) ≤ -(810427302632192858973 / 1000000000000000000000)

theorem Zeta5Irrational.U_454_6 : Uω (aρ 6) (bρ 6) (478481499969 / 1000000000000) ≤ -(170144541608308100213 / 200000000000000000000)

theorem Zeta5Irrational.U_454_7 : Uω (aρ 7) (bρ 7) (478481499969 / 1000000000000) ≤ -(1817842896817785574473 / 2000000000000000000000)

theorem Zeta5Irrational.U_454_8 : Uω (aρ 8) (bρ 8) (478481499969 / 1000000000000) ≤ -(9914883532630687762813 / 10000000000000000000000)

theorem Zeta5Irrational.U_454_9 : Uω (aρ 9) (bρ 9) (478481499969 / 1000000000000) ≤ -(11086538371389681350551 / 10000000000000000000000)

theorem Zeta5Irrational.U_454_10 : Uω (aρ 10) (bρ 10) (478481499969 / 1000000000000) ≤ -(1601131982700614138667 / 1250000000000000000000)

theorem Zeta5Irrational.U_454_11 : Uω (aρ 11) (bρ 11) (478481499969 / 1000000000000) ≤ -(15749408998553283782167 / 10000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_454 : Uρ (478481499969 / 1000000000000) ≤ -(11265188586184623207311 / 10000000000000000000000)

theorem Zeta5Irrational.U_455_1 : Uω (aρ 1) (bρ 1) (959611599691 / 2000000000000) ≤ -(1869786451919637710493 / 2500000000000000000000)

theorem Zeta5Irrational.U_455_2 : Uω (aρ 2) (bρ 2) (959611599691 / 2000000000000) ≤ -(3764946137423207459503 / 5000000000000000000000)

theorem Zeta5Irrational.U_455_3 : Uω (aρ 3) (bρ 3) (959611599691 / 2000000000000) ≤ -(3816129473264321412793 / 5000000000000000000000)

theorem Zeta5Irrational.U_455_4 : Uω (aρ 4) (bρ 4) (959611599691 / 2000000000000) ≤ -(7804919958794561528009 / 10000000000000000000000)

theorem Zeta5Irrational.U_455_5 : Uω (aρ 5) (bρ 5) (959611599691 / 2000000000000) ≤ -(4037247798704166091837 / 5000000000000000000000)

theorem Zeta5Irrational.U_455_6 : Uω (aρ 6) (bρ 6) (959611599691 / 2000000000000) ≤ -(4238082354837365660861 / 5000000000000000000000)

theorem Zeta5Irrational.U_455_7 : Uω (aρ 7) (bρ 7) (959611599691 / 2000000000000) ≤ -(9056141129820026511853 / 10000000000000000000000)

theorem Zeta5Irrational.U_455_8 : Uω (aρ 8) (bρ 8) (959611599691 / 2000000000000) ≤ -(617412037109097621673 / 625000000000000000000)

theorem Zeta5Irrational.U_455_9 : Uω (aρ 9) (bρ 9) (959611599691 / 2000000000000) ≤ -(5522381092373664086313 / 5000000000000000000000)

theorem Zeta5Irrational.U_455_10 : Uω (aρ 10) (bρ 10) (959611599691 / 2000000000000) ≤ -(3189100213102396916873 / 2500000000000000000000)

theorem Zeta5Irrational.U_455_11 : Uω (aρ 11) (bρ 11) (959611599691 / 2000000000000) ≤ -(978898607132638238711 / 625000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_455 : Uρ (959611599691 / 2000000000000) ≤ -(351111886832178083997 / 312500000000000000000)

theorem Zeta5Irrational.U_456_1 : Uω (aρ 1) (bρ 1) (240565049861 / 500000000000) ≤ -(7451207645873873946861 / 10000000000000000000000)

theorem Zeta5Irrational.U_456_2 : Uω (aρ 2) (bρ 2) (240565049861 / 500000000000) ≤ -(7501811039978996837427 / 10000000000000000000000)

theorem Zeta5Irrational.U_456_3 : Uω (aρ 3) (bρ 3) (240565049861 / 500000000000) ≤ -(3801942864268135953877 / 5000000000000000000000)

theorem Zeta5Irrational.U_456_4 : Uω (aρ 4) (bρ 4) (240565049861 / 500000000000) ≤ -(3888021894446453529367 / 5000000000000000000000)

theorem Zeta5Irrational.U_456_5 : Uω (aρ 5) (bρ 5) (240565049861 / 500000000000) ≤ -(1608961362230212211269 / 2000000000000000000000)

theorem Zeta5Irrational.U_456_6 : Uω (aρ 6) (bρ 6) (240565049861 / 500000000000) ≤ -(8445199170563307895169 / 10000000000000000000000)

theorem Zeta5Irrational.U_456_7 : Uω (aρ 7) (bρ 7) (240565049861 / 500000000000) ≤ -(9023178537642414456629 / 10000000000000000000000)

theorem Zeta5Irrational.U_456_8 : Uω (aρ 8) (bρ 8) (240565049861 / 500000000000) ≤ -(9842437726581167586699 / 10000000000000000000000)

theorem Zeta5Irrational.U_456_9 : Uω (aρ 9) (bρ 9) (240565049861 / 500000000000) ≤ -(27507936702691674071 / 25000000000000000000)

theorem Zeta5Irrational.U_456_10 : Uω (aρ 10) (bρ 10) (240565049861 / 500000000000) ≤ -(12704080176489435428207 / 10000000000000000000000)

theorem Zeta5Irrational.U_456_11 : Uω (aρ 11) (bρ 11) (240565049861 / 500000000000) ≤ -(15576633237813044959681 / 10000000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_456 : Uρ (240565049861 / 500000000000) ≤ -(5603082807204348035771 / 5000000000000000000000)

theorem Zeta5Irrational.U_457_1 : Uω (aρ 1) (bρ 1) (19351147979 / 40000000000) ≤ -(7395564403113882945229 / 10000000000000000000000)

theorem Zeta5Irrational.U_457_2 : Uω (aρ 2) (bρ 2) (19351147979 / 40000000000) ≤ -(1489176811552806506841 / 2000000000000000000000)

theorem Zeta5Irrational.U_457_3 : Uω (aρ 3) (bρ 3) (19351147979 / 40000000000) ≤ -(60379037993088768907 / 80000000000000000000)

theorem Zeta5Irrational.U_457_4 : Uω (aρ 4) (bρ 4) (19351147979 / 40000000000) ≤ -(482408790506011869709 / 625000000000000000000)

theorem Zeta5Irrational.U_457_5 : Uω (aρ 5) (bρ 5) (19351147979 / 40000000000) ≤ -(798569306100694326047 / 1000000000000000000000)

theorem Zeta5Irrational.U_457_6 : Uω (aρ 6) (bρ 6) (19351147979 / 40000000000) ≤ -(2095889042436629020461 / 2500000000000000000000)

theorem Zeta5Irrational.U_457_7 : Uω (aρ 7) (bρ 7) (19351147979 / 40000000000) ≤ -(4478791321964708754081 / 5000000000000000000000)

theorem Zeta5Irrational.U_457_8 : Uω (aρ 8) (bρ 8) (19351147979 / 40000000000) ≤ -(9770532012500916071231 / 10000000000000000000000)

theorem Zeta5Irrational.U_457_9 : Uω (aρ 9) (bρ 9) (19351147979 / 40000000000) ≤ -(5460279227141323714019 / 5000000000000000000000)

theorem Zeta5Irrational.U_457_10 : Uω (aρ 10) (bρ 10) (19351147979 / 40000000000) ≤ -(1260042240769293479831 / 1000000000000000000000)

theorem Zeta5Irrational.U_457_11 : Uω (aρ 11) (bρ 11) (19351147979 / 40000000000) ≤ -(15408810197614576507277 / 10000000000000000000000)

theorem Zeta5Irrational.U_457_12 : Uω (aρ 12) (bρ 12) (19351147979 / 40000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_457_13 : Uω (aρ 13) (bρ 13) (19351147979 / 40000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_457_14 : Uω (aρ 14) (bρ 14) (19351147979 / 40000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_457_15 : Uω (aρ 15) (bρ 15) (19351147979 / 40000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_457_16 : Uω (aρ 16) (bρ 16) (19351147979 / 40000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_457 : Uρ (19351147979 / 40000000000) ≤ -(278697438641564643689 / 250000000000000000000)

theorem Zeta5Irrational.U_458_1 : Uω (aρ 1) (bρ 1) (121606824807 / 250000000000) ≤ -(1468045813851038955841 / 2000000000000000000000)

theorem Zeta5Irrational.U_458_2 : Uω (aρ 2) (bρ 2) (121606824807 / 250000000000) ≤ -(7390268148614046540739 / 10000000000000000000000)

theorem Zeta5Irrational.U_458_3 : Uω (aρ 3) (bρ 3) (121606824807 / 250000000000) ≤ -(7491191374781335902451 / 10000000000000000000000)

theorem Zeta5Irrational.U_458_4 : Uω (aρ 4) (bρ 4) (121606824807 / 250000000000) ≤ -(7661366600977939292389 / 10000000000000000000000)

theorem Zeta5Irrational.U_458_5 : Uω (aρ 5) (bρ 5) (121606824807 / 250000000000) ≤ -(7926927611440030024571 / 10000000000000000000000)

theorem Zeta5Irrational.U_458_6 : Uω (aρ 6) (bρ 6) (121606824807 / 250000000000) ≤ -(8322293299607536327821 / 10000000000000000000000)

theorem Zeta5Irrational.U_458_7 : Uω (aρ 7) (bρ 7) (121606824807 / 250000000000) ≤ -(4446210444125925813017 / 5000000000000000000000)

theorem Zeta5Irrational.U_458_8 : Uω (aρ 8) (bρ 8) (121606824807 / 250000000000) ≤ -(4849579062306917657777 / 5000000000000000000000)

theorem Zeta5Irrational.U_458_9 : Uω (aρ 9) (bρ 9) (121606824807 / 250000000000) ≤ -(10838675429623092885493 / 10000000000000000000000)

theorem Zeta5Irrational.U_458_10 : Uω (aρ 10) (bρ 10) (121606824807 / 250000000000) ≤ -(2499608972782357176879 / 2000000000000000000000)

theorem Zeta5Irrational.U_458_11 : Uω (aρ 11) (bρ 11) (121606824807 / 250000000000) ≤ -(1905697556669964850993 / 1250000000000000000000)

theorem Zeta5Irrational.U_458_12 : Uω (aρ 12) (bρ 12) (121606824807 / 250000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_458_13 : Uω (aρ 13) (bρ 13) (121606824807 / 250000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_458_14 : Uω (aρ 14) (bρ 14) (121606824807 / 250000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_458_15 : Uω (aρ 15) (bρ 15) (121606824807 / 250000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_458_16 : Uω (aρ 16) (bρ 16) (121606824807 / 250000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_458 : Uρ (121606824807 / 250000000000) ≤ -(2772587281831520040409 / 2500000000000000000000)

theorem Zeta5Irrational.U_459_1 : Uω (aρ 1) (bρ 1) (489075898981 / 1000000000000) ≤ -(455324890955604488009 / 625000000000000000000)

theorem Zeta5Irrational.U_459_2 : Uω (aρ 2) (bρ 2) (489075898981 / 1000000000000) ≤ -(7334959870886187479617 / 10000000000000000000000)

theorem Zeta5Irrational.U_459_3 : Uω (aρ 3) (bρ 3) (489075898981 / 1000000000000) ≤ -(3717658526951898766839 / 5000000000000000000000)

theorem Zeta5Irrational.U_459_4 : Uω (aρ 4) (bρ 4) (489075898981 / 1000000000000) ≤ -(1520903579699353452909 / 2000000000000000000000)

theorem Zeta5Irrational.U_459_5 : Uω (aρ 5) (bρ 5) (489075898981 / 1000000000000) ≤ -(1573701274312190521749 / 2000000000000000000000)

theorem Zeta5Irrational.U_459_6 : Uω (aρ 6) (bρ 6) (489075898981 / 1000000000000) ≤ -(4130702935387415911649 / 5000000000000000000000)

theorem Zeta5Irrational.U_459_7 : Uω (aρ 7) (bρ 7) (489075898981 / 1000000000000) ≤ -(4413843738031198771433 / 5000000000000000000000)

theorem Zeta5Irrational.U_459_8 : Uω (aρ 8) (bρ 8) (489075898981 / 1000000000000) ≤ -(1203538498895373722573 / 1250000000000000000000)

theorem Zeta5Irrational.U_459_9 : Uω (aρ 9) (bρ 9) (489075898981 / 1000000000000) ≤ -(5378755886702058761049 / 5000000000000000000000)

theorem Zeta5Irrational.U_459_10 : Uω (aρ 10) (bρ 10) (489075898981 / 1000000000000) ≤ -(619845579902810326079 / 500000000000000000000)

theorem Zeta5Irrational.U_459_11 : Uω (aρ 11) (bρ 11) (489075898981 / 1000000000000) ≤ -(1885828314317794521397 / 1250000000000000000000)

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

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

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

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

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

theorem Zeta5Irrational.U_459 : Uρ (489075898981 / 1000000000000) ≤ -(5516744325173004896139 / 5000000000000000000000)