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 \notin ℚ$

Step	Hyp	Ref	Expression
1		eqid	$⊢ (n \in ℕ_{0} ⟼ \frac{1}{n!}) = (n \in ℕ_{0} ⟼ \frac{1}{n!})$
2		simpll	$⊢ ((p \in ℤ \land q \in ℕ) \land e = \frac{p}{q}) \to p \in ℤ$
3		simplr	$⊢ ((p \in ℤ \land q \in ℕ) \land e = \frac{p}{q}) \to q \in ℕ$
4		simpr	$⊢ ((p \in ℤ \land q \in ℕ) \land e = \frac{p}{q}) \to e = \frac{p}{q}$
5	1 2 3 4	eirrlem	$⊢ \neg ((p \in ℤ \land q \in ℕ) \land e = \frac{p}{q})$
6	5	imnani	$⊢ (p \in ℤ \land q \in ℕ) \to \neg e = \frac{p}{q}$
7	6	nrexdv	$⊢ p \in ℤ \to \neg \exists q \in ℕ e = \frac{p}{q}$
8	7	nrex	$⊢ \neg \exists p \in ℤ \exists q \in ℕ e = \frac{p}{q}$
9		elq	$⊢ e \in ℚ \leftrightarrow \exists p \in ℤ \exists q \in ℕ e = \frac{p}{q}$
10	8 9	mtbir	$⊢ \neg e \in ℚ$
11	10	nelir	$⊢ e \notin ℚ$

Metamath Proof Explorer