Certified arcsine potential bounds (U54)

theorem Zeta5Irrational.U_652_1 : Uω (aρ 1) (bρ 1) (773330129695373 / 1024000000000000) ≤ -(2893456901553794808471 / 10000000000000000000000)

theorem Zeta5Irrational.U_652_2 : Uω (aρ 2) (bρ 2) (773330129695373 / 1024000000000000) ≤ -(1462706849909965999691 / 5000000000000000000000)

theorem Zeta5Irrational.U_652_3 : Uω (aρ 3) (bρ 3) (773330129695373 / 1024000000000000) ≤ -(1494799872180451229579 / 5000000000000000000000)

theorem Zeta5Irrational.U_652_4 : Uω (aρ 4) (bρ 4) (773330129695373 / 1024000000000000) ≤ -(3097011815094364335053 / 10000000000000000000000)

theorem Zeta5Irrational.U_652_5 : Uω (aρ 5) (bρ 5) (773330129695373 / 1024000000000000) ≤ -(3262544425323638530593 / 10000000000000000000000)

theorem Zeta5Irrational.U_652_6 : Uω (aρ 6) (bρ 6) (773330129695373 / 1024000000000000) ≤ -(1752077120803032959657 / 5000000000000000000000)

theorem Zeta5Irrational.U_652_7 : Uω (aρ 7) (bρ 7) (773330129695373 / 1024000000000000) ≤ -(3841985736840612427921 / 10000000000000000000000)

theorem Zeta5Irrational.U_652_8 : Uω (aρ 8) (bρ 8) (773330129695373 / 1024000000000000) ≤ -(4297532680459312403669 / 10000000000000000000000)

theorem Zeta5Irrational.U_652_9 : Uω (aρ 9) (bρ 9) (773330129695373 / 1024000000000000) ≤ -(2446440040483157550377 / 5000000000000000000000)

theorem Zeta5Irrational.U_652_10 : Uω (aρ 10) (bρ 10) (773330129695373 / 1024000000000000) ≤ -(5650069981818022359461 / 10000000000000000000000)

theorem Zeta5Irrational.U_652_11 : Uω (aρ 11) (bρ 11) (773330129695373 / 1024000000000000) ≤ -(6590630992571855497951 / 10000000000000000000000)

theorem Zeta5Irrational.U_652_12 : Uω (aρ 12) (bρ 12) (773330129695373 / 1024000000000000) ≤ -(7735265208020603162373 / 10000000000000000000000)

theorem Zeta5Irrational.U_652_13 : Uω (aρ 13) (bρ 13) (773330129695373 / 1024000000000000) ≤ -(9103538205482609527087 / 10000000000000000000000)

theorem Zeta5Irrational.U_652_14 : Uω (aρ 14) (bρ 14) (773330129695373 / 1024000000000000) ≤ -(10712917914125938837233 / 10000000000000000000000)

theorem Zeta5Irrational.U_652_15 : Uω (aρ 15) (bρ 15) (773330129695373 / 1024000000000000) ≤ -(1571724976514098835237 / 1250000000000000000000)

theorem Zeta5Irrational.U_652_16 : Uω (aρ 16) (bρ 16) (773330129695373 / 1024000000000000) ≤ -(7323588502680710169883 / 5000000000000000000000)

theorem Zeta5Irrational.U_652 : Uρ (773330129695373 / 1024000000000000) ≤ -(636726646180617477787 / 1250000000000000000000)

theorem Zeta5Irrational.U_653_1 : Uω (aρ 1) (bρ 1) (96822936549963 / 128000000000000) ≤ -(2877123201811696091637 / 10000000000000000000000)

theorem Zeta5Irrational.U_653_2 : Uω (aρ 2) (bρ 2) (96822936549963 / 128000000000000) ≤ -(1454513748973133960733 / 5000000000000000000000)

theorem Zeta5Irrational.U_653_3 : Uω (aρ 3) (bρ 3) (96822936549963 / 128000000000000) ≤ -(185819207586795205137 / 625000000000000000000)

theorem Zeta5Irrational.U_653_4 : Uω (aρ 4) (bρ 4) (96822936549963 / 128000000000000) ≤ -(3080339305095248653731 / 10000000000000000000000)

theorem Zeta5Irrational.U_653_5 : Uω (aρ 5) (bρ 5) (96822936549963 / 128000000000000) ≤ -(64911770518235379883 / 200000000000000000000)

theorem Zeta5Irrational.U_653_6 : Uω (aρ 6) (bρ 6) (96822936549963 / 128000000000000) ≤ -(174338573018717726637 / 500000000000000000000)

theorem Zeta5Irrational.U_653_7 : Uω (aρ 7) (bρ 7) (96822936549963 / 128000000000000) ≤ -(1911989087255013801439 / 5000000000000000000000)

theorem Zeta5Irrational.U_653_8 : Uω (aρ 8) (bρ 8) (96822936549963 / 128000000000000) ≤ -(2139313420275157981527 / 5000000000000000000000)

