Certified arcsine potential bounds (U43)

theorem Zeta5Irrational.U_520_1 : Uω (aρ 1) (bρ 1) (9287519810631 / 16000000000000) ≤ -(2775477411467269153561 / 5000000000000000000000)

theorem Zeta5Irrational.U_520_2 : Uω (aρ 2) (bρ 2) (9287519810631 / 16000000000000) ≤ -(5592724374280311294667 / 10000000000000000000000)

theorem Zeta5Irrational.U_520_3 : Uω (aρ 3) (bρ 3) (9287519810631 / 16000000000000) ≤ -(5676808531728931494759 / 10000000000000000000000)

theorem Zeta5Irrational.U_520_4 : Uω (aρ 4) (bρ 4) (9287519810631 / 16000000000000) ≤ -(5818095913874656755391 / 10000000000000000000000)

theorem Zeta5Irrational.U_520_5 : Uω (aρ 5) (bρ 5) (9287519810631 / 16000000000000) ≤ -(3018650477316833315497 / 5000000000000000000000)

theorem Zeta5Irrational.U_520_6 : Uω (aρ 6) (bρ 6) (9287519810631 / 16000000000000) ≤ -(795079433204800478269 / 1250000000000000000000)

theorem Zeta5Irrational.U_520_7 : Uω (aρ 7) (bρ 7) (9287519810631 / 16000000000000) ≤ -(6820086630363946455629 / 10000000000000000000000)

theorem Zeta5Irrational.U_520_8 : Uω (aρ 8) (bρ 8) (9287519810631 / 16000000000000) ≤ -(7455040704754400716783 / 10000000000000000000000)

theorem Zeta5Irrational.U_520_9 : Uω (aρ 9) (bρ 9) (9287519810631 / 16000000000000) ≤ -(8316941009312002770807 / 10000000000000000000000)

theorem Zeta5Irrational.U_520_10 : Uω (aρ 10) (bρ 10) (9287519810631 / 16000000000000) ≤ -(4740976483772919301281 / 5000000000000000000000)

theorem Zeta5Irrational.U_520_11 : Uω (aρ 11) (bρ 11) (9287519810631 / 16000000000000) ≤ -(5545371965551789929277 / 5000000000000000000000)

