lcmcom

Description: The lcm operator is commutative. (Contributed by Steve Rodriguez, 20-Jan-2020) (Proof shortened by AV, 16-Sep-2020)

		Ref	Expression
	Assertion	lcmcom	$⊢ (M \in ℤ \land N \in ℤ) \to M lcm N = N lcm M$

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

Metamath Proof Explorer