---

Step * 1 1 1 1 of Lemma divides_iff_rem_zero


1. i : ℕ
2. j : ℕ+
3. j | i
⊢ (i - (i ÷ j) * j) = 0 ∈ ℤ
BY
{ (InstLemma `div_elim` [⌜i⌝;⌜j⌝] THENA Auto) }

1
1. i : ℕ
2. j : ℕ+
3. j | i
4. ∃q:ℕ. (Div(i;j;q) ∧ ((i ÷ j) = q ∈ ℤ))
⊢ (i - (i ÷ j) * j) = 0 ∈ ℤ

---

Latex:

---

Latex:

1.  i  :  \mBbbN{}
2.  j  :  \mBbbN{}\msupplus{}
3.  j  |  i
\mvdash{}  (i  -  (i  \mdiv{}  j)  *  j)  =  0


By

---

Latex:
(InstLemma  `div\_elim`  [\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{}]  THENA  Auto)

---

Home Index