---

Step * of Lemma rem_base_case_z

No Annotations
∀[a:ℤ]. ∀[b:ℤ-o].  (a rem b) = a ∈ ℤ supposing |a| < |b|
BY
{ ((UnivCD THENA Auto) THEN MoveToConcl (-1) THEN RWO "absval_unfold" 0 THEN Repeat (AutoSplit) THEN Auto') }

1
1. a : ℤ
2. b : ℤ-o
3. ¬-1 < b
4. -1 < a
5. a < -b
⊢ (a rem b) = a ∈ ℤ

2
1. a : ℤ
2. ¬-1 < a
3. b : ℤ-o
4. -1 < b
5. -a < b
⊢ (a rem b) = a ∈ ℤ

3
1. a : ℤ
2. ¬-1 < a
3. b : ℤ-o
4. ¬-1 < b
5. -a < -b
⊢ (a rem b) = a ∈ ℤ

---

Latex:

---

Latex:
No  Annotations
\mforall{}[a:\mBbbZ{}].  \mforall{}[b:\mBbbZ{}\msupminus{}\msupzero{}].    (a  rem  b)  =  a  supposing  |a|  <  |b|


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  RWO  "absval\_unfold"  0
  THEN  Repeat  (AutoSplit)
  THEN  Auto')

---

Home Index