---

Step * 1 1 of Lemma eqmod_fun


1. m : ℤ
2. a : ℤ
3. a' : ℤ
4. b : ℤ
5. b' : ℤ
6. b ≡ b' mod m
7. a ≡ b mod m
8. a' ≡ a mod m
⊢ a' ≡ b' mod m
BY
{ ((FwdThruLemma `eqmod_transitivity` [8;7] THENM FwdThruLemma `eqmod_transitivity` [6;9]) THEN Auto) }

---

Latex:

---

Latex:

1.  m  :  \mBbbZ{}
2.  a  :  \mBbbZ{}
3.  a'  :  \mBbbZ{}
4.  b  :  \mBbbZ{}
5.  b'  :  \mBbbZ{}
6.  b  \mequiv{}  b'  mod  m
7.  a  \mequiv{}  b  mod  m
8.  a'  \mequiv{}  a  mod  m
\mvdash{}  a'  \mequiv{}  b'  mod  m


By

---

Latex:
((FwdThruLemma  `eqmod\_transitivity`  [8;7]  THENM  FwdThruLemma  `eqmod\_transitivity`  [6;9])  THEN  Auto)

---

Home Index