V47: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_565 : 156339399393304630697 / 312500000000000000000 - 6 * (3 / 40) * -(1058494856331202102067 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2014312849883663 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3391110724922073870779 / 10000000000000000000000)) - 6 * (464081982859780515481 / 5000000000000000000000))) ≤ Vfield (20774176036897 / 32000000000000)

theorem Zeta5Irrational.V_566 : 2507943784957586433653 / 5000000000000000000000 - 6 * (3 / 40) * -(4201203176702343280537 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (63051413737327 / 78125000000000 * (Real.pi + (Real.pi / 2 - 2 * (169757466539305760399 / 500000000000000000000)) - 6 * (926639756078741289001 / 10000000000000000000000))) ≤ Vfield (10421484320917 / 16000000000000)

theorem Zeta5Irrational.V_567 : 314306088224720380513 / 625000000000000000000 - 6 * (3 / 40) * -(4168534005463306455681 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8083888538083597 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3399176031881748881431 / 10000000000000000000000)) - 6 * (925123030975232317823 / 10000000000000000000000))) ≤ Vfield (20911761246771 / 32000000000000)

theorem Zeta5Irrational.V_568 : 1008378069933354245329 / 2000000000000000000000 - 6 * (3 / 40) * -(2067985607129381824541 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4048587123509493 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3403190891892478111163 / 10000000000000000000000)) - 6 * (923613729354546866129 / 10000000000000000000000))) ≤ Vfield (5245138462927 / 8000000000000)

theorem Zeta5Irrational.V_569 : 2533912845142745232631 / 5000000000000000000000 - 6 * (3 / 40) * -(1017790504105132442423 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8123680481619383 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1705592670410026563051 / 5000000000000000000000)) - 6 * (920617155808572349771 / 10000000000000000000000))) ≤ Vfield (10559069530791 / 16000000000000)

theorem Zeta5Irrational.V_570 : 1018738788135635374369 / 2000000000000000000000 - 6 * (3 / 40) * -(801354027725657851151 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8150100511545853 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1709566588411900250929 / 5000000000000000000000)) - 6 * (9176495607237304067 / 100000000000000000000))) ≤ Vfield (664241383483 / 1000000000000)

theorem Zeta5Irrational.V_571 : 510343822688833403141 / 1000000000000000000000 - 6 * (3 / 40) * -(796515710353325413713 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8160048151107357 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1711060181048130356787 / 5000000000000000000000)) - 6 * (183307428647100260073 / 2000000000000000000000))) ≤ Vfield (4261528693017 / 6400000000000)

theorem Zeta5Irrational.V_572 : 5113173027229668871761 / 10000000000000000000000 - 6 * (3 / 40) * -(791689069397068086157 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8169983678593319 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (428137625724666504333 / 1250000000000000000000)) - 6 * (915428761561533214527 / 10000000000000000000000))) ≤ Vfield (10679781329357 / 16000000000000)

theorem Zeta5Irrational.V_573 : 5122898360152830778087 / 10000000000000000000000 - 6 * (3 / 40) * -(1967185121586613830879 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8179907138138663 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3428075133878351375991 / 10000000000000000000000)) - 6 * (3571579653740407077 / 39062500000000000000))) ≤ Vfield (21411481852343 / 32000000000000)

theorem Zeta5Irrational.V_574 : 320788390253418113291 / 625000000000000000000 - 6 * (3 / 40) * -(1955176480622274021633 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2047454643402731 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (85776069303373838337 / 250000000000000000000)) - 6 * (182644801696868735909 / 2000000000000000000000))) ≤ Vfield (5365850261493 / 8000000000000)

theorem Zeta5Irrational.V_575 : 5142320697278545517473 / 10000000000000000000000 - 6 * (3 / 40) * -(3886393224119610109169 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4099859014306257 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (686800789241670516879 / 2000000000000000000000)) - 6 * (114015948625701972549 / 1250000000000000000000))) ≤ Vfield (21515320239601 / 32000000000000)

theorem Zeta5Irrational.V_576 : 5147170393103906195523 / 10000000000000000000000 - 6 * (3 / 40) * -(1937217424407472507173 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8204663276990617 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1717741058573659101171 / 5000000000000000000000)) - 6 * (911580858114015239713 / 10000000000000000000000))) ≤ Vfield (43082559672831 / 64000000000000)