Theorem dvdsgcdidd

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

	Ref	Expression
Hypotheses	dvdsgcdidd.1	$$⊢\phi \to M\in \mathbb{N}$$
	dvdsgcdidd.2	$$⊢\phi \to N\in \mathbb{Z}$$
	dvdsgcdidd.3	$$⊢\phi \to M\parallel N$$
Assertion	dvdsgcdidd	$$⊢\phi \to M\gcd N=M$$

Proof

Step	Hyp	Ref	Expression
1		dvdsgcdidd.1	$$⊢\phi \to M\in \mathbb{N}$$
2		dvdsgcdidd.2	$$⊢\phi \to N\in \mathbb{Z}$$
3		dvdsgcdidd.3	$$⊢\phi \to M\parallel N$$
4	2	zcnd	$$⊢\phi \to N\in ℂ$$
5	1	nncnd	$$⊢\phi \to M\in ℂ$$
6	1	nnne0d	$$⊢\phi \to M\ne 0$$
7	4 5 6	divcan1d	$$⊢\phi \to \left(\frac{N}{M}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=N$$
8	7	oveq2d	$$⊢\phi \to M\gcd \left(\frac{N}{M}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M\gcd N$$
9	1	nnnn0d	$$⊢\phi \to M\in {\mathbb{N}}_0$$
10	1	nnzd	$$⊢\phi \to M\in \mathbb{Z}$$
11		dvdsval2	$$⊢\left(M\in \mathbb{Z}\wedge M\ne 0\wedge N\in \mathbb{Z}\right)\to \left(M\parallel N\leftrightarrow \frac{N}{M}\in \mathbb{Z}\right)$$
12	10 6 2 11	syl3anc	$$⊢\phi \to \left(M\parallel N\leftrightarrow \frac{N}{M}\in \mathbb{Z}\right)$$
13	3 12	mpbid	$$⊢\phi \to \frac{N}{M}\in \mathbb{Z}$$
14	9 13	gcdmultipled	$$⊢\phi \to M\gcd \left(\frac{N}{M}\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M$$
15	8 14	eqtr3d	$$⊢\phi \to M\gcd N=M$$