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	$$⊢M\in \mathbb{N}$$
	gcdmultiplei.2	$$⊢N\in \mathbb{N}$$
Assertion	gcdmultiplei	$$⊢M\gcd \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=M$$

Proof

Step	Hyp	Ref	Expression
1		gcdmultiplei.1	$$⊢M\in \mathbb{N}$$
2		gcdmultiplei.2	$$⊢N\in \mathbb{N}$$
3		gcdmultiple	$$⊢\left(M\in \mathbb{N}\wedge N\in \mathbb{N}\right)\to M\gcd \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=M$$
4	1 2 3	mp2an	$$⊢M\gcd \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=M$$