---

Step * 1 of Lemma modulus_base


1. m : ℕ+
2. a : ℕm
3. ¬a rem m < 0
4. (0 ≤ (a rem m)) ∧ a rem m < m
⊢ (a rem m) = a ∈ ℕ
BY
{ ((InstLemma `div_bounds_1` [⌜a⌝;⌜m⌝]⋅ THENA Auto) THEN (InstLemma `div_rem_sum` [⌜a⌝;⌜m⌝]⋅ THENA Auto)) }

1
1. m : ℕ+
2. a : ℕm
3. ¬a rem m < 0
4. (0 ≤ (a rem m)) ∧ a rem m < m
5. 0 ≤ (a ÷ m)
6. a = (((a ÷ m) * m) + (a rem m)) ∈ ℤ
⊢ (a rem m) = a ∈ ℕ

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}\msupplus{}
2.  a  :  \mBbbN{}m
3.  \mneg{}a  rem  m  <  0
4.  (0  \mleq{}  (a  rem  m))  \mwedge{}  a  rem  m  <  m
\mvdash{}  (a  rem  m)  =  a


By

---

Latex:
((InstLemma  `div\_bounds\_1`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
  )

---

Home Index