Metamath Proof Explorer

Theorem gcdneg

Description: Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 21-Mar-2011)

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

Proof

Step Hyp Ref Expression
1 oveq12 
 |-  ( ( M = 0 /\ N = 0 ) -> ( M gcd N ) = ( 0 gcd 0 ) )
2 1 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) = ( 0 gcd 0 ) )
3 zcn 
 |-  ( N e. ZZ -> N e. CC )
4 3 negeq0d 
 |-  ( N e. ZZ -> ( N = 0 <-> -u N = 0 ) )
5 4 anbi2d 
 |-  ( N e. ZZ -> ( ( M = 0 /\ N = 0 ) <-> ( M = 0 /\ -u N = 0 ) ) )
6 5 adantl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M = 0 /\ N = 0 ) <-> ( M = 0 /\ -u N = 0 ) ) )
7 oveq12 
 |-  ( ( M = 0 /\ -u N = 0 ) -> ( M gcd -u N ) = ( 0 gcd 0 ) )
8 6 7 syl6bi 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M = 0 /\ N = 0 ) -> ( M gcd -u N ) = ( 0 gcd 0 ) ) )
9 8 imp 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M = 0 /\ N = 0 ) ) -> ( M gcd -u N ) = ( 0 gcd 0 ) )
10 2 9 eqtr4d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) = ( M gcd -u N ) )
11 gcddvds 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) || M /\ ( M gcd N ) || N ) )
12 gcdcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. NN0 )
13 12 nn0zd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. ZZ )
14 dvdsnegb 
 |-  ( ( ( M gcd N ) e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) || N <-> ( M gcd N ) || -u N ) )
15 13 14 sylancom 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) || N <-> ( M gcd N ) || -u N ) )
16 15 anbi2d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( M gcd N ) || M /\ ( M gcd N ) || N ) <-> ( ( M gcd N ) || M /\ ( M gcd N ) || -u N ) ) )
17 11 16 mpbid 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) || M /\ ( M gcd N ) || -u N ) )
18 6 notbid 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( -. ( M = 0 /\ N = 0 ) <-> -. ( M = 0 /\ -u N = 0 ) ) )
19 simpl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> M e. ZZ )
20 znegcl 
 |-  ( N e. ZZ -> -u N e. ZZ )
21 20 adantl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> -u N e. ZZ )
22 dvdslegcd 
 |-  ( ( ( ( M gcd N ) e. ZZ /\ M e. ZZ /\ -u N e. ZZ ) /\ -. ( M = 0 /\ -u N = 0 ) ) -> ( ( ( M gcd N ) || M /\ ( M gcd N ) || -u N ) -> ( M gcd N ) <_ ( M gcd -u N ) ) )
23 22 ex 
 |-  ( ( ( M gcd N ) e. ZZ /\ M e. ZZ /\ -u N e. ZZ ) -> ( -. ( M = 0 /\ -u N = 0 ) -> ( ( ( M gcd N ) || M /\ ( M gcd N ) || -u N ) -> ( M gcd N ) <_ ( M gcd -u N ) ) ) )
24 13 19 21 23 syl3anc 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( -. ( M = 0 /\ -u N = 0 ) -> ( ( ( M gcd N ) || M /\ ( M gcd N ) || -u N ) -> ( M gcd N ) <_ ( M gcd -u N ) ) ) )
25 18 24 sylbid 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( -. ( M = 0 /\ N = 0 ) -> ( ( ( M gcd N ) || M /\ ( M gcd N ) || -u N ) -> ( M gcd N ) <_ ( M gcd -u N ) ) ) )
26 25 com12 
 |-  ( -. ( M = 0 /\ N = 0 ) -> ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( M gcd N ) || M /\ ( M gcd N ) || -u N ) -> ( M gcd N ) <_ ( M gcd -u N ) ) ) )
27 17 26 mpdi 
 |-  ( -. ( M = 0 /\ N = 0 ) -> ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) <_ ( M gcd -u N ) ) )
28 27 impcom 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) <_ ( M gcd -u N ) )
29 gcddvds 
 |-  ( ( M e. ZZ /\ -u N e. ZZ ) -> ( ( M gcd -u N ) || M /\ ( M gcd -u N ) || -u N ) )
30 20 29 sylan2 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd -u N ) || M /\ ( M gcd -u N ) || -u N ) )
31 gcdcl 
 |-  ( ( M e. ZZ /\ -u N e. ZZ ) -> ( M gcd -u N ) e. NN0 )
32 31 nn0zd 
 |-  ( ( M e. ZZ /\ -u N e. ZZ ) -> ( M gcd -u N ) e. ZZ )
33 20 32 sylan2 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd -u N ) e. ZZ )
34 dvdsnegb 
 |-  ( ( ( M gcd -u N ) e. ZZ /\ N e. ZZ ) -> ( ( M gcd -u N ) || N <-> ( M gcd -u N ) || -u N ) )
35 33 34 sylancom 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd -u N ) || N <-> ( M gcd -u N ) || -u N ) )
36 35 anbi2d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( M gcd -u N ) || M /\ ( M gcd -u N ) || N ) <-> ( ( M gcd -u N ) || M /\ ( M gcd -u N ) || -u N ) ) )
37 30 36 mpbird 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd -u N ) || M /\ ( M gcd -u N ) || N ) )
38 simpr 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> N e. ZZ )
39 dvdslegcd 
 |-  ( ( ( ( M gcd -u N ) e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( ( ( M gcd -u N ) || M /\ ( M gcd -u N ) || N ) -> ( M gcd -u N ) <_ ( M gcd N ) ) )
40 39 ex 
 |-  ( ( ( M gcd -u N ) e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( -. ( M = 0 /\ N = 0 ) -> ( ( ( M gcd -u N ) || M /\ ( M gcd -u N ) || N ) -> ( M gcd -u N ) <_ ( M gcd N ) ) ) )
41 33 19 38 40 syl3anc 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( -. ( M = 0 /\ N = 0 ) -> ( ( ( M gcd -u N ) || M /\ ( M gcd -u N ) || N ) -> ( M gcd -u N ) <_ ( M gcd N ) ) ) )
42 41 com12 
 |-  ( -. ( M = 0 /\ N = 0 ) -> ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( M gcd -u N ) || M /\ ( M gcd -u N ) || N ) -> ( M gcd -u N ) <_ ( M gcd N ) ) ) )
43 37 42 mpdi 
 |-  ( -. ( M = 0 /\ N = 0 ) -> ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd -u N ) <_ ( M gcd N ) ) )
44 43 impcom 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd -u N ) <_ ( M gcd N ) )
45 13 zred 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. RR )
46 33 zred 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd -u N ) e. RR )
47 45 46 letri3d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M gcd N ) = ( M gcd -u N ) <-> ( ( M gcd N ) <_ ( M gcd -u N ) /\ ( M gcd -u N ) <_ ( M gcd N ) ) ) )
48 47 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( ( M gcd N ) = ( M gcd -u N ) <-> ( ( M gcd N ) <_ ( M gcd -u N ) /\ ( M gcd -u N ) <_ ( M gcd N ) ) ) )
49 28 44 48 mpbir2and 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) = ( M gcd -u N ) )
50 10 49 pm2.61dan 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = ( M gcd -u N ) )
51 50 eqcomd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd -u N ) = ( M gcd N ) )