---

Step * of Lemma r2-det-add

∀[p,q,r,t:ℝ^2].  (|p + tqr| = (|pqr| + |tqr| + (((q 1) * (r 0)) - (q 0) * (r 1))))
BY
{ (Auto THEN RepUR ``r2-det real-vec-add real-vec-mul`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[p,q,r,t:\mBbbR{}\^{}2].    (|p  +  tqr|  =  (|pqr|  +  |tqr|  +  (((q  1)  *  (r  0))  -  (q  0)  *  (r  1))))


By

---

Latex:
(Auto  THEN  RepUR  ``r2-det  real-vec-add  real-vec-mul``  0  THEN  Auto)

---

Home Index