Metamath Proof Explorer

Theorem gcdid

Description: The gcd of a number and itself is its absolute value. (Contributed by Paul Chapman, 31-Mar-2011)

Ref Expression
Assertion gcdid 
|- ( N e. ZZ -> ( N gcd N ) = ( abs ` N ) )

Proof

Step Hyp Ref Expression
1 1z 
 |-  1 e. ZZ
2 0z 
 |-  0 e. ZZ
3 gcdaddm 
 |-  ( ( 1 e. ZZ /\ N e. ZZ /\ 0 e. ZZ ) -> ( N gcd 0 ) = ( N gcd ( 0 + ( 1 x. N ) ) ) )
4 1 2 3 mp3an13 
 |-  ( N e. ZZ -> ( N gcd 0 ) = ( N gcd ( 0 + ( 1 x. N ) ) ) )
5 gcdid0 
 |-  ( N e. ZZ -> ( N gcd 0 ) = ( abs ` N ) )
6 zcn 
 |-  ( N e. ZZ -> N e. CC )
7 mulid2 
 |-  ( N e. CC -> ( 1 x. N ) = N )
8 7 oveq2d 
 |-  ( N e. CC -> ( 0 + ( 1 x. N ) ) = ( 0 + N ) )
9 addid2 
 |-  ( N e. CC -> ( 0 + N ) = N )
10 8 9 eqtrd 
 |-  ( N e. CC -> ( 0 + ( 1 x. N ) ) = N )
11 6 10 syl 
 |-  ( N e. ZZ -> ( 0 + ( 1 x. N ) ) = N )
12 11 oveq2d 
 |-  ( N e. ZZ -> ( N gcd ( 0 + ( 1 x. N ) ) ) = ( N gcd N ) )
13 4 5 12 3eqtr3rd 
 |-  ( N e. ZZ -> ( N gcd N ) = ( abs ` N ) )