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 𝑀 ) )