Step * of Lemma eqmod_transitivity

m,a,b,c:ℤ.  ((a ≡ mod m)  (b ≡ mod m)  (a ≡ mod m))
BY
(Unfold `eqmod` THEN Auto) }

1
1. : ℤ
2. : ℤ
3. : ℤ
4. : ℤ
5. (a b)
6. (b c)
⊢ (a c)


Latex:


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


By


Latex:
(Unfold  `eqmod`  0  THEN  Auto)




Home Index