---

Step * 1 1 2 1 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 ∈ ℤ)
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 ∈ ℤ))
BY
{ (ExRepD
   THEN (Evaluate ⌜q' = (q ÷ p) ∈ ℤ⌝⋅ THENA Auto)
   THEN (Evaluate ⌜b' = ((b * q') + a) ∈ ℤ⌝⋅ THENA Auto)
   THEN (Evaluate ⌜x' = (y - x * q') ∈ ℤ⌝⋅ THENA Auto)
   THEN InstConcl [⌜g⌝;⌜b⌝;⌜b'⌝;⌜x'⌝;⌜x⌝]⋅
   THEN Auto)⋅ }

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 : ℕ
8. a : ℤ
9. b : ℤ
10. x : ℤ
11. y : ℤ
12. r = (a * g) ∈ ℤ
13. p = (b * g) ∈ ℤ
14. ((x * a) + (y * b)) = 1 ∈ ℤ
15. q' : ℤ
16. q' = (q ÷ p) ∈ ℤ
17. b' : ℤ
18. b' = ((b * q') + a) ∈ ℤ
19. x' : ℤ
20. x' = (y - x * q') ∈ ℤ
21. p = (b * g) ∈ ℤ
⊢ q = (b' * g) ∈ ℤ

2
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 : ℕ
8. a : ℤ
9. b : ℤ
10. x : ℤ
11. y : ℤ
12. r = (a * g) ∈ ℤ
13. p = (b * g) ∈ ℤ
14. ((x * a) + (y * b)) = 1 ∈ ℤ
15. q' : ℤ
16. q' = (q ÷ p) ∈ ℤ
17. b' : ℤ
18. b' = ((b * q') + a) ∈ ℤ
19. x' : ℤ
20. x' = (y - x * q') ∈ ℤ
21. p = (b * g) ∈ ℤ
22. q = (b' * g) ∈ ℤ
⊢ ((x' * b) + (x * 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)
5.  r  :  \mBbbZ{}
6.  r  =  (q  rem  p)
7.  \mexists{}g:\mBbbN{}.  \mexists{}a,b,x,y:\mBbbZ{}.  ((r  =  (a  *  g))  \mwedge{}  (p  =  (b  *  g))  \mwedge{}  (((x  *  a)  +  (y  *  b))  =  1))
\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:
(ExRepD
  THEN  (Evaluate  \mkleeneopen{}q'  =  (q  \mdiv{}  p)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Evaluate  \mkleeneopen{}b'  =  ((b  *  q')  +  a)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Evaluate  \mkleeneopen{}x'  =  (y  -  x  *  q')\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  InstConcl  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index