V27: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_325 : 2602736867247839204543 / 10000000000000000000000 - 6 * (3 / 40) * -(5971596284766294893433 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2726192802200519 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2495901233890856705717 / 10000000000000000000000)) - 6 * (683483096073199743303 / 5000000000000000000000))) ≤ Vfield (19026245618611 / 64000000000000)

theorem Zeta5Irrational.V_326 : 651854409488761182881 / 2500000000000000000000 - 6 * (3 / 40) * -(11923161429885025563023 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1364488135098277 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2498046341966979991561 / 10000000000000000000000)) - 6 * (1365589208491496565637 / 10000000000000000000000))) ≤ Vfield (1525209391779 / 5120000000000)

theorem Zeta5Irrational.V_327 : 2612096218725827974741 / 10000000000000000000000 - 6 * (3 / 40) * -(5951585167346387345697 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (27317569020361 / 50000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2500188261746333242647 / 10000000000000000000000)) - 6 * (341054094455857365227 / 2500000000000000000000))) ≤ Vfield (2387998646983 / 8000000000000)

theorem Zeta5Irrational.V_328 : 2616772611608389628563 / 10000000000000000000000 - 6 * (3 / 40) * -(11883219124168659191989 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1367267353185529 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2502327002872303514111 / 10000000000000000000000)) - 6 * (681423839653867688303 / 5000000000000000000000))) ≤ Vfield (38285721908981 / 128000000000000)

theorem Zeta5Irrational.V_329 : 262144681864805827297 / 1000000000000000000000 - 6 * (3 / 40) * -(11863307639479982018991 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1094923876723771 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1252231287470484669311 / 5000000000000000000000)) - 6 * (340370773063998395589 / 2500000000000000000000))) ≤ Vfield (19181732733117 / 64000000000000)

theorem Zeta5Irrational.V_330 : 525223768377459148197 / 2000000000000000000000 - 6 * (3 / 40) * -(11843435722740940104459 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1370040933457811 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1253297493750716190239 / 5000000000000000000000)) - 6 * (272024519224901943929 / 2000000000000000000000))) ≤ Vfield (38441209023487 / 128000000000000)

theorem Zeta5Irrational.V_331 : 2630788683365702473583 / 10000000000000000000000 - 6 * (3 / 40) * -(11823603217005112636329 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5485702480421547 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2508724250056138755739 / 10000000000000000000000)) - 6 * (135876617051301854297 / 1000000000000000000000))) ≤ Vfield (1925947629037 / 6400000000000)

theorem Zeta5Irrational.V_332 : 66003045729603764453 / 250000000000000000000 - 6 * (3 / 40) * -(736503488463111140191 / 625000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1099352646095163 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (314121670365840661703 / 1250000000000000000000)) - 6 * (678032724979199444369 / 5000000000000000000000))) ≤ Vfield (19337219847623 / 64000000000000)

theorem Zeta5Irrational.V_333 : 2649446272363180973399 / 10000000000000000000000 - 6 * (3 / 40) * -(2348932839525893305633 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5507801768411671 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1258604994325691642003 / 5000000000000000000000)) - 6 * (270676154042019708727 / 2000000000000000000000))) ≤ Vfield (4853740851219 / 16000000000000)

theorem Zeta5Irrational.V_334 : 166172626819820649641 / 625000000000000000000 - 6 * (3 / 40) * -(2926356785290338176897 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5518818227512711 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2521434201602609004749 / 10000000000000000000000)) - 6 * (1350711973100143615783 / 10000000000000000000000))) ≤ Vfield (19492706962129 / 64000000000000)

theorem Zeta5Irrational.V_335 : 533613823123012619069 / 2000000000000000000000 - 6 * (3 / 40) * -(729146464864790530219 / 625000000000000000000) - 2 + 12 * (3 / 40) + 2 * (345613296233431 / 625000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1262823037718319180193 / 5000000000000000000000)) - 6 * (337014725658869163649 / 2500000000000000000000))) ≤ Vfield (9785225259691 / 32000000000000)

theorem Zeta5Irrational.V_336 : 1338683773990469618213 / 5000000000000000000000 - 6 * (3 / 40) * -(2906852973399345608809 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (554078543572499 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1264922841551584207157 / 5000000000000000000000)) - 6 * (672710702479827681713 / 5000000000000000000000))) ≤ Vfield (3929638815327 / 12800000000000)