V40: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_481 : 536605400492879213153 / 1250000000000000000000 - 6 * (3 / 40) * -(306445109372711187137 / 500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7322279244099123 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3160148103563553089317 / 10000000000000000000000)) - 6 * (10207116303724433279 / 100000000000000000000))) ≤ Vfield (68628189860563 / 128000000000000)

theorem Zeta5Irrational.V_482 : 537113152319473669229 / 1250000000000000000000 - 6 * (3 / 40) * -(122347782789297651323 / 200000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1465307953368911 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3161534568468916080673 / 10000000000000000000000)) - 6 * (1020122177634482114133 / 10000000000000000000000))) ≤ Vfield (34354038371299 / 64000000000000)

theorem Zeta5Irrational.V_483 : 4300965583842209674487 / 10000000000000000000000 - 6 * (3 / 40) * -(6105889331261373677087 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (293231912538167 / 400000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1581459832479321819787 / 5000000000000000000000)) - 6 * (1019533744940917633747 / 10000000000000000000000))) ≤ Vfield (68787963624633 / 128000000000000)

theorem Zeta5Irrational.V_484 : 2152512150570562284839 / 5000000000000000000000 - 6 * (3 / 40) * -(6094402732427668675489 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7335053388240221 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (791075848886423354773 / 2500000000000000000000)) - 6 * (203789265870628778459 / 2000000000000000000000))) ≤ Vfield (17216962626667 / 32000000000000)

theorem Zeta5Irrational.V_485 : 4309081371789734423577 / 10000000000000000000000 - 6 * (3 / 40) * -(3041464656326215977173 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (229353327984451 / 312500000000000 * (Real.pi + (Real.pi / 2 - 2 * (3165685762735902141383 / 10000000000000000000000)) - 6 * (1018359927944392969983 / 10000000000000000000000))) ≤ Vfield (68947737388703 / 128000000000000)

theorem Zeta5Irrational.V_486 : 4313136797123612745393 / 10000000000000000000000 - 6 * (3 / 40) * -(3035734520864270388191 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3671778569764047 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (633413353805602304743 / 2000000000000000000000)) - 6 * (6361090861247965123 / 62500000000000000000))) ≤ Vfield (34513812135369 / 64000000000000)

theorem Zeta5Irrational.V_487 : 1079297644619177201843 / 2500000000000000000000 - 6 * (3 / 40) * -(6060021889552608097611 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7347805324592091 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (63368928338273947477 / 200000000000000000000)) - 6 * (127148769501964290459 / 1250000000000000000000))) ≤ Vfield (69107511152773 / 128000000000000)

theorem Zeta5Irrational.V_488 : 4321242717181350277451 / 10000000000000000000000 - 6 * (3 / 40) * -(1209717565224901623787 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7352051054956959 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (79245617721939937011 / 250000000000000000000)) - 6 * (1016606779700894286959 / 10000000000000000000000))) ≤ Vfield (8648424754351 / 16000000000000)

theorem Zeta5Irrational.V_489 : 270330825910515365411 / 625000000000000000000 - 6 * (3 / 40) * -(6037166821546904547073 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7356294334872931 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1585600823698669241149 / 5000000000000000000000)) - 6 * (508012202987596007037 / 5000000000000000000000))) ≤ Vfield (69267284916843 / 128000000000000)

theorem Zeta5Irrational.V_490 : 432934207196648785071 / 1000000000000000000000 - 6 * (3 / 40) * -(6025758846024781546297 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (736053516857799 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3172577234943563944481 / 10000000000000000000000)) - 6 * (203088606394024225601 / 2000000000000000000000))) ≤ Vfield (34673585899439 / 64000000000000)

theorem Zeta5Irrational.V_491 : 4333389290703554887527 / 10000000000000000000000 - 6 * (3 / 40) * -(1202872773972995472511 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7364773560297917 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (634790294795992208869 / 2000000000000000000000)) - 6 * (1014862654828672016827 / 10000000000000000000000))) ≤ Vfield (69427058680913 / 128000000000000)

theorem Zeta5Irrational.V_492 : 542179359013164303477 / 1250000000000000000000 - 6 * (3 / 40) * -(1200596372695144120349 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3684504757123171 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1587662183481644612061 / 5000000000000000000000)) - 6 * (25357081792631315167 / 250000000000000000000))) ≤ Vfield (17376736390737 / 32000000000000)