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	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	isumcl.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	isumcl.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
	isumcl.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
	sumnul.5	⊢ ( 𝜑 → ¬ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
Assertion	sumnul	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 = ∅ )

Proof

Step	Hyp	Ref	Expression
1		isumcl.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		isumcl.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		isumcl.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
4		isumcl.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
5		sumnul.5	⊢ ( 𝜑 → ¬ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
6	1 2 3 4	isum	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 = ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )
7		ndmfv	⊢ ( ¬ seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ → ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) = ∅ )
8	5 7	syl	⊢ ( 𝜑 → ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) = ∅ )
9	6 8	eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 = ∅ )