V02: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_25 : 1017781512086277763 / 625000000000000000000 - 6 * (3 / 40) * -(24630475597680706138947 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (50463121818531 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 403485872391495007731 / 10000000000000000000000) - 6 * (Real.pi / 2 - 2 * (2468977145022571269173 / 10000000000000000000000)))) ≤ Vfield (6519108259 / 4000000000000)

theorem Zeta5Irrational.V_26 : 9277724379122655699 / 5000000000000000000000 - 6 * (3 / 40) * -(48952193938876747273721 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (430960260871001 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 53836719370999942317 / 1250000000000000000000) - 6 * (Real.pi / 2 - 2 * (130385975621936090201 / 500000000000000000000)))) ≤ Vfield (3714534929 / 2000000000000)

theorem Zeta5Irrational.V_27 : 10412938860637891291 / 5000000000000000000000 - 6 * (3 / 40) * -(6081585619044427772321 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (456591487464453 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 57034323691496256243 / 1250000000000000000000) - 6 * (Real.pi / 2 - 2 * (683570867995966803463 / 2500000000000000000000)))) ≤ Vfield (8339031457 / 4000000000000)

theorem Zeta5Irrational.V_28 : 23095791316545841351 / 10000000000000000000000 - 6 * (3 / 40) * -(48361886282182873980137 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (480858426566491 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 480488318545920830527 / 10000000000000000000000) - 6 * (Real.pi / 2 - 2 * (2850623752102888537797 / 10000000000000000000000)))) ≤ Vfield (289031033 / 125000000000)

theorem Zeta5Irrational.V_29 : 1552336842063143213 / 500000000000000000000 - 6 * (3 / 40) * -(23702373925704740231503 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (278814372611959 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 557051839319540677711 / 10000000000000000000000) - 6 * (Real.pi / 2 - 2 * (639331329091312161727 / 2000000000000000000000)))) ≤ Vfield (124379927 / 40000000000)

theorem Zeta5Irrational.V_30 : 35019840201976078429 / 10000000000000000000000 - 6 * (3 / 40) * -(46958475676102112366331 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (74036763782639 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 591602950926025152249 / 10000000000000000000000) - 6 * (Real.pi / 2 - 2 * (1671111291423061004301 / 5000000000000000000000)))) ≤ Vfield (7016246261 / 2000000000000)

theorem Zeta5Irrational.V_31 : 487392070432052579 / 125000000000000000000 - 6 * (3 / 40) * -(9306254293033936914081 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (625039845609863 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 624227790518306883007 / 10000000000000000000000) - 6 * (Real.pi / 2 - 2 * (3473848146500016081923 / 10000000000000000000000)))) ≤ Vfield (1953374043 / 500000000000)

theorem Zeta5Irrational.V_32 : 236122014583635193 / 40000000000000000000 - 6 * (3 / 40) * -(11153647148939723420669 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (384724177171127 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 38396760876845215791 / 500000000000000000000) - 6 * (2 * (772599247056886688553 / 2000000000000000000000)))) ≤ Vfield qm

theorem Zeta5Irrational.V_33 : 29515252817068737431 / 5000000000000000000000 - 6 * (3 / 40) * -(5576823552816418281887 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (384724183669287 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 6143481843653882843 / 80000000000000000000) - 6 * (2 * (1931498096536080841753 / 5000000000000000000000)))) ≤ Vfield qp

theorem Zeta5Irrational.V_34 : 22381255075260993563 / 2500000000000000000000 - 6 * (3 / 40) * -(1056380614920881581967 / 250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (237074560146697 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 945470894474292487187 / 10000000000000000000000) - 6 * (2 * (3345807944831543455677 / 10000000000000000000000)))) ≤ Vfield (8992695531 / 1000000000000)

theorem Zeta5Irrational.V_35 : 9738658275375887661 / 1000000000000000000000 - 6 * (3 / 40) * -(834531719438274254441 / 200000000000000000000) - 2 + 12 * (3 / 40) + 2 * (989253927032891 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 986045720575090130693 / 10000000000000000000000) - 6 * (2 * (1621737244125958055291 / 5000000000000000000000)))) ≤ Vfield (19572466643 / 2000000000000)

theorem Zeta5Irrational.V_36 : 101315047537995983751 / 10000000000000000000000 - 6 * (3 / 40) * -(20736194980936662302051 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1009108627291927 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1005704152080836199331 / 10000000000000000000000) - 6 * (2 * (3195771674208240842333 / 10000000000000000000000)))) ≤ Vfield (40732008867 / 4000000000000)