V48: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_577 : 5152017738114334704557 / 10000000000000000000000 - 6 * (3 / 40) * -(3862490756705591713337 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8209605546482957 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1718479340793304782101 / 5000000000000000000000)) - 6 * (911035109185732816891 / 10000000000000000000000))) ≤ Vfield (2156723943323 / 3200000000000)

theorem Zeta5Irrational.V_578 : 1031372546917553828993 / 2000000000000000000000 - 6 * (3 / 40) * -(3850560913712286605501 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (410727242123313 / 500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3438433642688509428973 / 10000000000000000000000)) - 6 * (9104903392848186487 / 100000000000000000000))) ≤ Vfield (43186398060089 / 64000000000000)

theorem Zeta5Irrational.V_579 : 5161705384798838239711 / 10000000000000000000000 - 6 * (3 / 40) * -(959661321469397220031 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8219481170301101 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1719953501802942922099 / 5000000000000000000000)) - 6 * (227486636371899300713 / 2500000000000000000000))) ≤ Vfield (21619158626859 / 32000000000000)

theorem Zeta5Irrational.V_580 : 5166545691018867741703 / 10000000000000000000000 - 6 * (3 / 40) * -(1913371919682650284589 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8224414535331963 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (860344691870556942057 / 2500000000000000000000)) - 6 * (454701862441301176601 / 5000000000000000000000))) ≤ Vfield (43290236447347 / 64000000000000)

theorem Zeta5Irrational.V_581 : 2585691827757943412823 / 5000000000000000000000 - 6 * (3 / 40) * -(1907428270229945023543 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (514334058930457 / 625000000000000 * (Real.pi + (Real.pi / 2 - 2 * (860712234362921461299 / 2500000000000000000000)) - 6 * (908861874570511082349 / 10000000000000000000000))) ≤ Vfield (2708884727561 / 4000000000000)

theorem Zeta5Irrational.V_582 : 2588109640277317232227 / 5000000000000000000000 - 6 * (3 / 40) * -(3802983355565918952933 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8234272398279661 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (430539689579888660491 / 1250000000000000000000)) - 6 * (908320991664078785569 / 10000000000000000000000))) ≤ Vfield (8678814966921 / 12800000000000)

theorem Zeta5Irrational.V_583 : 2590526284198282895123 / 5000000000000000000000 - 6 * (3 / 40) * -(473890531400934063847 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4119598453402819 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (430723063520010527707 / 1250000000000000000000)) - 6 * (181556214657614903937 / 2000000000000000000000))) ≤ Vfield (21722997014117 / 32000000000000)

theorem Zeta5Irrational.V_584 : 2592941760649929219989 / 5000000000000000000000 - 6 * (3 / 40) * -(755855838805518644779 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8244118473746051 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3447249915120971146511 / 10000000000000000000000)) - 6 * (181448423315843392787 / 2000000000000000000000))) ≤ Vfield (43497913221863 / 64000000000000)

theorem Zeta5Irrational.V_585 : 5190712141519418885757 / 10000000000000000000000 - 6 * (3 / 40) * -(75348963015754358381 / 200000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8249037104365953 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (215544608788683865353 / 625000000000000000000)) - 6 * (113338014835763844939 / 1250000000000000000000))) ≤ Vfield (10887458103873 / 16000000000000)

theorem Zeta5Irrational.V_586 : 41564307450455109999 / 80000000000000000000 - 6 * (3 / 40) * -(3755631088367118116969 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1031744100489339 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1725087993871008903277 / 5000000000000000000000)) - 6 * (1132708845961478349 / 12500000000000000000))) ≤ Vfield (43601751609121 / 64000000000000)

theorem Zeta5Irrational.V_587 : 2600181196455325552307 / 5000000000000000000000 - 6 * (3 / 40) * -(58497312090036620399 / 156250000000000000000) - 2 + 12 * (3 / 40) + 2 * (8258865577626073 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (53931822805767294657 / 156250000000000000000)) - 6 * (226407747000154761683 / 2500000000000000000000))) ≤ Vfield (174614683211 / 256000000000)

theorem Zeta5Irrational.V_588 : 2602592014287918378433 / 5000000000000000000000 - 6 * (3 / 40) * -(1866019387043334946147 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (516485964419889 / 625000000000000 * (Real.pi + (Real.pi / 2 - 2 * (215818484948127477083 / 625000000000000000000)) - 6 * (452547924782151544459 / 5000000000000000000000))) ≤ Vfield (43705589996379 / 64000000000000)