Description: If every term in a sum is divisible by N , then so is the sum. (Contributed by Mario Carneiro, 17-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fsumdvds.1 | |
|
fsumdvds.2 | |
||
fsumdvds.3 | |
||
fsumdvds.4 | |
||
Assertion | fsumdvds | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fsumdvds.1 | |
|
2 | fsumdvds.2 | |
|
3 | fsumdvds.3 | |
|
4 | fsumdvds.4 | |
|
5 | 0z | |
|
6 | dvds0 | |
|
7 | 5 6 | mp1i | |
8 | simpr | |
|
9 | simplr | |
|
10 | 4 | adantlr | |
11 | 9 10 | eqbrtrrd | |
12 | 3 | adantlr | |
13 | 0dvds | |
|
14 | 12 13 | syl | |
15 | 11 14 | mpbid | |
16 | 15 | sumeq2dv | |
17 | 1 | adantr | |
18 | 17 | olcd | |
19 | sumz | |
|
20 | 18 19 | syl | |
21 | 16 20 | eqtrd | |
22 | 7 8 21 | 3brtr4d | |
23 | 1 | adantr | |
24 | 2 | adantr | |
25 | 24 | zcnd | |
26 | 3 | adantlr | |
27 | 26 | zcnd | |
28 | simpr | |
|
29 | 23 25 27 28 | fsumdivc | |
30 | 4 | adantlr | |
31 | 24 | adantr | |
32 | simplr | |
|
33 | dvdsval2 | |
|
34 | 31 32 26 33 | syl3anc | |
35 | 30 34 | mpbid | |
36 | 23 35 | fsumzcl | |
37 | 29 36 | eqeltrd | |
38 | 1 3 | fsumzcl | |
39 | 38 | adantr | |
40 | dvdsval2 | |
|
41 | 24 28 39 40 | syl3anc | |
42 | 37 41 | mpbird | |
43 | 22 42 | pm2.61dane | |