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

Theorem ege2le3 11287
 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 8946 . . . . . . . . 9 0 ∈ ℕ0
2 nn0uz 9312 . . . . . . . . 9 0 = (ℤ‘0)
31, 2eleqtri 2190 . . . . . . . 8 0 ∈ (ℤ‘0)
43a1i 9 . . . . . . 7 (⊤ → 0 ∈ (ℤ‘0))
5 elnn0uz 9315 . . . . . . . . . 10 (𝑘 ∈ ℕ0𝑘 ∈ (ℤ‘0))
65biimpri 132 . . . . . . . . 9 (𝑘 ∈ (ℤ‘0) → 𝑘 ∈ ℕ0)
7 faccl 10432 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (!‘𝑘) ∈ ℕ)
87nnrecred 8727 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (1 / (!‘𝑘)) ∈ ℝ)
9 fveq2 5387 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (!‘𝑛) = (!‘𝑘))
109oveq2d 5756 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (1 / (!‘𝑛)) = (1 / (!‘𝑘)))
11 erelem1.2 . . . . . . . . . . . 12 𝐺 = (𝑛 ∈ ℕ0 ↦ (1 / (!‘𝑛)))
1210, 11fvmptg 5463 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0 ∧ (1 / (!‘𝑘)) ∈ ℝ) → (𝐺𝑘) = (1 / (!‘𝑘)))
138, 12mpdan 415 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → (𝐺𝑘) = (1 / (!‘𝑘)))
1413, 8eqeltrd 2192 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (𝐺𝑘) ∈ ℝ)
156, 14syl 14 . . . . . . . 8 (𝑘 ∈ (ℤ‘0) → (𝐺𝑘) ∈ ℝ)
1615adantl 273 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ (ℤ‘0)) → (𝐺𝑘) ∈ ℝ)
17 readdcl 7710 . . . . . . . 8 ((𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑘 + 𝑦) ∈ ℝ)
1817adantl 273 . . . . . . 7 ((⊤ ∧ (𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑘 + 𝑦) ∈ ℝ)
194, 16, 18seq3p1 10186 . . . . . 6 (⊤ → (seq0( + , 𝐺)‘(0 + 1)) = ((seq0( + , 𝐺)‘0) + (𝐺‘(0 + 1))))
20 0zd 9020 . . . . . . . . 9 (⊤ → 0 ∈ ℤ)
2120, 16, 18seq3-1 10184 . . . . . . . 8 (⊤ → (seq0( + , 𝐺)‘0) = (𝐺‘0))
22 fveq2 5387 . . . . . . . . . . . . 13 (𝑛 = 0 → (!‘𝑛) = (!‘0))
23 fac0 10425 . . . . . . . . . . . . 13 (!‘0) = 1
2422, 23syl6eq 2164 . . . . . . . . . . . 12 (𝑛 = 0 → (!‘𝑛) = 1)
2524oveq2d 5756 . . . . . . . . . . 11 (𝑛 = 0 → (1 / (!‘𝑛)) = (1 / 1))
26 ax-1cn 7677 . . . . . . . . . . . 12 1 ∈ ℂ
2726div1i 8463 . . . . . . . . . . 11 (1 / 1) = 1
2825, 27syl6eq 2164 . . . . . . . . . 10 (𝑛 = 0 → (1 / (!‘𝑛)) = 1)
29 1ex 7725 . . . . . . . . . 10 1 ∈ V
3028, 11, 29fvmpt 5464 . . . . . . . . 9 (0 ∈ ℕ0 → (𝐺‘0) = 1)
311, 30mp1i 10 . . . . . . . 8 (⊤ → (𝐺‘0) = 1)
3221, 31eqtrd 2148 . . . . . . 7 (⊤ → (seq0( + , 𝐺)‘0) = 1)
33 1e0p1 9177 . . . . . . . . 9 1 = (0 + 1)
3433fveq2i 5390 . . . . . . . 8 (𝐺‘1) = (𝐺‘(0 + 1))
35 1nn0 8947 . . . . . . . . 9 1 ∈ ℕ0
36 fveq2 5387 . . . . . . . . . . . . 13 (𝑛 = 1 → (!‘𝑛) = (!‘1))
37 fac1 10426 . . . . . . . . . . . . 13 (!‘1) = 1
3836, 37syl6eq 2164 . . . . . . . . . . . 12 (𝑛 = 1 → (!‘𝑛) = 1)
3938oveq2d 5756 . . . . . . . . . . 11 (𝑛 = 1 → (1 / (!‘𝑛)) = (1 / 1))
4039, 27syl6eq 2164 . . . . . . . . . 10 (𝑛 = 1 → (1 / (!‘𝑛)) = 1)
4140, 11, 29fvmpt 5464 . . . . . . . . 9 (1 ∈ ℕ0 → (𝐺‘1) = 1)
4235, 41mp1i 10 . . . . . . . 8 (⊤ → (𝐺‘1) = 1)
4334, 42syl5eqr 2162 . . . . . . 7 (⊤ → (𝐺‘(0 + 1)) = 1)
4432, 43oveq12d 5758 . . . . . 6 (⊤ → ((seq0( + , 𝐺)‘0) + (𝐺‘(0 + 1))) = (1 + 1))
4519, 44eqtrd 2148 . . . . 5 (⊤ → (seq0( + , 𝐺)‘(0 + 1)) = (1 + 1))
4633fveq2i 5390 . . . . 5 (seq0( + , 𝐺)‘1) = (seq0( + , 𝐺)‘(0 + 1))
47 df-2 8739 . . . . 5 2 = (1 + 1)
4845, 46, 473eqtr4g 2173 . . . 4 (⊤ → (seq0( + , 𝐺)‘1) = 2)
4935a1i 9 . . . . 5 (⊤ → 1 ∈ ℕ0)
50 nn0z 9028 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0𝑛 ∈ ℤ)
51 1exp 10273 . . . . . . . . . . . 12 (𝑛 ∈ ℤ → (1↑𝑛) = 1)
5250, 51syl 14 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 → (1↑𝑛) = 1)
5352oveq1d 5755 . . . . . . . . . 10 (𝑛 ∈ ℕ0 → ((1↑𝑛) / (!‘𝑛)) = (1 / (!‘𝑛)))
5453mpteq2ia 3982 . . . . . . . . 9 (𝑛 ∈ ℕ0 ↦ ((1↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (1 / (!‘𝑛)))
5511, 54eqtr4i 2139 . . . . . . . 8 𝐺 = (𝑛 ∈ ℕ0 ↦ ((1↑𝑛) / (!‘𝑛)))
5655efcvg 11282 . . . . . . 7 (1 ∈ ℂ → seq0( + , 𝐺) ⇝ (exp‘1))
5726, 56mp1i 10 . . . . . 6 (⊤ → seq0( + , 𝐺) ⇝ (exp‘1))
58 df-e 11265 . . . . . 6 e = (exp‘1)
5957, 58breqtrrdi 3938 . . . . 5 (⊤ → seq0( + , 𝐺) ⇝ e)
6013adantl 273 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) = (1 / (!‘𝑘)))
617adantl 273 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℕ)
6261nnrecred 8727 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / (!‘𝑘)) ∈ ℝ)
6360, 62eqeltrd 2192 . . . . 5 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℝ)
6461nnred 8693 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℝ)
6561nngt0d 8724 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ0) → 0 < (!‘𝑘))
66 1re 7729 . . . . . . . 8 1 ∈ ℝ
67 0le1 8207 . . . . . . . 8 0 ≤ 1
68 divge0 8591 . . . . . . . 8 (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ ((!‘𝑘) ∈ ℝ ∧ 0 < (!‘𝑘))) → 0 ≤ (1 / (!‘𝑘)))
6966, 67, 68mpanl12 430 . . . . . . 7 (((!‘𝑘) ∈ ℝ ∧ 0 < (!‘𝑘)) → 0 ≤ (1 / (!‘𝑘)))
7064, 65, 69syl2anc 406 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ0) → 0 ≤ (1 / (!‘𝑘)))
7170, 60breqtrrd 3924 . . . . 5 ((⊤ ∧ 𝑘 ∈ ℕ0) → 0 ≤ (𝐺𝑘))
722, 49, 59, 63, 71climserle 11065 . . . 4 (⊤ → (seq0( + , 𝐺)‘1) ≤ e)
7348, 72eqbrtrrd 3920 . . 3 (⊤ → 2 ≤ e)
7473mptru 1323 . 2 2 ≤ e
75 nnuz 9313 . . . . . 6 ℕ = (ℤ‘1)
76 1zzd 9035 . . . . . 6 (⊤ → 1 ∈ ℤ)
771a1i 9 . . . . . . . 8 (⊤ → 0 ∈ ℕ0)
7863recnd 7758 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℂ)
792, 77, 78, 59clim2ser 11057 . . . . . . 7 (⊤ → seq(0 + 1)( + , 𝐺) ⇝ (e − (seq0( + , 𝐺)‘0)))
80 0p1e1 8794 . . . . . . . 8 (0 + 1) = 1
81 seqeq1 10172 . . . . . . . 8 ((0 + 1) = 1 → seq(0 + 1)( + , 𝐺) = seq1( + , 𝐺))
8280, 81ax-mp 5 . . . . . . 7 seq(0 + 1)( + , 𝐺) = seq1( + , 𝐺)
8332mptru 1323 . . . . . . . 8 (seq0( + , 𝐺)‘0) = 1
8483oveq2i 5751 . . . . . . 7 (e − (seq0( + , 𝐺)‘0)) = (e − 1)
8579, 82, 843brtr3g 3929 . . . . . 6 (⊤ → seq1( + , 𝐺) ⇝ (e − 1))
86 2cnd 8753 . . . . . . . 8 (⊤ → 2 ∈ ℂ)
87 halfre 8887 . . . . . . . . . . . . . . 15 (1 / 2) ∈ ℝ
8887a1i 9 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → (1 / 2) ∈ ℝ)
89 id 19 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0𝑘 ∈ ℕ0)
9088, 89reexpcld 10392 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 → ((1 / 2)↑𝑘) ∈ ℝ)
91 oveq2 5748 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 → ((1 / 2)↑𝑛) = ((1 / 2)↑𝑘))
92 eqid 2115 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)) = (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))
9391, 92fvmptg 5463 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0 ∧ ((1 / 2)↑𝑘) ∈ ℝ) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
9490, 93mpdan 415 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
9594adantl 273 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
96 simpr 109 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
97 reexpcl 10261 . . . . . . . . . . . . 13 (((1 / 2) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) ∈ ℝ)
9887, 96, 97sylancr 408 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) ∈ ℝ)
9998recnd 7758 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) ∈ ℂ)
10095, 99eqeltrd 2192 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) ∈ ℂ)
101 1lt2 8843 . . . . . . . . . . . . . 14 1 < 2
102 2re 8750 . . . . . . . . . . . . . . 15 2 ∈ ℝ
103 0le2 8770 . . . . . . . . . . . . . . 15 0 ≤ 2
104 absid 10794 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ ∧ 0 ≤ 2) → (abs‘2) = 2)
105102, 103, 104mp2an 420 . . . . . . . . . . . . . 14 (abs‘2) = 2
106101, 105breqtrri 3923 . . . . . . . . . . . . 13 1 < (abs‘2)
107106a1i 9 . . . . . . . . . . . 12 (⊤ → 1 < (abs‘2))
10886, 107, 95georeclim 11233 . . . . . . . . . . 11 (⊤ → seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ (2 / (2 − 1)))
109 2m1e1 8798 . . . . . . . . . . . . 13 (2 − 1) = 1
110109oveq2i 5751 . . . . . . . . . . . 12 (2 / (2 − 1)) = (2 / 1)
111 2cn 8751 . . . . . . . . . . . . 13 2 ∈ ℂ
112111div1i 8463 . . . . . . . . . . . 12 (2 / 1) = 2
113110, 112eqtri 2136 . . . . . . . . . . 11 (2 / (2 − 1)) = 2
114108, 113breqtrdi 3937 . . . . . . . . . 10 (⊤ → seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ 2)
1152, 77, 100, 114clim2ser 11057 . . . . . . . . 9 (⊤ → seq(0 + 1)( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ (2 − (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0)))
116 seqeq1 10172 . . . . . . . . . 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 273 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑘 ∈ (ℤ‘0)) → 𝑘 ∈ ℕ0)
11994, 90eqeltrd 2192 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) ∈ ℝ)
120118, 119syl 14 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑘 ∈ (ℤ‘0)) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) ∈ ℝ)
12120, 120, 18seq3-1 10184 . . . . . . . . . . . . 13 (⊤ → (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0) = ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0))
122 halfcn 8888 . . . . . . . . . . . . . . . . 17 (1 / 2) ∈ ℂ
123 exp0 10248 . . . . . . . . . . . . . . . . 17 ((1 / 2) ∈ ℂ → ((1 / 2)↑0) = 1)
124122, 123ax-mp 5 . . . . . . . . . . . . . . . 16 ((1 / 2)↑0) = 1
125124, 35eqeltri 2188 . . . . . . . . . . . . . . 15 ((1 / 2)↑0) ∈ ℕ0
126 oveq2 5748 . . . . . . . . . . . . . . . 16 (𝑛 = 0 → ((1 / 2)↑𝑛) = ((1 / 2)↑0))
127126, 92fvmptg 5463 . . . . . . . . . . . . . . 15 ((0 ∈ ℕ0 ∧ ((1 / 2)↑0) ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0) = ((1 / 2)↑0))
1281, 125, 127mp2an 420 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0) = ((1 / 2)↑0)
129128, 124eqtri 2136 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0) = 1
130121, 129syl6eq 2164 . . . . . . . . . . . 12 (⊤ → (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0) = 1)
131130mptru 1323 . . . . . . . . . . 11 (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0) = 1
132131oveq2i 5751 . . . . . . . . . 10 (2 − (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0)) = (2 − 1)
133132, 109eqtri 2136 . . . . . . . . 9 (2 − (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0)) = 1
134115, 117, 1333brtr3g 3929 . . . . . . . 8 (⊤ → seq1( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ 1)
135 nnnn0 8938 . . . . . . . . 9 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
136135, 100sylan2 282 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) ∈ ℂ)
137102a1i 9 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 2 ∈ ℝ)
138135, 90syl 14 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → ((1 / 2)↑𝑘) ∈ ℝ)
139137, 138remulcld 7760 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
14091oveq2d 5756 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (2 · ((1 / 2)↑𝑛)) = (2 · ((1 / 2)↑𝑘)))
141 erelem1.1 . . . . . . . . . . . 12 𝐹 = (𝑛 ∈ ℕ ↦ (2 · ((1 / 2)↑𝑛)))
142140, 141fvmptg 5463 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ (2 · ((1 / 2)↑𝑘)) ∈ ℝ) → (𝐹𝑘) = (2 · ((1 / 2)↑𝑘)))
143139, 142mpdan 415 . . . . . . . . . 10 (𝑘 ∈ ℕ → (𝐹𝑘) = (2 · ((1 / 2)↑𝑘)))
144143adantl 273 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) = (2 · ((1 / 2)↑𝑘)))
145135, 95sylan2 282 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
146145oveq2d 5756 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ) → (2 · ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘)) = (2 · ((1 / 2)↑𝑘)))
147144, 146eqtr4d 2151 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) = (2 · ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘)))
14875, 76, 86, 134, 136, 147isermulc2 11060 . . . . . . 7 (⊤ → seq1( + , 𝐹) ⇝ (2 · 1))
149 2t1e2 8827 . . . . . . 7 (2 · 1) = 2
150148, 149breqtrdi 3937 . . . . . 6 (⊤ → seq1( + , 𝐹) ⇝ 2)
151135, 63sylan2 282 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)
152 remulcl 7712 . . . . . . . . 9 ((2 ∈ ℝ ∧ ((1 / 2)↑𝑘) ∈ ℝ) → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
153102, 98, 152sylancr 408 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
154135, 153sylan2 282 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
155144, 154eqeltrd 2192 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℝ)
156 faclbnd2 10439 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → ((2↑𝑘) / 2) ≤ (!‘𝑘))
157156adantl 273 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((2↑𝑘) / 2) ≤ (!‘𝑘))
158 2nn 8835 . . . . . . . . . . . . . 14 2 ∈ ℕ
159 nnexpcl 10257 . . . . . . . . . . . . . 14 ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
160158, 96, 159sylancr 408 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
161160nnrpd 9433 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℝ+)
162161rphalfcld 9447 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((2↑𝑘) / 2) ∈ ℝ+)
16361nnrpd 9433 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℝ+)
164162, 163lerecd 9454 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (((2↑𝑘) / 2) ≤ (!‘𝑘) ↔ (1 / (!‘𝑘)) ≤ (1 / ((2↑𝑘) / 2))))
165157, 164mpbid 146 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / (!‘𝑘)) ≤ (1 / ((2↑𝑘) / 2)))
166 2cnd 8753 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → 2 ∈ ℂ)
167160nncnd 8694 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℂ)
168160nnap0d 8726 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) # 0)
169166, 167, 168divrecapd 8516 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 / (2↑𝑘)) = (2 · (1 / (2↑𝑘))))
170 2ap0 8773 . . . . . . . . . . . 12 2 # 0
171170a1i 9 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → 2 # 0)
172167, 166, 168, 171recdivapd 8530 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / ((2↑𝑘) / 2)) = (2 / (2↑𝑘)))
173 nn0z 9028 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℤ)
174173adantl 273 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℤ)
175166, 171, 174exprecapd 10383 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) = (1 / (2↑𝑘)))
176175oveq2d 5756 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · ((1 / 2)↑𝑘)) = (2 · (1 / (2↑𝑘))))
177169, 172, 1763eqtr4rd 2159 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · ((1 / 2)↑𝑘)) = (1 / ((2↑𝑘) / 2)))
178165, 177breqtrrd 3924 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / (!‘𝑘)) ≤ (2 · ((1 / 2)↑𝑘)))
179135, 178sylan2 282 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (1 / (!‘𝑘)) ≤ (2 · ((1 / 2)↑𝑘)))
180135, 60sylan2 282 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) = (1 / (!‘𝑘)))
181179, 180, 1443brtr4d 3928 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ≤ (𝐹𝑘))
18275, 76, 85, 150, 151, 155, 181iserle 11062 . . . . 5 (⊤ → (e − 1) ≤ 2)
183182mptru 1323 . . . 4 (e − 1) ≤ 2
184 ere 11286 . . . . 5 e ∈ ℝ
185184, 66, 102lesubaddi 8232 . . . 4 ((e − 1) ≤ 2 ↔ e ≤ (2 + 1))
186183, 185mpbi 144 . . 3 e ≤ (2 + 1)
187 df-3 8740 . . 3 3 = (2 + 1)
188186, 187breqtrri 3923 . 2 e ≤ 3
18974, 188pm3.2i 268 1 (2 ≤ e ∧ e ≤ 3)
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   = wceq 1314  ⊤wtru 1315   ∈ wcel 1463   class class class wbr 3897   ↦ cmpt 3957  ‘cfv 5091  (class class class)co 5740  ℂcc 7582  ℝcr 7583  0cc0 7584  1c1 7585   + caddc 7587   · cmul 7589   < clt 7764   ≤ cle 7765   − cmin 7897   # cap 8306   / cdiv 8395  ℕcn 8680  2c2 8731  3c3 8732  ℕ0cn0 8931  ℤcz 9008  ℤ≥cuz 9278  seqcseq 10169  ↑cexp 10243  !cfa 10422  abscabs 10720   ⇝ cli 10998  expce 11258  eceu 11259 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-coll 4011  ax-sep 4014  ax-nul 4022  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-setind 4420  ax-iinf 4470  ax-cnex 7675  ax-resscn 7676  ax-1cn 7677  ax-1re 7678  ax-icn 7679  ax-addcl 7680  ax-addrcl 7681  ax-mulcl 7682  ax-mulrcl 7683  ax-addcom 7684  ax-mulcom 7685  ax-addass 7686  ax-mulass 7687  ax-distr 7688  ax-i2m1 7689  ax-0lt1 7690  ax-1rid 7691  ax-0id 7692  ax-rnegex 7693  ax-precex 7694  ax-cnre 7695  ax-pre-ltirr 7696  ax-pre-ltwlin 7697  ax-pre-lttrn 7698  ax-pre-apti 7699  ax-pre-ltadd 7700  ax-pre-mulgt0 7701  ax-pre-mulext 7702  ax-arch 7703  ax-caucvg 7704 This theorem depends on definitions:  df-bi 116  df-dc 803  df-3or 946  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-nel 2379  df-ral 2396  df-rex 2397  df-reu 2398  df-rmo 2399  df-rab 2400  df-v 2660  df-sbc 2881  df-csb 2974  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-if 3443  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-int 3740  df-iun 3783  df-br 3898  df-opab 3958  df-mpt 3959  df-tr 3995  df-id 4183  df-po 4186  df-iso 4187  df-iord 4256  df-on 4258  df-ilim 4259  df-suc 4261  df-iom 4473  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-ima 4520  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-f1 5096  df-fo 5097  df-f1o 5098  df-fv 5099  df-isom 5100  df-riota 5696  df-ov 5743  df-oprab 5744  df-mpo 5745  df-1st 6004  df-2nd 6005  df-recs 6168  df-irdg 6233  df-frec 6254  df-1o 6279  df-oadd 6283  df-er 6395  df-en 6601  df-dom 6602  df-fin 6603  df-pnf 7766  df-mnf 7767  df-xr 7768  df-ltxr 7769  df-le 7770  df-sub 7899  df-neg 7900  df-reap 8300  df-ap 8307  df-div 8396  df-inn 8681  df-2 8739  df-3 8740  df-4 8741  df-n0 8932  df-z 9009  df-uz 9279  df-q 9364  df-rp 9394  df-ico 9628  df-fz 9742  df-fzo 9871  df-seqfrec 10170  df-exp 10244  df-fac 10423  df-ihash 10473  df-cj 10565  df-re 10566  df-im 10567  df-rsqrt 10721  df-abs 10722  df-clim 10999  df-sumdc 11074  df-ef 11264  df-e 11265 This theorem is referenced by:  egt2lt3  11393
 Copyright terms: Public domain W3C validator