---

Step * 1 1 1 of Lemma eqmod-divides-implies


1. m' : ℤ
2. c1 : ℤ
3. m : ℤ
4. m = (m' * c1) ∈ ℤ
5. a : ℤ
6. b : ℤ
7. c : ℤ
8. (a - b) = (m' * c1 * c) ∈ ℤ
⊢ a ≡ b mod m'
BY
{ (With ⌜c1 * c⌝ (D 0)⋅ THEN Auto')⋅ }

---

Latex:

---

Latex:

1.  m'  :  \mBbbZ{}
2.  c1  :  \mBbbZ{}
3.  m  :  \mBbbZ{}
4.  m  =  (m'  *  c1)
5.  a  :  \mBbbZ{}
6.  b  :  \mBbbZ{}
7.  c  :  \mBbbZ{}
8.  (a  -  b)  =  (m'  *  c1  *  c)
\mvdash{}  a  \mequiv{}  b  mod  m'


By

---

Latex:
(With  \mkleeneopen{}c1  *  c\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto')\mcdot{}

---

Home Index