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

Metamath Proof Explorer

Theorem lcmfpr

Description: The value of the _lcm function for an unordered pair is the value of the lcm operator for both elements. (Contributed by AV, 22-Aug-2020) (Proof shortened by AV, 16-Sep-2020)

Ref Expression
Assertion lcmfpr 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( _lcm ` { M , N } ) = ( M lcm N ) )

Proof

Step Hyp Ref Expression
1 c0ex 
 |-  0 e. _V
2 1 elpr 
 |-  ( 0 e. { M , N } <-> ( 0 = M \/ 0 = N ) )
3 eqcom 
 |-  ( 0 = M <-> M = 0 )
4 eqcom 
 |-  ( 0 = N <-> N = 0 )
5 3 4 orbi12i 
 |-  ( ( 0 = M \/ 0 = N ) <-> ( M = 0 \/ N = 0 ) )
6 2 5 bitri 
 |-  ( 0 e. { M , N } <-> ( M = 0 \/ N = 0 ) )
7 6 a1i 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( 0 e. { M , N } <-> ( M = 0 \/ N = 0 ) ) )
8 breq1 
 |-  ( m = M -> ( m || n <-> M || n ) )
9 breq1 
 |-  ( m = N -> ( m || n <-> N || n ) )
10 8 9 ralprg 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( A. m e. { M , N } m || n <-> ( M || n /\ N || n ) ) )
11 10 rabbidv 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> { n e. NN | A. m e. { M , N } m || n } = { n e. NN | ( M || n /\ N || n ) } )
12 11 infeq1d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> inf ( { n e. NN | A. m e. { M , N } m || n } , RR , < ) = inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) )
13 7 12 ifbieq2d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> if ( 0 e. { M , N } , 0 , inf ( { n e. NN | A. m e. { M , N } m || n } , RR , < ) ) = if ( ( M = 0 \/ N = 0 ) , 0 , inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) ) )
14 prssi 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> { M , N } C_ ZZ )
15 prfi 
 |-  { M , N } e. Fin
16 lcmfval 
 |-  ( ( { M , N } C_ ZZ /\ { M , N } e. Fin ) -> ( _lcm ` { M , N } ) = if ( 0 e. { M , N } , 0 , inf ( { n e. NN | A. m e. { M , N } m || n } , RR , < ) ) )
17 14 15 16 sylancl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( _lcm ` { M , N } ) = if ( 0 e. { M , N } , 0 , inf ( { n e. NN | A. m e. { M , N } m || n } , RR , < ) ) )
18 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 , < ) ) )
19 13 17 18 3eqtr4d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( _lcm ` { M , N } ) = ( M lcm N ) )