V03: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_37 : 21048393928938516659 / 2000000000000000000000 - 6 * (3 / 40) * -(41224495654581728135701 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (20571602866087 / 200000000000000 * (Real.pi + (Real.pi / 2 - 1024975616002557514417 / 10000000000000000000000) - 6 * (2 * (630029876112921474829 / 2000000000000000000000)))) ≤ Vfield (1322471389 / 125000000000)

theorem Zeta5Irrational.V_38 : 113091190668515940261 / 10000000000000000000000 - 6 * (3 / 40) * -(40746414146378761469201 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1066457167564641 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1062441486169975621307 / 10000000000000000000000) - 6 * (2 * (3064563126433209565083 / 10000000000000000000000)))) ≤ Vfield (4549323561 / 400000000000)

theorem Zeta5Irrational.V_39 : 120934255497089002089 / 10000000000000000000000 - 6 * (3 / 40) * -(8058029952033732590147 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (551517150526617 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 549296596867263340437 / 5000000000000000000000) - 6 * (2 * (1492843499897578576763 / 5000000000000000000000)))) ≤ Vfield (12166846693 / 1000000000000)

theorem Zeta5Irrational.V_40 : 152245145501698111849 / 10000000000000000000000 - 6 * (3 / 40) * -(38648533017005889889951 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (309646954762597 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 154038970346850627713 / 1250000000000000000000) - 6 * (2 * (2722372641804015738093 / 10000000000000000000000)))) ≤ Vfield (3068199571 / 200000000000)

theorem Zeta5Irrational.V_41 : 158638233080768093329 / 10000000000000000000000 - 6 * (3 / 40) * -(38343528723300591384029 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (126452844113181 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 251570460987800448443 / 2000000000000000000000) - 6 * (2 * (1338338273905248023557 / 5000000000000000000000)))) ≤ Vfield (255845148549 / 16000000000000)

theorem Zeta5Irrational.V_42 : 165027236114105152063 / 10000000000000000000000 - 6 * (3 / 40) * -(4755944063788979246611 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1289947507212017 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 160357918015002146829 / 1250000000000000000000) - 6 * (2 * (2633224767274595554807 / 10000000000000000000000)))) ≤ Vfield (133117165709 / 8000000000000)

theorem Zeta5Irrational.V_43 : 168220207556483795939 / 10000000000000000000000 - 6 * (3 / 40) * -(37902785946772965577681 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (130247102379597 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 647589960594501769007 / 5000000000000000000000) - 6 * (2 * (1306141833947405153479 / 5000000000000000000000)))) ≤ Vfield (108571569141 / 6400000000000)

theorem Zeta5Irrational.V_44 : 42853039954403033183 / 2500000000000000000000 - 6 * (3 / 40) * -(7552017049555776737193 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1314875265678743 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 653687650225280262137 / 5000000000000000000000) - 6 * (2 * (1295919005291486724873 / 5000000000000000000000)))) ≤ Vfield (276623514287 / 16000000000000)

theorem Zeta5Irrational.V_45 : 174603093547929167631 / 10000000000000000000000 - 6 * (3 / 40) * -(7523878456169585870279 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1327163577242599 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1319452846275249601221 / 10000000000000000000000) - 6 * (2 * (514373683695854022843 / 2000000000000000000000)))) ≤ Vfield (563636211443 / 32000000000000)

theorem Zeta5Irrational.V_46 : 177793009397219830411 / 10000000000000000000000 - 6 * (3 / 40) * -(37480651333224899688083 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1339339149440871 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1331415769064528188357 / 10000000000000000000000) - 6 * (2 * (510471313435554669691 / 2000000000000000000000)))) ≤ Vfield (71753174289 / 4000000000000)

theorem Zeta5Irrational.V_47 : 180981908014677709171 / 10000000000000000000000 - 6 * (3 / 40) * -(3734380897942405989187 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1351405029475109 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 335816783738066689991 / 2500000000000000000000) - 6 * (2 * (2533285111816478099343 / 10000000000000000000000)))) ≤ Vfield (584414577181 / 32000000000000)

theorem Zeta5Irrational.V_48 : 184169790048865831767 / 10000000000000000000000 - 6 * (3 / 40) * -(18604406978856690119019 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1363364129701323 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 677504937366921683649 / 5000000000000000000000) - 6 * (2 * (1257318810145620304883 / 5000000000000000000000)))) ≤ Vfield (11896075201 / 640000000000)