V44: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_529 : 4732002263155807105589 / 10000000000000000000000 - 6 * (3 / 40) * -(986142542453729802313 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3889481773370539 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (661117047132910503789 / 2000000000000000000000)) - 6 * (192233570110948262549 / 2000000000000000000000))) ≤ Vfield (38727855271377 / 64000000000000)

theorem Zeta5Irrational.V_530 : 4738696609226712308587 / 10000000000000000000000 - 6 * (3 / 40) * -(4913128698083634611777 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3892934699771517 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3307735707316062547853 / 10000000000000000000000)) - 6 * (960320555090723355467 / 10000000000000000000000))) ≤ Vfield (19398323938157 / 32000000000000)

theorem Zeta5Irrational.V_531 : 474538647686853408261 / 1000000000000000000000 - 6 * (3 / 40) * -(4895575549388124547303 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (974096141558569 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3309882835885235928563 / 10000000000000000000000)) - 6 * (479737748220980712743 / 5000000000000000000000))) ≤ Vfield (38865440481251 / 64000000000000)

theorem Zeta5Irrational.V_532 : 4752071872069286534347 / 10000000000000000000000 - 6 * (3 / 40) * -(2439026579007312957233 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1949915690439729 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3312026630892787282743 / 10000000000000000000000)) - 6 * (479316332391940315167 / 5000000000000000000000))) ≤ Vfield (9733558271547 / 16000000000000)

theorem Zeta5Irrational.V_533 : 594844100100622765061 / 1250000000000000000000 - 6 * (3 / 40) * -(972112283272651519513 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3903275151791851 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3314167101818064698889 / 10000000000000000000000)) - 6 * (239448012588053166339 / 2500000000000000000000))) ≤ Vfield (312024205529 / 512000000000)

theorem Zeta5Irrational.V_534 : 953085853807932739837 / 2000000000000000000000 - 6 * (3 / 40) * -(4843100217397785791881 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1562686354808243 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (829076064524823682427 / 2500000000000000000000)) - 6 * (956953643442521360779 / 10000000000000000000000))) ≤ Vfield (19535909148031 / 32000000000000)

theorem Zeta5Irrational.V_535 : 4772101282725436474587 / 10000000000000000000000 - 6 * (3 / 40) * -(4825669454641694078661 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3910153594579467 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (829609527283457739137 / 2500000000000000000000)) - 6 * (478058717204865695451 / 5000000000000000000000))) ≤ Vfield (39140610900999 / 64000000000000)

theorem Zeta5Irrational.V_536 : 4778768847802499834877 / 10000000000000000000000 - 6 * (3 / 40) * -(4808269022174287691333 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1565435312978789 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3320568664278397156717 / 10000000000000000000000)) - 6 * (238820853416915635233 / 2500000000000000000000))) ≤ Vfield (2450587719121 / 4000000000000)

theorem Zeta5Irrational.V_537 : 4785431970199179084243 / 10000000000000000000000 - 6 * (3 / 40) * -(2395449407313415808313 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7834039917133371 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (664539186569865807171 / 2000000000000000000000)) - 6 * (954451571688568381881 / 10000000000000000000000))) ≤ Vfield (39278196110873 / 64000000000000)

theorem Zeta5Irrational.V_538 : 2396045327915978534597 / 5000000000000000000000 - 6 * (3 / 40) * -(2386779363589361089281 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3920448630847403 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3324819924122815790111 / 10000000000000000000000)) - 6 * (953621899002678461567 / 10000000000000000000000))) ≤ Vfield (3934698871581 / 6400000000000)

theorem Zeta5Irrational.V_539 : 2399372455302752849833 / 5000000000000000000000 - 6 * (3 / 40) * -(1189062163888422939389 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (7847748614326733 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3326940647335136480411 / 10000000000000000000000)) - 6 * (119099298274718298781 / 1250000000000000000000))) ≤ Vfield (39415781320747 / 64000000000000)

theorem Zeta5Irrational.V_540 : 4805394740412717365303 / 10000000000000000000000 - 6 * (3 / 40) * -(4738968496016046301109 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1570918798141791 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (83226452792072501471 / 250000000000000000000)) - 6 * (475984511959300131801 / 5000000000000000000000))) ≤ Vfield (9871143481421 / 16000000000000)