Metamath Proof Explorer

Theorem lcmfn0cl

Description: Closure of the _lcm function. (Contributed by AV, 21-Aug-2020)

Ref Expression
Assertion lcmfn0cl 
|- ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( _lcm ` Z ) e. NN )

Proof

Step Hyp Ref Expression
1 ssrab2 
 |-  { n e. NN | A. m e. Z m || n } C_ NN
2 lcmfcllem 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( _lcm ` Z ) e. { n e. NN | A. m e. Z m || n } )
3 1 2 sseldi 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( _lcm ` Z ) e. NN )