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 ( ( 𝐴 ⊆ ( ℤ𝑀 ) ∨ 𝐴 ∈ Fin ) → Σ 𝑘𝐴 0 = 0 )

Proof

Step Hyp Ref Expression
1 eqid ( ℤ𝑀 ) = ( ℤ𝑀 )
2 simpr ( ( 𝐴 ⊆ ( ℤ𝑀 ) ∧ 𝑀 ∈ ℤ ) → 𝑀 ∈ ℤ )
3 simpl ( ( 𝐴 ⊆ ( ℤ𝑀 ) ∧ 𝑀 ∈ ℤ ) → 𝐴 ⊆ ( ℤ𝑀 ) )
4 c0ex 0 ∈ V
5 4 fvconst2 ( 𝑘 ∈ ( ℤ𝑀 ) → ( ( ( ℤ𝑀 ) × { 0 } ) ‘ 𝑘 ) = 0 )
6 ifid if ( 𝑘𝐴 , 0 , 0 ) = 0
7 5 6 eqtr4di ( 𝑘 ∈ ( ℤ𝑀 ) → ( ( ( ℤ𝑀 ) × { 0 } ) ‘ 𝑘 ) = if ( 𝑘𝐴 , 0 , 0 ) )
8 7 adantl ( ( ( 𝐴 ⊆ ( ℤ𝑀 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑘 ∈ ( ℤ𝑀 ) ) → ( ( ( ℤ𝑀 ) × { 0 } ) ‘ 𝑘 ) = if ( 𝑘𝐴 , 0 , 0 ) )
9 0cnd ( ( ( 𝐴 ⊆ ( ℤ𝑀 ) ∧ 𝑀 ∈ ℤ ) ∧ 𝑘𝐴 ) → 0 ∈ ℂ )
10 1 2 3 8 9 zsum ( ( 𝐴 ⊆ ( ℤ𝑀 ) ∧ 𝑀 ∈ ℤ ) → Σ 𝑘𝐴 0 = ( ⇝ ‘ seq 𝑀 ( + , ( ( ℤ𝑀 ) × { 0 } ) ) ) )
11 fclim ⇝ : dom ⇝ ⟶ ℂ
12 ffun ( ⇝ : dom ⇝ ⟶ ℂ → Fun ⇝ )
13 11 12 ax-mp Fun ⇝
14 serclim0 ( 𝑀 ∈ ℤ → seq 𝑀 ( + , ( ( ℤ𝑀 ) × { 0 } ) ) ⇝ 0 )
15 14 adantl ( ( 𝐴 ⊆ ( ℤ𝑀 ) ∧ 𝑀 ∈ ℤ ) → seq 𝑀 ( + , ( ( ℤ𝑀 ) × { 0 } ) ) ⇝ 0 )
16 funbrfv ( Fun ⇝ → ( seq 𝑀 ( + , ( ( ℤ𝑀 ) × { 0 } ) ) ⇝ 0 → ( ⇝ ‘ seq 𝑀 ( + , ( ( ℤ𝑀 ) × { 0 } ) ) ) = 0 ) )
17 13 15 16 mpsyl ( ( 𝐴 ⊆ ( ℤ𝑀 ) ∧ 𝑀 ∈ ℤ ) → ( ⇝ ‘ seq 𝑀 ( + , ( ( ℤ𝑀 ) × { 0 } ) ) ) = 0 )
18 10 17 eqtrd ( ( 𝐴 ⊆ ( ℤ𝑀 ) ∧ 𝑀 ∈ ℤ ) → Σ 𝑘𝐴 0 = 0 )
19 uzf : ℤ ⟶ 𝒫 ℤ
20 19 fdmi dom ℤ = ℤ
21 20 eleq2i ( 𝑀 ∈ dom ℤ𝑀 ∈ ℤ )
22 ndmfv ( ¬ 𝑀 ∈ dom ℤ → ( ℤ𝑀 ) = ∅ )
23 21 22 sylnbir ( ¬ 𝑀 ∈ ℤ → ( ℤ𝑀 ) = ∅ )
24 23 sseq2d ( ¬ 𝑀 ∈ ℤ → ( 𝐴 ⊆ ( ℤ𝑀 ) ↔ 𝐴 ⊆ ∅ ) )
25 24 biimpac ( ( 𝐴 ⊆ ( ℤ𝑀 ) ∧ ¬ 𝑀 ∈ ℤ ) → 𝐴 ⊆ ∅ )
26 ss0 ( 𝐴 ⊆ ∅ → 𝐴 = ∅ )
27 sumeq1 ( 𝐴 = ∅ → Σ 𝑘𝐴 0 = Σ 𝑘 ∈ ∅ 0 )
28 sum0 Σ 𝑘 ∈ ∅ 0 = 0
29 27 28 eqtrdi ( 𝐴 = ∅ → Σ 𝑘𝐴 0 = 0 )
30 25 26 29 3syl ( ( 𝐴 ⊆ ( ℤ𝑀 ) ∧ ¬ 𝑀 ∈ ℤ ) → Σ 𝑘𝐴 0 = 0 )
31 18 30 pm2.61dan ( 𝐴 ⊆ ( ℤ𝑀 ) → Σ 𝑘𝐴 0 = 0 )
32 fz1f1o ( 𝐴 ∈ Fin → ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) )
33 eqidd ( 𝑘 = ( 𝑓𝑛 ) → 0 = 0 )
34 simpl ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) → ( ♯ ‘ 𝐴 ) ∈ ℕ )
35 simpr ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 )
36 0cnd ( ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ∧ 𝑘𝐴 ) → 0 ∈ ℂ )
37 elfznn ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → 𝑛 ∈ ℕ )
38 4 fvconst2 ( 𝑛 ∈ ℕ → ( ( ℕ × { 0 } ) ‘ 𝑛 ) = 0 )
39 37 38 syl ( 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) → ( ( ℕ × { 0 } ) ‘ 𝑛 ) = 0 )
40 39 adantl ( ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ∧ 𝑛 ∈ ( 1 ... ( ♯ ‘ 𝐴 ) ) ) → ( ( ℕ × { 0 } ) ‘ 𝑛 ) = 0 )
41 33 34 35 36 40 fsum ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) → Σ 𝑘𝐴 0 = ( seq 1 ( + , ( ℕ × { 0 } ) ) ‘ ( ♯ ‘ 𝐴 ) ) )
42 nnuz ℕ = ( ℤ ‘ 1 )
43 42 ser0 ( ( ♯ ‘ 𝐴 ) ∈ ℕ → ( seq 1 ( + , ( ℕ × { 0 } ) ) ‘ ( ♯ ‘ 𝐴 ) ) = 0 )
44 43 adantr ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) → ( seq 1 ( + , ( ℕ × { 0 } ) ) ‘ ( ♯ ‘ 𝐴 ) ) = 0 )
45 41 44 eqtrd ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) → Σ 𝑘𝐴 0 = 0 )
46 45 ex ( ( ♯ ‘ 𝐴 ) ∈ ℕ → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 → Σ 𝑘𝐴 0 = 0 ) )
47 46 exlimdv ( ( ♯ ‘ 𝐴 ) ∈ ℕ → ( ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 → Σ 𝑘𝐴 0 = 0 ) )
48 47 imp ( ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) → Σ 𝑘𝐴 0 = 0 )
49 29 48 jaoi ( ( 𝐴 = ∅ ∨ ( ( ♯ ‘ 𝐴 ) ∈ ℕ ∧ ∃ 𝑓 𝑓 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) ) → Σ 𝑘𝐴 0 = 0 )
50 32 49 syl ( 𝐴 ∈ Fin → Σ 𝑘𝐴 0 = 0 )
51 31 50 jaoi ( ( 𝐴 ⊆ ( ℤ𝑀 ) ∨ 𝐴 ∈ Fin ) → Σ 𝑘𝐴 0 = 0 )