Metamath Proof Explorer

Theorem dvdslcm

Description: The lcm of two integers is divisible by each of them. (Contributed by Steve Rodriguez, 20-Jan-2020)

Ref Expression
Assertion dvdslcm 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M || ( M lcm N ) /\ N || ( M lcm N ) ) )

Proof

Step Hyp Ref Expression
1 dvds0 
 |-  ( M e. ZZ -> M || 0 )
2 1 ad2antrr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M = 0 \/ N = 0 ) ) -> M || 0 )
3 oveq1 
 |-  ( M = 0 -> ( M lcm N ) = ( 0 lcm N ) )
4 0z 
 |-  0 e. ZZ
5 lcmcom 
 |-  ( ( N e. ZZ /\ 0 e. ZZ ) -> ( N lcm 0 ) = ( 0 lcm N ) )
6 4 5 mpan2 
 |-  ( N e. ZZ -> ( N lcm 0 ) = ( 0 lcm N ) )
7 lcm0val 
 |-  ( N e. ZZ -> ( N lcm 0 ) = 0 )
8 6 7 eqtr3d 
 |-  ( N e. ZZ -> ( 0 lcm N ) = 0 )
9 3 8 sylan9eqr 
 |-  ( ( N e. ZZ /\ M = 0 ) -> ( M lcm N ) = 0 )
10 9 adantll 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ M = 0 ) -> ( M lcm N ) = 0 )
11 oveq2 
 |-  ( N = 0 -> ( M lcm N ) = ( M lcm 0 ) )
12 lcm0val 
 |-  ( M e. ZZ -> ( M lcm 0 ) = 0 )
13 11 12 sylan9eqr 
 |-  ( ( M e. ZZ /\ N = 0 ) -> ( M lcm N ) = 0 )
14 13 adantlr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ N = 0 ) -> ( M lcm N ) = 0 )
15 10 14 jaodan 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) = 0 )
16 2 15 breqtrrd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M = 0 \/ N = 0 ) ) -> M || ( M lcm N ) )
17 dvds0 
 |-  ( N e. ZZ -> N || 0 )
18 17 ad2antlr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M = 0 \/ N = 0 ) ) -> N || 0 )
19 18 15 breqtrrd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M = 0 \/ N = 0 ) ) -> N || ( M lcm N ) )
20 16 19 jca 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M = 0 \/ N = 0 ) ) -> ( M || ( M lcm N ) /\ N || ( M lcm N ) ) )
21 lcmcllem 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) e. { n e. NN | ( M || n /\ N || n ) } )
22 lcmn0cl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M lcm N ) e. NN )
23 breq2 
 |-  ( n = ( M lcm N ) -> ( M || n <-> M || ( M lcm N ) ) )
24 breq2 
 |-  ( n = ( M lcm N ) -> ( N || n <-> N || ( M lcm N ) ) )
25 23 24 anbi12d 
 |-  ( n = ( M lcm N ) -> ( ( M || n /\ N || n ) <-> ( M || ( M lcm N ) /\ N || ( M lcm N ) ) ) )
26 25 elrab3 
 |-  ( ( M lcm N ) e. NN -> ( ( M lcm N ) e. { n e. NN | ( M || n /\ N || n ) } <-> ( M || ( M lcm N ) /\ N || ( M lcm N ) ) ) )
27 22 26 syl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( ( M lcm N ) e. { n e. NN | ( M || n /\ N || n ) } <-> ( M || ( M lcm N ) /\ N || ( M lcm N ) ) ) )
28 21 27 mpbid 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( M || ( M lcm N ) /\ N || ( M lcm N ) ) )
29 20 28 pm2.61dan 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M || ( M lcm N ) /\ N || ( M lcm N ) ) )