---

Step * of Lemma rv-pos-angle_functionality

∀n:ℕ. ∀a1,b1,c1,a2,b2,c2:ℝ^n.
  (req-vec(n;a1;a2) ⇒ req-vec(n;b1;b2) ⇒ req-vec(n;c1;c2) ⇒ {rv-pos-angle(n;a1;b1;c1) ⇐⇒ rv-pos-angle(n;a2;b2;c2)})
BY
{ (Auto THEN (D 0 THEN Auto) THEN ParallelLast) }

1
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. |a1 - b1⋅c1 - b1| < (||a1 - b1|| * ||c1 - b1||)
⊢ |a2 - b2⋅c2 - b2| < (||a2 - b2|| * ||c2 - b2||)

2
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||)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a1,b1,c1,a2,b2,c2:\mBbbR{}\^{}n.
    (req-vec(n;a1;a2)
    {}\mRightarrow{}  req-vec(n;b1;b2)
    {}\mRightarrow{}  req-vec(n;c1;c2)
    {}\mRightarrow{}  \{rv-pos-angle(n;a1;b1;c1)  \mLeftarrow{}{}\mRightarrow{}  rv-pos-angle(n;a2;b2;c2)\})


By

---

Latex:
(Auto  THEN  (D  0  THEN  Auto)  THEN  ParallelLast)

---

Home Index