---

Step * of Lemma divides-add

∀x,y,z:ℤ.  ((z | x) ⇒ (z | y) ⇒ (z | (x + y)))
BY
{ (Unfold `divides` 0 THEN Auto THEN ExRepD THEN InstConcl [⌜c1 + c⌝]⋅ THEN Auto') }

---

Latex:

---

Latex:
\mforall{}x,y,z:\mBbbZ{}.    ((z  |  x)  {}\mRightarrow{}  (z  |  y)  {}\mRightarrow{}  (z  |  (x  +  y)))


By

---

Latex:
(Unfold  `divides`  0  THEN  Auto  THEN  ExRepD  THEN  InstConcl  [\mkleeneopen{}c1  +  c\mkleeneclose{}]\mcdot{}  THEN  Auto')

---

Home Index