Metamath Proof Explorer

Theorem lcmfcl

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

Ref Expression
Assertion lcmfcl 
|- ( ( Z C_ ZZ /\ Z e. Fin ) -> ( _lcm ` Z ) e. NN0 )

Proof

Step Hyp Ref Expression
1 lcmf0val 
 |-  ( ( Z C_ ZZ /\ 0 e. Z ) -> ( _lcm ` Z ) = 0 )
2 0nn0 
 |-  0 e. NN0
3 1 2 eqeltrdi 
 |-  ( ( Z C_ ZZ /\ 0 e. Z ) -> ( _lcm ` Z ) e. NN0 )
4 3 adantlr 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin ) /\ 0 e. Z ) -> ( _lcm ` Z ) e. NN0 )
5 df-nel 
 |-  ( 0 e/ Z <-> -. 0 e. Z )
6 lcmfn0cl 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( _lcm ` Z ) e. NN )
7 6 3expa 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin ) /\ 0 e/ Z ) -> ( _lcm ` Z ) e. NN )
8 5 7 sylan2br 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin ) /\ -. 0 e. Z ) -> ( _lcm ` Z ) e. NN )
9 8 nnnn0d 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin ) /\ -. 0 e. Z ) -> ( _lcm ` Z ) e. NN0 )
10 4 9 pm2.61dan 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> ( _lcm ` Z ) e. NN0 )