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

Theorem ege2le3 11634
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 9150 . . . . . . . . 9 0 ∈ ℕ0
2 nn0uz 9521 . . . . . . . . 9 0 = (ℤ‘0)
31, 2eleqtri 2245 . . . . . . . 8 0 ∈ (ℤ‘0)
43a1i 9 . . . . . . 7 (⊤ → 0 ∈ (ℤ‘0))
5 elnn0uz 9524 . . . . . . . . . 10 (𝑘 ∈ ℕ0𝑘 ∈ (ℤ‘0))
65biimpri 132 . . . . . . . . 9 (𝑘 ∈ (ℤ‘0) → 𝑘 ∈ ℕ0)
7 faccl 10669 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → (!‘𝑘) ∈ ℕ)
87nnrecred 8925 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → (1 / (!‘𝑘)) ∈ ℝ)
9 fveq2 5496 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (!‘𝑛) = (!‘𝑘))
109oveq2d 5869 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (1 / (!‘𝑛)) = (1 / (!‘𝑘)))
11 erelem1.2 . . . . . . . . . . . 12 𝐺 = (𝑛 ∈ ℕ0 ↦ (1 / (!‘𝑛)))
1210, 11fvmptg 5572 . . . . . . . . . . 11 ((𝑘 ∈ ℕ0 ∧ (1 / (!‘𝑘)) ∈ ℝ) → (𝐺𝑘) = (1 / (!‘𝑘)))
138, 12mpdan 419 . . . . . . . . . 10 (𝑘 ∈ ℕ0 → (𝐺𝑘) = (1 / (!‘𝑘)))
1413, 8eqeltrd 2247 . . . . . . . . 9 (𝑘 ∈ ℕ0 → (𝐺𝑘) ∈ ℝ)
156, 14syl 14 . . . . . . . 8 (𝑘 ∈ (ℤ‘0) → (𝐺𝑘) ∈ ℝ)
1615adantl 275 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ (ℤ‘0)) → (𝐺𝑘) ∈ ℝ)
17 readdcl 7900 . . . . . . . 8 ((𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑘 + 𝑦) ∈ ℝ)
1817adantl 275 . . . . . . 7 ((⊤ ∧ (𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑘 + 𝑦) ∈ ℝ)
194, 16, 18seq3p1 10418 . . . . . 6 (⊤ → (seq0( + , 𝐺)‘(0 + 1)) = ((seq0( + , 𝐺)‘0) + (𝐺‘(0 + 1))))
20 0zd 9224 . . . . . . . . 9 (⊤ → 0 ∈ ℤ)
2120, 16, 18seq3-1 10416 . . . . . . . 8 (⊤ → (seq0( + , 𝐺)‘0) = (𝐺‘0))
22 fveq2 5496 . . . . . . . . . . . . 13 (𝑛 = 0 → (!‘𝑛) = (!‘0))
23 fac0 10662 . . . . . . . . . . . . 13 (!‘0) = 1
2422, 23eqtrdi 2219 . . . . . . . . . . . 12 (𝑛 = 0 → (!‘𝑛) = 1)
2524oveq2d 5869 . . . . . . . . . . 11 (𝑛 = 0 → (1 / (!‘𝑛)) = (1 / 1))
26 ax-1cn 7867 . . . . . . . . . . . 12 1 ∈ ℂ
2726div1i 8657 . . . . . . . . . . 11 (1 / 1) = 1
2825, 27eqtrdi 2219 . . . . . . . . . 10 (𝑛 = 0 → (1 / (!‘𝑛)) = 1)
29 1ex 7915 . . . . . . . . . 10 1 ∈ V
3028, 11, 29fvmpt 5573 . . . . . . . . 9 (0 ∈ ℕ0 → (𝐺‘0) = 1)
311, 30mp1i 10 . . . . . . . 8 (⊤ → (𝐺‘0) = 1)
3221, 31eqtrd 2203 . . . . . . 7 (⊤ → (seq0( + , 𝐺)‘0) = 1)
33 1e0p1 9384 . . . . . . . . 9 1 = (0 + 1)
3433fveq2i 5499 . . . . . . . 8 (𝐺‘1) = (𝐺‘(0 + 1))
35 1nn0 9151 . . . . . . . . 9 1 ∈ ℕ0
36 fveq2 5496 . . . . . . . . . . . . 13 (𝑛 = 1 → (!‘𝑛) = (!‘1))
37 fac1 10663 . . . . . . . . . . . . 13 (!‘1) = 1
3836, 37eqtrdi 2219 . . . . . . . . . . . 12 (𝑛 = 1 → (!‘𝑛) = 1)
3938oveq2d 5869 . . . . . . . . . . 11 (𝑛 = 1 → (1 / (!‘𝑛)) = (1 / 1))
4039, 27eqtrdi 2219 . . . . . . . . . 10 (𝑛 = 1 → (1 / (!‘𝑛)) = 1)
4140, 11, 29fvmpt 5573 . . . . . . . . 9 (1 ∈ ℕ0 → (𝐺‘1) = 1)
4235, 41mp1i 10 . . . . . . . 8 (⊤ → (𝐺‘1) = 1)
4334, 42eqtr3id 2217 . . . . . . 7 (⊤ → (𝐺‘(0 + 1)) = 1)
4432, 43oveq12d 5871 . . . . . 6 (⊤ → ((seq0( + , 𝐺)‘0) + (𝐺‘(0 + 1))) = (1 + 1))
4519, 44eqtrd 2203 . . . . 5 (⊤ → (seq0( + , 𝐺)‘(0 + 1)) = (1 + 1))
4633fveq2i 5499 . . . . 5 (seq0( + , 𝐺)‘1) = (seq0( + , 𝐺)‘(0 + 1))
47 df-2 8937 . . . . 5 2 = (1 + 1)
4845, 46, 473eqtr4g 2228 . . . 4 (⊤ → (seq0( + , 𝐺)‘1) = 2)
4935a1i 9 . . . . 5 (⊤ → 1 ∈ ℕ0)
50 nn0z 9232 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0𝑛 ∈ ℤ)
51 1exp 10505 . . . . . . . . . . . 12 (𝑛 ∈ ℤ → (1↑𝑛) = 1)
5250, 51syl 14 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 → (1↑𝑛) = 1)
5352oveq1d 5868 . . . . . . . . . 10 (𝑛 ∈ ℕ0 → ((1↑𝑛) / (!‘𝑛)) = (1 / (!‘𝑛)))
5453mpteq2ia 4075 . . . . . . . . 9 (𝑛 ∈ ℕ0 ↦ ((1↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (1 / (!‘𝑛)))
5511, 54eqtr4i 2194 . . . . . . . 8 𝐺 = (𝑛 ∈ ℕ0 ↦ ((1↑𝑛) / (!‘𝑛)))
5655efcvg 11629 . . . . . . 7 (1 ∈ ℂ → seq0( + , 𝐺) ⇝ (exp‘1))
5726, 56mp1i 10 . . . . . 6 (⊤ → seq0( + , 𝐺) ⇝ (exp‘1))
58 df-e 11612 . . . . . 6 e = (exp‘1)
5957, 58breqtrrdi 4031 . . . . 5 (⊤ → seq0( + , 𝐺) ⇝ e)
6013adantl 275 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) = (1 / (!‘𝑘)))
617adantl 275 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℕ)
6261nnrecred 8925 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / (!‘𝑘)) ∈ ℝ)
6360, 62eqeltrd 2247 . . . . 5 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℝ)
6461nnred 8891 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℝ)
6561nngt0d 8922 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ0) → 0 < (!‘𝑘))
66 1re 7919 . . . . . . . 8 1 ∈ ℝ
67 0le1 8400 . . . . . . . 8 0 ≤ 1
68 divge0 8789 . . . . . . . 8 (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ ((!‘𝑘) ∈ ℝ ∧ 0 < (!‘𝑘))) → 0 ≤ (1 / (!‘𝑘)))
6966, 67, 68mpanl12 434 . . . . . . 7 (((!‘𝑘) ∈ ℝ ∧ 0 < (!‘𝑘)) → 0 ≤ (1 / (!‘𝑘)))
7064, 65, 69syl2anc 409 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ0) → 0 ≤ (1 / (!‘𝑘)))
7170, 60breqtrrd 4017 . . . . 5 ((⊤ ∧ 𝑘 ∈ ℕ0) → 0 ≤ (𝐺𝑘))
722, 49, 59, 63, 71climserle 11308 . . . 4 (⊤ → (seq0( + , 𝐺)‘1) ≤ e)
7348, 72eqbrtrrd 4013 . . 3 (⊤ → 2 ≤ e)
7473mptru 1357 . 2 2 ≤ e
75 nnuz 9522 . . . . . 6 ℕ = (ℤ‘1)
76 1zzd 9239 . . . . . 6 (⊤ → 1 ∈ ℤ)
771a1i 9 . . . . . . . 8 (⊤ → 0 ∈ ℕ0)
7863recnd 7948 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℂ)
792, 77, 78, 59clim2ser 11300 . . . . . . 7 (⊤ → seq(0 + 1)( + , 𝐺) ⇝ (e − (seq0( + , 𝐺)‘0)))
80 0p1e1 8992 . . . . . . . 8 (0 + 1) = 1
81 seqeq1 10404 . . . . . . . 8 ((0 + 1) = 1 → seq(0 + 1)( + , 𝐺) = seq1( + , 𝐺))
8280, 81ax-mp 5 . . . . . . 7 seq(0 + 1)( + , 𝐺) = seq1( + , 𝐺)
8332mptru 1357 . . . . . . . 8 (seq0( + , 𝐺)‘0) = 1
8483oveq2i 5864 . . . . . . 7 (e − (seq0( + , 𝐺)‘0)) = (e − 1)
8579, 82, 843brtr3g 4022 . . . . . 6 (⊤ → seq1( + , 𝐺) ⇝ (e − 1))
86 2cnd 8951 . . . . . . . 8 (⊤ → 2 ∈ ℂ)
87 halfre 9091 . . . . . . . . . . . . . . 15 (1 / 2) ∈ ℝ
8887a1i 9 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0 → (1 / 2) ∈ ℝ)
89 id 19 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ0𝑘 ∈ ℕ0)
9088, 89reexpcld 10626 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0 → ((1 / 2)↑𝑘) ∈ ℝ)
91 oveq2 5861 . . . . . . . . . . . . . 14 (𝑛 = 𝑘 → ((1 / 2)↑𝑛) = ((1 / 2)↑𝑘))
92 eqid 2170 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)) = (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))
9391, 92fvmptg 5572 . . . . . . . . . . . . 13 ((𝑘 ∈ ℕ0 ∧ ((1 / 2)↑𝑘) ∈ ℝ) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
9490, 93mpdan 419 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
9594adantl 275 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
96 simpr 109 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
97 reexpcl 10493 . . . . . . . . . . . . 13 (((1 / 2) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) ∈ ℝ)
9887, 96, 97sylancr 412 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) ∈ ℝ)
9998recnd 7948 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) ∈ ℂ)
10095, 99eqeltrd 2247 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) ∈ ℂ)
101 1lt2 9047 . . . . . . . . . . . . . 14 1 < 2
102 2re 8948 . . . . . . . . . . . . . . 15 2 ∈ ℝ
103 0le2 8968 . . . . . . . . . . . . . . 15 0 ≤ 2
104 absid 11035 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ ∧ 0 ≤ 2) → (abs‘2) = 2)
105102, 103, 104mp2an 424 . . . . . . . . . . . . . 14 (abs‘2) = 2
106101, 105breqtrri 4016 . . . . . . . . . . . . 13 1 < (abs‘2)
107106a1i 9 . . . . . . . . . . . 12 (⊤ → 1 < (abs‘2))
10886, 107, 95georeclim 11476 . . . . . . . . . . 11 (⊤ → seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ (2 / (2 − 1)))
109 2m1e1 8996 . . . . . . . . . . . . 13 (2 − 1) = 1
110109oveq2i 5864 . . . . . . . . . . . 12 (2 / (2 − 1)) = (2 / 1)
111 2cn 8949 . . . . . . . . . . . . 13 2 ∈ ℂ
112111div1i 8657 . . . . . . . . . . . 12 (2 / 1) = 2
113110, 112eqtri 2191 . . . . . . . . . . 11 (2 / (2 − 1)) = 2
114108, 113breqtrdi 4030 . . . . . . . . . 10 (⊤ → seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ 2)
1152, 77, 100, 114clim2ser 11300 . . . . . . . . 9 (⊤ → seq(0 + 1)( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ (2 − (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0)))
116 seqeq1 10404 . . . . . . . . . 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 2247 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) ∈ ℝ)
120118, 119syl 14 . . . . . . . . . . . . . 14 ((⊤ ∧ 𝑘 ∈ (ℤ‘0)) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) ∈ ℝ)
12120, 120, 18seq3-1 10416 . . . . . . . . . . . . 13 (⊤ → (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0) = ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0))
122 halfcn 9092 . . . . . . . . . . . . . . . . 17 (1 / 2) ∈ ℂ
123 exp0 10480 . . . . . . . . . . . . . . . . 17 ((1 / 2) ∈ ℂ → ((1 / 2)↑0) = 1)
124122, 123ax-mp 5 . . . . . . . . . . . . . . . 16 ((1 / 2)↑0) = 1
125124, 35eqeltri 2243 . . . . . . . . . . . . . . 15 ((1 / 2)↑0) ∈ ℕ0
126 oveq2 5861 . . . . . . . . . . . . . . . 16 (𝑛 = 0 → ((1 / 2)↑𝑛) = ((1 / 2)↑0))
127126, 92fvmptg 5572 . . . . . . . . . . . . . . 15 ((0 ∈ ℕ0 ∧ ((1 / 2)↑0) ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0) = ((1 / 2)↑0))
1281, 125, 127mp2an 424 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0) = ((1 / 2)↑0)
129128, 124eqtri 2191 . . . . . . . . . . . . 13 ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0) = 1
130121, 129eqtrdi 2219 . . . . . . . . . . . 12 (⊤ → (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0) = 1)
131130mptru 1357 . . . . . . . . . . 11 (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0) = 1
132131oveq2i 5864 . . . . . . . . . 10 (2 − (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0)) = (2 − 1)
133132, 109eqtri 2191 . . . . . . . . 9 (2 − (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0)) = 1
134115, 117, 1333brtr3g 4022 . . . . . . . 8 (⊤ → seq1( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ 1)
135 nnnn0 9142 . . . . . . . . 9 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
136135, 100sylan2 284 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) ∈ ℂ)
137102a1i 9 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → 2 ∈ ℝ)
138135, 90syl 14 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → ((1 / 2)↑𝑘) ∈ ℝ)
139137, 138remulcld 7950 . . . . . . . . . . 11 (𝑘 ∈ ℕ → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
14091oveq2d 5869 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (2 · ((1 / 2)↑𝑛)) = (2 · ((1 / 2)↑𝑘)))
141 erelem1.1 . . . . . . . . . . . 12 𝐹 = (𝑛 ∈ ℕ ↦ (2 · ((1 / 2)↑𝑛)))
142140, 141fvmptg 5572 . . . . . . . . . . 11 ((𝑘 ∈ ℕ ∧ (2 · ((1 / 2)↑𝑘)) ∈ ℝ) → (𝐹𝑘) = (2 · ((1 / 2)↑𝑘)))
143139, 142mpdan 419 . . . . . . . . . 10 (𝑘 ∈ ℕ → (𝐹𝑘) = (2 · ((1 / 2)↑𝑘)))
144143adantl 275 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) = (2 · ((1 / 2)↑𝑘)))
145135, 95sylan2 284 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
146145oveq2d 5869 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ) → (2 · ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘)) = (2 · ((1 / 2)↑𝑘)))
147144, 146eqtr4d 2206 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) = (2 · ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘)))
14875, 76, 86, 134, 136, 147isermulc2 11303 . . . . . . 7 (⊤ → seq1( + , 𝐹) ⇝ (2 · 1))
149 2t1e2 9031 . . . . . . 7 (2 · 1) = 2
150148, 149breqtrdi 4030 . . . . . 6 (⊤ → seq1( + , 𝐹) ⇝ 2)
151135, 63sylan2 284 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)
152 remulcl 7902 . . . . . . . . 9 ((2 ∈ ℝ ∧ ((1 / 2)↑𝑘) ∈ ℝ) → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
153102, 98, 152sylancr 412 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
154135, 153sylan2 284 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
155144, 154eqeltrd 2247 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℝ)
156 faclbnd2 10676 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → ((2↑𝑘) / 2) ≤ (!‘𝑘))
157156adantl 275 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((2↑𝑘) / 2) ≤ (!‘𝑘))
158 2nn 9039 . . . . . . . . . . . . . 14 2 ∈ ℕ
159 nnexpcl 10489 . . . . . . . . . . . . . 14 ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
160158, 96, 159sylancr 412 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
161160nnrpd 9651 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℝ+)
162161rphalfcld 9666 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((2↑𝑘) / 2) ∈ ℝ+)
16361nnrpd 9651 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℝ+)
164162, 163lerecd 9673 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (((2↑𝑘) / 2) ≤ (!‘𝑘) ↔ (1 / (!‘𝑘)) ≤ (1 / ((2↑𝑘) / 2))))
165157, 164mpbid 146 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / (!‘𝑘)) ≤ (1 / ((2↑𝑘) / 2)))
166 2cnd 8951 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → 2 ∈ ℂ)
167160nncnd 8892 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℂ)
168160nnap0d 8924 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) # 0)
169166, 167, 168divrecapd 8710 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 / (2↑𝑘)) = (2 · (1 / (2↑𝑘))))
170 2ap0 8971 . . . . . . . . . . . 12 2 # 0
171170a1i 9 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → 2 # 0)
172167, 166, 168, 171recdivapd 8724 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / ((2↑𝑘) / 2)) = (2 / (2↑𝑘)))
173 nn0z 9232 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℤ)
174173adantl 275 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℤ)
175166, 171, 174exprecapd 10617 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) = (1 / (2↑𝑘)))
176175oveq2d 5869 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · ((1 / 2)↑𝑘)) = (2 · (1 / (2↑𝑘))))
177169, 172, 1763eqtr4rd 2214 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · ((1 / 2)↑𝑘)) = (1 / ((2↑𝑘) / 2)))
178165, 177breqtrrd 4017 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / (!‘𝑘)) ≤ (2 · ((1 / 2)↑𝑘)))
179135, 178sylan2 284 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (1 / (!‘𝑘)) ≤ (2 · ((1 / 2)↑𝑘)))
180135, 60sylan2 284 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) = (1 / (!‘𝑘)))
181179, 180, 1443brtr4d 4021 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ≤ (𝐹𝑘))
18275, 76, 85, 150, 151, 155, 181iserle 11305 . . . . 5 (⊤ → (e − 1) ≤ 2)
183182mptru 1357 . . . 4 (e − 1) ≤ 2
184 ere 11633 . . . . 5 e ∈ ℝ
185184, 66, 102lesubaddi 8425 . . . 4 ((e − 1) ≤ 2 ↔ e ≤ (2 + 1))
186183, 185mpbi 144 . . 3 e ≤ (2 + 1)
187 df-3 8938 . . 3 3 = (2 + 1)
188186, 187breqtrri 4016 . 2 e ≤ 3
18974, 188pm3.2i 270 1 (2 ≤ e ∧ e ≤ 3)
Colors of variables: wff set class
Syntax hints:  wa 103   = wceq 1348  wtru 1349  wcel 2141   class class class wbr 3989  cmpt 4050  cfv 5198  (class class class)co 5853  cc 7772  cr 7773  0cc0 7774  1c1 7775   + caddc 7777   · cmul 7779   < clt 7954  cle 7955  cmin 8090   # cap 8500   / cdiv 8589  cn 8878  2c2 8929  3c3 8930  0cn0 9135  cz 9212  cuz 9487  seqcseq 10401  cexp 10475  !cfa 10659  abscabs 10961  cli 11241  expce 11605  eceu 11606
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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4104  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-iinf 4572  ax-cnex 7865  ax-resscn 7866  ax-1cn 7867  ax-1re 7868  ax-icn 7869  ax-addcl 7870  ax-addrcl 7871  ax-mulcl 7872  ax-mulrcl 7873  ax-addcom 7874  ax-mulcom 7875  ax-addass 7876  ax-mulass 7877  ax-distr 7878  ax-i2m1 7879  ax-0lt1 7880  ax-1rid 7881  ax-0id 7882  ax-rnegex 7883  ax-precex 7884  ax-cnre 7885  ax-pre-ltirr 7886  ax-pre-ltwlin 7887  ax-pre-lttrn 7888  ax-pre-apti 7889  ax-pre-ltadd 7890  ax-pre-mulgt0 7891  ax-pre-mulext 7892  ax-arch 7893  ax-caucvg 7894
This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rmo 2456  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-if 3527  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-int 3832  df-iun 3875  df-br 3990  df-opab 4051  df-mpt 4052  df-tr 4088  df-id 4278  df-po 4281  df-iso 4282  df-iord 4351  df-on 4353  df-ilim 4354  df-suc 4356  df-iom 4575  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-isom 5207  df-riota 5809  df-ov 5856  df-oprab 5857  df-mpo 5858  df-1st 6119  df-2nd 6120  df-recs 6284  df-irdg 6349  df-frec 6370  df-1o 6395  df-oadd 6399  df-er 6513  df-en 6719  df-dom 6720  df-fin 6721  df-pnf 7956  df-mnf 7957  df-xr 7958  df-ltxr 7959  df-le 7960  df-sub 8092  df-neg 8093  df-reap 8494  df-ap 8501  df-div 8590  df-inn 8879  df-2 8937  df-3 8938  df-4 8939  df-n0 9136  df-z 9213  df-uz 9488  df-q 9579  df-rp 9611  df-ico 9851  df-fz 9966  df-fzo 10099  df-seqfrec 10402  df-exp 10476  df-fac 10660  df-ihash 10710  df-cj 10806  df-re 10807  df-im 10808  df-rsqrt 10962  df-abs 10963  df-clim 11242  df-sumdc 11317  df-ef 11611  df-e 11612
This theorem is referenced by:  egt2lt3  11742
  Copyright terms: Public domain W3C validator