Theorem gcdmultiple

Description: The GCD of a multiple of a positive integer is the positive integer itself. (Contributed by Scott Fenton, 12-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof shortened by AV, 12-Jan-2023)

	Ref	Expression
Assertion	gcdmultiple	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 gcd ( 𝑀 · 𝑁 ) ) = 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		nnz	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
2		gcdmultiplez	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd ( 𝑀 · 𝑁 ) ) = 𝑀 )
3	1 2	sylan2	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 gcd ( 𝑀 · 𝑁 ) ) = 𝑀 )