---

Step * 2 1 of Lemma gcd-reduce


1. ∀p,q:ℕ.  ∃g:ℕ. ∃a,b,x,y:ℤ. ((p = (a * g) ∈ ℤ) ∧ (q = (b * g) ∈ ℤ) ∧ (((x * a) + (y * b)) = 1 ∈ ℤ))
2. p : ℤ@i
3. q : ℤ@i
4. g : ℕ
5. a : ℤ
6. b : ℤ
7. x : ℤ
8. y : ℤ
9. |p| = (a * g) ∈ ℤ
10. |q| = (b * g) ∈ ℤ
11. ((x * a) + (y * b)) = 1 ∈ ℤ
⊢ ∃g:ℕ. ∃a,b,x,y:ℤ. ((p = (a * g) ∈ ℤ) ∧ (q = (b * g) ∈ ℤ) ∧ (((x * a) + (y * b)) = 1 ∈ ℤ))
BY
{ TACTIC:(UseWitness ⌜<g, sign(p) * a, sign(q) * b, sign(p) * x, sign(q) * y, Ax, Ax, Ax>⌝⋅ THEN Auto) }

1
1. ∀p,q:ℕ.  ∃g:ℕ. ∃a,b,x,y:ℤ. ((p = (a * g) ∈ ℤ) ∧ (q = (b * g) ∈ ℤ) ∧ (((x * a) + (y * b)) = 1 ∈ ℤ))
2. p : ℤ@i
3. q : ℤ@i
4. g : ℕ
5. a : ℤ
6. b : ℤ
7. x : ℤ
8. y : ℤ
9. |p| = (a * g) ∈ ℤ
10. |q| = (b * g) ∈ ℤ
11. ((x * a) + (y * b)) = 1 ∈ ℤ
⊢ p = ((sign(p) * a) * g) ∈ ℤ

2
1. ∀p,q:ℕ.  ∃g:ℕ. ∃a,b,x,y:ℤ. ((p = (a * g) ∈ ℤ) ∧ (q = (b * g) ∈ ℤ) ∧ (((x * a) + (y * b)) = 1 ∈ ℤ))
2. p : ℤ@i
3. q : ℤ@i
4. g : ℕ
5. a : ℤ
6. b : ℤ
7. x : ℤ
8. y : ℤ
9. |p| = (a * g) ∈ ℤ
10. |q| = (b * g) ∈ ℤ
11. ((x * a) + (y * b)) = 1 ∈ ℤ
⊢ q = ((sign(q) * b) * g) ∈ ℤ

3
1. ∀p,q:ℕ.  ∃g:ℕ. ∃a,b,x,y:ℤ. ((p = (a * g) ∈ ℤ) ∧ (q = (b * g) ∈ ℤ) ∧ (((x * a) + (y * b)) = 1 ∈ ℤ))
2. p : ℤ@i
3. q : ℤ@i
4. g : ℕ
5. a : ℤ
6. b : ℤ
7. x : ℤ
8. y : ℤ
9. |p| = (a * g) ∈ ℤ
10. |q| = (b * g) ∈ ℤ
11. ((x * a) + (y * b)) = 1 ∈ ℤ
⊢ (((sign(p) * x) * sign(p) * a) + ((sign(q) * y) * sign(q) * b)) = 1 ∈ ℤ

---

Latex:

---

Latex:

1.  \mforall{}p,q:\mBbbN{}.    \mexists{}g:\mBbbN{}.  \mexists{}a,b,x,y:\mBbbZ{}.  ((p  =  (a  *  g))  \mwedge{}  (q  =  (b  *  g))  \mwedge{}  (((x  *  a)  +  (y  *  b))  =  1))
2.  p  :  \mBbbZ{}@i
3.  q  :  \mBbbZ{}@i
4.  g  :  \mBbbN{}
5.  a  :  \mBbbZ{}
6.  b  :  \mBbbZ{}
7.  x  :  \mBbbZ{}
8.  y  :  \mBbbZ{}
9.  |p|  =  (a  *  g)
10.  |q|  =  (b  *  g)
11.  ((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:
TACTIC:(UseWitness  \mkleeneopen{}<g,  sign(p)  *  a,  sign(q)  *  b,  sign(p)  *  x,  sign(q)  *  y,  Ax,  Ax,  Ax>\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index