Theorem gcdmultipled

Description: The greatest common divisor of a nonnegative integer M and a multiple of it is M itself. (Contributed by Rohan Ridenour, 3-Aug-2023)

	Ref	Expression
Hypotheses	gcdmultipled.1	$$⊢\phi \to M\in {\mathbb{N}}_0$$
	gcdmultipled.2	$$⊢\phi \to N\in \mathbb{Z}$$
Assertion	gcdmultipled	$$⊢\phi \to M\gcd \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M$$

Proof

Step	Hyp	Ref	Expression
1		gcdmultipled.1	$$⊢\phi \to M\in {\mathbb{N}}_0$$
2		gcdmultipled.2	$$⊢\phi \to N\in \mathbb{Z}$$
3	1	nn0zd	$$⊢\phi \to M\in \mathbb{Z}$$
4		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
5		gcdaddm	$$⊢\left(N\in \mathbb{Z}\wedge M\in \mathbb{Z}\wedge 0\in \mathbb{Z}\right)\to M\gcd 0=M\gcd \left(0+\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\right)$$
6	2 3 4 5	syl3anc	$$⊢\phi \to M\gcd 0=M\gcd \left(0+\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\right)$$
7		nn0gcdid0	$$⊢M\in {\mathbb{N}}_0\to M\gcd 0=M$$
8	1 7	syl	$$⊢\phi \to M\gcd 0=M$$
9	2 3	zmulcld	$$⊢\phi \to \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in \mathbb{Z}$$
10	9	zcnd	$$⊢\phi \to \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in ℂ$$
11	10	addid2d	$$⊢\phi \to 0+\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
12	11	oveq2d	$$⊢\phi \to M\gcd \left(0+\mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\right)=M\gcd \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
13	6 8 12	3eqtr3rd	$$⊢\phi \to M\gcd \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M$$