V37: certified bounds for the zeta(5) proof

theorem Zeta5Irrational.V_445 : 765842864606636857627 / 2000000000000000000000 - 6 * (3 / 40) * -(234493277614459757331 / 312500000000000000000) - 2 + 12 * (3 / 40) + 2 * (6830540250086371 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (2996310293174500557039 / 10000000000000000000000)) - 6 * (546814399689969324883 / 5000000000000000000000))) ≤ Vfield (933125602161 / 2000000000000)

theorem Zeta5Irrational.V_446 : 3838240205298106251957 / 10000000000000000000000 - 6 * (3 / 40) * -(747577809759293719037 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1710056835599697 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (599922291000491826411 / 2000000000000000000000)) - 6 * (218418460430541568817 / 2000000000000000000000))) ≤ Vfield (467887100957 / 1000000000000)

theorem Zeta5Irrational.V_447 : 240453621765865922073 / 625000000000000000000 - 6 * (3 / 40) * -(7447849530514487331947 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1369980147058343 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (750726243913883062749 / 2500000000000000000000)) - 6 * (218112452596585238241 / 2000000000000000000000))) ≤ Vfield (938422801667 / 2000000000000)

theorem Zeta5Irrational.V_448 : 3856267566566845575453 / 10000000000000000000000 - 6 * (3 / 40) * -(1854999686683688517279 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3429780243361081 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (1503095444308757277833 / 5000000000000000000000)) - 6 * (217807727351321952453 / 2000000000000000000000))) ≤ Vfield (47053570071 / 100000000000)

theorem Zeta5Irrational.V_449 : 3865269074863888535449 / 10000000000000000000000 - 6 * (3 / 40) * -(7392225314191339633631 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1717301663559907 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3009469227143283066133 / 10000000000000000000000)) - 6 * (1087521378799764588307 / 10000000000000000000000))) ≤ Vfield (943720001173 / 2000000000000)

theorem Zeta5Irrational.V_450 : 3874262487732329959907 / 10000000000000000000000 - 6 * (3 / 40) * -(7364528804411839307839 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3439419647495053 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (753185006065245064909 / 2500000000000000000000)) - 6 * (1086010444872883962773 / 10000000000000000000000))) ≤ Vfield (473184300463 / 1000000000000)

theorem Zeta5Irrational.V_451 : 776649563944038904551 / 2000000000000000000000 - 6 * (3 / 40) * -(3668454396237089531377 / 5000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (215264327053751 / 312500000000000 * (Real.pi + (Real.pi / 2 - 2 * (754000828193542139837 / 2500000000000000000000)) - 6 * (54225289558276524857 / 500000000000000000000))) ≤ Vfield (949017200679 / 2000000000000)

theorem Zeta5Irrational.V_452 : 7784450170672652891 / 20000000000000000000 - 6 * (3 / 40) * -(7309364856967499426647 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (862258027847523 / 1250000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3019259125263958673499 / 10000000000000000000000)) - 6 * (270751843572750147929 / 2500000000000000000000))) ≤ Vfield (59479112527 / 125000000000)

theorem Zeta5Irrational.V_453 : 780238859810106012883 / 2000000000000000000000 - 6 * (3 / 40) * -(7281896579953576581699 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1726914155532383 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (604501498818222252083 / 2000000000000000000000)) - 6 * (216303030256213961533 / 2000000000000000000000))) ≤ Vfield (190862880037 / 400000000000)

theorem Zeta5Irrational.V_454 : 782031095058741953577 / 2000000000000000000000 - 6 * (3 / 40) * -(1813625886732192964727 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6917235719339047 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (3025748451398115421169 / 10000000000000000000000)) - 6 * (33750908736900517841 / 312500000000000000000))) ≤ Vfield (478481499969 / 1000000000000)

theorem Zeta5Irrational.V_455 : 3919108628458009307323 / 10000000000000000000000 - 6 * (3 / 40) * -(451699084174156310643 / 625000000000000000000) - 2 + 12 * (3 / 40) + 2 * (6926801569595449 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2 * (757245507277809449937 / 2500000000000000000000)) - 6 * (269637279260881504219 / 2500000000000000000000))) ≤ Vfield (959611599691 / 2000000000000)

theorem Zeta5Irrational.V_456 : 245503360806059405313 / 625000000000000000000 - 6 * (3 / 40) * -(7199941571780214482551 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1734088556926231 / 2500000000000000 * (Real.pi + (Real.pi / 2 - 2 * (606441651788510147911 / 2000000000000000000000)) - 6 * (538537610962834018837 / 5000000000000000000000))) ≤ Vfield (240565049861 / 500000000000)