---

Step * 2 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'
BY
{ (Subst' a' = (a + (m * c)) ∈ ℤ 0 THEN Auto') }

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

---

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'


By

---

Latex:
(Subst'  a'  =  (a  +  (m  *  c))  0  THEN  Auto')

---

Home Index