V12: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_145 : 474191423687705405539 / 5000000000000000000000 - 6 * (3 / 40) * -(11263927763828573808227 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3154061475050857 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 95478208413835360219 / 312500000000000000000) - 6 * (1167265072719666656229 / 5000000000000000000000))) ≤ Vfield (24870259471 / 250000000000)

theorem Zeta5Irrational.V_146 : 120140089155551917327 / 1250000000000000000000 - 6 * (3 / 40) * -(22395404883448735089487 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (198512470516247 / 625000000000000 * (Real.pi + (Real.pi / 2 - 3075424865340954955163 / 10000000000000000000000) - 6 * (2318837467048294312633 / 10000000000000000000000))) ≤ Vfield (1614118950931 / 16000000000000)

theorem Zeta5Irrational.V_147 : 194768474885970078339 / 2000000000000000000000 - 6 * (3 / 40) * -(22264685648903831350143 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (799546086001203 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 1547691177866349120623 / 5000000000000000000000) - 6 * (575864282886168339093 / 2500000000000000000000))) ≤ Vfield (818270647859 / 8000000000000)

theorem Zeta5Irrational.V_148 : 98654787210944095483 / 1000000000000000000000 - 6 * (3 / 40) * -(22135653141131857303987 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3220019060992689 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 124607136184504540319 / 400000000000000000000) - 6 * (457675782124995330019 / 2000000000000000000000))) ≤ Vfield (331792728101 / 3200000000000)

theorem Zeta5Irrational.V_149 : 496447286229849446731 / 5000000000000000000000 - 6 * (3 / 40) * -(4414351183143760254287 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3230881084257917 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 781254219709386649659 / 2500000000000000000000) - 6 * (1140475012063116264297 / 5000000000000000000000))) ≤ Vfield (3340349625797 / 32000000000000)

theorem Zeta5Irrational.V_150 : 499618623652078033613 / 5000000000000000000000 - 6 * (3 / 40) * -(22008264384942687831393 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (648341342444703 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 313481616803270820263 / 1000000000000000000000) - 6 * (2273593038966975577993 / 10000000000000000000000))) ≤ Vfield (420346496323 / 4000000000000)

theorem Zeta5Irrational.V_151 : 201115180349214172211 / 2000000000000000000000 - 6 * (3 / 40) * -(2194517342963678964519 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1626248154152247 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 3144576650626855419069 / 10000000000000000000000) - 6 * (18130454419663968323 / 80000000000000000000))) ≤ Vfield (3385194315371 / 32000000000000)

theorem Zeta5Irrational.V_152 : 1011910540879013487081 / 10000000000000000000000 - 6 * (3 / 40) * -(21882478026919803602261 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1631625114953933 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 630859739779612780437 / 2000000000000000000000) - 6 * (2259090187622654074271 / 10000000000000000000000))) ≤ Vfield (1703808330079 / 16000000000000)

theorem Zeta5Irrational.V_153 : 2545602924467127949 / 25000000000000000000 - 6 * (3 / 40) * -(21820173247796202238733 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1636984414285389 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 3163982679114103670613 / 10000000000000000000000) - 6 * (225194209246394264897 / 1000000000000000000000))) ≤ Vfield (686007800989 / 6400000000000)

theorem Zeta5Irrational.V_154 : 1024567793543830700313 / 10000000000000000000000 - 6 * (3 / 40) * -(21758254254830878525977 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (656930490018921 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 3173628951668722226459 / 10000000000000000000000) - 6 * (89794457570276818707 / 400000000000000000000))) ≤ Vfield (863115337433 / 8000000000000)

theorem Zeta5Irrational.V_155 : 20554592101476308083 / 200000000000000000000 - 6 * (3 / 40) * -(21727437940939080223441 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1644990625478013 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 1589219029311252440703 / 5000000000000000000000) - 6 * (448269214612905134469 / 2000000000000000000000))) ≤ Vfield (6927345044251 / 64000000000000)

theorem Zeta5Irrational.V_156 : 1030890417214564711111 / 10000000000000000000000 - 6 * (3 / 40) * -(10848358149947670282237 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1647650717337557 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 795809467803487892921 / 2500000000000000000000) - 6 * (279730896733188049123 / 1250000000000000000000))) ≤ Vfield (3474883694519 / 32000000000000)