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 )