Theorem gcdmultiplei

Description: The GCD of a multiple of a positive integer is the positive integer itself. (Contributed by metakunt, 25-Apr-2024)

	Ref	Expression
Hypotheses	gcdmultiplei.1	⊢ 𝑀 ∈ ℕ
	gcdmultiplei.2	⊢ 𝑁 ∈ ℕ
Assertion	gcdmultiplei	⊢ ( 𝑀 gcd ( 𝑀 · 𝑁 ) ) = 𝑀

Proof

Step	Hyp	Ref	Expression
1		gcdmultiplei.1	⊢ 𝑀 ∈ ℕ
2		gcdmultiplei.2	⊢ 𝑁 ∈ ℕ
3		gcdmultiple	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 gcd ( 𝑀 · 𝑁 ) ) = 𝑀 )
4	1 2 3	mp2an	⊢ ( 𝑀 gcd ( 𝑀 · 𝑁 ) ) = 𝑀