V39: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_469 : 841431502833399730677 / 2000000000000000000000 - 6 * (3 / 40) * -(6373789591157519530799 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (904028563312041 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1565355854444793571363 / 5000000000000000000000)) - 6 * (258332775384579108939 / 2500000000000000000000))) ≤ Vfield (16737641334457 / 32000000000000)

theorem Zeta5Irrational.V_470 : 1053837440410898379117 / 2500000000000000000000 - 6 * (3 / 40) * -(6350206894233353416501 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7240853017660129 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3133541876096710658859 / 10000000000000000000000)) - 6 * (1032109037888209828613 / 10000000000000000000000))) ≤ Vfield (33555169550949 / 64000000000000)

theorem Zeta5Irrational.V_471 : 422353530332149810381 / 1000000000000000000000 - 6 * (3 / 40) * -(6326679680849111885173 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3624733634232227 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (784091590609151552069 / 2500000000000000000000)) - 6 * (1030891299853228078583 / 10000000000000000000000))) ≤ Vfield (4204382054123 / 8000000000000)

theorem Zeta5Irrational.V_472 : 846342830033970747269 / 2000000000000000000000 - 6 * (3 / 40) * -(393950480658920792153 / 625000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3629035647720933 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3139185189170562755643 / 10000000000000000000000)) - 6 * (1029677861974945545847 / 10000000000000000000000))) ≤ Vfield (33714943315019 / 64000000000000)

theorem Zeta5Irrational.V_473 : 33919090505047273979 / 80000000000000000000 - 6 * (3 / 40) * -(6279790664681930096523 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7266665134908643 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1570999188718471372011 / 5000000000000000000000)) - 6 * (102846869900421664989 / 1000000000000000000000))) ≤ Vfield (16897415098527 / 32000000000000)

theorem Zeta5Irrational.V_474 : 531006475390013602341 / 1250000000000000000000 - 6 * (3 / 40) * -(782053543305886984727 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (291009952918663 / 400000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3144805948252172401271 / 10000000000000000000000)) - 6 * (1027263785898967908693 / 10000000000000000000000))) ≤ Vfield (33874717079089 / 64000000000000)

theorem Zeta5Irrational.V_475 : 425621063102617945859 / 1000000000000000000000 - 6 * (3 / 40) * -(1246624096162879854307 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (910477799438091 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (629521584502343043317 / 2000000000000000000000)) - 6 * (513031548911010165729 / 5000000000000000000000))) ≤ Vfield (8488650990281 / 16000000000000)

theorem Zeta5Irrational.V_476 : 4264362807711218122773 / 10000000000000000000000 - 6 * (3 / 40) * -(776233351817385457859 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3646192944100597 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (157520216049551920661 / 500000000000000000000)) - 6 * (512433305069469542579 / 5000000000000000000000))) ≤ Vfield (34034490843159 / 64000000000000)

theorem Zeta5Irrational.V_477 : 2136254172005389240579 / 5000000000000000000000 - 6 * (3 / 40) * -(6186667096138956931663 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7300939336524829 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3153195164346571015303 / 10000000000000000000000)) - 6 * (1023674298415909778301 / 10000000000000000000000))) ≤ Vfield (17057188862597 / 32000000000000)

theorem Zeta5Irrational.V_478 : 4280647250733957331043 / 10000000000000000000000 - 6 * (3 / 40) * -(770440134484759110209 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (11421066837089 / 15625000000000 * (Real.pi + (Real.pi / 2 - 2 * (3155980473116647307711 / 10000000000000000000000)) - 6 * (127810767302205454203 / 1250000000000000000000))) ≤ Vfield (34194264607229 / 64000000000000)

theorem Zeta5Irrational.V_479 : 4284714221375033324851 / 10000000000000000000000 - 6 * (3 / 40) * -(6151968124980879444211 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7313750752889049 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (631474211683661753521 / 2000000000000000000000)) - 6 * (1021893607795543436653 / 10000000000000000000000))) ≤ Vfield (68468416096493 / 128000000000000)

theorem Zeta5Irrational.V_480 : 4288779538663480659127 / 10000000000000000000000 - 6 * (3 / 40) * -(383776781609412568073 / 625000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3659008120446543 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1579380133861223043083 / 5000000000000000000000)) - 6 * (127662763263163460067 / 1250000000000000000000))) ≤ Vfield (2142134468079 / 4000000000000)