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

Metamath Proof Explorer

Theorem lcmfcllem

Description: Lemma for lcmfn0cl and dvdslcmf . (Contributed by AV, 21-Aug-2020) (Proof shortened by AV, 16-Sep-2020)

Ref Expression
Assertion lcmfcllem 
|- ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( _lcm ` Z ) e. { n e. NN | A. m e. Z m || n } )

Proof

Step Hyp Ref Expression
1 lcmfn0val 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( _lcm ` Z ) = inf ( { n e. NN | A. m e. Z m || n } , RR , < ) )
2 ssrab2 
 |-  { n e. NN | A. m e. Z m || n } C_ NN
3 nnuz 
 |-  NN = ( ZZ>= ` 1 )
4 2 3 sseqtri 
 |-  { n e. NN | A. m e. Z m || n } C_ ( ZZ>= ` 1 )
5 fissn0dvdsn0 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> { n e. NN | A. m e. Z m || n } =/= (/) )
6 infssuzcl 
 |-  ( ( { n e. NN | A. m e. Z m || n } C_ ( ZZ>= ` 1 ) /\ { n e. NN | A. m e. Z m || n } =/= (/) ) -> inf ( { n e. NN | A. m e. Z m || n } , RR , < ) e. { n e. NN | A. m e. Z m || n } )
7 4 5 6 sylancr 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> inf ( { n e. NN | A. m e. Z m || n } , RR , < ) e. { n e. NN | A. m e. Z m || n } )
8 1 7 eqeltrd 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( _lcm ` Z ) e. { n e. NN | A. m e. Z m || n } )