Metamath Proof Explorer

Theorem gcdadd

Description: The GCD of two numbers is the same as the GCD of the left and their sum. (Contributed by Scott Fenton, 20-Apr-2014)

Ref Expression
Assertion gcdadd 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = ( M gcd ( N + M ) ) )

Proof

Step Hyp Ref Expression
1 1z 
 |-  1 e. ZZ
2 gcdaddm 
 |-  ( ( 1 e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = ( M gcd ( N + ( 1 x. M ) ) ) )
3 1 2 mp3an1 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = ( M gcd ( N + ( 1 x. M ) ) ) )
4 zcn 
 |-  ( M e. ZZ -> M e. CC )
5 mulid2 
 |-  ( M e. CC -> ( 1 x. M ) = M )
6 5 oveq2d 
 |-  ( M e. CC -> ( N + ( 1 x. M ) ) = ( N + M ) )
7 6 oveq2d 
 |-  ( M e. CC -> ( M gcd ( N + ( 1 x. M ) ) ) = ( M gcd ( N + M ) ) )
8 4 7 syl 
 |-  ( M e. ZZ -> ( M gcd ( N + ( 1 x. M ) ) ) = ( M gcd ( N + M ) ) )
9 8 adantr 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd ( N + ( 1 x. M ) ) ) = ( M gcd ( N + M ) ) )
10 3 9 eqtrd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = ( M gcd ( N + M ) ) )