V31: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_373 : 3167046557416502155937 / 10000000000000000000000 - 6 * (3 / 40) * -(9722736274507547290279 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3052036710852029 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2740184174711295780057 / 10000000000000000000000)) - 6 * (1222560062854347182191 / 10000000000000000000000))) ≤ Vfield (47692431792069 / 128000000000000)

theorem Zeta5Irrational.V_374 : 3171810405818957948811 / 10000000000000000000000 - 6 * (3 / 40) * -(4852729359299315616467 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (305471424036659 / 500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2742134413310491105127 / 10000000000000000000000)) - 6 * (610749546040129944137 / 5000000000000000000000))) ≤ Vfield (5972018617791 / 16000000000000)

theorem Zeta5Irrational.V_375 : 1588285992938407841959 / 5000000000000000000000 - 6 * (3 / 40) * -(9688210962603965581069 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3057389425017427 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1372041008083511690423 / 5000000000000000000000)) - 6 * (305110219698251537417 / 2500000000000000000000))) ≤ Vfield (47859866092587 / 128000000000000)

theorem Zeta5Irrational.V_376 : 3181331299749228225409 / 10000000000000000000000 - 6 * (3 / 40) * -(4835496451952082468179 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (76501556773859 / 125000000000000 * (Real.pi + (Real.pi / 2 - 2 * (686506747566213541199 / 2500000000000000000000)) - 6 * (243877082213678186227 / 2000000000000000000000))) ≤ Vfield (23971791621423 / 64000000000000)

theorem Zeta5Irrational.V_377 : 19913052184951669237 / 62500000000000000000 - 6 * (3 / 40) * -(4826902220204502580303 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3062732784300373 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (171748083909903721723 / 625000000000000000000)) - 6 * (15229158463178572059 / 125000000000000000000))) ≤ Vfield (9605460078621 / 25600000000000)

theorem Zeta5Irrational.V_378 : 1595421568779464123529 / 5000000000000000000000 - 6 * (3 / 40) * -(9636645470553791427333 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (153270048557589 / 250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (54998181599460134389 / 200000000000000000000)) - 6 * (608641332485034393921 / 5000000000000000000000))) ≤ Vfield (12027754385841 / 32000000000000)

theorem Zeta5Irrational.V_379 : 798898916449784521491 / 2500000000000000000000 - 6 * (3 / 40) * -(9619515893295757380253 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1534033418789193 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2751846209404526497207 / 10000000000000000000000)) - 6 * (1216235363106071541963 / 10000000000000000000000))) ≤ Vfield (48194734693623 / 128000000000000)

theorem Zeta5Irrational.V_380 : 1600172968229879563989 / 5000000000000000000000 - 6 * (3 / 40) * -(9602415608110495079503 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1228292155849459 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2753780737720085654817 / 10000000000000000000000)) - 6 * (303797689955757674163 / 2500000000000000000000))) ≤ Vfield (24139225921941 / 64000000000000)

theorem Zeta5Irrational.V_381 : 1602546975842297952737 / 5000000000000000000000 - 6 * (3 / 40) * -(9585344514988415420279 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6146783266609669 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (275571267175795931953 / 1000000000000000000000)) - 6 * (75884302721971491671 / 625000000000000000000))) ≤ Vfield (48362168994141 / 128000000000000)

theorem Zeta5Irrational.V_382 : 320983971361440075487 / 1000000000000000000000 - 6 * (3 / 40) * -(1196037814303904839033 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (49216809193811 / 80000000000000 * (Real.pi + (Real.pi / 2 - 2 * (551528403665559915819 / 2000000000000000000000)) - 6 * (1213109602791532020873 / 10000000000000000000000))) ≤ Vfield (121114715361 / 320000000000)

theorem Zeta5Irrational.V_383 : 3214583224386879607881 / 10000000000000000000000 - 6 * (3 / 40) * -(1193911188431064389001 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1539353609757037 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (86236524506587603067 / 312500000000000000000)) - 6 * (60603651305585332871 / 500000000000000000000))) ≤ Vfield (48529603294659 / 128000000000000)

theorem Zeta5Irrational.V_384 : 643864897227339553809 / 2000000000000000000000 - 6 * (3 / 40) * -(9534305395554174604017 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1232544629578859 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (276149297615988133653 / 1000000000000000000000)) - 6 * (242207820429808106391 / 2000000000000000000000))) ≤ Vfield (24306660222459 / 64000000000000)