Theorem isumge0

Description: An infinite sum of nonnegative terms is nonnegative. (Contributed by Mario Carneiro, 28-Apr-2014)

	Ref	Expression
Hypotheses	isumrecl.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	isumrecl.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	isumrecl.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
	isumrecl.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℝ )
	isumrecl.5	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
	isumge0.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ 𝐴 )
Assertion	isumge0	⊢ ( 𝜑 → 0 ≤ Σ 𝑘 ∈ 𝑍 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		isumrecl.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		isumrecl.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		isumrecl.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
4		isumrecl.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℝ )
5		isumrecl.5	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
6		isumge0.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ 𝐴 )
7	4	recnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
8	1 2 3 7 5	isumclim2	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ Σ 𝑘 ∈ 𝑍 𝐴 )
9		fveq2	⊢ ( 𝑗 = 𝑘 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑘 ) )
10	9	cbvsumv	⊢ Σ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) = Σ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 )
11	3	sumeq2dv	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) = Σ 𝑘 ∈ 𝑍 𝐴 )
12	10 11	syl5eq	⊢ ( 𝜑 → Σ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) = Σ 𝑘 ∈ 𝑍 𝐴 )
13	8 12	breqtrrd	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ Σ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) )
14	3 4	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
15	6 3	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ ( 𝐹 ‘ 𝑘 ) )
16	1 2 13 14 15	iserge0	⊢ ( 𝜑 → 0 ≤ Σ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) )
17	16 12	breqtrd	⊢ ( 𝜑 → 0 ≤ Σ 𝑘 ∈ 𝑍 𝐴 )