This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 lcm 𝑁 ) = ( 𝑁 lcm 𝑀 ) )

Proof

Step Hyp Ref Expression
1 orcom ⊢ ( ( 𝑀 = 0 ∨ 𝑁 = 0 ) ↔ ( 𝑁 = 0 ∨ 𝑀 = 0 ) )
2 ancom ⊢ ( ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) ↔ ( 𝑁 ∥ 𝑛 ∧ 𝑀 ∥ 𝑛 ) )
3 2 rabbii ⊢ { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } = { 𝑛 ∈ ℕ ∣ ( 𝑁 ∥ 𝑛 ∧ 𝑀 ∥ 𝑛 ) }
4 3 infeq1i ⊢ inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) = inf ( { 𝑛 ∈ ℕ ∣ ( 𝑁 ∥ 𝑛 ∧ 𝑀 ∥ 𝑛 ) } , ℝ , < )
5 1 4 ifbieq2i ⊢ if ( ( 𝑀 = 0 ∨ 𝑁 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ) = if ( ( 𝑁 = 0 ∨ 𝑀 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑁 ∥ 𝑛 ∧ 𝑀 ∥ 𝑛 ) } , ℝ , < ) )
6 lcmval ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 lcm 𝑁 ) = if ( ( 𝑀 = 0 ∨ 𝑁 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛 ) } , ℝ , < ) ) )
7 lcmval ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑁 lcm 𝑀 ) = if ( ( 𝑁 = 0 ∨ 𝑀 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑁 ∥ 𝑛 ∧ 𝑀 ∥ 𝑛 ) } , ℝ , < ) ) )
8 7 ancoms ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 lcm 𝑀 ) = if ( ( 𝑁 = 0 ∨ 𝑀 = 0 ) , 0 , inf ( { 𝑛 ∈ ℕ ∣ ( 𝑁 ∥ 𝑛 ∧ 𝑀 ∥ 𝑛 ) } , ℝ , < ) ) )
9 5 6 8 3eqtr4a ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 lcm 𝑁 ) = ( 𝑁 lcm 𝑀 ) )