V33: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_397 : 830766881093553021839 / 2500000000000000000000 - 6 * (3 / 40) * -(8952902555955087179 / 9765625000000000000) - 2 + 12 * (3 / 40) + 2 * (1255675835837717 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (700796828610549806021 / 2500000000000000000000)) - 6 * (118894174383393800607 / 1000000000000000000000))) ≤ Vfield (6306887218827 / 16000000000000)

theorem Zeta5Irrational.V_398 : 3341814806437021744403 / 10000000000000000000000 - 6 * (3 / 40) * -(4551274765307920417809 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1574794851961441 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1405319994812823534829 / 5000000000000000000000)) - 6 * (237010501418881799479 / 2000000000000000000000))) ≤ Vfield (12697491587913 / 32000000000000)

theorem Zeta5Irrational.V_399 : 840131752049283713763 / 2500000000000000000000 - 6 * (3 / 40) * -(2259437372176322009597 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1263982235742061 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2818054236801107742807 / 10000000000000000000000)) - 6 * (590600595064456682237 / 5000000000000000000000))) ≤ Vfield (3195302184543 / 8000000000000)

theorem Zeta5Irrational.V_400 : 3379204260695362054447 / 10000000000000000000000 - 6 * (3 / 40) * -(8973366649314295692837 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (99071486926427 / 156250000000000 * (Real.pi + (Real.pi / 2 - 2 * (2825430439216674767041 / 10000000000000000000000)) - 6 * (1177387180713437419171 / 10000000000000000000000))) ≤ Vfield (12864925888431 / 32000000000000)

theorem Zeta5Irrational.V_401 : 3397846694239637457303 / 10000000000000000000000 - 6 * (3 / 40) * -(8909395674635741552251 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1272234404438211 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2832768974090960128569 / 10000000000000000000000)) - 6 * (293402470093434932507 / 2500000000000000000000))) ≤ Vfield (1294864303869 / 3200000000000)

theorem Zeta5Irrational.V_402 : 3416454438410473535733 / 10000000000000000000000 - 6 * (3 / 40) * -(8845831328651810423357 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (255268096214049 / 400000000000000 * (Real.pi + (Real.pi / 2 - 2 * (14200351063728030601 / 50000000000000000000)) - 6 * (584934351995421838111 / 5000000000000000000000))) ≤ Vfield (13032360188949 / 32000000000000)

theorem Zeta5Irrational.V_403 : 1717513811033182669897 / 5000000000000000000000 - 6 * (3 / 40) * -(4391334237281119106909 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3201083476146201 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (355916815091755312081 / 1250000000000000000000)) - 6 * (583081539710138134777 / 5000000000000000000000))) ≤ Vfield (1639509667401 / 4000000000000)

theorem Zeta5Irrational.V_404 : 868017704922321109341 / 2500000000000000000000 - 6 * (3 / 40) * -(541095448505268199687 / 625000000000000000000) - 2 + 12 * (3 / 40) + 2 * (805362630610271 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (715438444708057385753 / 2500000000000000000000)) - 6 * (115885625981794946927 / 1000000000000000000000))) ≤ Vfield (6641755819863 / 16000000000000)

theorem Zeta5Irrational.V_405 : 175448865186911473401 / 500000000000000000000 - 6 * (3 / 40) * -(8533932576410381810459 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6483379216370309 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2876029562117140236423 / 10000000000000000000000)) - 6 * (115168509024532050863 / 1000000000000000000000))) ≤ Vfield (3362736485061 / 8000000000000)

theorem Zeta5Irrational.V_406 : 886437019907079153121 / 2500000000000000000000 - 6 * (3 / 40) * -(8411846908633533086469 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (652360623063511 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1445082299841854199793 / 5000000000000000000000)) - 6 * (1144645424719571608529 / 10000000000000000000000))) ≤ Vfield (6809190120381 / 16000000000000)

theorem Zeta5Irrational.V_407 : 3582384141724289505683 / 10000000000000000000000 - 6 * (3 / 40) * -(8291233772453230333 / 10000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3281793352783657 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (290416153952159878763 / 1000000000000000000000)) - 6 * (568866646261417588901 / 5000000000000000000000))) ≤ Vfield (86161340883 / 200000000000)

theorem Zeta5Irrational.V_408 : 3600878263421158486701 / 10000000000000000000000 - 6 * (3 / 40) * -(8230729569040064947449 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1316746451171219 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2911194962262022984371 / 10000000000000000000000)) - 6 * (1134281773410074366533 / 10000000000000000000000))) ≤ Vfield (54181913021 / 125000000000)