Metamath Proof Explorer

Theorem lcmfnncl

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

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

Proof

Step Hyp Ref Expression
1 id 
 |-  ( Z C_ NN -> Z C_ NN )
2 nnssz 
 |-  NN C_ ZZ
3 1 2 sstrdi 
 |-  ( Z C_ NN -> Z C_ ZZ )
4 3 adantr 
 |-  ( ( Z C_ NN /\ Z e. Fin ) -> Z C_ ZZ )
5 simpr 
 |-  ( ( Z C_ NN /\ Z e. Fin ) -> Z e. Fin )
6 0nnn 
 |-  -. 0 e. NN
7 ssel 
 |-  ( Z C_ NN -> ( 0 e. Z -> 0 e. NN ) )
8 6 7 mtoi 
 |-  ( Z C_ NN -> -. 0 e. Z )
9 df-nel 
 |-  ( 0 e/ Z <-> -. 0 e. Z )
10 8 9 sylibr 
 |-  ( Z C_ NN -> 0 e/ Z )
11 10 adantr 
 |-  ( ( Z C_ NN /\ Z e. Fin ) -> 0 e/ Z )
12 lcmfn0cl 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( _lcm ` Z ) e. NN )
13 4 5 11 12 syl3anc 
 |-  ( ( Z C_ NN /\ Z e. Fin ) -> ( _lcm ` Z ) e. NN )