---

Step * of Lemma rv-T-partially-implies-rv-T'

∀n:ℕ+. ∀a,b,c:ℝ^n.  ((a ≠ c ∨ (¬a ≠ c)) ⇒ rv-T(n;a;b;c) ⇒ rv-T'(n;a;b;c))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN SplitOrHyps
   THEN D 6
   THEN ThinTrivial
   THEN Try (((FLemma `not-real-vec-sep-iff-eq` [-1] THENA Auto) THEN RWO  "-1" 0 THEN Auto))
   THEN RepeatFor 2 (D -1)
   THEN Reduce -2
   THEN (RWO  "-1" 0 THENA Auto)
   THEN ThinVar `b'
   THEN D -4
   THEN RepeatFor 2 (D -5)
   THEN (RWO "-5" 0 THENA Auto)
   THEN ThinVar `a'
   THEN D -3
   THEN RepeatFor 2 (D -4)
   THEN (RWO "-4" 0 THENA Auto)
   THEN ThinVar `c'
   THEN D 0
   THEN Auto) }

1
1. n : ℕ+
2. x : ℝ^n
3. y : ℝ^n
4. t1 : ℝ
5. t1 ∈ (r0, r1)
6. x ≠ y
7. t2 : ℝ
8. t2 ∈ (r0, r1)
9. x ≠ y
10. t : ℝ
11. r0 ≤ t
12. t ≤ r1
⊢ x-t*t1*x + r1 - t1*y + r1 - t*t2*x + r1 - t2*y-y

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}a,b,c:\mBbbR{}\^{}n.    ((a  \mneq{}  c  \mvee{}  (\mneg{}a  \mneq{}  c))  {}\mRightarrow{}  rv-T(n;a;b;c)  {}\mRightarrow{}  rv-T'(n;a;b;c))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  SplitOrHyps
  THEN  D  6
  THEN  ThinTrivial
  THEN  Try  (((FLemma  `not-real-vec-sep-iff-eq`  [-1]  THENA  Auto)  THEN  RWO    "-1"  0  THEN  Auto))
  THEN  RepeatFor  2  (D  -1)
  THEN  Reduce  -2
  THEN  (RWO    "-1"  0  THENA  Auto)
  THEN  ThinVar  `b'
  THEN  D  -4
  THEN  RepeatFor  2  (D  -5)
  THEN  (RWO  "-5"  0  THENA  Auto)
  THEN  ThinVar  `a'
  THEN  D  -3
  THEN  RepeatFor  2  (D  -4)
  THEN  (RWO  "-4"  0  THENA  Auto)
  THEN  ThinVar  `c'
  THEN  D  0
  THEN  Auto)

---

Home Index