Metamath Proof Explorer


Theorem eirr

Description: _e is irrational. (Contributed by Paul Chapman, 9-Feb-2008) (Proof shortened by Mario Carneiro, 29-Apr-2014)

Ref Expression
Assertion eirr e ∉ ℚ

Proof

Step Hyp Ref Expression
1 eqid ( 𝑛 ∈ ℕ0 ↦ ( 1 / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 1 / ( ! ‘ 𝑛 ) ) )
2 simpll ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ e = ( 𝑝 / 𝑞 ) ) → 𝑝 ∈ ℤ )
3 simplr ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ e = ( 𝑝 / 𝑞 ) ) → 𝑞 ∈ ℕ )
4 simpr ( ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ e = ( 𝑝 / 𝑞 ) ) → e = ( 𝑝 / 𝑞 ) )
5 1 2 3 4 eirrlem ¬ ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) ∧ e = ( 𝑝 / 𝑞 ) )
6 5 imnani ( ( 𝑝 ∈ ℤ ∧ 𝑞 ∈ ℕ ) → ¬ e = ( 𝑝 / 𝑞 ) )
7 6 nrexdv ( 𝑝 ∈ ℤ → ¬ ∃ 𝑞 ∈ ℕ e = ( 𝑝 / 𝑞 ) )
8 7 nrex ¬ ∃ 𝑝 ∈ ℤ ∃ 𝑞 ∈ ℕ e = ( 𝑝 / 𝑞 )
9 elq ( e ∈ ℚ ↔ ∃ 𝑝 ∈ ℤ ∃ 𝑞 ∈ ℕ e = ( 𝑝 / 𝑞 ) )
10 8 9 mtbir ¬ e ∈ ℚ
11 10 nelir e ∉ ℚ