theorem Zeta5Irrational.U_653_9 : Uω (aρ 9) (bρ 9) (96822936549963 / 128000000000000) ≤ -(1218173088127056917877 / 2500000000000000000000)

theorem Zeta5Irrational.U_653_10 : Uω (aρ 10) (bρ 10) (96822936549963 / 128000000000000) ≤ -(5628046299432133914873 / 10000000000000000000000)

theorem Zeta5Irrational.U_653_11 : Uω (aρ 11) (bρ 11) (96822936549963 / 128000000000000) ≤ -(6565933545682449290393 / 10000000000000000000000)

theorem Zeta5Irrational.U_653_12 : Uω (aρ 12) (bρ 12) (96822936549963 / 128000000000000) ≤ -(7706540205108390999763 / 10000000000000000000000)

theorem Zeta5Irrational.U_653_13 : Uω (aρ 13) (bρ 13) (96822936549963 / 128000000000000) ≤ -(2267094840206635581753 / 2500000000000000000000)

theorem Zeta5Irrational.U_653_14 : Uω (aρ 14) (bρ 14) (96822936549963 / 128000000000000) ≤ -(10666391102895760677611 / 10000000000000000000000)

theorem Zeta5Irrational.U_653_15 : Uω (aρ 15) (bρ 15) (96822936549963 / 128000000000000) ≤ -(12503095599865301573741 / 10000000000000000000000)

theorem Zeta5Irrational.U_653_16 : Uω (aρ 16) (bρ 16) (96822936549963 / 128000000000000) ≤ -(14500144393995872475567 / 10000000000000000000000)

theorem Zeta5Irrational.U_653 : Uρ (96822936549963 / 128000000000000) ≤ -(2535469459548085995737 / 5000000000000000000000)

theorem Zeta5Irrational.U_654_1 : Uω (aρ 1) (bρ 1) (155167371020807 / 204800000000000) ≤ -(178801008606094785107 / 625000000000000000000)

theorem Zeta5Irrational.U_654_2 : Uω (aρ 2) (bρ 2) (155167371020807 / 204800000000000) ≤ -(180791756495602557493 / 625000000000000000000)

theorem Zeta5Irrational.U_654_3 : Uω (aρ 3) (bρ 3) (155167371020807 / 204800000000000) ≤ -(2956642057273893298753 / 10000000000000000000000)

theorem Zeta5Irrational.U_654_4 : Uω (aρ 4) (bρ 4) (155167371020807 / 204800000000000) ≤ -(612738911377929143541 / 2000000000000000000000)

theorem Zeta5Irrational.U_654_5 : Uω (aρ 5) (bρ 5) (155167371020807 / 204800000000000) ≤ -(3228661357312839731263 / 10000000000000000000000)

theorem Zeta5Irrational.U_654_6 : Uω (aρ 6) (bρ 6) (155167371020807 / 204800000000000) ≤ -(1734709458567699032261 / 5000000000000000000000)

theorem Zeta5Irrational.U_654_7 : Uω (aρ 7) (bρ 7) (155167371020807 / 204800000000000) ≤ -(761200632335293118429 / 2000000000000000000000)

theorem Zeta5Irrational.U_654_8 : Uω (aρ 8) (bρ 8) (155167371020807 / 204800000000000) ≤ -(425975710149634223111 / 1000000000000000000000)

theorem Zeta5Irrational.U_654_9 : Uω (aρ 9) (bρ 9) (155167371020807 / 204800000000000) ≤ -(4852546282406263118157 / 10000000000000000000000)

theorem Zeta5Irrational.U_654_10 : Uω (aρ 10) (bρ 10) (155167371020807 / 204800000000000) ≤ -(2803036653647281027841 / 5000000000000000000000)

theorem Zeta5Irrational.U_654_11 : Uω (aρ 11) (bρ 11) (155167371020807 / 204800000000000) ≤ -(817662801515715558399 / 1250000000000000000000)

theorem Zeta5Irrational.U_654_12 : Uω (aρ 12) (bρ 12) (155167371020807 / 204800000000000) ≤ -(239934727155107788411 / 312500000000000000000)

theorem Zeta5Irrational.U_654_13 : Uω (aρ 13) (bρ 13) (155167371020807 / 204800000000000) ≤ -(2258345563885136111871 / 2500000000000000000000)

theorem Zeta5Irrational.U_654_14 : Uω (aρ 14) (bρ 14) (155167371020807 / 204800000000000) ≤ -(5310104766705545786437 / 5000000000000000000000)

theorem Zeta5Irrational.U_654_15 : Uω (aρ 15) (bρ 15) (155167371020807 / 204800000000000) ≤ -(12433514339998384626713 / 10000000000000000000000)

theorem Zeta5Irrational.U_654_16 : Uω (aρ 16) (bρ 16) (155167371020807 / 204800000000000) ≤ -(14362160113274664036023 / 10000000000000000000000)

