---

Step * 1 of Lemma divides-mul


1. x : ℤ@i
2. y : ℤ@i
3. z : ℤ@i
4. c : ℤ@i
5. x = (z * c) ∈ ℤ@i
⊢ ∃c@0:ℤ. (((z * c) * y) = (z * c@0) ∈ ℤ)
BY
{ (InstConcl [⌜y * c⌝]⋅ THEN Auto')⋅ }

---

Latex:

---

Latex:

1.  x  :  \mBbbZ{}@i
2.  y  :  \mBbbZ{}@i
3.  z  :  \mBbbZ{}@i
4.  c  :  \mBbbZ{}@i
5.  x  =  (z  *  c)@i
\mvdash{}  \mexists{}c@0:\mBbbZ{}.  (((z  *  c)  *  y)  =  (z  *  c@0))


By

---

Latex:
(InstConcl  [\mkleeneopen{}y  *  c\mkleeneclose{}]\mcdot{}  THEN  Auto')\mcdot{}

---

Home Index