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 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd - 𝑁 ) = ( 𝑀 gcd 𝑁 ) )

Proof

Step Hyp Ref Expression
1 oveq12 ⊢ ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( 𝑀 gcd 𝑁 ) = ( 0 gcd 0 ) )
2 1 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑀 gcd 𝑁 ) = ( 0 gcd 0 ) )
3 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
4 3 negeq0d ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 = 0 ↔ - 𝑁 = 0 ) )
5 4 anbi2d ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) ↔ ( 𝑀 = 0 ∧ - 𝑁 = 0 ) ) )
6 5 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) ↔ ( 𝑀 = 0 ∧ - 𝑁 = 0 ) ) )
7 oveq12 ⊢ ( ( 𝑀 = 0 ∧ - 𝑁 = 0 ) → ( 𝑀 gcd - 𝑁 ) = ( 0 gcd 0 ) )
8 6 7 biimtrdi ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( 𝑀 gcd - 𝑁 ) = ( 0 gcd 0 ) ) )
9 8 imp ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑀 gcd - 𝑁 ) = ( 0 gcd 0 ) )
10 2 9 eqtr4d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd - 𝑁 ) )
11 gcddvds ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) )
12 gcdcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∈ ℕ0 )
13 12 nn0zd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∈ ℤ )
14 dvdsnegb ⊢ ( ( ( 𝑀 gcd 𝑁 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ↔ ( 𝑀 gcd 𝑁 ) ∥ - 𝑁 ) )
15 13 14 sylancom ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ↔ ( 𝑀 gcd 𝑁 ) ∥ - 𝑁 ) )
16 15 anbi2d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ 𝑁 ) ↔ ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ - 𝑁 ) ) )
17 11 16 mpbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ - 𝑁 ) )
18 6 notbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ↔ ¬ ( 𝑀 = 0 ∧ - 𝑁 = 0 ) ) )
19 simpl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑀 ∈ ℤ )
20 znegcl ⊢ ( 𝑁 ∈ ℤ → - 𝑁 ∈ ℤ )
21 20 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → - 𝑁 ∈ ℤ )
22 dvdslegcd ⊢ ( ( ( ( 𝑀 gcd 𝑁 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ - 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ - 𝑁 = 0 ) ) → ( ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ - 𝑁 ) → ( 𝑀 gcd 𝑁 ) ≤ ( 𝑀 gcd - 𝑁 ) ) )
23 22 ex ⊢ ( ( ( 𝑀 gcd 𝑁 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ - 𝑁 ∈ ℤ ) → ( ¬ ( 𝑀 = 0 ∧ - 𝑁 = 0 ) → ( ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ - 𝑁 ) → ( 𝑀 gcd 𝑁 ) ≤ ( 𝑀 gcd - 𝑁 ) ) ) )
24 13 19 21 23 syl3anc ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ ( 𝑀 = 0 ∧ - 𝑁 = 0 ) → ( ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ - 𝑁 ) → ( 𝑀 gcd 𝑁 ) ≤ ( 𝑀 gcd - 𝑁 ) ) ) )
25 18 24 sylbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ - 𝑁 ) → ( 𝑀 gcd 𝑁 ) ≤ ( 𝑀 gcd - 𝑁 ) ) ) )
26 25 com12 ⊢ ( ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑀 gcd 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd 𝑁 ) ∥ - 𝑁 ) → ( 𝑀 gcd 𝑁 ) ≤ ( 𝑀 gcd - 𝑁 ) ) ) )
27 17 26 mpdi ⊢ ( ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ≤ ( 𝑀 gcd - 𝑁 ) ) )
28 27 impcom ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑀 gcd 𝑁 ) ≤ ( 𝑀 gcd - 𝑁 ) )
29 gcddvds ⊢ ( ( 𝑀 ∈ ℤ ∧ - 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd - 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd - 𝑁 ) ∥ - 𝑁 ) )
30 20 29 sylan2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd - 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd - 𝑁 ) ∥ - 𝑁 ) )
31 gcdcl ⊢ ( ( 𝑀 ∈ ℤ ∧ - 𝑁 ∈ ℤ ) → ( 𝑀 gcd - 𝑁 ) ∈ ℕ0 )
32 31 nn0zd ⊢ ( ( 𝑀 ∈ ℤ ∧ - 𝑁 ∈ ℤ ) → ( 𝑀 gcd - 𝑁 ) ∈ ℤ )
33 20 32 sylan2 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd - 𝑁 ) ∈ ℤ )
34 dvdsnegb ⊢ ( ( ( 𝑀 gcd - 𝑁 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd - 𝑁 ) ∥ 𝑁 ↔ ( 𝑀 gcd - 𝑁 ) ∥ - 𝑁 ) )
35 33 34 sylancom ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd - 𝑁 ) ∥ 𝑁 ↔ ( 𝑀 gcd - 𝑁 ) ∥ - 𝑁 ) )
36 35 anbi2d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑀 gcd - 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd - 𝑁 ) ∥ 𝑁 ) ↔ ( ( 𝑀 gcd - 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd - 𝑁 ) ∥ - 𝑁 ) ) )
37 30 36 mpbird ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd - 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd - 𝑁 ) ∥ 𝑁 ) )
38 simpr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
39 dvdslegcd ⊢ ( ( ( ( 𝑀 gcd - 𝑁 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( ( 𝑀 gcd - 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd - 𝑁 ) ∥ 𝑁 ) → ( 𝑀 gcd - 𝑁 ) ≤ ( 𝑀 gcd 𝑁 ) ) )
40 39 ex ⊢ ( ( ( 𝑀 gcd - 𝑁 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( ( 𝑀 gcd - 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd - 𝑁 ) ∥ 𝑁 ) → ( 𝑀 gcd - 𝑁 ) ≤ ( 𝑀 gcd 𝑁 ) ) ) )
41 33 19 38 40 syl3anc ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( ( 𝑀 gcd - 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd - 𝑁 ) ∥ 𝑁 ) → ( 𝑀 gcd - 𝑁 ) ≤ ( 𝑀 gcd 𝑁 ) ) ) )
42 41 com12 ⊢ ( ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( 𝑀 gcd - 𝑁 ) ∥ 𝑀 ∧ ( 𝑀 gcd - 𝑁 ) ∥ 𝑁 ) → ( 𝑀 gcd - 𝑁 ) ≤ ( 𝑀 gcd 𝑁 ) ) ) )
43 37 42 mpdi ⊢ ( ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) → ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd - 𝑁 ) ≤ ( 𝑀 gcd 𝑁 ) ) )
44 43 impcom ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑀 gcd - 𝑁 ) ≤ ( 𝑀 gcd 𝑁 ) )
45 13 zred ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∈ ℝ )
46 33 zred ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd - 𝑁 ) ∈ ℝ )
47 45 46 letri3d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd - 𝑁 ) ↔ ( ( 𝑀 gcd 𝑁 ) ≤ ( 𝑀 gcd - 𝑁 ) ∧ ( 𝑀 gcd - 𝑁 ) ≤ ( 𝑀 gcd 𝑁 ) ) ) )
48 47 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd - 𝑁 ) ↔ ( ( 𝑀 gcd 𝑁 ) ≤ ( 𝑀 gcd - 𝑁 ) ∧ ( 𝑀 gcd - 𝑁 ) ≤ ( 𝑀 gcd 𝑁 ) ) ) )
49 28 44 48 mpbir2and ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 𝑁 = 0 ) ) → ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd - 𝑁 ) )
50 10 49 pm2.61dan ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) = ( 𝑀 gcd - 𝑁 ) )
51 50 eqcomd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd - 𝑁 ) = ( 𝑀 gcd 𝑁 ) )