theorem Zeta5Irrational.U_654 : Uρ (155167371020807 / 204800000000000) ≤ -(5048211830024685695573 / 10000000000000000000000)

theorem Zeta5Irrational.U_655_1 : Uω (aρ 1) (bρ 1) (388545108904183 / 512000000000000) ≤ -(44445869101279289721 / 156250000000000000000)

theorem Zeta5Irrational.U_655_2 : Uω (aρ 2) (bρ 2) (388545108904183 / 512000000000000) ≤ -(2876335430194582704191 / 10000000000000000000000)

theorem Zeta5Irrational.U_655_3 : Uω (aρ 3) (bρ 3) (388545108904183 / 512000000000000) ≤ -(2940203862703970074569 / 10000000000000000000000)

theorem Zeta5Irrational.U_655_4 : Uω (aρ 4) (bρ 4) (388545108904183 / 512000000000000) ≤ -(3047077478141810132203 / 10000000000000000000000)

theorem Zeta5Irrational.U_655_5 : Uω (aρ 5) (bρ 5) (388545108904183 / 512000000000000) ≤ -(80294070555689559269 / 250000000000000000000)

theorem Zeta5Irrational.U_655_6 : Uω (aρ 6) (bρ 6) (388545108904183 / 512000000000000) ≤ -(1726048253307382550747 / 5000000000000000000000)

theorem Zeta5Irrational.U_655_7 : Uω (aρ 7) (bρ 7) (388545108904183 / 512000000000000) ≤ -(3788060580235419980457 / 10000000000000000000000)

theorem Zeta5Irrational.U_655_8 : Uω (aρ 8) (bρ 8) (388545108904183 / 512000000000000) ≤ -(4240923324085287446963 / 10000000000000000000000)

theorem Zeta5Irrational.U_655_9 : Uω (aρ 9) (bρ 9) (388545108904183 / 512000000000000) ≤ -(966488339018040144383 / 2000000000000000000000)

theorem Zeta5Irrational.U_655_10 : Uω (aρ 10) (bρ 10) (388545108904183 / 512000000000000) ≤ -(5584150762359065444067 / 10000000000000000000000)

theorem Zeta5Irrational.U_655_11 : Uω (aρ 11) (bρ 11) (388545108904183 / 512000000000000) ≤ -(6516737208834470122621 / 10000000000000000000000)

theorem Zeta5Irrational.U_655_12 : Uω (aρ 12) (bρ 12) (388545108904183 / 512000000000000) ≤ -(7649377674455245816967 / 10000000000000000000000)

theorem Zeta5Irrational.U_655_13 : Uω (aρ 13) (bρ 13) (388545108904183 / 512000000000000) ≤ -(8998545100638613692049 / 10000000000000000000000)

theorem Zeta5Irrational.U_655_14 : Uω (aρ 14) (bρ 14) (388545108904183 / 512000000000000) ≤ -(10574366596004491116633 / 10000000000000000000000)

theorem Zeta5Irrational.U_655_15 : Uω (aρ 15) (bρ 15) (388545108904183 / 512000000000000) ≤ -(247300147688838586911 / 200000000000000000000)

theorem Zeta5Irrational.U_655_16 : Uω (aρ 16) (bρ 16) (388545108904183 / 512000000000000) ≤ -(889484798547236706907 / 625000000000000000000)

theorem Zeta5Irrational.U_655 : Uρ (388545108904183 / 512000000000000) ≤ -(5025621108762662119411 / 10000000000000000000000)

theorem Zeta5Irrational.U_656_1 : Uω (aρ 1) (bρ 1) (194899235804257 / 256000000000000) ≤ -(703013473485130443647 / 2500000000000000000000)

theorem Zeta5Irrational.U_656_2 : Uω (aρ 2) (bρ 2) (194899235804257 / 256000000000000) ≤ -(568749979081353075301 / 2000000000000000000000)

theorem Zeta5Irrational.U_656_3 : Uω (aρ 3) (bρ 3) (194899235804257 / 256000000000000) ≤ -(2907408327145662851251 / 10000000000000000000000)

theorem Zeta5Irrational.U_656_4 : Uω (aρ 4) (bρ 4) (194899235804257 / 256000000000000) ≤ -(3013925961973787554127 / 10000000000000000000000)

theorem Zeta5Irrational.U_656_5 : Uω (aρ 5) (bρ 5) (194899235804257 / 256000000000000) ≤ -(1589025632933657282791 / 5000000000000000000000)

theorem Zeta5Irrational.U_656_6 : Uω (aρ 6) (bρ 6) (194899235804257 / 256000000000000) ≤ -(1708770832688818507607 / 5000000000000000000000)

theorem Zeta5Irrational.U_656_7 : Uω (aρ 7) (bρ 7) (194899235804257 / 256000000000000) ≤ -(1876136121166841495429 / 5000000000000000000000)

theorem Zeta5Irrational.U_656_8 : Uω (aρ 8) (bρ 8) (194899235804257 / 256000000000000) ≤ -(420336310140069993621 / 1000000000000000000000)

