---

Step * 1 1 of Lemma gcd-reduce-coprime

.....assertion..... 
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. CoPrime(p,q)
⊢ g = 1 ∈ ℤ
BY
{ (RepeatFor 2 (D -1) THEN InstHyp [⌜g⌝] (-1)⋅ 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))
⊢ g | p

2
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 | p
⊢ g | q

3
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
⊢ g = 1 ∈ ℤ

---

Latex:

---

Latex:
.....assertion..... 
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.  CoPrime(p,q)
\mvdash{}  g  =  1


By

---

Latex:
(RepeatFor  2  (D  -1)  THEN  InstHyp  [\mkleeneopen{}g\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)

---

Home Index