V25: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_301 : 1240130691140485734679 / 5000000000000000000000 - 6 * (3 / 40) * -(12478605076626120675669 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5305595421098193 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (152436035464757284741 / 625000000000000000000)) - 6 * (175537173293389352119 / 1250000000000000000000))) ≤ Vfield (9007789687161 / 32000000000000)

theorem Zeta5Irrational.V_302 : 1244868006543635756541 / 5000000000000000000000 - 6 * (3 / 40) * -(12436386238777361036033 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5317030851949791 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2443436214313161845841 / 10000000000000000000000)) - 6 * (10947785663169174833 / 78125000000000000000))) ≤ Vfield (723732917263 / 2560000000000)

theorem Zeta5Irrational.V_303 : 2499201675527205748003 / 10000000000000000000000 - 6 * (3 / 40) * -(6197172447429658443921 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (532844174114663 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2447882078016176642779 / 10000000000000000000000)) - 6 * (349588661375526816723 / 2500000000000000000000))) ≤ Vfield (4542766622207 / 16000000000000)

theorem Zeta5Irrational.V_304 : 62598278722809241977 / 250000000000000000000 - 6 * (3 / 40) * -(6186695158982756371369 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (666767253982059 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1225049934248501779659 / 5000000000000000000000)) - 6 * (698440355903575839597 / 5000000000000000000000))) ≤ Vfield (36419876534909 / 128000000000000)

theorem Zeta5Irrational.V_305 : 1254329193281513271393 / 5000000000000000000000 - 6 * (3 / 40) * -(2470495911739800849337 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5339828246020797 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (245231424585502598539 / 1000000000000000000000)) - 6 * (348852857314937662517 / 2500000000000000000000))) ≤ Vfield (18248810046081 / 64000000000000)

theorem Zeta5Irrational.V_306 : 2513383390591947328477 / 10000000000000000000000 - 6 * (3 / 40) * -(6165806217095040688203 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (167047262595149 / 312500000000000 * (Real.pi + (Real.pi / 2 - 2 * (2454525220863704290673 / 10000000000000000000000)) - 6 * (1393946773448474205463 / 10000000000000000000000))) ≤ Vfield (7315072729883 / 25600000000000)

theorem Zeta5Irrational.V_307 : 314763270388613698039 / 1250000000000000000000 - 6 * (3 / 40) * -(6155394381355720490859 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1337797630557621 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1228366402120582497673 / 5000000000000000000000)) - 6 * (278497344028178964147 / 2000000000000000000000))) ≤ Vfield (9163276801667 / 32000000000000)

theorem Zeta5Irrational.V_308 : 2522826706220703069523 / 10000000000000000000000 - 6 * (3 / 40) * -(12290008363668690903519 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1071372524555549 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2458937006650601874589 / 10000000000000000000000)) - 6 * (347757811320475804929 / 2500000000000000000000))) ≤ Vfield (36730850763921 / 128000000000000)

theorem Zeta5Irrational.V_309 : 2527545022031135393343 / 10000000000000000000000 - 6 * (3 / 40) * -(12269271057590952551449 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5362528723784813 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (492227567740135145223 / 2000000000000000000000)) - 6 * (1389580324992042662019 / 10000000000000000000000))) ≤ Vfield (18404297160587 / 64000000000000)

theorem Zeta5Irrational.V_310 : 50645222252820752813 / 200000000000000000000 - 6 * (3 / 40) * -(122485766661215607187 / 100000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1073637768849831 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (24633353109459053127 / 100000000000000000000)) - 6 * (277626787113173012921 / 2000000000000000000000))) ≤ Vfield (36886337878427 / 128000000000000)

theorem Zeta5Irrational.V_311 : 2536974980148269984337 / 10000000000000000000000 - 6 * (3 / 40) * -(12227925012008859438829 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2686921501534097 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (308191179235882659497 / 1250000000000000000000)) - 6 * (693346026735151028923 / 5000000000000000000000))) ≤ Vfield (231025508973 / 800000000000)

theorem Zeta5Irrational.V_312 : 2541686626647727284469 / 10000000000000000000000 - 6 * (3 / 40) * -(3051828979774273160183 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5379491219040039 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1233860108985775068049 / 5000000000000000000000)) - 6 * (277050931068611634373 / 2000000000000000000000))) ≤ Vfield (37041824992933 / 128000000000000)