theorem Zeta5Irrational.U_656_9 : Uω (aρ 9) (bρ 9) (194899235804257 / 256000000000000) ≤ -(2396178136091364650849 / 5000000000000000000000)

theorem Zeta5Irrational.U_656_10 : Uω (aρ 10) (bρ 10) (194899235804257 / 256000000000000) ≤ -(692557006368090820231 / 1250000000000000000000)

theorem Zeta5Irrational.U_656_11 : Uω (aρ 11) (bρ 11) (194899235804257 / 256000000000000) ≤ -(6467803078306683504167 / 10000000000000000000000)

theorem Zeta5Irrational.U_656_12 : Uω (aρ 12) (bρ 12) (194899235804257 / 256000000000000) ≤ -(237268551693682025271 / 312500000000000000000)

theorem Zeta5Irrational.U_656_13 : Uω (aρ 13) (bρ 13) (194899235804257 / 256000000000000) ≤ -(4464671824597859984033 / 5000000000000000000000)

theorem Zeta5Irrational.U_656_14 : Uω (aρ 14) (bρ 14) (194899235804257 / 256000000000000) ≤ -(163807362855826435447 / 156250000000000000000)

theorem Zeta5Irrational.U_656_15 : Uω (aρ 15) (bρ 15) (194899235804257 / 256000000000000) ≤ -(2446207738464103347739 / 2000000000000000000000)

theorem Zeta5Irrational.U_656_16 : Uω (aρ 16) (bρ 16) (194899235804257 / 256000000000000) ≤ -(559580302932836820887 / 400000000000000000000)

theorem Zeta5Irrational.U_656 : Uρ (194899235804257 / 256000000000000) ≤ -(498081621074527344563 / 1000000000000000000000)

theorem Zeta5Irrational.U_657_1 : Uω (aρ 1) (bρ 1) (78210366862569 / 102400000000000) ≤ -(1389838665380847924577 / 5000000000000000000000)

theorem Zeta5Irrational.U_657_2 : Uω (aρ 2) (bρ 2) (78210366862569 / 102400000000000) ≤ -(2811270201498031012067 / 10000000000000000000000)

theorem Zeta5Irrational.U_657_3 : Uω (aρ 3) (bρ 3) (78210366862569 / 102400000000000) ≤ -(57494400179207807219 / 200000000000000000000)

theorem Zeta5Irrational.U_657_4 : Uω (aρ 4) (bρ 4) (78210366862569 / 102400000000000) ≤ -(1490442013525983607791 / 5000000000000000000000)

theorem Zeta5Irrational.U_657_5 : Uω (aρ 5) (bρ 5) (78210366862569 / 102400000000000) ≤ -(3144453088255461251677 / 10000000000000000000000)

theorem Zeta5Irrational.U_657_6 : Uω (aρ 6) (bρ 6) (78210366862569 / 102400000000000) ≤ -(3383106105401640094821 / 10000000000000000000000)

theorem Zeta5Irrational.U_657_7 : Uω (aρ 7) (bρ 7) (78210366862569 / 102400000000000) ≤ -(1858306114393186210517 / 5000000000000000000000)

theorem Zeta5Irrational.U_657_8 : Uω (aρ 8) (bρ 8) (78210366862569 / 102400000000000) ≤ -(2082972537469778711169 / 5000000000000000000000)

theorem Zeta5Irrational.U_657_9 : Uω (aρ 9) (bρ 9) (78210366862569 / 102400000000000) ≤ -(4752434701677612012609 / 10000000000000000000000)

theorem Zeta5Irrational.U_657_10 : Uω (aρ 10) (bρ 10) (78210366862569 / 102400000000000) ≤ -(1374240064175814711503 / 2500000000000000000000)

theorem Zeta5Irrational.U_657_11 : Uω (aρ 11) (bρ 11) (78210366862569 / 102400000000000) ≤ -(6419128159047950867803 / 10000000000000000000000)

theorem Zeta5Irrational.U_657_12 : Uω (aρ 12) (bρ 12) (78210366862569 / 102400000000000) ≤ -(942022814831744407111 / 1250000000000000000000)

theorem Zeta5Irrational.U_657_13 : Uω (aρ 13) (bρ 13) (78210366862569 / 102400000000000) ≤ -(4430380667806009793779 / 5000000000000000000000)

theorem Zeta5Irrational.U_657_14 : Uω (aρ 14) (bρ 14) (78210366862569 / 102400000000000) ≤ -(5197128077412783468093 / 5000000000000000000000)

theorem Zeta5Irrational.U_657_15 : Uω (aρ 15) (bρ 15) (78210366862569 / 102400000000000) ≤ -(12100863543607861278483 / 10000000000000000000000)

theorem Zeta5Irrational.U_657_16 : Uω (aρ 16) (bρ 16) (78210366862569 / 102400000000000) ≤ -(6883547383324041154463 / 5000000000000000000000)

theorem Zeta5Irrational.U_657 : Uρ (78210366862569 / 102400000000000) ≤ -(4936472451356495359701 / 10000000000000000000000)

