Theorem dvdscmulr

Description: Cancellation law for the divides relation. Theorem 1.1(e) in ApostolNT p. 14. (Contributed by Paul Chapman, 21-Mar-2011)

	Ref	Expression
Assertion	dvdscmulr	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) → ( ( 𝐾 · 𝑀 ) ∥ ( 𝐾 · 𝑁 ) ↔ 𝑀 ∥ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		zmulcl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐾 · 𝑀 ) ∈ ℤ )
2	1	3adant3	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · 𝑀 ) ∈ ℤ )
3		zmulcl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · 𝑁 ) ∈ ℤ )
4	3	3adant2	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · 𝑁 ) ∈ ℤ )
5	2 4	jca	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) ∈ ℤ ∧ ( 𝐾 · 𝑁 ) ∈ ℤ ) )
6	5	3coml	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) ∈ ℤ ∧ ( 𝐾 · 𝑁 ) ∈ ℤ ) )
7	6	3adant3r	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) → ( ( 𝐾 · 𝑀 ) ∈ ℤ ∧ ( 𝐾 · 𝑁 ) ∈ ℤ ) )
8		3simpa	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
9		simpr	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) ∧ 𝑥 ∈ ℤ ) → 𝑥 ∈ ℤ )
10		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
11		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
12	10 11	anim12i	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) )
13		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
14		zcn	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
15	14	anim1i	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) → ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) )
16		mul12	⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝐾 · ( 𝑥 · 𝑀 ) ) = ( 𝑥 · ( 𝐾 · 𝑀 ) ) )
17	16	3adant1r	⊢ ( ( ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) ∧ 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝐾 · ( 𝑥 · 𝑀 ) ) = ( 𝑥 · ( 𝐾 · 𝑀 ) ) )
18	17	3expb	⊢ ( ( ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) ) → ( 𝐾 · ( 𝑥 · 𝑀 ) ) = ( 𝑥 · ( 𝐾 · 𝑀 ) ) )
19	18	ancoms	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) ∧ ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) ) → ( 𝐾 · ( 𝑥 · 𝑀 ) ) = ( 𝑥 · ( 𝐾 · 𝑀 ) ) )
20	19	3adant2	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) ∧ 𝑁 ∈ ℂ ∧ ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) ) → ( 𝐾 · ( 𝑥 · 𝑀 ) ) = ( 𝑥 · ( 𝐾 · 𝑀 ) ) )
21	20	eqeq1d	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) ∧ 𝑁 ∈ ℂ ∧ ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) ) → ( ( 𝐾 · ( 𝑥 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ) )
22		mulcl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝑥 · 𝑀 ) ∈ ℂ )
23		mulcan	⊢ ( ( ( 𝑥 · 𝑀 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) ) → ( ( 𝐾 · ( 𝑥 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) )
24	22 23	syl3an1	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) ∧ 𝑁 ∈ ℂ ∧ ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) ) → ( ( 𝐾 · ( 𝑥 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) )
25	21 24	bitr3d	⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) ∧ 𝑁 ∈ ℂ ∧ ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) ) → ( ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) )
26	12 13 15 25	syl3an	⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) → ( ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) )
27	26	3expb	⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) ) → ( ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) )
28	27	3impa	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) ) → ( ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) )
29	28	3coml	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) )
30	29	3expia	⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) ) → ( 𝑥 ∈ ℤ → ( ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) ) )
31	30	3impb	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) → ( 𝑥 ∈ ℤ → ( ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) ) )
32	31	imp	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) )
33	32	biimpd	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) → ( 𝑥 · 𝑀 ) = 𝑁 ) )
34	7 8 9 33	dvds1lem	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) → ( ( 𝐾 · 𝑀 ) ∥ ( 𝐾 · 𝑁 ) → 𝑀 ∥ 𝑁 ) )
35		dvdscmul	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 → ( 𝐾 · 𝑀 ) ∥ ( 𝐾 · 𝑁 ) ) )
36	35	3adant3r	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) → ( 𝑀 ∥ 𝑁 → ( 𝐾 · 𝑀 ) ∥ ( 𝐾 · 𝑁 ) ) )
37	34 36	impbid	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) → ( ( 𝐾 · 𝑀 ) ∥ ( 𝐾 · 𝑁 ) ↔ 𝑀 ∥ 𝑁 ) )