Metamath Proof Explorer

Theorem 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 ∈ ℤ ∧ N ∈ ℤ → M lcm N = N lcm M

Proof

Step Hyp Ref Expression
1 orcom ⊢ M = 0 ∨ N = 0 ↔ N = 0 ∨ M = 0
2 ancom ⊢ M ∥ n ∧ N ∥ n ↔ N ∥ n ∧ M ∥ n
3 2 rabbii ⊢ n ∈ ℕ | M ∥ n ∧ N ∥ n = n ∈ ℕ | N ∥ n ∧ M ∥ n
4 3 infeq1i ⊢ inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ < = inf n ∈ ℕ | N ∥ n ∧ M ∥ n ℝ <
5 1 4 ifbieq2i ⊢ if M = 0 ∨ N = 0 0 inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ < = if N = 0 ∨ M = 0 0 inf n ∈ ℕ | N ∥ n ∧ M ∥ n ℝ <
6 lcmval ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm N = if M = 0 ∨ N = 0 0 inf n ∈ ℕ | M ∥ n ∧ N ∥ n ℝ <
7 lcmval ⊢ N ∈ ℤ ∧ M ∈ ℤ → N lcm M = if N = 0 ∨ M = 0 0 inf n ∈ ℕ | N ∥ n ∧ M ∥ n ℝ <
8 7 ancoms ⊢ M ∈ ℤ ∧ N ∈ ℤ → N lcm M = if N = 0 ∨ M = 0 0 inf n ∈ ℕ | N ∥ n ∧ M ∥ n ℝ <
9 5 6 8 3eqtr4a ⊢ M ∈ ℤ ∧ N ∈ ℤ → M lcm N = N lcm M