---

Step * 2 of Lemma divides-mul


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index