Certified arcsine potential bounds (U45)

theorem Zeta5Irrational.U_544_1 : Uω (aρ 1) (bρ 1) (4969968043179 / 8000000000000) ≤ -(243234294615614466823 / 500000000000000000000)

theorem Zeta5Irrational.U_544_2 : Uω (aρ 2) (bρ 2) (4969968043179 / 8000000000000) ≤ -(980732507775771540851 / 2000000000000000000000)

theorem Zeta5Irrational.U_544_3 : Uω (aρ 3) (bρ 3) (4969968043179 / 8000000000000) ≤ -(2491037061290261113757 / 5000000000000000000000)

theorem Zeta5Irrational.U_544_4 : Uω (aρ 4) (bρ 4) (4969968043179 / 8000000000000) ≤ -(5113675763595366645521 / 10000000000000000000000)

theorem Zeta5Irrational.U_544_5 : Uω (aρ 5) (bρ 5) (4969968043179 / 8000000000000) ≤ -(166170619676123348097 / 312500000000000000000)

theorem Zeta5Irrational.U_544_6 : Uω (aρ 6) (bρ 6) (4969968043179 / 8000000000000) ≤ -(2808566494661532032637 / 5000000000000000000000)

theorem Zeta5Irrational.U_544_7 : Uω (aρ 7) (bρ 7) (4969968043179 / 8000000000000) ≤ -(755119197430400781771 / 1250000000000000000000)

theorem Zeta5Irrational.U_544_8 : Uω (aρ 8) (bρ 8) (4969968043179 / 8000000000000) ≤ -(1655595618708660814971 / 2500000000000000000000)

theorem Zeta5Irrational.U_544_9 : Uω (aρ 9) (bρ 9) (4969968043179 / 8000000000000) ≤ -(7402464053785215584387 / 10000000000000000000000)

theorem Zeta5Irrational.U_544_10 : Uω (aρ 10) (bρ 10) (4969968043179 / 8000000000000) ≤ -(4218182011013012442561 / 5000000000000000000000)

theorem Zeta5Irrational.U_544_11 : Uω (aρ 11) (bρ 11) (4969968043179 / 8000000000000) ≤ -(981205691910561245223 / 1000000000000000000000)

theorem Zeta5Irrational.U_544_12 : Uω (aρ 12) (bρ 12) (4969968043179 / 8000000000000) ≤ -(292944600445161657491 / 250000000000000000000)

theorem Zeta5Irrational.U_544_13 : Uω (aρ 13) (bρ 13) (4969968043179 / 8000000000000) ≤ -(1864386724188942654493 / 1250000000000000000000)

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

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

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

theorem Zeta5Irrational.U_544 : Uρ (4969968043179 / 8000000000000) ≤ -(7887909540485613658987 / 10000000000000000000000)

theorem Zeta5Irrational.U_545_1 : Uω (aρ 1) (bρ 1) (39828536950369 / 64000000000000) ≤ -(4847217421798197610027 / 10000000000000000000000)

theorem Zeta5Irrational.U_545_2 : Uω (aρ 2) (bρ 2) (39828536950369 / 64000000000000) ≤ -(2443062744530523726207 / 5000000000000000000000)

theorem Zeta5Irrational.U_545_3 : Uω (aρ 3) (bρ 3) (39828536950369 / 64000000000000) ≤ -(992879575151331134011 / 2000000000000000000000)

theorem Zeta5Irrational.U_545_4 : Uω (aρ 4) (bρ 4) (39828536950369 / 64000000000000) ≤ -(1273940532409412364583 / 2500000000000000000000)

theorem Zeta5Irrational.U_545_5 : Uω (aρ 5) (bρ 5) (39828536950369 / 64000000000000) ≤ -(2649584500781039761267 / 5000000000000000000000)

theorem Zeta5Irrational.U_545_6 : Uω (aρ 6) (bρ 6) (39828536950369 / 64000000000000) ≤ -(559826525414619874691 / 1000000000000000000000)

theorem Zeta5Irrational.U_545_7 : Uω (aρ 7) (bρ 7) (39828536950369 / 64000000000000) ≤ -(240848857808598739739 / 400000000000000000000)

