---

Step * 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))
⊢ ¬((¬rv-T(n;a;b;c)) ∧ (¬rv-T(n;b;c;a)) ∧ (¬rv-T(n;c;a;b)))
BY
{ (((DistinguishCases ⌜a ≠ b⌝⋅ THENA Auto)
    THENL [Id; ((D 0 THENA Auto) THEN ExRepD THEN D -3 THEN BLemma `rv-T-iff` THEN Auto)]
   )
   THEN ((DistinguishCases ⌜b ≠ c⌝⋅ THENA Auto)
         THENL [Id; ((D 0 THENA Auto) THEN ExRepD THEN D -2 THEN BLemma `rv-T-iff` THEN Auto)]
   )
   THEN ((DistinguishCases ⌜c ≠ a⌝⋅ THENA Auto)
         THENL [Id; ((D 0 THENA Auto) THEN ExRepD THEN D -1 THEN BLemma `rv-T-iff` THEN Auto)]
   )) }

1
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
⊢ ¬((¬rv-T(n;a;b;c)) ∧ (¬rv-T(n;b;c;a)) ∧ (¬rv-T(n;c;a;b)))

---

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))
\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:
(((DistinguishCases  \mkleeneopen{}a  \mneq{}  b\mkleeneclose{}\mcdot{}  THENA  Auto)
    THENL  [Id;  ((D  0  THENA  Auto)  THEN  ExRepD  THEN  D  -3  THEN  BLemma  `rv-T-iff`  THEN  Auto)]
  )
  THEN  ((DistinguishCases  \mkleeneopen{}b  \mneq{}  c\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [Id;  ((D  0  THENA  Auto)  THEN  ExRepD  THEN  D  -2  THEN  BLemma  `rv-T-iff`  THEN  Auto)]
  )
  THEN  ((DistinguishCases  \mkleeneopen{}c  \mneq{}  a\mkleeneclose{}\mcdot{}  THENA  Auto)
              THENL  [Id;  ((D  0  THENA  Auto)  THEN  ExRepD  THEN  D  -1  THEN  BLemma  `rv-T-iff`  THEN  Auto)]
  ))

---

Home Index