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 
|- ( ( ( I e. ZZ /\ J e. ZZ ) /\ ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) ) -> ( ( K || M /\ K || N ) -> K || ( ( I x. M ) + ( J x. N ) ) ) )

Proof

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