V00: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_1 : 8967502915859873 / 250000000000000000000 - 6 * (3 / 40) * -(25870887852728765963031 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (14973028876951 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 11978279880015751031 / 2000000000000000000000) - 6 * (Real.pi / 2 - 796870528491162609301 / 10000000000000000000000))) ≤ Vfield (7174131 / 200000000000)

theorem Zeta5Irrational.V_2 : 67255668762557231 / 1250000000000000000000 - 6 * (3 / 40) * -(25855071403081196359633 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (4584535081561 / 625000000000000 * (Real.pi + (Real.pi / 2 - 73351245745236760791 / 10000000000000000000000) - 6 * (Real.pi / 2 - 974933462669317096681 / 10000000000000000000000))) ≤ Vfield (21522393 / 400000000000)

theorem Zeta5Irrational.V_3 : 358693683576464417 / 5000000000000000000000 - 6 * (3 / 40) * -(25839304827724134032909 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (5293765126897 / 625000000000000 * (Real.pi + (Real.pi / 2 - 16939643323085595789 / 2000000000000000000000) - 6 * (Real.pi / 2 - 35142868108192574273 / 312500000000000000000))) ≤ Vfield (7174131 / 100000000000)

theorem Zeta5Irrational.V_4 : 37063408769787157 / 500000000000000000000 - 6 * (3 / 40) * -(51674418216178446788859 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (86098527861981 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 17219280094892480421 / 2000000000000000000000) - 6 * (Real.pi / 2 - 1142976954465331252621 / 10000000000000000000000))) ≤ Vfield (14825913 / 200000000000)

theorem Zeta5Irrational.V_5 : 196661542144736661 / 2500000000000000000000 - 6 * (3 / 40) * -(51666458509222761164599 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (88694820029133 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 44346247166374961649 / 5000000000000000000000) - 6 * (Real.pi / 2 - 117713038222569168397 / 1000000000000000000000))) ≤ Vfield (78667711 / 1000000000000)

theorem Zeta5Irrational.V_6 : 85811957048696007 / 1000000000000000000000 - 6 * (3 / 40) * -(51653934194779139713727 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (92636730836101 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 92634081079116824847 / 10000000000000000000000) - 6 * (Real.pi / 2 - 614466029692359913717 / 5000000000000000000000))) ≤ Vfield (85815639 / 1000000000000)

theorem Zeta5Irrational.V_7 : 30107723030942933 / 312500000000000000000 - 6 * (3 / 40) * -(25817752990537051829671 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (19631541457563 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 49077277496392064609 / 5000000000000000000000) - 6 * (Real.pi / 2 - 1301372761809135071741 / 10000000000000000000000))) ≤ Vfield (19269871 / 200000000000)

theorem Zeta5Irrational.V_8 : 278789739678365227 / 2500000000000000000000 - 6 * (3 / 40) * -(51609021536891161835761 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (105604031173059 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 52800052853726802719 / 5000000000000000000000) - 6 * (Real.pi / 2 - 1398857469718843080699 / 10000000000000000000000))) ≤ Vfield (55761057 / 500000000000)

theorem Zeta5Irrational.V_9 : 1333382420614834419 / 10000000000000000000000 - 6 * (3 / 40) * -(51571047996245974723013 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (57738014340641 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 115470896292829511109 / 10000000000000000000000) - 6 * (Real.pi / 2 - 763841962364687947279 / 5000000000000000000000))) ≤ Vfield (33336783 / 250000000000)

theorem Zeta5Irrational.V_10 : 66033623550755633 / 400000000000000000000 - 6 * (3 / 40) * -(51516061139574022265869 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (128490344384317 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 25696654786369851871 / 2000000000000000000000) - 6 * (Real.pi / 2 - 1696732463001094446147 / 10000000000000000000000))) ≤ Vfield (82548843 / 500000000000)

theorem Zeta5Irrational.V_11 : 1060918377258494863 / 5000000000000000000000 - 6 * (3 / 40) * -(51435029869943759185693 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (18209123228481 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 145662682903283762149 / 10000000000000000000000) - 6 * (Real.pi / 2 - 1918420011923721109387 / 10000000000000000000000))) ≤ Vfield (53051547 / 250000000000)

theorem Zeta5Irrational.V_12 : 2480279280302765263 / 10000000000000000000000 - 6 * (3 / 40) * -(12843449268270218651961 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (9843674394551 / 625000000000000 * (Real.pi + (Real.pi / 2 - 39371442317394135319 / 2500000000000000000000) - 6 * (Real.pi / 2 - 2069906494283519593871 / 10000000000000000000000))) ≤ Vfield (496117379 / 2000000000000)