V05: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_61 : 283579045197899142671 / 10000000000000000000000 - 6 * (3 / 40) * -(33700238312826287098913 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1695989910328919 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1680003860151625494353 / 10000000000000000000000) - 6 * (4163649465840225933501 / 10000000000000000000000))) ≤ Vfield (9204421683 / 320000000000)

theorem Zeta5Irrational.V_62 : 28603609146785446397 / 1000000000000000000000 - 6 * (3 / 40) * -(6725398807852979702343 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (851713285760769 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 42180792698504378977 / 250000000000000000000) - 6 * (2073744912138374589189 / 5000000000000000000000))) ≤ Vfield (928531867061 / 32000000000000)

theorem Zeta5Irrational.V_63 : 2307940273427734419 / 80000000000000000000 - 6 * (3 / 40) * -(33554282339629042240773 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1710830907247629 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 847213185079392045819 / 5000000000000000000000) - 6 * (2065758707467686423337 / 5000000000000000000000))) ≤ Vfield (468310782911 / 16000000000000)

theorem Zeta5Irrational.V_64 : 290948373626185129557 / 10000000000000000000000 - 6 * (3 / 40) * -(418526194061101859357 / 125000000000000000000) - 2 + 12 * (3 / 40) + 2 * (429550833853069 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 1701588269078549890509 / 10000000000000000000000) - 6 * (2057864319825470333217 / 5000000000000000000000))) ≤ Vfield (944711264583 / 32000000000000)

theorem Zeta5Irrational.V_65 : 293403610107240061481 / 10000000000000000000000 - 6 * (3 / 40) * -(3341042607133438815809 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1725544264992931 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1708717817988970253053 / 10000000000000000000000) - 6 * (4100119996605776193839 / 10000000000000000000000))) ≤ Vfield (59550060209 / 2000000000000)

theorem Zeta5Irrational.V_66 : 147929121958822036403 / 5000000000000000000000 - 6 * (3 / 40) * -(104185208174615246663 / 31250000000000000000) - 2 + 12 * (3 / 40) + 2 * (433213524076041 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 428953855365956309143 / 2500000000000000000000) - 6 * (816937615405656711109 / 2000000000000000000000))) ≤ Vfield (192178132421 / 6400000000000)

theorem Zeta5Irrational.V_67 : 9322258604787240969 / 312500000000000000000 - 6 * (3 / 40) * -(33268609951502147843163 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1740133221252397 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 861440737808505226089 / 5000000000000000000000) - 6 * (813885912405834617621 / 2000000000000000000000))) ≤ Vfield (484490180433 / 16000000000000)

theorem Zeta5Irrational.V_68 : 75191426177364952563 / 2500000000000000000000 - 6 * (3 / 40) * -(33198449022893842451719 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1747382023581097 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1729916368348796967283 / 10000000000000000000000) - 6 * (4054341219568550892639 / 10000000000000000000000))) ≤ Vfield (977070059627 / 32000000000000)

theorem Zeta5Irrational.V_69 : 303218532281807704997 / 10000000000000000000000 - 6 * (3 / 40) * -(6625755384441007730879 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (43865021977671 / 250000000000000 * (Real.pi + (Real.pi / 2 - 1736920479582931750383 / 10000000000000000000000) - 6 * (201970995077376040719 / 500000000000000000000))) ≤ Vfield (246289939597 / 8000000000000)

theorem Zeta5Irrational.V_70 : 154061191627547000041 / 5000000000000000000000 - 6 * (3 / 40) * -(32990872286197016689579 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (442237553684297 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 1750837838732508012519 / 10000000000000000000000) - 6 * (501258268688367222693 / 1250000000000000000000))) ≤ Vfield (100133915591 / 3200000000000)

theorem Zeta5Irrational.V_71 : 156511915315791689151 / 5000000000000000000000 - 6 * (3 / 40) * -(16427421789228452963099 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1783184084573153 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 220579555174712374839 / 1250000000000000000000) - 6 * (3981344696696963220873 / 10000000000000000000000))) ≤ Vfield (127189819179 / 4000000000000)

theorem Zeta5Irrational.V_72 : 317922876766342253191 / 10000000000000000000000 - 6 * (3 / 40) * -(32720640446352325306753 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1797305231932307 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 355663812413146259823 / 2000000000000000000000) - 6 * (1976616554840196050209 / 5000000000000000000000))) ≤ Vfield (516848975477 / 16000000000000)