Step
*
of Lemma
modulus-equal-iff-eqmod
∀x,y:ℤ. ∀m:ℕ+.  ((x mod m) = (y mod m) ∈ ℤ 
⇐⇒ x ≡ y mod m)
BY
{ ((InstLemma `modulus-equal` [] THEN Fold `eqmod` (-1)) THEN Auto) }
Latex:
Latex:
\mforall{}x,y:\mBbbZ{}.  \mforall{}m:\mBbbN{}\msupplus{}.    ((x  mod  m)  =  (y  mod  m)  \mLeftarrow{}{}\mRightarrow{}  x  \mequiv{}  y  mod  m)
By
Latex:
((InstLemma  `modulus-equal`  []  THEN  Fold  `eqmod`  (-1))  THEN  Auto)
Home
Index