V21: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_253 : 243944585903856897783 / 1250000000000000000000 - 6 * (3 / 40) * -(3018052558963085022733 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (580274971356627 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 4346161340798394868929 / 10000000000000000000000) - 6 * (100110784012609814337 / 625000000000000000000))) ≤ Vfield (2758402395201 / 12800000000000)

theorem Zeta5Irrational.V_254 : 488985448782286927153 / 2500000000000000000000 - 6 * (3 / 40) * -(15066182083325074857749 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2323969201358757 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 4350881516122305889661 / 10000000000000000000000) - 6 * (1599828489360179180629 / 10000000000000000000000))) ≤ Vfield (3456533023273 / 16000000000000)

theorem Zeta5Irrational.V_255 : 1960324980953131803927 / 10000000000000000000000 - 6 * (3 / 40) * -(1504215922062519674107 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (290854372377773 / 625000000000000 * (Real.pi + (Real.pi / 2 - 544449225552295190347 / 1250000000000000000000) - 6 * (1597891496232632013767 / 10000000000000000000000))) ≤ Vfield (13860252210179 / 64000000000000)

theorem Zeta5Irrational.V_256 : 982353123193515533941 / 5000000000000000000000 - 6 * (3 / 40) * -(7509096964721451375789 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2329697231474141 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 872059646811761308523 / 2000000000000000000000) - 6 * (1595961522167481885227 / 10000000000000000000000))) ≤ Vfield (6947186163633 / 32000000000000)

theorem Zeta5Irrational.V_257 : 246135699139107045039 / 1250000000000000000000 - 6 * (3 / 40) * -(14994285934494019374537 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4665111943383733 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 17459979332987969381 / 40000000000000000000) - 6 * (398509631218225111797 / 2500000000000000000000))) ≤ Vfield (13928492444353 / 64000000000000)

theorem Zeta5Irrational.V_258 : 1973463022810409675657 / 10000000000000000000000 - 6 * (3 / 40) * -(14970434962464114446783 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (934164485029269 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2184841815009400424567 / 5000000000000000000000) - 6 * (796061231206485465923 / 5000000000000000000000))) ≤ Vfield (87266328509 / 400000000000)

theorem Zeta5Irrational.V_259 : 395567707431457601787 / 2000000000000000000000 - 6 * (3 / 40) * -(1868330092748718717143 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (18706103735497 / 40000000000000 * (Real.pi + (Real.pi / 2 - 109359116306101365259 / 250000000000000000000) - 6 * (1590213293203845113049 / 10000000000000000000000))) ≤ Vfield (13996732678527 / 64000000000000)

theorem Zeta5Irrational.V_260 : 1982212137828887213253 / 10000000000000000000000 - 6 * (3 / 40) * -(7461451501819978019017 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (187288899801977 / 400000000000000 * (Real.pi + (Real.pi / 2 - 2189518963813952082979 / 5000000000000000000000) - 6 * (1588310976009953894083 / 10000000000000000000000))) ≤ Vfield (7015426397807 / 32000000000000)

theorem Zeta5Irrational.V_261 : 198658382649840584889 / 1000000000000000000000 - 6 * (3 / 40) * -(7449610739948963803307 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2343956066999513 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 219185174185610494233 / 500000000000000000000) - 6 * (1586415469940263764489 / 10000000000000000000000))) ≤ Vfield (14064972912701 / 64000000000000)

theorem Zeta5Irrational.V_262 : 248869200604606127997 / 1250000000000000000000 - 6 * (3 / 40) * -(14875595905142932846117 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2346797437948349 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 4388361347876901126497 / 10000000000000000000000) - 6 * (396131683611146364051 / 2500000000000000000000))) ≤ Vfield (3524773257447 / 16000000000000)

theorem Zeta5Irrational.V_263 : 1995321474513032226771 / 10000000000000000000000 - 6 * (3 / 40) * -(14852026015632438169299 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1174817686440969 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 1098252886835331265209 / 2500000000000000000000) - 6 * (1582644729309929085451 / 10000000000000000000000))) ≤ Vfield (4522628207 / 20480000000)

theorem Zeta5Irrational.V_264 : 999843718596792574793 / 5000000000000000000000 - 6 * (3 / 40) * -(14828511549484442036283 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4704939768471071 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 4397654109165580255539 / 10000000000000000000000) - 6 * (158076941465690711107 / 1000000000000000000000))) ≤ Vfield (7083666631981 / 32000000000000)