Theorem iserge0

Description: The limit of an infinite series of nonnegative reals is nonnegative. (Contributed by Paul Chapman, 9-Feb-2008) (Revised by Mario Carneiro, 3-Feb-2014)

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

Proof

Step	Hyp	Ref	Expression
1		clim2ser.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		iserge0.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		iserge0.3	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ 𝐴 )
4		iserge0.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
5		iserge0.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ ( 𝐹 ‘ 𝑘 ) )
6		serclim0	⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( + , ( ( ℤ≥ ‘ 𝑀 ) × { 0 } ) ) ⇝ 0 )
7	2 6	syl	⊢ ( 𝜑 → seq 𝑀 ( + , ( ( ℤ≥ ‘ 𝑀 ) × { 0 } ) ) ⇝ 0 )
8		simpr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ 𝑍 )
9	8 1	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
10		c0ex	⊢ 0 ∈ V
11	10	fvconst2	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) → ( ( ( ℤ≥ ‘ 𝑀 ) × { 0 } ) ‘ 𝑘 ) = 0 )
12	9 11	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( ℤ≥ ‘ 𝑀 ) × { 0 } ) ‘ 𝑘 ) = 0 )
13		0re	⊢ 0 ∈ ℝ
14	12 13	eqeltrdi	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( ℤ≥ ‘ 𝑀 ) × { 0 } ) ‘ 𝑘 ) ∈ ℝ )
15	12 5	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( ( ℤ≥ ‘ 𝑀 ) × { 0 } ) ‘ 𝑘 ) ≤ ( 𝐹 ‘ 𝑘 ) )
16	1 2 7 3 14 4 15	iserle	⊢ ( 𝜑 → 0 ≤ 𝐴 )