Metamath Proof Explorer

Theorem lcmfn0val

Description: The value of the _lcm function for a set without 0. (Contributed by AV, 21-Aug-2020) (Revised by AV, 16-Sep-2020)

Ref Expression
Assertion lcmfn0val 
|- ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( _lcm ` Z ) = inf ( { n e. NN | A. m e. Z m || n } , RR , < ) )

Proof

Step Hyp Ref Expression
1 lcmfval 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> ( _lcm ` Z ) = if ( 0 e. Z , 0 , inf ( { n e. NN | A. m e. Z m || n } , RR , < ) ) )
2 1 3adant3 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( _lcm ` Z ) = if ( 0 e. Z , 0 , inf ( { n e. NN | A. m e. Z m || n } , RR , < ) ) )
3 df-nel 
 |-  ( 0 e/ Z <-> -. 0 e. Z )
4 iffalse 
 |-  ( -. 0 e. Z -> if ( 0 e. Z , 0 , inf ( { n e. NN | A. m e. Z m || n } , RR , < ) ) = inf ( { n e. NN | A. m e. Z m || n } , RR , < ) )
5 3 4 sylbi 
 |-  ( 0 e/ Z -> if ( 0 e. Z , 0 , inf ( { n e. NN | A. m e. Z m || n } , RR , < ) ) = inf ( { n e. NN | A. m e. Z m || n } , RR , < ) )
6 5 3ad2ant3 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> if ( 0 e. Z , 0 , inf ( { n e. NN | A. m e. Z m || n } , RR , < ) ) = inf ( { n e. NN | A. m e. Z m || n } , RR , < ) )
7 2 6 eqtrd 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( _lcm ` Z ) = inf ( { n e. NN | A. m e. Z m || n } , RR , < ) )