V09: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_109 : 83409097129161147991 / 1250000000000000000000 - 6 * (3 / 40) * -(3244034354456449727219 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2626859288543901 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1284411327890970380713 / 5000000000000000000000) - 6 * (695281708072396394957 / 2500000000000000000000))) ≤ Vfield (2208124710979 / 32000000000000)

theorem Zeta5Irrational.V_110 : 16804676517263733869 / 250000000000000000000 - 6 * (3 / 40) * -(6470527693651944065921 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (659210537122859 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 1289079416002930597313 / 5000000000000000000000) - 6 * (554225892774949028251 / 2000000000000000000000))) ≤ Vfield (4449879370279 / 64000000000000)

theorem Zeta5Irrational.V_111 : 33854946525780009319 / 500000000000000000000 - 6 * (3 / 40) * -(1613277224061336718483 / 625000000000000000000) - 2 + 12 * (3 / 40) + 2 * (66169683911481 / 250000000000000 * (Real.pi + (Real.pi / 2 - 2587455226799105179707 / 10000000000000000000000) - 6 * (2761239196892071779283 / 10000000000000000000000))) ≤ Vfield (22417546593 / 320000000000)

theorem Zeta5Irrational.V_112 : 170502097219640879853 / 2500000000000000000000 - 6 * (3 / 40) * -(25743242501413712938097 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (531339067058467 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 40573629285751086729 / 156250000000000000000) - 6 * (343931766448437447047 / 1250000000000000000000))) ≤ Vfield (4517139266921 / 64000000000000)

theorem Zeta5Irrational.V_113 : 343457719073036051437 / 5000000000000000000000 - 6 * (3 / 40) * -(12837262449008737335481 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1333283249990003 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2605930400624028400873 / 10000000000000000000000) - 6 * (1370886207538278677507 / 5000000000000000000000))) ≤ Vfield (2275384607621 / 32000000000000)

theorem Zeta5Irrational.V_114 : 345910040340638219639 / 5000000000000000000000 - 6 * (3 / 40) * -(3200784535571160288559 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (334550157232327 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 1307555012094042014081 / 5000000000000000000000) - 6 * (170762014991703940461 / 625000000000000000000))) ≤ Vfield (4584399163563 / 64000000000000)

theorem Zeta5Irrational.V_115 : 13934446376877032259 / 200000000000000000000 - 6 * (3 / 40) * -(25538490302831131762179 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2686200008807747 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 524850311157877829367 / 2000000000000000000000) - 6 * (2722711842439540008903 / 10000000000000000000000))) ≤ Vfield (1154507277971 / 16000000000000)

theorem Zeta5Irrational.V_116 : 701622154990004101623 / 10000000000000000000000 - 6 * (3 / 40) * -(6367790180748935590831 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2695963145439919 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2633355398856895131241 / 10000000000000000000000) - 6 * (1356664750939314845041 / 5000000000000000000000))) ≤ Vfield (930331812041 / 12800000000000)

theorem Zeta5Irrational.V_117 : 706519591472478571351 / 10000000000000000000000 - 6 * (3 / 40) * -(5080856288050152583271 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (541138210656829 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 21139375596999086211 / 80000000000000000000) - 6 * (338005442320010944411 / 1250000000000000000000))) ≤ Vfield (2342644504263 / 32000000000000)

theorem Zeta5Irrational.V_118 : 354483705287062168277 / 5000000000000000000000 - 6 * (3 / 40) * -(3171376098236488809029 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (677635478748883 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 1323470681148397034747 / 5000000000000000000000) - 6 * (1349718092230963117081 / 5000000000000000000000))) ≤ Vfield (9404207965373 / 128000000000000)

theorem Zeta5Irrational.V_119 : 711414630640564654789 / 10000000000000000000000 - 6 * (3 / 40) * -(12668923235728554122461 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (678846027740893 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 662862899328136929311 / 2500000000000000000000) - 6 * (2694852312884068981851 / 10000000000000000000000))) ≤ Vfield (4718918956847 / 64000000000000)

theorem Zeta5Irrational.V_120 : 713861251964921990511 / 10000000000000000000000 - 6 * (3 / 40) * -(1581549610471153343741 / 625000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2720217687465327 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 663988175564238770757 / 2500000000000000000000) - 6 * (2690291724930460355717 / 10000000000000000000000))) ≤ Vfield (1894293572403 / 25600000000000)