V54: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_649 : 5604915436253217929901 / 10000000000000000000000 - 6 * (3 / 40) * -(695457516331357721269 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4334550852547449 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3571148693088848187633 / 10000000000000000000000)) - 6 * (862992740403722005993 / 10000000000000000000000))) ≤ Vfield (38478502079119 / 51200000000000)

theorem Zeta5Irrational.V_650 : 5611901084701233859877 / 10000000000000000000000 - 6 * (3 / 40) * -(2765677579757732943883 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4338079156575929 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3573162398496421435577 / 10000000000000000000000)) - 6 * (215573578818150291501 / 2500000000000000000000))) ≤ Vfield (770823404286711 / 1024000000000000)

theorem Zeta5Irrational.V_651 : 112377637132543891181 / 200000000000000000000 - 6 * (3 / 40) * -(2749551142400356585123 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4341604593248587 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (178758653142059377991 / 500000000000000000000)) - 6 * (861597583128492385527 / 10000000000000000000000))) ≤ Vfield (386038383495521 / 512000000000000)

theorem Zeta5Irrational.V_652 : 2812928879417364386841 / 5000000000000000000000 - 6 * (3 / 40) * -(136672533468778197849 / 500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2172563584772373 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (894295173585930991351 / 2500000000000000000000)) - 6 * (215225634285677686871 / 2500000000000000000000))) ≤ Vfield (773330129695373 / 1024000000000000)

theorem Zeta5Irrational.V_653 : 5632828798113236739333 / 10000000000000000000000 - 6 * (3 / 40) * -(543475215442021519619 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (8697293784830921 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3579185301191316278443 / 10000000000000000000000)) - 6 * (21505229263126765113 / 250000000000000000000))) ≤ Vfield (96822936549963 / 128000000000000)

theorem Zeta5Irrational.V_654 : 5639794981237929828231 / 10000000000000000000000 - 6 * (3 / 40) * -(1350663641416316901041 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2176081884391839 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1790593445769071451627 / 5000000000000000000000)) - 6 * (85951747652360666837 / 1000000000000000000000))) ≤ Vfield (155167371020807 / 204800000000000)

theorem Zeta5Irrational.V_655 : 1411689078742467514661 / 2500000000000000000000 - 6 * (3 / 40) * -(2685304203571106785121 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4355677805544397 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1791592736752728819669 / 5000000000000000000000)) - 6 * (107353431053037252639 / 1250000000000000000000))) ≤ Vfield (388545108904183 / 512000000000000)

theorem Zeta5Irrational.V_656 : 5660664461229229342117 / 10000000000000000000000 - 6 * (3 / 40) * -(1326667430844514298871 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (872539477536907 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1793586822311514017451 / 5000000000000000000000)) - 6 * (428726181632072282809 / 5000000000000000000000))) ≤ Vfield (194899235804257 / 256000000000000)

theorem Zeta5Irrational.V_657 : 2837276645349158187007 / 5000000000000000000000 - 6 * (3 / 40) * -(524293479615471020593 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1092426423360713 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (897787469715603738619 / 2500000000000000000000)) - 6 * (85608386208098783843 / 1000000000000000000000))) ≤ Vfield (78210366862569 / 102400000000000)

theorem Zeta5Irrational.V_658 : 711052857120031112197 / 1250000000000000000000 - 6 * (3 / 40) * -(1294850582738612798973 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2188351388494561 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (898778560006669417019 / 2500000000000000000000)) - 6 * (17094437850020888933 / 200000000000000000000))) ≤ Vfield (49038149627147 / 64000000000000)

theorem Zeta5Irrational.V_659 : 1425568303343877683293 / 2500000000000000000000 - 6 * (3 / 40) * -(319754440347319404593 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4383688692060797 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3599066791409163219773 / 10000000000000000000000)) - 6 * (853366402731951753291 / 10000000000000000000000))) ≤ Vfield (393558559721507 / 512000000000000)

theorem Zeta5Irrational.V_660 : 5716104413083145056471 / 10000000000000000000000 - 6 * (3 / 40) * -(2526469834942398681093 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4390663491967827 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (720601519159810012143 / 2000000000000000000000)) - 6 * (6656385480894487883 / 78125000000000000000))) ≤ Vfield (197405961212919 / 256000000000000)