ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ege2le3 GIF version

Theorem ege2le3 11681
Description: Euler's constant e = 2.71828... is bounded by 2 and 3. (Contributed by NM, 20-Mar-2005.) (Proof shortened by Mario Carneiro, 28-Apr-2014.)
Hypotheses
Ref Expression
erelem1.1 𝐹 = (𝑛 ∈ ℕ ↦ (2 · ((1 / 2)↑𝑛)))
erelem1.2 𝐺 = (𝑛 ∈ ℕ0 ↦ (1 / (!‘𝑛)))
Assertion
Ref Expression
ege2le3 (2 ≤ e ∧ e ≤ 3)

Proof of Theorem ege2le3
Dummy variables 𝑘 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 0nn0 9193 . . . . . . . . 9 0 ∈ ℕ0
2 nn0uz 9564 . . . . . . . . 9 0 = (ℤ‘0)
31, 2eleqtri 2252 . . . . . . . 8 0 ∈ (ℤ‘0)
43a1i 9 . . . . . . 7 (⊤ → 0 ∈ (ℤ‘0))
5 elnn0uz 9567 . . . . . . . . . 10 (𝑘 ∈ ℕ0𝑘 ∈ (ℤ‘0))
65biimpri 133 . . . . . . . . 9 (𝑘 ∈ (ℤ‘0) → 𝑘 ∈ ℕ0)
7 faccl 10717 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (!‘𝑘) ∈ ℕ)
87nnrecred 8968 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (1 / (!‘𝑘)) ∈ ℝ)
9 fveq2 5517 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (!‘𝑛) = (!‘𝑘))
109oveq2d 5893 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (1 / (!‘𝑛)) = (1 / (!‘𝑘)))
11 erelem1.2 . . . . . . . . . . . 12 𝐺 = (𝑛 ∈ ℕ0 ↦ (1 / (!‘𝑛)))
1210, 11fvmptg 5594 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0 ∧ (1 / (!‘𝑘)) ∈ ℝ) → (𝐺𝑘) = (1 / (!‘𝑘)))
138, 12mpdan 421 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → (𝐺𝑘) = (1 / (!‘𝑘)))
1413, 8eqeltrd 2254 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (𝐺𝑘) ∈ ℝ)
156, 14syl 14 . . . . . . . 8 (𝑘 ∈ (ℤ‘0) → (𝐺𝑘) ∈ ℝ)
1615adantl 277 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ (ℤ‘0)) → (𝐺𝑘) ∈ ℝ)
17 readdcl 7939 . . . . . . . 8 ((𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑘 + 𝑦) ∈ ℝ)
1817adantl 277 . . . . . . 7 ((⊤ ∧ (𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑘 + 𝑦) ∈ ℝ)
194, 16, 18seq3p1 10464 . . . . . 6 (⊤ → (seq0( + , 𝐺)‘(0 + 1)) = ((seq0( + , 𝐺)‘0) + (𝐺‘(0 + 1))))
20 0zd 9267 . . . . . . . . 9 (⊤ → 0 ∈ ℤ)
2120, 16, 18seq3-1 10462 . . . . . . . 8 (⊤ → (seq0( + , 𝐺)‘0) = (𝐺‘0))
22 fveq2 5517 . . . . . . . . . . . . 13 (𝑛 = 0 → (!‘𝑛) = (!‘0))
23 fac0 10710 . . . . . . . . . . . . 13 (!‘0) = 1
2422, 23eqtrdi 2226 . . . . . . . . . . . 12 (𝑛 = 0 → (!‘𝑛) = 1)
2524oveq2d 5893 . . . . . . . . . . 11 (𝑛 = 0 → (1 / (!‘𝑛)) = (1 / 1))
26 ax-1cn 7906 . . . . . . . . . . . 12 1 ∈ ℂ
2726div1i 8699 . . . . . . . . . . 11 (1 / 1) = 1
2825, 27eqtrdi 2226 . . . . . . . . . 10 (𝑛 = 0 → (1 / (!‘𝑛)) = 1)
29 1ex 7954 . . . . . . . . . 10 1 ∈ V
3028, 11, 29fvmpt 5595 . . . . . . . . 9 (0 ∈ ℕ0 → (𝐺‘0) = 1)
311, 30mp1i 10 . . . . . . . 8 (⊤ → (𝐺‘0) = 1)
3221, 31eqtrd 2210 . . . . . . 7 (⊤ → (seq0( + , 𝐺)‘0) = 1)
33 1e0p1 9427 . . . . . . . . 9 1 = (0 + 1)
3433fveq2i 5520 . . . . . . . 8 (𝐺‘1) = (𝐺‘(0 + 1))
35 1nn0 9194 . . . . . . . . 9 1 ∈ ℕ0
36 fveq2 5517 . . . . . . . . . . . . 13 (𝑛 = 1 → (!‘𝑛) = (!‘1))
37 fac1 10711 . . . . . . . . . . . . 13 (!‘1) = 1
3836, 37eqtrdi 2226 . . . . . . . . . . . 12 (𝑛 = 1 → (!‘𝑛) = 1)
3938oveq2d 5893 . . . . . . . . . . 11 (𝑛 = 1 → (1 / (!‘𝑛)) = (1 / 1))
4039, 27eqtrdi 2226 . . . . . . . . . 10 (𝑛 = 1 → (1 / (!‘𝑛)) = 1)
4140, 11, 29fvmpt 5595 . . . . . . . . 9 (1 ∈ ℕ0 → (𝐺‘1) = 1)
4235, 41mp1i 10 . . . . . . . 8 (⊤ → (𝐺‘1) = 1)
4334, 42eqtr3id 2224 . . . . . . 7 (⊤ → (𝐺‘(0 + 1)) = 1)
4432, 43oveq12d 5895 . . . . . 6 (⊤ → ((seq0( + , 𝐺)‘0) + (𝐺‘(0 + 1))) = (1 + 1))
4519, 44eqtrd 2210 . . . . 5 (⊤ → (seq0( + , 𝐺)‘(0 + 1)) = (1 + 1))
4633fveq2i 5520 . . . . 5 (seq0( + , 𝐺)‘1) = (seq0( + , 𝐺)‘(0 + 1))
47 df-2 8980 . . . . 5 2 = (1 + 1)
4845, 46, 473eqtr4g 2235 . . . 4 (⊤ → (seq0( + , 𝐺)‘1) = 2)
4935a1i 9 . . . . 5 (⊤ → 1 ∈ ℕ0)
50 nn0z 9275 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0𝑛 ∈ ℤ)
51 1exp 10551 . . . . . . . . . . . 12 (𝑛 ∈ ℤ → (1↑𝑛) = 1)
5250, 51syl 14 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 → (1↑𝑛) = 1)
5352oveq1d 5892 . . . . . . . . . 10 (𝑛 ∈ ℕ0 → ((1↑𝑛) / (!‘𝑛)) = (1 / (!‘𝑛)))
5453mpteq2ia 4091 . . . . . . . . 9 (𝑛 ∈ ℕ0 ↦ ((1↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (1 / (!‘𝑛)))
5511, 54eqtr4i 2201 . . . . . . . 8 𝐺 = (𝑛 ∈ ℕ0 ↦ ((1↑𝑛) / (!‘𝑛)))
5655efcvg 11676 . . . . . . 7 (1 ∈ ℂ → seq0( + , 𝐺) ⇝ (exp‘1))
5726, 56mp1i 10 . . . . . 6 (⊤ → seq0( + , 𝐺) ⇝ (exp‘1))
58 df-e 11659 . . . . . 6 e = (exp‘1)
5957, 58breqtrrdi 4047 . . . . 5 (⊤ → seq0( + , 𝐺) ⇝ e)
6013adantl 277 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) = (1 / (!‘𝑘)))
617adantl 277 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℕ)
6261nnrecred 8968 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / (!‘𝑘)) ∈ ℝ)
6360, 62eqeltrd 2254 . . . . 5 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℝ)
6461nnred 8934 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℝ)
6561nngt0d 8965 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ0) → 0 < (!‘𝑘))
66 1re 7958 . . . . . . . 8 1 ∈ ℝ
67 0le1 8440 . . . . . . . 8 0 ≤ 1
68 divge0 8832 . . . . . . . 8 (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ ((!‘𝑘) ∈ ℝ ∧ 0 < (!‘𝑘))) → 0 ≤ (1 / (!‘𝑘)))
6966, 67, 68mpanl12 436 . . . . . . 7 (((!‘𝑘) ∈ ℝ ∧ 0 < (!‘𝑘)) → 0 ≤ (1 / (!‘𝑘)))
7064, 65, 69syl2anc 411 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ0) → 0 ≤ (1 / (!‘𝑘)))
7170, 60breqtrrd 4033 . . . . 5 ((⊤ ∧ 𝑘 ∈ ℕ0) → 0 ≤ (𝐺𝑘))
722, 49, 59, 63, 71climserle 11355 . . . 4 (⊤ → (seq0( + , 𝐺)‘1) ≤ e)
7348, 72eqbrtrrd 4029 . . 3 (⊤ → 2 ≤ e)
7473mptru 1362 . 2 2 ≤ e
75 nnuz 9565 . . . . . 6 ℕ = (ℤ‘1)
76 1zzd 9282 . . . . . 6 (⊤ → 1 ∈ ℤ)
771a1i 9 . . . . . . . 8 (⊤ → 0 ∈ ℕ0)
7863recnd 7988 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℂ)
792, 77, 78, 59clim2ser 11347 . . . . . . 7 (⊤ → seq(0 + 1)( + , 𝐺) ⇝ (e − (seq0( + , 𝐺)‘0)))
80 0p1e1 9035 . . . . . . . 8 (0 + 1) = 1
81 seqeq1 10450 . . . . . . . 8 ((0 + 1) = 1 → seq(0 + 1)( + , 𝐺) = seq1( + , 𝐺))
8280, 81ax-mp 5 . . . . . . 7 seq(0 + 1)( + , 𝐺) = seq1( + , 𝐺)
8332mptru 1362 . . . . . . . 8 (seq0( + , 𝐺)‘0) = 1
8483oveq2i 5888 . . . . . . 7 (e − (seq0( + , 𝐺)‘0)) = (e − 1)
8579, 82, 843brtr3g 4038 . . . . . 6 (⊤ → seq1( + , 𝐺) ⇝ (e − 1))
86 2cnd 8994 . . . . . . . 8 (⊤ → 2 ∈ ℂ)
87 halfre 9134 . . . . . . . . . . . . . . 15 (1 / 2) ∈ ℝ
8887a1i 9 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → (1 / 2) ∈ ℝ)
89 id 19 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0𝑘 ∈ ℕ0)
9088, 89reexpcld 10673 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 → ((1 / 2)↑𝑘) ∈ ℝ)
91 oveq2 5885 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 → ((1 / 2)↑𝑛) = ((1 / 2)↑𝑘))
92 eqid 2177 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)) = (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))
9391, 92fvmptg 5594 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0 ∧ ((1 / 2)↑𝑘) ∈ ℝ) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
9490, 93mpdan 421 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
9594adantl 277 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
96 simpr 110 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
97 reexpcl 10539 . . . . . . . . . . . . 13 (((1 / 2) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) ∈ ℝ)
9887, 96, 97sylancr 414 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) ∈ ℝ)
9998recnd 7988 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) ∈ ℂ)
10095, 99eqeltrd 2254 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) ∈ ℂ)
101 1lt2 9090 . . . . . . . . . . . . . 14 1 < 2
102 2re 8991 . . . . . . . . . . . . . . 15 2 ∈ ℝ
103 0le2 9011 . . . . . . . . . . . . . . 15 0 ≤ 2
104 absid 11082 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ ∧ 0 ≤ 2) → (abs‘2) = 2)
105102, 103, 104mp2an 426 . . . . . . . . . . . . . 14 (abs‘2) = 2
106101, 105breqtrri 4032 . . . . . . . . . . . . 13 1 < (abs‘2)
107106a1i 9 . . . . . . . . . . . 12 (⊤ → 1 < (abs‘2))
10886, 107, 95georeclim 11523 . . . . . . . . . . 11 (⊤ → seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ (2 / (2 − 1)))
109 2m1e1 9039 . . . . . . . . . . . . 13 (2 − 1) = 1
110109oveq2i 5888 . . . . . . . . . . . 12 (2 / (2 − 1)) = (2 / 1)
111 2cn 8992 . . . . . . . . . . . . 13 2 ∈ ℂ
112111div1i 8699 . . . . . . . . . . . 12 (2 / 1) = 2
113110, 112eqtri 2198 . . . . . . . . . . 11 (2 / (2 − 1)) = 2
114108, 113breqtrdi 4046 . . . . . . . . . 10 (⊤ → seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ 2)
1152, 77, 100, 114clim2ser 11347 . . . . . . . . 9 (⊤ → seq(0 + 1)( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ (2 − (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0)))
116 seqeq1 10450 . . . . . . . . . 10 ((0 + 1) = 1 → seq(0 + 1)( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) = seq1( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))))
11780, 116ax-mp 5 . . . . . . . . 9 seq(0 + 1)( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) = seq1( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))
1186adantl 277 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑘 ∈ (ℤ‘0)) → 𝑘 ∈ ℕ0)
11994, 90eqeltrd 2254 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) ∈ ℝ)
120118, 119syl 14 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑘 ∈ (ℤ‘0)) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) ∈ ℝ)
12120, 120, 18seq3-1 10462 . . . . . . . . . . . . 13 (⊤ → (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0) = ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0))
122 halfcn 9135 . . . . . . . . . . . . . . . . 17 (1 / 2) ∈ ℂ
123 exp0 10526 . . . . . . . . . . . . . . . . 17 ((1 / 2) ∈ ℂ → ((1 / 2)↑0) = 1)
124122, 123ax-mp 5 . . . . . . . . . . . . . . . 16 ((1 / 2)↑0) = 1
125124, 35eqeltri 2250 . . . . . . . . . . . . . . 15 ((1 / 2)↑0) ∈ ℕ0
126 oveq2 5885 . . . . . . . . . . . . . . . 16 (𝑛 = 0 → ((1 / 2)↑𝑛) = ((1 / 2)↑0))
127126, 92fvmptg 5594 . . . . . . . . . . . . . . 15 ((0 ∈ ℕ0 ∧ ((1 / 2)↑0) ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0) = ((1 / 2)↑0))
1281, 125, 127mp2an 426 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0) = ((1 / 2)↑0)
129128, 124eqtri 2198 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0) = 1
130121, 129eqtrdi 2226 . . . . . . . . . . . 12 (⊤ → (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0) = 1)
131130mptru 1362 . . . . . . . . . . 11 (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0) = 1
132131oveq2i 5888 . . . . . . . . . 10 (2 − (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0)) = (2 − 1)
133132, 109eqtri 2198 . . . . . . . . 9 (2 − (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0)) = 1
134115, 117, 1333brtr3g 4038 . . . . . . . 8 (⊤ → seq1( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ 1)
135 nnnn0 9185 . . . . . . . . 9 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
136135, 100sylan2 286 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) ∈ ℂ)
137102a1i 9 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 2 ∈ ℝ)
138135, 90syl 14 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → ((1 / 2)↑𝑘) ∈ ℝ)
139137, 138remulcld 7990 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
14091oveq2d 5893 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (2 · ((1 / 2)↑𝑛)) = (2 · ((1 / 2)↑𝑘)))
141 erelem1.1 . . . . . . . . . . . 12 𝐹 = (𝑛 ∈ ℕ ↦ (2 · ((1 / 2)↑𝑛)))
142140, 141fvmptg 5594 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ (2 · ((1 / 2)↑𝑘)) ∈ ℝ) → (𝐹𝑘) = (2 · ((1 / 2)↑𝑘)))
143139, 142mpdan 421 . . . . . . . . . 10 (𝑘 ∈ ℕ → (𝐹𝑘) = (2 · ((1 / 2)↑𝑘)))
144143adantl 277 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) = (2 · ((1 / 2)↑𝑘)))
145135, 95sylan2 286 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
146145oveq2d 5893 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ) → (2 · ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘)) = (2 · ((1 / 2)↑𝑘)))
147144, 146eqtr4d 2213 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) = (2 · ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘)))
14875, 76, 86, 134, 136, 147isermulc2 11350 . . . . . . 7 (⊤ → seq1( + , 𝐹) ⇝ (2 · 1))
149 2t1e2 9074 . . . . . . 7 (2 · 1) = 2
150148, 149breqtrdi 4046 . . . . . 6 (⊤ → seq1( + , 𝐹) ⇝ 2)
151135, 63sylan2 286 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)
152 remulcl 7941 . . . . . . . . 9 ((2 ∈ ℝ ∧ ((1 / 2)↑𝑘) ∈ ℝ) → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
153102, 98, 152sylancr 414 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
154135, 153sylan2 286 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
155144, 154eqeltrd 2254 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℝ)
156 faclbnd2 10724 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → ((2↑𝑘) / 2) ≤ (!‘𝑘))
157156adantl 277 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((2↑𝑘) / 2) ≤ (!‘𝑘))
158 2nn 9082 . . . . . . . . . . . . . 14 2 ∈ ℕ
159 nnexpcl 10535 . . . . . . . . . . . . . 14 ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
160158, 96, 159sylancr 414 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
161160nnrpd 9696 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℝ+)
162161rphalfcld 9711 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((2↑𝑘) / 2) ∈ ℝ+)
16361nnrpd 9696 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℝ+)
164162, 163lerecd 9718 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (((2↑𝑘) / 2) ≤ (!‘𝑘) ↔ (1 / (!‘𝑘)) ≤ (1 / ((2↑𝑘) / 2))))
165157, 164mpbid 147 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / (!‘𝑘)) ≤ (1 / ((2↑𝑘) / 2)))
166 2cnd 8994 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → 2 ∈ ℂ)
167160nncnd 8935 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℂ)
168160nnap0d 8967 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) # 0)
169166, 167, 168divrecapd 8752 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 / (2↑𝑘)) = (2 · (1 / (2↑𝑘))))
170 2ap0 9014 . . . . . . . . . . . 12 2 # 0
171170a1i 9 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → 2 # 0)
172167, 166, 168, 171recdivapd 8766 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / ((2↑𝑘) / 2)) = (2 / (2↑𝑘)))
173 nn0z 9275 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℤ)
174173adantl 277 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℤ)
175166, 171, 174exprecapd 10664 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) = (1 / (2↑𝑘)))
176175oveq2d 5893 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · ((1 / 2)↑𝑘)) = (2 · (1 / (2↑𝑘))))
177169, 172, 1763eqtr4rd 2221 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · ((1 / 2)↑𝑘)) = (1 / ((2↑𝑘) / 2)))
178165, 177breqtrrd 4033 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / (!‘𝑘)) ≤ (2 · ((1 / 2)↑𝑘)))
179135, 178sylan2 286 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (1 / (!‘𝑘)) ≤ (2 · ((1 / 2)↑𝑘)))
180135, 60sylan2 286 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) = (1 / (!‘𝑘)))
181179, 180, 1443brtr4d 4037 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ≤ (𝐹𝑘))
18275, 76, 85, 150, 151, 155, 181iserle 11352 . . . . 5 (⊤ → (e − 1) ≤ 2)
183182mptru 1362 . . . 4 (e − 1) ≤ 2
184 ere 11680 . . . . 5 e ∈ ℝ
185184, 66, 102lesubaddi 8465 . . . 4 ((e − 1) ≤ 2 ↔ e ≤ (2 + 1))
186183, 185mpbi 145 . . 3 e ≤ (2 + 1)
187 df-3 8981 . . 3 3 = (2 + 1)
188186, 187breqtrri 4032 . 2 e ≤ 3
18974, 188pm3.2i 272 1 (2 ≤ e ∧ e ≤ 3)
Colors of variables: wff set class
Syntax hints:  wa 104   = wceq 1353  wtru 1354  wcel 2148   class class class wbr 4005  cmpt 4066  cfv 5218  (class class class)co 5877  cc 7811  cr 7812  0cc0 7813  1c1 7814   + caddc 7816   · cmul 7818   < clt 7994  cle 7995  cmin 8130   # cap 8540   / cdiv 8631  cn 8921  2c2 8972  3c3 8973  0cn0 9178  cz 9255  cuz 9530  seqcseq 10447  cexp 10521  !cfa 10707  abscabs 11008  cli 11288  expce 11652  eceu 11653
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4120  ax-sep 4123  ax-nul 4131  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-iinf 4589  ax-cnex 7904  ax-resscn 7905  ax-1cn 7906  ax-1re 7907  ax-icn 7908  ax-addcl 7909  ax-addrcl 7910  ax-mulcl 7911  ax-mulrcl 7912  ax-addcom 7913  ax-mulcom 7914  ax-addass 7915  ax-mulass 7916  ax-distr 7917  ax-i2m1 7918  ax-0lt1 7919  ax-1rid 7920  ax-0id 7921  ax-rnegex 7922  ax-precex 7923  ax-cnre 7924  ax-pre-ltirr 7925  ax-pre-ltwlin 7926  ax-pre-lttrn 7927  ax-pre-apti 7928  ax-pre-ltadd 7929  ax-pre-mulgt0 7930  ax-pre-mulext 7931  ax-arch 7932  ax-caucvg 7933
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rmo 2463  df-rab 2464  df-v 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-nul 3425  df-if 3537  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-tr 4104  df-id 4295  df-po 4298  df-iso 4299  df-iord 4368  df-on 4370  df-ilim 4371  df-suc 4373  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-isom 5227  df-riota 5833  df-ov 5880  df-oprab 5881  df-mpo 5882  df-1st 6143  df-2nd 6144  df-recs 6308  df-irdg 6373  df-frec 6394  df-1o 6419  df-oadd 6423  df-er 6537  df-en 6743  df-dom 6744  df-fin 6745  df-pnf 7996  df-mnf 7997  df-xr 7998  df-ltxr 7999  df-le 8000  df-sub 8132  df-neg 8133  df-reap 8534  df-ap 8541  df-div 8632  df-inn 8922  df-2 8980  df-3 8981  df-4 8982  df-n0 9179  df-z 9256  df-uz 9531  df-q 9622  df-rp 9656  df-ico 9896  df-fz 10011  df-fzo 10145  df-seqfrec 10448  df-exp 10522  df-fac 10708  df-ihash 10758  df-cj 10853  df-re 10854  df-im 10855  df-rsqrt 11009  df-abs 11010  df-clim 11289  df-sumdc 11364  df-ef 11658  df-e 11659
This theorem is referenced by:  egt2lt3  11789
  Copyright terms: Public domain W3C validator