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