Metamath Proof Explorer

Theorem lcmf

Description: Characterization of the least common multiple of a set of integers (without 0): A positiven integer is the least common multiple of a set of integers iff it divides each of the elements of the set and every integer which divides each of the elements of the set is greater than or equal to this integer. (Contributed by AV, 22-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 dvdslcmf 
 |-  ( ( Z C_ ZZ /\ Z e. Fin ) -> A. m e. Z m || ( _lcm ` Z ) )
2 1 3adant3 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> A. m e. Z m || ( _lcm ` Z ) )
3 lcmfledvds 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( ( k e. NN /\ A. m e. Z m || k ) -> ( _lcm ` Z ) <_ k ) )
4 3 expdimp 
 |-  ( ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) /\ k e. NN ) -> ( A. m e. Z m || k -> ( _lcm ` Z ) <_ k ) )
5 4 ralrimiva 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> A. k e. NN ( A. m e. Z m || k -> ( _lcm ` Z ) <_ k ) )
6 2 5 jca 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( A. m e. Z m || ( _lcm ` Z ) /\ A. k e. NN ( A. m e. Z m || k -> ( _lcm ` Z ) <_ k ) ) )
7 6 adantl 
 |-  ( ( K e. NN /\ ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) ) -> ( A. m e. Z m || ( _lcm ` Z ) /\ A. k e. NN ( A. m e. Z m || k -> ( _lcm ` Z ) <_ k ) ) )
8 breq2 
 |-  ( K = ( _lcm ` Z ) -> ( m || K <-> m || ( _lcm ` Z ) ) )
9 8 ralbidv 
 |-  ( K = ( _lcm ` Z ) -> ( A. m e. Z m || K <-> A. m e. Z m || ( _lcm ` Z ) ) )
10 breq1 
 |-  ( K = ( _lcm ` Z ) -> ( K <_ k <-> ( _lcm ` Z ) <_ k ) )
11 10 imbi2d 
 |-  ( K = ( _lcm ` Z ) -> ( ( A. m e. Z m || k -> K <_ k ) <-> ( A. m e. Z m || k -> ( _lcm ` Z ) <_ k ) ) )
12 11 ralbidv 
 |-  ( K = ( _lcm ` Z ) -> ( A. k e. NN ( A. m e. Z m || k -> K <_ k ) <-> A. k e. NN ( A. m e. Z m || k -> ( _lcm ` Z ) <_ k ) ) )
13 9 12 anbi12d 
 |-  ( K = ( _lcm ` Z ) -> ( ( A. m e. Z m || K /\ A. k e. NN ( A. m e. Z m || k -> K <_ k ) ) <-> ( A. m e. Z m || ( _lcm ` Z ) /\ A. k e. NN ( A. m e. Z m || k -> ( _lcm ` Z ) <_ k ) ) ) )
14 7 13 syl5ibrcom 
 |-  ( ( K e. NN /\ ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) ) -> ( K = ( _lcm ` Z ) -> ( A. m e. Z m || K /\ A. k e. NN ( A. m e. Z m || k -> K <_ k ) ) ) )
15 lcmfn0cl 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( _lcm ` Z ) e. NN )
16 15 adantl 
 |-  ( ( K e. NN /\ ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) ) -> ( _lcm ` Z ) e. NN )
17 breq2 
 |-  ( k = ( _lcm ` Z ) -> ( m || k <-> m || ( _lcm ` Z ) ) )
18 17 ralbidv 
 |-  ( k = ( _lcm ` Z ) -> ( A. m e. Z m || k <-> A. m e. Z m || ( _lcm ` Z ) ) )
19 breq2 
 |-  ( k = ( _lcm ` Z ) -> ( K <_ k <-> K <_ ( _lcm ` Z ) ) )
20 18 19 imbi12d 
 |-  ( k = ( _lcm ` Z ) -> ( ( A. m e. Z m || k -> K <_ k ) <-> ( A. m e. Z m || ( _lcm ` Z ) -> K <_ ( _lcm ` Z ) ) ) )
21 20 rspcv 
 |-  ( ( _lcm ` Z ) e. NN -> ( A. k e. NN ( A. m e. Z m || k -> K <_ k ) -> ( A. m e. Z m || ( _lcm ` Z ) -> K <_ ( _lcm ` Z ) ) ) )
22 16 21 syl 
 |-  ( ( K e. NN /\ ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) ) -> ( A. k e. NN ( A. m e. Z m || k -> K <_ k ) -> ( A. m e. Z m || ( _lcm ` Z ) -> K <_ ( _lcm ` Z ) ) ) )
23 22 adantld 
 |-  ( ( K e. NN /\ ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) ) -> ( ( A. m e. Z m || K /\ A. k e. NN ( A. m e. Z m || k -> K <_ k ) ) -> ( A. m e. Z m || ( _lcm ` Z ) -> K <_ ( _lcm ` Z ) ) ) )
24 2 adantl 
 |-  ( ( K e. NN /\ ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) ) -> A. m e. Z m || ( _lcm ` Z ) )
25 nnre 
 |-  ( K e. NN -> K e. RR )
26 15 nnred 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( _lcm ` Z ) e. RR )
27 leloe 
 |-  ( ( K e. RR /\ ( _lcm ` Z ) e. RR ) -> ( K <_ ( _lcm ` Z ) <-> ( K < ( _lcm ` Z ) \/ K = ( _lcm ` Z ) ) ) )
28 25 26 27 syl2an 
 |-  ( ( K e. NN /\ ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) ) -> ( K <_ ( _lcm ` Z ) <-> ( K < ( _lcm ` Z ) \/ K = ( _lcm ` Z ) ) ) )
29 lcmfledvds 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( ( K e. NN /\ A. m e. Z m || K ) -> ( _lcm ` Z ) <_ K ) )
30 29 expd 
 |-  ( ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) -> ( K e. NN -> ( A. m e. Z m || K -> ( _lcm ` Z ) <_ K ) ) )
31 30 impcom 
 |-  ( ( K e. NN /\ ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) ) -> ( A. m e. Z m || K -> ( _lcm ` Z ) <_ K ) )
32 lenlt 
 |-  ( ( ( _lcm ` Z ) e. RR /\ K e. RR ) -> ( ( _lcm ` Z ) <_ K <-> -. K < ( _lcm ` Z ) ) )
33 26 25 32 syl2anr 
 |-  ( ( K e. NN /\ ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) ) -> ( ( _lcm ` Z ) <_ K <-> -. K < ( _lcm ` Z ) ) )
34 pm2.21 
 |-  ( -. K < ( _lcm ` Z ) -> ( K < ( _lcm ` Z ) -> K = ( _lcm ` Z ) ) )
35 33 34 syl6bi 
 |-  ( ( K e. NN /\ ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) ) -> ( ( _lcm ` Z ) <_ K -> ( K < ( _lcm ` Z ) -> K = ( _lcm ` Z ) ) ) )
36 31 35 syldc 
 |-  ( A. m e. Z m || K -> ( ( K e. NN /\ ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) ) -> ( K < ( _lcm ` Z ) -> K = ( _lcm ` Z ) ) ) )
37 36 adantr 
 |-  ( ( A. m e. Z m || K /\ A. k e. NN ( A. m e. Z m || k -> K <_ k ) ) -> ( ( K e. NN /\ ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) ) -> ( K < ( _lcm ` Z ) -> K = ( _lcm ` Z ) ) ) )
38 37 com13 
 |-  ( K < ( _lcm ` Z ) -> ( ( K e. NN /\ ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) ) -> ( ( A. m e. Z m || K /\ A. k e. NN ( A. m e. Z m || k -> K <_ k ) ) -> K = ( _lcm ` Z ) ) ) )