theorem Zeta5Irrational.U_658_1 : Uω (aρ 1) (bρ 1) (49038149627147 / 64000000000000) ≤ -(171712828384726161937 / 625000000000000000000)

theorem Zeta5Irrational.U_658_2 : Uω (aρ 2) (bρ 2) (49038149627147 / 64000000000000) ≤ -(2778895663106141822649 / 10000000000000000000000)

theorem Zeta5Irrational.U_658_3 : Uω (aρ 3) (bρ 3) (49038149627147 / 64000000000000) ≤ -(2842138209295904021429 / 10000000000000000000000)

theorem Zeta5Irrational.U_658_4 : Uω (aρ 4) (bρ 4) (49038149627147 / 64000000000000) ≤ -(1473975475526614955667 / 5000000000000000000000)

theorem Zeta5Irrational.U_658_5 : Uω (aρ 5) (bρ 5) (49038149627147 / 64000000000000) ≤ -(12443870114242395501 / 40000000000000000000)

theorem Zeta5Irrational.U_658_6 : Uω (aρ 6) (bρ 6) (49038149627147 / 64000000000000) ≤ -(3348789004045531172871 / 10000000000000000000000)

theorem Zeta5Irrational.U_658_7 : Uω (aρ 7) (bρ 7) (49038149627147 / 64000000000000) ≤ -(3681079617672882922721 / 10000000000000000000000)

theorem Zeta5Irrational.U_658_8 : Uω (aρ 8) (bρ 8) (49038149627147 / 64000000000000) ≤ -(3225521999879289743 / 7812500000000000000)

theorem Zeta5Irrational.U_658_9 : Uω (aρ 9) (bρ 9) (49038149627147 / 64000000000000) ≤ -(4712675619102600426311 / 10000000000000000000000)

theorem Zeta5Irrational.U_658_10 : Uω (aρ 10) (bρ 10) (49038149627147 / 64000000000000) ≤ -(2726830749623017945813 / 5000000000000000000000)

theorem Zeta5Irrational.U_658_11 : Uω (aρ 11) (bρ 11) (49038149627147 / 64000000000000) ≤ -(6370709510127633117299 / 10000000000000000000000)

theorem Zeta5Irrational.U_658_12 : Uω (aρ 12) (bρ 12) (49038149627147 / 64000000000000) ≤ -(7480138777450943837259 / 10000000000000000000000)

theorem Zeta5Irrational.U_658_13 : Uω (aρ 13) (bρ 13) (49038149627147 / 64000000000000) ≤ -(8792784974843993706773 / 10000000000000000000000)

theorem Zeta5Irrational.U_658_14 : Uω (aρ 14) (bρ 14) (49038149627147 / 64000000000000) ≤ -(644129719662722860471 / 625000000000000000000)

theorem Zeta5Irrational.U_658_15 : Uω (aρ 15) (bρ 15) (49038149627147 / 64000000000000) ≤ -(11974197185992771512583 / 10000000000000000000000)

theorem Zeta5Irrational.U_658_16 : Uω (aρ 16) (bρ 16) (49038149627147 / 64000000000000) ≤ -(13560409783495217840437 / 10000000000000000000000)

theorem Zeta5Irrational.U_658 : Uρ (49038149627147 / 64000000000000) ≤ -(1223138141627158991151 / 2500000000000000000000)

theorem Zeta5Irrational.U_659_1 : Uω (aρ 1) (bρ 1) (393558559721507 / 512000000000000) ≤ -(2715236991883287655507 / 10000000000000000000000)

theorem Zeta5Irrational.U_659_2 : Uω (aρ 2) (bρ 2) (393558559721507 / 512000000000000) ≤ -(10986502406018490339 / 40000000000000000000)

theorem Zeta5Irrational.U_659_3 : Uω (aρ 3) (bρ 3) (393558559721507 / 512000000000000) ≤ -(2809662236111423922899 / 10000000000000000000000)

theorem Zeta5Irrational.U_659_4 : Uω (aρ 4) (bρ 4) (393558559721507 / 512000000000000) ≤ -(1457563009387830351699 / 5000000000000000000000)

theorem Zeta5Irrational.U_659_5 : Uω (aρ 5) (bρ 5) (393558559721507 / 512000000000000) ≤ -(3077593833591589989139 / 10000000000000000000000)

theorem Zeta5Irrational.U_659_6 : Uω (aρ 6) (bρ 6) (393558559721507 / 512000000000000) ≤ -(1657294773584553884893 / 5000000000000000000000)

theorem Zeta5Irrational.U_659_7 : Uω (aρ 7) (bρ 7) (393558559721507 / 512000000000000) ≤ -(729134699404871384131 / 2000000000000000000000)

theorem Zeta5Irrational.U_659_8 : Uω (aρ 8) (bρ 8) (393558559721507 / 512000000000000) ≤ -(4091531283765524748763 / 10000000000000000000000)

