This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sumz

Description: Any sum of zero over a summable set is zero. (Contributed by Mario Carneiro, 12-Aug-2013) (Revised by Mario Carneiro, 20-Apr-2014)

Ref Expression
Assertion sumz 
|- ( ( A C_ ( ZZ>= ` M ) \/ A e. Fin ) -> sum_ k e. A 0 = 0 )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
2 simpr 
 |-  ( ( A C_ ( ZZ>= ` M ) /\ M e. ZZ ) -> M e. ZZ )
3 simpl 
 |-  ( ( A C_ ( ZZ>= ` M ) /\ M e. ZZ ) -> A C_ ( ZZ>= ` M ) )
4 c0ex 
 |-  0 e. _V
5 4 fvconst2 
 |-  ( k e. ( ZZ>= ` M ) -> ( ( ( ZZ>= ` M ) X. { 0 } ) ` k ) = 0 )
6 ifid 
 |-  if ( k e. A , 0 , 0 ) = 0
7 5 6 eqtr4di 
 |-  ( k e. ( ZZ>= ` M ) -> ( ( ( ZZ>= ` M ) X. { 0 } ) ` k ) = if ( k e. A , 0 , 0 ) )
8 7 adantl 
 |-  ( ( ( A C_ ( ZZ>= ` M ) /\ M e. ZZ ) /\ k e. ( ZZ>= ` M ) ) -> ( ( ( ZZ>= ` M ) X. { 0 } ) ` k ) = if ( k e. A , 0 , 0 ) )
9 0cnd 
 |-  ( ( ( A C_ ( ZZ>= ` M ) /\ M e. ZZ ) /\ k e. A ) -> 0 e. CC )
10 1 2 3 8 9 zsum 
 |-  ( ( A C_ ( ZZ>= ` M ) /\ M e. ZZ ) -> sum_ k e. A 0 = ( ~~> ` seq M ( + , ( ( ZZ>= ` M ) X. { 0 } ) ) ) )
11 fclim 
 |-  ~~> : dom ~~> --> CC
12 ffun 
 |-  ( ~~> : dom ~~> --> CC -> Fun ~~> )
13 11 12 ax-mp 
 |-  Fun ~~>
14 serclim0 
 |-  ( M e. ZZ -> seq M ( + , ( ( ZZ>= ` M ) X. { 0 } ) ) ~~> 0 )
15 14 adantl 
 |-  ( ( A C_ ( ZZ>= ` M ) /\ M e. ZZ ) -> seq M ( + , ( ( ZZ>= ` M ) X. { 0 } ) ) ~~> 0 )
16 funbrfv 
 |-  ( Fun ~~> -> ( seq M ( + , ( ( ZZ>= ` M ) X. { 0 } ) ) ~~> 0 -> ( ~~> ` seq M ( + , ( ( ZZ>= ` M ) X. { 0 } ) ) ) = 0 ) )
17 13 15 16 mpsyl 
 |-  ( ( A C_ ( ZZ>= ` M ) /\ M e. ZZ ) -> ( ~~> ` seq M ( + , ( ( ZZ>= ` M ) X. { 0 } ) ) ) = 0 )
18 10 17 eqtrd 
 |-  ( ( A C_ ( ZZ>= ` M ) /\ M e. ZZ ) -> sum_ k e. A 0 = 0 )
19 uzf 
 |-  ZZ>= : ZZ --> ~P ZZ
20 19 fdmi 
 |-  dom ZZ>= = ZZ
21 20 eleq2i 
 |-  ( M e. dom ZZ>= <-> M e. ZZ )
22 ndmfv 
 |-  ( -. M e. dom ZZ>= -> ( ZZ>= ` M ) = (/) )
23 21 22 sylnbir 
 |-  ( -. M e. ZZ -> ( ZZ>= ` M ) = (/) )
24 23 sseq2d 
 |-  ( -. M e. ZZ -> ( A C_ ( ZZ>= ` M ) <-> A C_ (/) ) )
25 24 biimpac 
 |-  ( ( A C_ ( ZZ>= ` M ) /\ -. M e. ZZ ) -> A C_ (/) )
26 ss0 
 |-  ( A C_ (/) -> A = (/) )
27 sumeq1 
 |-  ( A = (/) -> sum_ k e. A 0 = sum_ k e. (/) 0 )
28 sum0 
 |-  sum_ k e. (/) 0 = 0
29 27 28 eqtrdi 
 |-  ( A = (/) -> sum_ k e. A 0 = 0 )
30 25 26 29 3syl 
 |-  ( ( A C_ ( ZZ>= ` M ) /\ -. M e. ZZ ) -> sum_ k e. A 0 = 0 )
31 18 30 pm2.61dan 
 |-  ( A C_ ( ZZ>= ` M ) -> sum_ k e. A 0 = 0 )
32 fz1f1o 
 |-  ( A e. Fin -> ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) )
33 eqidd 
 |-  ( k = ( f ` n ) -> 0 = 0 )
34 simpl 
 |-  ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( # ` A ) e. NN )
35 simpr 
 |-  ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> f : ( 1 ... ( # ` A ) ) -1-1-onto-> A )
36 0cnd 
 |-  ( ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ k e. A ) -> 0 e. CC )
37 elfznn 
 |-  ( n e. ( 1 ... ( # ` A ) ) -> n e. NN )
38 4 fvconst2 
 |-  ( n e. NN -> ( ( NN X. { 0 } ) ` n ) = 0 )
39 37 38 syl 
 |-  ( n e. ( 1 ... ( # ` A ) ) -> ( ( NN X. { 0 } ) ` n ) = 0 )
40 39 adantl 
 |-  ( ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) /\ n e. ( 1 ... ( # ` A ) ) ) -> ( ( NN X. { 0 } ) ` n ) = 0 )
41 33 34 35 36 40 fsum 
 |-  ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> sum_ k e. A 0 = ( seq 1 ( + , ( NN X. { 0 } ) ) ` ( # ` A ) ) )
42 nnuz 
 |-  NN = ( ZZ>= ` 1 )
43 42 ser0 
 |-  ( ( # ` A ) e. NN -> ( seq 1 ( + , ( NN X. { 0 } ) ) ` ( # ` A ) ) = 0 )
44 43 adantr 
 |-  ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> ( seq 1 ( + , ( NN X. { 0 } ) ) ` ( # ` A ) ) = 0 )
45 41 44 eqtrd 
 |-  ( ( ( # ` A ) e. NN /\ f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> sum_ k e. A 0 = 0 )
46 45 ex 
 |-  ( ( # ` A ) e. NN -> ( f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> sum_ k e. A 0 = 0 ) )
47 46 exlimdv 
 |-  ( ( # ` A ) e. NN -> ( E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A -> sum_ k e. A 0 = 0 ) )
48 47 imp 
 |-  ( ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) -> sum_ k e. A 0 = 0 )
49 29 48 jaoi 
 |-  ( ( A = (/) \/ ( ( # ` A ) e. NN /\ E. f f : ( 1 ... ( # ` A ) ) -1-1-onto-> A ) ) -> sum_ k e. A 0 = 0 )
50 32 49 syl 
 |-  ( A e. Fin -> sum_ k e. A 0 = 0 )
51 31 50 jaoi 
 |-  ( ( A C_ ( ZZ>= ` M ) \/ A e. Fin ) -> sum_ k e. A 0 = 0 )