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 = ( ZZ>= ` M )
	isumcl.2	|- ( ph -> M e. ZZ )
	isumcl.3	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
	isumcl.4	|- ( ( ph /\ k e. Z ) -> A e. CC )
	sumnul.5	|- ( ph -> -. seq M ( + , F ) e. dom ~~> )
Assertion	sumnul	|- ( ph -> sum_ k e. Z A = (/) )

Proof

Step	Hyp	Ref	Expression
1		isumcl.1	|- Z = ( ZZ>= ` M )
2		isumcl.2	|- ( ph -> M e. ZZ )
3		isumcl.3	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
4		isumcl.4	|- ( ( ph /\ k e. Z ) -> A e. CC )
5		sumnul.5	|- ( ph -> -. seq M ( + , F ) e. dom ~~> )
6	1 2 3 4	isum	|- ( ph -> sum_ k e. Z A = ( ~~> ` seq M ( + , F ) ) )
7		ndmfv	|- ( -. seq M ( + , F ) e. dom ~~> -> ( ~~> ` seq M ( + , F ) ) = (/) )
8	5 7	syl	|- ( ph -> ( ~~> ` seq M ( + , F ) ) = (/) )
9	6 8	eqtrd	|- ( ph -> sum_ k e. Z A = (/) )