This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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