Certified arcsine potential bounds (U25)

theorem Zeta5Irrational.U_304_1 : Uω (aρ 1) (bρ 1) (36419876534909 / 128000000000000) ≤ -(319966329192450738377 / 250000000000000000000)

theorem Zeta5Irrational.U_304_2 : Uω (aρ 2) (bρ 2) (36419876534909 / 128000000000000) ≤ -(12885682785381020929319 / 10000000000000000000000)

theorem Zeta5Irrational.U_304_3 : Uω (aρ 3) (bρ 3) (36419876534909 / 128000000000000) ≤ -(13062733067052531422153 / 10000000000000000000000)

theorem Zeta5Irrational.U_304_4 : Uω (aρ 4) (bρ 4) (36419876534909 / 128000000000000) ≤ -(2673224740282882651271 / 2000000000000000000000)

theorem Zeta5Irrational.U_304_5 : Uω (aρ 5) (bρ 5) (36419876534909 / 128000000000000) ≤ -(13852885671077141140659 / 10000000000000000000000)

theorem Zeta5Irrational.U_304_6 : Uω (aρ 6) (bρ 6) (36419876534909 / 128000000000000) ≤ -(14612502027911626169787 / 10000000000000000000000)

theorem Zeta5Irrational.U_304_7 : Uω (aρ 7) (bρ 7) (36419876534909 / 128000000000000) ≤ -(7901134692862773503333 / 5000000000000000000000)

theorem Zeta5Irrational.U_304_8 : Uω (aρ 8) (bρ 8) (36419876534909 / 128000000000000) ≤ -(4445519034434660549931 / 2500000000000000000000)

theorem Zeta5Irrational.U_304_9 : Uω (aρ 9) (bρ 9) (36419876534909 / 128000000000000) ≤ -(4456019168123497172333 / 2000000000000000000000)

