---

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


1. n : ℕ
2. t : ℝ
3. v : ℝ^n
4. v1 : ℝ
5. |t| = v1 ∈ ℝ
6. v2 : ℝ
7. |t - r1| = v2 ∈ ℝ
⊢ ¬((v1 * v2 * ||v||^2) < ((v2 * ||v||) * v1 * ||v||))
BY
{ (RWW "real-vec-norm-squared< rnexp2" 0 THENA Auto) }

1
1. n : ℕ
2. t : ℝ
3. v : ℝ^n
4. v1 : ℝ
5. |t| = v1 ∈ ℝ
6. v2 : ℝ
7. |t - r1| = v2 ∈ ℝ
⊢ ¬((v1 * v2 * ||v|| * ||v||) < ((v2 * ||v||) * v1 * ||v||))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  t  :  \mBbbR{}
3.  v  :  \mBbbR{}\^{}n
4.  v1  :  \mBbbR{}
5.  |t|  =  v1
6.  v2  :  \mBbbR{}
7.  |t  -  r1|  =  v2
\mvdash{}  \mneg{}((v1  *  v2  *  ||v||\^{}2)  <  ((v2  *  ||v||)  *  v1  *  ||v||))


By

---

Latex:
(RWW  "real-vec-norm-squared<  rnexp2"  0  THENA  Auto)

---

Home Index