---

Step * 1 of Lemma exists-rneq-iff


1. n : ℕ
2. a : ℕn ⟶ ℝ
3. b : ℕn ⟶ ℝ
⊢ ∃i:ℕn. a[i] ≠ b[i] ⇐⇒ ∃i:ℕn. (r0 < |a[i] - b[i]|)
BY
{ ((Auto THEN ParallelLast) THEN EAuto 1) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbR{}
3.  b  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbR{}
\mvdash{}  \mexists{}i:\mBbbN{}n.  a[i]  \mneq{}  b[i]  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}n.  (r0  <  |a[i]  -  b[i]|)


By

---

Latex:
((Auto  THEN  ParallelLast)  THEN  EAuto  1)

---

Home Index