---

Step * of Lemma modulus_base_neg

∀[m:ℕ+]. ∀[a:{-m..0-}].  (a mod m ~ m + a)
BY
{ (Auto
   THEN Unfold `modulus` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (InstLemma `rem_bounds_2` [⌜a⌝;⌜m⌝]⋅ THENA Auto)
   THEN (InstLemma `div_bounds_2` [⌜a⌝;⌜m⌝]⋅ THENA Auto)
   THEN (InstLemma `div_rem_sum` [⌜a⌝;⌜m⌝]⋅ THENA Auto)
   THEN (Subst' |m| ~ m 0 THENA Auto)) }

1
1. m : ℕ+
2. a : {-m..0-}
3. (0 ≥ (a rem m) ) ∧ ((a rem m) > (-m))
4. (a ÷ m) ≤ 0
5. a = (((a ÷ m) * m) + (a rem m)) ∈ ℤ
⊢ if (a rem m) < (0)  then m + (a rem m)  else (a rem m) = (m + a) ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[m:\mBbbN{}\msupplus{}].  \mforall{}[a:\{-m..0\msupminus{}\}].    (a  mod  m  \msim{}  m  +  a)


By

---

Latex:
(Auto
  THEN  Unfold  `modulus`  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (InstLemma  `rem\_bounds\_2`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `div\_bounds\_2`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Subst'  |m|  \msim{}  m  0  THENA  Auto))

---

Home Index