---

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


1. n : ℕ
2. t : ℝ
3. v : ℝ^n
⊢ ¬((|t| * |t - r1| * |||v||^2|) < ((|t - r1| * ||v||) * |t| * ||v||))
BY
{ (GenConclTerms Auto [⌜|t|⌝;⌜|t - r1|⌝]⋅ THEN (RWO "rabs-of-nonneg" 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||^2) < ((v2 * ||v||) * v1 * ||v||))

---

Latex:

---

Latex:

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


By

---

Latex:
(GenConclTerms  Auto  [\mkleeneopen{}|t|\mkleeneclose{};\mkleeneopen{}|t  -  r1|\mkleeneclose{}]\mcdot{}  THEN  (RWO  "rabs-of-nonneg"  0  THENA  Auto))

---

Home Index