---

Step * 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)) ∈ ℤ
⊢ (a rem m) = a ∈ ℕ
BY
{ (Decide (a ÷ m) = 0 ∈ ℤ 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)) ∈ ℤ
7. (a ÷ m) = 0 ∈ ℤ
⊢ (a rem m) = a ∈ ℕ

2
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 ∈ ℤ)
⊢ (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
5.  0  \mleq{}  (a  \mdiv{}  m)
6.  a  =  (((a  \mdiv{}  m)  *  m)  +  (a  rem  m))
\mvdash{}  (a  rem  m)  =  a


By

---

Latex:
(Decide  (a  \mdiv{}  m)  =  0  THENA  Auto)

---

Home Index