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