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

Metamath Proof Explorer

Theorem lcmfnnval

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

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

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 6 nelir 
 |-  0 e/ NN
8 ssel 
 |-  ( Z C_ NN -> ( 0 e. Z -> 0 e. NN ) )
9 8 nelcon3d 
 |-  ( Z C_ NN -> ( 0 e/ NN -> 0 e/ Z ) )
10 7 9 mpi 
 |-  ( Z C_ NN -> 0 e/ Z )
11 10 adantr 
 |-  ( ( Z C_ NN /\ Z e. Fin ) -> 0 e/ Z )
12 lcmfn0val 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( _lcm ` Z ) = inf ( { n e. NN | A. m e. Z m || n } , RR , < ) )
13 4 5 11 12 syl3anc 
 |-  ( ( Z C_ NN /\ Z e. Fin ) -> ( _lcm ` Z ) = inf ( { n e. NN | A. m e. Z m || n } , RR , < ) )