---

Step * 1 1 2 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 ∈ ℤ)
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 ∈ ℤ
BY
{ ((HypSubst' (-3) 0 THEN Auto) THEN HypSubst' (-5) 0 THEN Auto) }

---

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.  g  :  \mBbbN{}
8.  a  :  \mBbbZ{}
9.  b  :  \mBbbZ{}
10.  x  :  \mBbbZ{}
11.  y  :  \mBbbZ{}
12.  r  =  (a  *  g)
13.  p  =  (b  *  g)
14.  ((x  *  a)  +  (y  *  b))  =  1
15.  q'  :  \mBbbZ{}
16.  q'  =  (q  \mdiv{}  p)
17.  b'  :  \mBbbZ{}
18.  b'  =  ((b  *  q')  +  a)
19.  x'  :  \mBbbZ{}
20.  x'  =  (y  -  x  *  q')
21.  p  =  (b  *  g)
22.  q  =  (b'  *  g)
\mvdash{}  ((x'  *  b)  +  (x  *  b'))  =  1


By

---

Latex:
((HypSubst'  (-3)  0  THEN  Auto)  THEN  HypSubst'  (-5)  0  THEN  Auto)

---

Home Index