---

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

∀[n:ℕ]. ∀[a,b,c:ℝ^n].  ¬a-b-c supposing rv-pos-angle(n;a;b;c)
BY
{ (Auto THEN Unfold `rv-pos-angle` -1 THEN (D 0 THENA Auto) THEN D -1 THEN RepeatFor 2 (D -2)) }

1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. |a - b⋅c - b| < (||a - b|| * ||c - b||)
6. t : ℝ
7. t ∈ (r0, r1)
8. req-vec(n;b;t*a + r1 - t*c)
9. a ≠ c
⊢ False

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[a,b,c:\mBbbR{}\^{}n].    \mneg{}a-b-c  supposing  rv-pos-angle(n;a;b;c)


By

---

Latex:
(Auto  THEN  Unfold  `rv-pos-angle`  -1  THEN  (D  0  THENA  Auto)  THEN  D  -1  THEN  RepeatFor  2  (D  -2))

---

Home Index