---

Step * 1 1 2 1 1 1 of Lemma gcd-reduce

.....subterm..... T:t
3:n
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 = (((q ÷ p) * p) + (q rem p)) ∈ ℤ
⊢ (b' * g) = (((q ÷ p) * p) + (q rem p)) ∈ ℤ
BY
{ (ElimVar `b\'' THEN RWO "mul_add_distrib" 0 THEN Auto THEN EqCD THEN Auto THEN HypSubst' (-2) 0 THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
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  =  (((q  \mdiv{}  p)  *  p)  +  (q  rem  p))
\mvdash{}  (b'  *  g)  =  (((q  \mdiv{}  p)  *  p)  +  (q  rem  p))


By

---

Latex:
(ElimVar  `b\mbackslash{}''
  THEN  RWO  "mul\_add\_distrib"  0
  THEN  Auto
  THEN  EqCD
  THEN  Auto
  THEN  HypSubst'  (-2)  0
  THEN  Auto)

---

Home Index