V20: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_241 : 916213007214556584881 / 5000000000000000000000 - 6 * (3 / 40) * -(15763379946783387163977 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (280280107331961 / 625000000000000 * (Real.pi + (Real.pi / 2 - 526953344135841385621 / 1250000000000000000000) - 6 * (828548887056965813683 / 5000000000000000000000))) ≤ Vfield (201105762729 / 1000000000000)

theorem Zeta5Irrational.V_242 : 925082402975123894543 / 5000000000000000000000 - 6 * (3 / 40) * -(978797156642601188271 / 625000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4508195537539797 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 132354768328260144823 / 312500000000000000000) - 6 * (1648538651467957972391 / 10000000000000000000000))) ≤ Vfield (3251812320751 / 16000000000000)

theorem Zeta5Irrational.V_243 : 233484023338699112559 / 1250000000000000000000 - 6 * (3 / 40) * -(15559171574152312277573 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (906357054068373 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2127470226874638958149 / 5000000000000000000000) - 6 * (205013851103837126691 / 1250000000000000000000))) ≤ Vfield (1642966218919 / 8000000000000)

theorem Zeta5Irrational.V_244 : 942774133875520337323 / 5000000000000000000000 - 6 * (3 / 40) * -(15458610182818172849901 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (569406605438411 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 427439244048937257737 / 1000000000000000000000) - 6 * (326362184796567935759 / 2000000000000000000000))) ≤ Vfield (132802102197 / 640000000000)

theorem Zeta5Irrational.V_245 : 473593651354481801167 / 2500000000000000000000 - 6 * (3 / 40) * -(15408706184512598421353 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4566941409102827 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1071017029048578874257 / 2500000000000000000000) - 6 * (325541591908918348673 / 2000000000000000000000))) ≤ Vfield (6674225226937 / 32000000000000)

theorem Zeta5Irrational.V_246 : 380638631906135117007 / 2000000000000000000000 - 6 * (3 / 40) * -(3071809998195709492653 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2289300067710379 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 268356911279549160589 / 625000000000000000000) - 6 * (1623635791236049692747 / 10000000000000000000000))) ≤ Vfield (838543168003 / 4000000000000)

theorem Zeta5Irrational.V_247 : 956001971902565436247 / 5000000000000000000000 - 6 * (3 / 40) * -(3061927830671543104789 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1147557312456873 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 1075830019932161256039 / 2500000000000000000000) - 6 * (1619594035700487665621 / 10000000000000000000000))) ≤ Vfield (6742465461111 / 32000000000000)

theorem Zeta5Irrational.V_248 : 30012608936264309779 / 156250000000000000000 - 6 * (3 / 40) * -(15260471258913580618157 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4601828976816581 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 215644842867158688389 / 500000000000000000000) - 6 * (64623292649177857249 / 400000000000000000000))) ≤ Vfield (3388292789099 / 16000000000000)

theorem Zeta5Irrational.V_249 : 1929602257521558340209 / 10000000000000000000000 - 6 * (3 / 40) * -(1901442991290557573503 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1153349884514821 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 86448823074548479773 / 200000000000000000000) - 6 * (805800131307608396503 / 5000000000000000000000))) ≤ Vfield (1362141139057 / 6400000000000)

theorem Zeta5Irrational.V_250 : 484597453553654580303 / 2500000000000000000000 - 6 * (3 / 40) * -(3790713706248445209689 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (924988230490799 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 4331953206373391881623 / 10000000000000000000000) - 6 * (1607647511007304005851 / 10000000000000000000000))) ≤ Vfield (1711206453093 / 8000000000000)

theorem Zeta5Irrational.V_251 : 971390349231681716199 / 5000000000000000000000 - 6 * (3 / 40) * -(15138598883318111695953 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4630701172242809 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 4336697214724926254481 / 10000000000000000000000) - 6 * (321136402291257269187 / 2000000000000000000000))) ≤ Vfield (13723771741831 / 64000000000000)

theorem Zeta5Irrational.V_252 : 486792413892953500607 / 2500000000000000000000 - 6 * (3 / 40) * -(944650102148565756543 / 625000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4636454036174559 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 4341433249904055055669 / 10000000000000000000000) - 6 * (400930925943187151183 / 2500000000000000000000))) ≤ Vfield (6878945929459 / 32000000000000)