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