V13: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_157 : 206810046119531065579 / 2000000000000000000000 - 6 * (3 / 40) * -(2166608875177930686979 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3300613042921201 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 3188028432898504270633 / 10000000000000000000000) - 6 * (2234364613470351213961 / 10000000000000000000000))) ≤ Vfield (278887589353 / 2560000000000)

theorem Zeta5Irrational.V_158 : 1037209045854065450943 / 10000000000000000000000 - 6 * (3 / 40) * -(21635554721982830516497 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (330591611702887 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 798202446697152099411 / 2500000000000000000000) - 6 * (2230898265082615487957 / 10000000000000000000000))) ≤ Vfield (1748653019653 / 16000000000000)

theorem Zeta5Irrational.V_159 : 520183431807087761219 / 5000000000000000000000 - 6 * (3 / 40) * -(5401278410286320760879 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3311210698001703 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 3197581975657524269899 / 10000000000000000000000) - 6 * (445489600655899282081 / 2000000000000000000000))) ≤ Vfield (7017034423399 / 64000000000000)

theorem Zeta5Irrational.V_160 : 1043523684507768985099 / 10000000000000000000000 - 6 * (3 / 40) * -(5393691236272463449183 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3316496826515987 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 3202345041943094693627 / 10000000000000000000000) - 6 * (139000856499547490079 / 625000000000000000000))) ≤ Vfield (3519728384093 / 32000000000000)

theorem Zeta5Irrational.V_161 : 1046679509164033035797 / 10000000000000000000000 - 6 * (3 / 40) * -(21544508074760811294807 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1660887271462177 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 801774756937861789931 / 2500000000000000000000) - 6 * (2220595244489986577137 / 10000000000000000000000))) ≤ Vfield (7061879112973 / 64000000000000)

theorem Zeta5Irrational.V_162 : 41993373528462375119 / 400000000000000000000 - 6 * (3 / 40) * -(21514342476161710872833 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1663521943629689 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 1605921987430325739573 / 5000000000000000000000) - 6 * (138574531459758201139 / 625000000000000000000))) ≤ Vfield (44276884111 / 400000000000)

theorem Zeta5Irrational.V_163 : 526494086139172486441 / 5000000000000000000000 - 6 * (3 / 40) * -(21484267600294531528243 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (666460979847423 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 804144981181080084799 / 2500000000000000000000) - 6 * (2213805360475395042061 / 10000000000000000000000))) ≤ Vfield (7106723802547 / 64000000000000)

theorem Zeta5Irrational.V_164 : 132017626498974098703 / 1250000000000000000000 - 6 * (3 / 40) * -(21454282903099725251803 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3337557618260599 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1610653459237582293741 / 5000000000000000000000) - 6 * (442086739402679778117 / 2000000000000000000000))) ≤ Vfield (3564573073667 / 32000000000000)

theorem Zeta5Irrational.V_165 : 1059292857978712554033 / 10000000000000000000000 - 6 * (3 / 40) * -(2142438784539716247631 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (668560416684657 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 806506249232123808033 / 2500000000000000000000) - 6 * (2207077395399656451427 / 10000000000000000000000))) ≤ Vfield (7151568492121 / 64000000000000)

theorem Zeta5Irrational.V_166 : 531221855432660748179 / 5000000000000000000000 - 6 * (3 / 40) * -(10697290946413978844261 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1674019166756219 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 807683550146417840233 / 2500000000000000000000) - 6 * (2203736339310343190637 / 10000000000000000000000))) ≤ Vfield (1793497709227 / 16000000000000)

theorem Zeta5Irrational.V_167 : 266398392819311274443 / 2500000000000000000000 - 6 * (3 / 40) * -(21364864515797159093447 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1676633203506243 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 647086913927502052769 / 2000000000000000000000) - 6 * (2200410413651344220241 / 10000000000000000000000))) ≤ Vfield (1439282636339 / 12800000000000)

theorem Zeta5Irrational.V_168 : 16699100622492466183 / 156250000000000000000 - 6 * (3 / 40) * -(21335235189417287986779 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3358486342108319 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1620063071983821825819 / 5000000000000000000000) - 6 * (137318719033849222699 / 625000000000000000000))) ≤ Vfield (3609417763241 / 32000000000000)