---

Step * of Lemma r2-left-sep

∀a,b,c:ℝ^2.  (r2-left(a;b;c) ⇒ b ≠ c)
BY
{ (Auto
   THEN (Assert r0 < (||a - b|| * ||c - b||) BY
               (FLemma `r2-left-pos-angle` [-1]
                THEN Auto
                THEN Unfold `rv-pos-angle` -1
                THEN (Assert r0 ≤ |a - b⋅c - b| BY
                            Auto)
                THEN RWO "-1<" (-2)
                THEN Auto))
   THEN (RWO "rmul-is-positive" (-1) THENA Auto)
   THEN D -1
   THEN Auto
   THEN Fold `real-vec-dist` (-1)
   THEN Try ((Fold `real-vec-sep` (-1) THEN BLemma `real-vec-sep-symmetry` THEN Auto))
   THEN (Assert r0 ≤ d(c;b) BY
               Auto)
   THEN RelRST
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Assert  r0  <  (||a  -  b||  *  ||c  -  b||)  BY
                          (FLemma  `r2-left-pos-angle`  [-1]
                            THEN  Auto
                            THEN  Unfold  `rv-pos-angle`  -1
                            THEN  (Assert  r0  \mleq{}  |a  -  b\mcdot{}c  -  b|  BY
                                                    Auto)
                            THEN  RWO  "-1<"  (-2)
                            THEN  Auto))
  THEN  (RWO  "rmul-is-positive"  (-1)  THENA  Auto)
  THEN  D  -1
  THEN  Auto
  THEN  Fold  `real-vec-dist`  (-1)
  THEN  Try  ((Fold  `real-vec-sep`  (-1)  THEN  BLemma  `real-vec-sep-symmetry`  THEN  Auto))
  THEN  (Assert  r0  \mleq{}  d(c;b)  BY
                          Auto)
  THEN  RelRST
  THEN  Auto)

---

Home Index