Theorem egt2lt3

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

	Ref	Expression
Assertion	egt2lt3	⊢ ( 2 < e ∧ e < 3 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑛 ∈ ℕ ↦ ( 2 · ( ( 1 / 2 ) ↑ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( 2 · ( ( 1 / 2 ) ↑ 𝑛 ) ) )
2		eqid	⊢ ( 𝑛 ∈ ℕ0 ↦ ( 1 / ( ! ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ0 ↦ ( 1 / ( ! ‘ 𝑛 ) ) )
3	1 2	ege2le3	⊢ ( 2 ≤ e ∧ e ≤ 3 )
4	3	simpli	⊢ 2 ≤ e
5		eirr	⊢ e ∉ ℚ
6	5	neli	⊢ ¬ e ∈ ℚ
7		nnq	⊢ ( e ∈ ℕ → e ∈ ℚ )
8	6 7	mto	⊢ ¬ e ∈ ℕ
9		2nn	⊢ 2 ∈ ℕ
10		eleq1	⊢ ( e = 2 → ( e ∈ ℕ ↔ 2 ∈ ℕ ) )
11	9 10	mpbiri	⊢ ( e = 2 → e ∈ ℕ )
12	11	necon3bi	⊢ ( ¬ e ∈ ℕ → e ≠ 2 )
13	8 12	ax-mp	⊢ e ≠ 2
14		2re	⊢ 2 ∈ ℝ
15		ere	⊢ e ∈ ℝ
16	14 15	ltleni	⊢ ( 2 < e ↔ ( 2 ≤ e ∧ e ≠ 2 ) )
17	4 13 16	mpbir2an	⊢ 2 < e
18	3	simpri	⊢ e ≤ 3
19		3nn	⊢ 3 ∈ ℕ
20		eleq1	⊢ ( 3 = e → ( 3 ∈ ℕ ↔ e ∈ ℕ ) )
21	19 20	mpbii	⊢ ( 3 = e → e ∈ ℕ )
22	21	necon3bi	⊢ ( ¬ e ∈ ℕ → 3 ≠ e )
23	8 22	ax-mp	⊢ 3 ≠ e
24		3re	⊢ 3 ∈ ℝ
25	15 24	ltleni	⊢ ( e < 3 ↔ ( e ≤ 3 ∧ 3 ≠ e ) )
26	18 23 25	mpbir2an	⊢ e < 3
27	17 26	pm3.2i	⊢ ( 2 < e ∧ e < 3 )