V10: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_121 : 358153637420051856447 / 5000000000000000000000 - 6 * (3 / 40) * -(505436999038738140509 / 200000000000000000000) - 2 + 12 * (3 / 40) + 2 * (681260672591859 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2660444724297807303401 / 10000000000000000000000) - 6 * (2685754224056738553489 / 10000000000000000000000))) ≤ Vfield (297034306573 / 4000000000000)

theorem Zeta5Irrational.V_122 : 143750539911760461247 / 2000000000000000000000 - 6 * (3 / 40) * -(25239014309567609724181 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2729859165131193 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1332463855095506303277 / 5000000000000000000000) - 6 * (2681239616034587774699 / 10000000000000000000000))) ≤ Vfield (9538727758657 / 128000000000000)

theorem Zeta5Irrational.V_123 : 180299381603373895023 / 2500000000000000000000 - 6 * (3 / 40) * -(25206286132366748618349 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (546933431363509 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2669401706285649911771 / 10000000000000000000000) - 6 * (2676747708916748668133 / 10000000000000000000000))) ≤ Vfield (4786178853489 / 64000000000000)

theorem Zeta5Irrational.V_124 : 180910438924111719793 / 2500000000000000000000 - 6 * (3 / 40) * -(6293416179799985485973 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2739466710092009 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2673866758528940898129 / 10000000000000000000000) - 6 * (1336139156501337456721 / 5000000000000000000000))) ≤ Vfield (9605987655299 / 128000000000000)

theorem Zeta5Irrational.V_125 : 726085387699705292959 / 10000000000000000000000 - 6 * (3 / 40) * -(6285287343943028423973 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (548851573845903 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2678322912471147172359 / 10000000000000000000000) - 6 * (1333915620402408418013 / 5000000000000000000000))) ≤ Vfield (481980880181 / 6400000000000)

theorem Zeta5Irrational.V_126 : 72852842271510586509 / 1000000000000000000000 - 6 * (3 / 40) * -(12554369707269414330891 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2749040678119169 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2682770213270387066649 / 10000000000000000000000) - 6 * (1331703153507762705967 / 5000000000000000000000))) ≤ Vfield (9673247551941 / 128000000000000)

theorem Zeta5Irrational.V_127 : 730970861034269802467 / 10000000000000000000000 - 6 * (3 / 40) * -(25076434154619059633243 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (172113448766809 / 625000000000000 * (Real.pi + (Real.pi / 2 - 335901088212172452663 / 1250000000000000000000) - 6 * (10636013313898229031 / 40000000000000000000))) ≤ Vfield (4853438750131 / 64000000000000)

theorem Zeta5Irrational.V_128 : 735853948749304669843 / 10000000000000000000000 - 6 * (3 / 40) * -(5002427009599881711513 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2763339436502733 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 5265741098844656167 / 19531250000000000000) - 6 * (2650262515042783265311 / 10000000000000000000000))) ≤ Vfield (1221767174613 / 16000000000000)

theorem Zeta5Irrational.V_129 : 740734653173510746083 / 10000000000000000000000 - 6 * (3 / 40) * -(6237061684726463436083 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1386415489272859 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 676218868449462891921 / 2500000000000000000000) - 6 * (52832147539552359909 / 200000000000000000000))) ≤ Vfield (4920698646773 / 64000000000000)

theorem Zeta5Irrational.V_130 : 37280648831609041759 / 500000000000000000000 - 6 * (3 / 40) * -(6221191002898389833279 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2782290141202813 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 542731428790419567221 / 2000000000000000000000) - 6 * (658259130780697986243 / 2500000000000000000000))) ≤ Vfield (2477164297547 / 32000000000000)

theorem Zeta5Irrational.V_131 : 750488921447206341103 / 10000000000000000000000 - 6 * (3 / 40) * -(24821681749024979579647 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1395858626803403 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2722404791990247254829 / 10000000000000000000000) - 6 * (2624548593756629872647 / 10000000000000000000000))) ≤ Vfield (997591708683 / 12800000000000)

theorem Zeta5Irrational.V_132 : 377681244968541949289 / 5000000000000000000000 - 6 * (3 / 40) * -(24758994930394767520483 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1400556319675997 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2731118751199019664549 / 10000000000000000000000) - 6 * (2616142259684255857913 / 10000000000000000000000))) ≤ Vfield (627698561467 / 8000000000000)