V42: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_505 : 4409976854913976428969 / 10000000000000000000000 - 6 * (3 / 40) * -(5800290439484741597991 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7444844558462607 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3199809025526181901943 / 10000000000000000000000)) - 6 * (1004021175411097253659 / 10000000000000000000000))) ≤ Vfield (35472454719789 / 64000000000000)

theorem Zeta5Irrational.V_506 : 883600937481077002919 / 2000000000000000000000 - 6 * (3 / 40) * -(5778020694737567426223 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (931652880577461 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3202503278670062354709 / 10000000000000000000000)) - 6 * (250725017368404689187 / 2500000000000000000000))) ≤ Vfield (1111010675057 / 2000000000000)

theorem Zeta5Irrational.V_507 : 885205216091294371751 / 2000000000000000000000 - 6 * (3 / 40) * -(719475054245545283031 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (74615921227329 / 100000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3205192347747627695933 / 10000000000000000000000)) - 6 * (500891355368140157209 / 5000000000000000000000))) ≤ Vfield (35632228483859 / 64000000000000)

theorem Zeta5Irrational.V_508 : 2217020522194807226801 / 5000000000000000000000 - 6 * (3 / 40) * -(5733629437743145774003 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (933743978052949 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1603938125610509220697 / 5000000000000000000000)) - 6 * (125083634796351411801 / 1250000000000000000000))) ≤ Vfield (17856057682947 / 32000000000000)

theorem Zeta5Irrational.V_509 : 111051239737559752989 / 250000000000000000000 - 6 * (3 / 40) * -(5711507488108152006311 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7478302181136373 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (128422200298052838079 / 400000000000000000000)) - 6 * (999559151710662100997 / 10000000000000000000000))) ≤ Vfield (35792002247929 / 64000000000000)

theorem Zeta5Irrational.V_510 : 4450051726067655387087 / 10000000000000000000000 - 6 * (3 / 40) * -(5689434368536972102147 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7486643224140491 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (803307158674833361741 / 2500000000000000000000)) - 6 * (499226455124696702811 / 5000000000000000000000))) ≤ Vfield (8967972282491 / 16000000000000)

theorem Zeta5Irrational.V_511 : 2229023732166812530537 / 5000000000000000000000 - 6 * (3 / 40) * -(5667409863937838582023 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7494974984531197 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (100496785972697601687 / 312500000000000000000)) - 6 * (997350333639085100309 / 10000000000000000000000))) ≤ Vfield (35951776011999 / 64000000000000)

theorem Zeta5Irrational.V_512 : 4466036814523950969417 / 10000000000000000000000 - 6 * (3 / 40) * -(5645433760637049356529 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (75032974932311 / 100000000000000 * (Real.pi + (Real.pi / 2 - 2 * (643712114958955676583 / 2000000000000000000000)) - 6 * (498125700844381961051 / 5000000000000000000000))) ≤ Vfield (18015831447017 / 32000000000000)

theorem Zeta5Irrational.V_513 : 4474019786837800397257 / 10000000000000000000000 - 6 * (3 / 40) * -(1124701169273305923953 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (469475673811969 / 625000000000000 * (Real.pi + (Real.pi / 2 - 2 * (161060946183457558827 / 500000000000000000000)) - 6 * (124394511795356336081 / 1250000000000000000000))) ≤ Vfield (36111549776069 / 64000000000000)

theorem Zeta5Irrational.V_514 : 2240998195724967104201 / 5000000000000000000000 - 6 * (3 / 40) * -(5601625910251529815539 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (939989359799217 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3223872215616594728717 / 10000000000000000000000)) - 6 * (497032195889812852133 / 5000000000000000000000))) ≤ Vfield (4523929582263 / 8000000000000)

theorem Zeta5Irrational.V_515 : 2248965269073266439973 / 5000000000000000000000 - 6 * (3 / 40) * -(5558009135882844102449 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7536495623606959 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3229163699717176018831 / 10000000000000000000000)) - 6 * (30996616314830743811 / 312500000000000000000))) ≤ Vfield (18175605211087 / 32000000000000)

theorem Zeta5Irrational.V_516 : 4513839335526654517601 / 10000000000000000000000 - 6 * (3 / 40) * -(5514581777940426081753 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7553039970171363 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1617217584057645801541 / 5000000000000000000000)) - 6 * (989733236539927218279 / 10000000000000000000000))) ≤ Vfield (9127746046561 / 16000000000000)