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 ⊢ Z = ℤ ≥ M
isumrecl.2 ⊢ φ → M ∈ ℤ
isumrecl.3 ⊢ φ ∧ k ∈ Z → F ⁡ k = A
isumrecl.4 ⊢ φ ∧ k ∈ Z → A ∈ ℝ
isumrecl.5 ⊢ φ → seq M + F ∈ dom ⁡ ⇝
isumge0.6 ⊢ φ ∧ k ∈ Z → 0 ≤ A
Assertion isumge0 ⊢ φ → 0 ≤ ∑ k ∈ Z A

Proof

Step Hyp Ref Expression
1 isumrecl.1 ⊢ Z = ℤ ≥ M
2 isumrecl.2 ⊢ φ → M ∈ ℤ
3 isumrecl.3 ⊢ φ ∧ k ∈ Z → F ⁡ k = A
4 isumrecl.4 ⊢ φ ∧ k ∈ Z → A ∈ ℝ
5 isumrecl.5 ⊢ φ → seq M + F ∈ dom ⁡ ⇝
6 isumge0.6 ⊢ φ ∧ k ∈ Z → 0 ≤ A
7 4 recnd ⊢ φ ∧ k ∈ Z → A ∈ ℂ
8 1 2 3 7 5 isumclim2 ⊢ φ → seq M + F ⇝ ∑ k ∈ Z A
9 fveq2 ⊢ j = k → F ⁡ j = F ⁡ k
10 9 cbvsumv ⊢ ∑ j ∈ Z F ⁡ j = ∑ k ∈ Z F ⁡ k
11 3 sumeq2dv ⊢ φ → ∑ k ∈ Z F ⁡ k = ∑ k ∈ Z A
12 10 11 eqtrid ⊢ φ → ∑ j ∈ Z F ⁡ j = ∑ k ∈ Z A
13 8 12 breqtrrd ⊢ φ → seq M + F ⇝ ∑ j ∈ Z F ⁡ j
14 3 4 eqeltrd ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ
15 6 3 breqtrrd ⊢ φ ∧ k ∈ Z → 0 ≤ F ⁡ k
16 1 2 13 14 15 iserge0 ⊢ φ → 0 ≤ ∑ j ∈ Z F ⁡ j
17 16 12 breqtrd ⊢ φ → 0 ≤ ∑ k ∈ Z A