Metamath Proof Explorer


Theorem 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 ∧ 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 )