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={\mathbb{Z}}_{\ge M}$$
	isumcl.2	$$⊢\phi \to M\in \mathbb{Z}$$
	isumcl.3	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
	isumcl.4	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℂ$$
	sumnul.5	$$⊢\phi \to \neg seqM\left(+,F\right)\in \mathrm{dom}⇝$$
Assertion	sumnul	$$⊢\phi \to \sum _{k\in Z}A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		isumcl.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		isumcl.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		isumcl.3	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
4		isumcl.4	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℂ$$
5		sumnul.5	$$⊢\phi \to \neg seqM\left(+,F\right)\in \mathrm{dom}⇝$$
6	1 2 3 4	isum	$$⊢\phi \to \sum _{k\in Z}A=⇝\left(seqM\left(+,F\right)\right)$$
7		ndmfv	$$⊢\neg seqM\left(+,F\right)\in \mathrm{dom}⇝\to ⇝\left(seqM\left(+,F\right)\right)=\varnothing$$
8	5 7	syl	$$⊢\phi \to ⇝\left(seqM\left(+,F\right)\right)=\varnothing$$
9	6 8	eqtrd	$$⊢\phi \to \sum _{k\in Z}A=\varnothing$$