---

Step * of Lemma rem_bounds_absval

∀b:ℤ-o. ∀a:ℤ.  |a rem b| < |b|
BY
{ (Auto THEN (RWO "absval_unfold2" 0 THENA Auto) THEN RepeatFor 2 (AutoSplit) THEN (All (RWO "not-lt-2") THENA Auto)) }

1
1. b : ℤ-o
2. a : ℤ
3. 0 < a rem b
4. 0 < b
⊢ a rem b < b

2
1. b : ℤ-o
2. b ≤ 0
3. a : ℤ
4. 0 < a rem b
⊢ a rem b < -b

3
1. b : ℤ-o
2. a : ℤ
3. (a rem b) ≤ 0
4. 0 < b
⊢ -(a rem b) < b

4
1. b : ℤ-o
2. b ≤ 0
3. a : ℤ
4. (a rem b) ≤ 0
⊢ -(a rem b) < -b

---

Latex:

---

Latex:
\mforall{}b:\mBbbZ{}\msupminus{}\msupzero{}.  \mforall{}a:\mBbbZ{}.    |a  rem  b|  <  |b|


By

---

Latex:
(Auto
  THEN  (RWO  "absval\_unfold2"  0  THENA  Auto)
  THEN  RepeatFor  2  (AutoSplit)
  THEN  (All  (RWO  "not-lt-2")  THENA  Auto))

---

Home Index