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 e. ZZ /\ N e. ZZ ) -> ( 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 e. NN | ( M || n /\ N || n ) } = { n e. NN | ( N || n /\ M || n ) }
4 3 infeq1i 
 |-  inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) = inf ( { n e. NN | ( N || n /\ M || n ) } , RR , < )
5 1 4 ifbieq2i 
 |-  if ( ( M = 0 \/ N = 0 ) , 0 , inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) ) = if ( ( N = 0 \/ M = 0 ) , 0 , inf ( { n e. NN | ( N || n /\ M || n ) } , RR , < ) )
6 lcmval 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) = if ( ( M = 0 \/ N = 0 ) , 0 , inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) ) )
7 lcmval 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> ( N lcm M ) = if ( ( N = 0 \/ M = 0 ) , 0 , inf ( { n e. NN | ( N || n /\ M || n ) } , RR , < ) ) )
8 7 ancoms 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( N lcm M ) = if ( ( N = 0 \/ M = 0 ) , 0 , inf ( { n e. NN | ( N || n /\ M || n ) } , RR , < ) ) )
9 5 6 8 3eqtr4a 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) = ( N lcm M ) )