---

Step * of Lemma coprime_divides_prod

∀a1,a2,b:ℤ.  ((b | (a1 * a2)) ⇒ CoPrime(b,a1) ⇒ (b | a2))
BY
{ (Auto THEN (FwdThruLemma `coprime_bezout_id` [-1] THENA Auto) THEN ExRepD) }

1
1. a1 : ℤ
2. a2 : ℤ
3. b : ℤ
4. b | (a1 * a2)
5. CoPrime(b,a1)
6. x : ℤ
7. y : ℤ
8. ((b * x) + (a1 * y)) = 1 ∈ ℤ
⊢ b | a2

---

Latex:

---

Latex:
\mforall{}a1,a2,b:\mBbbZ{}.    ((b  |  (a1  *  a2))  {}\mRightarrow{}  CoPrime(b,a1)  {}\mRightarrow{}  (b  |  a2))


By

---

Latex:
(Auto  THEN  (FwdThruLemma  `coprime\_bezout\_id`  [-1]  THENA  Auto)  THEN  ExRepD)

---

Home Index