egt2lt3

Description: Euler's constant _e = 2.71828... is strictly bounded below by 2 and above by 3. (Contributed by NM, 28-Nov-2008) (Revised by Mario Carneiro, 29-Apr-2014)

		Ref	Expression
	Assertion	egt2lt3	$⊢ (2 < e \land e < 3)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ (n \in ℕ ⟼ 2 {(\frac{1}{2})}^{n}) = (n \in ℕ ⟼ 2 {(\frac{1}{2})}^{n})$
2		eqid	$⊢ (n \in ℕ_{0} ⟼ \frac{1}{n!}) = (n \in ℕ_{0} ⟼ \frac{1}{n!})$
3	1 2	ege2le3	$⊢ (2 \leq e \land e \leq 3)$
4	3	simpli	$⊢ 2 \leq e$
5		eirr	$⊢ e \notin ℚ$
6	5	neli	$⊢ \neg e \in ℚ$
7		nnq	$⊢ e \in ℕ \to e \in ℚ$
8	6 7	mto	$⊢ \neg e \in ℕ$
9		2nn	$⊢ 2 \in ℕ$
10		eleq1	$⊢ e = 2 \to (e \in ℕ \leftrightarrow 2 \in ℕ)$
11	9 10	mpbiri	$⊢ e = 2 \to e \in ℕ$
12	11	necon3bi	$⊢ \neg e \in ℕ \to e \neq 2$
13	8 12	ax-mp	$⊢ e \neq 2$
14		2re	$⊢ 2 \in ℝ$
15		ere	$⊢ e \in ℝ$
16	14 15	ltleni	$⊢ 2 < e \leftrightarrow (2 \leq e \land e \neq 2)$
17	4 13 16	mpbir2an	$⊢ 2 < e$
18	3	simpri	$⊢ e \leq 3$
19		3nn	$⊢ 3 \in ℕ$
20		eleq1	$⊢ 3 = e \to (3 \in ℕ \leftrightarrow e \in ℕ)$
21	19 20	mpbii	$⊢ 3 = e \to e \in ℕ$
22	21	necon3bi	$⊢ \neg e \in ℕ \to 3 \neq e$
23	8 22	ax-mp	$⊢ 3 \neq e$
24		3re	$⊢ 3 \in ℝ$
25	15 24	ltleni	$⊢ e < 3 \leftrightarrow (e \leq 3 \land 3 \neq e)$
26	18 23 25	mpbir2an	$⊢ e < 3$
27	17 26	pm3.2i	$⊢ (2 < e \land e < 3)$

Metamath Proof Explorer

Theorem egt2lt3

Proof