---

Step * 1 of Lemma eqmod-divides-implies


1. m : ℤ
2. m' : ℤ
3. m' | m
4. a : ℤ
5. b : ℤ
6. a ≡ b mod m
⊢ a ≡ b mod m'
BY
{ (D -1 THEN D 3) }

1
1. m : ℤ
2. m' : ℤ
3. c1 : ℤ
4. m = (m' * c1) ∈ ℤ
5. a : ℤ
6. b : ℤ
7. c : ℤ
8. (a - b) = (m * c) ∈ ℤ
⊢ a ≡ b mod m'

---

Latex:

---

Latex:

1.  m  :  \mBbbZ{}
2.  m'  :  \mBbbZ{}
3.  m'  |  m
4.  a  :  \mBbbZ{}
5.  b  :  \mBbbZ{}
6.  a  \mequiv{}  b  mod  m
\mvdash{}  a  \mequiv{}  b  mod  m'


By

---

Latex:
(D  -1  THEN  D  3)

---

Home Index