Metamath Proof Explorer


Theorem fsumdvds

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 φAFin
fsumdvds.2 φN
fsumdvds.3 φkAB
fsumdvds.4 φkANB
Assertion fsumdvds φNkAB

Proof

Step Hyp Ref Expression
1 fsumdvds.1 φAFin
2 fsumdvds.2 φN
3 fsumdvds.3 φkAB
4 fsumdvds.4 φkANB
5 0z 0
6 dvds0 000
7 5 6 mp1i φN=000
8 simpr φN=0N=0
9 simplr φN=0kAN=0
10 4 adantlr φN=0kANB
11 9 10 eqbrtrrd φN=0kA0B
12 3 adantlr φN=0kAB
13 0dvds B0BB=0
14 12 13 syl φN=0kA0BB=0
15 11 14 mpbid φN=0kAB=0
16 15 sumeq2dv φN=0kAB=kA0
17 1 adantr φN=0AFin
18 17 olcd φN=0A0AFin
19 sumz A0AFinkA0=0
20 18 19 syl φN=0kA0=0
21 16 20 eqtrd φN=0kAB=0
22 7 8 21 3brtr4d φN=0NkAB
23 1 adantr φN0AFin
24 2 adantr φN0N
25 24 zcnd φN0N
26 3 adantlr φN0kAB
27 26 zcnd φN0kAB
28 simpr φN0N0
29 23 25 27 28 fsumdivc φN0kABN=kABN
30 4 adantlr φN0kANB
31 24 adantr φN0kAN
32 simplr φN0kAN0
33 dvdsval2 NN0BNBBN
34 31 32 26 33 syl3anc φN0kANBBN
35 30 34 mpbid φN0kABN
36 23 35 fsumzcl φN0kABN
37 29 36 eqeltrd φN0kABN
38 1 3 fsumzcl φkAB
39 38 adantr φN0kAB
40 dvdsval2 NN0kABNkABkABN
41 24 28 39 40 syl3anc φN0NkABkABN
42 37 41 mpbird φN0NkAB
43 22 42 pm2.61dane φNkAB