Step
*
of Lemma
gcd_p_mul
∀a,b,y,n:ℤ. (GCD(a;b;y)
⇒ GCD(n * a;n * b;n * y))
BY
{ (RWN 2 (UnfoldTopC `gcd_p`) 0 THEN Auto) }
1
1. a : ℤ
2. b : ℤ
3. y : ℤ
4. n : ℤ
5. GCD(a;b;y)
⊢ (n * y) | (n * a)
2
1. a : ℤ
2. b : ℤ
3. y : ℤ
4. n : ℤ
5. GCD(a;b;y)
6. (n * y) | (n * a)
⊢ (n * y) | (n * b)
3
1. a : ℤ
2. b : ℤ
3. y : ℤ
4. n : ℤ
5. GCD(a;b;y)
6. (n * y) | (n * a)
7. (n * y) | (n * b)
8. z : ℤ
9. z | (n * a)
10. z | (n * b)
⊢ z | (n * y)
Latex:
Latex:
\mforall{}a,b,y,n:\mBbbZ{}. (GCD(a;b;y) {}\mRightarrow{} GCD(n * a;n * b;n * y))
By
Latex:
(RWN 2 (UnfoldTopC `gcd\_p`) 0 THEN Auto)
Home
Index