Metamath Proof Explorer

Theorem dvdslcmf

Description: The least common multiple of a set of integers is divisible by each of its elements. (Contributed by AV, 22-Aug-2020)

Ref Expression
Assertion dvdslcmf 
|- ( ( Z C_ ZZ /\ Z e. Fin ) -> A. x e. Z x || ( _lcm ` Z ) )

Proof

Step Hyp Ref Expression
1 ssel 
 |-  ( Z C_ ZZ -> ( x e. Z -> x e. ZZ ) )
2 1 ad2antrr 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin ) /\ 0 e. Z ) -> ( x e. Z -> x e. ZZ ) )
3 2 imp 
 |-  ( ( ( ( Z C_ ZZ /\ Z e. Fin ) /\ 0 e. Z ) /\ x e. Z ) -> x e. ZZ )
4 dvds0 
 |-  ( x e. ZZ -> x || 0 )
5 3 4 syl 
 |-  ( ( ( ( Z C_ ZZ /\ Z e. Fin ) /\ 0 e. Z ) /\ x e. Z ) -> x || 0 )
6 lcmf0val 
 |-  ( ( Z C_ ZZ /\ 0 e. Z ) -> ( _lcm ` Z ) = 0 )
7 6 ad4ant13 
 |-  ( ( ( ( Z C_ ZZ /\ Z e. Fin ) /\ 0 e. Z ) /\ x e. Z ) -> ( _lcm ` Z ) = 0 )
8 5 7 breqtrrd 
 |-  ( ( ( ( Z C_ ZZ /\ Z e. Fin ) /\ 0 e. Z ) /\ x e. Z ) -> x || ( _lcm ` Z ) )
9 8 ralrimiva 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin ) /\ 0 e. Z ) -> A. x e. Z x || ( _lcm ` Z ) )
10 df-nel 
 |-  ( 0 e/ Z <-> -. 0 e. Z )
11 lcmfcllem 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( _lcm ` Z ) e. { n e. NN | A. x e. Z x || n } )
12 11 3expa 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin ) /\ 0 e/ Z ) -> ( _lcm ` Z ) e. { n e. NN | A. x e. Z x || n } )
13 10 12 sylan2br 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin ) /\ -. 0 e. Z ) -> ( _lcm ` Z ) e. { n e. NN | A. x e. Z x || n } )
14 lcmfn0cl 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( _lcm ` Z ) e. NN )
15 14 3expa 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin ) /\ 0 e/ Z ) -> ( _lcm ` Z ) e. NN )
16 10 15 sylan2br 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin ) /\ -. 0 e. Z ) -> ( _lcm ` Z ) e. NN )
17 breq2 
 |-  ( n = ( _lcm ` Z ) -> ( x || n <-> x || ( _lcm ` Z ) ) )
18 17 ralbidv 
 |-  ( n = ( _lcm ` Z ) -> ( A. x e. Z x || n <-> A. x e. Z x || ( _lcm ` Z ) ) )
19 18 elrab3 
 |-  ( ( _lcm ` Z ) e. NN -> ( ( _lcm ` Z ) e. { n e. NN | A. x e. Z x || n } <-> A. x e. Z x || ( _lcm ` Z ) ) )
20 16 19 syl 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin ) /\ -. 0 e. Z ) -> ( ( _lcm ` Z ) e. { n e. NN | A. x e. Z x || n } <-> A. x e. Z x || ( _lcm ` Z ) ) )
21 13 20 mpbid 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin ) /\ -. 0 e. Z ) -> A. x e. Z x || ( _lcm ` Z ) )
22 9 21 pm2.61dan 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> A. x e. Z x || ( _lcm ` Z ) )