V34: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_409 : 1809669122496870992029 / 5000000000000000000000 - 6 * (3 / 40) * -(408529462049720624371 / 500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1320763270114671 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2918193984890556559269 / 10000000000000000000000)) - 6 * (1130861477778600441087 / 10000000000000000000000))) ≤ Vfield (436103903921 / 1000000000000)

theorem Zeta5Irrational.V_410 : 28420032908242764527 / 78125000000000000000 - 6 * (3 / 40) * -(8110808437737774119867 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (103497492949001 / 156250000000000 * (Real.pi + (Real.pi / 2 - 2 * (1462579464314678080479 / 5000000000000000000000)) - 6 * (563735968840652122499 / 5000000000000000000000))) ≤ Vfield (219376251837 / 500000000000)

theorem Zeta5Irrational.V_411 : 91174111991140909019 / 250000000000000000000 - 6 * (3 / 40) * -(8081051519608223970771 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6633828483993989 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (292862872001000197323 / 1000000000000000000000)) - 6 * (1125788557400433642409 / 10000000000000000000000))) ≤ Vfield (880153607101 / 2000000000000)

theorem Zeta5Irrational.V_412 : 3656156290323998442747 / 10000000000000000000000 - 6 * (3 / 40) * -(503211430390812632561 / 625000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6643802400937281 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (586418022000673760631 / 2000000000000000000000)) - 6 * (224822538986222456981 / 2000000000000000000000))) ≤ Vfield (441401103427 / 1000000000000)

theorem Zeta5Irrational.V_413 : 733067931964476973299 / 2000000000000000000000 - 6 * (3 / 40) * -(8021802015363241262467 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6653761367102819 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2935543137456839238447 / 10000000000000000000000)) - 6 * (1122444294482276282733 / 10000000000000000000000))) ≤ Vfield (885450806607 / 2000000000000)

theorem Zeta5Irrational.V_414 : 146980584145210727889 / 400000000000000000000 - 6 * (3 / 40) * -(7992308389251518931253 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6663705449522809 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (587797568187209344421 / 2000000000000000000000)) - 6 * (560391650420402333093 / 5000000000000000000000))) ≤ Vfield (22202485159 / 50000000000)

theorem Zeta5Irrational.V_415 : 1841840568597262780059 / 5000000000000000000000 - 6 * (3 / 40) * -(1592580298959499282641 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3336817357365023 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2942424258727729199681 / 10000000000000000000000)) - 6 * (559564829681922406319 / 5000000000000000000000))) ≤ Vfield (890748006113 / 2000000000000)

theorem Zeta5Irrational.V_416 : 923209818979901109979 / 2500000000000000000000 - 6 * (3 / 40) * -(1983395205848588651167 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6683549228763111 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2945852428842548212577 / 10000000000000000000000)) - 6 * (558741657985630589877 / 5000000000000000000000))) ≤ Vfield (446698302933 / 1000000000000)

theorem Zeta5Irrational.V_417 : 3701989035167639417921 / 10000000000000000000000 - 6 * (3 / 40) * -(3952172935448006424207 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1338689811434299 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2949272389017869224799 / 10000000000000000000000)) - 6 * (1115844217138206506899 / 10000000000000000000000))) ≤ Vfield (896045205619 / 2000000000000)

theorem Zeta5Irrational.V_418 : 926640194319229491321 / 2500000000000000000000 - 6 * (3 / 40) * -(1972440095724352398719 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6698393484618157 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2950979302097091334933 / 10000000000000000000000)) - 6 * (278756841963755830087 / 2500000000000000000000))) ≤ Vfield (1794739010991 / 4000000000000)

theorem Zeta5Irrational.V_419 : 3711130430258663998133 / 10000000000000000000000 - 6 * (3 / 40) * -(1968799034391279262693 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6703334265020653 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (738171044180126359817 / 2500000000000000000000)) - 6 * (222842461977562569229 / 2000000000000000000000))) ≤ Vfield (224673451343 / 500000000000)

theorem Zeta5Irrational.V_420 : 1857848998010661530569 / 5000000000000000000000 - 6 * (3 / 40) * -(786065307311242032783 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6708271406437353 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (5908774035059268563 / 20000000000000000000)) - 6 * (278349759174727094639 / 2500000000000000000000))) ≤ Vfield (1800036210497 / 4000000000000)