V30: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_361 : 621940531108982726093 / 2000000000000000000000 - 6 * (3 / 40) * -(993242943074726082441 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6039442362824217 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2716573140403061887061 / 10000000000000000000000)) - 6 * (617755618701384853011 / 5000000000000000000000))) ≤ Vfield (46687825988961 / 128000000000000)

theorem Zeta5Irrational.V_362 : 1557246946813072634581 / 5000000000000000000000 - 6 * (3 / 40) * -(2478696518460755041279 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6044854677948479 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (42477430681884392329 / 156250000000000000000)) - 6 * (617208109840245433709 / 5000000000000000000000))) ≤ Vfield (2338577156961 / 6400000000000)

theorem Zeta5Irrational.V_363 : 623856567442089207543 / 2000000000000000000000 - 6 * (3 / 40) * -(154643340483221346247 / 156250000000000000000) - 2 + 12 * (3 / 40) + 2 * (6050262151440667 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (544107052992504643051 / 2000000000000000000000)) - 6 * (9635344596621206931 / 78125000000000000000))) ≤ Vfield (46855260289479 / 128000000000000)

theorem Zeta5Irrational.V_364 : 1562034744247203678047 / 5000000000000000000000 - 6 * (3 / 40) * -(9879592472732310410423 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6055664796270951 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (544502450344153676819 / 2000000000000000000000)) - 6 * (1232234890629238011593 / 10000000000000000000000))) ≤ Vfield (23469488719869 / 64000000000000)

theorem Zeta5Irrational.V_365 : 3128853849671467858077 / 10000000000000000000000 - 6 * (3 / 40) * -(9862042010572357117663 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6061062625351691 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2724486531235580131221 / 10000000000000000000000)) - 6 * (1231148553710269436801 / 10000000000000000000000))) ≤ Vfield (47022694589997 / 128000000000000)

theorem Zeta5Irrational.V_366 : 313363592293191942199 / 1000000000000000000000 - 6 * (3 / 40) * -(9844522296328471492081 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3033227825768903 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2726458110795700910111 / 10000000000000000000000)) - 6 * (615032542466899038457 / 5000000000000000000000))) ≤ Vfield (1472075366883 / 4000000000000)

theorem Zeta5Irrational.V_367 : 627683142092582637407 / 2000000000000000000000 - 6 * (3 / 40) * -(491351661122504170979 / 500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6071843887627121 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (545685399531711867479 / 2000000000000000000000)) - 6 * (19202882370327738227 / 156250000000000000000))) ≤ Vfield (9438025778103 / 25600000000000)

theorem Zeta5Irrational.V_368 : 12572772857793862221 / 40000000000000000000 - 6 * (3 / 40) * -(4904787340974963006027 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6077227346360729 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1365196599525230821389 / 5000000000000000000000)) - 6 * (613953350745148672973 / 5000000000000000000000))) ≤ Vfield (23636923020387 / 64000000000000)

theorem Zeta5Irrational.V_369 : 49187006829210377799 / 156250000000000000000 - 6 * (3 / 40) * -(1958429313680021735671 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6082606040423341 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2732356722166779862839 / 10000000000000000000000)) - 6 * (61341588092849836077 / 500000000000000000000))) ≤ Vfield (47357563191033 / 128000000000000)

theorem Zeta5Irrational.V_370 : 3152741380503673934997 / 10000000000000000000000 - 6 * (3 / 40) * -(9774748775928224355261 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6087979982443631 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (683579393543033958129 / 2500000000000000000000)) - 6 * (1225759640432438821581 / 10000000000000000000000))) ≤ Vfield (11860320085323 / 32000000000000)

theorem Zeta5Irrational.V_371 : 394689005865717860253 / 1250000000000000000000 - 6 * (3 / 40) * -(4878690599606745271231 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6093349184994587 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1368137881100294212459 / 5000000000000000000000)) - 6 * (244938064984704678467 / 2000000000000000000000))) ≤ Vfield (47524997491551 / 128000000000000)

theorem Zeta5Irrational.V_372 : 1581140219253604103593 / 5000000000000000000000 - 6 * (3 / 40) * -(974004373348292378993 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6098713660593851 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2738231293355815583263 / 10000000000000000000000)) - 6 * (1223623803112093052309 / 10000000000000000000000))) ≤ Vfield (4760871464181 / 12800000000000)