V52: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_625 : 2730877782592370590811 / 5000000000000000000000 - 6 * (3 / 40) * -(3116169747917816613287 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1704860051870497 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3529515644499602674989 / 10000000000000000000000)) - 6 * (877577784756869561493 / 10000000000000000000000))) ≤ Vfield (23252382371711 / 32000000000000)

theorem Zeta5Irrational.V_626 : 546726995479048066533 / 1000000000000000000000 - 6 * (3 / 40) * -(77579298971171939033 / 250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8529884797410073 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1765566185380807726961 / 5000000000000000000000)) - 6 * (219251543692524048579 / 2500000000000000000000))) ≤ Vfield (5820714772567 / 8000000000000)

theorem Zeta5Irrational.V_627 : 5472781305222789424267 / 10000000000000000000000 - 6 * (3 / 40) * -(3090191042100093015749 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8535465681647259 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3532747148789359859367 / 10000000000000000000000)) - 6 * (175287136058003471421 / 2000000000000000000000))) ≤ Vfield (932533432353 / 1280000000000)

theorem Zeta5Irrational.V_628 : 5478289619829812308189 / 10000000000000000000000 - 6 * (3 / 40) * -(769306738482647776489 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2135260729806619 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (441794997850047114757 / 1250000000000000000000)) - 6 * (218966574423277628579 / 2500000000000000000000))) ≤ Vfield (11671906263691 / 16000000000000)

theorem Zeta5Irrational.V_629 : 5483794901954164421831 / 10000000000000000000000 - 6 * (3 / 40) * -(38303495634517765457 / 125000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2136654129321697 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3535970876998488086731 / 10000000000000000000000)) - 6 * (875298023372310254261 / 10000000000000000000000))) ≤ Vfield (23374289245939 / 32000000000000)

theorem Zeta5Irrational.V_630 : 5489297154932943295337 / 10000000000000000000000 - 6 * (3 / 40) * -(122053963567387008637 / 400000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1710437296588799 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (884394958893463844413 / 2500000000000000000000)) - 6 * (174946170747382495469 / 2000000000000000000000))) ≤ Vfield (1462797872781 / 2000000000000)

theorem Zeta5Irrational.V_631 : 1098959276419548204243 / 2000000000000000000000 - 6 * (3 / 40) * -(3038435225960614059479 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4278876411645369 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (884796715675760448579 / 2500000000000000000000)) - 6 * (437082392606239601383 / 5000000000000000000000))) ≤ Vfield (23435242683053 / 32000000000000)

theorem Zeta5Irrational.V_632 : 5500292586774656357943 / 10000000000000000000000 - 6 * (3 / 40) * -(184664185669970729 / 610351562500000000) - 2 + 12 * (3 / 40) + 2 * (8563315545396609 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (708158392509814711217 / 2000000000000000000000)) - 6 * (436799907120371740757 / 5000000000000000000000))) ≤ Vfield (2346571940161 / 3200000000000)

theorem Zeta5Irrational.V_633 : 5505785772284306800337 / 10000000000000000000000 - 6 * (3 / 40) * -(3012657422447236628907 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8568874656308251 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3542395139261497851501 / 10000000000000000000000)) - 6 * (109129492159939492009 / 1250000000000000000000))) ≤ Vfield (23496196120167 / 32000000000000)

theorem Zeta5Irrational.V_634 : 5511275941941840616771 / 10000000000000000000000 - 6 * (3 / 40) * -(2999793396511508222773 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1714886032609893 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (885999099244110855617 / 2500000000000000000000)) - 6 * (872473150802591192013 / 10000000000000000000000))) ≤ Vfield (5881668209681 / 8000000000000)

theorem Zeta5Irrational.V_635 : 1379190774764237213347 / 2500000000000000000000 - 6 * (3 / 40) * -(2986945897633933050071 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (33515554971177 / 39062500000000 * (Real.pi + (Real.pi / 2 - 2 * (1772797869908340061831 / 5000000000000000000000)) - 6 * (174382290259931083323 / 2000000000000000000000))) ≤ Vfield (23557149557281 / 32000000000000)

theorem Zeta5Irrational.V_636 : 5522247246933877305379 / 10000000000000000000000 - 6 * (3 / 40) * -(2974114883402715778061 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1073191299000277 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3547193171891676928569 / 10000000000000000000000)) - 6 * (435675417638097174757 / 5000000000000000000000))) ≤ Vfield (11793813137919 / 16000000000000)