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

Theorem ege2le3 14864
Description: Lemma for egt2lt3 14978. (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 11760 . . . . . 6 0 = (ℤ‘0)
2 0nn0 11345 . . . . . 6 0 ∈ ℕ0
3 1e0p1 11590 . . . . . 6 1 = (0 + 1)
4 0z 11426 . . . . . . 7 0 ∈ ℤ
5 fveq2 6229 . . . . . . . . . . . 12 (𝑛 = 0 → (!‘𝑛) = (!‘0))
6 fac0 13103 . . . . . . . . . . . 12 (!‘0) = 1
75, 6syl6eq 2701 . . . . . . . . . . 11 (𝑛 = 0 → (!‘𝑛) = 1)
87oveq2d 6706 . . . . . . . . . 10 (𝑛 = 0 → (1 / (!‘𝑛)) = (1 / 1))
9 ax-1cn 10032 . . . . . . . . . . 11 1 ∈ ℂ
109div1i 10791 . . . . . . . . . 10 (1 / 1) = 1
118, 10syl6eq 2701 . . . . . . . . 9 (𝑛 = 0 → (1 / (!‘𝑛)) = 1)
12 erelem1.2 . . . . . . . . 9 𝐺 = (𝑛 ∈ ℕ0 ↦ (1 / (!‘𝑛)))
13 1ex 10073 . . . . . . . . 9 1 ∈ V
1411, 12, 13fvmpt 6321 . . . . . . . 8 (0 ∈ ℕ0 → (𝐺‘0) = 1)
152, 14mp1i 13 . . . . . . 7 (⊤ → (𝐺‘0) = 1)
164, 15seq1i 12855 . . . . . 6 (⊤ → (seq0( + , 𝐺)‘0) = 1)
17 1nn0 11346 . . . . . . 7 1 ∈ ℕ0
18 fveq2 6229 . . . . . . . . . . 11 (𝑛 = 1 → (!‘𝑛) = (!‘1))
19 fac1 13104 . . . . . . . . . . 11 (!‘1) = 1
2018, 19syl6eq 2701 . . . . . . . . . 10 (𝑛 = 1 → (!‘𝑛) = 1)
2120oveq2d 6706 . . . . . . . . 9 (𝑛 = 1 → (1 / (!‘𝑛)) = (1 / 1))
2221, 10syl6eq 2701 . . . . . . . 8 (𝑛 = 1 → (1 / (!‘𝑛)) = 1)
2322, 12, 13fvmpt 6321 . . . . . . 7 (1 ∈ ℕ0 → (𝐺‘1) = 1)
2417, 23mp1i 13 . . . . . 6 (⊤ → (𝐺‘1) = 1)
251, 2, 3, 16, 24seqp1i 12857 . . . . 5 (⊤ → (seq0( + , 𝐺)‘1) = (1 + 1))
26 df-2 11117 . . . . 5 2 = (1 + 1)
2725, 26syl6eqr 2703 . . . 4 (⊤ → (seq0( + , 𝐺)‘1) = 2)
2817a1i 11 . . . . 5 (⊤ → 1 ∈ ℕ0)
29 nn0z 11438 . . . . . . . . . . . 12 (𝑛 ∈ ℕ0𝑛 ∈ ℤ)
30 1exp 12929 . . . . . . . . . . . 12 (𝑛 ∈ ℤ → (1↑𝑛) = 1)
3129, 30syl 17 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 → (1↑𝑛) = 1)
3231oveq1d 6705 . . . . . . . . . 10 (𝑛 ∈ ℕ0 → ((1↑𝑛) / (!‘𝑛)) = (1 / (!‘𝑛)))
3332mpteq2ia 4773 . . . . . . . . 9 (𝑛 ∈ ℕ0 ↦ ((1↑𝑛) / (!‘𝑛))) = (𝑛 ∈ ℕ0 ↦ (1 / (!‘𝑛)))
3412, 33eqtr4i 2676 . . . . . . . 8 𝐺 = (𝑛 ∈ ℕ0 ↦ ((1↑𝑛) / (!‘𝑛)))
3534efcvg 14859 . . . . . . 7 (1 ∈ ℂ → seq0( + , 𝐺) ⇝ (exp‘1))
369, 35mp1i 13 . . . . . 6 (⊤ → seq0( + , 𝐺) ⇝ (exp‘1))
37 df-e 14843 . . . . . 6 e = (exp‘1)
3836, 37syl6breqr 4727 . . . . 5 (⊤ → seq0( + , 𝐺) ⇝ e)
39 fveq2 6229 . . . . . . . . 9 (𝑛 = 𝑘 → (!‘𝑛) = (!‘𝑘))
4039oveq2d 6706 . . . . . . . 8 (𝑛 = 𝑘 → (1 / (!‘𝑛)) = (1 / (!‘𝑘)))
41 ovex 6718 . . . . . . . 8 (1 / (!‘𝑘)) ∈ V
4240, 12, 41fvmpt 6321 . . . . . . 7 (𝑘 ∈ ℕ0 → (𝐺𝑘) = (1 / (!‘𝑘)))
4342adantl 481 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) = (1 / (!‘𝑘)))
44 faccl 13110 . . . . . . . 8 (𝑘 ∈ ℕ0 → (!‘𝑘) ∈ ℕ)
4544adantl 481 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℕ)
4645nnrecred 11104 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / (!‘𝑘)) ∈ ℝ)
4743, 46eqeltrd 2730 . . . . 5 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℝ)
4845nnred 11073 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℝ)
4945nngt0d 11102 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ0) → 0 < (!‘𝑘))
50 1re 10077 . . . . . . . 8 1 ∈ ℝ
51 0le1 10589 . . . . . . . 8 0 ≤ 1
52 divge0 10930 . . . . . . . 8 (((1 ∈ ℝ ∧ 0 ≤ 1) ∧ ((!‘𝑘) ∈ ℝ ∧ 0 < (!‘𝑘))) → 0 ≤ (1 / (!‘𝑘)))
5350, 51, 52mpanl12 718 . . . . . . 7 (((!‘𝑘) ∈ ℝ ∧ 0 < (!‘𝑘)) → 0 ≤ (1 / (!‘𝑘)))
5448, 49, 53syl2anc 694 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ0) → 0 ≤ (1 / (!‘𝑘)))
5554, 43breqtrrd 4713 . . . . 5 ((⊤ ∧ 𝑘 ∈ ℕ0) → 0 ≤ (𝐺𝑘))
561, 28, 38, 47, 55climserle 14437 . . . 4 (⊤ → (seq0( + , 𝐺)‘1) ≤ e)
5727, 56eqbrtrrd 4709 . . 3 (⊤ → 2 ≤ e)
5857trud 1533 . 2 2 ≤ e
59 nnuz 11761 . . . . . 6 ℕ = (ℤ‘1)
60 1zzd 11446 . . . . . 6 (⊤ → 1 ∈ ℤ)
612a1i 11 . . . . . . . 8 (⊤ → 0 ∈ ℕ0)
6247recnd 10106 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ0) → (𝐺𝑘) ∈ ℂ)
631, 61, 62, 38clim2ser 14429 . . . . . . 7 (⊤ → seq(0 + 1)( + , 𝐺) ⇝ (e − (seq0( + , 𝐺)‘0)))
64 0p1e1 11170 . . . . . . . 8 (0 + 1) = 1
65 seqeq1 12844 . . . . . . . 8 ((0 + 1) = 1 → seq(0 + 1)( + , 𝐺) = seq1( + , 𝐺))
6664, 65ax-mp 5 . . . . . . 7 seq(0 + 1)( + , 𝐺) = seq1( + , 𝐺)
6716trud 1533 . . . . . . . 8 (seq0( + , 𝐺)‘0) = 1
6867oveq2i 6701 . . . . . . 7 (e − (seq0( + , 𝐺)‘0)) = (e − 1)
6963, 66, 683brtr3g 4718 . . . . . 6 (⊤ → seq1( + , 𝐺) ⇝ (e − 1))
70 2cnd 11131 . . . . . . . 8 (⊤ → 2 ∈ ℂ)
71 oveq2 6698 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → ((1 / 2)↑𝑛) = ((1 / 2)↑𝑘))
72 eqid 2651 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)) = (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))
73 ovex 6718 . . . . . . . . . . . . 13 ((1 / 2)↑𝑘) ∈ V
7471, 72, 73fvmpt 6321 . . . . . . . . . . . 12 (𝑘 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
7574adantl 481 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
76 halfre 11284 . . . . . . . . . . . . 13 (1 / 2) ∈ ℝ
77 simpr 476 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℕ0)
78 reexpcl 12917 . . . . . . . . . . . . 13 (((1 / 2) ∈ ℝ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) ∈ ℝ)
7976, 77, 78sylancr 696 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) ∈ ℝ)
8079recnd 10106 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) ∈ ℂ)
8175, 80eqeltrd 2730 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) ∈ ℂ)
82 1lt2 11232 . . . . . . . . . . . . . 14 1 < 2
83 2re 11128 . . . . . . . . . . . . . . 15 2 ∈ ℝ
84 0le2 11149 . . . . . . . . . . . . . . 15 0 ≤ 2
85 absid 14080 . . . . . . . . . . . . . . 15 ((2 ∈ ℝ ∧ 0 ≤ 2) → (abs‘2) = 2)
8683, 84, 85mp2an 708 . . . . . . . . . . . . . 14 (abs‘2) = 2
8782, 86breqtrri 4712 . . . . . . . . . . . . 13 1 < (abs‘2)
8887a1i 11 . . . . . . . . . . . 12 (⊤ → 1 < (abs‘2))
8970, 88, 75georeclim 14647 . . . . . . . . . . 11 (⊤ → seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ (2 / (2 − 1)))
90 2m1e1 11173 . . . . . . . . . . . . 13 (2 − 1) = 1
9190oveq2i 6701 . . . . . . . . . . . 12 (2 / (2 − 1)) = (2 / 1)
92 2cn 11129 . . . . . . . . . . . . 13 2 ∈ ℂ
9392div1i 10791 . . . . . . . . . . . 12 (2 / 1) = 2
9491, 93eqtri 2673 . . . . . . . . . . 11 (2 / (2 − 1)) = 2
9589, 94syl6breq 4726 . . . . . . . . . 10 (⊤ → seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ 2)
961, 61, 81, 95clim2ser 14429 . . . . . . . . 9 (⊤ → seq(0 + 1)( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ (2 − (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0)))
97 seqeq1 12844 . . . . . . . . . 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 6698 . . . . . . . . . . . . . . . . 17 (𝑛 = 0 → ((1 / 2)↑𝑛) = ((1 / 2)↑0))
100 ovex 6718 . . . . . . . . . . . . . . . . 17 ((1 / 2)↑0) ∈ V
10199, 72, 100fvmpt 6321 . . . . . . . . . . . . . . . 16 (0 ∈ ℕ0 → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0) = ((1 / 2)↑0))
1022, 101ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0) = ((1 / 2)↑0)
103 halfcn 11285 . . . . . . . . . . . . . . . 16 (1 / 2) ∈ ℂ
104 exp0 12904 . . . . . . . . . . . . . . . 16 ((1 / 2) ∈ ℂ → ((1 / 2)↑0) = 1)
105103, 104ax-mp 5 . . . . . . . . . . . . . . 15 ((1 / 2)↑0) = 1
106102, 105eqtri 2673 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0) = 1
107106a1i 11 . . . . . . . . . . . . 13 (⊤ → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘0) = 1)
1084, 107seq1i 12855 . . . . . . . . . . . 12 (⊤ → (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0) = 1)
109108trud 1533 . . . . . . . . . . 11 (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0) = 1
110109oveq2i 6701 . . . . . . . . . 10 (2 − (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0)) = (2 − 1)
111110, 90eqtri 2673 . . . . . . . . 9 (2 − (seq0( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛)))‘0)) = 1
11296, 98, 1113brtr3g 4718 . . . . . . . 8 (⊤ → seq1( + , (𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))) ⇝ 1)
113 nnnn0 11337 . . . . . . . . 9 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
114113, 81sylan2 490 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) ∈ ℂ)
11571oveq2d 6706 . . . . . . . . . . 11 (𝑛 = 𝑘 → (2 · ((1 / 2)↑𝑛)) = (2 · ((1 / 2)↑𝑘)))
116 erelem1.1 . . . . . . . . . . 11 𝐹 = (𝑛 ∈ ℕ ↦ (2 · ((1 / 2)↑𝑛)))
117 ovex 6718 . . . . . . . . . . 11 (2 · ((1 / 2)↑𝑘)) ∈ V
118115, 116, 117fvmpt 6321 . . . . . . . . . 10 (𝑘 ∈ ℕ → (𝐹𝑘) = (2 · ((1 / 2)↑𝑘)))
119118adantl 481 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) = (2 · ((1 / 2)↑𝑘)))
120113, 75sylan2 490 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ) → ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘) = ((1 / 2)↑𝑘))
121120oveq2d 6706 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ) → (2 · ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘)) = (2 · ((1 / 2)↑𝑘)))
122119, 121eqtr4d 2688 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) = (2 · ((𝑛 ∈ ℕ0 ↦ ((1 / 2)↑𝑛))‘𝑘)))
12359, 60, 70, 112, 114, 122isermulc2 14432 . . . . . . 7 (⊤ → seq1( + , 𝐹) ⇝ (2 · 1))
124 2t1e2 11214 . . . . . . 7 (2 · 1) = 2
125123, 124syl6breq 4726 . . . . . 6 (⊤ → seq1( + , 𝐹) ⇝ 2)
126113, 47sylan2 490 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)
127 remulcl 10059 . . . . . . . . 9 ((2 ∈ ℝ ∧ ((1 / 2)↑𝑘) ∈ ℝ) → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
12883, 79, 127sylancr 696 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
129113, 128sylan2 490 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (2 · ((1 / 2)↑𝑘)) ∈ ℝ)
130119, 129eqeltrd 2730 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹𝑘) ∈ ℝ)
131 faclbnd2 13118 . . . . . . . . . . 11 (𝑘 ∈ ℕ0 → ((2↑𝑘) / 2) ≤ (!‘𝑘))
132131adantl 481 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((2↑𝑘) / 2) ≤ (!‘𝑘))
133 2nn 11223 . . . . . . . . . . . . . 14 2 ∈ ℕ
134 nnexpcl 12913 . . . . . . . . . . . . . 14 ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
135133, 77, 134sylancr 696 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℕ)
136135nnrpd 11908 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℝ+)
137136rphalfcld 11922 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((2↑𝑘) / 2) ∈ ℝ+)
13845nnrpd 11908 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → (!‘𝑘) ∈ ℝ+)
139137, 138lerecd 11929 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (((2↑𝑘) / 2) ≤ (!‘𝑘) ↔ (1 / (!‘𝑘)) ≤ (1 / ((2↑𝑘) / 2))))
140132, 139mpbid 222 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / (!‘𝑘)) ≤ (1 / ((2↑𝑘) / 2)))
141 2cnd 11131 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → 2 ∈ ℂ)
142135nncnd 11074 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ∈ ℂ)
143135nnne0d 11103 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2↑𝑘) ≠ 0)
144141, 142, 143divrecd 10842 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 / (2↑𝑘)) = (2 · (1 / (2↑𝑘))))
145 2ne0 11151 . . . . . . . . . . . 12 2 ≠ 0
146 recdiv 10769 . . . . . . . . . . . 12 ((((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (1 / ((2↑𝑘) / 2)) = (2 / (2↑𝑘)))
14792, 145, 146mpanr12 721 . . . . . . . . . . 11 (((2↑𝑘) ∈ ℂ ∧ (2↑𝑘) ≠ 0) → (1 / ((2↑𝑘) / 2)) = (2 / (2↑𝑘)))
148142, 143, 147syl2anc 694 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / ((2↑𝑘) / 2)) = (2 / (2↑𝑘)))
149145a1i 11 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → 2 ≠ 0)
150 nn0z 11438 . . . . . . . . . . . . 13 (𝑘 ∈ ℕ0𝑘 ∈ ℤ)
151150adantl 481 . . . . . . . . . . . 12 ((⊤ ∧ 𝑘 ∈ ℕ0) → 𝑘 ∈ ℤ)
152141, 149, 151exprecd 13056 . . . . . . . . . . 11 ((⊤ ∧ 𝑘 ∈ ℕ0) → ((1 / 2)↑𝑘) = (1 / (2↑𝑘)))
153152oveq2d 6706 . . . . . . . . . 10 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · ((1 / 2)↑𝑘)) = (2 · (1 / (2↑𝑘))))
154144, 148, 1533eqtr4rd 2696 . . . . . . . . 9 ((⊤ ∧ 𝑘 ∈ ℕ0) → (2 · ((1 / 2)↑𝑘)) = (1 / ((2↑𝑘) / 2)))
155140, 154breqtrrd 4713 . . . . . . . 8 ((⊤ ∧ 𝑘 ∈ ℕ0) → (1 / (!‘𝑘)) ≤ (2 · ((1 / 2)↑𝑘)))
156113, 155sylan2 490 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (1 / (!‘𝑘)) ≤ (2 · ((1 / 2)↑𝑘)))
157113, 43sylan2 490 . . . . . . 7 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) = (1 / (!‘𝑘)))
158156, 157, 1193brtr4d 4717 . . . . . 6 ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺𝑘) ≤ (𝐹𝑘))
15959, 60, 69, 125, 126, 130, 158iserle 14434 . . . . 5 (⊤ → (e − 1) ≤ 2)
160159trud 1533 . . . 4 (e − 1) ≤ 2
161 ere 14863 . . . . 5 e ∈ ℝ
162161, 50, 83lesubaddi 10624 . . . 4 ((e − 1) ≤ 2 ↔ e ≤ (2 + 1))
163160, 162mpbi 220 . . 3 e ≤ (2 + 1)
164 df-3 11118 . . 3 3 = (2 + 1)
165163, 164breqtrri 4712 . 2 e ≤ 3
16658, 165pm3.2i 470 1 (2 ≤ e ∧ e ≤ 3)
Colors of variables: wff setvar class
Syntax hints:  wa 383   = wceq 1523  wtru 1524  wcel 2030  wne 2823   class class class wbr 4685  cmpt 4762  cfv 5926  (class class class)co 6690  cc 9972  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   < clt 10112  cle 10113  cmin 10304   / cdiv 10722  cn 11058  2c2 11108  3c3 11109  0cn0 11330  cz 11415  seqcseq 12841  cexp 12900  !cfa 13100  abscabs 14018  cli 14259  expce 14836  eceu 14837
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-oadd 7609  df-er 7787  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-ico 12219  df-fz 12365  df-fzo 12505  df-fl 12633  df-seq 12842  df-exp 12901  df-fac 13101  df-hash 13158  df-shft 13851  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-sum 14461  df-ef 14842  df-e 14843
This theorem is referenced by:  egt2lt3  14978
  Copyright terms: Public domain W3C validator