V46: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_553 : 2445721257994797455589 / 5000000000000000000000 - 6 * (3 / 40) * -(4517002183391446592761 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3971523528403931 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3356292705214036771549 / 10000000000000000000000)) - 6 * (941430856712295929961 / 10000000000000000000000))) ≤ Vfield (8075775557973 / 12800000000000)

theorem Zeta5Irrational.V_554 : 2449015504249571333993 / 5000000000000000000000 - 6 * (3 / 40) * -(4500130194867739664721 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7949810374586183 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (671673097886714578427 / 2000000000000000000000)) - 6 * (37625386017259067461 / 400000000000000000000))) ≤ Vfield (20223835197401 / 32000000000000)

theorem Zeta5Irrational.V_555 : 4904615163043244052437 / 10000000000000000000000 - 6 * (3 / 40) * -(4483286624802846121209 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7956567943346689 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3360435148132570495601 / 10000000000000000000000)) - 6 * (187968092181113295817 / 2000000000000000000000))) ≤ Vfield (40516462999739 / 64000000000000)

theorem Zeta5Irrational.V_556 : 2455597492665253910909 / 5000000000000000000000 - 6 * (3 / 40) * -(2233235688812019465853 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1592663955545001 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3362501689903647580097 / 10000000000000000000000)) - 6 * (234762069908735241679 / 2500000000000000000000))) ≤ Vfield (10146313901169 / 16000000000000)

theorem Zeta5Irrational.V_557 : 4917770481058281652449 / 10000000000000000000000 - 6 * (3 / 40) * -(4449684358239905772299 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7970065892294761 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (672913024660701932149 / 2000000000000000000000)) - 6 * (117282262271255301799 / 1250000000000000000000))) ≤ Vfield (40654048209613 / 64000000000000)

theorem Zeta5Irrational.V_558 : 4924341655912681739097 / 10000000000000000000000 - 6 * (3 / 40) * -(4432925472037122503297 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3988403150783981 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1683312728426578497401 / 5000000000000000000000)) - 6 * (937469908111000802269 / 10000000000000000000000))) ≤ Vfield (814456816291 / 1280000000000)

theorem Zeta5Irrational.V_559 : 2465454257784311148601 / 5000000000000000000000 - 6 * (3 / 40) * -(2208097312438626819047 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7983541019995351 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1684341349519044723379 / 5000000000000000000000)) - 6 * (936683701107258921899 / 10000000000000000000000))) ≤ Vfield (40791633419487 / 64000000000000)

theorem Zeta5Irrational.V_560 : 4937471065689844968309 / 10000000000000000000000 - 6 * (3 / 40) * -(549936465386697441599 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1997567515491693 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (842684214577127660523 / 2500000000000000000000)) - 6 * (467949734428600301737 / 5000000000000000000000))) ≤ Vfield (5107553253053 / 8000000000000)

theorem Zeta5Irrational.V_561 : 4950583259927416104161 / 10000000000000000000000 - 6 * (3 / 40) * -(2183084691663832143643 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8003711173798727 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (843708990432839064989 / 2500000000000000000000)) - 6 * (467168447827085537807 / 5000000000000000000000))) ≤ Vfield (20499005617149 / 32000000000000)

theorem Zeta5Irrational.V_562 : 2481839141856494072461 / 5000000000000000000000 - 6 * (3 / 40) * -(2166478856360513774443 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1603425950195627 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (844730708506255858439 / 2500000000000000000000)) - 6 * (466391061526950188599 / 5000000000000000000000))) ≤ Vfield (10283899111043 / 16000000000000)

theorem Zeta5Irrational.V_563 : 4976756181957258726983 / 10000000000000000000000 - 6 * (3 / 40) * -(1074963994651026888953 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4015262953233787 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (845749385385216735619 / 2500000000000000000000)) - 6 * (931235086368221112029 / 10000000000000000000000))) ≤ Vfield (20636590827023 / 32000000000000)

theorem Zeta5Irrational.V_564 : 498981699939495428459 / 1000000000000000000000 - 6 * (3 / 40) * -(853372691111829526357 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2010974938072249 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3387060150084523494817 / 10000000000000000000000)) - 6 * (929695721657504509173 / 10000000000000000000000))) ≤ Vfield (517634585799 / 800000000000)