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

Theorem ege2le3 11572
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 9106 . . . . . . . . 9 0 ∈ ℕ0
2 nn0uz 9474 . . . . . . . . 9 0 = (ℤ‘0)
31, 2eleqtri 2232 . . . . . . . 8 0 ∈ (ℤ‘0)
43a1i 9 . . . . . . 7 (⊤ → 0 ∈ (ℤ‘0))
5 elnn0uz 9477 . . . . . . . . . 10 (𝑘 ∈ ℕ0𝑘 ∈ (ℤ‘0))
65biimpri 132 . . . . . . . . 9 (𝑘 ∈ (ℤ‘0) → 𝑘 ∈ ℕ0)
7 faccl 10613 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (!‘𝑘) ∈ ℕ)
87nnrecred 8881 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (1 / (!‘𝑘)) ∈ ℝ)
9 fveq2 5469 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (!‘𝑛) = (!‘𝑘))
109oveq2d 5841 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (1 / (!‘𝑛)) = (1 / (!‘𝑘)))
11 erelem1.2 . . . . . . . . . . . 12 𝐺 = (𝑛 ∈ ℕ0 ↦ (1 / (!‘𝑛)))
1210, 11fvmptg 5545 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0 ∧ (1 / (!‘𝑘)) ∈ ℝ) → (𝐺𝑘) = (1 / (!‘𝑘)))
138, 12mpdan 418 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → (𝐺𝑘) = (1 / (!‘𝑘)))
1413, 8eqeltrd 2234 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (𝐺𝑘) ∈ ℝ)
156, 14syl 14 . . . . . . . 8 (𝑘 ∈ (ℤ‘0) → (𝐺𝑘) ∈ ℝ)
1615adantl 275 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ (ℤ‘0)) → (𝐺𝑘) ∈ ℝ)
17 readdcl 7859 . . . . . . . 8 ((𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑘 + 𝑦) ∈ ℝ)
1817adantl 275 . . . . . . 7 ((⊤ ∧ (𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑘 + 𝑦) ∈ ℝ)
194, 16, 18seq3p1 10365 . . . . . 6 (⊤ → (seq0( + , 𝐺)‘(0 + 1)) = ((seq0( + , 𝐺)‘0) + (𝐺‘(0 + 1))))
20 0zd 9180 . . . . . . . . 9 (⊤ → 0 ∈ ℤ)
2120, 16, 18seq3-1 10363 . . . . . . . 8 (⊤ → (seq0( + , 𝐺)‘0) = (𝐺‘0))
22 fveq2 5469 . . . . . . . . . . . . 13 (𝑛 = 0 → (!‘𝑛) = (!‘0))
23 fac0 10606 . . . . . . . . . . . . 13 (!‘0) = 1
2422, 23eqtrdi 2206 . . . . . . . . . . . 12 (𝑛 = 0 → (!‘𝑛) = 1)
2524oveq2d 5841 . . . . . . . . . . 11 (𝑛 = 0 → (1 / (!‘𝑛)) = (1 / 1))
26 ax-1cn 7826 . . . . . . . . . . . 12 1 ∈ ℂ
2726div1i 8614 . . . . . . . . . . 11 (1 / 1) = 1
2825, 27eqtrdi 2206 . . . . . . . . . 10 (𝑛 = 0 → (1 / (!‘𝑛)) = 1)
29 1ex 7874 . . . . . . . . . 10 1 ∈ V
3028, 11, 29fvmpt 5546 . . . . . . . . 9 (0 ∈ ℕ0 → (𝐺‘0) = 1)
311, 30mp1i 10 . . . . . . . 8 (⊤ → (𝐺‘0) = 1)
3221, 31eqtrd 2190 . . . . . . 7 (⊤ → (seq0( + , 𝐺)‘0) = 1)
33 1e0p1 9337 . . . . . . . . 9 1 = (0 + 1)
3433fveq2i 5472 . . . . . . . 8 (𝐺‘1) = (𝐺‘(0 + 1))
35 1nn0 9107 . . . . . . . . 9 1 ∈ ℕ0
36 fveq2 5469 . . . . . . . . . . . . 13 (𝑛 = 1 → (!‘𝑛) = (!‘1))
37 fac1 10607 . . . . . . . . . . . . 13 (!‘1) = 1
3836, 37eqtrdi 2206 . . . . . . . . . . . 12 (𝑛 = 1 → (!‘𝑛) = 1)
3938oveq2d 5841 . . . . . . . . . . 11 (𝑛 = 1 → (1 / (!‘𝑛)) = (1 / 1))
4039, 27eqtrdi 2206 . . . . . . . . . 10 (𝑛 = 1 → (1 / (!‘𝑛)) = 1)
4140, 11, 29fvmpt 5546 . . . . . . . . 9 (1 ∈ ℕ0 → (𝐺‘1) = 1)
4235, 41mp1i 10 . . . . . . . 8 (⊤ → (𝐺‘1) = 1)
4334, 42eqtr3id 2204 . . . . . . 7 (⊤ → (𝐺‘(0 + 1)) = 1)
4432, 43oveq12d 5843 . . . . . 6 (⊤ → ((seq0( + , 𝐺)‘0) + (𝐺‘(0 + 1))) = (1 + 1))
4519, 44eqtrd 2190 . . . . 5 (⊤ → (seq0( + , 𝐺)‘(0 + 1)) = (1 + 1))
4633fveq2i 5472 . . . . 5 (seq0( + , 𝐺)‘1) = (seq0( + , 𝐺)‘(0 + 1))
47 df-2 8893 . . . . 5 2 = (1 + 1)
4845, 46, 473eqtr4g 2215 . . . 4 (⊤ → (seq0( + , 𝐺)‘1) = 2)
4935a1i 9 . . . . 5 (⊤ → 1 ∈ ℕ0)
50 nn0z 9188 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0𝑛 ∈ ℤ)
51 1exp 10452 . . . . . . . . . . . 12 (𝑛 ∈ ℤ → (1↑𝑛) = 1)
5250, 51syl 14 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 → (1↑𝑛) = 1)
5352oveq1d 5840 . . . . . . . . . 10 (𝑛 ∈ ℕ0 → ((1↑𝑛) / (!‘𝑛)) = (1 / (!‘𝑛)))
5453mpteq2ia 4051 . . . . . . . . 9 (𝑛 ∈ ℕ0 ↦ ((1↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (1 / (!‘𝑛)))
5511, 54eqtr4i 2181 . . . . . . . 8 𝐺 = (𝑛 ∈ ℕ0 ↦ ((1↑𝑛) / (!‘𝑛)))
5655efcvg 11567 . . . . . . 7 (1 ∈ ℂ → seq0( + , 𝐺) ⇝ (exp‘1))
5726, 56mp1i 10 . . . . . 6 (⊤ → seq0( + , 𝐺) ⇝ (exp‘1))
58 df-e 11550 . . . . . 6 e = (exp‘1)
5957, 58breqtrrdi 4007 . . . . 5 (⊤ → seq0( + , 𝐺) ⇝ e)
6013adantl 275 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) = (1 / (!‘𝑘)))
617adantl 275 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℕ)
6261nnrecred 8881 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / (!‘𝑘)) ∈ ℝ)
6360, 62eqeltrd 2234 . . . . 5 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℝ)
6461nnred 8847 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℝ)
6561nngt0d 8878 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ0) → 0 < (!‘𝑘))
66 1re 7878 . . . . . . . 8 1 ∈ ℝ
67 0le1 8357 . . . . . . . 8 0 ≤ 1
68 divge0 8745 . . . . . . . 8 (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ ((!‘𝑘) ∈ ℝ ∧ 0 < (!‘𝑘))) → 0 ≤ (1 / (!‘𝑘)))
6966, 67, 68mpanl12 433 . . . . . . 7 (((!‘𝑘) ∈ ℝ ∧ 0 < (!‘𝑘)) → 0 ≤ (1 / (!‘𝑘)))
7064, 65, 69syl2anc 409 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ0) → 0 ≤ (1 / (!‘𝑘)))
7170, 60breqtrrd 3993 . . . . 5 ((⊤ ∧ 𝑘 ∈ ℕ0) → 0 ≤ (𝐺𝑘))
722, 49, 59, 63, 71climserle 11246 . . . 4 (⊤ → (seq0( + , 𝐺)‘1) ≤ e)
7348, 72eqbrtrrd 3989 . . 3 (⊤ → 2 ≤ e)
7473mptru 1344 . 2 2 ≤ e
75 nnuz 9475 . . . . . 6 ℕ = (ℤ‘1)
76 1zzd 9195 . . . . . 6 (⊤ → 1 ∈ ℤ)
771a1i 9 . . . . . . . 8 (⊤ → 0 ∈ ℕ0)
7863recnd 7907 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℂ)
792, 77, 78, 59clim2ser 11238 . . . . . . 7 (⊤ → seq(0 + 1)( + , 𝐺) ⇝ (e − (seq0( + , 𝐺)‘0)))
80 0p1e1 8948 . . . . . . . 8 (0 + 1) = 1
81 seqeq1 10351 . . . . . . . 8 ((0 + 1) = 1 → seq(0 + 1)( + , 𝐺) = seq1( + , 𝐺))
8280, 81ax-mp 5 . . . . . . 7 seq(0 + 1)( + , 𝐺) = seq1( + , 𝐺)
8332mptru 1344 . . . . . . . 8 (seq0( + , 𝐺)‘0) = 1
8483oveq2i 5836 . . . . . . 7 (e − (seq0( + , 𝐺)‘0)) = (e − 1)
8579, 82, 843brtr3g 3998 . . . . . 6 (⊤ → seq1( + , 𝐺) ⇝ (e − 1))
86 2cnd 8907 . . . . . . . 8 (⊤ → 2 ∈ ℂ)
87 halfre 9047 . . . . . . . . . . . . . . 15 (1 / 2) ∈ ℝ
8887a1i 9 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → (1 / 2) ∈ ℝ)
89 id 19 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0𝑘 ∈ ℕ0)
9088, 89reexpcld 10572 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 → ((1 / 2)↑𝑘) ∈ ℝ)
91 oveq2 5833 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 → ((1 / 2)↑𝑛) = ((1 / 2)↑𝑘))
92 eqid 2157 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)) = (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))
9391, 92fvmptg 5545 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0 ∧ ((1 / 2)↑𝑘) ∈ ℝ) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
9490, 93mpdan 418 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
9594adantl 275 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
96 simpr 109 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
97 reexpcl 10440 . . . . . . . . . . . . 13 (((1 / 2) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) ∈ ℝ)
9887, 96, 97sylancr 411 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) ∈ ℝ)
9998recnd 7907 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) ∈ ℂ)
10095, 99eqeltrd 2234 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) ∈ ℂ)
101 1lt2 9003 . . . . . . . . . . . . . 14 1 < 2
102 2re 8904 . . . . . . . . . . . . . . 15 2 ∈ ℝ
103 0le2 8924 . . . . . . . . . . . . . . 15 0 ≤ 2
104 absid 10975 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ ∧ 0 ≤ 2) → (abs‘2) = 2)
105102, 103, 104mp2an 423 . . . . . . . . . . . . . 14 (abs‘2) = 2
106101, 105breqtrri 3992 . . . . . . . . . . . . 13 1 < (abs‘2)
107106a1i 9 . . . . . . . . . . . 12 (⊤ → 1 < (abs‘2))
10886, 107, 95georeclim 11414 . . . . . . . . . . 11 (⊤ → seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ (2 / (2 − 1)))
109 2m1e1 8952 . . . . . . . . . . . . 13 (2 − 1) = 1
110109oveq2i 5836 . . . . . . . . . . . 12 (2 / (2 − 1)) = (2 / 1)
111 2cn 8905 . . . . . . . . . . . . 13 2 ∈ ℂ
112111div1i 8614 . . . . . . . . . . . 12 (2 / 1) = 2
113110, 112eqtri 2178 . . . . . . . . . . 11 (2 / (2 − 1)) = 2
114108, 113breqtrdi 4006 . . . . . . . . . 10 (⊤ → seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ 2)
1152, 77, 100, 114clim2ser 11238 . . . . . . . . 9 (⊤ → seq(0 + 1)( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ (2 − (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0)))
116 seqeq1 10351 . . . . . . . . . 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 275 . . . . . . . . . . . . . . 15 ((⊤ ∧ 𝑘 ∈ (ℤ‘0)) → 𝑘 ∈ ℕ0)
11994, 90eqeltrd 2234 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) ∈ ℝ)
120118, 119syl 14 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑘 ∈ (ℤ‘0)) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) ∈ ℝ)
12120, 120, 18seq3-1 10363 . . . . . . . . . . . . 13 (⊤ → (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0) = ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0))
122 halfcn 9048 . . . . . . . . . . . . . . . . 17 (1 / 2) ∈ ℂ
123 exp0 10427 . . . . . . . . . . . . . . . . 17 ((1 / 2) ∈ ℂ → ((1 / 2)↑0) = 1)
124122, 123ax-mp 5 . . . . . . . . . . . . . . . 16 ((1 / 2)↑0) = 1
125124, 35eqeltri 2230 . . . . . . . . . . . . . . 15 ((1 / 2)↑0) ∈ ℕ0
126 oveq2 5833 . . . . . . . . . . . . . . . 16 (𝑛 = 0 → ((1 / 2)↑𝑛) = ((1 / 2)↑0))
127126, 92fvmptg 5545 . . . . . . . . . . . . . . 15 ((0 ∈ ℕ0 ∧ ((1 / 2)↑0) ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0) = ((1 / 2)↑0))
1281, 125, 127mp2an 423 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0) = ((1 / 2)↑0)
129128, 124eqtri 2178 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0) = 1
130121, 129eqtrdi 2206 . . . . . . . . . . . 12 (⊤ → (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0) = 1)
131130mptru 1344 . . . . . . . . . . 11 (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0) = 1
132131oveq2i 5836 . . . . . . . . . 10 (2 − (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0)) = (2 − 1)
133132, 109eqtri 2178 . . . . . . . . 9 (2 − (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0)) = 1
134115, 117, 1333brtr3g 3998 . . . . . . . 8 (⊤ → seq1( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ 1)
135 nnnn0 9098 . . . . . . . . 9 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
136135, 100sylan2 284 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) ∈ ℂ)
137102a1i 9 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 2 ∈ ℝ)
138135, 90syl 14 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → ((1 / 2)↑𝑘) ∈ ℝ)
139137, 138remulcld 7909 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
14091oveq2d 5841 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (2 · ((1 / 2)↑𝑛)) = (2 · ((1 / 2)↑𝑘)))
141 erelem1.1 . . . . . . . . . . . 12 𝐹 = (𝑛 ∈ ℕ ↦ (2 · ((1 / 2)↑𝑛)))
142140, 141fvmptg 5545 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ (2 · ((1 / 2)↑𝑘)) ∈ ℝ) → (𝐹𝑘) = (2 · ((1 / 2)↑𝑘)))
143139, 142mpdan 418 . . . . . . . . . 10 (𝑘 ∈ ℕ → (𝐹𝑘) = (2 · ((1 / 2)↑𝑘)))
144143adantl 275 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) = (2 · ((1 / 2)↑𝑘)))
145135, 95sylan2 284 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
146145oveq2d 5841 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ) → (2 · ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘)) = (2 · ((1 / 2)↑𝑘)))
147144, 146eqtr4d 2193 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) = (2 · ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘)))
14875, 76, 86, 134, 136, 147isermulc2 11241 . . . . . . 7 (⊤ → seq1( + , 𝐹) ⇝ (2 · 1))
149 2t1e2 8987 . . . . . . 7 (2 · 1) = 2
150148, 149breqtrdi 4006 . . . . . 6 (⊤ → seq1( + , 𝐹) ⇝ 2)
151135, 63sylan2 284 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)
152 remulcl 7861 . . . . . . . . 9 ((2 ∈ ℝ ∧ ((1 / 2)↑𝑘) ∈ ℝ) → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
153102, 98, 152sylancr 411 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
154135, 153sylan2 284 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
155144, 154eqeltrd 2234 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℝ)
156 faclbnd2 10620 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → ((2↑𝑘) / 2) ≤ (!‘𝑘))
157156adantl 275 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((2↑𝑘) / 2) ≤ (!‘𝑘))
158 2nn 8995 . . . . . . . . . . . . . 14 2 ∈ ℕ
159 nnexpcl 10436 . . . . . . . . . . . . . 14 ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
160158, 96, 159sylancr 411 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
161160nnrpd 9602 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℝ+)
162161rphalfcld 9617 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((2↑𝑘) / 2) ∈ ℝ+)
16361nnrpd 9602 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℝ+)
164162, 163lerecd 9624 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (((2↑𝑘) / 2) ≤ (!‘𝑘) ↔ (1 / (!‘𝑘)) ≤ (1 / ((2↑𝑘) / 2))))
165157, 164mpbid 146 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / (!‘𝑘)) ≤ (1 / ((2↑𝑘) / 2)))
166 2cnd 8907 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → 2 ∈ ℂ)
167160nncnd 8848 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℂ)
168160nnap0d 8880 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) # 0)
169166, 167, 168divrecapd 8667 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 / (2↑𝑘)) = (2 · (1 / (2↑𝑘))))
170 2ap0 8927 . . . . . . . . . . . 12 2 # 0
171170a1i 9 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → 2 # 0)
172167, 166, 168, 171recdivapd 8681 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / ((2↑𝑘) / 2)) = (2 / (2↑𝑘)))
173 nn0z 9188 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℤ)
174173adantl 275 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℤ)
175166, 171, 174exprecapd 10563 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) = (1 / (2↑𝑘)))
176175oveq2d 5841 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · ((1 / 2)↑𝑘)) = (2 · (1 / (2↑𝑘))))
177169, 172, 1763eqtr4rd 2201 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · ((1 / 2)↑𝑘)) = (1 / ((2↑𝑘) / 2)))
178165, 177breqtrrd 3993 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / (!‘𝑘)) ≤ (2 · ((1 / 2)↑𝑘)))
179135, 178sylan2 284 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (1 / (!‘𝑘)) ≤ (2 · ((1 / 2)↑𝑘)))
180135, 60sylan2 284 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) = (1 / (!‘𝑘)))
181179, 180, 1443brtr4d 3997 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ≤ (𝐹𝑘))
18275, 76, 85, 150, 151, 155, 181iserle 11243 . . . . 5 (⊤ → (e − 1) ≤ 2)
183182mptru 1344 . . . 4 (e − 1) ≤ 2
184 ere 11571 . . . . 5 e ∈ ℝ
185184, 66, 102lesubaddi 8382 . . . 4 ((e − 1) ≤ 2 ↔ e ≤ (2 + 1))
186183, 185mpbi 144 . . 3 e ≤ (2 + 1)
187 df-3 8894 . . 3 3 = (2 + 1)
188186, 187breqtrri 3992 . 2 e ≤ 3
18974, 188pm3.2i 270 1 (2 ≤ e ∧ e ≤ 3)
Colors of variables: wff set class
Syntax hints:  wa 103   = wceq 1335  wtru 1336  wcel 2128   class class class wbr 3966  cmpt 4026  cfv 5171  (class class class)co 5825  cc 7731  cr 7732  0cc0 7733  1c1 7734   + caddc 7736   · cmul 7738   < clt 7913  cle 7914  cmin 8047   # cap 8457   / cdiv 8546  cn 8834  2c2 8885  3c3 8886  0cn0 9091  cz 9168  cuz 9440  seqcseq 10348  cexp 10422  !cfa 10603  abscabs 10901  cli 11179  expce 11543  eceu 11544
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 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-coll 4080  ax-sep 4083  ax-nul 4091  ax-pow 4136  ax-pr 4170  ax-un 4394  ax-setind 4497  ax-iinf 4548  ax-cnex 7824  ax-resscn 7825  ax-1cn 7826  ax-1re 7827  ax-icn 7828  ax-addcl 7829  ax-addrcl 7830  ax-mulcl 7831  ax-mulrcl 7832  ax-addcom 7833  ax-mulcom 7834  ax-addass 7835  ax-mulass 7836  ax-distr 7837  ax-i2m1 7838  ax-0lt1 7839  ax-1rid 7840  ax-0id 7841  ax-rnegex 7842  ax-precex 7843  ax-cnre 7844  ax-pre-ltirr 7845  ax-pre-ltwlin 7846  ax-pre-lttrn 7847  ax-pre-apti 7848  ax-pre-ltadd 7849  ax-pre-mulgt0 7850  ax-pre-mulext 7851  ax-arch 7852  ax-caucvg 7853
This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-nel 2423  df-ral 2440  df-rex 2441  df-reu 2442  df-rmo 2443  df-rab 2444  df-v 2714  df-sbc 2938  df-csb 3032  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-if 3506  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3774  df-int 3809  df-iun 3852  df-br 3967  df-opab 4027  df-mpt 4028  df-tr 4064  df-id 4254  df-po 4257  df-iso 4258  df-iord 4327  df-on 4329  df-ilim 4330  df-suc 4332  df-iom 4551  df-xp 4593  df-rel 4594  df-cnv 4595  df-co 4596  df-dm 4597  df-rn 4598  df-res 4599  df-ima 4600  df-iota 5136  df-fun 5173  df-fn 5174  df-f 5175  df-f1 5176  df-fo 5177  df-f1o 5178  df-fv 5179  df-isom 5180  df-riota 5781  df-ov 5828  df-oprab 5829  df-mpo 5830  df-1st 6089  df-2nd 6090  df-recs 6253  df-irdg 6318  df-frec 6339  df-1o 6364  df-oadd 6368  df-er 6481  df-en 6687  df-dom 6688  df-fin 6689  df-pnf 7915  df-mnf 7916  df-xr 7917  df-ltxr 7918  df-le 7919  df-sub 8049  df-neg 8050  df-reap 8451  df-ap 8458  df-div 8547  df-inn 8835  df-2 8893  df-3 8894  df-4 8895  df-n0 9092  df-z 9169  df-uz 9441  df-q 9530  df-rp 9562  df-ico 9799  df-fz 9914  df-fzo 10046  df-seqfrec 10349  df-exp 10423  df-fac 10604  df-ihash 10654  df-cj 10746  df-re 10747  df-im 10748  df-rsqrt 10902  df-abs 10903  df-clim 11180  df-sumdc 11255  df-ef 11549  df-e 11550
This theorem is referenced by:  egt2lt3  11680
  Copyright terms: Public domain W3C validator