---

Step * 1 of Lemma eqmod_transitivity


1. m : ℤ
2. a : ℤ
3. b : ℤ
4. c : ℤ
5. m | (a - b)
6. m | (b - c)
⊢ m | (a - c)
BY
{ (FwdThruLemma `divisor_of_sum` [5;6] THEN Auto) }

---

Latex:

---

Latex:

1.  m  :  \mBbbZ{}
2.  a  :  \mBbbZ{}
3.  b  :  \mBbbZ{}
4.  c  :  \mBbbZ{}
5.  m  |  (a  -  b)
6.  m  |  (b  -  c)
\mvdash{}  m  |  (a  -  c)


By

---

Latex:
(FwdThruLemma  `divisor\_of\_sum`  [5;6]  THEN  Auto)

---

Home Index