Step
*
2
of Lemma
absval-imin-difference
1. a : ℤ
2. b : ℤ
3. c : ℤ
4. d : ℤ
5. ¬(|a - c| ≤ |b - d|)
6. ¬(c ≤ d)
7. a ≤ b
⊢ |a - d| ≤ |a - c|
BY
{ TACTIC:(MoveToConcl (-3) THEN All (RWO "absval_unfold") THEN Repeat (AutoSplit) THEN Auto) }
Latex:
Latex:
1. a : \mBbbZ{}
2. b : \mBbbZ{}
3. c : \mBbbZ{}
4. d : \mBbbZ{}
5. \mneg{}(|a - c| \mleq{} |b - d|)
6. \mneg{}(c \mleq{} d)
7. a \mleq{} b
\mvdash{} |a - d| \mleq{} |a - c|
By
Latex:
TACTIC:(MoveToConcl (-3) THEN All (RWO "absval\_unfold") THEN Repeat (AutoSplit) THEN Auto)
Home
Index