---

Step * of Lemma rinv-limit

∀x:ℕ ⟶ ℝ. ∀a:ℝ.  (lim n→∞.x[n] = a ⇒ (∀n:ℕ. x[n] ≠ r0) ⇒ a ≠ r0 ⇒ lim n→∞.(r1/x[n]) = (r1/a))
BY
{ (Auto THEN All (Unfold `converges-to`) THEN Assert ⌜∀n:ℕ. ((|a| - |x[n] - a|) ≤ |x[n]|)⌝⋅) }

1
.....assertion..... 
1. x : ℕ ⟶ ℝ
2. a : ℝ
3. ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|x[n] - a| ≤ (r1/r(k)))))])
4. ∀n:ℕ. x[n] ≠ r0
5. a ≠ r0
⊢ ∀n:ℕ. ((|a| - |x[n] - a|) ≤ |x[n]|)

2
1. x : ℕ ⟶ ℝ
2. a : ℝ
3. ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|x[n] - a| ≤ (r1/r(k)))))])
4. ∀n:ℕ. x[n] ≠ r0
5. a ≠ r0
6. ∀n:ℕ. ((|a| - |x[n] - a|) ≤ |x[n]|)
⊢ ∀k:ℕ+. (∃N:ℕ [(∀n:ℕ. ((N ≤ n) ⇒ (|(r1/x[n]) - (r1/a)| ≤ (r1/r(k)))))])

---

Latex:

---

Latex:
\mforall{}x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}a:\mBbbR{}.    (lim  n\mrightarrow{}\minfty{}.x[n]  =  a  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  x[n]  \mneq{}  r0)  {}\mRightarrow{}  a  \mneq{}  r0  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.(r1/x[n])  =  (r1/a))


By

---

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

---

Home Index