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	$⊢ (M \in ℤ \land N \in ℤ \land (K \in ℤ \land K \neq 0)) \to (K \cdot M ∥ K \cdot N \leftrightarrow M ∥ N)$

Proof

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

Metamath Proof Explorer

Theorem dvdscmulr

Proof