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	⊢ 𝑀 ∈ ℕ
	gcdaddmzz2nni.2	⊢ 𝑁 ∈ ℕ
	gcdaddmzz2nni.3	⊢ 𝐾 ∈ ℤ
Assertion	gcdaddmzz2nni	⊢ ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd ( 𝑁 + ( 𝐾 · 𝑀 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gcdaddmzz2nni.1	⊢ 𝑀 ∈ ℕ
2		gcdaddmzz2nni.2	⊢ 𝑁 ∈ ℕ
3		gcdaddmzz2nni.3	⊢ 𝐾 ∈ ℤ
4	1	nnzi	⊢ 𝑀 ∈ ℤ
5	2	nnzi	⊢ 𝑁 ∈ ℤ
6	3 4 5	3pm3.2i	⊢ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ )
7		gcdaddm	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd ( 𝑁 + ( 𝐾 · 𝑀 ) ) ) )
8	6 7	ax-mp	⊢ ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd ( 𝑁 + ( 𝐾 · 𝑀 ) ) )