---

Step * of Lemma rmul-limit

∀x,y:ℕ ⟶ ℝ. ∀a,b:ℝ.  (lim n→∞.x[n] = a ⇒ lim n→∞.y[n] = b ⇒ lim n→∞.x[n] * y[n] = a * b)
BY
{ (Auto THEN All (Unfold `converges-to`) THEN Assert ⌜∃m:ℕ+. ((|b| ≤ r(m)) ∧ (∀n:ℕ. (|x[n]| ≤ r(m))))⌝⋅) }

1
.....assertion..... 
1. x : ℕ ⟶ ℝ
2. y : ℕ ⟶ ℝ
3. a : ℝ
4. b : ℝ
5. ∀k:ℕ+. (∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|x[n] - a| ≤ (r1/r(k)))))})
6. ∀k:ℕ+. (∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|y[n] - b| ≤ (r1/r(k)))))})
⊢ ∃m:ℕ+. ((|b| ≤ r(m)) ∧ (∀n:ℕ. (|x[n]| ≤ r(m))))

2
1. x : ℕ ⟶ ℝ
2. y : ℕ ⟶ ℝ
3. a : ℝ
4. b : ℝ
5. ∀k:ℕ+. (∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|x[n] - a| ≤ (r1/r(k)))))})
6. ∀k:ℕ+. (∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|y[n] - b| ≤ (r1/r(k)))))})
7. ∃m:ℕ+. ((|b| ≤ r(m)) ∧ (∀n:ℕ. (|x[n]| ≤ r(m))))
⊢ ∀k:ℕ+. (∃N:{ℕ| (∀n:ℕ. ((N ≤ n) ⇒ (|(x[n] * y[n]) - a * b| ≤ (r1/r(k)))))})

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}a,b:\mBbbR{}.    (lim  n\mrightarrow{}\minfty{}.x[n]  =  a  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.y[n]  =  b  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.x[n]  *  y[n]  =  a  *  b)


By

---

Latex:
(Auto
  THEN  All  (Unfold  `converges-to`)
  THEN  Assert  \mkleeneopen{}\mexists{}m:\mBbbN{}\msupplus{}.  ((|b|  \mleq{}  r(m))  \mwedge{}  (\mforall{}n:\mBbbN{}.  (|x[n]|  \mleq{}  r(m))))\mkleeneclose{}\mcdot{})

---

Home Index