---

Step * 1 1 2 1 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 : ℕ
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) ∈ ℤ
BY
{ ((InstLemma `div_rem_sum` [⌜q⌝;⌜p⌝]⋅ THENA Auto) THEN NthHypEq (-1) THEN EqCD THEN Auto)⋅ }

1
.....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)) ∈ ℤ

---

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)
\mvdash{}  q  =  (b'  *  g)


By

---

Latex:
((InstLemma  `div\_rem\_sum`  [\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  NthHypEq  (-1)  THEN  EqCD  THEN  Auto)\mcdot{}

---

Home Index