Step * of Lemma rv-T-dist

n:ℕ. ∀a,b,c:ℝ^n.  (rv-T(n;a;b;c)  (d(a;c) (d(a;b) d(b;c))))
BY
(Unfold `rv-T` 0
   THEN Auto
   THEN (BLemma `not-rneq` THENM 0)
   THEN Auto
   THEN (DistinguishCases ⌜a ≠ c⌝⋅ THENA Auto)
   THEN ThinTrivial) }

1
1. : ℕ
2. : ℝ^n
3. : ℝ^n
4. : ℝ^n
5. a ≠ c)  b ≠ c)
6. d(a;c) ≠ d(a;b) d(b;c)
7. a ≠ c
8. real-vec-be(n;a;b;c)
⊢ False

2
1. : ℕ
2. : ℝ^n
3. : ℝ^n
4. : ℝ^n
5. d(a;c) ≠ d(a;b) d(b;c)
6. ¬a ≠ c
7. ¬b ≠ c
⊢ False


Latex:


Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b,c:\mBbbR{}\^{}n.    (rv-T(n;a;b;c)  {}\mRightarrow{}  (d(a;c)  =  (d(a;b)  +  d(b;c))))


By


Latex:
(Unfold  `rv-T`  0
  THEN  Auto
  THEN  (BLemma  `not-rneq`  THENM  D  0)
  THEN  Auto
  THEN  (DistinguishCases  \mkleeneopen{}a  \mneq{}  c\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinTrivial)




Home Index