---

Step * of Lemma rv-congruent-implies-eq

∀n:ℕ. ∀a,b,c:ℝ^n.  (aa=bc ⇒ req-vec(n;b;c))
BY
{ ((Unfold `rv-congruent` 0 THEN Auto) THEN (Assert d(a;a) = r0 BY Auto) THEN (RWO "-1" (-2) THENA Auto) THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b,c:\mBbbR{}\^{}n.    (aa=bc  {}\mRightarrow{}  req-vec(n;b;c))


By

---

Latex:
((Unfold  `rv-congruent`  0  THEN  Auto)
  THEN  (Assert  d(a;a)  =  r0  BY
                          Auto)
  THEN  (RWO  "-1"  (-2)  THENA  Auto)
  THEN  EAuto  1)

---

Home Index