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 𝑁 ) ∥ 𝐾 ) )