Metamath Proof Explorer

Theorem lcmdvds

Description: The lcm of two integers divides any integer the two divide. (Contributed by Steve Rodriguez, 20-Jan-2020)

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

Proof

Step Hyp Ref Expression
1 id 
 |-  ( 0 || K -> 0 || K )
2 breq1 
 |-  ( M = 0 -> ( M || K <-> 0 || K ) )
3 2 adantl 
 |-  ( ( N e. ZZ /\ M = 0 ) -> ( M || K <-> 0 || K ) )
4 oveq1 
 |-  ( M = 0 -> ( M lcm N ) = ( 0 lcm N ) )
5 0z 
 |-  0 e. ZZ
6 lcmcom 
 |-  ( ( 0 e. ZZ /\ N e. ZZ ) -> ( 0 lcm N ) = ( N lcm 0 ) )
7 5 6 mpan 
 |-  ( N e. ZZ -> ( 0 lcm N ) = ( N lcm 0 ) )
8 lcm0val 
 |-  ( N e. ZZ -> ( N lcm 0 ) = 0 )
9 7 8 eqtrd 
 |-  ( N e. ZZ -> ( 0 lcm N ) = 0 )
10 4 9 sylan9eqr 
 |-  ( ( N e. ZZ /\ M = 0 ) -> ( M lcm N ) = 0 )
11 10 breq1d 
 |-  ( ( N e. ZZ /\ M = 0 ) -> ( ( M lcm N ) || K <-> 0 || K ) )
12 3 11 imbi12d 
 |-  ( ( N e. ZZ /\ M = 0 ) -> ( ( M || K -> ( M lcm N ) || K ) <-> ( 0 || K -> 0 || K ) ) )
13 1 12 mpbiri 
 |-  ( ( N e. ZZ /\ M = 0 ) -> ( M || K -> ( M lcm N ) || K ) )
14 13 3ad2antl3 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ M = 0 ) -> ( M || K -> ( M lcm N ) || K ) )
15 14 adantrd 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ M = 0 ) -> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) )
16 15 ex 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M = 0 -> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) ) )
17 breq1 
 |-  ( N = 0 -> ( N || K <-> 0 || K ) )
18 17 adantl 
 |-  ( ( M e. ZZ /\ N = 0 ) -> ( N || K <-> 0 || K ) )
19 oveq2 
 |-  ( N = 0 -> ( M lcm N ) = ( M lcm 0 ) )
20 lcm0val 
 |-  ( M e. ZZ -> ( M lcm 0 ) = 0 )
21 19 20 sylan9eqr 
 |-  ( ( M e. ZZ /\ N = 0 ) -> ( M lcm N ) = 0 )
22 21 breq1d 
 |-  ( ( M e. ZZ /\ N = 0 ) -> ( ( M lcm N ) || K <-> 0 || K ) )
23 18 22 imbi12d 
 |-  ( ( M e. ZZ /\ N = 0 ) -> ( ( N || K -> ( M lcm N ) || K ) <-> ( 0 || K -> 0 || K ) ) )
24 1 23 mpbiri 
 |-  ( ( M e. ZZ /\ N = 0 ) -> ( N || K -> ( M lcm N ) || K ) )
25 24 3ad2antl2 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ N = 0 ) -> ( N || K -> ( M lcm N ) || K ) )
26 25 adantld 
 |-  ( ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) /\ N = 0 ) -> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) )
27 26 ex 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( N = 0 -> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) ) )
28 neanior 
 |-  ( ( M =/= 0 /\ N =/= 0 ) <-> -. ( M = 0 \/ N = 0 ) )
29 lcmcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) e. NN0 )
30 29 nn0zd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) e. ZZ )
31 dvds0 
 |-  ( ( M lcm N ) e. ZZ -> ( M lcm N ) || 0 )
32 30 31 syl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M lcm N ) || 0 )
33 32 a1d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M || 0 /\ N || 0 ) -> ( M lcm N ) || 0 ) )
34 33 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ K = 0 ) -> ( ( M || 0 /\ N || 0 ) -> ( M lcm N ) || 0 ) )
35 breq2 
 |-  ( K = 0 -> ( M || K <-> M || 0 ) )
36 breq2 
 |-  ( K = 0 -> ( N || K <-> N || 0 ) )
37 35 36 anbi12d 
 |-  ( K = 0 -> ( ( M || K /\ N || K ) <-> ( M || 0 /\ N || 0 ) ) )
