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 ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) → ( 𝑀 lcm 𝑁 ) ∥ 𝐾 ) )

Proof

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