---

Step * of Lemma not-rv-pos-angle

∀n:ℕ. ∀a,b,c:ℝ^n.
  ((r0 < d(a;b)) ⇒ (r0 < d(c;b)) ⇒ (¬rv-pos-angle(n;a;b;c)) ⇒ (∃t:ℝ. ((r0 < |t|) ∧ req-vec(n;c;b + t*a - b))))
BY
{ (Auto
   THEN All (Unfold `real-vec-dist`)
   THEN Unfold `rv-pos-angle` -1
   THEN (FLemma `not-rless` [-1] THENA Auto)
   THEN Thin (-2)
   THEN ((InstLemma `Cauchy-Schwarz` [⌜n⌝;⌜a - b⌝;⌜c - b⌝]⋅ THENA Auto)
         THEN (Assert |a - b⋅c - b| = (||a - b|| * ||c - b||) BY
                     (BLemma `rleq_antisymmetry` THEN Auto))
         )
   THEN (InstLemma `Cauchy-Schwarz-equality` [⌜n⌝;⌜c - b⌝;⌜a - b⌝]⋅
         THENA (Auto THEN RWO "rmul_comm dot-product-comm" 0 THEN Auto)
         )) }

1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. r0 < ||a - b||
6. r0 < ||c - b||
7. (||a - b|| * ||c - b||) ≤ |a - b⋅c - b|
8. |a - b⋅c - b| ≤ (||a - b|| * ||c - b||)
9. |a - b⋅c - b| = (||a - b|| * ||c - b||)
10. req-vec(n;c - b;(c - b⋅a - b/||a - b||^2)*a - b)
⊢ ∃t:ℝ. ((r0 < |t|) ∧ req-vec(n;c;b + t*a - b))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b,c:\mBbbR{}\^{}n.
    ((r0  <  d(a;b))
    {}\mRightarrow{}  (r0  <  d(c;b))
    {}\mRightarrow{}  (\mneg{}rv-pos-angle(n;a;b;c))
    {}\mRightarrow{}  (\mexists{}t:\mBbbR{}.  ((r0  <  |t|)  \mwedge{}  req-vec(n;c;b  +  t*a  -  b))))


By

---

Latex:
(Auto
  THEN  All  (Unfold  `real-vec-dist`)
  THEN  Unfold  `rv-pos-angle`  -1
  THEN  (FLemma  `not-rless`  [-1]  THENA  Auto)
  THEN  Thin  (-2)
  THEN  ((InstLemma  `Cauchy-Schwarz`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}a  -  b\mkleeneclose{};\mkleeneopen{}c  -  b\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (Assert  |a  -  b\mcdot{}c  -  b|  =  (||a  -  b||  *  ||c  -  b||)  BY
                                      (BLemma  `rleq\_antisymmetry`  THEN  Auto))
              )
  THEN  (InstLemma  `Cauchy-Schwarz-equality`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}c  -  b\mkleeneclose{};\mkleeneopen{}a  -  b\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  RWO  "rmul\_comm  dot-product-comm"  0  THEN  Auto)
              ))

---

Home Index