theorem Zeta5Irrational.U_545_8 : Uω (aρ 8) (bρ 8) (39828536950369 / 64000000000000) ≤ -(3300681018533957643367 / 5000000000000000000000)

theorem Zeta5Irrational.U_545_9 : Uω (aρ 9) (bρ 9) (39828536950369 / 64000000000000) ≤ -(1844874861177744237403 / 2500000000000000000000)

theorem Zeta5Irrational.U_545_10 : Uω (aρ 10) (bρ 10) (39828536950369 / 64000000000000) ≤ -(336414102829495814321 / 400000000000000000000)

theorem Zeta5Irrational.U_545_11 : Uω (aρ 11) (bρ 11) (39828536950369 / 64000000000000) ≤ -(1956172290722271357863 / 2000000000000000000000)

theorem Zeta5Irrational.U_545_12 : Uω (aρ 12) (bρ 12) (39828536950369 / 64000000000000) ≤ -(11675955630294015158997 / 10000000000000000000000)

theorem Zeta5Irrational.U_545_13 : Uω (aρ 13) (bρ 13) (39828536950369 / 64000000000000) ≤ -(14831083687162373912247 / 10000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_545 : Uρ (39828536950369 / 64000000000000) ≤ -(245766429868497178311 / 312500000000000000000)

theorem Zeta5Irrational.U_546_1 : Uω (aρ 1) (bρ 1) (19948664777653 / 32000000000000) ≤ -(4829779413085618008589 / 10000000000000000000000)

theorem Zeta5Irrational.U_546_2 : Uω (aρ 2) (bρ 2) (19948664777653 / 32000000000000) ≤ -(2434309570975091985393 / 5000000000000000000000)

theorem Zeta5Irrational.U_546_3 : Uω (aρ 3) (bρ 3) (19948664777653 / 32000000000000) ≤ -(4946752824996576485697 / 10000000000000000000000)

theorem Zeta5Irrational.U_546_4 : Uω (aρ 4) (bρ 4) (19948664777653 / 32000000000000) ≤ -(1269470136695590692193 / 2500000000000000000000)

theorem Zeta5Irrational.U_546_5 : Uω (aρ 5) (bρ 5) (19948664777653 / 32000000000000) ≤ -(1056182323825263913179 / 2000000000000000000000)

theorem Zeta5Irrational.U_546_6 : Uω (aρ 6) (bρ 6) (19948664777653 / 32000000000000) ≤ -(1394858296170015163569 / 2500000000000000000000)

theorem Zeta5Irrational.U_546_7 : Uω (aρ 7) (bρ 7) (19948664777653 / 32000000000000) ≤ -(6001528506852776076673 / 10000000000000000000000)

theorem Zeta5Irrational.U_546_8 : Uω (aρ 8) (bρ 8) (19948664777653 / 32000000000000) ≤ -(1316077306315072704157 / 2000000000000000000000)

theorem Zeta5Irrational.U_546_9 : Uω (aρ 9) (bρ 9) (19948664777653 / 32000000000000) ≤ -(1839147393547709124913 / 2500000000000000000000)

theorem Zeta5Irrational.U_546_10 : Uω (aρ 10) (bρ 10) (19948664777653 / 32000000000000) ≤ -(8384414277493951212261 / 10000000000000000000000)

theorem Zeta5Irrational.U_546_11 : Uω (aρ 11) (bρ 11) (19948664777653 / 32000000000000) ≤ -(9749780267626559126277 / 10000000000000000000000)

theorem Zeta5Irrational.U_546_12 : Uω (aρ 12) (bρ 12) (19948664777653 / 32000000000000) ≤ -(2326874644250277370813 / 2000000000000000000000)

theorem Zeta5Irrational.U_546_13 : Uω (aρ 13) (bρ 13) (19948664777653 / 32000000000000) ≤ -(14748808740681928824749 / 10000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_546 : Uρ (19948664777653 / 32000000000000) ≤ -(7841298324713687178439 / 10000000000000000000000)

theorem Zeta5Irrational.U_547_1 : Uω (aρ 1) (bρ 1) (39966122160243 / 64000000000000) ≤ -(4812371760118998631747 / 10000000000000000000000)

theorem Zeta5Irrational.U_547_2 : Uω (aρ 2) (bρ 2) (39966122160243 / 64000000000000) ≤ -(1212785847555891833407 / 2500000000000000000000)

theorem Zeta5Irrational.U_547_3 : Uω (aρ 3) (bρ 3) (39966122160243 / 64000000000000) ≤ -(2464569430179590840317 / 5000000000000000000000)

theorem Zeta5Irrational.U_547_4 : Uω (aρ 4) (bρ 4) (39966122160243 / 64000000000000) ≤ -(316251931279762199151 / 625000000000000000000)

theorem Zeta5Irrational.U_547_5 : Uω (aρ 5) (bρ 5) (39966122160243 / 64000000000000) ≤ -(5262687560051708840297 / 10000000000000000000000)

theorem Zeta5Irrational.U_547_6 : Uω (aρ 6) (bρ 6) (39966122160243 / 64000000000000) ≤ -(5560636645839827234383 / 10000000000000000000000)

theorem Zeta5Irrational.U_547_7 : Uω (aρ 7) (bρ 7) (39966122160243 / 64000000000000) ≤ -(2990937303811851794713 / 5000000000000000000000)

theorem Zeta5Irrational.U_547_8 : Uω (aρ 8) (bρ 8) (39966122160243 / 64000000000000) ≤ -(3279727881572910084163 / 5000000000000000000000)

theorem Zeta5Irrational.U_547_9 : Uω (aρ 9) (bρ 9) (39966122160243 / 64000000000000) ≤ -(7333734172046849876191 / 10000000000000000000000)

theorem Zeta5Irrational.U_547_10 : Uω (aρ 10) (bρ 10) (39966122160243 / 64000000000000) ≤ -(417927435075955961471 / 500000000000000000000)

theorem Zeta5Irrational.U_547_11 : Uω (aρ 11) (bρ 11) (39966122160243 / 64000000000000) ≤ -(4859406205668740621801 / 5000000000000000000000)

theorem Zeta5Irrational.U_547_12 : Uω (aρ 12) (bρ 12) (39966122160243 / 64000000000000) ≤ -(11593033208050026335313 / 10000000000000000000000)

theorem Zeta5Irrational.U_547_13 : Uω (aρ 13) (bρ 13) (39966122160243 / 64000000000000) ≤ -(183352136630615516529 / 125000000000000000000)

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

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

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

theorem Zeta5Irrational.U_547 : Uρ (39966122160243 / 64000000000000) ≤ -(1954555256450453128983 / 2500000000000000000000)

theorem Zeta5Irrational.U_548_1 : Uω (aρ 1) (bρ 1) (2001745738259 / 3200000000000) ≤ -(2397497178697846703457 / 5000000000000000000000)

theorem Zeta5Irrational.U_548_2 : Uω (aρ 2) (bρ 2) (2001745738259 / 3200000000000) ≤ -(1208424531780068070263 / 2500000000000000000000)

theorem Zeta5Irrational.U_548_3 : Uω (aρ 3) (bρ 3) (2001745738259 / 3200000000000) ≤ -(613944484060455122537 / 1250000000000000000000)

theorem Zeta5Irrational.U_548_4 : Uω (aρ 4) (bρ 4) (2001745738259 / 3200000000000) ≤ -(252110653838961592423 / 500000000000000000000)

theorem Zeta5Irrational.U_548_5 : Uω (aρ 5) (bρ 5) (2001745738259 / 3200000000000) ≤ -(5244496702731643532673 / 10000000000000000000000)

theorem Zeta5Irrational.U_548_6 : Uω (aρ 6) (bρ 6) (2001745738259 / 3200000000000) ≤ -(55418755033094918291 / 100000000000000000000)

theorem Zeta5Irrational.U_548_7 : Uω (aρ 7) (bρ 7) (2001745738259 / 3200000000000) ≤ -(953961534678529139 / 1600000000000000000)

theorem Zeta5Irrational.U_548_8 : Uω (aρ 8) (bρ 8) (2001745738259 / 3200000000000) ≤ -(1634642384464888181893 / 2500000000000000000000)

theorem Zeta5Irrational.U_548_9 : Uω (aρ 9) (bρ 9) (2001745738259 / 3200000000000) ≤ -(3655466485081770504419 / 5000000000000000000000)

theorem Zeta5Irrational.U_548_10 : Uω (aρ 10) (bρ 10) (2001745738259 / 3200000000000) ≤ -(4166377703121249495059 / 5000000000000000000000)

theorem Zeta5Irrational.U_548_11 : Uω (aρ 11) (bρ 11) (2001745738259 / 3200000000000) ≤ -(121099461847467560769 / 125000000000000000000)

theorem Zeta5Irrational.U_548_12 : Uω (aρ 12) (bρ 12) (2001745738259 / 3200000000000) ≤ -(5775966047425651859671 / 5000000000000000000000)

theorem Zeta5Irrational.U_548_13 : Uω (aρ 13) (bρ 13) (2001745738259 / 3200000000000) ≤ -(3647270300163015730903 / 2500000000000000000000)

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

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

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

theorem Zeta5Irrational.U_548 : Uρ (2001745738259 / 3200000000000) ≤ -(7795288173310978959933 / 10000000000000000000000)

theorem Zeta5Irrational.U_549_1 : Uω (aρ 1) (bρ 1) (40103707370117 / 64000000000000) ≤ -(1194411774990531570599 / 2500000000000000000000)

theorem Zeta5Irrational.U_549_2 : Uω (aρ 2) (bρ 2) (40103707370117 / 64000000000000) ≤ -(4816283246437239450033 / 10000000000000000000000)

theorem Zeta5Irrational.U_549_3 : Uω (aρ 3) (bρ 3) (40103707370117 / 64000000000000) ≤ -(195760150103412896917 / 400000000000000000000)

theorem Zeta5Irrational.U_549_4 : Uω (aρ 4) (bρ 4) (40103707370117 / 64000000000000) ≤ -(1256106740590143561431 / 2500000000000000000000)

theorem Zeta5Irrational.U_549_5 : Uω (aρ 5) (bρ 5) (40103707370117 / 64000000000000) ≤ -(653292365778121990287 / 1250000000000000000000)

theorem Zeta5Irrational.U_549_6 : Uω (aρ 6) (bρ 6) (40103707370117 / 64000000000000) ≤ -(690393702942002721149 / 1250000000000000000000)

theorem Zeta5Irrational.U_549_7 : Uω (aρ 7) (bρ 7) (40103707370117 / 64000000000000) ≤ -(185708853261108282267 / 312500000000000000000)

theorem Zeta5Irrational.U_549_8 : Uω (aρ 8) (bρ 8) (40103707370117 / 64000000000000) ≤ -(6517727663076715180429 / 10000000000000000000000)

theorem Zeta5Irrational.U_549_9 : Uω (aρ 9) (bρ 9) (40103707370117 / 64000000000000) ≤ -(7288185702466368188041 / 10000000000000000000000)

theorem Zeta5Irrational.U_549_10 : Uω (aρ 10) (bρ 10) (40103707370117 / 64000000000000) ≤ -(8307033959244178314683 / 10000000000000000000000)

theorem Zeta5Irrational.U_549_11 : Uω (aρ 11) (bρ 11) (40103707370117 / 64000000000000) ≤ -(603575809542648455083 / 625000000000000000000)

theorem Zeta5Irrational.U_549_12 : Uω (aρ 12) (bρ 12) (40103707370117 / 64000000000000) ≤ -(5755533234833897135403 / 5000000000000000000000)

theorem Zeta5Irrational.U_549_13 : Uω (aρ 13) (bρ 13) (40103707370117 / 64000000000000) ≤ -(14511458352928684789089 / 10000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_549 : Uρ (40103707370117 / 64000000000000) ≤ -(7772494551631630816607 / 10000000000000000000000)

theorem Zeta5Irrational.U_550_1 : Uω (aρ 1) (bρ 1) (20086249987527 / 32000000000000) ≤ -(4760329883409985412941 / 10000000000000000000000)

theorem Zeta5Irrational.U_550_2 : Uω (aρ 2) (bρ 2) (20086249987527 / 32000000000000) ≤ -(959779728505078014553 / 2000000000000000000000)

theorem Zeta5Irrational.U_550_3 : Uω (aρ 3) (bρ 3) (20086249987527 / 32000000000000) ≤ -(2438241196225873571523 / 5000000000000000000000)

theorem Zeta5Irrational.U_550_4 : Uω (aρ 4) (bρ 4) (20086249987527 / 32000000000000) ≤ -(19557314236304715771 / 39062500000000000000)

theorem Zeta5Irrational.U_550_5 : Uω (aρ 5) (bρ 5) (20086249987527 / 32000000000000) ≤ -(520821411025116205967 / 1000000000000000000000)

theorem Zeta5Irrational.U_550_6 : Uω (aρ 6) (bρ 6) (20086249987527 / 32000000000000) ≤ -(5504458873723566257013 / 10000000000000000000000)

theorem Zeta5Irrational.U_550_7 : Uω (aρ 7) (bρ 7) (20086249987527 / 32000000000000) ≤ -(1184629118309960228537 / 2000000000000000000000)

theorem Zeta5Irrational.U_550_8 : Uω (aρ 8) (bρ 8) (20086249987527 / 32000000000000) ≤ -(6496929947425930102249 / 10000000000000000000000)

theorem Zeta5Irrational.U_550_9 : Uω (aρ 9) (bρ 9) (20086249987527 / 32000000000000) ≤ -(3632746052450233074369 / 5000000000000000000000)

theorem Zeta5Irrational.U_550_10 : Uω (aρ 10) (bρ 10) (20086249987527 / 32000000000000) ≤ -(8281383932199983076381 / 10000000000000000000000)

theorem Zeta5Irrational.U_550_11 : Uω (aρ 11) (bρ 11) (20086249987527 / 32000000000000) ≤ -(9626579514052903566141 / 10000000000000000000000)

theorem Zeta5Irrational.U_550_12 : Uω (aρ 12) (bρ 12) (20086249987527 / 32000000000000) ≤ -(11470433001551724661083 / 10000000000000000000000)

theorem Zeta5Irrational.U_550_13 : Uω (aρ 13) (bρ 13) (20086249987527 / 32000000000000) ≤ -(7217614053428216597823 / 5000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_550 : Uρ (20086249987527 / 32000000000000) ≤ -(7749835359783882693713 / 10000000000000000000000)

theorem Zeta5Irrational.U_551_1 : Uω (aρ 1) (bρ 1) (40241292579991 / 64000000000000) ≤ -(4743042603872454263259 / 10000000000000000000000)

theorem Zeta5Irrational.U_551_2 : Uω (aρ 2) (bρ 2) (40241292579991 / 64000000000000) ≤ -(2390772105142890830111 / 5000000000000000000000)

theorem Zeta5Irrational.U_551_3 : Uω (aρ 3) (bρ 3) (40241292579991 / 64000000000000) ≤ -(2429495842219293840209 / 5000000000000000000000)

theorem Zeta5Irrational.U_551_4 : Uω (aρ 4) (bρ 4) (40241292579991 / 64000000000000) ≤ -(2494474705526851839749 / 5000000000000000000000)

theorem Zeta5Irrational.U_551_5 : Uω (aρ 5) (bρ 5) (40241292579991 / 64000000000000) ≤ -(259506106759272505429 / 500000000000000000000)

theorem Zeta5Irrational.U_551_6 : Uω (aρ 6) (bρ 6) (40241292579991 / 64000000000000) ≤ -(5485803121827726466689 / 10000000000000000000000)

theorem Zeta5Irrational.U_551_7 : Uω (aρ 7) (bρ 7) (40241292579991 / 64000000000000) ≤ -(5903646300329178437817 / 10000000000000000000000)

theorem Zeta5Irrational.U_551_8 : Uω (aρ 8) (bρ 8) (40241292579991 / 64000000000000) ≤ -(6476176200793001902877 / 10000000000000000000000)

theorem Zeta5Irrational.U_551_9 : Uω (aρ 9) (bρ 9) (40241292579991 / 64000000000000) ≤ -(905356489426210870313 / 1250000000000000000000)

theorem Zeta5Irrational.U_551_10 : Uω (aρ 10) (bρ 10) (40241292579991 / 64000000000000) ≤ -(412790245041383228599 / 500000000000000000000)

theorem Zeta5Irrational.U_551_11 : Uω (aρ 11) (bρ 11) (40241292579991 / 64000000000000) ≤ -(2399013933030365643021 / 2500000000000000000000)

theorem Zeta5Irrational.U_551_12 : Uω (aρ 12) (bρ 12) (40241292579991 / 64000000000000) ≤ -(11430028437903927354641 / 10000000000000000000000)

theorem Zeta5Irrational.U_551_13 : Uω (aρ 13) (bρ 13) (40241292579991 / 64000000000000) ≤ -(1436032230020782576113 / 1000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_551 : Uρ (40241292579991 / 64000000000000) ≤ -(7727306164144297624663 / 10000000000000000000000)

theorem Zeta5Irrational.U_552_1 : Uω (aρ 1) (bρ 1) (1259690162029 / 2000000000000) ≤ -(4725785158020472823779 / 10000000000000000000000)

theorem Zeta5Irrational.U_552_2 : Uω (aρ 2) (bρ 2) (1259690162029 / 2000000000000) ≤ -(4764219845165794570447 / 10000000000000000000000)

theorem Zeta5Irrational.U_552_3 : Uω (aρ 3) (bρ 3) (1259690162029 / 2000000000000) ≤ -(2420765760732845746699 / 5000000000000000000000)

theorem Zeta5Irrational.U_552_4 : Uω (aρ 4) (bρ 4) (1259690162029 / 2000000000000) ≤ -(1242814437627491156317 / 2500000000000000000000)

theorem Zeta5Irrational.U_552_5 : Uω (aρ 5) (bρ 5) (1259690162029 / 2000000000000) ≤ -(5172062882054117301997 / 10000000000000000000000)

theorem Zeta5Irrational.U_552_6 : Uω (aρ 6) (bρ 6) (1259690162029 / 2000000000000) ≤ -(136679555913746854773 / 250000000000000000000)

theorem Zeta5Irrational.U_552_7 : Uω (aρ 7) (bρ 7) (1259690162029 / 2000000000000) ≤ -(5884185278614776937653 / 10000000000000000000000)

theorem Zeta5Irrational.U_552_8 : Uω (aρ 8) (bρ 8) (1259690162029 / 2000000000000) ≤ -(5164372987447805311 / 8000000000000000000)

theorem Zeta5Irrational.U_552_9 : Uω (aρ 9) (bρ 9) (1259690162029 / 2000000000000) ≤ -(3610132436957952754391 / 5000000000000000000000)

theorem Zeta5Irrational.U_552_10 : Uω (aρ 10) (bρ 10) (1259690162029 / 2000000000000) ≤ -(8230296444833993408677 / 10000000000000000000000)

theorem Zeta5Irrational.U_552_11 : Uω (aρ 11) (bρ 11) (1259690162029 / 2000000000000) ≤ -(2391410179756399555909 / 2500000000000000000000)

theorem Zeta5Irrational.U_552_12 : Uω (aρ 12) (bρ 12) (1259690162029 / 2000000000000) ≤ -(11389849601897008077703 / 10000000000000000000000)

theorem Zeta5Irrational.U_552_13 : Uω (aρ 13) (bρ 13) (1259690162029 / 2000000000000) ≤ -(1428667820436467843137 / 1000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_552 : Uρ (1259690162029 / 2000000000000) ≤ -(61639222863656401809 / 80000000000000000000)

theorem Zeta5Irrational.U_553_1 : Uω (aρ 1) (bρ 1) (8075775557973 / 12800000000000) ≤ -(294284840191189489643 / 625000000000000000000)

theorem Zeta5Irrational.U_553_2 : Uω (aρ 2) (bρ 2) (8075775557973 / 12800000000000) ≤ -(593365680394418844097 / 1250000000000000000000)

theorem Zeta5Irrational.U_553_3 : Uω (aρ 3) (bρ 3) (8075775557973 / 12800000000000) ≤ -(4824101797013151299569 / 10000000000000000000000)

theorem Zeta5Irrational.U_553_4 : Uω (aρ 4) (bρ 4) (8075775557973 / 12800000000000) ≤ -(990719470384999601177 / 2000000000000000000000)

theorem Zeta5Irrational.U_553_5 : Uω (aρ 5) (bρ 5) (8075775557973 / 12800000000000) ≤ -(16106363226655447673 / 31250000000000000000)

theorem Zeta5Irrational.U_553_6 : Uω (aρ 6) (bρ 6) (8075775557973 / 12800000000000) ≤ -(2724298043665763560073 / 5000000000000000000000)

theorem Zeta5Irrational.U_553_7 : Uω (aρ 7) (bρ 7) (8075775557973 / 12800000000000) ≤ -(183273824226132342093 / 312500000000000000000)

theorem Zeta5Irrational.U_553_8 : Uω (aρ 8) (bρ 8) (8075775557973 / 12800000000000) ≤ -(3217399930171501478579 / 5000000000000000000000)

theorem Zeta5Irrational.U_553_9 : Uω (aρ 9) (bρ 9) (8075775557973 / 12800000000000) ≤ -(143954614445972021909 / 200000000000000000000)

theorem Zeta5Irrational.U_553_10 : Uω (aρ 10) (bρ 10) (8075775557973 / 12800000000000) ≤ -(4102429073931367588247 / 5000000000000000000000)

theorem Zeta5Irrational.U_553_11 : Uω (aρ 11) (bρ 11) (8075775557973 / 12800000000000) ≤ -(9535333598606493714421 / 10000000000000000000000)

theorem Zeta5Irrational.U_553_12 : Uω (aρ 12) (bρ 12) (8075775557973 / 12800000000000) ≤ -(11349893390006880405851 / 10000000000000000000000)

theorem Zeta5Irrational.U_553_13 : Uω (aρ 13) (bρ 13) (8075775557973 / 12800000000000) ≤ -(7107118967621958687121 / 5000000000000000000000)

theorem Zeta5Irrational.U_553_14 : Uω (aρ 14) (bρ 14) (8075775557973 / 12800000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_553_15 : Uω (aρ 15) (bρ 15) (8075775557973 / 12800000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_553_16 : Uω (aρ 16) (bρ 16) (8075775557973 / 12800000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_553 : Uρ (8075775557973 / 12800000000000) ≤ -(3841310813236541712291 / 5000000000000000000000)

theorem Zeta5Irrational.U_554_1 : Uω (aρ 1) (bρ 1) (20223835197401 / 32000000000000) ≤ -(293209959795218729589 / 625000000000000000000)

theorem Zeta5Irrational.U_554_2 : Uω (aρ 2) (bρ 2) (20223835197401 / 32000000000000) ≤ -(4729660900783168347879 / 10000000000000000000000)

theorem Zeta5Irrational.U_554_3 : Uω (aρ 3) (bρ 3) (20223835197401 / 32000000000000) ≤ -(2403351202558697929501 / 5000000000000000000000)

theorem Zeta5Irrational.U_554_4 : Uω (aρ 4) (bρ 4) (20223835197401 / 32000000000000) ≤ -(123399202623718425537 / 250000000000000000000)

theorem Zeta5Irrational.U_554_5 : Uω (aρ 5) (bρ 5) (20223835197401 / 32000000000000) ≤ -(1284010517231633783179 / 2500000000000000000000)

theorem Zeta5Irrational.U_554_6 : Uω (aρ 6) (bρ 6) (20223835197401 / 32000000000000) ≤ -(1357511136087193952523 / 2500000000000000000000)

theorem Zeta5Irrational.U_554_7 : Uω (aρ 7) (bρ 7) (20223835197401 / 32000000000000) ≤ -(5845377439924378908381 / 10000000000000000000000)

theorem Zeta5Irrational.U_554_8 : Uω (aρ 8) (bρ 8) (20223835197401 / 32000000000000) ≤ -(3207088446241811533109 / 5000000000000000000000)

theorem Zeta5Irrational.U_554_9 : Uω (aρ 9) (bρ 9) (20223835197401 / 32000000000000) ≤ -(1793812301093678316561 / 2500000000000000000000)

theorem Zeta5Irrational.U_554_10 : Uω (aρ 10) (bρ 10) (20223835197401 / 32000000000000) ≤ -(4089744798721756566173 / 5000000000000000000000)

theorem Zeta5Irrational.U_554_11 : Uω (aρ 11) (bρ 11) (20223835197401 / 32000000000000) ≤ -(190102670123856259617 / 200000000000000000000)

theorem Zeta5Irrational.U_554_12 : Uω (aρ 12) (bρ 12) (20223835197401 / 32000000000000) ≤ -(113101567696471236689 / 100000000000000000000)

theorem Zeta5Irrational.U_554_13 : Uω (aρ 13) (bρ 13) (20223835197401 / 32000000000000) ≤ -(7071473971965871018263 / 5000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_554 : Uρ (20223835197401 / 32000000000000) ≤ -(7660458916787004784987 / 10000000000000000000000)

theorem Zeta5Irrational.U_555_1 : Uω (aρ 1) (bρ 1) (40516462999739 / 64000000000000) ≤ -(1168547699318994396631 / 2500000000000000000000)

theorem Zeta5Irrational.U_555_2 : Uω (aρ 2) (bρ 2) (40516462999739 / 64000000000000) ≤ -(1178106528778261540091 / 2500000000000000000000)

theorem Zeta5Irrational.U_555_3 : Uω (aρ 3) (bρ 3) (40516462999739 / 64000000000000) ≤ -(4789333240367326840447 / 10000000000000000000000)

theorem Zeta5Irrational.U_555_4 : Uω (aρ 4) (bρ 4) (40516462999739 / 64000000000000) ≤ -(2459184949907346047189 / 5000000000000000000000)

theorem Zeta5Irrational.U_555_5 : Uω (aρ 5) (bρ 5) (40516462999739 / 64000000000000) ≤ -(5118080274195688240163 / 10000000000000000000000)

theorem Zeta5Irrational.U_555_6 : Uω (aρ 6) (bρ 6) (40516462999739 / 64000000000000) ≤ -(1352881869626692158181 / 2500000000000000000000)

theorem Zeta5Irrational.U_555_7 : Uω (aρ 7) (bρ 7) (40516462999739 / 64000000000000) ≤ -(1165206064660802796103 / 2000000000000000000000)

theorem Zeta5Irrational.U_555_8 : Uω (aρ 8) (bρ 8) (40516462999739 / 64000000000000) ≤ -(6393597145535780670923 / 10000000000000000000000)

theorem Zeta5Irrational.U_555_9 : Uω (aρ 9) (bρ 9) (40516462999739 / 64000000000000) ≤ -(7152820065878755550463 / 10000000000000000000000)

theorem Zeta5Irrational.U_555_10 : Uω (aρ 10) (bρ 10) (40516462999739 / 64000000000000) ≤ -(1630838076988301541033 / 2000000000000000000000)

theorem Zeta5Irrational.U_555_11 : Uω (aρ 11) (bρ 11) (40516462999739 / 64000000000000) ≤ -(2368759897097424207653 / 2500000000000000000000)

theorem Zeta5Irrational.U_555_12 : Uω (aρ 12) (bρ 12) (40516462999739 / 64000000000000) ≤ -(5635318388450483959479 / 5000000000000000000000)

theorem Zeta5Irrational.U_555_13 : Uω (aρ 13) (bρ 13) (40516462999739 / 64000000000000) ≤ -(7036379287111782039099 / 5000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_555 : Uρ (40516462999739 / 64000000000000) ≤ -(3819205705809023544411 / 5000000000000000000000)