V56: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_673 : 6122387374240496023273 / 10000000000000000000000 - 6 * (3 / 40) * -(1623057085064450056693 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1837994838888139 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1858030802236809204597 / 5000000000000000000000)) - 6 * (407151059969191178087 / 5000000000000000000000))) ≤ Vfield (54051600444471 / 64000000000000)

theorem Zeta5Irrational.V_674 : 389249904457505137419 / 625000000000000000000 - 6 * (3 / 40) * -(1395321619366648151237 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (9295913345121237 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1872313611514181767439 / 5000000000000000000000)) - 6 * (805062351806162380989 / 10000000000000000000000))) ≤ Vfield (27652481574401 / 32000000000000)

theorem Zeta5Irrational.V_675 : 6332505844415552817503 / 10000000000000000000000 - 6 * (3 / 40) * -(586328612943406901771 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1880131741613021 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3772575766913640194333 / 10000000000000000000000)) - 6 * (796130138632003110727 / 10000000000000000000000))) ≤ Vfield (56558325853133 / 64000000000000)

theorem Zeta5Irrational.V_676 : 1287186464959551226363 / 2000000000000000000000 - 6 * (3 / 40) * -(954842976206395349259 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (9504249753191331 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (379993042391329462331 / 1000000000000000000000)) - 6 * (196872197076237575761 / 2500000000000000000000))) ≤ Vfield (7226461069683 / 8000000000000)

theorem Zeta5Irrational.V_677 : 6639630455055536452119 / 10000000000000000000000 - 6 * (3 / 40) * -(532950666319523470387 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (9708116285978029 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (770588915703197956467 / 2000000000000000000000)) - 6 * (385508999245285394263 / 5000000000000000000000))) ≤ Vfield (30159206983063 / 32000000000000)

theorem Zeta5Irrational.V_678 : 3419630995230294538113 / 5000000000000000000000 - 6 * (3 / 40) * -(64069730353516965177 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4953894434510747 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3903831421400330573611 / 10000000000000000000000)) - 6 * (377769635349620863439 / 5000000000000000000000))) ≤ Vfield (15706284843697 / 16000000000000)

theorem Zeta5Irrational.V_679 : 3613476445799885952621 / 5000000000000000000000 - 6 * (3 / 40) * (158852024015426556119 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5147761580900357 / 5000000000000000 * (Real.pi + 2 * (481773868711436053381 / 1250000000000000000000) - 6 * (727187456097735281609 / 10000000000000000000000))) ≤ Vfield (4239911887007 / 4000000000000)

theorem Zeta5Irrational.V_680 : 1520034531928750963607 / 2000000000000000000000 - 6 * (3 / 40) * (1344768187442564119861 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5334587942785359 / 5000000000000000 * (Real.pi + 2 * (3765169602758050855633 / 10000000000000000000000) - 6 * (21931411260193838793 / 312500000000000000000))) ≤ Vfield (18213010252359 / 16000000000000)

theorem Zeta5Irrational.V_681 : 3979981422045415289587 / 5000000000000000000000 - 6 * (3 / 40) * (1003562467551241527391 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (11030178193452383 / 10000000000000000 * (Real.pi + 2 * (1841128949775744109199 / 5000000000000000000000) - 6 * (339453879744246898597 / 5000000000000000000000))) ≤ Vfield (1946637295669 / 1600000000000)

theorem Zeta5Irrational.V_682 : 216072312191625710833 / 250000000000000000000 - 6 * (3 / 40) * (3213177334616844766239 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5859433948417073 / 5000000000000000 * (Real.pi + 2 * (1766052720082905933429 / 5000000000000000000000) - 6 * (639121915477979050969 / 10000000000000000000000))) ≤ Vfield (2746637295669 / 2000000000000)

theorem Zeta5Irrational.V_683 : 247074633638366187549 / 250000000000000000000 - 6 * (3 / 40) * (1052158574414174657667 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (12987144889918067 / 10000000000000000 * (Real.pi + 2 * (102527157563947062571 / 312500000000000000000) - 6 * (288426718122331681813 / 5000000000000000000000))) ≤ Vfield (6746637295669 / 4000000000000)