theorem Zeta5Irrational.U_304_10 : Uω (aρ 10) (bρ 10) (36419876534909 / 128000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_304_11 : Uω (aρ 11) (bρ 11) (36419876534909 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_304_12 : Uω (aρ 12) (bρ 12) (36419876534909 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_304 : Uρ (36419876534909 / 128000000000000) ≤ -(3334862897898375222561 / 2000000000000000000000)

theorem Zeta5Irrational.U_305_1 : Uω (aρ 1) (bρ 1) (18248810046081 / 64000000000000) ≤ -(12776834507854284359341 / 10000000000000000000000)

theorem Zeta5Irrational.U_305_2 : Uω (aρ 2) (bρ 2) (18248810046081 / 64000000000000) ≤ -(200994859613764106703 / 156250000000000000000)

theorem Zeta5Irrational.U_305_3 : Uω (aρ 3) (bρ 3) (18248810046081 / 64000000000000) ≤ -(13040320400032887200957 / 10000000000000000000000)

theorem Zeta5Irrational.U_305_4 : Uω (aρ 4) (bρ 4) (18248810046081 / 64000000000000) ≤ -(13342997919963146336917 / 10000000000000000000000)

theorem Zeta5Irrational.U_305_5 : Uω (aρ 5) (bρ 5) (18248810046081 / 64000000000000) ≤ -(3457135375880206226739 / 2500000000000000000000)

theorem Zeta5Irrational.U_305_6 : Uω (aρ 6) (bρ 6) (18248810046081 / 64000000000000) ≤ -(7293024924857735976821 / 5000000000000000000000)

theorem Zeta5Irrational.U_305_7 : Uω (aρ 7) (bρ 7) (18248810046081 / 64000000000000) ≤ -(31543787609354435141 / 20000000000000000000)

theorem Zeta5Irrational.U_305_8 : Uω (aρ 8) (bρ 8) (18248810046081 / 64000000000000) ≤ -(17742731513520089426687 / 10000000000000000000000)

theorem Zeta5Irrational.U_305_9 : Uω (aρ 9) (bρ 9) (18248810046081 / 64000000000000) ≤ -(2218861948983381281 / 1000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_305 : Uρ (18248810046081 / 64000000000000) ≤ -(8326613935861223524661 / 5000000000000000000000)

theorem Zeta5Irrational.U_306_1 : Uω (aρ 1) (bρ 1) (7315072729883 / 25600000000000) ≤ -(6377531675875982707461 / 5000000000000000000000)

theorem Zeta5Irrational.U_306_2 : Uω (aρ 2) (bρ 2) (7315072729883 / 25600000000000) ≤ -(802606725249877005899 / 625000000000000000000)

theorem Zeta5Irrational.U_306_3 : Uω (aρ 3) (bρ 3) (7315072729883 / 25600000000000) ≤ -(2603591580741016814553 / 2000000000000000000000)

theorem Zeta5Irrational.U_306_4 : Uω (aρ 4) (bρ 4) (7315072729883 / 25600000000000) ≤ -(13319925657080517909239 / 10000000000000000000000)

theorem Zeta5Irrational.U_306_5 : Uω (aρ 5) (bρ 5) (7315072729883 / 25600000000000) ≤ -(13804256957131762695407 / 10000000000000000000000)

theorem Zeta5Irrational.U_306_6 : Uω (aρ 6) (bρ 6) (7315072729883 / 25600000000000) ≤ -(14559669056125745715263 / 10000000000000000000000)

theorem Zeta5Irrational.U_306_7 : Uω (aρ 7) (bρ 7) (7315072729883 / 25600000000000) ≤ -(3148323192084140152897 / 2000000000000000000000)

theorem Zeta5Irrational.U_306_8 : Uω (aρ 8) (bρ 8) (7315072729883 / 25600000000000) ≤ -(3540714116985614482459 / 2000000000000000000000)

theorem Zeta5Irrational.U_306_9 : Uω (aρ 9) (bρ 9) (7315072729883 / 25600000000000) ≤ -(2209898160607914061911 / 1000000000000000000000)

theorem Zeta5Irrational.U_306_10 : Uω (aρ 10) (bρ 10) (7315072729883 / 25600000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_306_11 : Uω (aρ 11) (bρ 11) (7315072729883 / 25600000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_306_12 : Uω (aρ 12) (bρ 12) (7315072729883 / 25600000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_306_13 : Uω (aρ 13) (bρ 13) (7315072729883 / 25600000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_306_14 : Uω (aρ 14) (bρ 14) (7315072729883 / 25600000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_306_15 : Uω (aρ 15) (bρ 15) (7315072729883 / 25600000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_306_16 : Uω (aρ 16) (bρ 16) (7315072729883 / 25600000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_306 : Uρ (7315072729883 / 25600000000000) ≤ -(8316172534289768010333 / 5000000000000000000000)

theorem Zeta5Irrational.U_307_1 : Uω (aρ 1) (bρ 1) (9163276801667 / 32000000000000) ≤ -(3183334873245216212523 / 2500000000000000000000)

theorem Zeta5Irrational.U_307_2 : Uω (aρ 2) (bρ 2) (9163276801667 / 32000000000000) ≤ -(12819792339455511980223 / 10000000000000000000000)

theorem Zeta5Irrational.U_307_3 : Uω (aρ 3) (bρ 3) (9163276801667 / 32000000000000) ≤ -(3248911338433372805021 / 2500000000000000000000)

theorem Zeta5Irrational.U_307_4 : Uω (aρ 4) (bρ 4) (9163276801667 / 32000000000000) ≤ -(6648453332443258315593 / 5000000000000000000000)

theorem Zeta5Irrational.U_307_5 : Uω (aρ 5) (bρ 5) (9163276801667 / 32000000000000) ≤ -(13780031738160772080827 / 10000000000000000000000)

theorem Zeta5Irrational.U_307_6 : Uω (aρ 6) (bρ 6) (9163276801667 / 32000000000000) ≤ -(14533359254442350572721 / 10000000000000000000000)

theorem Zeta5Irrational.U_307_7 : Uω (aρ 7) (bρ 7) (9163276801667 / 32000000000000) ≤ -(628457407618548892479 / 400000000000000000000)

theorem Zeta5Irrational.U_307_8 : Uω (aρ 8) (bρ 8) (9163276801667 / 32000000000000) ≤ -(17664591395044278791573 / 10000000000000000000000)

theorem Zeta5Irrational.U_307_9 : Uω (aρ 9) (bρ 9) (9163276801667 / 32000000000000) ≤ -(1375692650065395914491 / 625000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_307 : Uρ (9163276801667 / 32000000000000) ≤ -(8305828477742148551567 / 5000000000000000000000)

theorem Zeta5Irrational.U_308_1 : Uω (aρ 1) (bρ 1) (36730850763921 / 128000000000000) ≤ -(1588957840809154527443 / 1250000000000000000000)

theorem Zeta5Irrational.U_308_2 : Uω (aρ 2) (bρ 2) (36730850763921 / 128000000000000) ≤ -(2559585002193774210817 / 2000000000000000000000)

theorem Zeta5Irrational.U_308_3 : Uω (aρ 3) (bρ 3) (36730850763921 / 128000000000000) ≤ -(12973382527285262823649 / 10000000000000000000000)

theorem Zeta5Irrational.U_308_4 : Uω (aρ 4) (bρ 4) (36730850763921 / 128000000000000) ≤ -(6636970348612193216359 / 5000000000000000000000)

theorem Zeta5Irrational.U_308_5 : Uω (aρ 5) (bρ 5) (36730850763921 / 128000000000000) ≤ -(13755865555041763943411 / 10000000000000000000000)

theorem Zeta5Irrational.U_308_6 : Uω (aρ 6) (bρ 6) (36730850763921 / 128000000000000) ≤ -(7253560027631494245037 / 5000000000000000000000)

theorem Zeta5Irrational.U_308_7 : Uω (aρ 7) (bρ 7) (36730850763921 / 128000000000000) ≤ -(7840675419673181174101 / 5000000000000000000000)

theorem Zeta5Irrational.U_308_8 : Uω (aρ 8) (bρ 8) (36730850763921 / 128000000000000) ≤ -(8812896010485875851931 / 5000000000000000000000)

theorem Zeta5Irrational.U_308_9 : Uω (aρ 9) (bρ 9) (36730850763921 / 128000000000000) ≤ -(2740603860275247694661 / 1250000000000000000000)

theorem Zeta5Irrational.U_308_10 : Uω (aρ 10) (bρ 10) (36730850763921 / 128000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_308_11 : Uω (aρ 11) (bρ 11) (36730850763921 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_308_12 : Uω (aρ 12) (bρ 12) (36730850763921 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_308 : Uρ (36730850763921 / 128000000000000) ≤ -(16591155188789344255453 / 10000000000000000000000)

theorem Zeta5Irrational.U_309_1 : Uω (aρ 1) (bρ 1) (18404297160587 / 64000000000000) ≤ -(396563526515380477321 / 312500000000000000000)

theorem Zeta5Irrational.U_309_2 : Uω (aρ 2) (bρ 2) (18404297160587 / 64000000000000) ≤ -(12776105409233890902293 / 10000000000000000000000)

theorem Zeta5Irrational.U_309_3 : Uω (aρ 3) (bρ 3) (18404297160587 / 64000000000000) ≤ -(12951169203016937992483 / 10000000000000000000000)

theorem Zeta5Irrational.U_309_4 : Uω (aρ 4) (bρ 4) (18404297160587 / 64000000000000) ≤ -(13251027509644650616501 / 10000000000000000000000)

theorem Zeta5Irrational.U_309_5 : Uω (aρ 5) (bρ 5) (18404297160587 / 64000000000000) ≤ -(13731758118370003654299 / 10000000000000000000000)

theorem Zeta5Irrational.U_309_6 : Uω (aρ 6) (bρ 6) (18404297160587 / 64000000000000) ≤ -(905059442027853315307 / 625000000000000000000)

theorem Zeta5Irrational.U_309_7 : Uω (aρ 7) (bρ 7) (18404297160587 / 64000000000000) ≤ -(2445525352896588967 / 1562500000000000000)

theorem Zeta5Irrational.U_309_8 : Uω (aρ 8) (bρ 8) (18404297160587 / 64000000000000) ≤ -(8793585286503424790819 / 5000000000000000000000)

theorem Zeta5Irrational.U_309_9 : Uω (aρ 9) (bρ 9) (18404297160587 / 64000000000000) ≤ -(873605752059970258149 / 400000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_309 : Uρ (18404297160587 / 64000000000000) ≤ -(16570832112858170651139 / 10000000000000000000000)

theorem Zeta5Irrational.U_310_1 : Uω (aρ 1) (bρ 1) (36886337878427 / 128000000000000) ≤ -(791778103538758106661 / 625000000000000000000)

theorem Zeta5Irrational.U_310_2 : Uω (aρ 2) (bρ 2) (36886337878427 / 128000000000000) ≤ -(797145832894660626739 / 625000000000000000000)

theorem Zeta5Irrational.U_310_3 : Uω (aρ 3) (bρ 3) (36886337878427 / 128000000000000) ≤ -(12929005161061176723777 / 10000000000000000000000)

theorem Zeta5Irrational.U_310_4 : Uω (aρ 4) (bρ 4) (36886337878427 / 128000000000000) ≤ -(1322816685938930461697 / 1000000000000000000000)

theorem Zeta5Irrational.U_310_5 : Uω (aρ 5) (bρ 5) (36886337878427 / 128000000000000) ≤ -(13707709140880624061209 / 10000000000000000000000)

theorem Zeta5Irrational.U_310_6 : Uω (aρ 6) (bρ 6) (36886337878427 / 128000000000000) ≤ -(289097038461433344131 / 200000000000000000000)

theorem Zeta5Irrational.U_310_7 : Uω (aρ 7) (bρ 7) (36886337878427 / 128000000000000) ≤ -(3124293761267432852327 / 2000000000000000000000)

theorem Zeta5Irrational.U_310_8 : Uω (aρ 8) (bρ 8) (36886337878427 / 128000000000000) ≤ -(877436259691853950059 / 500000000000000000000)

theorem Zeta5Irrational.U_310_9 : Uω (aρ 9) (bρ 9) (36886337878427 / 128000000000000) ≤ -(1087847238022731517901 / 500000000000000000000)

theorem Zeta5Irrational.U_310_10 : Uω (aρ 10) (bρ 10) (36886337878427 / 128000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_310_11 : Uω (aρ 11) (bρ 11) (36886337878427 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_310_12 : Uω (aρ 12) (bρ 12) (36886337878427 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_310 : Uρ (36886337878427 / 128000000000000) ≤ -(4137670170238638207857 / 2500000000000000000000)

theorem Zeta5Irrational.U_311_1 : Uω (aρ 1) (bρ 1) (231025508973 / 800000000000) ≤ -(632345647487376720253 / 500000000000000000000)

theorem Zeta5Irrational.U_311_2 : Uω (aρ 2) (bρ 2) (231025508973 / 800000000000) ≤ -(6366304277815616426409 / 5000000000000000000000)

theorem Zeta5Irrational.U_311_3 : Uω (aρ 3) (bρ 3) (231025508973 / 800000000000) ≤ -(12906890183013655558881 / 10000000000000000000000)

theorem Zeta5Irrational.U_311_4 : Uω (aρ 4) (bρ 4) (231025508973 / 800000000000) ≤ -(3301339626344053614233 / 2500000000000000000000)

theorem Zeta5Irrational.U_311_5 : Uω (aρ 5) (bρ 5) (231025508973 / 800000000000) ≤ -(3420929584356858442139 / 2500000000000000000000)

theorem Zeta5Irrational.U_311_6 : Uω (aρ 6) (bρ 6) (231025508973 / 800000000000) ≤ -(14428822227409249675339 / 10000000000000000000000)

theorem Zeta5Irrational.U_311_7 : Uω (aρ 7) (bρ 7) (231025508973 / 800000000000) ≤ -(15591669847770762946373 / 10000000000000000000000)

theorem Zeta5Irrational.U_311_8 : Uω (aρ 8) (bρ 8) (231025508973 / 800000000000) ≤ -(8755227028881924606817 / 5000000000000000000000)

theorem Zeta5Irrational.U_311_9 : Uω (aρ 9) (bρ 9) (231025508973 / 800000000000) ≤ -(1083758172203001746681 / 500000000000000000000)

theorem Zeta5Irrational.U_311_10 : Uω (aρ 10) (bρ 10) (231025508973 / 800000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_311_11 : Uω (aρ 11) (bρ 11) (231025508973 / 800000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_311_12 : Uω (aρ 12) (bρ 12) (231025508973 / 800000000000) ≤ -(640305991230515290559 / 312500000000000000000)

theorem Zeta5Irrational.U_311_13 : Uω (aρ 13) (bρ 13) (231025508973 / 800000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

theorem Zeta5Irrational.U_311_14 : Uω (aρ 14) (bρ 14) (231025508973 / 800000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_311_15 : Uω (aρ 15) (bρ 15) (231025508973 / 800000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_311_16 : Uω (aρ 16) (bρ 16) (231025508973 / 800000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_311 : Uρ (231025508973 / 800000000000) ≤ -(16530694387511013761449 / 10000000000000000000000)

theorem Zeta5Irrational.U_312_1 : Uω (aρ 1) (bρ 1) (37041824992933 / 128000000000000) ≤ -(12625422528061556459799 / 10000000000000000000000)

theorem Zeta5Irrational.U_312_2 : Uω (aρ 2) (bρ 2) (37041824992933 / 128000000000000) ≤ -(12710930891948740915369 / 10000000000000000000000)

theorem Zeta5Irrational.U_312_3 : Uω (aρ 3) (bρ 3) (37041824992933 / 128000000000000) ≤ -(12884824051920100839147 / 10000000000000000000000)

theorem Zeta5Irrational.U_312_4 : Uω (aρ 4) (bρ 4) (37041824992933 / 128000000000000) ≤ -(1318260220818366757497 / 1000000000000000000000)

theorem Zeta5Irrational.U_312_5 : Uω (aρ 5) (bρ 5) (37041824992933 / 128000000000000) ≤ -(13659785424961961456927 / 10000000000000000000000)

theorem Zeta5Irrational.U_312_6 : Uω (aρ 6) (bρ 6) (37041824992933 / 128000000000000) ≤ -(14402861608877604147629 / 10000000000000000000000)

theorem Zeta5Irrational.U_312_7 : Uω (aρ 7) (bρ 7) (37041824992933 / 128000000000000) ≤ -(7780982377249255875523 / 5000000000000000000000)

theorem Zeta5Irrational.U_312_8 : Uω (aρ 8) (bρ 8) (37041824992933 / 128000000000000) ≤ -(17472355369949165105051 / 10000000000000000000000)

theorem Zeta5Irrational.U_312_9 : Uω (aρ 9) (bρ 9) (37041824992933 / 128000000000000) ≤ -(10797367480776861680277 / 5000000000000000000000)

theorem Zeta5Irrational.U_312_10 : Uω (aρ 10) (bρ 10) (37041824992933 / 128000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_312_11 : Uω (aρ 11) (bρ 11) (37041824992933 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_312_12 : Uω (aρ 12) (bρ 12) (37041824992933 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_312 : Uρ (37041824992933 / 128000000000000) ≤ -(16510867209835616507937 / 10000000000000000000000)

theorem Zeta5Irrational.U_313_1 : Uω (aρ 1) (bρ 1) (18559784275093 / 64000000000000) ≤ -(1575497274129372754583 / 1250000000000000000000)

theorem Zeta5Irrational.U_313_2 : Uω (aρ 2) (bρ 2) (18559784275093 / 64000000000000) ≤ -(12689300131364860125261 / 10000000000000000000000)

theorem Zeta5Irrational.U_313_3 : Uω (aρ 3) (bρ 3) (18559784275093 / 64000000000000) ≤ -(6431403276131736116647 / 5000000000000000000000)

theorem Zeta5Irrational.U_313_4 : Uω (aρ 4) (bρ 4) (18559784275093 / 64000000000000) ≤ -(1644987216254391239947 / 1250000000000000000000)

theorem Zeta5Irrational.U_313_5 : Uω (aρ 5) (bρ 5) (18559784275093 / 64000000000000) ≤ -(13635910122512783687653 / 10000000000000000000000)

theorem Zeta5Irrational.U_313_6 : Uω (aρ 6) (bρ 6) (18559784275093 / 64000000000000) ≤ -(898560605875719717287 / 625000000000000000000)

theorem Zeta5Irrational.U_313_7 : Uω (aρ 7) (bρ 7) (18559784275093 / 64000000000000) ≤ -(155323529047166465161 / 100000000000000000000)

theorem Zeta5Irrational.U_313_8 : Uω (aρ 8) (bρ 8) (18559784275093 / 64000000000000) ≤ -(17434427365685407335693 / 10000000000000000000000)

theorem Zeta5Irrational.U_313_9 : Uω (aρ 9) (bρ 9) (18559784275093 / 64000000000000) ≤ -(10757799638185708569451 / 5000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_313 : Uρ (18559784275093 / 64000000000000) ≤ -(659647742307838339129 / 400000000000000000000)

theorem Zeta5Irrational.U_314_1 : Uω (aρ 1) (bρ 1) (37197312107439 / 128000000000000) ≤ -(2516515949483040556447 / 2000000000000000000000)

theorem Zeta5Irrational.U_314_2 : Uω (aρ 2) (bρ 2) (37197312107439 / 128000000000000) ≤ -(6333858035649365264693 / 5000000000000000000000)

theorem Zeta5Irrational.U_314_3 : Uω (aρ 3) (bρ 3) (37197312107439 / 128000000000000) ≤ -(2568167493990255296731 / 2000000000000000000000)

theorem Zeta5Irrational.U_314_4 : Uω (aρ 4) (bρ 4) (37197312107439 / 128000000000000) ≤ -(2627448966956830868993 / 2000000000000000000000)

theorem Zeta5Irrational.U_314_5 : Uω (aρ 5) (bρ 5) (37197312107439 / 128000000000000) ≤ -(13612092151165089101821 / 10000000000000000000000)

theorem Zeta5Irrational.U_314_6 : Uω (aρ 6) (bρ 6) (37197312107439 / 128000000000000) ≤ -(14351146112426458858217 / 10000000000000000000000)

theorem Zeta5Irrational.U_314_7 : Uω (aρ 7) (bρ 7) (37197312107439 / 128000000000000) ≤ -(15502833683064404763959 / 10000000000000000000000)

theorem Zeta5Irrational.U_314_8 : Uω (aρ 8) (bρ 8) (37197312107439 / 128000000000000) ≤ -(695866732387491057881 / 400000000000000000000)

theorem Zeta5Irrational.U_314_9 : Uω (aρ 9) (bρ 9) (37197312107439 / 128000000000000) ≤ -(21437700710955841835511 / 10000000000000000000000)

theorem Zeta5Irrational.U_314_10 : Uω (aρ 10) (bρ 10) (37197312107439 / 128000000000000) ≤ -(12224255358108186379559 / 5000000000000000000000)

theorem Zeta5Irrational.U_314_11 : Uω (aρ 11) (bρ 11) (37197312107439 / 128000000000000) ≤ -(4457298065613116122159 / 2000000000000000000000)

theorem Zeta5Irrational.U_314_12 : Uω (aρ 12) (bρ 12) (37197312107439 / 128000000000000) ≤ -(640305991230515290559 / 312500000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_314 : Uρ (37197312107439 / 128000000000000) ≤ -(514739632172362430889 / 312500000000000000000)

theorem Zeta5Irrational.U_315_1 : Uω (aρ 1) (bρ 1) (9318763916173 / 32000000000000) ≤ -(1256122699521332861959 / 1000000000000000000000)

theorem Zeta5Irrational.U_315_2 : Uω (aρ 2) (bρ 2) (9318763916173 / 32000000000000) ≤ -(790386156904967377561 / 625000000000000000000)

theorem Zeta5Irrational.U_315_3 : Uω (aρ 3) (bρ 3) (9318763916173 / 32000000000000) ≤ -(6409458296151520141253 / 5000000000000000000000)

theorem Zeta5Irrational.U_315_4 : Uω (aρ 4) (bρ 4) (9318763916173 / 32000000000000) ≤ -(1311464328789948097699 / 1000000000000000000000)

theorem Zeta5Irrational.U_315_5 : Uω (aρ 5) (bρ 5) (9318763916173 / 32000000000000) ≤ -(13588331234040514537341 / 10000000000000000000000)

theorem Zeta5Irrational.U_315_6 : Uω (aρ 6) (bρ 6) (9318763916173 / 32000000000000) ≤ -(7162695248392099559029 / 5000000000000000000000)

theorem Zeta5Irrational.U_315_7 : Uω (aρ 7) (bρ 7) (9318763916173 / 32000000000000) ≤ -(15473406480532042506811 / 10000000000000000000000)

theorem Zeta5Irrational.U_315_8 : Uω (aρ 8) (bρ 8) (9318763916173 / 32000000000000) ≤ -(8679538247702567513831 / 5000000000000000000000)

theorem Zeta5Irrational.U_315_9 : Uω (aρ 9) (bρ 9) (9318763916173 / 32000000000000) ≤ -(21360987514744639833261 / 10000000000000000000000)

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

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

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

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

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

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

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

theorem Zeta5Irrational.U_315 : Uρ (9318763916173 / 32000000000000) ≤ -(4113071593537865275113 / 2500000000000000000000)