# 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 )`
` |-  ( ( 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`