This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ( 𝑁 + ( 𝐾 · 𝑀 ) ) ) )