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 
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = ( M gcd ( N + ( K x. M ) ) ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( K = if ( K e. ZZ , K , 0 ) -> ( K x. M ) = ( if ( K e. ZZ , K , 0 ) x. M ) )
2 1 oveq1d 
 |-  ( K = if ( K e. ZZ , K , 0 ) -> ( ( K x. M ) + N ) = ( ( if ( K e. ZZ , K , 0 ) x. M ) + N ) )
3 2 oveq2d 
 |-  ( K = if ( K e. ZZ , K , 0 ) -> ( M gcd ( ( K x. M ) + N ) ) = ( M gcd ( ( if ( K e. ZZ , K , 0 ) x. M ) + N ) ) )
4 3 eqeq2d 
 |-  ( K = if ( K e. ZZ , K , 0 ) -> ( ( M gcd N ) = ( M gcd ( ( K x. M ) + N ) ) <-> ( M gcd N ) = ( M gcd ( ( if ( K e. ZZ , K , 0 ) x. M ) + N ) ) ) )
5 oveq1 
 |-  ( M = if ( M e. ZZ , M , 0 ) -> ( M gcd N ) = ( if ( M e. ZZ , M , 0 ) gcd N ) )
6 id 
 |-  ( M = if ( M e. ZZ , M , 0 ) -> M = if ( M e. ZZ , M , 0 ) )
7 oveq2 
 |-  ( M = if ( M e. ZZ , M , 0 ) -> ( if ( K e. ZZ , K , 0 ) x. M ) = ( if ( K e. ZZ , K , 0 ) x. if ( M e. ZZ , M , 0 ) ) )
8 7 oveq1d 
 |-  ( M = if ( M e. ZZ , M , 0 ) -> ( ( if ( K e. ZZ , K , 0 ) x. M ) + N ) = ( ( if ( K e. ZZ , K , 0 ) x. if ( M e. ZZ , M , 0 ) ) + N ) )
9 6 8 oveq12d 
 |-  ( M = if ( M e. ZZ , M , 0 ) -> ( M gcd ( ( if ( K e. ZZ , K , 0 ) x. M ) + N ) ) = ( if ( M e. ZZ , M , 0 ) gcd ( ( if ( K e. ZZ , K , 0 ) x. if ( M e. ZZ , M , 0 ) ) + N ) ) )
10 5 9 eqeq12d 
 |-  ( M = if ( M e. ZZ , M , 0 ) -> ( ( M gcd N ) = ( M gcd ( ( if ( K e. ZZ , K , 0 ) x. M ) + N ) ) <-> ( if ( M e. ZZ , M , 0 ) gcd N ) = ( if ( M e. ZZ , M , 0 ) gcd ( ( if ( K e. ZZ , K , 0 ) x. if ( M e. ZZ , M , 0 ) ) + N ) ) ) )
11 oveq2 
 |-  ( N = if ( N e. ZZ , N , 0 ) -> ( if ( M e. ZZ , M , 0 ) gcd N ) = ( if ( M e. ZZ , M , 0 ) gcd if ( N e. ZZ , N , 0 ) ) )
12 oveq2 
 |-  ( N = if ( N e. ZZ , N , 0 ) -> ( ( if ( K e. ZZ , K , 0 ) x. if ( M e. ZZ , M , 0 ) ) + N ) = ( ( if ( K e. ZZ , K , 0 ) x. if ( M e. ZZ , M , 0 ) ) + if ( N e. ZZ , N , 0 ) ) )
13 12 oveq2d 
 |-  ( N = if ( N e. ZZ , N , 0 ) -> ( if ( M e. ZZ , M , 0 ) gcd ( ( if ( K e. ZZ , K , 0 ) x. if ( M e. ZZ , M , 0 ) ) + N ) ) = ( if ( M e. ZZ , M , 0 ) gcd ( ( if ( K e. ZZ , K , 0 ) x. if ( M e. ZZ , M , 0 ) ) + if ( N e. ZZ , N , 0 ) ) ) )
14 11 13 eqeq12d 
 |-  ( N = if ( N e. ZZ , N , 0 ) -> ( ( if ( M e. ZZ , M , 0 ) gcd N ) = ( if ( M e. ZZ , M , 0 ) gcd ( ( if ( K e. ZZ , K , 0 ) x. if ( M e. ZZ , M , 0 ) ) + N ) ) <-> ( if ( M e. ZZ , M , 0 ) gcd if ( N e. ZZ , N , 0 ) ) = ( if ( M e. ZZ , M , 0 ) gcd ( ( if ( K e. ZZ , K , 0 ) x. if ( M e. ZZ , M , 0 ) ) + if ( N e. ZZ , N , 0 ) ) ) ) )
15 0z 
 |-  0 e. ZZ
16 15 elimel 
 |-  if ( K e. ZZ , K , 0 ) e. ZZ
17 15 elimel 
 |-  if ( M e. ZZ , M , 0 ) e. ZZ
18 15 elimel 
 |-  if ( N e. ZZ , N , 0 ) e. ZZ
19 16 17 18 gcdaddmlem 
 |-  ( if ( M e. ZZ , M , 0 ) gcd if ( N e. ZZ , N , 0 ) ) = ( if ( M e. ZZ , M , 0 ) gcd ( ( if ( K e. ZZ , K , 0 ) x. if ( M e. ZZ , M , 0 ) ) + if ( N e. ZZ , N , 0 ) ) )
20 4 10 14 19 dedth3h 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = ( M gcd ( ( K x. M ) + N ) ) )
21 zcn 
 |-  ( K e. ZZ -> K e. CC )
22 zcn 
 |-  ( M e. ZZ -> M e. CC )
23 mulcl 
 |-  ( ( K e. CC /\ M e. CC ) -> ( K x. M ) e. CC )
24 21 22 23 syl2an 
 |-  ( ( K e. ZZ /\ M e. ZZ ) -> ( K x. M ) e. CC )
25 zcn 
 |-  ( N e. ZZ -> N e. CC )
26 addcom 
 |-  ( ( ( K x. M ) e. CC /\ N e. CC ) -> ( ( K x. M ) + N ) = ( N + ( K x. M ) ) )
27 24 25 26 syl2an 
 |-  ( ( ( K e. ZZ /\ M e. ZZ ) /\ N e. ZZ ) -> ( ( K x. M ) + N ) = ( N + ( K x. M ) ) )
28 27 3impa 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K x. M ) + N ) = ( N + ( K x. M ) ) )
29 28 oveq2d 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M gcd ( ( K x. M ) + N ) ) = ( M gcd ( N + ( K x. M ) ) ) )
30 20 29 eqtrd 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = ( M gcd ( N + ( K x. M ) ) ) )