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

Metamath Proof Explorer

Theorem sumnul

Description: The sum of a non-convergent infinite series evaluates to the empty set. (Contributed by Paul Chapman, 4-Nov-2007) (Revised by Mario Carneiro, 23-Apr-2014)

		Ref	Expression
	Hypotheses	isumcl.1	$⊢ Z = ℤ_{\geq M}$
		isumcl.2	$⊢ φ \to M \in ℤ$
		isumcl.3	$⊢ (φ \land k \in Z) \to F (k) = A$
		isumcl.4	$⊢ (φ \land k \in Z) \to A \in ℂ$
		sumnul.5	$⊢ φ \to \neg seq M (+ F) \in dom ⇝$
	Assertion	sumnul	$⊢ φ \to \sum_{k \in Z} A = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		isumcl.1	$⊢ Z = ℤ_{\geq M}$
2		isumcl.2	$⊢ φ \to M \in ℤ$
3		isumcl.3	$⊢ (φ \land k \in Z) \to F (k) = A$
4		isumcl.4	$⊢ (φ \land k \in Z) \to A \in ℂ$
5		sumnul.5	$⊢ φ \to \neg seq M (+ F) \in dom ⇝$
6	1 2 3 4	isum	$⊢ φ \to \sum_{k \in Z} A = ⇝ (seq M (+ F))$
7		ndmfv	$⊢ \neg seq M (+ F) \in dom ⇝ \to ⇝ (seq M (+ F)) = \emptyset$
8	5 7	syl	$⊢ φ \to ⇝ (seq M (+ F)) = \emptyset$
9	6 8	eqtrd	$⊢ φ \to \sum_{k \in Z} A = \emptyset$