V06: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_73 : 20176220250686091201 / 625000000000000000000 - 6 * (3 / 40) * -(2036763408608682511547 / 625000000000000000000) - 2 + 12 * (3 / 40) + 2 * (905658146596647 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 895944183790336958567 / 5000000000000000000000) - 6 * (785142011276042781277 / 2000000000000000000000))) ≤ Vfield (262469337119 / 8000000000000)

theorem Zeta5Irrational.V_74 : 332605631219046927529 / 10000000000000000000000 - 6 * (3 / 40) * -(32328510364068521412621 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1839018202329709 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1818697196560381043083 / 10000000000000000000000) - 6 * (3872349322266150066581 / 10000000000000000000000))) ≤ Vfield (6763975897 / 200000000000)

theorem Zeta5Irrational.V_75 : 68476434199942366179 / 2000000000000000000000 - 6 * (3 / 40) * -(16037690220153861181957 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (466577243270909 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 1845082320061846925631 / 10000000000000000000000) - 6 * (764222275881632837763 / 2000000000000000000000))) ≤ Vfield (278648734641 / 8000000000000)

theorem Zeta5Irrational.V_76 : 352149162041970693603 / 10000000000000000000000 - 6 * (3 / 40) * -(7957125030406035210083 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (75728255413947 / 400000000000000 * (Real.pi + (Real.pi / 2 - 935530869456240818211 / 5000000000000000000000) - 6 * (3771858836909198659297 / 10000000000000000000000))) ≤ Vfield (143369216701 / 4000000000000)

theorem Zeta5Irrational.V_77 : 371654572393941879647 / 10000000000000000000000 - 6 * (3 / 40) * -(313523048550250673131 / 100000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1945886144292619 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 48046732795733132627 / 250000000000000000000) - 6 * (183940991600097138117 / 500000000000000000000))) ≤ Vfield (75729457731 / 2000000000000)

theorem Zeta5Irrational.V_78 : 51318953063325241837 / 1250000000000000000000 - 6 * (3 / 40) * -(15231489342023646879373 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (409436579929053 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2019282332713757840697 / 10000000000000000000000) - 6 * (877929728397766997881 / 2500000000000000000000))) ≤ Vfield (20954789123 / 500000000000)

theorem Zeta5Irrational.V_79 : 26556429962361706593 / 625000000000000000000 - 6 * (3 / 40) * -(1884565064399020768501 / 625000000000000000000) - 2 + 12 * (3 / 40) + 2 * (16276631329523 / 78125000000000 * (Real.pi + (Real.pi / 2 - 2054026228998431747243 / 10000000000000000000000) - 6 * (431930043648711482693 / 1250000000000000000000))) ≤ Vfield (694494763253 / 16000000000000)

theorem Zeta5Irrational.V_80 : 54008848847639878331 / 1250000000000000000000 - 6 * (3 / 40) * -(30001601622668503149493 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2101287579841671 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 258894388269868848451 / 1250000000000000000000) - 6 * (1714149204325831240059 / 5000000000000000000000))) ≤ Vfield (1412931037823 / 32000000000000)

theorem Zeta5Irrational.V_81 : 219616783974515609901 / 5000000000000000000000 - 6 * (3 / 40) * -(1492621071671766733419 / 500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (105950775316447 / 500000000000000 * (Real.pi + (Real.pi / 2 - 1044063650657751722727 / 5000000000000000000000) - 6 * (850446742255768075683 / 2500000000000000000000))) ≤ Vfield (71843627457 / 1600000000000)

theorem Zeta5Irrational.V_82 : 442813033499629176129 / 10000000000000000000000 - 6 * (3 / 40) * -(14889328837725568225533 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1063912041417817 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 1048277920962015937779 / 5000000000000000000000) - 6 * (3388760114959635706763 / 10000000000000000000000))) ≤ Vfield (2897686609597 / 64000000000000)

theorem Zeta5Irrational.V_83 : 223195609125654108827 / 5000000000000000000000 - 6 * (3 / 40) * -(2970543404491423273459 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1068298172202887 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 1052473315449602418319 / 5000000000000000000000) - 6 * (1687940980739126299293 / 5000000000000000000000))) ≤ Vfield (1460814060457 / 32000000000000)

theorem Zeta5Irrational.V_84 : 449968123120327541017 / 10000000000000000000000 - 6 * (3 / 40) * -(29632742689235428438627 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (536333184128633 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2113300121198763880449 / 10000000000000000000000) - 6 * (420393712183787165013 / 1250000000000000000000))) ≤ Vfield (2945569632231 / 64000000000000)