---

Step * of Lemma ip-triangle-implies-separated

∀rv:InnerProductSpace. ∀a,b,c:Point.  (Δ(a;b;c) ⇒ a # c)
BY
{ (Auto
   THEN Unfold `ip-triangle` -1
   THEN (BLemma `rv-sep-iff` THENA Auto)
   THEN (BLemma `rv-norm-positive-iff` THENA Auto)
   THEN ((Assert a - c ≡ a - b - c - b BY (RealVecEqual THEN Auto)) THEN (RWO "-1" 0 THENA Auto))
   THEN Thin (-1)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜a - b = x ∈ Point⌝⋅ THENA Auto)
   THEN (GenConcl ⌜c - b = y ∈ Point⌝⋅ THENA Auto)
   THEN All Thin
   THEN Auto) }

1
1. rv : InnerProductSpace
2. x : Point
3. y : Point
4. |x ⋅ y| < (||x|| * ||y||)
⊢ r0 < ||x - y||

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}a,b,c:Point.    (\mDelta{}(a;b;c)  {}\mRightarrow{}  a  \#  c)


By

---

Latex:
(Auto
  THEN  Unfold  `ip-triangle`  -1
  THEN  (BLemma  `rv-sep-iff`  THENA  Auto)
  THEN  (BLemma  `rv-norm-positive-iff`  THENA  Auto)
  THEN  ((Assert  a  -  c  \mequiv{}  a  -  b  -  c  -  b  BY  (RealVecEqual  THEN  Auto))  THEN  (RWO  "-1"  0  THENA  Auto))
  THEN  Thin  (-1)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}a  -  b  =  x\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}c  -  b  =  y\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Auto)

---

Home Index