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

Metamath Proof Explorer

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 
|- ( ph -> M e. NN0 )
gcdmultipled.2 
|- ( ph -> N e. ZZ )
Assertion gcdmultipled 
|- ( ph -> ( M gcd ( N x. M ) ) = M )

Proof

Step Hyp Ref Expression
1 gcdmultipled.1 
 |-  ( ph -> M e. NN0 )
2 gcdmultipled.2 
 |-  ( ph -> N e. ZZ )
3 1 nn0zd 
 |-  ( ph -> M e. ZZ )
4 0zd 
 |-  ( ph -> 0 e. ZZ )
5 gcdaddm 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ 0 e. ZZ ) -> ( M gcd 0 ) = ( M gcd ( 0 + ( N x. M ) ) ) )
6 2 3 4 5 syl3anc 
 |-  ( ph -> ( M gcd 0 ) = ( M gcd ( 0 + ( N x. M ) ) ) )
7 nn0gcdid0 
 |-  ( M e. NN0 -> ( M gcd 0 ) = M )
8 1 7 syl 
 |-  ( ph -> ( M gcd 0 ) = M )
9 2 3 zmulcld 
 |-  ( ph -> ( N x. M ) e. ZZ )
10 9 zcnd 
 |-  ( ph -> ( N x. M ) e. CC )
11 10 addlidd 
 |-  ( ph -> ( 0 + ( N x. M ) ) = ( N x. M ) )
12 11 oveq2d 
 |-  ( ph -> ( M gcd ( 0 + ( N x. M ) ) ) = ( M gcd ( N x. M ) ) )
13 6 8 12 3eqtr3rd 
 |-  ( ph -> ( M gcd ( N x. M ) ) = M )