---

Step * of Lemma r2-det-nonzero

∀p,q,r:ℝ^2.  (rv-pos-angle(2;p;q;r) ⇒ |pqr| ≠ r0)
BY
{ (Auto THEN RepUR ``rv-pos-angle`` -1) }

1
1. p : ℝ^2
2. q : ℝ^2
3. r : ℝ^2
4. |p - q⋅r - q| < (||p - q|| * ||r - q||)
⊢ |pqr| ≠ r0

---

Latex:

---

Latex:
\mforall{}p,q,r:\mBbbR{}\^{}2.    (rv-pos-angle(2;p;q;r)  {}\mRightarrow{}  |pqr|  \mneq{}  r0)


By

---

Latex:
(Auto  THEN  RepUR  ``rv-pos-angle``  -1)

---

Home Index