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 
|- ( ph -> A e. Fin )
fsumdvds.2 
|- ( ph -> N e. ZZ )
fsumdvds.3 
|- ( ( ph /\ k e. A ) -> B e. ZZ )
fsumdvds.4 
|- ( ( ph /\ k e. A ) -> N || B )
Assertion fsumdvds 
|- ( ph -> N || sum_ k e. A B )

Proof

Step Hyp Ref Expression
1 fsumdvds.1 
 |-  ( ph -> A e. Fin )
2 fsumdvds.2 
 |-  ( ph -> N e. ZZ )
3 fsumdvds.3 
 |-  ( ( ph /\ k e. A ) -> B e. ZZ )
4 fsumdvds.4 
 |-  ( ( ph /\ k e. A ) -> N || B )
5 0z 
 |-  0 e. ZZ
6 dvds0 
 |-  ( 0 e. ZZ -> 0 || 0 )
7 5 6 mp1i 
 |-  ( ( ph /\ N = 0 ) -> 0 || 0 )
8 simpr 
 |-  ( ( ph /\ N = 0 ) -> N = 0 )
9 simplr 
 |-  ( ( ( ph /\ N = 0 ) /\ k e. A ) -> N = 0 )
10 4 adantlr 
 |-  ( ( ( ph /\ N = 0 ) /\ k e. A ) -> N || B )
11 9 10 eqbrtrrd 
 |-  ( ( ( ph /\ N = 0 ) /\ k e. A ) -> 0 || B )
12 3 adantlr 
 |-  ( ( ( ph /\ N = 0 ) /\ k e. A ) -> B e. ZZ )
13 0dvds 
 |-  ( B e. ZZ -> ( 0 || B <-> B = 0 ) )
14 12 13 syl 
 |-  ( ( ( ph /\ N = 0 ) /\ k e. A ) -> ( 0 || B <-> B = 0 ) )
15 11 14 mpbid 
 |-  ( ( ( ph /\ N = 0 ) /\ k e. A ) -> B = 0 )
16 15 sumeq2dv 
 |-  ( ( ph /\ N = 0 ) -> sum_ k e. A B = sum_ k e. A 0 )
17 1 adantr 
 |-  ( ( ph /\ N = 0 ) -> A e. Fin )
18 17 olcd 
 |-  ( ( ph /\ N = 0 ) -> ( A C_ ( ZZ>= ` 0 ) \/ A e. Fin ) )
19 sumz 
 |-  ( ( A C_ ( ZZ>= ` 0 ) \/ A e. Fin ) -> sum_ k e. A 0 = 0 )
20 18 19 syl 
 |-  ( ( ph /\ N = 0 ) -> sum_ k e. A 0 = 0 )
21 16 20 eqtrd 
 |-  ( ( ph /\ N = 0 ) -> sum_ k e. A B = 0 )
22 7 8 21 3brtr4d 
 |-  ( ( ph /\ N = 0 ) -> N || sum_ k e. A B )
23 1 adantr 
 |-  ( ( ph /\ N =/= 0 ) -> A e. Fin )
24 2 adantr 
 |-  ( ( ph /\ N =/= 0 ) -> N e. ZZ )
25 24 zcnd 
 |-  ( ( ph /\ N =/= 0 ) -> N e. CC )
26 3 adantlr 
 |-  ( ( ( ph /\ N =/= 0 ) /\ k e. A ) -> B e. ZZ )
27 26 zcnd 
 |-  ( ( ( ph /\ N =/= 0 ) /\ k e. A ) -> B e. CC )
28 simpr 
 |-  ( ( ph /\ N =/= 0 ) -> N =/= 0 )
29 23 25 27 28 fsumdivc 
 |-  ( ( ph /\ N =/= 0 ) -> ( sum_ k e. A B / N ) = sum_ k e. A ( B / N ) )
30 4 adantlr 
 |-  ( ( ( ph /\ N =/= 0 ) /\ k e. A ) -> N || B )
31 24 adantr 
 |-  ( ( ( ph /\ N =/= 0 ) /\ k e. A ) -> N e. ZZ )
32 simplr 
 |-  ( ( ( ph /\ N =/= 0 ) /\ k e. A ) -> N =/= 0 )
33 dvdsval2 
 |-  ( ( N e. ZZ /\ N =/= 0 /\ B e. ZZ ) -> ( N || B <-> ( B / N ) e. ZZ ) )
34 31 32 26 33 syl3anc 
 |-  ( ( ( ph /\ N =/= 0 ) /\ k e. A ) -> ( N || B <-> ( B / N ) e. ZZ ) )
35 30 34 mpbid 
 |-  ( ( ( ph /\ N =/= 0 ) /\ k e. A ) -> ( B / N ) e. ZZ )
36 23 35 fsumzcl 
 |-  ( ( ph /\ N =/= 0 ) -> sum_ k e. A ( B / N ) e. ZZ )
37 29 36 eqeltrd 
 |-  ( ( ph /\ N =/= 0 ) -> ( sum_ k e. A B / N ) e. ZZ )
38 1 3 fsumzcl 
 |-  ( ph -> sum_ k e. A B e. ZZ )
39 38 adantr 
 |-  ( ( ph /\ N =/= 0 ) -> sum_ k e. A B e. ZZ )
40 dvdsval2 
 |-  ( ( N e. ZZ /\ N =/= 0 /\ sum_ k e. A B e. ZZ ) -> ( N || sum_ k e. A B <-> ( sum_ k e. A B / N ) e. ZZ ) )
41 24 28 39 40 syl3anc 
 |-  ( ( ph /\ N =/= 0 ) -> ( N || sum_ k e. A B <-> ( sum_ k e. A B / N ) e. ZZ ) )
42 37 41 mpbird 
 |-  ( ( ph /\ N =/= 0 ) -> N || sum_ k e. A B )
43 22 42 pm2.61dane 
 |-  ( ph -> N || sum_ k e. A B )