V41: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_493 : 868295763499205084321 / 2000000000000000000000 - 6 * (3 / 40) * -(5991612797366169144041 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1843310758656197 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (198543494771462783499 / 625000000000000000000)) - 6 * (50685243988281521377 / 500000000000000000000))) ≤ Vfield (69586832444983 / 128000000000000)

theorem Zeta5Irrational.V_494 : 2172760564099170449509 / 5000000000000000000000 - 6 * (3 / 40) * -(2990128321072975838143 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (295098965024909 / 400000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3178066124563289035779 / 10000000000000000000000)) - 6 * (506563738093436821663 / 5000000000000000000000))) ≤ Vfield (34833359663509 / 64000000000000)

theorem Zeta5Irrational.V_495 : 2174780902766655282939 / 5000000000000000000000 - 6 * (3 / 40) * -(298445668426235591233 / 500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7381702791417617 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (397429374257384632401 / 1250000000000000000000)) - 6 * (1012551058157293370951 / 10000000000000000000000))) ≤ Vfield (69746606209053 / 128000000000000)

theorem Zeta5Irrational.V_496 : 4353600850820383394063 / 10000000000000000000000 - 6 * (3 / 40) * -(5957582947311654869927 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7385929036174967 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (159040126363004019747 / 500000000000000000000)) - 6 * (25299390571909664953 / 250000000000000000000))) ≤ Vfield (4364155818193 / 8000000000000)

theorem Zeta5Irrational.V_497 : 4357638265377410206641 / 10000000000000000000000 - 6 * (3 / 40) * -(2973132674707548513867 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (739015286404837 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1591084363294408453171 / 5000000000000000000000)) - 6 * (1011401167554778336271 / 10000000000000000000000))) ≤ Vfield (69906379973123 / 128000000000000)

theorem Zeta5Irrational.V_498 : 4361674050520646257781 / 10000000000000000000000 - 6 * (3 / 40) * -(5934960545842017276557 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1478874855835911 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3183533594461034959257 / 10000000000000000000000)) - 6 * (252706922353541398699 / 2500000000000000000000))) ≤ Vfield (34993133427579 / 64000000000000)

theorem Zeta5Irrational.V_499 : 2182854103782376903733 / 5000000000000000000000 - 6 * (3 / 40) * -(5923668507697611716043 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3699296642849219 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (15924485666428705901 / 50000000000000000000)) - 6 * (1010255185687260178931 / 10000000000000000000000))) ≤ Vfield (70066153737193 / 128000000000000)

theorem Zeta5Irrational.V_500 : 4369740737822804691011 / 10000000000000000000000 - 6 * (3 / 40) * -(739048650773106305367 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1480561977544633 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (159312967273261300701 / 500000000000000000000)) - 6 * (1009683653617733165789 / 10000000000000000000000))) ≤ Vfield (17536510154807 / 32000000000000)

theorem Zeta5Irrational.V_501 : 4377800923225096597531 / 10000000000000000000000 - 6 * (3 / 40) * -(5889868698352369758921 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7411235894704171 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1594489899732132286837 / 5000000000000000000000)) - 6 * (1008543493479960270289 / 10000000000000000000000))) ≤ Vfield (35152907191649 / 64000000000000)

theorem Zeta5Irrational.V_502 : 4385854617200366767653 / 10000000000000000000000 - 6 * (3 / 40) * -(5867398793907133653737 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7419652332834149 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3191694975543130921949 / 10000000000000000000000)) - 6 * (503703593583643605337 / 5000000000000000000000))) ≤ Vfield (8808198518421 / 16000000000000)

theorem Zeta5Irrational.V_503 : 2196950915098102340867 / 5000000000000000000000 - 6 * (3 / 40) * -(292248963297407018761 / 500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7428059234639349 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3194404892680992092831 / 10000000000000000000000)) - 6 * (251568678254492200593 / 2500000000000000000000))) ≤ Vfield (35312680955719 / 64000000000000)

theorem Zeta5Irrational.V_504 : 4401942572634988737343 / 10000000000000000000000 - 6 * (3 / 40) * -(2911304944548540144719 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (743645663246217 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3197109569752017389649 / 10000000000000000000000)) - 6 * (1005146049540338767613 / 10000000000000000000000))) ≤ Vfield (17696283918877 / 32000000000000)