theorem Zeta5Irrational.U_659_9 : Uω (aρ 9) (bρ 9) (393558559721507 / 512000000000000) ≤ -(2336538838658455572537 / 5000000000000000000000)

theorem Zeta5Irrational.U_659_10 : Uω (aρ 10) (bρ 10) (393558559721507 / 512000000000000) ≤ -(2705278962857846117447 / 5000000000000000000000)

theorem Zeta5Irrational.U_659_11 : Uω (aρ 11) (bρ 11) (393558559721507 / 512000000000000) ≤ -(1580636060845473348809 / 2500000000000000000000)

theorem Zeta5Irrational.U_659_12 : Uω (aρ 12) (bρ 12) (393558559721507 / 512000000000000) ≤ -(742445707098810187001 / 1000000000000000000000)

theorem Zeta5Irrational.U_659_13 : Uω (aρ 13) (bρ 13) (393558559721507 / 512000000000000) ≤ -(8725401843653626065141 / 10000000000000000000000)

theorem Zeta5Irrational.U_659_14 : Uω (aρ 14) (bρ 14) (393558559721507 / 512000000000000) ≤ -(5109543065045329487741 / 5000000000000000000000)

theorem Zeta5Irrational.U_659_15 : Uω (aρ 15) (bρ 15) (393558559721507 / 512000000000000) ≤ -(5925394563411376445939 / 5000000000000000000000)

theorem Zeta5Irrational.U_659_16 : Uω (aρ 16) (bρ 16) (393558559721507 / 512000000000000) ≤ -(6683298545853789424627 / 5000000000000000000000)

theorem Zeta5Irrational.U_659 : Uρ (393558559721507 / 512000000000000) ≤ -(2424513986067734309671 / 5000000000000000000000)

theorem Zeta5Irrational.U_660_1 : Uω (aρ 1) (bρ 1) (197405961212919 / 256000000000000) ≤ -(2683171878172451050851 / 10000000000000000000000)

theorem Zeta5Irrational.U_660_2 : Uω (aρ 2) (bρ 2) (197405961212919 / 256000000000000) ≤ -(1357229672258682030653 / 5000000000000000000000)

theorem Zeta5Irrational.U_660_3 : Uω (aρ 3) (bρ 3) (197405961212919 / 256000000000000) ≤ -(1388645702044695172863 / 5000000000000000000000)

theorem Zeta5Irrational.U_660_4 : Uω (aρ 4) (bρ 4) (197405961212919 / 256000000000000) ≤ -(720602130511302706029 / 2500000000000000000000)

theorem Zeta5Irrational.U_660_5 : Uω (aρ 5) (bρ 5) (197405961212919 / 256000000000000) ≤ -(1522165628847763865193 / 5000000000000000000000)

theorem Zeta5Irrational.U_660_6 : Uω (aρ 6) (bρ 6) (197405961212919 / 256000000000000) ≤ -(20503168306351268131 / 62500000000000000000)

theorem Zeta5Irrational.U_660_7 : Uω (aρ 7) (bρ 7) (197405961212919 / 256000000000000) ≤ -(1805196482340114028887 / 5000000000000000000000)

theorem Zeta5Irrational.U_660_8 : Uω (aρ 8) (bρ 8) (197405961212919 / 256000000000000) ≤ -(4054533386656685392731 / 10000000000000000000000)

theorem Zeta5Irrational.U_660_9 : Uω (aρ 9) (bρ 9) (197405961212919 / 256000000000000) ≤ -(1158409886553347536791 / 2500000000000000000000)

theorem Zeta5Irrational.U_660_10 : Uω (aρ 10) (bρ 10) (197405961212919 / 256000000000000) ≤ -(5367647710234672246907 / 10000000000000000000000)

theorem Zeta5Irrational.U_660_11 : Uω (aρ 11) (bρ 11) (197405961212919 / 256000000000000) ≤ -(1568657380525846977687 / 2500000000000000000000)

theorem Zeta5Irrational.U_660_12 : Uω (aρ 12) (bρ 12) (197405961212919 / 256000000000000) ≤ -(3684566083047103674919 / 5000000000000000000000)

theorem Zeta5Irrational.U_660_13 : Uω (aρ 13) (bρ 13) (197405961212919 / 256000000000000) ≤ -(4329299829043131844737 / 5000000000000000000000)

theorem Zeta5Irrational.U_660_14 : Uω (aρ 14) (bρ 14) (197405961212919 / 256000000000000) ≤ -(1013324731520483938837 / 1000000000000000000000)

theorem Zeta5Irrational.U_660_15 : Uω (aρ 15) (bρ 15) (197405961212919 / 256000000000000) ≤ -(11730417611087330118851 / 10000000000000000000000)

theorem Zeta5Irrational.U_660_16 : Uω (aρ 16) (bρ 16) (197405961212919 / 256000000000000) ≤ -(659178816886656724683 / 500000000000000000000)

theorem Zeta5Irrational.U_660 : Uρ (197405961212919 / 256000000000000) ≤ -(2402937868237377408313 / 5000000000000000000000)

