dvdsmulcr

Description: Cancellation law for the divides relation. (Contributed by Paul Chapman, 21-Mar-2011)

		Ref	Expression
	Assertion	dvdsmulcr	$⊢ (M \in ℤ \land N \in ℤ \land (K \in ℤ \land K \neq 0)) \to (M K ∥ N K \leftrightarrow M ∥ N)$

Proof

Step	Hyp	Ref	Expression
1		zmulcl	$⊢ (M \in ℤ \land K \in ℤ) \to M K \in ℤ$
2	1	3adant2	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to M K \in ℤ$
3		zmulcl	$⊢ (N \in ℤ \land K \in ℤ) \to N K \in ℤ$
4	3	3adant1	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to N K \in ℤ$
5	2 4	jca	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (M K \in ℤ \land N K \in ℤ)$
6	5	3adant3r	$⊢ (M \in ℤ \land N \in ℤ \land (K \in ℤ \land K \neq 0)) \to (M K \in ℤ \land N K \in ℤ)$
7		3simpa	$⊢ (M \in ℤ \land N \in ℤ \land (K \in ℤ \land K \neq 0)) \to (M \in ℤ \land N \in ℤ)$
8		simpr	$⊢ ((M \in ℤ \land N \in ℤ \land (K \in ℤ \land K \neq 0)) \land x \in ℤ) \to x \in ℤ$
9		zcn	$⊢ x \in ℤ \to x \in ℂ$
10		zcn	$⊢ M \in ℤ \to M \in ℂ$
11	9 10	anim12i	$⊢ (x \in ℤ \land M \in ℤ) \to (x \in ℂ \land M \in ℂ)$
12		zcn	$⊢ N \in ℤ \to N \in ℂ$
13		zcn	$⊢ K \in ℤ \to K \in ℂ$
14	13	anim1i	$⊢ (K \in ℤ \land K \neq 0) \to (K \in ℂ \land K \neq 0)$
15		mulass	$⊢ (x \in ℂ \land M \in ℂ \land K \in ℂ) \to x \cdot M K = x M K$
16	15	3expa	$⊢ ((x \in ℂ \land M \in ℂ) \land K \in ℂ) \to x \cdot M K = x M K$
17	16	adantrr	$⊢ ((x \in ℂ \land M \in ℂ) \land (K \in ℂ \land K \neq 0)) \to x \cdot M K = x M K$
18	17	3adant2	$⊢ ((x \in ℂ \land M \in ℂ) \land N \in ℂ \land (K \in ℂ \land K \neq 0)) \to x \cdot M K = x M K$
19	18	eqeq1d	$⊢ ((x \in ℂ \land M \in ℂ) \land N \in ℂ \land (K \in ℂ \land K \neq 0)) \to (x \cdot M K = N K \leftrightarrow x M K = N K)$
20		mulcl	$⊢ (x \in ℂ \land M \in ℂ) \to x \cdot M \in ℂ$
21		mulcan2	$⊢ (x \cdot M \in ℂ \land N \in ℂ \land (K \in ℂ \land K \neq 0)) \to (x \cdot M K = N K \leftrightarrow x \cdot M = N)$
22	20 21	syl3an1	$⊢ ((x \in ℂ \land M \in ℂ) \land N \in ℂ \land (K \in ℂ \land K \neq 0)) \to (x \cdot M K = N K \leftrightarrow x \cdot M = N)$
23	19 22	bitr3d	$⊢ ((x \in ℂ \land M \in ℂ) \land N \in ℂ \land (K \in ℂ \land K \neq 0)) \to (x M K = N K \leftrightarrow x \cdot M = N)$
24	11 12 14 23	syl3an	$⊢ ((x \in ℤ \land M \in ℤ) \land N \in ℤ \land (K \in ℤ \land K \neq 0)) \to (x M K = N K \leftrightarrow x \cdot M = N)$
25	24	3expb	$⊢ ((x \in ℤ \land M \in ℤ) \land (N \in ℤ \land (K \in ℤ \land K \neq 0))) \to (x M K = N K \leftrightarrow x \cdot M = N)$
26	25	3impa	$⊢ (x \in ℤ \land M \in ℤ \land (N \in ℤ \land (K \in ℤ \land K \neq 0))) \to (x M K = N K \leftrightarrow x \cdot M = N)$
27	26	3coml	$⊢ (M \in ℤ \land (N \in ℤ \land (K \in ℤ \land K \neq 0)) \land x \in ℤ) \to (x M K = N K \leftrightarrow x \cdot M = N)$
28	27	3expia	$⊢ (M \in ℤ \land (N \in ℤ \land (K \in ℤ \land K \neq 0))) \to (x \in ℤ \to (x M K = N K \leftrightarrow x \cdot M = N))$
29	28	3impb	$⊢ (M \in ℤ \land N \in ℤ \land (K \in ℤ \land K \neq 0)) \to (x \in ℤ \to (x M K = N K \leftrightarrow x \cdot M = N))$
30	29	imp	$⊢ ((M \in ℤ \land N \in ℤ \land (K \in ℤ \land K \neq 0)) \land x \in ℤ) \to (x M K = N K \leftrightarrow x \cdot M = N)$
31	30	biimpd	$⊢ ((M \in ℤ \land N \in ℤ \land (K \in ℤ \land K \neq 0)) \land x \in ℤ) \to (x M K = N K \to x \cdot M = N)$
32	6 7 8 31	dvds1lem	$⊢ (M \in ℤ \land N \in ℤ \land (K \in ℤ \land K \neq 0)) \to (M K ∥ N K \to M ∥ N)$
33		dvdsmulc	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \to (M ∥ N \to M K ∥ N K)$
34	33	3adant3r	$⊢ (M \in ℤ \land N \in ℤ \land (K \in ℤ \land K \neq 0)) \to (M ∥ N \to M K ∥ N K)$
35	32 34	impbid	$⊢ (M \in ℤ \land N \in ℤ \land (K \in ℤ \land K \neq 0)) \to (M K ∥ N K \leftrightarrow M ∥ N)$

Metamath Proof Explorer

Theorem dvdsmulcr

Proof