V51: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_613 : 5372493143715501039287 / 10000000000000000000000 - 6 * (3 / 40) * -(332793597066236323861 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1054227466493001 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1751598472914581166259 / 5000000000000000000000)) - 6 * (886943661285501435459 / 10000000000000000000000))) ≤ Vfield (22761380886697 / 32000000000000)

theorem Zeta5Irrational.V_614 : 5381969639025595980783 / 10000000000000000000000 - 6 * (3 / 40) * -(1652665149511791927237 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1688686622805057 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (876501105435104276007 / 2500000000000000000000)) - 6 * (885939098663711472987 / 10000000000000000000000))) ≤ Vfield (11406650040163 / 16000000000000)

theorem Zeta5Irrational.V_615 : 5400895730933659307041 / 10000000000000000000000 - 6 * (3 / 40) * -(815067921368615468109 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (846262711639831 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1755800926009630248063 / 5000000000000000000000)) - 6 * (88394017114811751033 / 1000000000000000000000))) ≤ Vfield (89520072139 / 125000000000)

theorem Zeta5Irrational.V_616 : 216479549629272587089 / 400000000000000000000 - 6 * (3 / 40) * -(808479101909136909281 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8473873801407549 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3514876734834164438587 / 10000000000000000000000)) - 6 * (17655461571844476817 / 200000000000000000000))) ≤ Vfield (11489045952349 / 16000000000000)

theorem Zeta5Irrational.V_617 : 2708765317241712306349 / 5000000000000000000000 - 6 * (3 / 40) * -(3220764770559494080803 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8479491550067837 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3516511187288392257217 / 10000000000000000000000)) - 6 * (882191263222842597187 / 10000000000000000000000))) ≤ Vfield (4601713724651 / 6400000000000)

theorem Zeta5Irrational.V_618 : 2711534729338718410971 / 5000000000000000000000 - 6 * (3 / 40) * -(1603815203661389908143 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (212127639484407 / 250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (439767956615355164713 / 1250000000000000000000)) - 6 * (881610596728614691281 / 10000000000000000000000))) ≤ Vfield (5759761335453 / 8000000000000)

theorem Zeta5Irrational.V_619 : 1085721043342463421133 / 2000000000000000000000 - 6 * (3 / 40) * -(3194513272609733674267 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4245357948355271 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3519774136081336267697 / 10000000000000000000000)) - 6 * (22025776883336704059 / 250000000000000000000))) ≤ Vfield (23069522060369 / 32000000000000)

theorem Zeta5Irrational.V_620 : 2717068955990445230723 / 5000000000000000000000 - 6 * (3 / 40) * -(3181413321281778418051 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8496322509423929 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (176070132054670847363 / 500000000000000000000)) - 6 * (440226347639341872671 / 5000000000000000000000))) ≤ Vfield (11549999389463 / 16000000000000)

theorem Zeta5Irrational.V_621 : 543966754787035356037 / 1000000000000000000000 - 6 * (3 / 40) * -(3168330508377498755171 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8501925424845501 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (220189323267150120757 / 625000000000000000000)) - 6 * (439937726411396261549 / 5000000000000000000000))) ≤ Vfield (23130475497483 / 32000000000000)

theorem Zeta5Irrational.V_622 : 5445194127762287189187 / 10000000000000000000000 - 6 * (3 / 40) * -(126210591564468617503 / 400000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1063440581285023 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3524653733925453359381 / 10000000000000000000000)) - 6 * (219824836060368561831 / 2500000000000000000000))) ≤ Vfield (579023805401 / 800000000000)

theorem Zeta5Irrational.V_623 : 85167463359885447783 / 156250000000000000000 - 6 * (3 / 40) * -(314221611887456540269 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8513120193008883 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3526276330333639916337 / 10000000000000000000000)) - 6 * (87872436582745622019 / 1000000000000000000000))) ≤ Vfield (23191428934597 / 32000000000000)

theorem Zeta5Irrational.V_624 : 5456238133051884174373 / 10000000000000000000000 - 6 * (3 / 40) * -(1564592226615293954067 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8518712060288587 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1763948482885999733877 / 5000000000000000000000)) - 6 * (878150513890413655597 / 10000000000000000000000))) ≤ Vfield (11610952826577 / 16000000000000)