---

Step * 2 1 of Lemma infinity-norm-rneq-real-vec-sep


1. n : ℤ
2. 0 < n
3. ∀x,v:ℝ^n.  (||v||∞ ≠ ||x||∞ ⇒ (∃i:ℕn. (r0 < |(x i) - v i|)))
4. x : ℝ^n + 1
5. v : ℝ^n + 1
6. rmax(||v||∞;|v ((n + 1) - 1)|) ≠ rmax(||x||∞;|x ((n + 1) - 1)|)
7. ||v||∞ ≠ ||x||∞
⊢ ∃i:ℕn + 1. (r0 < |(x i) - v i|)
BY
{ ((Subst' (n + 1) - 1 ~ n -1 THENA Auto) THEN FHyp 3 [-1] THEN Auto THEN ParallelLast) }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}x,v:\mBbbR{}\^{}n.    (||v||\minfty{}  \mneq{}  ||x||\minfty{}  {}\mRightarrow{}  (\mexists{}i:\mBbbN{}n.  (r0  <  |(x  i)  -  v  i|)))
4.  x  :  \mBbbR{}\^{}n  +  1
5.  v  :  \mBbbR{}\^{}n  +  1
6.  rmax(||v||\minfty{};|v  ((n  +  1)  -  1)|)  \mneq{}  rmax(||x||\minfty{};|x  ((n  +  1)  -  1)|)
7.  ||v||\minfty{}  \mneq{}  ||x||\minfty{}
\mvdash{}  \mexists{}i:\mBbbN{}n  +  1.  (r0  <  |(x  i)  -  v  i|)


By

---

Latex:
((Subst'  (n  +  1)  -  1  \msim{}  n  -1  THENA  Auto)  THEN  FHyp  3  [-1]  THEN  Auto  THEN  ParallelLast)

---

Home Index