Theorem gcdaddmzz2nni

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	gcdaddmzz2nni.1	|- M e. NN
	gcdaddmzz2nni.2	|- N e. NN
	gcdaddmzz2nni.3	|- K e. ZZ
Assertion	gcdaddmzz2nni	|- ( M gcd N ) = ( M gcd ( N + ( K x. M ) ) )

Proof

Step	Hyp	Ref	Expression
1		gcdaddmzz2nni.1	|- M e. NN
2		gcdaddmzz2nni.2	|- N e. NN
3		gcdaddmzz2nni.3	|- K e. ZZ
4	1	nnzi	|- M e. ZZ
5	2	nnzi	|- N e. ZZ
6	3 4 5	3pm3.2i	|- ( K e. ZZ /\ M e. ZZ /\ N e. ZZ )
7		gcdaddm	|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = ( M gcd ( N + ( K x. M ) ) ) )
8	6 7	ax-mp	|- ( M gcd N ) = ( M gcd ( N + ( K x. M ) ) )