Theorem gcdaddmzz2nncomi

Description: Adding a multiple of one operand of the gcd operator to the other does not alter the result. (Contributed by metakunt, 25-Apr-2024)

	Ref	Expression
Hypotheses	gcdaddmzz2nncomi.1	|- M e. NN
	gcdaddmzz2nncomi.2	|- N e. NN
	gcdaddmzz2nncomi.3	|- K e. ZZ
Assertion	gcdaddmzz2nncomi	|- ( M gcd N ) = ( M gcd ( ( K x. M ) + N ) )

Proof

Step	Hyp	Ref	Expression
1		gcdaddmzz2nncomi.1	|- M e. NN
2		gcdaddmzz2nncomi.2	|- N e. NN
3		gcdaddmzz2nncomi.3	|- K e. ZZ
4	1 2 3	gcdaddmzz2nni	|- ( M gcd N ) = ( M gcd ( N + ( K x. M ) ) )
5	2	nncni	|- N e. CC
6		zcn	|- ( K e. ZZ -> K e. CC )
7	3 6	ax-mp	|- K e. CC
8	1	nncni	|- M e. CC
9	7 8	mulcli	|- ( K x. M ) e. CC
10	5 9	addcomi	|- ( N + ( K x. M ) ) = ( ( K x. M ) + N )
11	10	oveq2i	|- ( M gcd ( N + ( K x. M ) ) ) = ( M gcd ( ( K x. M ) + N ) )
12	4 11	eqtri	|- ( M gcd N ) = ( M gcd ( ( K x. M ) + N ) )