V38: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_457 : 1972960046410281505363 / 5000000000000000000000 - 6 * (3 / 40) * -(7145675682770966266981 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6955420184827081 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3038638800749049350961 / 10000000000000000000000)) - 6 * (16783522952507147781 / 156250000000000000000))) ≤ Vfield (19351147979 / 40000000000)

theorem Zeta5Irrational.V_458 : 3963754549125513984239 / 10000000000000000000000 - 6 * (3 / 40) * -(709170268375400157447 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6974434021682331 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (304504032630575797579 / 1000000000000000000000)) - 6 * (21424789892291219471 / 200000000000000000000))) ≤ Vfield (121606824807 / 250000000000)

theorem Zeta5Irrational.V_459 : 995389313815897849753 / 2500000000000000000000 - 6 * (3 / 40) * -(703801943005654114471 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3496698081694357 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3051413081799342518727 / 10000000000000000000000)) - 6 * (534178489479691317771 / 5000000000000000000000))) ≤ Vfield (489075898981 / 1000000000000)

theorem Zeta5Irrational.V_460 : 499916040510216863701 / 1250000000000000000000 - 6 * (3 / 40) * -(873077853422577693929 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1402461405863277 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3057757310175657760821 / 10000000000000000000000)) - 6 * (213099521612080179629 / 2000000000000000000000))) ≤ Vfield (245862249367 / 500000000000)

theorem Zeta5Irrational.V_461 : 4017067867826327729629 / 10000000000000000000000 - 6 * (3 / 40) * -(6931509830732862114179 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7031167033195839 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1532036625599493404347 / 5000000000000000000000)) - 6 * (132832634229193100987 / 1250000000000000000000))) ≤ Vfield (494373098487 / 1000000000000)

theorem Zeta5Irrational.V_462 : 4034775998147450528869 / 10000000000000000000000 - 6 * (3 / 40) * -(1719669361495489087719 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (44062353645147 / 62500000000000 * (Real.pi + (Real.pi / 2 - 2 * (383795142688735162467 / 1250000000000000000000)) - 6 * (1059847073905755610613 / 10000000000000000000000))) ≤ Vfield (1553192807 / 3125000000)

theorem Zeta5Irrational.V_463 : 4052452826103097732711 / 10000000000000000000000 - 6 * (3 / 40) * -(6826122718446278959801 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (70687360821649 / 100000000000000 * (Real.pi + (Real.pi / 2 - 2 * (769155303670411559609 / 2500000000000000000000)) - 6 * (105705531147958899277 / 1000000000000000000000))) ≤ Vfield (499670297993 / 1000000000000)

theorem Zeta5Irrational.V_464 : 4087713016214549625359 / 10000000000000000000000 - 6 * (3 / 40) * -(3360917337612814841707 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3553053255648583 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1544529414447257797889 / 5000000000000000000000)) - 6 * (210307467807043208833 / 2000000000000000000000))) ≤ Vfield (504967497499 / 1000000000000)

theorem Zeta5Irrational.V_465 : 4122849314940802649517 / 10000000000000000000000 - 6 * (3 / 40) * -(6618623015859148835301 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1785820359465433 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1550693951571935343901 / 5000000000000000000000)) - 6 * (209220977745917649767 / 2000000000000000000000))) ≤ Vfield (102052939401 / 200000000000)

theorem Zeta5Irrational.V_466 : 4157862589852264614611 / 10000000000000000000000 - 6 * (3 / 40) * -(1629116436967895470151 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1436052779686039 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3113610201061039069011 / 10000000000000000000000)) - 6 * (520377886983577812947 / 5000000000000000000000))) ≤ Vfield (515561896511 / 1000000000000)

theorem Zeta5Irrational.V_467 : 834864249188940764473 / 2000000000000000000000 - 6 * (3 / 40) * -(6468680488511488354407 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (899703389990447 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (623866760360916799687 / 2000000000000000000000)) - 6 * (1038263128909289262889 / 10000000000000000000000))) ≤ Vfield (16577867570387 / 32000000000000)

theorem Zeta5Irrational.V_468 : 1047688214451545209707 / 2500000000000000000000 - 6 * (3 / 40) * -(3210561243363384980221 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7214948555867791 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3125034246207891380201 / 10000000000000000000000)) - 6 * (103578830857744472109 / 1000000000000000000000))) ≤ Vfield (8328877226211 / 16000000000000)