V15: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_181 : 565756240004760742753 / 5000000000000000000000 - 6 * (3 / 40) * -(20760370400176964455387 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1730616131954301 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 3332169574449736592719 / 10000000000000000000000) - 6 * (213386950021971650621 / 1000000000000000000000))) ≤ Vfield (3833641211111 / 32000000000000)

theorem Zeta5Irrational.V_182 : 227553573578023514173 / 2000000000000000000000 - 6 * (3 / 40) * -(4140932104806516067421 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3471339599085811 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 668238552174649568123 / 2000000000000000000000) - 6 * (265980315177075916949 / 1250000000000000000000))) ≤ Vfield (1928031777949 / 16000000000000)

theorem Zeta5Irrational.V_183 : 115026691691253115783 / 1000000000000000000000 - 6 * (3 / 40) * -(10297081645966272621029 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (139658659693411 / 400000000000000 * (Real.pi + (Real.pi / 2 - 3359143938006206998433 / 10000000000000000000000) - 6 * (1057970113702477507409 / 5000000000000000000000))) ≤ Vfield (121903382671 / 1000000000000)

theorem Zeta5Irrational.V_184 : 72671897675793028739 / 625000000000000000000 - 6 * (3 / 40) * -(10242436845908227152729 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (877869506319801 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 1688484972162490177399 / 5000000000000000000000) - 6 * (263029436248314576797 / 1250000000000000000000))) ≤ Vfield (1972876467523 / 16000000000000)

theorem Zeta5Irrational.V_185 : 293804561124544004693 / 2500000000000000000000 - 6 * (3 / 40) * -(101883828061061805467 / 50000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3531376159082673 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 424334104594847274703 / 1250000000000000000000) - 6 * (1046361451427109468381 / 5000000000000000000000))) ≤ Vfield (199529881231 / 1600000000000)

theorem Zeta5Irrational.V_186 : 74229412545702061359 / 625000000000000000000 - 6 * (3 / 40) * -(158357920152138572839 / 78125000000000000000) - 2 + 12 * (3 / 40) + 2 * (1775581399982569 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 106632956741550105427 / 312500000000000000000) - 6 * (2081397264622508967207 / 10000000000000000000000))) ≤ Vfield (2017721157097 / 16000000000000)

theorem Zeta5Irrational.V_187 : 1200107470129474167961 / 10000000000000000000000 - 6 * (3 / 40) * -(5040998430578654879721 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (446354975166469 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 342971722732483462099 / 1000000000000000000000) - 6 * (82810142757838897227 / 400000000000000000000))) ≤ Vfield (510035875471 / 4000000000000)

theorem Zeta5Irrational.V_188 : 612467451086576923913 / 5000000000000000000000 - 6 * (3 / 40) * -(9977827430743743884387 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (360987204712473 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 1732146236679985576439 / 5000000000000000000000) - 6 * (128030806236496645127 / 625000000000000000000))) ≤ Vfield (1042494095729 / 8000000000000)

theorem Zeta5Irrational.V_189 : 24994016934096835669 / 200000000000000000000 - 6 * (3 / 40) * -(19751568072237638037033 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (145939469679453 / 400000000000000 * (Real.pi + (Real.pi / 2 - 1749206566456722486477 / 5000000000000000000000) - 6 * (1013702202475916540091 / 5000000000000000000000))) ≤ Vfield (266229110129 / 2000000000000)

theorem Zeta5Irrational.V_190 : 259809897242961142701 / 2000000000000000000000 - 6 * (3 / 40) * -(1935548032090052720183 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (465564410925817 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 3565345242591427109191 / 10000000000000000000000) - 6 * (397422127297066665873 / 2000000000000000000000))) ≤ Vfield (110976113009 / 800000000000)

theorem Zeta5Irrational.V_191 : 13481557922957465779 / 100000000000000000000 - 6 * (3 / 40) * -(4743621304204845889853 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3799022604012773 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 3630616003248135794793 / 10000000000000000000000) - 6 * (1949127934440516860467 / 10000000000000000000000))) ≤ Vfield (72162863729 / 500000000000)

theorem Zeta5Irrational.V_192 : 1363649648793105799231 / 10000000000000000000000 - 6 * (3 / 40) * -(18856849239285061292259 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1911152162703291 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 1825472812071868163633 / 5000000000000000000000) - 6 * (968775768368206191403 / 5000000000000000000000))) ≤ Vfield (4675203313927 / 32000000000000)