V50: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_601 : 5267654647466773897281 / 10000000000000000000000 - 6 * (3 / 40) * -(895007670617208076217 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4163670045462633 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (138876894475193245607 / 400000000000000000000)) - 6 * (898224269702467027377 / 10000000000000000000000))) ≤ Vfield (11095134878389 / 16000000000000)

theorem Zeta5Irrational.V_602 : 5272443953924180262591 / 10000000000000000000000 - 6 * (3 / 40) * -(1784216451385933877829 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2083052398674487 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1736679883824976458027 / 5000000000000000000000)) - 6 * (897702146630215959721 / 10000000000000000000000))) ≤ Vfield (8886491741437 / 12800000000000)

theorem Zeta5Irrational.V_603 : 5277230967733927753499 / 10000000000000000000000 - 6 * (3 / 40) * -(111151517448245887379 / 312500000000000000000) - 2 + 12 * (3 / 40) + 2 * (1042134531787567 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (434349455772083549517 / 1250000000000000000000)) - 6 * (897180933010781682679 / 10000000000000000000000))) ≤ Vfield (22242188950407 / 32000000000000)

theorem Zeta5Irrational.V_604 : 5286798126183046578949 / 10000000000000000000000 - 6 * (3 / 40) * -(3533720051035585403877 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8346801060892279 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3477662833209266870603 / 10000000000000000000000)) - 6 * (448070611796229685211 / 5000000000000000000000))) ≤ Vfield (5573527036009 / 8000000000000)

theorem Zeta5Irrational.V_605 : 5296356140327890318239 / 10000000000000000000000 - 6 * (3 / 40) * -(3510644913100674866389 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1044564318793689 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3480523946311819555931 / 10000000000000000000000)) - 6 * (111888140059786550771 / 1250000000000000000000))) ≤ Vfield (4469205467533 / 6400000000000)

theorem Zeta5Irrational.V_606 : 5305905027632047828519 / 10000000000000000000000 - 6 * (3 / 40) * -(3487622898804823612337 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4183108381045539 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (870844752170985371119 / 2500000000000000000000)) - 6 * (894072602868394696077 / 10000000000000000000000))) ≤ Vfield (11198973265647 / 16000000000000)

theorem Zeta5Irrational.V_607 : 332215300344320520497 / 625000000000000000000 - 6 * (3 / 40) * -(866163441026753018953 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6543677918209 / 7812500000000 * (Real.pi + (Real.pi / 2 - 2 * (3486228043391734482853 / 10000000000000000000000)) - 6 * (446521825065223545333 / 5000000000000000000000))) ≤ Vfield (22449865724923 / 32000000000000)

theorem Zeta5Irrational.V_608 : 1064995098264590386373 / 2000000000000000000000 - 6 * (3 / 40) * -(3441737266643992525549 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8385587508962921 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3489071073368835962193 / 10000000000000000000000)) - 6 * (892018241797966445617 / 10000000000000000000000))) ≤ Vfield (2812723114819 / 4000000000000)

theorem Zeta5Irrational.V_609 : 5334497102387739281797 / 10000000000000000000000 - 6 * (3 / 40) * -(3418873165714944740207 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4197628060898369 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3491908121417462665577 / 10000000000000000000000)) - 6 * (890996357568595104887 / 10000000000000000000000))) ≤ Vfield (22553704112181 / 32000000000000)

theorem Zeta5Irrational.V_610 : 2672004827984150136307 / 5000000000000000000000 - 6 * (3 / 40) * -(339606122226630670097 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8404913612325603 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3494739210209437387999 / 10000000000000000000000)) - 6 * (889977977302413373633 / 10000000000000000000000))) ≤ Vfield (2260562330581 / 3200000000000)

theorem Zeta5Irrational.V_611 : 1070702633856044376569 / 2000000000000000000000 - 6 * (3 / 40) * -(674660239775355582283 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2103640004711281 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1748782181143606580643 / 5000000000000000000000)) - 6 * (888963081020271195629 / 10000000000000000000000))) ≤ Vfield (22657542499439 / 32000000000000)

theorem Zeta5Irrational.V_612 : 1340751914872513778333 / 2500000000000000000000 - 6 * (3 / 40) * -(1675296429871246496299 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1684839075886329 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3500383600064879102301 / 10000000000000000000000)) - 6 * (887951648902143076857 / 10000000000000000000000))) ≤ Vfield (5677365423267 / 8000000000000)