V49: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_589 : 5210003340544330517601 / 10000000000000000000000 - 6 * (3 / 40) * -(3720263456569547413113 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8268682368393859 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3454553289605606480941 / 10000000000000000000000)) - 6 * (452280829327876491589 / 5000000000000000000000))) ≤ Vfield (5469688648751 / 8000000000000)

theorem Zeta5Irrational.V_590 : 1303705082763694364061 / 2500000000000000000000 - 6 * (3 / 40) * -(370850198855605597403 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4136793197920123 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (138240370157103788799 / 400000000000000000000)) - 6 * (452014206241029862917 / 5000000000000000000000))) ≤ Vfield (43809428383637 / 64000000000000)

theorem Zeta5Irrational.V_591 : 521963500234258913999 / 1000000000000000000000 - 6 * (3 / 40) * -(924188584376590225871 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8278487518229287 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (86436591379470589641 / 250000000000000000000)) - 6 * (903496108261826234217 / 10000000000000000000000))) ≤ Vfield (21930673788633 / 32000000000000)

theorem Zeta5Irrational.V_592 : 5224447356639949858109 / 10000000000000000000000 - 6 * (3 / 40) * -(737004094199034598467 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1656677148143517 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (345891649639318181503 / 1000000000000000000000)) - 6 * (180592948645021209329 / 2000000000000000000000))) ≤ Vfield (8782653354179 / 12800000000000)

theorem Zeta5Irrational.V_593 : 2614628698087911415639 / 5000000000000000000000 - 6 * (3 / 40) * -(14693201426844845997 / 40000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1036035133555813 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3460367780595662617999 / 10000000000000000000000)) - 6 * (180486862922668628021 / 2000000000000000000000))) ≤ Vfield (10991296491131 / 16000000000000)

theorem Zeta5Irrational.V_594 : 654258140396994550749 / 1250000000000000000000 - 6 * (3 / 40) * -(3661593962456670299233 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1658634701308447 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (216363594425149969639 / 625000000000000000000)) - 6 * (901904819679311450819 / 10000000000000000000000))) ≤ Vfield (44017105158153 / 64000000000000)

theorem Zeta5Irrational.V_595 : 1047774107972578046817 / 2000000000000000000000 - 6 * (3 / 40) * -(729980251229337430647 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4149031530057929 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3463265690020702793097 / 10000000000000000000000)) - 6 * (901376255687055180941 / 10000000000000000000000))) ≤ Vfield (22034512175891 / 32000000000000)

theorem Zeta5Irrational.V_596 : 2621836824227980718709 / 5000000000000000000000 - 6 * (3 / 40) * -(727644441161763215397 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (41514748671317 / 50000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1732356160624546634617 / 5000000000000000000000)) - 6 * (900848619911829885433 / 10000000000000000000000))) ≤ Vfield (44120943545411 / 64000000000000)

theorem Zeta5Irrational.V_597 : 5248474451171310757761 / 10000000000000000000000 - 6 * (3 / 40) * -(453319597447812848417 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (519239595879119 / 625000000000000 * (Real.pi + (Real.pi / 2 - 2 * (69323148149546782071 / 200000000000000000000)) - 6 * (225080477410010679099 / 2500000000000000000000))) ≤ Vfield (276080392119 / 400000000000)

theorem Zeta5Irrational.V_598 : 656659118777736086491 / 1250000000000000000000 - 6 * (3 / 40) * -(3614904945718563204627 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8312714464589487 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3467600951686490417953 / 10000000000000000000000)) - 6 * (899796122169194200699 / 10000000000000000000000))) ≤ Vfield (44224781932669 / 64000000000000)

theorem Zeta5Irrational.V_599 : 5258069147817461612193 / 10000000000000000000000 - 6 * (3 / 40) * -(3603266672578664989709 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (41587962654427 / 50000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3469042956848913514917 / 10000000000000000000000)) - 6 * (899271254807820140911 / 10000000000000000000000))) ≤ Vfield (22138350563149 / 32000000000000)

theorem Zeta5Irrational.V_600 : 131571576154115446801 / 250000000000000000000 - 6 * (3 / 40) * -(897910482158703023617 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2080616934497523 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3470483425928326162743 / 10000000000000000000000)) - 6 * (898747304875433424139 / 10000000000000000000000))) ≤ Vfield (44328620319927 / 64000000000000)