This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ELEMENTARY NUMBER THEORY Elementary properties of divisibility The greatest common divisor operator gcdabs
Description: The gcd of two integers is the same as that of their absolute values.
(Contributed by Paul Chapman , 31-Mar-2011) (Proof shortened by SN , 15-Sep-2024)
Ref
Expression
Assertion
gcdabs ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = M gcd N
Proof
Step
Hyp
Ref
Expression
1
zabscl ⊢ N ∈ ℤ → N ∈ ℤ
2
gcdabs1 ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = M gcd N
3
1 2
sylan2 ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = M gcd N
4
gcdabs2 ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = M gcd N
5
3 4
eqtrd ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = M gcd N