---

Step * 1 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')
8. m | (((a - a') * b) + ((b - b') * a'))
⊢ m | ((a * b) - a' * b')
BY
{ (All (RW IntNormC) THEN Auto) }

---

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')
8.  m  |  (((a  -  a')  *  b)  +  ((b  -  b')  *  a'))
\mvdash{}  m  |  ((a  *  b)  -  a'  *  b')


By

---

Latex:
(All  (RW  IntNormC)  THEN  Auto)

---

Home Index