Metamath Proof Explorer

Theorem lcmledvds

Description: A positive integer which both operands of the lcm operator divide bounds it. (Contributed by Steve Rodriguez, 20-Jan-2020) (Proof shortened by AV, 16-Sep-2020)

Ref Expression
Assertion lcmledvds 
|- ( ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( ( M || K /\ N || K ) -> ( M lcm N ) <_ K ) )

Proof

Step Hyp Ref Expression
1 lcmn0val 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) = inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) )
2 1 3adantl1 
 |-  ( ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) = inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) )
3 2 adantr 
 |-  ( ( ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) /\ ( M || K /\ N || K ) ) -> ( M lcm N ) = inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) )
4 breq2 
 |-  ( n = K -> ( M || n <-> M || K ) )
5 breq2 
 |-  ( n = K -> ( N || n <-> N || K ) )
6 4 5 anbi12d 
 |-  ( n = K -> ( ( M || n /\ N || n ) <-> ( M || K /\ N || K ) ) )
7 6 elrab 
 |-  ( K e. { n e. NN | ( M || n /\ N || n ) } <-> ( K e. NN /\ ( M || K /\ N || K ) ) )
8 ssrab2 
 |-  { n e. NN | ( M || n /\ N || n ) } C_ NN
9 nnuz 
 |-  NN = ( ZZ>= ` 1 )
10 8 9 sseqtri 
 |-  { n e. NN | ( M || n /\ N || n ) } C_ ( ZZ>= ` 1 )
11 infssuzle 
 |-  ( ( { n e. NN | ( M || n /\ N || n ) } C_ ( ZZ>= ` 1 ) /\ K e. { n e. NN | ( M || n /\ N || n ) } ) -> inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) <_ K )
12 10 11 mpan 
 |-  ( K e. { n e. NN | ( M || n /\ N || n ) } -> inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) <_ K )
13 7 12 sylbir 
 |-  ( ( K e. NN /\ ( M || K /\ N || K ) ) -> inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) <_ K )
14 13 ex 
 |-  ( K e. NN -> ( ( M || K /\ N || K ) -> inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) <_ K ) )
15 14 3ad2ant1 
 |-  ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) -> ( ( M || K /\ N || K ) -> inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) <_ K ) )
16 15 adantr 
 |-  ( ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( ( M || K /\ N || K ) -> inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) <_ K ) )
17 16 imp 
 |-  ( ( ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) /\ ( M || K /\ N || K ) ) -> inf ( { n e. NN | ( M || n /\ N || n ) } , RR , < ) <_ K )
18 3 17 eqbrtrd 
 |-  ( ( ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) /\ ( M || K /\ N || K ) ) -> ( M lcm N ) <_ K )
19 18 ex 
 |-  ( ( ( K e. NN /\ M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( ( M || K /\ N || K ) -> ( M lcm N ) <_ K ) )