Theorem 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	⊢ ( ( ( 𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ∥ ( ( 𝐼 · 𝑀 ) + ( 𝐽 · 𝑁 ) ) ) )

Proof

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