---

Step * 1 of Lemma multiply_functionality_wrt_eqmod


1. m : ℤ
2. a : ℤ
3. a' : ℤ
4. b : ℤ
5. b' : ℤ
6. m | (a - a')
7. m | (b - b')
⊢ m | ((a * b) - a' * b')
BY
{ (((Using [`c',⌜b⌝] (FwdThruLemma `divisor_of_mul` [6]) THENM Using [`c',⌜a'⌝] (FwdThruLemma `divisor_of_mul` [7]))
   THENM OnHyps [7;6] Thin
   )
   THENA Auto
   ) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
(((Using  [`c',\mkleeneopen{}b\mkleeneclose{}]  (FwdThruLemma  `divisor\_of\_mul`  [6])
    THENM  Using  [`c',\mkleeneopen{}a'\mkleeneclose{}]  (FwdThruLemma  `divisor\_of\_mul`  [7])
    )
  THENM  OnHyps  [7;6]  Thin
  )
  THENA  Auto
  )

---

Home Index