---

Step * 1 1 of Lemma coprime_prod


1. a : ℤ
2. b1 : ℤ
3. b2 : ℤ
4. ∃x,y:ℤ. (((a * x) + (b1 * y)) = 1 ∈ ℤ)
5. ∃x,y:ℤ. (((a * x) + (b2 * y)) = 1 ∈ ℤ)
⊢ ∃x,y:ℤ. (((a * x) + ((b1 * b2) * y)) = 1 ∈ ℤ)
BY
{ ((OnHyps [5;6;4;5] D THEN RenameVar `x2' 7) THEN RenameVar `y2' 8) }

1
1. a : ℤ
2. b1 : ℤ
3. b2 : ℤ
4. x1 : ℤ
5. y1 : ℤ
6. ((a * x1) + (b1 * y1)) = 1 ∈ ℤ
7. x2 : ℤ
8. y2 : ℤ
9. ((a * x2) + (b2 * y2)) = 1 ∈ ℤ
⊢ ∃x,y:ℤ. (((a * x) + ((b1 * b2) * y)) = 1 ∈ ℤ)

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b1  :  \mBbbZ{}
3.  b2  :  \mBbbZ{}
4.  \mexists{}x,y:\mBbbZ{}.  (((a  *  x)  +  (b1  *  y))  =  1)
5.  \mexists{}x,y:\mBbbZ{}.  (((a  *  x)  +  (b2  *  y))  =  1)
\mvdash{}  \mexists{}x,y:\mBbbZ{}.  (((a  *  x)  +  ((b1  *  b2)  *  y))  =  1)


By

---

Latex:
((OnHyps  [5;6;4;5]  D  THEN  RenameVar  `x2'  7)  THEN  RenameVar  `y2'  8)

---

Home Index