---

Step * 1 1 of Lemma gcd_mul


1. a : ℤ
2. b : ℤ
3. n : ℤ
4. y : ℤ
5. GCD(a;b;y)
6. z : ℤ
7. GCD(n * a;n * b;z)
⊢ (n * y) ~ z
BY
{ ((Using [`n',⌜n⌝] (FLemma `gcd_p_mul` [5]) THENM FLemma `gcd_unique` [-1;-2]) THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b  :  \mBbbZ{}
3.  n  :  \mBbbZ{}
4.  y  :  \mBbbZ{}
5.  GCD(a;b;y)
6.  z  :  \mBbbZ{}
7.  GCD(n  *  a;n  *  b;z)
\mvdash{}  (n  *  y)  \msim{}  z


By

---

Latex:
((Using  [`n',\mkleeneopen{}n\mkleeneclose{}]  (FLemma  `gcd\_p\_mul`  [5])  THENM  FLemma  `gcd\_unique`  [-1;-2])  THEN  Auto)

---

Home Index