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

Proof

Step	Hyp	Ref	Expression
1		gcdaddmzz2nncomi.1	⊢ 𝑀 ∈ ℕ
2		gcdaddmzz2nncomi.2	⊢ 𝑁 ∈ ℕ
3		gcdaddmzz2nncomi.3	⊢ 𝐾 ∈ ℤ
4	1 2 3	gcdaddmzz2nni	⊢ ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd ( 𝑁 + ( 𝐾 · 𝑀 ) ) )
5	2	nncni	⊢ 𝑁 ∈ ℂ
6		zcn	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
7	3 6	ax-mp	⊢ 𝐾 ∈ ℂ
8	1	nncni	⊢ 𝑀 ∈ ℂ
9	7 8	mulcli	⊢ ( 𝐾 · 𝑀 ) ∈ ℂ
10	5 9	addcomi	⊢ ( 𝑁 + ( 𝐾 · 𝑀 ) ) = ( ( 𝐾 · 𝑀 ) + 𝑁 )
11	10	oveq2i	⊢ ( 𝑀 gcd ( 𝑁 + ( 𝐾 · 𝑀 ) ) ) = ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) )
12	4 11	eqtri	⊢ ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) )