theorem Zeta5Irrational.U_520_12 : Uω (aρ 12) (bρ 12) (9287519810631 / 16000000000000) ≤ -(1353380204255246507751 / 1000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_520 : Uρ (9287519810631 / 16000000000000) ≤ -(8876311486619942590457 / 10000000000000000000000)

theorem Zeta5Irrational.U_521_1 : Uω (aρ 1) (bρ 1) (4683703346333 / 8000000000000) ≤ -(218573932723313454971 / 400000000000000000000)

theorem Zeta5Irrational.U_521_2 : Uω (aρ 2) (bρ 2) (4683703346333 / 8000000000000) ≤ -(5505754567146598031943 / 10000000000000000000000)

theorem Zeta5Irrational.U_521_3 : Uω (aρ 3) (bρ 3) (4683703346333 / 8000000000000) ≤ -(698637552390495291897 / 1250000000000000000000)

theorem Zeta5Irrational.U_521_4 : Uω (aρ 4) (bρ 4) (4683703346333 / 8000000000000) ≤ -(5729125871667981875797 / 10000000000000000000000)

theorem Zeta5Irrational.U_521_5 : Uω (aρ 5) (bρ 5) (4683703346333 / 8000000000000) ≤ -(2973159163481224856561 / 5000000000000000000000)

theorem Zeta5Irrational.U_521_6 : Uω (aρ 6) (bρ 6) (4683703346333 / 8000000000000) ≤ -(7833195515449707049 / 12500000000000000000)

theorem Zeta5Irrational.U_521_7 : Uω (aρ 7) (bρ 7) (4683703346333 / 8000000000000) ≤ -(6721324909858084649313 / 10000000000000000000000)

theorem Zeta5Irrational.U_521_8 : Uω (aρ 8) (bρ 8) (4683703346333 / 8000000000000) ≤ -(1469839420203114228919 / 2000000000000000000000)

theorem Zeta5Irrational.U_521_9 : Uω (aρ 9) (bρ 9) (4683703346333 / 8000000000000) ≤ -(6406369439884059803 / 7812500000000000000)

theorem Zeta5Irrational.U_521_10 : Uω (aρ 10) (bρ 10) (4683703346333 / 8000000000000) ≤ -(9347289623404676103549 / 10000000000000000000000)

theorem Zeta5Irrational.U_521_11 : Uω (aρ 11) (bρ 11) (4683703346333 / 8000000000000) ≤ -(2730769626571057740701 / 2500000000000000000000)

theorem Zeta5Irrational.U_521_12 : Uω (aρ 12) (bρ 12) (4683703346333 / 8000000000000) ≤ -(6640928384740651911177 / 5000000000000000000000)

theorem Zeta5Irrational.U_521_13 : Uω (aρ 13) (bρ 13) (4683703346333 / 8000000000000) ≤ -(4762195995179309567439 / 2500000000000000000000)

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

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

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

theorem Zeta5Irrational.U_521 : Uρ (4683703346333 / 8000000000000) ≤ -(877967859898227552371 / 1000000000000000000000)

theorem Zeta5Irrational.U_522_1 : Uω (aρ 1) (bρ 1) (9447293574701 / 16000000000000) ≤ -(2689242726636831311537 / 5000000000000000000000)

theorem Zeta5Irrational.U_522_2 : Uω (aρ 2) (bρ 2) (9447293574701 / 16000000000000) ≤ -(2709767332690208033799 / 5000000000000000000000)

theorem Zeta5Irrational.U_522_3 : Uω (aρ 3) (bρ 3) (9447293574701 / 16000000000000) ≤ -(275107753260969971343 / 500000000000000000000)

theorem Zeta5Irrational.U_522_4 : Uω (aρ 4) (bρ 4) (9447293574701 / 16000000000000) ≤ -(5640940935750156606193 / 10000000000000000000000)

theorem Zeta5Irrational.U_522_5 : Uω (aρ 5) (bρ 5) (9447293574701 / 16000000000000) ≤ -(292807872430797669627 / 500000000000000000000)

theorem Zeta5Irrational.U_522_6 : Uω (aρ 6) (bρ 6) (9447293574701 / 16000000000000) ≤ -(3086678972250842838001 / 5000000000000000000000)

theorem Zeta5Irrational.U_522_7 : Uω (aρ 7) (bρ 7) (9447293574701 / 16000000000000) ≤ -(1655884651729656945347 / 2500000000000000000000)

theorem Zeta5Irrational.U_522_8 : Uω (aρ 8) (bρ 8) (9447293574701 / 16000000000000) ≤ -(3622243194618693881327 / 5000000000000000000000)

theorem Zeta5Irrational.U_522_9 : Uω (aρ 9) (bρ 9) (9447293574701 / 16000000000000) ≤ -(1616955332102858313771 / 2000000000000000000000)

theorem Zeta5Irrational.U_522_10 : Uω (aρ 10) (bρ 10) (9447293574701 / 16000000000000) ≤ -(9214596541511311802389 / 10000000000000000000000)

theorem Zeta5Irrational.U_522_11 : Uω (aρ 11) (bρ 11) (9447293574701 / 16000000000000) ≤ -(10758800567764580269163 / 10000000000000000000000)

theorem Zeta5Irrational.U_522_12 : Uω (aρ 12) (bρ 12) (9447293574701 / 16000000000000) ≤ -(1629974352488310309933 / 1250000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_522 : Uρ (9447293574701 / 16000000000000) ≤ -(108558985643967623763 / 125000000000000000000)

theorem Zeta5Irrational.U_523_1 : Uω (aρ 1) (bρ 1) (297724389273 / 500000000000) ≤ -(1323338391653748969901 / 2500000000000000000000)

theorem Zeta5Irrational.U_523_2 : Uω (aρ 2) (bρ 2) (297724389273 / 500000000000) ≤ -(2667025923201519139487 / 5000000000000000000000)

theorem Zeta5Irrational.U_523_3 : Uω (aρ 3) (bρ 3) (297724389273 / 500000000000) ≤ -(5415959314664550473199 / 10000000000000000000000)

theorem Zeta5Irrational.U_523_4 : Uω (aρ 4) (bρ 4) (297724389273 / 500000000000) ≤ -(694190920277763514999 / 1250000000000000000000)

theorem Zeta5Irrational.U_523_5 : Uω (aρ 5) (bρ 5) (297724389273 / 500000000000) ≤ -(1441700895845914328219 / 2500000000000000000000)

theorem Zeta5Irrational.U_523_6 : Uω (aρ 6) (bρ 6) (297724389273 / 500000000000) ≤ -(1216204732437666014063 / 2000000000000000000000)

theorem Zeta5Irrational.U_523_7 : Uω (aρ 7) (bρ 7) (297724389273 / 500000000000) ≤ -(326335422999999054939 / 500000000000000000000)

theorem Zeta5Irrational.U_523_8 : Uω (aρ 8) (bρ 8) (297724389273 / 500000000000) ≤ -(7140884075452489921343 / 10000000000000000000000)

theorem Zeta5Irrational.U_523_9 : Uω (aρ 9) (bρ 9) (297724389273 / 500000000000) ≤ -(3985388580009479571857 / 5000000000000000000000)

theorem Zeta5Irrational.U_523_10 : Uω (aρ 10) (bρ 10) (297724389273 / 500000000000) ≤ -(9083812071916347774149 / 10000000000000000000000)

theorem Zeta5Irrational.U_523_11 : Uω (aρ 11) (bρ 11) (297724389273 / 500000000000) ≤ -(10597754534486675358283 / 10000000000000000000000)

theorem Zeta5Irrational.U_523_12 : Uω (aρ 12) (bρ 12) (297724389273 / 500000000000) ≤ -(12806664000284943041083 / 10000000000000000000000)

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

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

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

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

theorem Zeta5Irrational.U_523 : Uρ (297724389273 / 500000000000) ≤ -(8591336616545901455247 / 10000000000000000000000)

theorem Zeta5Irrational.U_524_1 : Uω (aρ 1) (bρ 1) (19123153518409 / 32000000000000) ≤ -(1314230248183163826137 / 2500000000000000000000)

theorem Zeta5Irrational.U_524_2 : Uω (aρ 2) (bρ 2) (19123153518409 / 32000000000000) ≤ -(5297470015337856711679 / 10000000000000000000000)

theorem Zeta5Irrational.U_524_3 : Uω (aρ 3) (bρ 3) (19123153518409 / 32000000000000) ≤ -(107581485947053385999 / 200000000000000000000)

theorem Zeta5Irrational.U_524_4 : Uω (aρ 4) (bρ 4) (19123153518409 / 32000000000000) ≤ -(5516124554661589611093 / 10000000000000000000000)

theorem Zeta5Irrational.U_524_5 : Uω (aρ 5) (bρ 5) (19123153518409 / 32000000000000) ≤ -(5728576098328493848859 / 10000000000000000000000)

theorem Zeta5Irrational.U_524_6 : Uω (aρ 6) (bρ 6) (19123153518409 / 32000000000000) ≤ -(6041530126911093500149 / 10000000000000000000000)

theorem Zeta5Irrational.U_524_7 : Uω (aρ 7) (bρ 7) (19123153518409 / 32000000000000) ≤ -(3242653404335615268931 / 5000000000000000000000)

theorem Zeta5Irrational.U_524_8 : Uω (aρ 8) (bρ 8) (19123153518409 / 32000000000000) ≤ -(7096612213048692962003 / 10000000000000000000000)

theorem Zeta5Irrational.U_524_9 : Uω (aρ 9) (bρ 9) (19123153518409 / 32000000000000) ≤ -(1584421749117207670283 / 2000000000000000000000)

theorem Zeta5Irrational.U_524_10 : Uω (aρ 10) (bρ 10) (19123153518409 / 32000000000000) ≤ -(72224593962241507771 / 80000000000000000000)

theorem Zeta5Irrational.U_524_11 : Uω (aρ 11) (bρ 11) (19123153518409 / 32000000000000) ≤ -(10529373141229537227421 / 10000000000000000000000)

theorem Zeta5Irrational.U_524_12 : Uω (aρ 12) (bρ 12) (19123153518409 / 32000000000000) ≤ -(2541766278107864221893 / 2000000000000000000000)

theorem Zeta5Irrational.U_524_13 : Uω (aρ 13) (bρ 13) (19123153518409 / 32000000000000) ≤ -(3569539676245047689691 / 2000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_524 : Uρ (19123153518409 / 32000000000000) ≤ -(530057725649425284243 / 625000000000000000000)

theorem Zeta5Irrational.U_525_1 : Uω (aρ 1) (bρ 1) (9595973061673 / 16000000000000) ≤ -(522062067163280364799 / 1000000000000000000000)

theorem Zeta5Irrational.U_525_2 : Uω (aρ 2) (bρ 2) (9595973061673 / 16000000000000) ≤ -(328813845489025310421 / 625000000000000000000)

theorem Zeta5Irrational.U_525_3 : Uω (aρ 3) (bρ 3) (9595973061673 / 16000000000000) ≤ -(5342324859967229659017 / 10000000000000000000000)

theorem Zeta5Irrational.U_525_4 : Uω (aρ 4) (bρ 4) (9595973061673 / 16000000000000) ≤ -(2739430605522132083087 / 5000000000000000000000)

theorem Zeta5Irrational.U_525_5 : Uω (aρ 5) (bρ 5) (9595973061673 / 16000000000000) ≤ -(5690494434089613539713 / 10000000000000000000000)

theorem Zeta5Irrational.U_525_6 : Uω (aρ 6) (bρ 6) (9595973061673 / 16000000000000) ≤ -(3001096294645691980019 / 5000000000000000000000)

theorem Zeta5Irrational.U_525_7 : Uω (aρ 7) (bρ 7) (9595973061673 / 16000000000000) ≤ -(3222038740598697037627 / 5000000000000000000000)

theorem Zeta5Irrational.U_525_8 : Uω (aρ 8) (bρ 8) (9595973061673 / 16000000000000) ≤ -(1763134895300513255911 / 2500000000000000000000)

theorem Zeta5Irrational.U_525_9 : Uω (aρ 9) (bρ 9) (9595973061673 / 16000000000000) ≤ -(1574737327668269272281 / 2000000000000000000000)

theorem Zeta5Irrational.U_525_10 : Uω (aρ 10) (bρ 10) (9595973061673 / 16000000000000) ≤ -(8972674828002439749491 / 10000000000000000000000)

theorem Zeta5Irrational.U_525_11 : Uω (aρ 11) (bρ 11) (9595973061673 / 16000000000000) ≤ -(52307765738945663703 / 50000000000000000000)

theorem Zeta5Irrational.U_525_12 : Uω (aρ 12) (bρ 12) (9595973061673 / 16000000000000) ≤ -(12612446007478394770303 / 10000000000000000000000)

theorem Zeta5Irrational.U_525_13 : Uω (aρ 13) (bρ 13) (9595973061673 / 16000000000000) ≤ -(17351210317533614871703 / 10000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_525 : Uρ (9595973061673 / 16000000000000) ≤ -(1682447810411330092499 / 2000000000000000000000)

theorem Zeta5Irrational.U_526_1 : Uω (aρ 1) (bρ 1) (19260738728283 / 32000000000000) ≤ -(1296112911651224119971 / 2500000000000000000000)

theorem Zeta5Irrational.U_526_2 : Uω (aρ 2) (bρ 2) (19260738728283 / 32000000000000) ≤ -(5224705415238725644339 / 10000000000000000000000)

theorem Zeta5Irrational.U_526_3 : Uω (aρ 3) (bρ 3) (19260738728283 / 32000000000000) ≤ -(1326427502307451136827 / 2500000000000000000000)

theorem Zeta5Irrational.U_526_4 : Uω (aρ 4) (bρ 4) (19260738728283 / 32000000000000) ≤ -(5441736294544028744673 / 10000000000000000000000)

theorem Zeta5Irrational.U_526_5 : Uω (aρ 5) (bρ 5) (19260738728283 / 32000000000000) ≤ -(113051149611568404339 / 200000000000000000000)

theorem Zeta5Irrational.U_526_6 : Uω (aρ 6) (bρ 6) (19260738728283 / 32000000000000) ≤ -(1192601963369088836747 / 2000000000000000000000)

theorem Zeta5Irrational.U_526_7 : Uω (aρ 7) (bρ 7) (19260738728283 / 32000000000000) ≤ -(6403019035753007704611 / 10000000000000000000000)

theorem Zeta5Irrational.U_526_8 : Uω (aρ 8) (bρ 8) (19260738728283 / 32000000000000) ≤ -(1752166089705982821403 / 2500000000000000000000)

theorem Zeta5Irrational.U_526_9 : Uω (aρ 9) (bρ 9) (19260738728283 / 32000000000000) ≤ -(1565101650889641952791 / 2000000000000000000000)

theorem Zeta5Irrational.U_526_10 : Uω (aρ 10) (bρ 10) (19260738728283 / 32000000000000) ≤ -(2229402349962983556549 / 2500000000000000000000)

theorem Zeta5Irrational.U_526_11 : Uω (aρ 11) (bρ 11) (19260738728283 / 32000000000000) ≤ -(5197141997269709507939 / 5000000000000000000000)

theorem Zeta5Irrational.U_526_12 : Uω (aρ 12) (bρ 12) (19260738728283 / 32000000000000) ≤ -(12517454039065267076341 / 10000000000000000000000)

theorem Zeta5Irrational.U_526_13 : Uω (aρ 13) (bρ 13) (19260738728283 / 32000000000000) ≤ -(16970931968603725312893 / 10000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_526 : Uρ (19260738728283 / 32000000000000) ≤ -(1670131396109797597861 / 2000000000000000000000)

theorem Zeta5Irrational.U_527_1 : Uω (aρ 1) (bρ 1) (38590270061503 / 64000000000000) ≤ -(645802009247295681979 / 1250000000000000000000)

theorem Zeta5Irrational.U_527_2 : Uω (aρ 2) (bρ 2) (38590270061503 / 64000000000000) ≤ -(1301649174932163817053 / 2500000000000000000000)

theorem Zeta5Irrational.U_527_3 : Uω (aρ 3) (bρ 3) (38590270061503 / 64000000000000) ≤ -(660931593304168506057 / 1250000000000000000000)

theorem Zeta5Irrational.U_527_4 : Uω (aρ 4) (bρ 4) (38590270061503 / 64000000000000) ≤ -(1355806356402784096183 / 2500000000000000000000)

theorem Zeta5Irrational.U_527_5 : Uω (aρ 5) (bρ 5) (38590270061503 / 64000000000000) ≤ -(352102682931682360927 / 625000000000000000000)

theorem Zeta5Irrational.U_527_6 : Uω (aρ 6) (bρ 6) (38590270061503 / 64000000000000) ≤ -(46433406925091649199 / 78125000000000000000)

theorem Zeta5Irrational.U_527_7 : Uω (aρ 7) (bρ 7) (38590270061503 / 64000000000000) ≤ -(6382553448201340794523 / 10000000000000000000000)

theorem Zeta5Irrational.U_527_8 : Uω (aρ 8) (bρ 8) (38590270061503 / 64000000000000) ≤ -(3493400107016278783557 / 5000000000000000000000)

theorem Zeta5Irrational.U_527_9 : Uω (aρ 9) (bρ 9) (38590270061503 / 64000000000000) ≤ -(7801509662796789883127 / 10000000000000000000000)

theorem Zeta5Irrational.U_527_10 : Uω (aρ 10) (bρ 10) (38590270061503 / 64000000000000) ≤ -(4445100287735114038913 / 5000000000000000000000)

theorem Zeta5Irrational.U_527_11 : Uω (aρ 11) (bρ 11) (38590270061503 / 64000000000000) ≤ -(10360852771929530826219 / 10000000000000000000000)

theorem Zeta5Irrational.U_527_12 : Uω (aρ 12) (bρ 12) (38590270061503 / 64000000000000) ≤ -(2494092935186941707943 / 2000000000000000000000)

theorem Zeta5Irrational.U_527_13 : Uω (aρ 13) (bρ 13) (38590270061503 / 64000000000000) ≤ -(16805116772664291941307 / 10000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_527 : Uρ (38590270061503 / 64000000000000) ≤ -(832139470866167297877 / 1000000000000000000000)

theorem Zeta5Irrational.U_528_1 : Uω (aρ 1) (bρ 1) (966476566661 / 1600000000000) ≤ -(2574206485641140088087 / 5000000000000000000000)

theorem Zeta5Irrational.U_528_2 : Uω (aρ 2) (bρ 2) (966476566661 / 1600000000000) ≤ -(1297130179868403671289 / 2500000000000000000000)

theorem Zeta5Irrational.U_528_3 : Uω (aρ 3) (bρ 3) (966476566661 / 1600000000000) ≤ -(5269228762739811181977 / 10000000000000000000000)

theorem Zeta5Irrational.U_528_4 : Uω (aρ 4) (bρ 4) (966476566661 / 1600000000000) ≤ -(675593597482667857747 / 1250000000000000000000)

theorem Zeta5Irrational.U_528_5 : Uω (aρ 5) (bρ 5) (966476566661 / 1600000000000) ≤ -(5614764140355019561613 / 10000000000000000000000)

theorem Zeta5Irrational.U_528_6 : Uω (aρ 6) (bρ 6) (966476566661 / 1600000000000) ≤ -(5923980591695871839469 / 10000000000000000000000)

theorem Zeta5Irrational.U_528_7 : Uω (aρ 7) (bρ 7) (966476566661 / 1600000000000) ≤ -(159053251217352304367 / 250000000000000000000)

theorem Zeta5Irrational.U_528_8 : Uω (aρ 8) (bρ 8) (966476566661 / 1600000000000) ≤ -(6964984750148177349421 / 10000000000000000000000)

theorem Zeta5Irrational.U_528_9 : Uω (aρ 9) (bρ 9) (966476566661 / 1600000000000) ≤ -(7777571051986987253239 / 10000000000000000000000)

theorem Zeta5Irrational.U_528_10 : Uω (aρ 10) (bρ 10) (966476566661 / 1600000000000) ≤ -(4431436816050858759941 / 5000000000000000000000)

theorem Zeta5Irrational.U_528_11 : Uω (aρ 11) (bρ 11) (966476566661 / 1600000000000) ≤ -(5163777722653102252189 / 5000000000000000000000)

theorem Zeta5Irrational.U_528_12 : Uω (aρ 12) (bρ 12) (966476566661 / 1600000000000) ≤ -(2484760992263260070481 / 2000000000000000000000)

theorem Zeta5Irrational.U_528_13 : Uω (aρ 13) (bρ 13) (966476566661 / 1600000000000) ≤ -(260170584264644178209 / 156250000000000000000)

theorem Zeta5Irrational.U_528_14 : Uω (aρ 14) (bρ 14) (966476566661 / 1600000000000) ≤ -(8977612329965299982791 / 5000000000000000000000)

theorem Zeta5Irrational.U_528_15 : Uω (aρ 15) (bρ 15) (966476566661 / 1600000000000) ≤ -(268788866070650094343 / 156250000000000000000)

theorem Zeta5Irrational.U_528_16 : Uω (aρ 16) (bρ 16) (966476566661 / 1600000000000) ≤ -(419641552645073499393 / 250000000000000000000)

theorem Zeta5Irrational.U_528 : Uρ (966476566661 / 1600000000000) ≤ -(518305002869011146653 / 625000000000000000000)

theorem Zeta5Irrational.U_529_1 : Uω (aρ 1) (bρ 1) (38727855271377 / 64000000000000) ≤ -(5130442221812664608347 / 10000000000000000000000)

theorem Zeta5Irrational.U_529_2 : Uω (aρ 2) (bρ 2) (38727855271377 / 64000000000000) ≤ -(5170477356328555880841 / 10000000000000000000000)

theorem Zeta5Irrational.U_529_3 : Uω (aρ 3) (bρ 3) (38727855271377 / 64000000000000) ≤ -(5251037937022816384007 / 10000000000000000000000)

theorem Zeta5Irrational.U_529_4 : Uω (aρ 4) (bρ 4) (38727855271377 / 64000000000000) ≤ -(5386306230905287627101 / 10000000000000000000000)

theorem Zeta5Irrational.U_529_5 : Uω (aρ 5) (bρ 5) (38727855271377 / 64000000000000) ≤ -(5595920985687641589971 / 10000000000000000000000)

theorem Zeta5Irrational.U_529_6 : Uω (aρ 6) (bρ 6) (38727855271377 / 64000000000000) ≤ -(738065397838446361183 / 1250000000000000000000)

theorem Zeta5Irrational.U_529_7 : Uω (aρ 7) (bρ 7) (38727855271377 / 64000000000000) ≤ -(792718582758281840787 / 1250000000000000000000)

theorem Zeta5Irrational.U_529_8 : Uω (aρ 8) (bρ 8) (38727855271377 / 64000000000000) ≤ -(6943217746578683048433 / 10000000000000000000000)

theorem Zeta5Irrational.U_529_9 : Uω (aρ 9) (bρ 9) (38727855271377 / 64000000000000) ≤ -(7753692110675952395933 / 10000000000000000000000)

theorem Zeta5Irrational.U_529_10 : Uω (aρ 10) (bρ 10) (38727855271377 / 64000000000000) ≤ -(4417814021261383902239 / 5000000000000000000000)

theorem Zeta5Irrational.U_529_11 : Uω (aρ 11) (bρ 11) (38727855271377 / 64000000000000) ≤ -(10294390783422403344033 / 10000000000000000000000)

theorem Zeta5Irrational.U_529_12 : Uω (aρ 12) (bρ 12) (38727855271377 / 64000000000000) ≤ -(12377469048134864274801 / 10000000000000000000000)

theorem Zeta5Irrational.U_529_13 : Uω (aρ 13) (bρ 13) (38727855271377 / 64000000000000) ≤ -(8253109536821764390211 / 5000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_529 : Uρ (38727855271377 / 64000000000000) ≤ -(8264987908352755707917 / 10000000000000000000000)

theorem Zeta5Irrational.U_530_1 : Uω (aρ 1) (bρ 1) (19398323938157 / 32000000000000) ≤ -(102250074189872219547 / 200000000000000000000)

theorem Zeta5Irrational.U_530_2 : Uω (aρ 2) (bρ 2) (19398323938157 / 32000000000000) ≤ -(1288116623196728951863 / 2500000000000000000000)

theorem Zeta5Irrational.U_530_3 : Uω (aρ 3) (bρ 3) (19398323938157 / 32000000000000) ≤ -(1308220037204054730923 / 2500000000000000000000)

theorem Zeta5Irrational.U_530_4 : Uω (aρ 4) (bρ 4) (19398323938157 / 32000000000000) ≤ -(670987206631612576549 / 1250000000000000000000)

theorem Zeta5Irrational.U_530_5 : Uω (aρ 5) (bρ 5) (19398323938157 / 32000000000000) ≤ -(5577113328436471908801 / 10000000000000000000000)

theorem Zeta5Irrational.U_530_6 : Uω (aρ 6) (bρ 6) (19398323938157 / 32000000000000) ≤ -(5885103710340832165453 / 10000000000000000000000)

theorem Zeta5Irrational.U_530_7 : Uω (aρ 7) (bρ 7) (19398323938157 / 32000000000000) ≤ -(1264281822850228723667 / 2000000000000000000000)

theorem Zeta5Irrational.U_530_8 : Uω (aρ 8) (bρ 8) (19398323938157 / 32000000000000) ≤ -(6921498986855282207523 / 10000000000000000000000)

theorem Zeta5Irrational.U_530_9 : Uω (aρ 9) (bρ 9) (19398323938157 / 32000000000000) ≤ -(1932468132506487573157 / 2500000000000000000000)

theorem Zeta5Irrational.U_530_10 : Uω (aρ 10) (bρ 10) (19398323938157 / 32000000000000) ≤ -(8808463284906202056157 / 10000000000000000000000)

theorem Zeta5Irrational.U_530_11 : Uω (aρ 11) (bρ 11) (19398323938157 / 32000000000000) ≤ -(513067878678141954839 / 500000000000000000000)

theorem Zeta5Irrational.U_530_12 : Uω (aρ 12) (bρ 12) (19398323938157 / 32000000000000) ≤ -(1541431407737169729987 / 1250000000000000000000)

theorem Zeta5Irrational.U_530_13 : Uω (aρ 13) (bρ 13) (19398323938157 / 32000000000000) ≤ -(16369481579601011001041 / 10000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_530 : Uρ (19398323938157 / 32000000000000) ≤ -(8237627031248805762037 / 10000000000000000000000)

theorem Zeta5Irrational.U_531_1 : Uω (aρ 1) (bρ 1) (38865440481251 / 64000000000000) ≤ -(1273649329718194240281 / 2500000000000000000000)

theorem Zeta5Irrational.U_531_2 : Uω (aρ 2) (bρ 2) (38865440481251 / 64000000000000) ≤ -(1026897602395204205191 / 2000000000000000000000)

theorem Zeta5Irrational.U_531_3 : Uω (aρ 3) (bρ 3) (38865440481251 / 64000000000000) ≤ -(5214755278309320413741 / 10000000000000000000000)

theorem Zeta5Irrational.U_531_4 : Uω (aρ 4) (bρ 4) (38865440481251 / 64000000000000) ≤ -(5349522921308249214813 / 10000000000000000000000)

theorem Zeta5Irrational.U_531_5 : Uω (aρ 5) (bρ 5) (38865440481251 / 64000000000000) ≤ -(5558341034894179748239 / 10000000000000000000000)

theorem Zeta5Irrational.U_531_6 : Uω (aρ 6) (bρ 6) (38865440481251 / 64000000000000) ≤ -(2932861013183497161807 / 5000000000000000000000)

theorem Zeta5Irrational.U_531_7 : Uω (aρ 7) (bρ 7) (38865440481251 / 64000000000000) ≤ -(6301111232271157612451 / 10000000000000000000000)

theorem Zeta5Irrational.U_531_8 : Uω (aρ 8) (bρ 8) (38865440481251 / 64000000000000) ≤ -(6899828248220443165641 / 10000000000000000000000)

theorem Zeta5Irrational.U_531_9 : Uω (aρ 9) (bρ 9) (38865440481251 / 64000000000000) ≤ -(1926528000919187657291 / 2500000000000000000000)

theorem Zeta5Irrational.U_531_10 : Uω (aρ 10) (bρ 10) (38865440481251 / 64000000000000) ≤ -(8781378842744531549129 / 10000000000000000000000)

theorem Zeta5Irrational.U_531_11 : Uω (aρ 11) (bρ 11) (38865440481251 / 64000000000000) ≤ -(1278556827644119619991 / 1250000000000000000000)

theorem Zeta5Irrational.U_531_12 : Uω (aρ 12) (bρ 12) (38865440481251 / 64000000000000) ≤ -(6142873046797036347843 / 5000000000000000000000)

theorem Zeta5Irrational.U_531_13 : Uω (aρ 13) (bρ 13) (38865440481251 / 64000000000000) ≤ -(16239541782885318070361 / 10000000000000000000000)

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

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

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

theorem Zeta5Irrational.U_531 : Uρ (38865440481251 / 64000000000000) ≤ -(1642145670387592022313 / 2000000000000000000000)