---

Step * of Lemma rv-pos-angle-implies-separated

∀n:ℕ. ∀a,b,c:ℝ^n.  (rv-pos-angle(n;a;b;c) ⇒ a ≠ c)
BY
{ ((Auto THEN Unfold `real-vec-sep` 0)
   THEN Unfold `rv-pos-angle` -1
   THEN (Assert d(a;c) = d(a - b;c - b) BY
               (RWO  "real-vec-dist-translation" 0 THEN Auto))
   THEN (RWO  "-1" 0 THENA Auto)
   THEN Thin (-1)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜a - b = x ∈ ℝ^n⌝⋅ THENA Auto)
   THEN (GenConcl ⌜c - b = y ∈ ℝ^n⌝⋅ THENA Auto)
   THEN All Thin
   THEN Auto) }

1
1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. |x⋅y| < (||x|| * ||y||)
⊢ r0 < d(x;y)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b,c:\mBbbR{}\^{}n.    (rv-pos-angle(n;a;b;c)  {}\mRightarrow{}  a  \mneq{}  c)


By

---

Latex:
((Auto  THEN  Unfold  `real-vec-sep`  0)
  THEN  Unfold  `rv-pos-angle`  -1
  THEN  (Assert  d(a;c)  =  d(a  -  b;c  -  b)  BY
                          (RWO    "real-vec-dist-translation"  0  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