V26: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_313 : 1273198027115672337129 / 5000000000000000000000 - 6 * (3 / 40) * -(2437349842463477713527 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (269256675543211 / 500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (154369229599612503803 / 625000000000000000000)) - 6 * (1383821717991019276453 / 10000000000000000000000))) ≤ Vfield (18559784275093 / 64000000000000)

theorem Zeta5Irrational.V_314 : 31888790812351289161 / 125000000000000000000 - 6 * (3 / 40) * -(6083112358839418315309 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2695384948571201 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2472091811095637514179 / 10000000000000000000000)) - 6 * (691196609194341337837 / 5000000000000000000000))) ≤ Vfield (37197312107439 / 128000000000000)

theorem Zeta5Irrational.V_315 : 511161652200807009039 / 2000000000000000000000 - 6 * (3 / 40) * -(12145742262259655687553 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5396400396379109 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (247427264076666588767 / 1000000000000000000000)) - 6 * (1380969133676600751081 / 10000000000000000000000))) ≤ Vfield (9318763916173 / 32000000000000)

theorem Zeta5Irrational.V_316 : 1280255522181114874191 / 5000000000000000000000 - 6 * (3 / 40) * -(47364459664837705379 / 39062500000000000000) - 2 + 12 * (3 / 40) + 2 * (5402025026982429 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (247645017284463756857 / 1000000000000000000000)) - 6 * (689774720579922654177 / 5000000000000000000000))) ≤ Vfield (7470559844389 / 25600000000000)

theorem Zeta5Irrational.V_317 : 1282605808571419532773 / 5000000000000000000000 - 6 * (3 / 40) * -(1210490278268556981051 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1081528761452943 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (619656104378955515141 / 2500000000000000000000)) - 6 * (344533529576622148267 / 2500000000000000000000))) ≤ Vfield (18715271389599 / 64000000000000)

theorem Zeta5Irrational.V_318 : 1284954990711541413163 / 5000000000000000000000 - 6 * (3 / 40) * -(6042272708977260666909 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2706628377721641 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2480795384915372937519 / 10000000000000000000000)) - 6 * (43022598210815649167 / 312500000000000000000))) ≤ Vfield (37508286336451 / 128000000000000)

theorem Zeta5Irrational.V_319 : 20114110463103549801 / 78125000000000000000 - 6 * (3 / 40) * -(12064229411273515284231 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5418863889641097 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (496592617025537929121 / 2000000000000000000000)) - 6 * (275063298453652888357 / 2000000000000000000000))) ≤ Vfield (4698253736713 / 16000000000000)

theorem Zeta5Irrational.V_320 : 2579300092776726062851 / 10000000000000000000000 - 6 * (3 / 40) * -(3010988648734265671267 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5424465227887459 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (310640941023347092163 / 1250000000000000000000)) - 6 * (1373914144821106679677 / 10000000000000000000000))) ≤ Vfield (37663773450957 / 128000000000000)

theorem Zeta5Irrational.V_321 : 645997960997488683677 / 2500000000000000000000 - 6 * (3 / 40) * -(12023720802257671034363 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5430060788118679 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (621822181019150037887 / 2500000000000000000000)) - 6 * (1372516078509845972423 / 10000000000000000000000))) ≤ Vfield (3774151700821 / 12800000000000)

theorem Zeta5Irrational.V_322 : 647170348745621798299 / 2500000000000000000000 - 6 * (3 / 40) * -(120035278675576217591 / 100000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2717825294089373 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (248944668273143873453 / 1000000000000000000000)) - 6 * (1371122271595357286801 / 10000000000000000000000))) ≤ Vfield (37819260565463 / 128000000000000)

theorem Zeta5Irrational.V_323 : 518673749563393131451 / 2000000000000000000000 - 6 * (3 / 40) * -(5991687813080415260473 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1360308661454999 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2491601414036235246563 / 10000000000000000000000)) - 6 * (684866351246375430211 / 5000000000000000000000))) ≤ Vfield (9474251030679 / 32000000000000)

theorem Zeta5Irrational.V_324 : 1299026952276566602519 / 5000000000000000000000 - 6 * (3 / 40) * -(11963263914384789373721 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1361703244675941 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2493752927826940413923 / 10000000000000000000000)) - 6 * (1368347349769969504417 / 10000000000000000000000))) ≤ Vfield (37974747679969 / 128000000000000)