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 simpr 
 |-  ( ( Z C_ ZZ /\ ( K e. NN /\ A. m e. Z m || K ) ) -> ( K e. NN /\ A. m e. Z m || K ) )
7 breq2 
 |-  ( k = K -> ( m || k <-> m || K ) )
8 7 ralbidv 
 |-  ( k = K -> ( A. m e. Z m || k <-> A. m e. Z m || K ) )
9 8 elrab 
 |-  ( K e. { k e. NN | A. m e. Z m || k } <-> ( K e. NN /\ A. m e. Z m || K ) )
10 6 9 sylibr 
 |-  ( ( Z C_ ZZ /\ ( K e. NN /\ A. m e. Z m || K ) ) -> K e. { k e. NN | A. m e. Z m || k } )
11 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 )
12 5 10 11 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 )
13 12 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 )
14 2 13 eqbrtrd 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) /\ ( K e. NN /\ A. m e. Z m || K ) ) -> ( _lcm ` Z ) <_ K )
15 14 ex 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( ( K e. NN /\ A. m e. Z m || K ) -> ( _lcm ` Z ) <_ K ) )