V24: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_289 : 2198488629086328392477 / 10000000000000000000000 - 6 * (3 / 40) * -(1725323680994778098129 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4958713708268379 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 184135701649771270463 / 400000000000000000000) - 6 * (750555712906224550967 / 5000000000000000000000))) ≤ Vfield (3934214662491 / 16000000000000)

theorem Zeta5Irrational.V_290 : 1107795178054387541519 / 5000000000000000000000 - 6 * (3 / 40) * -(13718159850552214083469 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (622521239250649 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2310299720564564919953 / 5000000000000000000000) - 6 * (1494740248442681908947 / 10000000000000000000000))) ≤ Vfield (1984167389789 / 8000000000000)

theorem Zeta5Irrational.V_291 : 281213289841407876621 / 1250000000000000000000 - 6 * (3 / 40) * -(3387852383232238012393 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (502280736600061 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (581838166519744333303 / 2500000000000000000000)) - 6 * (1482237548872014842613 / 10000000000000000000000))) ≤ Vfield (504571876719 / 2000000000000)

theorem Zeta5Irrational.V_292 : 1141853143538352302107 / 5000000000000000000000 - 6 * (3 / 40) * -(13387394237893872067869 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (31656786952219 / 62500000000000 * (Real.pi + (Real.pi / 2 - 2 * (2344204573684607949139 / 10000000000000000000000)) - 6 * (36751085971136076113 / 250000000000000000000))) ≤ Vfield (2052407623963 / 8000000000000)

theorem Zeta5Irrational.V_293 : 1158795523617137301057 / 5000000000000000000000 - 6 * (3 / 40) * -(13226025692197263579119 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2553507233352051 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (147553771669833188447 / 625000000000000000000)) - 6 * (72907271447543795003 / 500000000000000000000))) ≤ Vfield (41730554821 / 160000000000)

theorem Zeta5Irrational.V_294 : 2385018047629768990871 / 10000000000000000000000 - 6 * (3 / 40) * -(20173275815075893487 / 15625000000000000000) - 2 + 12 * (3 / 40) + 2 * (2594927729740271 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1196801073083827964937 / 5000000000000000000000)) - 6 * (1435191184916654243353 / 10000000000000000000000))) ≤ Vfield (269345996903 / 1000000000000)

theorem Zeta5Irrational.V_295 : 300517427895070866779 / 1250000000000000000000 - 6 * (3 / 40) * -(12822930291729512624071 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5213209021966759 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (96111696549200328527 / 400000000000000000000)) - 6 * (714424657120258015799 / 5000000000000000000000))) ≤ Vfield (8696815458149 / 32000000000000)

theorem Zeta5Irrational.V_296 : 1211612152879776726763 / 5000000000000000000000 - 6 * (3 / 40) * -(12735731124909343586647 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2618229216623863 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2411924233564044653293 / 10000000000000000000000)) - 6 * (56903631257368425313 / 400000000000000000000))) ≤ Vfield (4387279507701 / 16000000000000)

theorem Zeta5Irrational.V_297 : 152642052153384038571 / 625000000000000000000 - 6 * (3 / 40) * -(2529857151842140007031 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5259605074484857 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1210499184897321206457 / 5000000000000000000000)) - 6 * (708206888526691726481 / 5000000000000000000000))) ≤ Vfield (1770460514531 / 6400000000000)

theorem Zeta5Irrational.V_298 : 1225891754658183301957 / 5000000000000000000000 - 6 * (3 / 40) * -(6303170850486857560717 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (658892534956321 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (303189255113144357391 / 1250000000000000000000)) - 6 * (353338824384936034991 / 2500000000000000000000))) ≤ Vfield (17782348702563 / 64000000000000)

theorem Zeta5Irrational.V_299 : 1230642573739392974039 / 5000000000000000000000 - 6 * (3 / 40) * -(6281790636822936316249 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2641325148290271 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2430015570348441889311 / 10000000000000000000000)) - 6 * (282063309236787619361 / 2000000000000000000000))) ≤ Vfield (2232511532477 / 8000000000000)

theorem Zeta5Irrational.V_300 : 2470777766097794190011 / 10000000000000000000000 - 6 * (3 / 40) * -(6260501456740909970931 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5294135289560543 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2434503049163477909489 / 10000000000000000000000)) - 6 * (1407297311798374862231 / 10000000000000000000000))) ≤ Vfield (17937835817069 / 64000000000000)