ser0f

Description: A zero-valued infinite series is equal to the constant zero function. (Contributed by Mario Carneiro, 8-Feb-2014)

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

Step	Hyp	Ref	Expression
1		ser0.1	$⊢ Z = ℤ_{\geq M}$
2	1	ser0	$⊢ k \in Z \to seq M (+ (Z \times \{0\})) (k) = 0$
3		c0ex	$⊢ 0 \in V$
4	3	fvconst2	$⊢ k \in Z \to (Z \times \{0\}) (k) = 0$
5	2 4	eqtr4d	$⊢ k \in Z \to seq M (+ (Z \times \{0\})) (k) = (Z \times \{0\}) (k)$
6	5	rgen	$⊢ \forall k \in Z seq M (+ (Z \times \{0\})) (k) = (Z \times \{0\}) (k)$
7		seqfn	$⊢ M \in ℤ \to seq M (+ (Z \times \{0\})) Fn ℤ_{\geq M}$
8	1	fneq2i	$⊢ seq M (+ (Z \times \{0\})) Fn Z \leftrightarrow seq M (+ (Z \times \{0\})) Fn ℤ_{\geq M}$
9	7 8	sylibr	$⊢ M \in ℤ \to seq M (+ (Z \times \{0\})) Fn Z$
10	3	fconst	$⊢ (Z \times \{0\}) : Z ⟶ \{0\}$
11		ffn	$⊢ (Z \times \{0\}) : Z ⟶ \{0\} \to (Z \times \{0\}) Fn Z$
12	10 11	ax-mp	$⊢ (Z \times \{0\}) Fn Z$
13		eqfnfv	$⊢ (seq M (+ (Z \times \{0\})) Fn Z \land (Z \times \{0\}) Fn Z) \to (seq M (+ (Z \times \{0\})) = Z \times \{0\} \leftrightarrow \forall k \in Z seq M (+ (Z \times \{0\})) (k) = (Z \times \{0\}) (k))$
14	9 12 13	sylancl	$⊢ M \in ℤ \to (seq M (+ (Z \times \{0\})) = Z \times \{0\} \leftrightarrow \forall k \in Z seq M (+ (Z \times \{0\})) (k) = (Z \times \{0\}) (k))$
15	6 14	mpbiri	$⊢ M \in ℤ \to seq M (+ (Z \times \{0\})) = Z \times \{0\}$

Metamath Proof Explorer