---

Step * 1 1 1 1 of Lemma rv-pos-angle-not-between


1. n : ℕ
2. t : ℝ
3. v : ℝ^n
⊢ ¬(|t - r1*v⋅t*v| < (||t - r1*v|| * ||t*v||))
BY
{ ((RWW "real-vec-norm-mul dot-product-linearity2.1 dot-product-linearity2.2" 0 THENA Auto)
   THEN (RWW "rabs-rmul real-vec-norm-squared<" 0 THENA Auto)
   ) }

1
1. n : ℕ
2. t : ℝ
3. v : ℝ^n
⊢ ¬((|t| * |t - r1| * |||v||^2|) < ((|t - r1| * ||v||) * |t| * ||v||))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  t  :  \mBbbR{}
3.  v  :  \mBbbR{}\^{}n
\mvdash{}  \mneg{}(|t  -  r1*v\mcdot{}t*v|  <  (||t  -  r1*v||  *  ||t*v||))


By

---

Latex:
((RWW  "real-vec-norm-mul  dot-product-linearity2.1  dot-product-linearity2.2"  0  THENA  Auto)
  THEN  (RWW  "rabs-rmul  real-vec-norm-squared<"  0  THENA  Auto)
  )

---

Home Index