---

Step * of Lemma real-vec-sep-implies

No Annotations
∀n:ℕ. ∀a,c:ℝ^n.  (a ≠ c ⇒ (∃i:ℕn. (r0 < |(a i) - c i|)))
BY
{ (Auto THEN Unfold `real-vec-sep` -1 THEN (Assert r0 < d(a;c)^2 BY (BLemma `rnexp-positive` THEN Auto))) }

1
1. n : ℕ
2. a : ℝ^n
3. c : ℝ^n
4. r0 < d(a;c)
5. r0 < d(a;c)^2
⊢ ∃i:ℕn. (r0 < |(a i) - c i|)

---

Latex:

---

Latex:
No  Annotations
\mforall{}n:\mBbbN{}.  \mforall{}a,c:\mBbbR{}\^{}n.    (a  \mneq{}  c  {}\mRightarrow{}  (\mexists{}i:\mBbbN{}n.  (r0  <  |(a  i)  -  c  i|)))


By

---

Latex:
(Auto
  THEN  Unfold  `real-vec-sep`  -1
  THEN  (Assert  r0  <  d(a;c)\^{}2  BY
                          (BLemma  `rnexp-positive`  THEN  Auto)))

---

Home Index