---

Step * of Lemma eqmod_cancellation

∀m,x,a,b:ℤ.  (CoPrime(x,m) ⇒ ((x * a) ≡ (x * b) mod m) ⇒ (a ≡ b mod m))
BY
{ TACTIC:(Auto THEN Unfold `eqmod` -1 THEN Unfold `eqmod` 0) }

1
1. m : ℤ
2. x : ℤ
3. a : ℤ
4. b : ℤ
5. CoPrime(x,m)
6. m | ((x * a) - x * b)
⊢ m | (a - b)

---

Latex:

---

Latex:
\mforall{}m,x,a,b:\mBbbZ{}.    (CoPrime(x,m)  {}\mRightarrow{}  ((x  *  a)  \mequiv{}  (x  *  b)  mod  m)  {}\mRightarrow{}  (a  \mequiv{}  b  mod  m))


By

---

Latex:
TACTIC:(Auto  THEN  Unfold  `eqmod`  -1  THEN  Unfold  `eqmod`  0)

---

Home Index