This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ≤ 𝐴 )