V32: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_385 : 403007937624435709943 / 1250000000000000000000 - 6 * (3 / 40) * -(9517350080763106229959 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6168027287652999 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2763414600899822286143 / 10000000000000000000000)) - 6 * (605003909804122796891 / 5000000000000000000000))) ≤ Vfield (48697037595177 / 128000000000000)

theorem Zeta5Irrational.V_386 : 3228800271091844667397 / 10000000000000000000000 - 6 * (3 / 40) * -(4750211732793883134469 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (617332687008163 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2765333665127458345457 / 10000000000000000000000)) - 6 * (1208979167261253981733 / 10000000000000000000000))) ≤ Vfield (12195188686359 / 32000000000000)

theorem Zeta5Irrational.V_387 : 202095924909459542751 / 625000000000000000000 - 6 * (3 / 40) * -(4741762726517407558013 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6178621906907049 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1383625087755914228753 / 5000000000000000000000)) - 6 * (301988283486676190467 / 2500000000000000000000))) ≤ Vfield (9772894379139 / 25600000000000)

theorem Zeta5Irrational.V_388 : 323826708549657002721 / 1000000000000000000000 - 6 * (3 / 40) * -(9466655946601782328347 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6183912409805911 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (173072758668396268933 / 625000000000000000000)) - 6 * (1206929708569435187719 / 10000000000000000000000))) ≤ Vfield (24474094522977 / 64000000000000)

theorem Zeta5Irrational.V_389 : 405965618289914982473 / 1250000000000000000000 - 6 * (3 / 40) * -(9433002068520124417443 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1548619965070337 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (554596889976445321921 / 2000000000000000000000)) - 6 * (1204890637574057060631 / 10000000000000000000000))) ≤ Vfield (6139452918309 / 16000000000000)

theorem Zeta5Irrational.V_390 : 203573366905027506113 / 625000000000000000000 - 6 * (3 / 40) * -(4699730534507726419707 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3102514656964207 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2776794651275838889401 / 10000000000000000000000)) - 6 * (240572373363749729447 / 2000000000000000000000))) ≤ Vfield (4928305764699 / 12800000000000)

theorem Zeta5Irrational.V_391 : 816653468713089555349 / 2500000000000000000000 - 6 * (3 / 40) * -(2341508048351393276649 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3107780431191633 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (86893587344624066073 / 312500000000000000000)) - 6 * (1200843309874540748747 / 10000000000000000000000))) ≤ Vfield (12362622986877 / 32000000000000)

theorem Zeta5Irrational.V_392 : 3276044976259764027657 / 10000000000000000000000 - 6 * (3 / 40) * -(9332714694551548750447 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6226074596507039 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (21753007288003625813 / 78125000000000000000)) - 6 * (299708720331099562257 / 2500000000000000000000))) ≤ Vfield (24808963124013 / 64000000000000)

theorem Zeta5Irrational.V_393 : 657093438295957909727 / 2000000000000000000000 - 6 * (3 / 40) * -(2324876958189376444893 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6236570606394991 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2788165116089121008927 / 10000000000000000000000)) - 6 * (1196836496748037631457 / 10000000000000000000000))) ≤ Vfield (777896258571 / 2000000000000)

theorem Zeta5Irrational.V_394 : 1647440268621094061217 / 5000000000000000000000 - 6 * (3 / 40) * -(9266410875672095229157 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (195220280668297 / 312500000000000 * (Real.pi + (Real.pi / 2 - 2 * (2791935395588520664673 / 10000000000000000000000)) - 6 * (1194848072707023067937 / 10000000000000000000000))) ≤ Vfield (24976397424531 / 64000000000000)

theorem Zeta5Irrational.V_395 : 660857006045902524463 / 2000000000000000000000 - 6 * (3 / 40) * -(923342309819158098361 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6257509810068967 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (139784791091839437819 / 500000000000000000000)) - 6 * (596434763365065326249 / 5000000000000000000000))) ≤ Vfield (2506011457479 / 6400000000000)

theorem Zeta5Irrational.V_396 : 828420171769323212123 / 2500000000000000000000 - 6 * (3 / 40) * -(4600271891182260404739 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6267953180296503 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (349930805612534943393 / 1250000000000000000000)) - 6 * (1190900777298982651693 / 10000000000000000000000))) ≤ Vfield (25143831725049 / 64000000000000)