Metamath Proof Explorer

Theorem ser0

Description: The value of the partial sums in a zero-valued infinite series. (Contributed by Mario Carneiro, 31-Aug-2013) (Revised by Mario Carneiro, 15-Dec-2014)

		Ref	Expression
	Hypothesis	ser0.1	$⊢ Z = ℤ_{\geq M}$
	Assertion	ser0	$⊢ N \in Z \to seq M (+ (Z \times \{0\})) (N) = 0$

Proof

Step	Hyp	Ref	Expression
1		ser0.1	$⊢ Z = ℤ_{\geq M}$
2		00id	$⊢ 0 + 0 = 0$
3	2	a1i	$⊢ N \in Z \to 0 + 0 = 0$
4	1	eleq2i	$⊢ N \in Z \leftrightarrow N \in ℤ_{\geq M}$
5	4	biimpi	$⊢ N \in Z \to N \in ℤ_{\geq M}$
6		0cn	$⊢ 0 \in ℂ$
7		elfzuz	$⊢ k \in (M \dots N) \to k \in ℤ_{\geq M}$
8	7 1	eleqtrrdi	$⊢ k \in (M \dots N) \to k \in Z$
9	8	adantl	$⊢ (N \in Z \land k \in (M \dots N)) \to k \in Z$
10		fvconst2g	$⊢ (0 \in ℂ \land k \in Z) \to (Z \times \{0\}) (k) = 0$
11	6 9 10	sylancr	$⊢ (N \in Z \land k \in (M \dots N)) \to (Z \times \{0\}) (k) = 0$
12	3 5 11	seqid3	$⊢ N \in Z \to seq M (+ (Z \times \{0\})) (N) = 0$