---

Step * of Lemma gcd-reduce-coprime

∀p,q:ℤ.  ∃x,y:ℤ. (((x * p) + (y * q)) = 1 ∈ ℤ) supposing CoPrime(p,q)
BY
{ (InstLemma `gcd-reduce-ext` [] THEN RepeatFor 2 (ParallelLast') THEN (ExRepD THENA 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. [%] : CoPrime(p,q)
⊢ ∃x,y:ℤ. (((x * p) + (y * q)) = 1 ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}p,q:\mBbbZ{}.    \mexists{}x,y:\mBbbZ{}.  (((x  *  p)  +  (y  *  q))  =  1)  supposing  CoPrime(p,q)


By

---

Latex:
(InstLemma  `gcd-reduce-ext`  []  THEN  RepeatFor  2  (ParallelLast')  THEN  (ExRepD  THENA  Auto))

---

Home Index