This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ELEMENTARY NUMBER THEORY Elementary properties of divisibility The greatest common divisor operator gcdmultiplez
Description: The GCD of a multiple of an integer is the integer itself. (Contributed by Scott Fenton , 18-Apr-2014) (Revised by Mario Carneiro , 19-Apr-2014)
(Proof shortened by AV , 12-Jan-2023)
Ref
Expression
Assertion
gcdmultiplez ⊢ M ∈ ℕ ∧ N ∈ ℤ → M gcd M ⋅ N = M
Proof
Step
Hyp
Ref
Expression
1
nncn ⊢ M ∈ ℕ → M ∈ ℂ
2
1
adantr ⊢ M ∈ ℕ ∧ N ∈ ℤ → M ∈ ℂ
3
zcn ⊢ N ∈ ℤ → N ∈ ℂ
4
3
adantl ⊢ M ∈ ℕ ∧ N ∈ ℤ → N ∈ ℂ
5
2 4
mulcomd ⊢ M ∈ ℕ ∧ N ∈ ℤ → M ⋅ N = N ⋅ M
6
5
oveq2d ⊢ M ∈ ℕ ∧ N ∈ ℤ → M gcd M ⋅ N = M gcd N ⋅ M
7
nnnn0 ⊢ M ∈ ℕ → M ∈ ℕ 0
8
7
adantr ⊢ M ∈ ℕ ∧ N ∈ ℤ → M ∈ ℕ 0
9
simpr ⊢ M ∈ ℕ ∧ N ∈ ℤ → N ∈ ℤ
10
8 9
gcdmultipled ⊢ M ∈ ℕ ∧ N ∈ ℤ → M gcd N ⋅ M = M
11
6 10
eqtrd ⊢ M ∈ ℕ ∧ N ∈ ℤ → M gcd M ⋅ N = M