V23: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_277 : 64394112760097439463 / 312500000000000000000 - 6 * (3 / 40) * -(226640407886521376383 / 156250000000000000000) - 2 + 12 * (3 / 40) + 2 * (2391800356751099 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 4461862808171570115379 / 10000000000000000000000) - 6 * (1555195942020142671139 / 10000000000000000000000))) ≤ Vfield (732250745159 / 3200000000000)

theorem Zeta5Irrational.V_278 : 2069284840233233473751 / 10000000000000000000000 - 6 * (3 / 40) * -(2891922184229524885251 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (29967079041083 / 62500000000000 * (Real.pi + (Real.pi / 2 - 2235458931496437735461 / 5000000000000000000000) - 6 * (310328596773444075099 / 2000000000000000000000))) ≤ Vfield (7356627568677 / 32000000000000)

theorem Zeta5Irrational.V_279 : 2077950556166482502539 / 10000000000000000000000 - 6 * (3 / 40) * -(7207220349310972146853 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (600729849303283 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2239972057321476567427 / 5000000000000000000000) - 6 * (774057133603146563687 / 5000000000000000000000))) ≤ Vfield (1847686921441 / 8000000000000)

theorem Zeta5Irrational.V_280 : 2086608769137852456389 / 10000000000000000000000 - 6 * (3 / 40) * -(14369473593852945214773 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4816919335416503 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 280558859864199691039 / 625000000000000000000) - 6 * (308921903521780670773 / 2000000000000000000000))) ≤ Vfield (7424867802851 / 32000000000000)

theorem Zeta5Irrational.V_281 : 2095259492128553921179 / 10000000000000000000000 - 6 * (3 / 40) * -(14324707788288511762533 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4827974445852653 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 4497910985085163099573 / 10000000000000000000000) - 6 * (1541128464976589575851 / 10000000000000000000000))) ≤ Vfield (3729493959969 / 16000000000000)

theorem Zeta5Irrational.V_282 : 2103902738086137537693 / 10000000000000000000000 - 6 * (3 / 40) * -(14280141487690492393971 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4839004300029409 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1126712996706153351403 / 2500000000000000000000) - 6 * (1537670843453434960069 / 10000000000000000000000))) ≤ Vfield (299724321481 / 1280000000000)

theorem Zeta5Irrational.V_283 : 264067314990576284203 / 1250000000000000000000 - 6 * (3 / 40) * -(7117886460851593151109 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2425004535129779 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 4515764951354820672259 / 10000000000000000000000) - 6 * (383559097835192323907 / 2500000000000000000000))) ≤ Vfield (29403234977 / 125000000000)

theorem Zeta5Irrational.V_284 : 2121166850524551193967 / 10000000000000000000000 - 6 * (3 / 40) * -(1419160034343136087147 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (972197785381079 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2262325032459621594699 / 5000000000000000000000) - 6 * (61232994040558072229 / 400000000000000000000))) ≤ Vfield (7561348271199 / 32000000000000)

theorem Zeta5Irrational.V_285 : 266223467841653341547 / 1250000000000000000000 - 6 * (3 / 40) * -(14147622029027548248203 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2435972019204743 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 1133376877931879777319 / 2500000000000000000000) - 6 * (95464748052574244179 / 625000000000000000000))) ≤ Vfield (3797734194143 / 16000000000000)

theorem Zeta5Irrational.V_286 : 2147007263199972397 / 10000000000000000000 - 6 * (3 / 40) * -(1757530176157463034543 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4893780690344377 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 568892516491583260051 / 1250000000000000000000) - 6 * (760362591960730908383 / 5000000000000000000000))) ≤ Vfield (383185431123 / 1600000000000)

theorem Zeta5Irrational.V_287 : 541049295860268807619 / 2500000000000000000000 - 6 * (3 / 40) * -(13973617717453968005883 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4915520336340929 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 228433212307367662667 / 500000000000000000000) - 6 * (75705104221060272141 / 500000000000000000000))) ≤ Vfield (3865974428317 / 16000000000000)

theorem Zeta5Irrational.V_288 : 545339401261763887393 / 2500000000000000000000 - 6 * (3 / 40) * -(3471934488122335850373 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4937164257828069 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 36688650063609893199 / 80000000000000000000) - 6 * (12060518217518261529 / 80000000000000000000))) ≤ Vfield (975023636351 / 4000000000000)