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 \in ℤ \land N \in ℤ) \to M \gcd N = N \gcd M$

Step	Hyp	Ref	Expression
1		ancom	$⊢ (M = 0 \land N = 0) \leftrightarrow (N = 0 \land M = 0)$
2		ancom	$⊢ (n ∥ M \land n ∥ N) \leftrightarrow (n ∥ N \land n ∥ M)$
3	2	rabbii	$⊢ \{n \in ℤ \| (n ∥ M \land n ∥ N)\} = \{n \in ℤ \| (n ∥ N \land n ∥ M)\}$
4	3	supeq1i	$⊢ sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <) = sup (\{n \in ℤ \| (n ∥ N \land n ∥ M)\} ℝ <)$
5	1 4	ifbieq2i	$⊢ if ((M = 0 \land N = 0), 0, sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <)) = if ((N = 0 \land M = 0), 0, sup (\{n \in ℤ \| (n ∥ N \land n ∥ M)\} ℝ <))$
6		gcdval	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N = if ((M = 0 \land N = 0), 0, sup (\{n \in ℤ \| (n ∥ M \land n ∥ N)\} ℝ <))$
7		gcdval	$⊢ (N \in ℤ \land M \in ℤ) \to N \gcd M = if ((N = 0 \land M = 0), 0, sup (\{n \in ℤ \| (n ∥ N \land n ∥ M)\} ℝ <))$
8	7	ancoms	$⊢ (M \in ℤ \land N \in ℤ) \to N \gcd M = if ((N = 0 \land M = 0), 0, sup (\{n \in ℤ \| (n ∥ N \land n ∥ M)\} ℝ <))$
9	5 6 8	3eqtr4a	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N = N \gcd M$

Metamath Proof Explorer