# 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 Σ 𝑘 ∈ ∅ 𝐴 = 0

### Proof

Step Hyp Ref Expression
1 nnuz ℕ = ( ℤ ‘ 1 )
2 1z 1 ∈ ℤ
3 2 a1i ( ⊤ → 1 ∈ ℤ )
4 0ss ∅ ⊆ ℕ
5 4 a1i ( ⊤ → ∅ ⊆ ℕ )
6 simpr ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
7 6 1 eleqtrdi ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ( ℤ ‘ 1 ) )
8 c0ex 0 ∈ V
9 8 fvconst2 ( 𝑘 ∈ ( ℤ ‘ 1 ) → ( ( ( ℤ ‘ 1 ) × { 0 } ) ‘ 𝑘 ) = 0 )
10 7 9 syl ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( ( ℤ ‘ 1 ) × { 0 } ) ‘ 𝑘 ) = 0 )
11 noel ¬ 𝑘 ∈ ∅
12 11 iffalsei if ( 𝑘 ∈ ∅ , 𝐴 , 0 ) = 0
13 10 12 eqtr4di ( ( ⊤ ∧ 𝑘 ∈ ℕ ) → ( ( ( ℤ ‘ 1 ) × { 0 } ) ‘ 𝑘 ) = if ( 𝑘 ∈ ∅ , 𝐴 , 0 ) )
14 11 pm2.21i ( 𝑘 ∈ ∅ → 𝐴 ∈ ℂ )
15 14 adantl ( ( ⊤ ∧ 𝑘 ∈ ∅ ) → 𝐴 ∈ ℂ )
16 1 3 5 13 15 zsum ( ⊤ → Σ 𝑘 ∈ ∅ 𝐴 = ( ⇝ ‘ seq 1 ( + , ( ( ℤ ‘ 1 ) × { 0 } ) ) ) )
17 16 mptru Σ 𝑘 ∈ ∅ 𝐴 = ( ⇝ ‘ 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 Σ 𝑘 ∈ ∅ 𝐴 = 0