---

Step * 1 of Lemma coprime_prod


1. a : ℤ
2. b1 : ℤ
3. b2 : ℤ
4. CoPrime(a,b1)
5. CoPrime(a,b2)
⊢ CoPrime(a,b1 * b2)
BY
{ ((((FwdThruLemma `coprime_bezout_id` [4] THENM FwdThruLemma `coprime_bezout_id` [5]) THENM OnHyps [5;4] Thin)
   THENM BackThruLemma `coprime_bezout_id`
   )
   THENA Auto
   ) }

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

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b1  :  \mBbbZ{}
3.  b2  :  \mBbbZ{}
4.  CoPrime(a,b1)
5.  CoPrime(a,b2)
\mvdash{}  CoPrime(a,b1  *  b2)


By

---

Latex:
((((FwdThruLemma  `coprime\_bezout\_id`  [4]  THENM  FwdThruLemma  `coprime\_bezout\_id`  [5])
    THENM  OnHyps  [5;4]  Thin
    )
  THENM  BackThruLemma  `coprime\_bezout\_id`
  )
  THENA  Auto
  )

---

Home Index