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

Proof

Step Hyp Ref Expression
1 eqid M = M
2 simpr A M M M
3 simpl A M M A M
4 c0ex 0 V
5 4 fvconst2 k M M × 0 k = 0
6 ifid if k A 0 0 = 0
7 5 6 syl6eqr k M M × 0 k = if k A 0 0
8 7 adantl A M M k M M × 0 k = if k A 0 0
9 0cnd A M M k A 0
10 1 2 3 8 9 zsum A M M k A 0 = seq M + M × 0
11 fclim : dom
12 ffun : dom Fun
13 11 12 ax-mp Fun
14 serclim0 M seq M + M × 0 0
15 14 adantl A M M seq M + M × 0 0
16 funbrfv Fun seq M + M × 0 0 seq M + M × 0 = 0
17 13 15 16 mpsyl A M M seq M + M × 0 = 0
18 10 17 eqtrd A M M k A 0 = 0
19 uzf : 𝒫
20 19 fdmi dom =
21 20 eleq2i M dom M
22 ndmfv ¬ M dom M =
23 21 22 sylnbir ¬ M M =
24 23 sseq2d ¬ M A M A
25 24 biimpac A M ¬ M A
26 ss0 A A =
27 sumeq1 A = k A 0 = k 0
28 sum0 k 0 = 0
29 27 28 syl6eq A = k A 0 = 0
30 25 26 29 3syl A M ¬ M k A 0 = 0
31 18 30 pm2.61dan A M k A 0 = 0
32 fz1f1o A Fin A = A f f : 1 A 1-1 onto A
33 eqidd k = f n 0 = 0
34 simpl A f : 1 A 1-1 onto A A
35 simpr A f : 1 A 1-1 onto A f : 1 A 1-1 onto A
36 0cnd A f : 1 A 1-1 onto A k A 0
37 elfznn n 1 A n
38 4 fvconst2 n × 0 n = 0
39 37 38 syl n 1 A × 0 n = 0
40 39 adantl A f : 1 A 1-1 onto A n 1 A × 0 n = 0
41 33 34 35 36 40 fsum A f : 1 A 1-1 onto A k A 0 = seq 1 + × 0 A
42 nnuz = 1
43 42 ser0 A seq 1 + × 0 A = 0
44 43 adantr A f : 1 A 1-1 onto A seq 1 + × 0 A = 0
45 41 44 eqtrd A f : 1 A 1-1 onto A k A 0 = 0
46 45 ex A f : 1 A 1-1 onto A k A 0 = 0
47 46 exlimdv A f f : 1 A 1-1 onto A k A 0 = 0
48 47 imp A f f : 1 A 1-1 onto A k A 0 = 0
49 29 48 jaoi A = A f f : 1 A 1-1 onto A k A 0 = 0
50 32 49 syl A Fin k A 0 = 0
51 31 50 jaoi A M A Fin k A 0 = 0