V04: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_49 : 9367832807386358049 / 500000000000000000000 - 6 * (3 / 40) * -(37075617054825365057033 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1375219235839097 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 683323396048354980263 / 5000000000000000000000) - 6 * (2 * (62409962799765955357 / 250000000000000000000)))) ≤ Vfield (605192942919 / 32000000000000)

theorem Zeta5Irrational.V_50 : 19054250695858538469 / 1000000000000000000000 - 6 * (3 / 40) * -(7388834199649120704961 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (173371626818641 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 1378180571218092944099 / 10000000000000000000000) - 6 * (2 * (1239276500758368893079 / 5000000000000000000000)))) ≤ Vfield (153895531447 / 8000000000000)

theorem Zeta5Irrational.V_51 : 19691116530249562487 / 1000000000000000000000 - 6 * (3 / 40) * -(36686351439827391625567 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1410186702539329 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 140094889551191353099 / 1000000000000000000000) - 6 * (2 * (1221993650998643614353 / 5000000000000000000000)))) ≤ Vfield (318180245763 / 16000000000000)

theorem Zeta5Irrational.V_52 : 203275770246830504773 / 10000000000000000000000 - 6 * (3 / 40) * -(36435012247301481743849 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1433024399286347 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1423334185029087098537 / 10000000000000000000000) - 6 * (2 * (150677267173378803647 / 625000000000000000000)))) ≤ Vfield (41071178579 / 2000000000000)

theorem Zeta5Irrational.V_53 : 107996420276222433859 / 5000000000000000000000 - 6 * (3 / 40) * -(35950526579446718972183 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1477641267294771 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 146702560506701594711 / 1000000000000000000000) - 6 * (2 * (2348409106350313720017 / 10000000000000000000000)))) ≤ Vfield (34934779437 / 1600000000000)

theorem Zeta5Irrational.V_54 : 114346879504294972067 / 5000000000000000000000 - 6 * (3 / 40) * -(35488432866774594506247 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1520949867903277 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1509382020844949857689 / 10000000000000000000000) - 6 * (4581227649370826993687 / 10000000000000000000000))) ≤ Vfield (92531540027 / 4000000000000)

theorem Zeta5Irrational.V_55 : 127023652061630830299 / 5000000000000000000000 - 6 * (3 / 40) * -(34623757699024104622901 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (40101574722821 / 250000000000000 * (Real.pi + (Real.pi / 2 - 1590513943220726835857 / 10000000000000000000000) - 6 * (218681344812415938491 / 500000000000000000000))) ≤ Vfield (6432545181 / 250000000000)

theorem Zeta5Irrational.V_56 : 32987613906975619173 / 1250000000000000000000 - 6 * (3 / 40) * -(34306346441541073575049 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1635279580656621 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 324186506259879103831 / 2000000000000000000000) - 6 * (1075033352401525906013 / 2500000000000000000000))) ≤ Vfield (213931144553 / 8000000000000)

theorem Zeta5Irrational.V_57 : 13441203810162759651 / 500000000000000000000 - 6 * (3 / 40) * -(17075670345849735943963 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1650666509071031 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 817957512773989300277 / 5000000000000000000000) - 6 * (2132376865167301685317 / 5000000000000000000000))) ≤ Vfield (435951987867 / 16000000000000)

theorem Zeta5Irrational.V_58 : 34218102323501764669 / 1250000000000000000000 - 6 * (3 / 40) * -(33998700991624565113719 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (83295566229917 / 500000000000000 * (Real.pi + (Real.pi / 2 - 66030073509107242779 / 400000000000000000000) - 6 * (846047177419245798601 / 2000000000000000000000))) ≤ Vfield (111010421657 / 4000000000000)

theorem Zeta5Irrational.V_59 : 27866314079307059799 / 1000000000000000000000 - 6 * (3 / 40) * -(33848356193919409894199 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (42025447340579 / 250000000000000 * (Real.pi + (Real.pi / 2 - 208180859025354406709 / 1250000000000000000000) - 6 * (4196545340860832545349 / 10000000000000000000000))) ≤ Vfield (452131385389 / 16000000000000)

theorem Zeta5Irrational.V_60 : 4392521797998957757 / 156250000000000000000 - 6 * (3 / 40) * -(33774023019545920101553 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (844260248280909 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 418185598816008147827 / 2500000000000000000000) - 6 * (1045000009396149589471 / 2500000000000000000000))) ≤ Vfield (912352469539 / 32000000000000)