---

Step * 2 1 of Lemma gcd_functionality_wrt_eqmod


1. a : ℤ
2. a' : ℤ
3. m : ℤ
4. c : ℤ
5. (a' - a) = (m * c) ∈ ℤ
6. y1 : ℤ
7. y1 | a'
8. y1 | m
9. ∀z:ℤ. (((z | a') ∧ (z | m)) ⇒ (z | y1))
10. y : ℤ
11. y | a
12. y | m
13. ∀z:ℤ. (((z | a) ∧ (z | m)) ⇒ (z | y))
⊢ y | (a + (m * c))
BY
{ ((BLemma `divisor_of_sum` THENM Try (BLemma `divisor_of_mul`)) THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  a'  :  \mBbbZ{}
3.  m  :  \mBbbZ{}
4.  c  :  \mBbbZ{}
5.  (a'  -  a)  =  (m  *  c)
6.  y1  :  \mBbbZ{}
7.  y1  |  a'
8.  y1  |  m
9.  \mforall{}z:\mBbbZ{}.  (((z  |  a')  \mwedge{}  (z  |  m))  {}\mRightarrow{}  (z  |  y1))
10.  y  :  \mBbbZ{}
11.  y  |  a
12.  y  |  m
13.  \mforall{}z:\mBbbZ{}.  (((z  |  a)  \mwedge{}  (z  |  m))  {}\mRightarrow{}  (z  |  y))
\mvdash{}  y  |  (a  +  (m  *  c))


By

---

Latex:
((BLemma  `divisor\_of\_sum`  THENM  Try  (BLemma  `divisor\_of\_mul`))  THEN  Auto)

---

Home Index