---

Step * 2 1 of Lemma multiply_functionality_wrt_assoced


1. a : ℤ
2. a' : ℤ
3. b : ℤ
4. b' : ℤ
5. a | a'
6. c1 : ℤ
7. a = (a' * c1) ∈ ℤ
8. b | b'
9. c : ℤ
10. b = (b' * c) ∈ ℤ
11. (a * b) | (a' * b')
⊢ (a' * b') | (a * b)
BY
{ (Eliminate ⌜a⌝⋅ THEN Eliminate ⌜b⌝⋅ THEN With ⌜c * c1⌝ (D 0) THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  a'  :  \mBbbZ{}
3.  b  :  \mBbbZ{}
4.  b'  :  \mBbbZ{}
5.  a  |  a'
6.  c1  :  \mBbbZ{}
7.  a  =  (a'  *  c1)
8.  b  |  b'
9.  c  :  \mBbbZ{}
10.  b  =  (b'  *  c)
11.  (a  *  b)  |  (a'  *  b')
\mvdash{}  (a'  *  b')  |  (a  *  b)


By

---

Latex:
(Eliminate  \mkleeneopen{}a\mkleeneclose{}\mcdot{}  THEN  Eliminate  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THEN  With  \mkleeneopen{}c  *  c1\mkleeneclose{}  (D  0)  THEN  Auto)

---

Home Index