---

Step * of Lemma exists-rneq-iff

∀n:ℕ. ∀a,b:ℕn ⟶ ℝ.  (∃i:ℕn. a[i] ≠ b[i] ⇐⇒ r0 < Σ{|a[i] - b[i]| | 0≤i≤n - 1})
BY
{ ((UnivCD THENA Auto)
   THEN (RWO "rsum-of-nonneg-positive-iff" 0 THENA Auto)
   THEN (Subst' (n - 1) + 1 ~ n 0 THENA Auto)) }

1
1. n : ℕ
2. a : ℕn ⟶ ℝ
3. b : ℕn ⟶ ℝ
⊢ ∃i:ℕn. a[i] ≠ b[i] ⇐⇒ ∃i:ℕn. (r0 < |a[i] - b[i]|)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b:\mBbbN{}n  {}\mrightarrow{}  \mBbbR{}.    (\mexists{}i:\mBbbN{}n.  a[i]  \mneq{}  b[i]  \mLeftarrow{}{}\mRightarrow{}  r0  <  \mSigma{}\{|a[i]  -  b[i]|  |  0\mleq{}i\mleq{}n  -  1\})


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RWO  "rsum-of-nonneg-positive-iff"  0  THENA  Auto)
  THEN  (Subst'  (n  -  1)  +  1  \msim{}  n  0  THENA  Auto))

---

Home Index