---

Step * 1 1 2 1 1 of Lemma modulus_base


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)) ∈ ℤ
7. ¬((a ÷ m) = 0 ∈ ℤ)
8. 1 ≤ (a ÷ m)
9. (m * 1) ≤ (m * (a ÷ m))
⊢ (a rem m) = a ∈ ℕ
BY
{ (ExRepD THEN (Add ⌜a rem m⌝ (-1)⋅ THEN Add ⌜m⌝ 4 ⋅) THEN All(RW IntNormC) THEN Auto) }

---

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
5.  0  \mleq{}  (a  \mdiv{}  m)
6.  a  =  (((a  \mdiv{}  m)  *  m)  +  (a  rem  m))
7.  \mneg{}((a  \mdiv{}  m)  =  0)
8.  1  \mleq{}  (a  \mdiv{}  m)
9.  (m  *  1)  \mleq{}  (m  *  (a  \mdiv{}  m))
\mvdash{}  (a  rem  m)  =  a


By

---

Latex:
(ExRepD  THEN  (Add  \mkleeneopen{}a  rem  m\mkleeneclose{}  (-1)\mcdot{}  THEN  Add  \mkleeneopen{}m\mkleeneclose{}  4  \mcdot{})  THEN  All(RW  IntNormC)  THEN  Auto)

---

Home Index