---

Step * of Lemma r2-left-pos-angle

∀a,b,c:ℝ^2.  (r2-left(a;b;c) ⇒ rv-pos-angle(2;a;b;c))
BY
{ ((RepUR ``r2-left rv-pos-angle`` 0 THEN Auto)
   THEN (RWO "r2-det-is-dot-product" (-1) THENA Auto)
   THEN MoveToConcl (-1)
   THEN (GenConclTerms Auto [⌜a - b⌝;⌜c - b⌝]⋅ THEN All Thin)
   THEN RenameVar `a' 1
   THEN RenameVar `b' 2) }

1
1. a : ℝ^2
2. b : ℝ^2
⊢ (r0 < a⋅λi.if (i =z 0) then -(b 1) else b 0 fi ) ⇒ (|a⋅b| < (||a|| * ||b||))

---

Latex:

---

Latex:
\mforall{}a,b,c:\mBbbR{}\^{}2.    (r2-left(a;b;c)  {}\mRightarrow{}  rv-pos-angle(2;a;b;c))


By

---

Latex:
((RepUR  ``r2-left  rv-pos-angle``  0  THEN  Auto)
  THEN  (RWO  "r2-det-is-dot-product"  (-1)  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerms  Auto  [\mkleeneopen{}a  -  b\mkleeneclose{};\mkleeneopen{}c  -  b\mkleeneclose{}]\mcdot{}  THEN  All  Thin)
  THEN  RenameVar  `a'  1
  THEN  RenameVar  `b'  2)

---

Home Index