---

Step * 1 1 2 of Lemma gcd-reduce


1. p : ℕ
2. ∀p1:ℕp. ∀q:ℕ.  ∃g:ℕ. ∃a,b,x,y:ℤ. ((p1 = (a * g) ∈ ℤ) ∧ (q = (b * g) ∈ ℤ) ∧ (((x * a) + (y * b)) = 1 ∈ ℤ))
3. q : ℕ
4. ¬(p = 0 ∈ ℤ)
⊢ ∃g:ℕ. ∃a,b,x,y:ℤ. ((p = (a * g) ∈ ℤ) ∧ (q = (b * g) ∈ ℤ) ∧ (((x * a) + (y * b)) = 1 ∈ ℤ))
BY
{ (((Evaluate ⌜r = (q rem p) ∈ ℤ⌝⋅ THENM InstHyp [⌜r⌝] 2⋅)
    THENA (Auto' THEN InstLemma `rem_bounds_1` [⌜q⌝;⌜p⌝]⋅ THEN Auto')
    )
   THEN InstHyp [⌜p⌝] (-1)⋅
   THEN Auto
   THEN Thin (-2)) }

1
1. p : ℕ
2. ∀p1:ℕp. ∀q:ℕ.  ∃g:ℕ. ∃a,b,x,y:ℤ. ((p1 = (a * g) ∈ ℤ) ∧ (q = (b * g) ∈ ℤ) ∧ (((x * a) + (y * b)) = 1 ∈ ℤ))
3. q : ℕ
4. ¬(p = 0 ∈ ℤ)
5. r : ℤ
6. r = (q rem p) ∈ ℤ
7. ∃g:ℕ. ∃a,b,x,y:ℤ. ((r = (a * g) ∈ ℤ) ∧ (p = (b * g) ∈ ℤ) ∧ (((x * a) + (y * b)) = 1 ∈ ℤ))
⊢ ∃g:ℕ. ∃a,b,x,y:ℤ. ((p = (a * g) ∈ ℤ) ∧ (q = (b * g) ∈ ℤ) ∧ (((x * a) + (y * b)) = 1 ∈ ℤ))

---

Latex:

---

Latex:

1.  p  :  \mBbbN{}
2.  \mforall{}p1:\mBbbN{}p.  \mforall{}q:\mBbbN{}.    \mexists{}g:\mBbbN{}.  \mexists{}a,b,x,y:\mBbbZ{}.  ((p1  =  (a  *  g))  \mwedge{}  (q  =  (b  *  g))  \mwedge{}  (((x  *  a)  +  (y  *  b))  =  1))
3.  q  :  \mBbbN{}
4.  \mneg{}(p  =  0)
\mvdash{}  \mexists{}g:\mBbbN{}.  \mexists{}a,b,x,y:\mBbbZ{}.  ((p  =  (a  *  g))  \mwedge{}  (q  =  (b  *  g))  \mwedge{}  (((x  *  a)  +  (y  *  b))  =  1))


By

---

Latex:
(((Evaluate  \mkleeneopen{}r  =  (q  rem  p)\mkleeneclose{}\mcdot{}  THENM  InstHyp  [\mkleeneopen{}r\mkleeneclose{}]  2\mcdot{})
    THENA  (Auto'  THEN  InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THEN  Auto')
    )
  THEN  InstHyp  [\mkleeneopen{}p\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Auto
  THEN  Thin  (-2))

---

Home Index