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	|- ( ph -> M e. NN )
	dvdsgcdidd.2	|- ( ph -> N e. ZZ )
	dvdsgcdidd.3	|- ( ph -> M || N )
Assertion	dvdsgcdidd	|- ( ph -> ( M gcd N ) = M )

Proof

Step	Hyp	Ref	Expression
1		dvdsgcdidd.1	|- ( ph -> M e. NN )
2		dvdsgcdidd.2	|- ( ph -> N e. ZZ )
3		dvdsgcdidd.3	|- ( ph -> M || N )
4	2	zcnd	|- ( ph -> N e. CC )
5	1	nncnd	|- ( ph -> M e. CC )
6	1	nnne0d	|- ( ph -> M =/= 0 )
7	4 5 6	divcan1d	|- ( ph -> ( ( N / M ) x. M ) = N )
8	7	oveq2d	|- ( ph -> ( M gcd ( ( N / M ) x. M ) ) = ( M gcd N ) )
9	1	nnnn0d	|- ( ph -> M e. NN0 )
10	1	nnzd	|- ( ph -> M e. ZZ )
11		dvdsval2	|- ( ( M e. ZZ /\ M =/= 0 /\ N e. ZZ ) -> ( M || N <-> ( N / M ) e. ZZ ) )
12	10 6 2 11	syl3anc	|- ( ph -> ( M || N <-> ( N / M ) e. ZZ ) )
13	3 12	mpbid	|- ( ph -> ( N / M ) e. ZZ )
14	9 13	gcdmultipled	|- ( ph -> ( M gcd ( ( N / M ) x. M ) ) = M )
15	8 14	eqtr3d	|- ( ph -> ( M gcd N ) = M )