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	$$⊢\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$$

Proof

Step	Hyp	Ref	Expression
1		nnz	$$⊢N\in \mathbb{N}\to N\in \mathbb{Z}$$
2		gcdmultiplez	$$⊢\left(M\in \mathbb{N}\wedge N\in \mathbb{Z}\right)\to M\gcd \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=M$$
3	1 2	sylan2	$$⊢\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$$