Metamath Proof Explorer

Theorem gcd0id

Description: The gcd of 0 and an integer is the integer's absolute value. (Contributed by Paul Chapman, 21-Mar-2011)

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

Proof

Step Hyp Ref Expression
1 gcd0val 
 |-  ( 0 gcd 0 ) = 0
2 oveq2 
 |-  ( N = 0 -> ( 0 gcd N ) = ( 0 gcd 0 ) )
3 fveq2 
 |-  ( N = 0 -> ( abs ` N ) = ( abs ` 0 ) )
4 abs0 
 |-  ( abs ` 0 ) = 0
5 3 4 eqtrdi 
 |-  ( N = 0 -> ( abs ` N ) = 0 )
6 1 2 5 3eqtr4a 
 |-  ( N = 0 -> ( 0 gcd N ) = ( abs ` N ) )
7 6 adantl 
 |-  ( ( N e. ZZ /\ N = 0 ) -> ( 0 gcd N ) = ( abs ` N ) )
8 0z 
 |-  0 e. ZZ
9 gcddvds 
 |-  ( ( 0 e. ZZ /\ N e. ZZ ) -> ( ( 0 gcd N ) || 0 /\ ( 0 gcd N ) || N ) )
10 8 9 mpan 
 |-  ( N e. ZZ -> ( ( 0 gcd N ) || 0 /\ ( 0 gcd N ) || N ) )
11 10 simprd 
 |-  ( N e. ZZ -> ( 0 gcd N ) || N )
12 11 adantr 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> ( 0 gcd N ) || N )
13 gcdcl 
 |-  ( ( 0 e. ZZ /\ N e. ZZ ) -> ( 0 gcd N ) e. NN0 )
14 8 13 mpan 
 |-  ( N e. ZZ -> ( 0 gcd N ) e. NN0 )
15 14 nn0zd 
 |-  ( N e. ZZ -> ( 0 gcd N ) e. ZZ )
16 dvdsleabs 
 |-  ( ( ( 0 gcd N ) e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( ( 0 gcd N ) || N -> ( 0 gcd N ) <_ ( abs ` N ) ) )
17 15 16 syl3an1 
 |-  ( ( N e. ZZ /\ N e. ZZ /\ N =/= 0 ) -> ( ( 0 gcd N ) || N -> ( 0 gcd N ) <_ ( abs ` N ) ) )
18 17 3anidm12 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> ( ( 0 gcd N ) || N -> ( 0 gcd N ) <_ ( abs ` N ) ) )
19 12 18 mpd 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> ( 0 gcd N ) <_ ( abs ` N ) )
20 zabscl 
 |-  ( N e. ZZ -> ( abs ` N ) e. ZZ )
21 dvds0 
 |-  ( ( abs ` N ) e. ZZ -> ( abs ` N ) || 0 )
22 20 21 syl 
 |-  ( N e. ZZ -> ( abs ` N ) || 0 )
23 iddvds 
 |-  ( N e. ZZ -> N || N )
24 absdvdsb 
 |-  ( ( N e. ZZ /\ N e. ZZ ) -> ( N || N <-> ( abs ` N ) || N ) )
25 24 anidms 
 |-  ( N e. ZZ -> ( N || N <-> ( abs ` N ) || N ) )
26 23 25 mpbid 
 |-  ( N e. ZZ -> ( abs ` N ) || N )
27 22 26 jca 
 |-  ( N e. ZZ -> ( ( abs ` N ) || 0 /\ ( abs ` N ) || N ) )
28 27 adantr 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> ( ( abs ` N ) || 0 /\ ( abs ` N ) || N ) )
29 eqid 
 |-  0 = 0
30 29 biantrur 
 |-  ( N = 0 <-> ( 0 = 0 /\ N = 0 ) )
31 30 necon3abii 
 |-  ( N =/= 0 <-> -. ( 0 = 0 /\ N = 0 ) )
32 dvdslegcd 
 |-  ( ( ( ( abs ` N ) e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) /\ -. ( 0 = 0 /\ N = 0 ) ) -> ( ( ( abs ` N ) || 0 /\ ( abs ` N ) || N ) -> ( abs ` N ) <_ ( 0 gcd N ) ) )
33 32 ex 
 |-  ( ( ( abs ` N ) e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) -> ( -. ( 0 = 0 /\ N = 0 ) -> ( ( ( abs ` N ) || 0 /\ ( abs ` N ) || N ) -> ( abs ` N ) <_ ( 0 gcd N ) ) ) )
34 8 33 mp3an2 
 |-  ( ( ( abs ` N ) e. ZZ /\ N e. ZZ ) -> ( -. ( 0 = 0 /\ N = 0 ) -> ( ( ( abs ` N ) || 0 /\ ( abs ` N ) || N ) -> ( abs ` N ) <_ ( 0 gcd N ) ) ) )
35 20 34 mpancom 
 |-  ( N e. ZZ -> ( -. ( 0 = 0 /\ N = 0 ) -> ( ( ( abs ` N ) || 0 /\ ( abs ` N ) || N ) -> ( abs ` N ) <_ ( 0 gcd N ) ) ) )
36 31 35 syl5bi 
 |-  ( N e. ZZ -> ( N =/= 0 -> ( ( ( abs ` N ) || 0 /\ ( abs ` N ) || N ) -> ( abs ` N ) <_ ( 0 gcd N ) ) ) )
37 36 imp 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> ( ( ( abs ` N ) || 0 /\ ( abs ` N ) || N ) -> ( abs ` N ) <_ ( 0 gcd N ) ) )
38 28 37 mpd 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> ( abs ` N ) <_ ( 0 gcd N ) )
39 15 zred 
 |-  ( N e. ZZ -> ( 0 gcd N ) e. RR )
40 20 zred 
 |-  ( N e. ZZ -> ( abs ` N ) e. RR )
41 39 40 letri3d 
 |-  ( N e. ZZ -> ( ( 0 gcd N ) = ( abs ` N ) <-> ( ( 0 gcd N ) <_ ( abs ` N ) /\ ( abs ` N ) <_ ( 0 gcd N ) ) ) )
42 41 adantr 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> ( ( 0 gcd N ) = ( abs ` N ) <-> ( ( 0 gcd N ) <_ ( abs ` N ) /\ ( abs ` N ) <_ ( 0 gcd N ) ) ) )
43 19 38 42 mpbir2and 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> ( 0 gcd N ) = ( abs ` N ) )
44 7 43 pm2.61dane 
 |-  ( N e. ZZ -> ( 0 gcd N ) = ( abs ` N ) )