---

Step * 1 1 1 of Lemma gcd-reduce-coprime


1. p : ℤ
2. q : ℤ
3. g : ℕ
4. a : ℤ
5. b : ℤ
6. x : ℤ
7. y : ℤ
8. p = (a * g) ∈ ℤ
9. q = (b * g) ∈ ℤ
10. ((x * a) + (y * b)) = 1 ∈ ℤ
11. 1 | p
12. 1 | q
13. ∀z:ℤ. (((z | p) ∧ (z | q)) ⇒ (z | 1))
⊢ g | p
BY
{ (D 0 With ⌜a⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  p  :  \mBbbZ{}
2.  q  :  \mBbbZ{}
3.  g  :  \mBbbN{}
4.  a  :  \mBbbZ{}
5.  b  :  \mBbbZ{}
6.  x  :  \mBbbZ{}
7.  y  :  \mBbbZ{}
8.  p  =  (a  *  g)
9.  q  =  (b  *  g)
10.  ((x  *  a)  +  (y  *  b))  =  1
11.  1  |  p
12.  1  |  q
13.  \mforall{}z:\mBbbZ{}.  (((z  |  p)  \mwedge{}  (z  |  q))  {}\mRightarrow{}  (z  |  1))
\mvdash{}  g  |  p


By

---

Latex:
(D  0  With  \mkleeneopen{}a\mkleeneclose{}    THEN  Auto)

---

Home Index