This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )