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