39 2a1 
 |-  ( K = ( _lcm ` Z ) -> ( ( K e. NN /\ ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) ) -> ( ( A. m e. Z m || K /\ A. k e. NN ( A. m e. Z m || k -> K <_ k ) ) -> K = ( _lcm ` Z ) ) ) )
40 38 39 jaoi 
 |-  ( ( K < ( _lcm ` Z ) \/ K = ( _lcm ` Z ) ) -> ( ( K e. NN /\ ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) ) -> ( ( A. m e. Z m || K /\ A. k e. NN ( A. m e. Z m || k -> K <_ k ) ) -> K = ( _lcm ` Z ) ) ) )
41 40 com12 
 |-  ( ( K e. NN /\ ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) ) -> ( ( K < ( _lcm ` Z ) \/ K = ( _lcm ` Z ) ) -> ( ( A. m e. Z m || K /\ A. k e. NN ( A. m e. Z m || k -> K <_ k ) ) -> K = ( _lcm ` Z ) ) ) )
42 28 41 sylbid 
 |-  ( ( K e. NN /\ ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) ) -> ( K <_ ( _lcm ` Z ) -> ( ( A. m e. Z m || K /\ A. k e. NN ( A. m e. Z m || k -> K <_ k ) ) -> K = ( _lcm ` Z ) ) ) )
43 24 42 embantd 
 |-  ( ( K e. NN /\ ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) ) -> ( ( A. m e. Z m || ( _lcm ` Z ) -> K <_ ( _lcm ` Z ) ) -> ( ( A. m e. Z m || K /\ A. k e. NN ( A. m e. Z m || k -> K <_ k ) ) -> K = ( _lcm ` Z ) ) ) )
44 43 com23 
 |-  ( ( K e. NN /\ ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) ) -> ( ( A. m e. Z m || K /\ A. k e. NN ( A. m e. Z m || k -> K <_ k ) ) -> ( ( A. m e. Z m || ( _lcm ` Z ) -> K <_ ( _lcm ` Z ) ) -> K = ( _lcm ` Z ) ) ) )
45 23 44 mpdd 
 |-  ( ( K e. NN /\ ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) ) -> ( ( A. m e. Z m || K /\ A. k e. NN ( A. m e. Z m || k -> K <_ k ) ) -> K = ( _lcm ` Z ) ) )
46 14 45 impbid 
 |-  ( ( K e. NN /\ ( Z C_ ZZ /\ Z e. Fin /\ 0 e/ Z ) ) -> ( K = ( _lcm ` Z ) <-> ( A. m e. Z m || K /\ A. k e. NN ( A. m e. Z m || k -> K <_ k ) ) ) )