V43: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_517 : 452972286411765166689 / 1000000000000000000000 - 6 * (3 / 40) * -(5471342198361810627931 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7569548156750547 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1619843380159431640001 / 5000000000000000000000)) - 6 * (246897195377139917649 / 2500000000000000000000))) ≤ Vfield (18335378975157 / 32000000000000)

theorem Zeta5Irrational.V_518 : 4545581204063767592191 / 10000000000000000000000 - 6 * (3 / 40) * -(5428288780241887976119 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3793010209705643 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3244918614347308492101 / 10000000000000000000000)) - 6 * (492729102817023540833 / 5000000000000000000000))) ≤ Vfield (2301908232149 / 4000000000000)

theorem Zeta5Irrational.V_519 : 114035360878214065547 / 250000000000000000000 - 6 * (3 / 40) * -(1346354981867526213689 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1900614247915729 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3250130866753457043071 / 10000000000000000000000)) - 6 * (245835339961437818473 / 2500000000000000000000))) ≤ Vfield (18495152739227 / 32000000000000)

theorem Zeta5Irrational.V_520 : 228861131834866065769 / 500000000000000000000 - 6 * (3 / 40) * -(5342734064375408869163 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7618858104495957 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1627661826322526439887 / 5000000000000000000000)) - 6 * (245309524326254742311 / 2500000000000000000000))) ≤ Vfield (9287519810631 / 16000000000000)

theorem Zeta5Irrational.V_521 : 4608764267010799293243 / 10000000000000000000000 - 6 * (3 / 40) * -(131447627616321705781 / 250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3825777431750391 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (816412839554078022283 / 2500000000000000000000)) - 6 * (61066984094740587393 / 625000000000000000000))) ≤ Vfield (4683703346333 / 8000000000000)

theorem Zeta5Irrational.V_522 : 290012920163202756309 / 625000000000000000000 - 6 * (3 / 40) * -(323361855717053871977 / 625000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7684112495394717 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3275902783813129556593 / 10000000000000000000000)) - 6 * (486479009297971681703 / 5000000000000000000000))) ≤ Vfield (9447293574701 / 16000000000000)

theorem Zeta5Irrational.V_523 : 467155062520418752421 / 1000000000000000000000 - 6 * (3 / 40) * -(19884280940523666413 / 39062500000000000000) - 2 + 12 * (3 / 40) + 2 * (308661310447811 / 400000000000000 * (Real.pi + (Real.pi / 2 - 2 * (410759870046985860257 / 1250000000000000000000)) - 6 * (121111977243712197883 / 1250000000000000000000))) ≤ Vfield (297724389273 / 500000000000)

theorem Zeta5Irrational.V_524 : 4685015939116695900419 / 10000000000000000000000 - 6 * (3 / 40) * -(5054674252401897476843 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3865224920526233 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1645218759627469874719 / 5000000000000000000000)) - 6 * (193432477556515180871 / 2000000000000000000000))) ≤ Vfield (19123153518409 / 32000000000000)

theorem Zeta5Irrational.V_525 : 4698463145940359342123 / 10000000000000000000000 - 6 * (3 / 40) * -(5019099591638264099907 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7744341911063601 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3294782395019543481039 / 10000000000000000000000)) - 6 * (120679778530763911613 / 1250000000000000000000))) ≤ Vfield (9595973061673 / 16000000000000)

theorem Zeta5Irrational.V_526 : 2355946147153874507959 / 5000000000000000000000 - 6 * (3 / 40) * -(155739094938564335577 / 312500000000000000000) - 2 + 12 * (3 / 40) + 2 * (3879104552789353 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3299113666383077039093 / 10000000000000000000000)) - 6 * (481861628499394707899 / 5000000000000000000000))) ≤ Vfield (19260738728283 / 32000000000000)

theorem Zeta5Irrational.V_527 : 589825013964311084409 / 1250000000000000000000 - 6 * (3 / 40) * -(4965973772639253023391 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (776513341618149 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1650637112411661779237 / 5000000000000000000000)) - 6 * (481434595765630853183 / 5000000000000000000000))) ≤ Vfield (38590270061503 / 64000000000000)

theorem Zeta5Irrational.V_528 : 4725303432655770558119 / 10000000000000000000000 - 6 * (3 / 40) * -(2474163850341135916233 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3886025778874623 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (20646446321052335661 / 62500000000000000000)) - 6 * (48100869635968825743 / 500000000000000000000))) ≤ Vfield (966476566661 / 1600000000000)