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 )