38 breq2 
 |-  ( K = 0 -> ( ( M lcm N ) || K <-> ( M lcm N ) || 0 ) )
39 37 38 imbi12d 
 |-  ( K = 0 -> ( ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) <-> ( ( M || 0 /\ N || 0 ) -> ( M lcm N ) || 0 ) ) )
40 39 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ K = 0 ) -> ( ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) <-> ( ( M || 0 /\ N || 0 ) -> ( M lcm N ) || 0 ) ) )
41 34 40 mpbird 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ K = 0 ) -> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) )
42 41 adantrl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ K = 0 ) ) -> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) )
43 42 adantllr 
 |-  ( ( ( ( M e. ZZ /\ M =/= 0 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ K = 0 ) ) -> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) )
44 43 adantlrr 
 |-  ( ( ( ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( K e. ZZ /\ K = 0 ) ) -> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) )
45 44 anassrs 
 |-  ( ( ( ( ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ K e. ZZ ) /\ K = 0 ) -> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) )
46 nnabscl 
 |-  ( ( M e. ZZ /\ M =/= 0 ) -> ( abs ` M ) e. NN )
47 nnabscl 
 |-  ( ( N e. ZZ /\ N =/= 0 ) -> ( abs ` N ) e. NN )
48 nnabscl 
 |-  ( ( K e. ZZ /\ K =/= 0 ) -> ( abs ` K ) e. NN )
49 lcmgcdlem 
 |-  ( ( ( abs ` M ) e. NN /\ ( abs ` N ) e. NN ) -> ( ( ( ( abs ` M ) lcm ( abs ` N ) ) x. ( ( abs ` M ) gcd ( abs ` N ) ) ) = ( abs ` ( ( abs ` M ) x. ( abs ` N ) ) ) /\ ( ( ( abs ` K ) e. NN /\ ( ( abs ` M ) || ( abs ` K ) /\ ( abs ` N ) || ( abs ` K ) ) ) -> ( ( abs ` M ) lcm ( abs ` N ) ) || ( abs ` K ) ) ) )
