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