V16: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_193 : 1379119536463717589619 / 10000000000000000000000 - 6 * (3 / 40) * -(1874058101002048808097 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1922722546692823 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 3671120904872284070399 / 10000000000000000000000) - 6 * (1926179010437621127729 / 10000000000000000000000))) ≤ Vfield (2365991674599 / 16000000000000)

theorem Zeta5Irrational.V_194 : 1394565529352076953773 / 10000000000000000000000 - 6 * (3 / 40) * -(18625649088734036599843 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (120888982420927 / 312500000000000 * (Real.pi + (Real.pi / 2 - 922786131046177653937 / 2500000000000000000000) - 6 * (1915004440272120860647 / 10000000000000000000000))) ≤ Vfield (4788763384469 / 32000000000000)

theorem Zeta5Irrational.V_195 : 175284948537260638459 / 1250000000000000000000 - 6 * (3 / 40) * -(4642168678222045719597 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3879897470497971 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1850550138337685246867 / 5000000000000000000000) - 6 * (1909489605510279217527 / 10000000000000000000000))) ≤ Vfield (9634306804209 / 64000000000000)

theorem Zeta5Irrational.V_196 : 1409987701160100614743 / 10000000000000000000000 - 6 * (3 / 40) * -(4628005776724920317491 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3891313812414451 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 742203816691221276071 / 2000000000000000000000) - 6 * (1904022148523259736843 / 10000000000000000000000))) ≤ Vfield (242277170987 / 1600000000000)

theorem Zeta5Irrational.V_197 : 283537975419536278287 / 2000000000000000000000 - 6 * (3 / 40) * -(18455690634264303292773 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3902696758883327 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 744180251624464067841 / 2000000000000000000000) - 6 * (1898601394724880011151 / 10000000000000000000000))) ≤ Vfield (9747866874751 / 64000000000000)

theorem Zeta5Irrational.V_198 : 1425386125249237081831 / 10000000000000000000000 - 6 * (3 / 40) * -(73598694878360117537 / 40000000000000000000) - 2 + 12 * (3 / 40) + 2 * (782809320253901 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 3730747109815750035747 / 10000000000000000000000) - 6 * (1893226682901490889443 / 10000000000000000000000))) ≤ Vfield (4902323455011 / 32000000000000)

theorem Zeta5Irrational.V_199 : 716538227366047056267 / 5000000000000000000000 - 6 * (3 / 40) * -(18343968847235335596581 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3925363626725593 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 935139235828401014473 / 2500000000000000000000) - 6 * (47197434121825702827 / 250000000000000000000))) ≤ Vfield (9861426945293 / 64000000000000)

theorem Zeta5Irrational.V_200 : 360190218660640124399 / 2500000000000000000000 - 6 * (3 / 40) * -(914428627999259877791 / 500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3936648118276669 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 468791382389424016227 / 1250000000000000000000) - 6 * (117663300322781655899 / 625000000000000000000))) ≤ Vfield (2479551745141 / 16000000000000)

theorem Zeta5Irrational.V_201 : 722300435672506061083 / 5000000000000000000000 - 6 * (3 / 40) * -(18260989071053057397457 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (394227825117491 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 3755204815637543892277 / 10000000000000000000000) - 6 * (1879987114489769237383 / 10000000000000000000000))) ≤ Vfield (19893193996399 / 128000000000000)

theorem Zeta5Irrational.V_202 : 1448439394055990394649 / 10000000000000000000000 - 6 * (3 / 40) * -(18233481457763565163467 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1973950177451433 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 3760069753527545238699 / 10000000000000000000000) - 6 * (187737238068757978517 / 1000000000000000000000))) ≤ Vfield (1994997403167 / 12800000000000)

theorem Zeta5Irrational.V_203 : 1452276443906651095289 / 10000000000000000000000 - 6 * (3 / 40) * -(18206049303829734797543 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1976757231857117 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 1882462954591030446627 / 5000000000000000000000) - 6 * (937384263878327770559 / 5000000000000000000000))) ≤ Vfield (20006754066941 / 128000000000000)

theorem Zeta5Irrational.V_204 : 145611202202684841337 / 1000000000000000000000 - 6 * (3 / 40) * -(18178692196381109013093 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3959120611619847 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 3769773318745880151089 / 10000000000000000000000) - 6 * (1872175480431801522837 / 10000000000000000000000))) ≤ Vfield (5015883525553 / 32000000000000)