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 k A = 0

Proof

Step Hyp Ref Expression
1 nnuz = 1
2 1z 1
3 2 a1i 1
4 0ss
5 4 a1i
6 simpr k k
7 6 1 eleqtrdi k k 1
8 c0ex 0 V
9 8 fvconst2 k 1 1 × 0 k = 0
10 7 9 syl k 1 × 0 k = 0
11 noel ¬ k
12 11 iffalsei if k A 0 = 0
13 10 12 syl6eqr k 1 × 0 k = if k A 0
14 11 pm2.21i k A
15 14 adantl k A
16 1 3 5 13 15 zsum k A = seq 1 + 1 × 0
17 16 mptru k A = seq 1 + 1 × 0
18 fclim : dom
19 ffun : dom Fun
20 18 19 ax-mp Fun
21 serclim0 1 seq 1 + 1 × 0 0
22 2 21 ax-mp seq 1 + 1 × 0 0
23 funbrfv Fun seq 1 + 1 × 0 0 seq 1 + 1 × 0 = 0
24 20 22 23 mp2 seq 1 + 1 × 0 = 0
25 17 24 eqtri k A = 0