Metamath Proof Explorer

Theorem gcdabs

Description: The gcd of two integers is the same as that of their absolute values. (Contributed by Paul Chapman, 31-Mar-2011)

Ref Expression
Assertion gcdabs ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = M gcd N

Proof

Step Hyp Ref Expression
1 zre ⊢ M ∈ ℤ → M ∈ ℝ
2 zre ⊢ N ∈ ℤ → N ∈ ℝ
3 absor ⊢ M ∈ ℝ → M = M ∨ M = − M
4 absor ⊢ N ∈ ℝ → N = N ∨ N = − N
5 3 4 anim12i ⊢ M ∈ ℝ ∧ N ∈ ℝ → M = M ∨ M = − M ∧ N = N ∨ N = − N
6 1 2 5 syl2an ⊢ M ∈ ℤ ∧ N ∈ ℤ → M = M ∨ M = − M ∧ N = N ∨ N = − N
7 oveq12 ⊢ M = M ∧ N = N → M gcd N = M gcd N
8 7 a1i ⊢ M ∈ ℤ ∧ N ∈ ℤ → M = M ∧ N = N → M gcd N = M gcd N
9 oveq12 ⊢ M = − M ∧ N = N → M gcd N = -M gcd N
10 neggcd ⊢ M ∈ ℤ ∧ N ∈ ℤ → -M gcd N = M gcd N
11 9 10 sylan9eqr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M = − M ∧ N = N → M gcd N = M gcd N
12 11 ex ⊢ M ∈ ℤ ∧ N ∈ ℤ → M = − M ∧ N = N → M gcd N = M gcd N
13 oveq12 ⊢ M = M ∧ N = − N → M gcd N = M gcd -N
14 gcdneg ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd -N = M gcd N
15 13 14 sylan9eqr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M = M ∧ N = − N → M gcd N = M gcd N
16 15 ex ⊢ M ∈ ℤ ∧ N ∈ ℤ → M = M ∧ N = − N → M gcd N = M gcd N
17 oveq12 ⊢ M = − M ∧ N = − N → M gcd N = -M gcd -N
18 znegcl ⊢ M ∈ ℤ → − M ∈ ℤ
19 gcdneg ⊢ − M ∈ ℤ ∧ N ∈ ℤ → -M gcd -N = -M gcd N
20 18 19 sylan ⊢ M ∈ ℤ ∧ N ∈ ℤ → -M gcd -N = -M gcd N
21 20 10 eqtrd ⊢ M ∈ ℤ ∧ N ∈ ℤ → -M gcd -N = M gcd N
22 17 21 sylan9eqr ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ M = − M ∧ N = − N → M gcd N = M gcd N
23 22 ex ⊢ M ∈ ℤ ∧ N ∈ ℤ → M = − M ∧ N = − N → M gcd N = M gcd N
24 8 12 16 23 ccased ⊢ M ∈ ℤ ∧ N ∈ ℤ → M = M ∨ M = − M ∧ N = N ∨ N = − N → M gcd N = M gcd N
25 6 24 mpd ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = M gcd N