---

Step * 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. [%] : CoPrime(p,q)
⊢ ∃x,y:ℤ. (((x * p) + (y * q)) = 1 ∈ ℤ)
BY
{ (Assert ⌜g = 1 ∈ ℤ⌝⋅ THENM (Eliminate ⌜p⌝⋅ THEN Eliminate ⌜q⌝⋅ THEN Eliminate ⌜g⌝⋅ THEN Auto)) }

1
.....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 ∈ ℤ

---

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.  [\%]  :  CoPrime(p,q)
\mvdash{}  \mexists{}x,y:\mBbbZ{}.  (((x  *  p)  +  (y  *  q))  =  1)


By

---

Latex:
(Assert  \mkleeneopen{}g  =  1\mkleeneclose{}\mcdot{}  THENM  (Eliminate  \mkleeneopen{}p\mkleeneclose{}\mcdot{}  THEN  Eliminate  \mkleeneopen{}q\mkleeneclose{}\mcdot{}  THEN  Eliminate  \mkleeneopen{}g\mkleeneclose{}\mcdot{}  THEN  Auto))

---

Home Index