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 eqtr4di ⊢ ⊤ ∧ 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