---

Step * 1 of Lemma gcd_mul


1. a : ℤ
2. b : ℤ
3. n : ℤ
⊢ (n * gcd(a;b)) ~ gcd(n * a;n * b)
BY
{ ((FunElim ⌜gcd(a;b) = y ∈ ℤ⌝ THENM FunElim ⌜gcd(n * a;n * b) = z ∈ ℤ⌝) THENA Auto) }

1
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

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}
2.  b  :  \mBbbZ{}
3.  n  :  \mBbbZ{}
\mvdash{}  (n  *  gcd(a;b))  \msim{}  gcd(n  *  a;n  *  b)


By

---

Latex:
((FunElim  \mkleeneopen{}gcd(a;b)  =  y\mkleeneclose{}  THENM  FunElim  \mkleeneopen{}gcd(n  *  a;n  *  b)  =  z\mkleeneclose{})  THENA  Auto)

---

Home Index