V55: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_661 : 1145983301800406914357 / 2000000000000000000000 - 6 * (3 / 40) * -(499000694584906999959 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1759050891838961 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3606936715486809115069 / 10000000000000000000000)) - 6 * (170134931662895184751 / 2000000000000000000000))) ≤ Vfield (396065285130169 / 512000000000000)

theorem Zeta5Irrational.V_662 : 1148741910766415787971 / 2000000000000000000000 - 6 * (3 / 40) * -(2463635813600251484823 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8809159914837269 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3610854212269592993969 / 10000000000000000000000)) - 6 * (169867660582945952537 / 2000000000000000000000))) ≤ Vfield (794637295669 / 1024000000000)

theorem Zeta5Irrational.V_663 : 5757483600055410461667 / 10000000000000000000000 - 6 * (3 / 40) * -(1216183119845151522901 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2205760863743583 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3614760147456547547451 / 10000000000000000000000)) - 6 * (42400411290363432093 / 500000000000000000000))) ≤ Vfield (398572010538831 / 512000000000000)

theorem Zeta5Irrational.V_664 : 5771238699937592243929 / 10000000000000000000000 - 6 * (3 / 40) * -(120059706984401290531 / 500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2209226295724861 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1809327290937027190591 / 5000000000000000000000)) - 6 * (846684377985567652479 / 10000000000000000000000))) ≤ Vfield (199912686621581 / 256000000000000)

theorem Zeta5Irrational.V_665 : 5798692268665044501883 / 10000000000000000000000 - 6 * (3 / 40) * -(46782798876266465479 / 200000000000000000000) - 2 + 12 * (3 / 40) + 2 * (886456361125207 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3626409189323357591577 / 10000000000000000000000)) - 6 * (844055176835286775381 / 10000000000000000000000))) ≤ Vfield (25145756165739 / 32000000000000)

theorem Zeta5Irrational.V_666 : 728258834231571345467 / 1250000000000000000000 - 6 * (3 / 40) * -(2277468446675428642341 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2223034002555877 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (363411851176786735763 / 1000000000000000000000)) - 6 * (420725158977982490263 / 5000000000000000000000))) ≤ Vfield (202419412030243 / 256000000000000)

theorem Zeta5Irrational.V_667 : 5853374325948511987951 / 10000000000000000000000 - 6 * (3 / 40) * -(44323499137129365541 / 200000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1114952897202199 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1820891509478601631143 / 5000000000000000000000)) - 6 * (167773885606187475007 / 2000000000000000000000))) ≤ Vfield (101836387367287 / 128000000000000)

theorem Zeta5Irrational.V_668 : 2940301816024167914831 / 5000000000000000000000 - 6 * (3 / 40) * -(86210194747194041833 / 400000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4473512949491491 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (729880634679149746393 / 2000000000000000000000)) - 6 * (418156070855025838797 / 5000000000000000000000))) ≤ Vfield (40985227487781 / 51200000000000)

theorem Zeta5Irrational.V_669 : 1476939748982764032159 / 2500000000000000000000 - 6 * (3 / 40) * -(2094703660133547240031 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8974344947875111 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3656979430493994796031 / 10000000000000000000000)) - 6 * (833778101392414941191 / 10000000000000000000000))) ≤ Vfield (51544875035809 / 64000000000000)

theorem Zeta5Irrational.V_670 : 5961849495794045218043 / 10000000000000000000000 - 6 * (3 / 40) * -(1974690200181473962903 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2257183766004251 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3672002039722087261413 / 10000000000000000000000)) - 6 * (828778365856198504881 / 10000000000000000000000))) ≤ Vfield (104343112775949 / 128000000000000)

theorem Zeta5Irrational.V_671 : 3007824495396823922311 / 5000000000000000000000 - 6 * (3 / 40) * -(1856099999143922723371 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1135349935516639 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (737370870709823805733 / 2000000000000000000000)) - 6 * (82386750778903374503 / 1000000000000000000000))) ≤ Vfield (2639911887007 / 3200000000000)

theorem Zeta5Irrational.V_672 : 1517290148843070986257 / 2500000000000000000000 - 6 * (3 / 40) * -(434724923741976688371 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (9136543990028577 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (925384943603547055683 / 2500000000000000000000)) - 6 * (409521462399309001603 / 5000000000000000000000))) ≤ Vfield (106849838184611 / 128000000000000)