V35: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_421 : 1860131738235363403791 / 5000000000000000000000 - 6 * (3 / 40) * -(1569226225604356732877 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3356602458448497 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1478043914574713354633 / 5000000000000000000000)) - 6 * (222517508356799869161 / 2000000000000000000000))) ≤ Vfield (7210739241 / 16000000000)

theorem Zeta5Irrational.V_422 : 116400839797190555333 / 312500000000000000000 - 6 * (3 / 40) * -(1957907560260822272463 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1679533701099709 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2957786616188343050519 / 10000000000000000000000)) - 6 * (555888909335956105031 / 5000000000000000000000))) ≤ Vfield (1805333410003 / 4000000000000)

theorem Zeta5Irrational.V_423 : 3729388189040054123869 / 10000000000000000000000 - 6 * (3 / 40) * -(7817150351193086393177 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3361530538456403 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2959483383238434001347 / 10000000000000000000000)) - 6 * (1110969860924394921403 / 10000000000000000000000))) ≤ Vfield (451995502439 / 1000000000000)

theorem Zeta5Irrational.V_424 : 3733947424958614430597 / 10000000000000000000000 - 6 * (3 / 40) * -(975336424718981787153 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6727983742379657 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2961178134875425243097 / 10000000000000000000000)) - 6 * (1110163662135900473617 / 10000000000000000000000))) ≤ Vfield (1810630609509 / 4000000000000)

theorem Zeta5Irrational.V_425 : 3738504583161202382823 / 10000000000000000000000 - 6 * (3 / 40) * -(1557650664052654548403 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (841612851088889 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (592574175131759472259 / 2000000000000000000000)) - 6 * (1109359215933374475979 / 10000000000000000000000))) ≤ Vfield (906639604631 / 2000000000000)

theorem Zeta5Irrational.V_426 : 93576491638516288227 / 250000000000000000000 - 6 * (3 / 40) * -(7773836058532506180713 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1684454570947503 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1482280805065932959781 / 5000000000000000000000)) - 6 * (1108556515976043602471 / 10000000000000000000000))) ≤ Vfield (363185561803 / 800000000000)

theorem Zeta5Irrational.V_427 : 1873806336993604995811 / 5000000000000000000000 - 6 * (3 / 40) * -(3879719776312348896627 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3371365087735233 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (92695323213183203139 / 312500000000000000000)) - 6 * (1107755555955205237929 / 10000000000000000000000))) ≤ Vfield (28415256387 / 62500000000)

theorem Zeta5Irrational.V_428 : 938040902597136293219 / 2500000000000000000000 - 6 * (3 / 40) * -(968132967857934315427 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1686909622894499 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (593587415648002736951 / 2000000000000000000000)) - 6 * (2213912659188038901 / 20000000000000000000))) ≤ Vfield (1821225008521 / 4000000000000)

theorem Zeta5Irrational.V_429 : 3756712476629748451179 / 10000000000000000000000 - 6 * (3 / 40) * -(386535428491473142307 / 500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1350508647981937 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1484810910440810834293 / 5000000000000000000000)) - 6 * (276539707661825492393 / 2500000000000000000000))) ≤ Vfield (911936804137 / 2000000000000)

theorem Zeta5Irrational.V_430 : 3761259274593339865841 / 10000000000000000000000 - 6 * (3 / 40) * -(1929093493589703793197 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3378722214117157 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2971304575226139195549 / 10000000000000000000000)) - 6 * (1105363052901320432927 / 10000000000000000000000))) ≤ Vfield (1826522208027 / 4000000000000)

theorem Zeta5Irrational.V_431 : 1882902003079636395783 / 5000000000000000000000 - 6 * (3 / 40) * -(1925514974385436700747 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6762342064292517 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2972985345737252723841 / 10000000000000000000000)) - 6 * (1104568990173589174241 / 10000000000000000000000))) ≤ Vfield (91458540389 / 200000000000)

theorem Zeta5Irrational.V_432 : 1885173336602469301127 / 5000000000000000000000 - 6 * (3 / 40) * -(768776628072108333261 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6767236155796913 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2974664136862955190747 / 10000000000000000000000)) - 6 * (551888318156334600501 / 5000000000000000000000))) ≤ Vfield (1831819407533 / 4000000000000)