---

Step * 1 1 1 1 of Lemma real-vec-dist-identity


1. n : ℕ
2. v : ℝ^n
⊢ (v⋅v = r0) ⇒ req-vec(n;v;λi.r0)
BY
{ (Auto THEN RepUR ``dot-product`` -1 THEN (D 0 THEN Auto) THEN (BLemma `not-rneq` THENA Auto) THEN Reduce 0) }

1
1. n : ℕ
2. v : ℝ^n
3. Σ{(v i) * (v i) | 0≤i≤n - 1} = r0
4. i : ℕn
⊢ ¬v i ≠ r0

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  v  :  \mBbbR{}\^{}n
\mvdash{}  (v\mcdot{}v  =  r0)  {}\mRightarrow{}  req-vec(n;v;\mlambda{}i.r0)


By

---

Latex:
(Auto
  THEN  RepUR  ``dot-product``  -1
  THEN  (D  0  THEN  Auto)
  THEN  (BLemma  `not-rneq`  THENA  Auto)
  THEN  Reduce  0)

---

Home Index