---

Step * of Lemma multiply_functionality_wrt_assoced

∀a,a',b,b':ℤ.  ((a ~ a') ⇒ (b ~ b') ⇒ ((a * b) ~ (a' * b')))
BY
{ (Unfold `assoced` 0 THEN Auto) }

1
1. a : ℤ
2. a' : ℤ
3. b : ℤ
4. b' : ℤ
5. a | a'
6. a' | a
7. b | b'
8. b' | b
⊢ (a * b) | (a' * b')

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

---

Latex:

---

Latex:
\mforall{}a,a',b,b':\mBbbZ{}.    ((a  \msim{}  a')  {}\mRightarrow{}  (b  \msim{}  b')  {}\mRightarrow{}  ((a  *  b)  \msim{}  (a'  *  b')))


By

---

Latex:
(Unfold  `assoced`  0  THEN  Auto)

---

Home Index