Irrationality of ζ(5)

Zeta5Irrational.irrational_five is the target statement. It follows from Zeta5Irrational.main_estimate (Theorem 2.1 of the paper, with a smaller decay rate) and the criterion Zeta5Irrational.irrational_of_eventually_exists_int_poly. It depends only on the axioms propext, Classical.choice and Quot.sound.

theorem Zeta5Irrational.irrational_zeta5 : Irrational zeta5

Theorem 1.1 of the paper, from Theorem 2.1.

theorem Zeta5Irrational.irrational_five : ∃ (x : ℝ), Irrational x ∧ riemannZeta 5 = ↑x