dvds2ln

Description: If an integer divides each of two other integers, it divides any linear combination of them. Theorem 1.1(c) in ApostolNT p. 14 (linearity property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011)

		Ref	Expression
	Assertion	dvds2ln	$⊢ ((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \to ((K ∥ M \land K ∥ N) \to K ∥ (I \cdot M + J \cdot N))$

Proof

Step	Hyp	Ref	Expression
1		simpr1	$⊢ ((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \to K \in ℤ$
2		simpr2	$⊢ ((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \to M \in ℤ$
3	1 2	jca	$⊢ ((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \to (K \in ℤ \land M \in ℤ)$
4		simpr3	$⊢ ((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \to N \in ℤ$
5	1 4	jca	$⊢ ((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \to (K \in ℤ \land N \in ℤ)$
6		simpll	$⊢ ((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \to I \in ℤ$
7	6 2	zmulcld	$⊢ ((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \to I \cdot M \in ℤ$
8		simplr	$⊢ ((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \to J \in ℤ$
9	8 4	zmulcld	$⊢ ((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \to J \cdot N \in ℤ$
10	7 9	zaddcld	$⊢ ((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \to I \cdot M + J \cdot N \in ℤ$
11	1 10	jca	$⊢ ((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \to (K \in ℤ \land I \cdot M + J \cdot N \in ℤ)$
12		zmulcl	$⊢ (x \in ℤ \land I \in ℤ) \to x \cdot I \in ℤ$
13		zmulcl	$⊢ (y \in ℤ \land J \in ℤ) \to y \cdot J \in ℤ$
14	12 13	anim12i	$⊢ ((x \in ℤ \land I \in ℤ) \land (y \in ℤ \land J \in ℤ)) \to (x \cdot I \in ℤ \land y \cdot J \in ℤ)$
15	14	an4s	$⊢ ((x \in ℤ \land y \in ℤ) \land (I \in ℤ \land J \in ℤ)) \to (x \cdot I \in ℤ \land y \cdot J \in ℤ)$
16	15	expcom	$⊢ (I \in ℤ \land J \in ℤ) \to ((x \in ℤ \land y \in ℤ) \to (x \cdot I \in ℤ \land y \cdot J \in ℤ))$
17	16	adantr	$⊢ ((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \to ((x \in ℤ \land y \in ℤ) \to (x \cdot I \in ℤ \land y \cdot J \in ℤ))$
18	17	imp	$⊢ (((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \land (x \in ℤ \land y \in ℤ)) \to (x \cdot I \in ℤ \land y \cdot J \in ℤ)$
19		zaddcl	$⊢ (x \cdot I \in ℤ \land y \cdot J \in ℤ) \to x \cdot I + y \cdot J \in ℤ$
20	18 19	syl	$⊢ (((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \land (x \in ℤ \land y \in ℤ)) \to x \cdot I + y \cdot J \in ℤ$
21		zcn	$⊢ x \cdot I \in ℤ \to x \cdot I \in ℂ$
22		zcn	$⊢ y \cdot J \in ℤ \to y \cdot J \in ℂ$
23	21 22	anim12i	$⊢ (x \cdot I \in ℤ \land y \cdot J \in ℤ) \to (x \cdot I \in ℂ \land y \cdot J \in ℂ)$
24	18 23	syl	$⊢ (((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \land (x \in ℤ \land y \in ℤ)) \to (x \cdot I \in ℂ \land y \cdot J \in ℂ)$
25	1	zcnd	$⊢ ((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \to K \in ℂ$
26	25	adantr	$⊢ (((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \land (x \in ℤ \land y \in ℤ)) \to K \in ℂ$
27		adddir	$⊢ (x \cdot I \in ℂ \land y \cdot J \in ℂ \land K \in ℂ) \to (x \cdot I + y \cdot J) K = x \cdot I K + y \cdot J K$
28	27	3expa	$⊢ ((x \cdot I \in ℂ \land y \cdot J \in ℂ) \land K \in ℂ) \to (x \cdot I + y \cdot J) K = x \cdot I K + y \cdot J K$
29	24 26 28	syl2anc	$⊢ (((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \land (x \in ℤ \land y \in ℤ)) \to (x \cdot I + y \cdot J) K = x \cdot I K + y \cdot J K$
30		zcn	$⊢ x \in ℤ \to x \in ℂ$
31	30	adantr	$⊢ (x \in ℤ \land y \in ℤ) \to x \in ℂ$
32	31	adantl	$⊢ (((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \land (x \in ℤ \land y \in ℤ)) \to x \in ℂ$
33		zcn	$⊢ I \in ℤ \to I \in ℂ$
34	33	ad3antrrr	$⊢ (((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \land (x \in ℤ \land y \in ℤ)) \to I \in ℂ$
35	32 34 26	mul32d	$⊢ (((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \land (x \in ℤ \land y \in ℤ)) \to x \cdot I K = x K \cdot I$
36		zcn	$⊢ y \in ℤ \to y \in ℂ$
37	36	adantl	$⊢ (x \in ℤ \land y \in ℤ) \to y \in ℂ$
38	37	adantl	$⊢ (((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \land (x \in ℤ \land y \in ℤ)) \to y \in ℂ$
39	8	zcnd	$⊢ ((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \to J \in ℂ$
40	39	adantr	$⊢ (((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \land (x \in ℤ \land y \in ℤ)) \to J \in ℂ$
41	38 40 26	mul32d	$⊢ (((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \land (x \in ℤ \land y \in ℤ)) \to y \cdot J K = y K \cdot J$
42	35 41	oveq12d	$⊢ (((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \land (x \in ℤ \land y \in ℤ)) \to x \cdot I K + y \cdot J K = x K \cdot I + y K \cdot J$
43	32 26	mulcld	$⊢ (((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \land (x \in ℤ \land y \in ℤ)) \to x K \in ℂ$
44	43 34	mulcomd	$⊢ (((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \land (x \in ℤ \land y \in ℤ)) \to x K \cdot I = I x K$
45	38 26	mulcld	$⊢ (((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \land (x \in ℤ \land y \in ℤ)) \to y K \in ℂ$
46	45 40	mulcomd	$⊢ (((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \land (x \in ℤ \land y \in ℤ)) \to y K \cdot J = J y K$
47	44 46	oveq12d	$⊢ (((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \land (x \in ℤ \land y \in ℤ)) \to x K \cdot I + y K \cdot J = I x K + J y K$
48	29 42 47	3eqtrd	$⊢ (((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \land (x \in ℤ \land y \in ℤ)) \to (x \cdot I + y \cdot J) K = I x K + J y K$
49		oveq2	$⊢ x K = M \to I x K = I \cdot M$
50		oveq2	$⊢ y K = N \to J y K = J \cdot N$
51	49 50	oveqan12d	$⊢ (x K = M \land y K = N) \to I x K + J y K = I \cdot M + J \cdot N$
52	48 51	sylan9eq	$⊢ ((((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \land (x \in ℤ \land y \in ℤ)) \land (x K = M \land y K = N)) \to (x \cdot I + y \cdot J) K = I \cdot M + J \cdot N$
53	52	ex	$⊢ (((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \land (x \in ℤ \land y \in ℤ)) \to ((x K = M \land y K = N) \to (x \cdot I + y \cdot J) K = I \cdot M + J \cdot N)$
54	3 5 11 20 53	dvds2lem	$⊢ ((I \in ℤ \land J \in ℤ) \land (K \in ℤ \land M \in ℤ \land N \in ℤ)) \to ((K ∥ M \land K ∥ N) \to K ∥ (I \cdot M + J \cdot N))$

Metamath Proof Explorer

Theorem dvds2ln

Proof