---

Step * 2 of Lemma multiply_functionality_wrt_assoced


1. a : ℤ
2. a' : ℤ
3. b : ℤ
4. b' : ℤ
5. a | a'
6. a' | a
7. b | b'
8. b' | b
9. (a * b) | (a' * b')
⊢ (a' * b') | (a * b)
BY
{ (D 8 THEN D 6) }

1
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)

---

Latex:

---

Latex:

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


By

---

Latex:
(D  8  THEN  D  6)

---

Home Index