This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∉ ℚ