V45: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_541 : 1203010037783684061843 / 2500000000000000000000 - 6 * (3 / 40) * -(4721718145366935286647 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1965358351613251 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1665586163161638182387 / 5000000000000000000000)) - 6 * (951145802866699611319 / 10000000000000000000000))) ≤ Vfield (39553366530621 / 64000000000000)

theorem Zeta5Irrational.V_542 : 481868114864098952669 / 1000000000000000000000 - 6 * (3 / 40) * -(117612437523516345031 / 250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1573653375420513 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3333283300374232651811 / 10000000000000000000000)) - 6 * (118790589224961794759 / 1250000000000000000000))) ≤ Vfield (19811079567779 / 32000000000000)

theorem Zeta5Irrational.V_543 : 603164717348652311 / 1250000000000000000 - 6 * (3 / 40) * -(4687306460600976406899 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7875094418133881 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (66707820858295245557 / 200000000000000000000)) - 6 * (237376436882747463663 / 2500000000000000000000))) ≤ Vfield (7938190348099 / 12800000000000)

theorem Zeta5Irrational.V_544 : 603993740928188690151 / 1250000000000000000000 - 6 * (3 / 40) * -(4670144922737522464169 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (985239505619521 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3337495562985116148511 / 10000000000000000000000)) - 6 * (948688894929314443929 / 10000000000000000000000))) ≤ Vfield (4969968043179 / 8000000000000)

theorem Zeta5Irrational.V_545 : 38708621763074600159 / 80000000000000000000 - 6 * (3 / 40) * -(4653012786262152590651 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1577746354582403 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3339596869587028725083 / 10000000000000000000000)) - 6 * (947874146918292524199 / 10000000000000000000000))) ≤ Vfield (39828536950369 / 64000000000000)

theorem Zeta5Irrational.V_546 : 4845201123488534177387 / 10000000000000000000000 - 6 * (3 / 40) * -(2317954975302697975151 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7895541617277791 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1670847485841972874563 / 5000000000000000000000)) - 6 * (947061494476020427973 / 10000000000000000000000))) ≤ Vfield (19948664777653 / 32000000000000)

theorem Zeta5Irrational.V_547 : 4851820142549443681207 / 10000000000000000000000 - 6 * (3 / 40) * -(4618836315712907967727 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1580469118652809 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1671894939100624160823 / 5000000000000000000000)) - 6 * (946250928634646755839 / 10000000000000000000000))) ≤ Vfield (39966122160243 / 64000000000000)

theorem Zeta5Irrational.V_548 : 2429217391683414152803 / 5000000000000000000000 - 6 * (3 / 40) * -(4601791782041958375991 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1581828743203179 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3345881598026473956461 / 10000000000000000000000)) - 6 * (236360610119989398587 / 2500000000000000000000))) ≤ Vfield (2001745738259 / 3200000000000)

theorem Zeta5Irrational.V_549 : 2432522525864480701643 / 5000000000000000000000 - 6 * (3 / 40) * -(4584776250557949002001 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7915936000613433 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (418496267501192554361 / 1250000000000000000000)) - 6 * (472318010575481681801 / 5000000000000000000000))) ≤ Vfield (40103707370117 / 64000000000000)

theorem Zeta5Irrational.V_550 : 4871650953412645296287 / 10000000000000000000000 - 6 * (3 / 40) * -(4567789622730961196307 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7922722462072103 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3350055512962961865401 / 10000000000000000000000)) - 6 * (943831661839492373971 / 10000000000000000000000))) ≤ Vfield (20086249987527 / 32000000000000)

theorem Zeta5Irrational.V_551 : 609781561772905195823 / 1250000000000000000000 - 6 * (3 / 40) * -(1137707950133083130891 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7929503115343099 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3352137725662069253959 / 10000000000000000000000)) - 6 * (471514676894892731199 / 5000000000000000000000))) ≤ Vfield (40241292579991 / 64000000000000)

theorem Zeta5Irrational.V_552 : 2442424839897350623381 / 5000000000000000000000 - 6 * (3 / 40) * -(4533902686431262429811 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7936277975313741 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3354216786845224709769 / 10000000000000000000000)) - 6 * (942229088298096658871 / 10000000000000000000000))) ≤ Vfield (1259690162029 / 2000000000000)