Metamath Proof Explorer

Theorem lcmfledvds

Description: A positive integer which is divisible by all elements of a set of integers bounds the least common multiple of the set. (Contributed by AV, 22-Aug-2020) (Proof shortened by AV, 16-Sep-2020)

Ref Expression
Assertion lcmfledvds 
|- ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( ( K e. NN /\ A. m e. Z m || K ) -> ( _lcm ` Z ) <_ K ) )

Proof

Step Hyp Ref Expression
1 lcmfn0val 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( _lcm ` Z ) = inf ( { k e. NN | A. m e. Z m || k } , RR , < ) )
2 1 adantr 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) /\ ( K e. NN /\ A. m e. Z m || K ) ) -> ( _lcm ` Z ) = inf ( { k e. NN | A. m e. Z m || k } , RR , < ) )
3 ssrab2 
 |-  { k e. NN | A. m e. Z m || k } C_ NN
4 nnuz 
 |-  NN = ( ZZ>= ` 1 )
5 3 4 sseqtri 
 |-  { k e. NN | A. m e. Z m || k } C_ ( ZZ>= ` 1 )
6 breq2 
 |-  ( k = K -> ( m || k <-> m || K ) )
7 6 ralbidv 
 |-  ( k = K -> ( A. m e. Z m || k <-> A. m e. Z m || K ) )
8 7 elrab 
 |-  ( K e. { k e. NN | A. m e. Z m || k } <-> ( K e. NN /\ A. m e. Z m || K ) )
9 8 bilanri 
 |-  ( ( Z C_ ZZ /\ ( K e. NN /\ A. m e. Z m || K ) ) -> K e. { k e. NN | A. m e. Z m || k } )
10 infssuzle 
 |-  ( ( { k e. NN | A. m e. Z m || k } C_ ( ZZ>= ` 1 ) /\ K e. { k e. NN | A. m e. Z m || k } ) -> inf ( { k e. NN | A. m e. Z m || k } , RR , < ) <_ K )
11 5 9 10 sylancr 
 |-  ( ( Z C_ ZZ /\ ( K e. NN /\ A. m e. Z m || K ) ) -> inf ( { k e. NN | A. m e. Z m || k } , RR , < ) <_ K )
12 11 3ad2antl1 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) /\ ( K e. NN /\ A. m e. Z m || K ) ) -> inf ( { k e. NN | A. m e. Z m || k } , RR , < ) <_ K )
13 2 12 eqbrtrd 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) /\ ( K e. NN /\ A. m e. Z m || K ) ) -> ( _lcm ` Z ) <_ K )
14 13 ex 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( ( K e. NN /\ A. m e. Z m || K ) -> ( _lcm ` Z ) <_ K ) )