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

Metamath Proof Explorer

Theorem gcdmultiplez

Description: The GCD of a multiple of an integer is the integer itself. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof shortened by AV, 12-Jan-2023)

Ref Expression
Assertion gcdmultiplez 
|- ( ( M e. NN /\ N e. ZZ ) -> ( M gcd ( M x. N ) ) = M )

Proof

Step Hyp Ref Expression
1 nncn 
 |-  ( M e. NN -> M e. CC )
2 1 adantr 
 |-  ( ( M e. NN /\ N e. ZZ ) -> M e. CC )
3 zcn 
 |-  ( N e. ZZ -> N e. CC )
4 3 adantl 
 |-  ( ( M e. NN /\ N e. ZZ ) -> N e. CC )
5 2 4 mulcomd 
 |-  ( ( M e. NN /\ N e. ZZ ) -> ( M x. N ) = ( N x. M ) )
6 5 oveq2d 
 |-  ( ( M e. NN /\ N e. ZZ ) -> ( M gcd ( M x. N ) ) = ( M gcd ( N x. M ) ) )
7 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
8 7 adantr 
 |-  ( ( M e. NN /\ N e. ZZ ) -> M e. NN0 )
9 simpr 
 |-  ( ( M e. NN /\ N e. ZZ ) -> N e. ZZ )
10 8 9 gcdmultipled 
 |-  ( ( M e. NN /\ N e. ZZ ) -> ( M gcd ( N x. M ) ) = M )
11 6 10 eqtrd 
 |-  ( ( M e. NN /\ N e. ZZ ) -> ( M gcd ( M x. N ) ) = M )