Metamath Proof Explorer

Theorem sum0

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

Ref Expression
Assertion sum0 
|- sum_ k e. (/) A = 0

Proof

Step Hyp Ref Expression
1 nnuz 
 |-  NN = ( ZZ>= ` 1 )
2 1z 
 |-  1 e. ZZ
3 2 a1i 
 |-  ( T. -> 1 e. ZZ )
4 0ss 
 |-  (/) C_ NN
5 4 a1i 
 |-  ( T. -> (/) C_ NN )
6 simpr 
 |-  ( ( T. /\ k e. NN ) -> k e. NN )
7 6 1 eleqtrdi 
 |-  ( ( T. /\ k e. NN ) -> k e. ( ZZ>= ` 1 ) )
8 c0ex 
 |-  0 e. _V
9 8 fvconst2 
 |-  ( k e. ( ZZ>= ` 1 ) -> ( ( ( ZZ>= ` 1 ) X. { 0 } ) ` k ) = 0 )
10 7 9 syl 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( ZZ>= ` 1 ) X. { 0 } ) ` k ) = 0 )
11 noel 
 |-  -. k e. (/)
12 11 iffalsei 
 |-  if ( k e. (/) , A , 0 ) = 0
13 10 12 eqtr4di 
 |-  ( ( T. /\ k e. NN ) -> ( ( ( ZZ>= ` 1 ) X. { 0 } ) ` k ) = if ( k e. (/) , A , 0 ) )
14 11 pm2.21i 
 |-  ( k e. (/) -> A e. CC )
15 14 adantl 
 |-  ( ( T. /\ k e. (/) ) -> A e. CC )
16 1 3 5 13 15 zsum 
 |-  ( T. -> sum_ k e. (/) A = ( ~~> ` seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) ) )
17 16 mptru 
 |-  sum_ k e. (/) A = ( ~~> ` seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) )
18 fclim 
 |-  ~~> : dom ~~> --> CC
19 ffun 
 |-  ( ~~> : dom ~~> --> CC -> Fun ~~> )
20 18 19 ax-mp 
 |-  Fun ~~>
21 serclim0 
 |-  ( 1 e. ZZ -> seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) ~~> 0 )
22 2 21 ax-mp 
 |-  seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) ~~> 0
23 funbrfv 
 |-  ( Fun ~~> -> ( seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) ~~> 0 -> ( ~~> ` seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) ) = 0 ) )
24 20 22 23 mp2 
 |-  ( ~~> ` seq 1 ( + , ( ( ZZ>= ` 1 ) X. { 0 } ) ) ) = 0
25 17 24 eqtri 
 |-  sum_ k e. (/) A = 0