V17: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_205 : 729973064772568471697 / 5000000000000000000000 - 6 * (3 / 40) * -(9075704862963237331003 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3964718832390083 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 3774612018114385332253 / 10000000000000000000000) - 6 * (1869593164174766211853 / 10000000000000000000000))) ≤ Vfield (20120314137483 / 128000000000000)

theorem Zeta5Irrational.V_206 : 1463778767588773677433 / 10000000000000000000000 - 6 * (3 / 40) * -(18124201486317085329591 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (248144322472327 / 625000000000000 * (Real.pi + (Real.pi / 2 - 3779442042935979217611 / 10000000000000000000000) - 6 * (373404301033048224383 / 2000000000000000000000))) ≤ Vfield (10088547086377 / 64000000000000)

theorem Zeta5Irrational.V_207 : 1467609937283719993659 / 10000000000000000000000 - 6 * (3 / 40) * -(226213338433879786221 / 125000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3975891626417843 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1892131714307245280953 / 5000000000000000000000) - 6 * (233057553786498956527 / 1250000000000000000000))) ≤ Vfield (809354968321 / 5120000000000)

theorem Zeta5Irrational.V_208 : 367859909938660910269 / 2500000000000000000000 - 6 * (3 / 40) * -(2258750761441776246791 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1990733133017519 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 378907621031154650991 / 1000000000000000000000) - 6 * (1861909867144123045899 / 10000000000000000000000))) ≤ Vfield (634082945103 / 4000000000000)

theorem Zeta5Irrational.V_209 : 1475267876124920720441 / 10000000000000000000000 - 6 * (3 / 40) * -(18043018140451505241589 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (797406622248159 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 3793880422948913718569 / 10000000000000000000000) - 6 * (1859369744002478350221 / 10000000000000000000000))) ≤ Vfield (20347434278567 / 128000000000000)

theorem Zeta5Irrational.V_210 : 1479094647516637661407 / 10000000000000000000000 - 6 * (3 / 40) * -(9008051414162736961301 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1996296097319103 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 474834512651351679093 / 1250000000000000000000) - 6 * (928419994915581758669 / 5000000000000000000000))) ≤ Vfield (10202107156919 / 64000000000000)

theorem Zeta5Irrational.V_211 : 11863359640404745567 / 80000000000000000000 - 6 * (3 / 40) * -(1798925976518522571577 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3998143548603701 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1901731639773101406791 / 5000000000000000000000) - 6 * (927160267134600840667 / 5000000000000000000000))) ≤ Vfield (20460994349109 / 128000000000000)

theorem Zeta5Irrational.V_212 : 185842974980787540947 / 1250000000000000000000 - 6 * (3 / 40) * -(2245311070523984085901 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1000921801322313 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 1904120996085517332403 / 5000000000000000000000) - 6 * (185181130762230820097 / 1000000000000000000000))) ≤ Vfield (1025888719219 / 6400000000000)

theorem Zeta5Irrational.V_213 : 372641545755497074473 / 2500000000000000000000 - 6 * (3 / 40) * -(896789442080253987649 / 500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (801844639324909 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 3813012273070485265727 / 10000000000000000000000) - 6 * (1849312240854789952491 / 10000000000000000000000))) ≤ Vfield (20574554419651 / 128000000000000)

theorem Zeta5Irrational.V_214 : 747193552847302273959 / 5000000000000000000000 - 6 * (3 / 40) * -(17909160216750060519991 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4014751554319121 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 763554831200230249377 / 2000000000000000000000) - 6 * (369364653116313286371 / 2000000000000000000000))) ≤ Vfield (10315667227461 / 64000000000000)

theorem Zeta5Irrational.V_215 : 1498206568979816676777 / 10000000000000000000000 - 6 * (3 / 40) * -(17882602311985011388837 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4020272309864503 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 29863497456978361057 / 78125000000000000000) - 6 * (461086078515075774277 / 2500000000000000000000))) ≤ Vfield (20688114490193 / 128000000000000)

theorem Zeta5Irrational.V_216 : 300404914798402879239 / 2000000000000000000000 - 6 * (3 / 40) * -(17856114752668976953491 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2012892747268141 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 382727286185266192809 / 1000000000000000000000) - 6 * (460468829795916814311 / 2500000000000000000000))) ≤ Vfield (2593111815683 / 16000000000000)