V29: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_349 : 372432974215837231393 / 1250000000000000000000 - 6 * (3 / 40) * -(10420961770985507744611 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2945715338232803 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2661991062193999150973 / 10000000000000000000000)) - 6 * (1266224519414994741439 / 10000000000000000000000))) ≤ Vfield (86772388539 / 250000000000)

theorem Zeta5Irrational.V_350 : 119954631949475568979 / 400000000000000000000 - 6 * (3 / 40) * -(10347063308137192662121 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2956796049364893 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1335104378906465501497 / 5000000000000000000000)) - 6 * (630764785401862489949 / 5000000000000000000000))) ≤ Vfield (11190582883251 / 32000000000000)

theorem Zeta5Irrational.V_351 : 3018230232850539159649 / 10000000000000000000000 - 6 * (3 / 40) * -(2568426735005533212383 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5935670779677621 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (334797489789192552847 / 1250000000000000000000)) - 6 * (628443231648490909653 / 5000000000000000000000))) ≤ Vfield (1127430003351 / 3200000000000)

theorem Zeta5Irrational.V_352 : 759389310323588584061 / 2500000000000000000000 - 6 * (3 / 40) * -(10200884771266944986441 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5957667639208997 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2686505063364219207891 / 10000000000000000000000)) - 6 * (1252294249803677508751 / 10000000000000000000000))) ≤ Vfield (11358017183769 / 32000000000000)

theorem Zeta5Irrational.V_353 : 2437765404834750633 / 8000000000000000000 - 6 * (3 / 40) * -(5082335795652477889393 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (596863566877371 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1345275269978941688457 / 5000000000000000000000)) - 6 * (1250016938943352110893 / 10000000000000000000000))) ≤ Vfield (22799751517797 / 64000000000000)

theorem Zeta5Irrational.V_354 : 3056846968454616536319 / 10000000000000000000000 - 6 * (3 / 40) * -(10128589077740964565741 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5979583580303689 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1347292351694098581751 / 5000000000000000000000)) - 6 * (623876003640546214071 / 5000000000000000000000))) ≤ Vfield (2860433583507 / 8000000000000)

theorem Zeta5Irrational.V_355 : 766619474111480287379 / 2500000000000000000000 - 6 * (3 / 40) * -(5046318145504354096527 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5990511484098597 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1349303808025649067077 / 5000000000000000000000)) - 6 * (1245499343066240103687 / 10000000000000000000000))) ≤ Vfield (4593437163663 / 12800000000000)

theorem Zeta5Irrational.V_356 : 3076099557883663825427 / 10000000000000000000000 - 6 * (3 / 40) * -(2514203075409914914533 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6001419489453879 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2702619339793887572677 / 10000000000000000000000)) - 6 * (310814708988853740969 / 2500000000000000000000))) ≤ Vfield (11525451484287 / 32000000000000)

theorem Zeta5Irrational.V_357 : 3085711970582634738283 / 10000000000000000000000 - 6 * (3 / 40) * -(1252639523764855944051 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3006153852336759 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (8458187299750094947 / 31250000000000000000)) - 6 * (620515188494905216727 / 5000000000000000000000))) ≤ Vfield (23134620118833 / 64000000000000)

theorem Zeta5Irrational.V_358 : 773828788076575112559 / 2500000000000000000000 - 6 * (3 / 40) * -(4992773523371619840171 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6023176237082577 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1355304732598921570641 / 5000000000000000000000)) - 6 * (1238813858572936387099 / 10000000000000000000000))) ≤ Vfield (5804584317273 / 16000000000000)

theorem Zeta5Irrational.V_359 : 620022657417898369221 / 2000000000000000000000 - 6 * (3 / 40) * -(498390490323817900053 / 500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (602860315550759 / 1000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (542520019722747216779 / 2000000000000000000000)) - 6 * (1237710043813499311807 / 10000000000000000000000))) ≤ Vfield (46520391688443 / 128000000000000)

theorem Zeta5Irrational.V_360 : 3104909120767000870261 / 10000000000000000000000 - 6 * (3 / 40) * -(4975051985741318175863 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1206805038607909 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2714587987866077907253 / 10000000000000000000000)) - 6 * (1236609174448796264479 / 10000000000000000000000))) ≤ Vfield (23302054419351 / 64000000000000)