---

Step * of Lemma implies-rv-pos-angle

∀n:ℕ. ∀a,b,c,a':ℝ^n.  (a-b-a' ⇒ ab=a'b ⇒ ab=cb ⇒ c ≠ a ⇒ c ≠ a' ⇒ rv-pos-angle(n;a;b;c))
BY
{ (Auto THEN Unfold `rv-pos-angle` 0 THEN BLemma `rv-pos-angle-lemma` THEN Auto) }

1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. a' : ℝ^n
6. a-b-a'
7. ab=a'b
8. ab=cb
9. c ≠ a
10. c ≠ a'
⊢ r0 < d(a - b;c - b)

2
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. a' : ℝ^n
6. a-b-a'
7. ab=a'b
8. ab=cb
9. c ≠ a
10. c ≠ a'
⊢ r0 < d(r(-1)*a - b;c - b)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b,c,a':\mBbbR{}\^{}n.    (a-b-a'  {}\mRightarrow{}  ab=a'b  {}\mRightarrow{}  ab=cb  {}\mRightarrow{}  c  \mneq{}  a  {}\mRightarrow{}  c  \mneq{}  a'  {}\mRightarrow{}  rv-pos-angle(n;a;b;c))


By

---

Latex:
(Auto  THEN  Unfold  `rv-pos-angle`  0  THEN  BLemma  `rv-pos-angle-lemma`  THEN  Auto)

---

Home Index