Theorem gcdaddm

Description: Adding a multiple of one operand of the gcd operator to the other does not alter the result. (Contributed by Paul Chapman, 31-Mar-2011)

	Ref	Expression
Assertion	gcdaddm	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd ( 𝑁 + ( 𝐾 · 𝑀 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq1	⊢ ( 𝐾 = if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) → ( 𝐾 · 𝑀 ) = ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · 𝑀 ) )
2	1	oveq1d	⊢ ( 𝐾 = if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) → ( ( 𝐾 · 𝑀 ) + 𝑁 ) = ( ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · 𝑀 ) + 𝑁 ) )
3	2	oveq2d	⊢ ( 𝐾 = if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) → ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) = ( 𝑀 gcd ( ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · 𝑀 ) + 𝑁 ) ) )
4	3	eqeq2d	⊢ ( 𝐾 = if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) → ( ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) ↔ ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd ( ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · 𝑀 ) + 𝑁 ) ) ) )
5		oveq1	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( 𝑀 gcd 𝑁 ) = ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) gcd 𝑁 ) )
6		id	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) )
7		oveq2	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · 𝑀 ) = ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) )
8	7	oveq1d	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · 𝑀 ) + 𝑁 ) = ( ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) + 𝑁 ) )
9	6 8	oveq12d	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( 𝑀 gcd ( ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · 𝑀 ) + 𝑁 ) ) = ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) gcd ( ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) + 𝑁 ) ) )
10	5 9	eqeq12d	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd ( ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · 𝑀 ) + 𝑁 ) ) ↔ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) gcd 𝑁 ) = ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) gcd ( ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) + 𝑁 ) ) ) )
11		oveq2	⊢ ( 𝑁 = if ( 𝑁 ∈ ℤ , 𝑁 , 0 ) → ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) gcd 𝑁 ) = ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) gcd if ( 𝑁 ∈ ℤ , 𝑁 , 0 ) ) )
12		oveq2	⊢ ( 𝑁 = if ( 𝑁 ∈ ℤ , 𝑁 , 0 ) → ( ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) + 𝑁 ) = ( ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) + if ( 𝑁 ∈ ℤ , 𝑁 , 0 ) ) )
13	12	oveq2d	⊢ ( 𝑁 = if ( 𝑁 ∈ ℤ , 𝑁 , 0 ) → ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) gcd ( ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) + 𝑁 ) ) = ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) gcd ( ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) + if ( 𝑁 ∈ ℤ , 𝑁 , 0 ) ) ) )
14	11 13	eqeq12d	⊢ ( 𝑁 = if ( 𝑁 ∈ ℤ , 𝑁 , 0 ) → ( ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) gcd 𝑁 ) = ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) gcd ( ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) + 𝑁 ) ) ↔ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) gcd if ( 𝑁 ∈ ℤ , 𝑁 , 0 ) ) = ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) gcd ( ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) + if ( 𝑁 ∈ ℤ , 𝑁 , 0 ) ) ) ) )
15		0z	⊢ 0 ∈ ℤ
16	15	elimel	⊢ if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) ∈ ℤ
17	15	elimel	⊢ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ∈ ℤ
18	15	elimel	⊢ if ( 𝑁 ∈ ℤ , 𝑁 , 0 ) ∈ ℤ
19	16 17 18	gcdaddmlem	⊢ ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) gcd if ( 𝑁 ∈ ℤ , 𝑁 , 0 ) ) = ( if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) gcd ( ( if ( 𝐾 ∈ ℤ , 𝐾 , 0 ) · if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) + if ( 𝑁 ∈ ℤ , 𝑁 , 0 ) ) )
20	4 10 14 19	dedth3h	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) )
21		zcn	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
22		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
23		mulcl	⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝐾 · 𝑀 ) ∈ ℂ )
24	21 22 23	syl2an	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐾 · 𝑀 ) ∈ ℂ )
25		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
26		addcom	⊢ ( ( ( 𝐾 · 𝑀 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝐾 · 𝑀 ) + 𝑁 ) = ( 𝑁 + ( 𝐾 · 𝑀 ) ) )
27	24 25 26	syl2an	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) + 𝑁 ) = ( 𝑁 + ( 𝐾 · 𝑀 ) ) )
28	27	3impa	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) + 𝑁 ) = ( 𝑁 + ( 𝐾 · 𝑀 ) ) )
29	28	oveq2d	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd ( ( 𝐾 · 𝑀 ) + 𝑁 ) ) = ( 𝑀 gcd ( 𝑁 + ( 𝐾 · 𝑀 ) ) ) )
30	20 29	eqtrd	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd ( 𝑁 + ( 𝐾 · 𝑀 ) ) ) )