MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ege2le3 Structured version   Visualization version   GIF version

Theorem ege2le3 15036
Description: Lemma for egt2lt3 15150. (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 variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 nn0uz 11936 . . . . . 6 0 = (ℤ‘0)
2 0nn0 11570 . . . . . 6 0 ∈ ℕ0
3 1e0p1 11797 . . . . . 6 1 = (0 + 1)
4 0z 11650 . . . . . . 7 0 ∈ ℤ
5 fveq2 6404 . . . . . . . . . . . 12 (𝑛 = 0 → (!‘𝑛) = (!‘0))
6 fac0 13279 . . . . . . . . . . . 12 (!‘0) = 1
75, 6syl6eq 2856 . . . . . . . . . . 11 (𝑛 = 0 → (!‘𝑛) = 1)
87oveq2d 6886 . . . . . . . . . 10 (𝑛 = 0 → (1 / (!‘𝑛)) = (1 / 1))
9 ax-1cn 10275 . . . . . . . . . . 11 1 ∈ ℂ
109div1i 11034 . . . . . . . . . 10 (1 / 1) = 1
118, 10syl6eq 2856 . . . . . . . . 9 (𝑛 = 0 → (1 / (!‘𝑛)) = 1)
12 erelem1.2 . . . . . . . . 9 𝐺 = (𝑛 ∈ ℕ0 ↦ (1 / (!‘𝑛)))
13 1ex 10317 . . . . . . . . 9 1 ∈ V
1411, 12, 13fvmpt 6499 . . . . . . . 8 (0 ∈ ℕ0 → (𝐺‘0) = 1)
152, 14mp1i 13 . . . . . . 7 (⊤ → (𝐺‘0) = 1)
164, 15seq1i 13034 . . . . . 6 (⊤ → (seq0( + , 𝐺)‘0) = 1)
17 1nn0 11571 . . . . . . 7 1 ∈ ℕ0
18 fveq2 6404 . . . . . . . . . . 11 (𝑛 = 1 → (!‘𝑛) = (!‘1))
19 fac1 13280 . . . . . . . . . . 11 (!‘1) = 1
2018, 19syl6eq 2856 . . . . . . . . . 10 (𝑛 = 1 → (!‘𝑛) = 1)
2120oveq2d 6886 . . . . . . . . 9 (𝑛 = 1 → (1 / (!‘𝑛)) = (1 / 1))
2221, 10syl6eq 2856 . . . . . . . 8 (𝑛 = 1 → (1 / (!‘𝑛)) = 1)
2322, 12, 13fvmpt 6499 . . . . . . 7 (1 ∈ ℕ0 → (𝐺‘1) = 1)
2417, 23mp1i 13 . . . . . 6 (⊤ → (𝐺‘1) = 1)
251, 2, 3, 16, 24seqp1i 13036 . . . . 5 (⊤ → (seq0( + , 𝐺)‘1) = (1 + 1))
26 df-2 11360 . . . . 5 2 = (1 + 1)
2725, 26syl6eqr 2858 . . . 4 (⊤ → (seq0( + , 𝐺)‘1) = 2)
2817a1i 11 . . . . 5 (⊤ → 1 ∈ ℕ0)
29 nn0z 11662 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0𝑛 ∈ ℤ)
30 1exp 13108 . . . . . . . . . . . 12 (𝑛 ∈ ℤ → (1↑𝑛) = 1)
3129, 30syl 17 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 → (1↑𝑛) = 1)
3231oveq1d 6885 . . . . . . . . . 10 (𝑛 ∈ ℕ0 → ((1↑𝑛) / (!‘𝑛)) = (1 / (!‘𝑛)))
3332mpteq2ia 4934 . . . . . . . . 9 (𝑛 ∈ ℕ0 ↦ ((1↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (1 / (!‘𝑛)))
3412, 33eqtr4i 2831 . . . . . . . 8 𝐺 = (𝑛 ∈ ℕ0 ↦ ((1↑𝑛) / (!‘𝑛)))
3534efcvg 15031 . . . . . . 7 (1 ∈ ℂ → seq0( + , 𝐺) ⇝ (exp‘1))
369, 35mp1i 13 . . . . . 6 (⊤ → seq0( + , 𝐺) ⇝ (exp‘1))
37 df-e 15015 . . . . . 6 e = (exp‘1)
3836, 37syl6breqr 4886 . . . . 5 (⊤ → seq0( + , 𝐺) ⇝ e)
39 fveq2 6404 . . . . . . . . 9 (𝑛 = 𝑘 → (!‘𝑛) = (!‘𝑘))
4039oveq2d 6886 . . . . . . . 8 (𝑛 = 𝑘 → (1 / (!‘𝑛)) = (1 / (!‘𝑘)))
41 ovex 6902 . . . . . . . 8 (1 / (!‘𝑘)) ∈ V
4240, 12, 41fvmpt 6499 . . . . . . 7 (𝑘 ∈ ℕ0 → (𝐺𝑘) = (1 / (!‘𝑘)))
4342adantl 469 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) = (1 / (!‘𝑘)))
44 faccl 13286 . . . . . . . 8 (𝑘 ∈ ℕ0 → (!‘𝑘) ∈ ℕ)
4544adantl 469 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℕ)
4645nnrecred 11348 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / (!‘𝑘)) ∈ ℝ)
4743, 46eqeltrd 2885 . . . . 5 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℝ)
4845nnred 11316 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℝ)
4945nngt0d 11346 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ0) → 0 < (!‘𝑘))
50 1re 10321 . . . . . . . 8 1 ∈ ℝ
51 0le1 10832 . . . . . . . 8 0 ≤ 1
52 divge0 11173 . . . . . . . 8 (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ ((!‘𝑘) ∈ ℝ ∧ 0 < (!‘𝑘))) → 0 ≤ (1 / (!‘𝑘)))
5350, 51, 52mpanl12 685 . . . . . . 7 (((!‘𝑘) ∈ ℝ ∧ 0 < (!‘𝑘)) → 0 ≤ (1 / (!‘𝑘)))
5448, 49, 53syl2anc 575 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ0) → 0 ≤ (1 / (!‘𝑘)))
5554, 43breqtrrd 4872 . . . . 5 ((⊤ ∧ 𝑘 ∈ ℕ0) → 0 ≤ (𝐺𝑘))
561, 28, 38, 47, 55climserle 14612 . . . 4 (⊤ → (seq0( + , 𝐺)‘1) ≤ e)
5727, 56eqbrtrrd 4868 . . 3 (⊤ → 2 ≤ e)
5857mptru 1645 . 2 2 ≤ e
59 nnuz 11937 . . . . . 6 ℕ = (ℤ‘1)
60 1zzd 11670 . . . . . 6 (⊤ → 1 ∈ ℤ)
612a1i 11 . . . . . . . 8 (⊤ → 0 ∈ ℕ0)
6247recnd 10349 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℂ)
631, 61, 62, 38clim2ser 14604 . . . . . . 7 (⊤ → seq(0 + 1)( + , 𝐺) ⇝ (e − (seq0( + , 𝐺)‘0)))
64 0p1e1 11410 . . . . . . . 8 (0 + 1) = 1
65 seqeq1 13023 . . . . . . . 8 ((0 + 1) = 1 → seq(0 + 1)( + , 𝐺) = seq1( + , 𝐺))
6664, 65ax-mp 5 . . . . . . 7 seq(0 + 1)( + , 𝐺) = seq1( + , 𝐺)
6716mptru 1645 . . . . . . . 8 (seq0( + , 𝐺)‘0) = 1
6867oveq2i 6881 . . . . . . 7 (e − (seq0( + , 𝐺)‘0)) = (e − 1)
6963, 66, 683brtr3g 4877 . . . . . 6 (⊤ → seq1( + , 𝐺) ⇝ (e − 1))
70 2cnd 11373 . . . . . . . 8 (⊤ → 2 ∈ ℂ)
71 oveq2 6878 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → ((1 / 2)↑𝑛) = ((1 / 2)↑𝑘))
72 eqid 2806 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)) = (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))
73 ovex 6902 . . . . . . . . . . . . 13 ((1 / 2)↑𝑘) ∈ V
7471, 72, 73fvmpt 6499 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
7574adantl 469 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
76 halfre 11509 . . . . . . . . . . . . 13 (1 / 2) ∈ ℝ
77 simpr 473 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
78 reexpcl 13096 . . . . . . . . . . . . 13 (((1 / 2) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) ∈ ℝ)
7976, 77, 78sylancr 577 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) ∈ ℝ)
8079recnd 10349 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) ∈ ℂ)
8175, 80eqeltrd 2885 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) ∈ ℂ)
82 1lt2 11466 . . . . . . . . . . . . . 14 1 < 2
83 2re 11370 . . . . . . . . . . . . . . 15 2 ∈ ℝ
84 0le2 11390 . . . . . . . . . . . . . . 15 0 ≤ 2
85 absid 14255 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ ∧ 0 ≤ 2) → (abs‘2) = 2)
8683, 84, 85mp2an 675 . . . . . . . . . . . . . 14 (abs‘2) = 2
8782, 86breqtrri 4871 . . . . . . . . . . . . 13 1 < (abs‘2)
8887a1i 11 . . . . . . . . . . . 12 (⊤ → 1 < (abs‘2))
8970, 88, 75georeclim 14821 . . . . . . . . . . 11 (⊤ → seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ (2 / (2 − 1)))
90 2m1e1 11414 . . . . . . . . . . . . 13 (2 − 1) = 1
9190oveq2i 6881 . . . . . . . . . . . 12 (2 / (2 − 1)) = (2 / 1)
92 2cn 11371 . . . . . . . . . . . . 13 2 ∈ ℂ
9392div1i 11034 . . . . . . . . . . . 12 (2 / 1) = 2
9491, 93eqtri 2828 . . . . . . . . . . 11 (2 / (2 − 1)) = 2
9589, 94syl6breq 4885 . . . . . . . . . 10 (⊤ → seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ 2)
961, 61, 81, 95clim2ser 14604 . . . . . . . . 9 (⊤ → seq(0 + 1)( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ (2 − (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0)))
97 seqeq1 13023 . . . . . . . . . 10 ((0 + 1) = 1 → seq(0 + 1)( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) = seq1( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))))
9864, 97ax-mp 5 . . . . . . . . 9 seq(0 + 1)( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) = seq1( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))
99 oveq2 6878 . . . . . . . . . . . . . . . . 17 (𝑛 = 0 → ((1 / 2)↑𝑛) = ((1 / 2)↑0))
100 ovex 6902 . . . . . . . . . . . . . . . . 17 ((1 / 2)↑0) ∈ V
10199, 72, 100fvmpt 6499 . . . . . . . . . . . . . . . 16 (0 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0) = ((1 / 2)↑0))
1022, 101ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0) = ((1 / 2)↑0)
103 halfcn 11510 . . . . . . . . . . . . . . . 16 (1 / 2) ∈ ℂ
104 exp0 13083 . . . . . . . . . . . . . . . 16 ((1 / 2) ∈ ℂ → ((1 / 2)↑0) = 1)
105103, 104ax-mp 5 . . . . . . . . . . . . . . 15 ((1 / 2)↑0) = 1
106102, 105eqtri 2828 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0) = 1
107106a1i 11 . . . . . . . . . . . . 13 (⊤ → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0) = 1)
1084, 107seq1i 13034 . . . . . . . . . . . 12 (⊤ → (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0) = 1)
109108mptru 1645 . . . . . . . . . . 11 (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0) = 1
110109oveq2i 6881 . . . . . . . . . 10 (2 − (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0)) = (2 − 1)
111110, 90eqtri 2828 . . . . . . . . 9 (2 − (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0)) = 1
11296, 98, 1113brtr3g 4877 . . . . . . . 8 (⊤ → seq1( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ 1)
113 nnnn0 11562 . . . . . . . . 9 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
114113, 81sylan2 582 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) ∈ ℂ)
11571oveq2d 6886 . . . . . . . . . . 11 (𝑛 = 𝑘 → (2 · ((1 / 2)↑𝑛)) = (2 · ((1 / 2)↑𝑘)))
116 erelem1.1 . . . . . . . . . . 11 𝐹 = (𝑛 ∈ ℕ ↦ (2 · ((1 / 2)↑𝑛)))
117 ovex 6902 . . . . . . . . . . 11 (2 · ((1 / 2)↑𝑘)) ∈ V
118115, 116, 117fvmpt 6499 . . . . . . . . . 10 (𝑘 ∈ ℕ → (𝐹𝑘) = (2 · ((1 / 2)↑𝑘)))
119118adantl 469 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) = (2 · ((1 / 2)↑𝑘)))
120113, 75sylan2 582 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
121120oveq2d 6886 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ) → (2 · ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘)) = (2 · ((1 / 2)↑𝑘)))
122119, 121eqtr4d 2843 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) = (2 · ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘)))
12359, 60, 70, 112, 114, 122isermulc2 14607 . . . . . . 7 (⊤ → seq1( + , 𝐹) ⇝ (2 · 1))
124 2t1e2 11450 . . . . . . 7 (2 · 1) = 2
125123, 124syl6breq 4885 . . . . . 6 (⊤ → seq1( + , 𝐹) ⇝ 2)
126113, 47sylan2 582 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)
127 remulcl 10302 . . . . . . . . 9 ((2 ∈ ℝ ∧ ((1 / 2)↑𝑘) ∈ ℝ) → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
12883, 79, 127sylancr 577 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
129113, 128sylan2 582 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
130119, 129eqeltrd 2885 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℝ)
131 faclbnd2 13294 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → ((2↑𝑘) / 2) ≤ (!‘𝑘))
132131adantl 469 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((2↑𝑘) / 2) ≤ (!‘𝑘))
133 2nn 11458 . . . . . . . . . . . . . 14 2 ∈ ℕ
134 nnexpcl 13092 . . . . . . . . . . . . . 14 ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
135133, 77, 134sylancr 577 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
136135nnrpd 12080 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℝ+)
137136rphalfcld 12094 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((2↑𝑘) / 2) ∈ ℝ+)
13845nnrpd 12080 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℝ+)
139137, 138lerecd 12101 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (((2↑𝑘) / 2) ≤ (!‘𝑘) ↔ (1 / (!‘𝑘)) ≤ (1 / ((2↑𝑘) / 2))))
140132, 139mpbid 223 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / (!‘𝑘)) ≤ (1 / ((2↑𝑘) / 2)))
141 2cnd 11373 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → 2 ∈ ℂ)
142135nncnd 11317 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℂ)
143135nnne0d 11347 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ≠ 0)
144141, 142, 143divrecd 11085 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 / (2↑𝑘)) = (2 · (1 / (2↑𝑘))))
145 2ne0 11392 . . . . . . . . . . . 12 2 ≠ 0
146 recdiv 11012 . . . . . . . . . . . 12 ((((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (1 / ((2↑𝑘) / 2)) = (2 / (2↑𝑘)))
14792, 145, 146mpanr12 688 . . . . . . . . . . 11 (((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) → (1 / ((2↑𝑘) / 2)) = (2 / (2↑𝑘)))
148142, 143, 147syl2anc 575 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / ((2↑𝑘) / 2)) = (2 / (2↑𝑘)))
149145a1i 11 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → 2 ≠ 0)
150 nn0z 11662 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℤ)
151150adantl 469 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℤ)
152141, 149, 151exprecd 13235 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) = (1 / (2↑𝑘)))
153152oveq2d 6886 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · ((1 / 2)↑𝑘)) = (2 · (1 / (2↑𝑘))))
154144, 148, 1533eqtr4rd 2851 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · ((1 / 2)↑𝑘)) = (1 / ((2↑𝑘) / 2)))
155140, 154breqtrrd 4872 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / (!‘𝑘)) ≤ (2 · ((1 / 2)↑𝑘)))
156113, 155sylan2 582 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (1 / (!‘𝑘)) ≤ (2 · ((1 / 2)↑𝑘)))
157113, 43sylan2 582 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) = (1 / (!‘𝑘)))
158156, 157, 1193brtr4d 4876 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ≤ (𝐹𝑘))
15959, 60, 69, 125, 126, 130, 158iserle 14609 . . . . 5 (⊤ → (e − 1) ≤ 2)
160159mptru 1645 . . . 4 (e − 1) ≤ 2
161 ere 15035 . . . . 5 e ∈ ℝ
162161, 50, 83lesubaddi 10867 . . . 4 ((e − 1) ≤ 2 ↔ e ≤ (2 + 1))
163160, 162mpbi 221 . . 3 e ≤ (2 + 1)
164 df-3 11361 . . 3 3 = (2 + 1)
165163, 164breqtrri 4871 . 2 e ≤ 3
16658, 165pm3.2i 458 1 (2 ≤ e ∧ e ≤ 3)
Colors of variables: wff setvar class
Syntax hints:  wa 384   = wceq 1637  wtru 1638  wcel 2156  wne 2978   class class class wbr 4844  cmpt 4923  cfv 6097  (class class class)co 6870  cc 10215  cr 10216  0cc0 10217  1c1 10218   + caddc 10220   · cmul 10222   < clt 10355  cle 10356  cmin 10547   / cdiv 10965  cn 11301  2c2 11352  3c3 11353  0cn0 11555  cz 11639  seqcseq 13020  cexp 13079  !cfa 13276  abscabs 14193  cli 14434  expce 15008  eceu 15009
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-inf2 8781  ax-cnex 10273  ax-resscn 10274  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-mulcom 10281  ax-addass 10282  ax-mulass 10283  ax-distr 10284  ax-i2m1 10285  ax-1ne0 10286  ax-1rid 10287  ax-rnegex 10288  ax-rrecex 10289  ax-cnre 10290  ax-pre-lttri 10291  ax-pre-lttrn 10292  ax-pre-ltadd 10293  ax-pre-mulgt0 10294  ax-pre-sup 10295  ax-addf 10296  ax-mulf 10297
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-isom 6106  df-riota 6831  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-om 7292  df-1st 7394  df-2nd 7395  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-1o 7792  df-oadd 7796  df-er 7975  df-pm 8091  df-en 8189  df-dom 8190  df-sdom 8191  df-fin 8192  df-sup 8583  df-inf 8584  df-oi 8650  df-card 9044  df-pnf 10357  df-mnf 10358  df-xr 10359  df-ltxr 10360  df-le 10361  df-sub 10549  df-neg 10550  df-div 10966  df-nn 11302  df-2 11360  df-3 11361  df-4 11362  df-n0 11556  df-z 11640  df-uz 11901  df-rp 12043  df-ico 12395  df-fz 12546  df-fzo 12686  df-fl 12813  df-seq 13021  df-exp 13080  df-fac 13277  df-hash 13334  df-shft 14026  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-limsup 14421  df-clim 14438  df-rlim 14439  df-sum 14636  df-ef 15014  df-e 15015
This theorem is referenced by:  egt2lt3  15150
  Copyright terms: Public domain W3C validator