V07: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_85 : 226771874510981741379 / 5000000000000000000000 - 6 * (3 / 40) * -(14780287962918279265411 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (430806739120629 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 1060808378329828977447 / 5000000000000000000000) - 6 * (41882007321997290791 / 125000000000000000000))) ≤ Vfield (742377785887 / 16000000000000)

theorem Zeta5Irrational.V_86 : 457118096870510924543 / 10000000000000000000000 - 6 * (3 / 40) * -(29488926237277907956139 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2162699649333341 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2129896972254185019601 / 10000000000000000000000) - 6 * (834527990154732413477 / 2500000000000000000000))) ≤ Vfield (598690530973 / 12800000000000)

theorem Zeta5Irrational.V_87 : 460691167579284695889 / 10000000000000000000000 - 6 * (3 / 40) * -(29417786266558953428469 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2171331016832617 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2138141194336938362321 / 10000000000000000000000) - 6 * (3325801225385149696601 / 10000000000000000000000))) ≤ Vfield (1508697083091 / 32000000000000)

theorem Zeta5Irrational.V_88 : 464262962060620974379 / 10000000000000000000000 - 6 * (3 / 40) * -(29347148812585080077493 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (435985641786157 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 429269968176594904411 / 2000000000000000000000) - 6 * (1656812925087286155121 / 5000000000000000000000))) ≤ Vfield (3041335677499 / 64000000000000)

theorem Zeta5Irrational.V_89 : 233916740612939341691 / 5000000000000000000000 - 6 * (3 / 40) * -(3659625853224161050433 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (437698325677629 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2154523321717564278481 / 10000000000000000000000) - 6 * (1320633347875011933 / 4000000000000000000))) ≤ Vfield (191579824301 / 4000000000000)

theorem Zeta5Irrational.V_90 : 47140272598544088727 / 1000000000000000000000 - 6 * (3 / 40) * -(29207353403930246574293 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (109851083505783 / 500000000000000 * (Real.pi + (Real.pi / 2 - 432532407747580506091 / 2000000000000000000000) - 6 * (1644835690550822215319 / 5000000000000000000000))) ≤ Vfield (3089218700133 / 64000000000000)

theorem Zeta5Irrational.V_91 : 118742674312179046039 / 2500000000000000000000 - 6 * (3 / 40) * -(29138181787976365168227 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (220551872138747 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 2170766386127115701763 / 10000000000000000000000) - 6 * (655577508409682210587 / 2000000000000000000000))) ≤ Vfield (62263204229 / 1280000000000)

theorem Zeta5Irrational.V_92 : 478537395924140096139 / 10000000000000000000000 - 6 * (3 / 40) * -(1816842834888117217761 / 625000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2213983162046051 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 544709187640218728401 / 2500000000000000000000) - 6 * (25517418505229754007 / 78125000000000000000))) ≤ Vfield (3137101722767 / 64000000000000)

theorem Zeta5Irrational.V_93 : 241051411459588228539 / 5000000000000000000000 - 6 * (3 / 40) * -(14500628815202590003913 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1111207682350181 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2186873511406957655783 / 10000000000000000000000) - 6 * (3254695233748423021389 / 10000000000000000000000))) ≤ Vfield (790260808521 / 16000000000000)

theorem Zeta5Irrational.V_94 : 7588546549067481217 / 156250000000000000000 - 6 * (3 / 40) * -(361668653152000194621 / 125000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2230815694917233 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2194877040918014085383 / 10000000000000000000000) - 6 * (1621641182458017941551 / 5000000000000000000000))) ≤ Vfield (3184984745401 / 64000000000000)

theorem Zeta5Irrational.V_95 : 489229865493091729373 / 10000000000000000000000 - 6 * (3 / 40) * -(14433091499673113264557 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (22391845114063 / 100000000000000 * (Real.pi + (Real.pi / 2 - 1101423852208921727903 / 5000000000000000000000) - 6 * (807997210730837352441 / 2500000000000000000000))) ≤ Vfield (1604463128359 / 32000000000000)

theorem Zeta5Irrational.V_96 : 123197870720513080647 / 2500000000000000000000 - 6 * (3 / 40) * -(14399661886339595032899 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2247522166198741 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2210785860481439136199 / 10000000000000000000000) - 6 * (3220812599981731487411 / 10000000000000000000000))) ≤ Vfield (646573553607 / 12800000000000)