Step
*
of Lemma
rminus-limit
∀x:ℕ ⟶ ℝ. ∀a:ℝ.  (lim n→∞.x[n] = a 
⇒ lim n→∞.-(x[n]) = -(a))
BY
{ (Auto THEN All (Unfold `converges-to`) THEN RepeatFor 2 (ParallelLast)) }
1
.....set predicate..... 
1. x : ℕ ⟶ ℝ@i
2. a : ℝ@i
3. ∀k:ℕ+. (∃N:{ℕ| (∀n:ℕ. ((N ≤ n) 
⇒ (|x[n] - a| ≤ (r1/r(k)))))})@i
4. k : ℕ+@i
5. N : ℕ
6. ∀n:ℕ. ((N ≤ n) 
⇒ (|x[n] - a| ≤ (r1/r(k))))
⊢ ∀n:ℕ. ((N ≤ n) 
⇒ (|-(x[n]) - -(a)| ≤ (r1/r(k))))
Latex:
Latex:
\mforall{}x:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}a:\mBbbR{}.    (lim  n\mrightarrow{}\minfty{}.x[n]  =  a  {}\mRightarrow{}  lim  n\mrightarrow{}\minfty{}.-(x[n])  =  -(a))
By
Latex:
(Auto  THEN  All  (Unfold  `converges-to`)  THEN  RepeatFor  2  (ParallelLast))
Home
Index