V14: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_169 : 1071890317176583928039 / 10000000000000000000000 - 6 * (3 / 40) * -(21305693393452711451859 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3363698176688539 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1622404481577912283161 / 5000000000000000000000) - 6 * (548450874824163752413 / 2500000000000000000000))) ≤ Vfield (7241257871269 / 64000000000000)

theorem Zeta5Irrational.V_170 : 1075037203912298076033 / 10000000000000000000000 - 6 * (3 / 40) * -(10638119306132417311027 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1684450974174337 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 812370766620299188099 / 2500000000000000000000) - 6 * (273815285801581864431 / 1250000000000000000000))) ≤ Vfield (907960027007 / 8000000000000)

theorem Zeta5Irrational.V_171 : 539091550334963103107 / 5000000000000000000000 - 6 * (3 / 40) * -(5311717583689524422171 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (105440552949823 / 312500000000000 * (Real.pi + (Real.pi / 2 - 406768561615688575177 / 1250000000000000000000) - 6 * (1093627877775185649047 / 5000000000000000000000))) ≤ Vfield (7286102560843 / 64000000000000)

theorem Zeta5Irrational.V_172 : 1081328008072146210999 / 10000000000000000000000 - 6 * (3 / 40) * -(21217588054326763577179 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3379285451844349 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1629402640588147556519 / 5000000000000000000000) - 6 * (2184003797519659522247 / 10000000000000000000000))) ≤ Vfield (730852490563 / 6400000000000)

theorem Zeta5Irrational.V_173 : 271117981685262172049 / 2500000000000000000000 - 6 * (3 / 40) * -(1059419563440124122021 / 500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3384465257433817 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 3263453469630001012291 / 10000000000000000000000) - 6 * (2180766304264109440283 / 10000000000000000000000))) ≤ Vfield (7330947250417 / 64000000000000)

theorem Zeta5Irrational.V_174 : 217522971459627535867 / 2000000000000000000000 - 6 * (3 / 40) * -(5289819870100654850123 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1694818573808583 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 3268093096395075635043 / 10000000000000000000000) - 6 * (2177543168845947543807 / 10000000000000000000000))) ≤ Vfield (1838342398801 / 16000000000000)

theorem Zeta5Irrational.V_175 : 1093897756559963010019 / 10000000000000000000000 - 6 * (3 / 40) * -(2637663615683673257443 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (339995732619773 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 1638673407935689605673 / 5000000000000000000000) - 6 * (2171139549275033092439 / 10000000000000000000000))) ≤ Vfield (3699107142389 / 32000000000000)

theorem Zeta5Irrational.V_176 : 4400706843271805573 / 40000000000000000000 - 6 * (3 / 40) * -(10521836246531778932779 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (852561568430141 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 1643283369413787703769 / 5000000000000000000000) - 6 * (135299506569951335849 / 625000000000000000000))) ≤ Vfield (465191185897 / 4000000000000)

theorem Zeta5Irrational.V_177 : 1106451725023094177469 / 10000000000000000000000 - 6 * (3 / 40) * -(10493183176854784838949 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3420504272016681 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 3295753160068787053413 / 10000000000000000000000) - 6 * (431700003932662026033 / 2000000000000000000000))) ≤ Vfield (3743951831963 / 32000000000000)

theorem Zeta5Irrational.V_178 : 222544560823413658539 / 2000000000000000000000 - 6 * (3 / 40) * -(2092938674339300144207 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (686146319740731 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 66098127401491722431 / 200000000000000000000) - 6 * (1076131246361408251279 / 5000000000000000000000))) ≤ Vfield (15065496707 / 128000000000)

theorem Zeta5Irrational.V_179 : 1118989953032259600469 / 10000000000000000000000 - 6 * (3 / 40) * -(20872729962077034974551 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3440928527273287 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 3314026655088241252493 / 10000000000000000000000) - 6 * (429215748043235457857 / 2000000000000000000000))) ≤ Vfield (3788796521537 / 32000000000000)

theorem Zeta5Irrational.V_180 : 45010127067671446827 / 400000000000000000000 - 6 * (3 / 40) * -(20816392372260701008297 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3451095327176937 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 332311429720360928943 / 1000000000000000000000) - 6 * (2139947993750407451587 / 10000000000000000000000))) ≤ Vfield (952804716581 / 8000000000000)