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