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

Metamath Proof Explorer

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 eqtrid ⊢ ( 𝜑 → Σ 𝑗 ∈ 𝑍 ( 𝐹 ‘ 𝑗 ) = Σ 𝑘 ∈ 𝑍 𝐴 )
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 ≤ Σ 𝑘 ∈ 𝑍 𝐴 )