50 49 simprd 
 |-  ( ( ( abs ` M ) e. NN /\ ( abs ` N ) e. NN ) -> ( ( ( abs ` K ) e. NN /\ ( ( abs ` M ) || ( abs ` K ) /\ ( abs ` N ) || ( abs ` K ) ) ) -> ( ( abs ` M ) lcm ( abs ` N ) ) || ( abs ` K ) ) )
51 48 50 sylani 
 |-  ( ( ( abs ` M ) e. NN /\ ( abs ` N ) e. NN ) -> ( ( ( K e. ZZ /\ K =/= 0 ) /\ ( ( abs ` M ) || ( abs ` K ) /\ ( abs ` N ) || ( abs ` K ) ) ) -> ( ( abs ` M ) lcm ( abs ` N ) ) || ( abs ` K ) ) )
52 46 47 51 syl2an 
 |-  ( ( ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( ( ( K e. ZZ /\ K =/= 0 ) /\ ( ( abs ` M ) || ( abs ` K ) /\ ( abs ` N ) || ( abs ` K ) ) ) -> ( ( abs ` M ) lcm ( abs ` N ) ) || ( abs ` K ) ) )
53 52 expdimp 
 |-  ( ( ( ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( K e. ZZ /\ K =/= 0 ) ) -> ( ( ( abs ` M ) || ( abs ` K ) /\ ( abs ` N ) || ( abs ` K ) ) -> ( ( abs ` M ) lcm ( abs ` N ) ) || ( abs ` K ) ) )
54 dvdsabsb 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> ( M || K <-> M || ( abs ` K ) ) )
55 zabscl 
 |-  ( K e. ZZ -> ( abs ` K ) e. ZZ )
56 absdvdsb 
 |-  ( ( M e. ZZ /\ ( abs ` K ) e. ZZ ) -> ( M || ( abs ` K ) <-> ( abs ` M ) || ( abs ` K ) ) )
57 55 56 sylan2 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> ( M || ( abs ` K ) <-> ( abs ` M ) || ( abs ` K ) ) )
58 54 57 bitrd 
 |-  ( ( M e. ZZ /\ K e. ZZ ) -> ( M || K <-> ( abs ` M ) || ( abs ` K ) ) )
59 58 adantlr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) -> ( M || K <-> ( abs ` M ) || ( abs ` K ) ) )
60 dvdsabsb 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> ( N || K <-> N || ( abs ` K ) ) )
61 absdvdsb 
 |-  ( ( N e. ZZ /\ ( abs ` K ) e. ZZ ) -> ( N || ( abs ` K ) <-> ( abs ` N ) || ( abs ` K ) ) )
62 55 61 sylan2 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> ( N || ( abs ` K ) <-> ( abs ` N ) || ( abs ` K ) ) )
63 60 62 bitrd 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> ( N || K <-> ( abs ` N ) || ( abs ` K ) ) )
64 63 adantll 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) -> ( N || K <-> ( abs ` N ) || ( abs ` K ) ) )
65 59 64 anbi12d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) -> ( ( M || K /\ N || K ) <-> ( ( abs ` M ) || ( abs ` K ) /\ ( abs ` N ) || ( abs ` K ) ) ) )
66 65 bicomd 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) -> ( ( ( abs ` M ) || ( abs ` K ) /\ ( abs ` N ) || ( abs ` K ) ) <-> ( M || K /\ N || K ) ) )
67 lcmabs 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( abs ` M ) lcm ( abs ` N ) ) = ( M lcm N ) )
68 67 breq1d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( abs ` M ) lcm ( abs ` N ) ) || ( abs ` K ) <-> ( M lcm N ) || ( abs ` K ) ) )
69 68 adantr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) -> ( ( ( abs ` M ) lcm ( abs ` N ) ) || ( abs ` K ) <-> ( M lcm N ) || ( abs ` K ) ) )
70 dvdsabsb 
 |-  ( ( ( M lcm N ) e. ZZ /\ K e. ZZ ) -> ( ( M lcm N ) || K <-> ( M lcm N ) || ( abs ` K ) ) )
71 30 70 sylan 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) -> ( ( M lcm N ) || K <-> ( M lcm N ) || ( abs ` K ) ) )
72 69 71 bitr4d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) -> ( ( ( abs ` M ) lcm ( abs ` N ) ) || ( abs ` K ) <-> ( M lcm N ) || K ) )
73 66 72 imbi12d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) -> ( ( ( ( abs ` M ) || ( abs ` K ) /\ ( abs ` N ) || ( abs ` K ) ) -> ( ( abs ` M ) lcm ( abs ` N ) ) || ( abs ` K ) ) <-> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) ) )
74 73 adantrr 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ K =/= 0 ) ) -> ( ( ( ( abs ` M ) || ( abs ` K ) /\ ( abs ` N ) || ( abs ` K ) ) -> ( ( abs ` M ) lcm ( abs ` N ) ) || ( abs ` K ) ) <-> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) ) )
75 74 adantllr 
 |-  ( ( ( ( M e. ZZ /\ M =/= 0 ) /\ N e. ZZ ) /\ ( K e. ZZ /\ K =/= 0 ) ) -> ( ( ( ( abs ` M ) || ( abs ` K ) /\ ( abs ` N ) || ( abs ` K ) ) -> ( ( abs ` M ) lcm ( abs ` N ) ) || ( abs ` K ) ) <-> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) ) )
76 75 adantlrr 
 |-  ( ( ( ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( K e. ZZ /\ K =/= 0 ) ) -> ( ( ( ( abs ` M ) || ( abs ` K ) /\ ( abs ` N ) || ( abs ` K ) ) -> ( ( abs ` M ) lcm ( abs ` N ) ) || ( abs ` K ) ) <-> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) ) )
77 53 76 mpbid 
 |-  ( ( ( ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ ( K e. ZZ /\ K =/= 0 ) ) -> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) )
78 77 anassrs 
 |-  ( ( ( ( ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ K e. ZZ ) /\ K =/= 0 ) -> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) )
79 45 78 pm2.61dane 
 |-  ( ( ( ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) /\ K e. ZZ ) -> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) )
80 79 ex 
 |-  ( ( ( M e. ZZ /\ M =/= 0 ) /\ ( N e. ZZ /\ N =/= 0 ) ) -> ( K e. ZZ -> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) ) )
81 80 an4s 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M =/= 0 /\ N =/= 0 ) ) -> ( K e. ZZ -> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) ) )
82 28 81 sylan2br 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 \/ N = 0 ) ) -> ( K e. ZZ -> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) ) )
83 82 impancom 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) -> ( -. ( M = 0 \/ N = 0 ) -> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) ) )
84 83 3impa 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( -. ( M = 0 \/ N = 0 ) -> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) ) )
85 84 3comr 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( -. ( M = 0 \/ N = 0 ) -> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) ) )
86 16 27 85 ecase3d 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( M || K /\ N || K ) -> ( M lcm N ) || K ) )