Metamath Proof Explorer

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