theorem Zeta5Irrational.U_661_1 : Uω (aρ 1) (bρ 1) (396065285130169 / 512000000000000) ≤ -(662802313408731620701 / 2500000000000000000000)

theorem Zeta5Irrational.U_661_2 : Uω (aρ 2) (bρ 2) (396065285130169 / 512000000000000) ≤ -(2682396226434606046731 / 10000000000000000000000)

theorem Zeta5Irrational.U_661_3 : Uω (aρ 3) (bρ 3) (396065285130169 / 512000000000000) ≤ -(54900500690973011711 / 200000000000000000000)

theorem Zeta5Irrational.U_661_4 : Uω (aρ 4) (bρ 4) (396065285130169 / 512000000000000) ≤ -(2849797759623886644061 / 10000000000000000000000)

theorem Zeta5Irrational.U_661_5 : Uω (aρ 5) (bρ 5) (396065285130169 / 512000000000000) ≤ -(301117906265737937309 / 1000000000000000000000)

theorem Zeta5Irrational.U_661_6 : Uω (aρ 6) (bρ 6) (396065285130169 / 512000000000000) ≤ -(1623270176049848597967 / 5000000000000000000000)

theorem Zeta5Irrational.U_661_7 : Uω (aρ 7) (bρ 7) (396065285130169 / 512000000000000) ≤ -(3575237128147365079751 / 10000000000000000000000)

theorem Zeta5Irrational.U_661_8 : Uω (aρ 8) (bρ 8) (396065285130169 / 512000000000000) ≤ -(803534684119275944343 / 2000000000000000000000)

theorem Zeta5Irrational.U_661_9 : Uω (aρ 9) (bρ 9) (396065285130169 / 512000000000000) ≤ -(459435991242715682401 / 1000000000000000000000)

theorem Zeta5Irrational.U_661_10 : Uω (aρ 10) (bρ 10) (396065285130169 / 512000000000000) ≤ -(5324929053367865177511 / 10000000000000000000000)

theorem Zeta5Irrational.U_661_11 : Uω (aρ 11) (bρ 11) (396065285130169 / 512000000000000) ≤ -(15567406399431601151 / 25000000000000000000)

theorem Zeta5Irrational.U_661_12 : Uω (aρ 12) (bρ 12) (396065285130169 / 512000000000000) ≤ -(3657079475934853258049 / 5000000000000000000000)

theorem Zeta5Irrational.U_661_13 : Uω (aρ 13) (bρ 13) (396065285130169 / 512000000000000) ≤ -(4296183276173925836353 / 5000000000000000000000)

theorem Zeta5Irrational.U_661_14 : Uω (aρ 14) (bρ 14) (396065285130169 / 512000000000000) ≤ -(5024260336321951904853 / 5000000000000000000000)

theorem Zeta5Irrational.U_661_15 : Uω (aρ 15) (bρ 15) (396065285130169 / 512000000000000) ≤ -(11612885194558307579307 / 10000000000000000000000)

theorem Zeta5Irrational.U_661_16 : Uω (aρ 16) (bρ 16) (396065285130169 / 512000000000000) ≤ -(13009776067628077066779 / 10000000000000000000000)

theorem Zeta5Irrational.U_661 : Uρ (396065285130169 / 512000000000000) ≤ -(4763076847769005740497 / 10000000000000000000000)

theorem Zeta5Irrational.U_662_1 : Uω (aρ 1) (bρ 1) (794637295669 / 1024000000000) ≤ -(2619348465185242405921 / 10000000000000000000000)

theorem Zeta5Irrational.U_662_2 : Uω (aρ 2) (bρ 2) (794637295669 / 1024000000000) ≤ -(530087117586050276873 / 2000000000000000000000)

theorem Zeta5Irrational.U_662_3 : Uω (aρ 3) (bρ 3) (794637295669 / 1024000000000) ≤ -(1356431227679515851249 / 5000000000000000000000)

theorem Zeta5Irrational.U_662_4 : Uω (aρ 4) (bρ 4) (794637295669 / 1024000000000) ≤ -(56345860742388664727 / 200000000000000000000)

theorem Zeta5Irrational.U_662_5 : Uω (aρ 5) (bρ 5) (794637295669 / 1024000000000) ≤ -(1489068258800647595981 / 5000000000000000000000)

theorem Zeta5Irrational.U_662_6 : Uω (aρ 6) (bρ 6) (794637295669 / 1024000000000) ≤ -(401586128386062271131 / 1250000000000000000000)

theorem Zeta5Irrational.U_662_7 : Uω (aρ 7) (bρ 7) (794637295669 / 1024000000000) ≤ -(442525638057717244647 / 1250000000000000000000)

theorem Zeta5Irrational.U_662_8 : Uω (aρ 8) (bρ 8) (794637295669 / 1024000000000) ≤ -(39809503495964381451 / 100000000000000000000)

