---

Step * of Lemma gcd-reduce-prime

∀p,q:ℤ.  ∃x,y:ℤ. (((x * p) + (y * q)) = 1 ∈ ℤ) supposing prime(p) ∧ (¬(p | q))
BY
{ (InstLemma `gcd-reduce-coprime` [] THEN RepeatFor 3 (ParallelLast')) }

1
.....antecedent..... 
1. p : ℤ
2. q : ℤ
3. prime(p) ∧ (¬(p | q))
⊢ CoPrime(p,q)

---

Latex:

---

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


By

---

Latex:
(InstLemma  `gcd-reduce-coprime`  []  THEN  RepeatFor  3  (ParallelLast'))

---

Home Index