---

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


1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. ¬rv-pos-angle(n;a;b;c)
6. ¬(a ≠ b ∧ b ≠ c ∧ c ≠ a ∧ (¬a-b-c) ∧ (¬b-c-a) ∧ (¬c-a-b))
7. a ≠ b
8. b ≠ c
9. c ≠ a
10. ¬a-b-c
11. ¬b-c-a
12. ¬c-a-b
⊢ ¬((¬rv-T(n;a;b;c)) ∧ (¬rv-T(n;b;c;a)) ∧ (¬rv-T(n;c;a;b)))
BY
{ (D 6 THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbR{}\^{}n
3.  b  :  \mBbbR{}\^{}n
4.  c  :  \mBbbR{}\^{}n
5.  \mneg{}rv-pos-angle(n;a;b;c)
6.  \mneg{}(a  \mneq{}  b  \mwedge{}  b  \mneq{}  c  \mwedge{}  c  \mneq{}  a  \mwedge{}  (\mneg{}a-b-c)  \mwedge{}  (\mneg{}b-c-a)  \mwedge{}  (\mneg{}c-a-b))
7.  a  \mneq{}  b
8.  b  \mneq{}  c
9.  c  \mneq{}  a
10.  \mneg{}a-b-c
11.  \mneg{}b-c-a
12.  \mneg{}c-a-b
\mvdash{}  \mneg{}((\mneg{}rv-T(n;a;b;c))  \mwedge{}  (\mneg{}rv-T(n;b;c;a))  \mwedge{}  (\mneg{}rv-T(n;c;a;b)))


By

---

Latex:
(D  6  THEN  Auto)

---

Home Index