---

Step * 2 of Lemma rv-pos-angle_functionality


1. n : ℕ
2. a1 : ℝ^n
3. b1 : ℝ^n
4. c1 : ℝ^n
5. a2 : ℝ^n
6. b2 : ℝ^n
7. c2 : ℝ^n
8. req-vec(n;a1;a2)
9. req-vec(n;b1;b2)
10. req-vec(n;c1;c2)
11. |a2 - b2⋅c2 - b2| < (||a2 - b2|| * ||c2 - b2||)
⊢ |a1 - b1⋅c1 - b1| < (||a1 - b1|| * ||c1 - b1||)
BY
{ (RWO "-4 -3 -2" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a1  :  \mBbbR{}\^{}n
3.  b1  :  \mBbbR{}\^{}n
4.  c1  :  \mBbbR{}\^{}n
5.  a2  :  \mBbbR{}\^{}n
6.  b2  :  \mBbbR{}\^{}n
7.  c2  :  \mBbbR{}\^{}n
8.  req-vec(n;a1;a2)
9.  req-vec(n;b1;b2)
10.  req-vec(n;c1;c2)
11.  |a2  -  b2\mcdot{}c2  -  b2|  <  (||a2  -  b2||  *  ||c2  -  b2||)
\mvdash{}  |a1  -  b1\mcdot{}c1  -  b1|  <  (||a1  -  b1||  *  ||c1  -  b1||)


By

---

Latex:
(RWO  "-4  -3  -2"  0  THEN  Auto)

---

Home Index