V28: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_337 : 537331468458756497103 / 2000000000000000000000 - 6 * (3 / 40) * -(5794315664138754364461 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1387934111209669 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1267016548427454690201 / 5000000000000000000000)) - 6 * (1342799328315371089453 / 10000000000000000000000))) ≤ Vfield (616435551059 / 2000000000000)

theorem Zeta5Irrational.V_338 : 1347969257293923422131 / 5000000000000000000000 - 6 * (3 / 40) * -(11550000575388243838883 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1112533179031669 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1269104194128484300137 / 5000000000000000000000)) - 6 * (670096261503884641029 / 5000000000000000000000))) ≤ Vfield (19803681191141 / 64000000000000)

theorem Zeta5Irrational.V_339 : 1352605540426391349941 / 5000000000000000000000 - 6 * (3 / 40) * -(11511518481907533559663 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5573573913510577 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (79449113381127256143 / 312500000000000000000)) - 6 * (167200105171068611039 / 1250000000000000000000))) ≤ Vfield (9940712374197 / 32000000000000)

theorem Zeta5Irrational.V_340 : 680932614757960827541 / 2500000000000000000000 - 6 * (3 / 40) * -(11434995727182164588973 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (349707884715169 / 625000000000000 * (Real.pi + (Real.pi / 2 - 2 * (510132446778923655351 / 2000000000000000000000)) - 6 * (1332462268344726654813 / 10000000000000000000000))) ≤ Vfield (200369118629 / 640000000000)

theorem Zeta5Irrational.V_341 : 548443120772471356537 / 2000000000000000000000 - 6 * (3 / 40) * -(2271810820302100756551 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5616994160776461 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2558905467817166652031 / 10000000000000000000000)) - 6 * (265476493422338033503 / 2000000000000000000000))) ≤ Vfield (10096199488703 / 32000000000000)

theorem Zeta5Irrational.V_342 : 1380333320836278337613 / 5000000000000000000000 - 6 * (3 / 40) * -(5641842422477859503957 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5638578900628463 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (40110966774065083747 / 156250000000000000000)) - 6 * (1322360325788739087959 / 10000000000000000000000))) ≤ Vfield (2543485761489 / 8000000000000)

theorem Zeta5Irrational.V_343 : 2779083698092697689807 / 10000000000000000000000 - 6 * (3 / 40) * -(2241775878834215454377 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1415020331899601 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1287625992309098770811 / 5000000000000000000000)) - 6 * (1317394761724191804781 / 10000000000000000000000))) ≤ Vfield (10251686603209 / 32000000000000)

theorem Zeta5Irrational.V_344 : 1398733449030094056213 / 5000000000000000000000 - 6 * (3 / 40) * -(2783657344140277014661 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2840751188129811 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (322919540605409180593 / 1250000000000000000000)) - 6 * (131248472051481762243 / 1000000000000000000000))) ≤ Vfield (5164715080231 / 16000000000000)

theorem Zeta5Irrational.V_345 : 2834132224953083779733 / 10000000000000000000000 - 6 * (3 / 40) * -(5493881535351685480757 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1431025997411363 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (40616089696646176937 / 156250000000000000000)) - 6 * (1302827124684973012057 / 10000000000000000000000))) ≤ Vfield (1310614659371 / 4000000000000)

theorem Zeta5Irrational.V_346 : 2870663608185664775589 / 10000000000000000000000 - 6 * (3 / 40) * -(2710755638254187861199 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5766390874464393 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2615326125171193657161 / 10000000000000000000000)) - 6 * (1293379633233145650797 / 10000000000000000000000))) ≤ Vfield (5320202194737 / 16000000000000)

theorem Zeta5Irrational.V_347 : 726765505706868317119 / 2500000000000000000000 - 6 * (3 / 40) * -(5350173580933170941977 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (580836990470971 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2631049342012675989687 / 10000000000000000000000)) - 6 * (128413473666420098043 / 1000000000000000000000))) ≤ Vfield (539794575199 / 1600000000000)

theorem Zeta5Irrational.V_348 : 1471664216669667297137 / 5000000000000000000000 - 6 * (3 / 40) * -(10559678795699479359667 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5850047707734419 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2646603120442483009779 / 10000000000000000000000)) - 6 * (637542647980929447969 / 5000000000000000000000))) ≤ Vfield (5475689309243 / 16000000000000)