V11: certified bounds for the zeta(5) proof #
theorem
Zeta5Irrational.V_133 :
190058421104230496931 / 2500000000000000000000 - 6 * (3 / 40) * -(6174174657182944863893 / 2500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2810476616623781 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2739799349363924849661 / 10000000000000000000000) - 6 * (2607816221361664600063 / 10000000000000000000000))) ≤ Vfield (5055218440057 / 64000000000000)
theorem
Zeta5Irrational.V_134 :
382551253599223766289 / 5000000000000000000000 - 6 * (3 / 40) * -(1231739400428765560097 / 500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (140990474916221 / 500000000000000 * (Real.pi + (Real.pi / 2 - 687111727224121272759 / 2500000000000000000000) - 6 * (1299784604025157638269 / 5000000000000000000000))) ≤ Vfield (2544424194189 / 32000000000000)
theorem
Zeta5Irrational.V_135 :
30798758423600499343 / 400000000000000000000 - 6 * (3 / 40) * -(4914651664744565192507 / 2000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2829111592195009 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 689265436739419728229 / 2500000000000000000000) - 6 * (1295699988500512258437 / 5000000000000000000000))) ≤ Vfield (5122478336699 / 64000000000000)
theorem
Zeta5Irrational.V_136 :
774833046896600384011 / 10000000000000000000000 - 6 * (3 / 40) * -(24512104915046550125607 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (567676640186779 / 2000000000000000 * (Real.pi + (Real.pi / 2 - 691411043894439901673 / 2500000000000000000000) - 6 * (645826828166487246769 / 2500000000000000000000))) ≤ Vfield (257805414251 / 3200000000000)
theorem
Zeta5Irrational.V_137 :
196138531864494114447 / 2500000000000000000000 - 6 * (3 / 40) * -(3048863589055876755923 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2856836149282431 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2782713027656475583597 / 10000000000000000000000) - 6 * (2567346953413312793429 / 10000000000000000000000))) ≤ Vfield (2611684090831 / 32000000000000)
theorem
Zeta5Irrational.V_138 :
198566441813831119773 / 2500000000000000000000 - 6 * (3 / 40) * -(3033895473797801538299 / 1250000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1437585334193243 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 279965586309664145921 / 1000000000000000000000) - 6 * (2551678921654980299883 / 10000000000000000000000))) ≤ Vfield (165332127447 / 2000000000000)
theorem
Zeta5Irrational.V_139 :
803967984607916239937 / 10000000000000000000000 - 6 * (3 / 40) * -(1207641790130783507417 / 500000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2893389009596379 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 2816475004873911548537 / 10000000000000000000000) - 6 * (1268147198934660719937 / 5000000000000000000000))) ≤ Vfield (2678943987473 / 32000000000000)
theorem
Zeta5Irrational.V_140 :
406830398890876967997 / 5000000000000000000000 - 6 * (3 / 40) * -(24035891607929812287671 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2911493353823127 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1416586352121228549643 / 5000000000000000000000) - 6 * (1260592465377202839901 / 5000000000000000000000))) ≤ Vfield (1356286967897 / 16000000000000)
theorem
Zeta5Irrational.V_141 :
52063642774504058401 / 625000000000000000000 - 6 * (3 / 40) * -(2380602772690295968647 / 1000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (2947368440891381 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1433106220253817106089 / 5000000000000000000000) - 6 * (1245879543219645552791 / 5000000000000000000000))) ≤ Vfield (694958458109 / 8000000000000)
theorem
Zeta5Irrational.V_142 :
852338372156698860517 / 10000000000000000000000 - 6 * (3 / 40) * -(23581329078528711081391 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1491406039897313 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 2898791760613854838001 / 10000000000000000000000) - 6 * (2463340430743041968497 / 10000000000000000000000))) ≤ Vfield (1423546864539 / 16000000000000)
theorem
Zeta5Irrational.V_143 :
43581060265344278991 / 500000000000000000000 - 6 * (3 / 40) * -(23361568621129862900791 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (3017839472267369 / 10000000000000000 * (Real.pi + (Real.pi / 2 - 1465463193295560484297 / 5000000000000000000000) - 6 * (487174553803326026091 / 2000000000000000000000))) ≤ Vfield (72858840643 / 800000000000)
theorem
Zeta5Irrational.V_144 :
910075680531480208983 / 10000000000000000000000 - 6 * (3 / 40) * -(22936026120516716875781 / 10000000000000000000000) - 2 + 12 * (3 / 40) + 2 * (1543351016002799 / 5000000000000000 * (Real.pi + (Real.pi / 2 - 18712000414536656493 / 62500000000000000000) - 6 * (595896677737549471971 / 2500000000000000000000))) ≤ Vfield (762218354751 / 8000000000000)