theorem Zeta5Irrational.U_662_9 : Uω (aρ 9) (bρ 9) (794637295669 / 1024000000000) ≤ -(455523747905055093527 / 1000000000000000000000)

theorem Zeta5Irrational.U_662_10 : Uω (aρ 10) (bρ 10) (794637295669 / 1024000000000) ≤ -(1056480036319776071903 / 2000000000000000000000)

theorem Zeta5Irrational.U_662_11 : Uω (aρ 11) (bρ 11) (794637295669 / 1024000000000) ≤ -(1235908123765897962347 / 2000000000000000000000)

theorem Zeta5Irrational.U_662_12 : Uω (aρ 12) (bρ 12) (794637295669 / 1024000000000) ≤ -(7259532435704126432831 / 10000000000000000000000)

theorem Zeta5Irrational.U_662_13 : Uω (aρ 13) (bρ 13) (794637295669 / 1024000000000) ≤ -(8526691058976463844233 / 10000000000000000000000)

theorem Zeta5Irrational.U_662_14 : Uω (aρ 14) (bρ 14) (794637295669 / 1024000000000) ≤ -(4982434958219247805323 / 5000000000000000000000)

theorem Zeta5Irrational.U_662_15 : Uω (aρ 15) (bρ 15) (794637295669 / 1024000000000) ≤ -(11498015157682552696681 / 10000000000000000000000)

theorem Zeta5Irrational.U_662_16 : Uω (aρ 16) (bρ 16) (794637295669 / 1024000000000) ≤ -(50171776057069747423 / 39062500000000000000)

theorem Zeta5Irrational.U_662 : Uρ (794637295669 / 1024000000000) ≤ -(590076893444211888841 / 1250000000000000000000)

theorem Zeta5Irrational.U_663_1 : Uω (aρ 1) (bρ 1) (398572010538831 / 512000000000000) ≤ -(1293794432980282284923 / 5000000000000000000000)

theorem Zeta5Irrational.U_663_2 : Uω (aρ 2) (bρ 2) (398572010538831 / 512000000000000) ≤ -(654644193995127234473 / 2500000000000000000000)

theorem Zeta5Irrational.U_663_3 : Uω (aρ 3) (bρ 3) (398572010538831 / 512000000000000) ≤ -(2680803000857294788523 / 10000000000000000000000)

theorem Zeta5Irrational.U_663_4 : Uω (aρ 4) (bρ 4) (398572010538831 / 512000000000000) ≤ -(2784893666896482135699 / 10000000000000000000000)

theorem Zeta5Irrational.U_663_5 : Uω (aρ 5) (bρ 5) (398572010538831 / 512000000000000) ≤ -(368150362361694042147 / 1250000000000000000000)

theorem Zeta5Irrational.U_663_6 : Uω (aρ 6) (bρ 6) (398572010538831 / 512000000000000) ≤ -(1589476086348222504551 / 5000000000000000000000)

theorem Zeta5Irrational.U_663_7 : Uω (aρ 7) (bρ 7) (398572010538831 / 512000000000000) ≤ -(3505296020052566257047 / 10000000000000000000000)

theorem Zeta5Irrational.U_663_8 : Uω (aρ 8) (bρ 8) (398572010538831 / 512000000000000) ≤ -(493045393677593413659 / 1250000000000000000000)

theorem Zeta5Irrational.U_663_9 : Uω (aρ 9) (bρ 9) (398572010538831 / 512000000000000) ≤ -(903254193070843639721 / 2000000000000000000000)

theorem Zeta5Irrational.U_663_10 : Uω (aρ 10) (bρ 10) (398572010538831 / 512000000000000) ≤ -(5240059346819541959201 / 10000000000000000000000)

theorem Zeta5Irrational.U_663_11 : Uω (aρ 11) (bρ 11) (398572010538831 / 512000000000000) ≤ -(6132361009483060921937 / 10000000000000000000000)

theorem Zeta5Irrational.U_663_12 : Uω (aρ 12) (bρ 12) (398572010538831 / 512000000000000) ≤ -(1441049547891940481097 / 2000000000000000000000)

theorem Zeta5Irrational.U_663_13 : Uω (aρ 13) (bρ 13) (398572010538831 / 512000000000000) ≤ -(2115390522553072752363 / 2500000000000000000000)

theorem Zeta5Irrational.U_663_14 : Uω (aρ 14) (bρ 14) (398572010538831 / 512000000000000) ≤ -(9882260711854623304547 / 10000000000000000000000)

theorem Zeta5Irrational.U_663_15 : Uω (aρ 15) (bρ 15) (398572010538831 / 512000000000000) ≤ -(11385648572861481335083 / 10000000000000000000000)

theorem Zeta5Irrational.U_663_16 : Uω (aρ 16) (bρ 16) (398572010538831 / 512000000000000) ≤ -(3171300016281540266367 / 2500000000000000000000)

theorem Zeta5Irrational.U_663 : Uρ (398572010538831 / 512000000000000) ≤ -(4678476634791325595441 / 10000000000000000000000)