V01: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_13 : 2838708958444624399 / 10000000000000000000000 - 6 * (3 / 40) * -(51312936940985871685561 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (84248322090117 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 168480700868393777449 / 10000000000000000000000) - 6 * (Real.pi / 2 - 138120555504676214793 / 625000000000000000000))) ≤ Vfield (283911191 / 1000000000000)

theorem Zeta5Irrational.V_14 : 3400600750179924673 / 10000000000000000000000 - 6 * (3 / 40) * -(51218264559151743459197 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (36884571408653 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 46100488200992503859 / 2500000000000000000000) - 6 * (Real.pi / 2 - 37673974722398950663 / 156250000000000000000))) ≤ Vfield (170058951 / 500000000000)

theorem Zeta5Irrational.V_15 : 396246097145057287 / 1000000000000000000000 - 6 * (3 / 40) * -(25562240032020096608843 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (24884879099817 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 99526369538609389173 / 5000000000000000000000) - 6 * (Real.pi / 2 - 324319511825085218099 / 1250000000000000000000))) ≤ Vfield (396324613 / 1000000000000)

theorem Zeta5Irrational.V_16 : 2435712931404190679 / 5000000000000000000000 - 6 * (3 / 40) * -(25487292403074346048679 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (110369975480201 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 27588013595377272983 / 1250000000000000000000) - 6 * (Real.pi / 2 - 143118806689254327513 / 500000000000000000000))) ≤ Vfield (974522519 / 2000000000000)

theorem Zeta5Irrational.V_17 : 2890154069979049949 / 5000000000000000000000 - 6 * (3 / 40) * -(25413451632679054566369 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (30057182637849 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 120205566586796683229 / 5000000000000000000000) - 6 * (Real.pi / 2 - 3102561376671980779519 / 10000000000000000000000))) ≤ Vfield (289098953 / 500000000000)

theorem Zeta5Irrational.V_18 : 7296953385895796397 / 10000000000000000000000 - 6 * (3 / 40) * -(50585194098875661653047 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (270178021126813 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 54022462008273651983 / 2000000000000000000000) - 6 * (Real.pi / 2 - 691531386986268494069 / 2000000000000000000000))) ≤ Vfield (729961631 / 1000000000000)

theorem Zeta5Irrational.V_19 : 1611037951921033759 / 2000000000000000000000 - 6 * (3 / 40) * -(50466495663078367309339 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (283873826461689 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 283797610683746791347 / 10000000000000000000000) - 6 * (Real.pi / 2 - 3618342583696765969299 / 10000000000000000000000))) ≤ Vfield (1611686987 / 2000000000000)

theorem Zeta5Irrational.V_20 : 35253474581734419 / 40000000000000000000 - 6 * (3 / 40) * -(6293648705936709382501 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (148469302887837 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 74212844787754867117 / 2500000000000000000000) - 6 * (Real.pi / 2 - 3769825878752123006391 / 10000000000000000000000))) ≤ Vfield (220431339 / 250000000000)

theorem Zeta5Irrational.V_21 : 2528385230620046493 / 2500000000000000000000 - 6 * (3 / 40) * -(50151154605132541364319 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3180983626569 / 100000000000000 * (Real.pi + (Real.pi / 2 - 79497784202311396663 / 2500000000000000000000) - 6 * (Real.pi / 2 - 2005672468682107829937 / 5000000000000000000000))) ≤ Vfield (4047462733 / 4000000000000)

theorem Zeta5Irrational.V_22 : 5706772088353681693 / 5000000000000000000000 - 6 * (3 / 40) * -(24978482657227015538013 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (67587158854327 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 337807240776056924649 / 10000000000000000000000) - 6 * (Real.pi / 2 - 4233370302187970192887 / 10000000000000000000000))) ≤ Vfield (2284012021 / 2000000000000)

theorem Zeta5Irrational.V_23 : 6356689226027724381 / 5000000000000000000000 - 6 * (3 / 40) * -(12441618812709760022989 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (44583950618293 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 178260237063611828863 / 5000000000000000000000) - 6 * (Real.pi / 2 - 221953446107719388427 / 500000000000000000000))) ≤ Vfield (5088585351 / 4000000000000)

theorem Zeta5Irrational.V_24 : 350326094811190417 / 250000000000000000000 - 6 * (3 / 40) * -(49579546107330803619953 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (374471182469361 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 187148145473045818201 / 5000000000000000000000) - 6 * (Real.pi / 2 - 4630833778944860274891 / 10000000000000000000000))) ≤ Vfield (280457333 / 200000000000)