---

Step * 1 1 of Lemma multiply_functionality_wrt_eqmod


1. m : ℤ
2. a : ℤ
3. a' : ℤ
4. b : ℤ
5. b' : ℤ
6. m | ((a - a') * b)
7. m | ((b - b') * a')
⊢ m | ((a * b) - a' * b')
BY
{ (FwdThruLemma `divisor_of_sum` [6;7] THENA Auto) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(FwdThruLemma  `divisor\_of\_sum`  [6;7]  THENA  Auto)

---

Home Index