Metamath Proof Explorer

Theorem gcdcom

Description: The gcd operator is commutative. Theorem 1.4(a) in ApostolNT p. 16. (Contributed by Paul Chapman, 21-Mar-2011)

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

Proof

Step Hyp Ref Expression
1 ancom ⊢ M = 0 ∧ N = 0 ↔ N = 0 ∧ M = 0
2 ancom ⊢ n ∥ M ∧ n ∥ N ↔ n ∥ N ∧ n ∥ M
3 2 rabbii ⊢ n ∈ ℤ | n ∥ M ∧ n ∥ N = n ∈ ℤ | n ∥ N ∧ n ∥ M
4 3 supeq1i ⊢ sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ < = sup n ∈ ℤ | n ∥ N ∧ n ∥ M ℝ <
5 1 4 ifbieq2i ⊢ if M = 0 ∧ N = 0 0 sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ < = if N = 0 ∧ M = 0 0 sup n ∈ ℤ | n ∥ N ∧ n ∥ M ℝ <
6 gcdval ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = if M = 0 ∧ N = 0 0 sup n ∈ ℤ | n ∥ M ∧ n ∥ N ℝ <
7 gcdval ⊢ N ∈ ℤ ∧ M ∈ ℤ → N gcd M = if N = 0 ∧ M = 0 0 sup n ∈ ℤ | n ∥ N ∧ n ∥ M ℝ <
8 7 ancoms ⊢ M ∈ ℤ ∧ N ∈ ℤ → N gcd M = if N = 0 ∧ M = 0 0 sup n ∈ ℤ | n ∥ N ∧ n ∥ M ℝ <
9 5 6 8 3eqtr4a ⊢ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = N gcd M