---

Step * 1 1 of Lemma eqmod-divides-implies


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'
BY
{ (Eliminate ⌜m⌝⋅ THEN (RWO "mul_assoc<" (-1) THENA Auto)) }

1
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'

---

Latex:

---

Latex:

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


By

---

Latex:
(Eliminate  \mkleeneopen{}m\mkleeneclose{}\mcdot{}  THEN  (RWO  "mul\_assoc<"  (-1)  THENA  Auto))

---

Home Index