V18: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_217 : 301168224368862296271 / 2000000000000000000000 - 6 * (3 / 40) * -(17829697167130139861507 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4031291139396187 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 3832009751163251614927 / 10000000000000000000000) - 6 * (919708107235846697917 / 5000000000000000000000))) ≤ Vfield (4160334912147 / 25600000000000)

theorem Zeta5Irrational.V_218 : 11794189169129279047 / 78125000000000000000 - 6 * (3 / 40) * -(4450837296658632106129 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2018394637647063 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 1918369187644382154269 / 5000000000000000000000) - 6 * (1836966934064261994179 / 10000000000000000000000))) ≤ Vfield (10429227298003 / 64000000000000)

theorem Zeta5Irrational.V_219 : 189183731314411355741 / 1250000000000000000000 - 6 * (3 / 40) * -(1777707044535513541937 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1010569983217551 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 480182345859374426031 / 1250000000000000000000) - 6 * (229315926589210924701 / 1250000000000000000000))) ≤ Vfield (20915234631277 / 128000000000000)

theorem Zeta5Irrational.V_220 : 1517282033553838498547 / 10000000000000000000000 - 6 * (3 / 40) * -(17750860580341441455871 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (809552628511343 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 1923085479175907476307 / 5000000000000000000000) - 6 * (458024396444353584973 / 2500000000000000000000))) ≤ Vfield (5243003666637 / 32000000000000)

theorem Zeta5Irrational.V_221 : 1521092763872220139037 / 10000000000000000000000 - 6 * (3 / 40) * -(17724719231489336947553 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4053238934580107 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 3850874981935184802889 / 10000000000000000000000) - 6 * (182967738921082186107 / 1000000000000000000000))) ≤ Vfield (21028794701819 / 128000000000000)

theorem Zeta5Irrational.V_222 : 1524902042577198992607 / 10000000000000000000000 - 6 * (3 / 40) * -(2212330755188929494453 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (405870733896293 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 3855570869629157385863 / 10000000000000000000000) - 6 * (228408344945016066593 / 1250000000000000000000))) ≤ Vfield (2108557473709 / 12800000000000)

theorem Zeta5Irrational.V_223 : 1528709870774273975149 / 10000000000000000000000 - 6 * (3 / 40) * -(17672640655907776151439 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (812833677105151 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 3860258653227845737129 / 10000000000000000000000) - 6 * (912432816977701343561 / 5000000000000000000000))) ≤ Vfield (21142354772361 / 128000000000000)

theorem Zeta5Irrational.V_224 : 76625812478384080911 / 500000000000000000000 - 6 * (3 / 40) * -(8823351361468449374261 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1017405525972267 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 241558647769835521489 / 625000000000000000000) - 6 * (1822473950103674257329 / 10000000000000000000000))) ≤ Vfield (1324945925477 / 8000000000000)

theorem Zeta5Irrational.V_225 : 1540124663354140614713 / 10000000000000000000000 - 6 * (3 / 40) * -(17595027821549266170449 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (408050767350993 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 3874273694284965512503 / 10000000000000000000000) - 6 * (1817718661331479209709 / 10000000000000000000000))) ≤ Vfield (10656347439087 / 64000000000000)

theorem Zeta5Irrational.V_226 : 773863646372646733217 / 5000000000000000000000 - 6 * (3 / 40) * -(17543618577511353923213 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (255710267553653 / 625000000000000 * (Real.pi + (Real.pi / 2 - 970894277033406227889 / 2500000000000000000000) - 6 * (453250101545841468879 / 2500000000000000000000))) ≤ Vfield (5356563737179 / 32000000000000)

theorem Zeta5Irrational.V_227 : 1555324146529782093153 / 10000000000000000000000 - 6 * (3 / 40) * -(3498494454666579830101 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (256387009742743 / 625000000000000 * (Real.pi + (Real.pi / 2 - 973212212814486599171 / 2500000000000000000000) - 6 * (1808318706405921828007 / 10000000000000000000000))) ≤ Vfield (10769907509629 / 64000000000000)

theorem Zeta5Irrational.V_228 : 1562915233476233808219 / 10000000000000000000000 - 6 * (3 / 40) * -(17441586233008606041231 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2056495762754341 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 3902089165903819241319 / 10000000000000000000000) - 6 * (1803673092348793482377 / 10000000000000000000000))) ≤ Vfield (108266875449 / 640000000000)