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 D 0)
   THEN Auto
   THEN (DistinguishCases ⌜a ≠ c⌝⋅ THENA Auto)
   THEN ThinTrivial) }
1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^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. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^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