V53: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_637 : 1381932097217859613867 / 2500000000000000000000 - 6 * (3 / 40) * -(370162538946138480059 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2147768782037017 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (443598587162207701421 / 1250000000000000000000)) - 6 * (217697824813350455459 / 2500000000000000000000))) ≤ Vfield (4723620598879 / 6400000000000)

theorem Zeta5Irrational.V_638 : 691650816020377922461 / 1250000000000000000000 - 6 * (3 / 40) * -(147425107002328637843 / 500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8596616287992327 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3550382320117678762279 / 10000000000000000000000)) - 6 * (870232839768089163139 / 10000000000000000000000))) ≤ Vfield (2956072464119 / 4000000000000)

theorem Zeta5Irrational.V_639 : 1384670417024153405141 / 2500000000000000000000 - 6 * (3 / 40) * -(36696504086374459829 / 125000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8602153878446119 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3551974044421646939057 / 10000000000000000000000)) - 6 * (21741886334314884711 / 250000000000000000000))) ≤ Vfield (23679056431509 / 32000000000000)

theorem Zeta5Irrational.V_640 : 1108830762390958605563 / 2000000000000000000000 - 6 * (3 / 40) * -(2922954830394664874721 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8607687906398339 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3553563874266416429189 / 10000000000000000000000)) - 6 * (434559568317348828441 / 5000000000000000000000))) ≤ Vfield (11854766575033 / 16000000000000)

theorem Zeta5Irrational.V_641 : 2774811481507379783337 / 5000000000000000000000 - 6 * (3 / 40) * -(2910205608895841854953 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4306609189357877 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1777575906847914134599 / 5000000000000000000000)) - 6 * (868563886137522201071 / 10000000000000000000000))) ≤ Vfield (23740009868623 / 32000000000000)

theorem Zeta5Irrational.V_642 : 5555089124548337093933 / 10000000000000000000000 - 6 * (3 / 40) * -(2897472620967558860071 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4309372651121549 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (355673786674076914369 / 1000000000000000000000)) - 6 * (217002424619864156391 / 2500000000000000000000))) ≤ Vfield (1188524329359 / 1600000000000)

theorem Zeta5Irrational.V_643 : 222422091992879484073 / 400000000000000000000 - 6 * (3 / 40) * -(2884755825322004909539 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2156067170950793 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3558322037419228638997 / 10000000000000000000000)) - 6 * (216864142568515565517 / 2500000000000000000000))) ≤ Vfield (23800963305737 / 32000000000000)

theorem Zeta5Irrational.V_644 : 69575156151210255373 / 125000000000000000000 - 6 * (3 / 40) * -(718013795207170907293 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (539361783137309 / 625000000000000 * (Real.pi + (Real.pi / 2 - 2 * (889976082434089063109 / 2500000000000000000000)) - 6 * (866904498149987081409 / 10000000000000000000000))) ≤ Vfield (11915720012147 / 16000000000000)

theorem Zeta5Irrational.V_645 : 5576923940667797187807 / 10000000000000000000000 - 6 * (3 / 40) * -(2846702181558542557229 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8640817644580863 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3563063295243344731693 / 10000000000000000000000)) - 6 * (865803508735303275437 / 10000000000000000000000))) ≤ Vfield (746637295669 / 1000000000000)

theorem Zeta5Irrational.V_646 : 1395982290881571788087 / 2500000000000000000000 - 6 * (3 / 40) * -(283044465619030769971 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8647897332212889 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (356508924778024978169 / 1000000000000000000000)) - 6 * (865098242589412292353 / 10000000000000000000000))) ≤ Vfield (765809953469387 / 1024000000000000)

theorem Zeta5Irrational.V_647 : 2795464741252561992059 / 5000000000000000000000 - 6 * (3 / 40) * -(1407106759320460963231 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4327485614363427 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (356711212603540415007 / 1000000000000000000000)) - 6 * (432197348567961835751 / 5000000000000000000000))) ≤ Vfield (383531658086859 / 512000000000000)

theorem Zeta5Irrational.V_648 : 5597924904465249726207 / 10000000000000000000000 - 6 * (3 / 40) * -(1399004341694148145729 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1082754918538849 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1784565969182207295463 / 5000000000000000000000)) - 6 * (431846432694659931273 / 5000000000000000000000))) ≤ Vfield (768316678878049 / 1024000000000000)