---

Step * 1 1 3 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))
14. g | 1
15. g ≤ 1
⊢ g = 1 ∈ ℤ
BY
{ (CaseNat 0 `g' THEN Auto) }

1
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))
14. g | 1
15. g ≤ 1
16. g = 0 ∈ ℤ
⊢ 0 = 1 ∈ ℤ

---

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))
14.  g  |  1
15.  g  \mleq{}  1
\mvdash{}  g  =  1


By

---

Latex:
(CaseNat  0  `g'  THEN  Auto)

---

Home Index