---

Step * of Lemma absval-imax-difference

∀[a,b,c,d:ℤ].  (|imax(a;b) - imax(c;d)| ≤ imax(|a - c|;|b - d|))
BY
{ TACTIC:(Auto THEN (RWO  "imax_unfold" 0 THENA Auto) THEN Repeat (AutoSplit)) }

1
1. a : ℤ
2. b : ℤ
3. c : ℤ
4. d : ℤ
5. ¬(c ≤ d)
6. a ≤ b
7. |a - c| ≤ |b - d|
⊢ |b - c| ≤ |b - d|

2
1. a : ℤ
2. b : ℤ
3. c : ℤ
4. d : ℤ
5. ¬(|a - c| ≤ |b - d|)
6. ¬(c ≤ d)
7. a ≤ b
⊢ |b - c| ≤ |a - c|

3
1. a : ℤ
2. b : ℤ
3. ¬(a ≤ b)
4. c : ℤ
5. d : ℤ
6. c ≤ d
7. |a - c| ≤ |b - d|
⊢ |a - d| ≤ |b - d|

4
1. a : ℤ
2. b : ℤ
3. ¬(a ≤ b)
4. c : ℤ
5. d : ℤ
6. ¬(|a - c| ≤ |b - d|)
7. c ≤ d
⊢ |a - d| ≤ |a - c|

---

Latex:

---

Latex:
\mforall{}[a,b,c,d:\mBbbZ{}].    (|imax(a;b)  -  imax(c;d)|  \mleq{}  imax(|a  -  c|;|b  -  d|))


By

---

Latex:
TACTIC:(Auto  THEN  (RWO    "imax\_unfold"  0  THENA  Auto)  THEN  Repeat  (AutoSplit))

---

Home Index