V22: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_265 : 501012873635738876091 / 2500000000000000000000 - 6 * (3 / 40) * -(7402526123330008104227 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4710601968739139 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2201144530125916720343 / 5000000000000000000000) - 6 * (789450375468092547361 / 5000000000000000000000))) ≤ Vfield (14201453381049 / 64000000000000)

theorem Zeta5Irrational.V_266 : 1004206824111706414963 / 5000000000000000000000 - 6 * (3 / 40) * -(14781647848946051308547 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4716257371140541 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 4406916427345624348069 / 10000000000000000000000) - 6 * (39425967473124423959 / 250000000000000000000))) ≤ Vfield (1779446687267 / 8000000000000)

theorem Zeta5Irrational.V_267 : 125798368743440768183 / 625000000000000000000 - 6 * (3 / 40) * -(7379149049969101912307 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4721906000100587 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2205768118518581484771 / 5000000000000000000000) - 6 * (1575183219723586415793 / 10000000000000000000000))) ≤ Vfield (14269693615223 / 64000000000000)

theorem Zeta5Irrational.V_268 : 2017132251215798468539 / 10000000000000000000000 - 6 * (3 / 40) * -(92093767156400260889 / 62500000000000000000) - 2 + 12 * (3 / 40) + 2 * (945509575979733 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2208074257881297602699 / 5000000000000000000000) - 6 * (314666854950398720743 / 2000000000000000000000))) ≤ Vfield (1430381373231 / 6400000000000)

theorem Zeta5Irrational.V_269 : 1010744351920704571427 / 5000000000000000000000 - 6 * (3 / 40) * -(3677940382841596508797 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (236659151733473 / 500000000000000 * (Real.pi + (Real.pi / 2 - 2210376644902636965323 / 5000000000000000000000) - 6 * (785745912873242323847 / 5000000000000000000000))) ≤ Vfield (14337933849397 / 64000000000000)

theorem Zeta5Irrational.V_270 : 506460814856369766769 / 2500000000000000000000 - 6 * (3 / 40) * -(7344287103943422644799 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2369405744202079 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 4425350585297006953787 / 10000000000000000000000) - 6 * (9810348967227032483 / 62500000000000000000))) ≤ Vfield (3593013491621 / 16000000000000)

theorem Zeta5Irrational.V_271 : 2030195919619443733491 / 10000000000000000000000 - 6 * (3 / 40) * -(14665440525249540781007 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4744433264951639 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 4429940428219294879569 / 10000000000000000000000) - 6 * (1567826264140476018089 / 10000000000000000000000))) ≤ Vfield (14406174083571 / 64000000000000)

theorem Zeta5Irrational.V_272 : 1017273343036291565619 / 5000000000000000000000 - 6 * (3 / 40) * -(58569440943380077467 / 40000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2375024194009827 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 4434522844404553221673 / 10000000000000000000000) - 6 * (1566003076564351681379 / 10000000000000000000000))) ≤ Vfield (7220147100329 / 32000000000000)

theorem Zeta5Irrational.V_273 : 407779112086405099183 / 2000000000000000000000 - 6 * (3 / 40) * -(14619333093774351598831 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (475565688117599 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 4439097859537322069829 / 10000000000000000000000) - 6 * (1564186234996620458847 / 10000000000000000000000))) ≤ Vfield (2894882863549 / 12800000000000)

theorem Zeta5Irrational.V_274 : 2043242544342751051039 / 10000000000000000000000 - 6 * (3 / 40) * -(7298179427416706252041 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4761258767849631 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 4443665499155469865247 / 10000000000000000000000) - 6 * (390593925676510568093 / 2500000000000000000000))) ≤ Vfield (906783402177 / 4000000000000)

theorem Zeta5Irrational.V_275 : 1023793819723797870683 / 5000000000000000000000 - 6 * (3 / 40) * -(3643359319124335629843 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4766854071331891 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 88964515773027434811 / 200000000000000000000) - 6 * (390142860814587977897 / 2500000000000000000000))) ≤ Vfield (14542654551919 / 64000000000000)

theorem Zeta5Irrational.V_276 : 2051930847387254958117 / 10000000000000000000000 - 6 * (3 / 40) * -(14550568117905186109883 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (95448856295551 / 200000000000000 * (Real.pi + (Real.pi / 2 - 2226389376636543872639 / 5000000000000000000000) - 6 * (1558773420513176924499 / 10000000000000000000000))) ≤ Vfield (7288387334503 / 32000000000000)