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

Proof

Step Hyp Ref Expression
1 clim2ser.1 ⊢ Z = ℤ ≥ M
2 iserge0.2 ⊢ φ → M ∈ ℤ
3 iserge0.3 ⊢ φ → seq M + F ⇝ A
4 iserge0.4 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ
5 iserge0.5 ⊢ φ ∧ k ∈ Z → 0 ≤ F ⁡ k
6 serclim0 ⊢ M ∈ ℤ → seq M + ℤ ≥ M × 0 ⇝ 0
7 2 6 syl ⊢ φ → seq M + ℤ ≥ M × 0 ⇝ 0
8 simpr ⊢ φ ∧ k ∈ Z → k ∈ Z
9 8 1 eleqtrdi ⊢ φ ∧ k ∈ Z → k ∈ ℤ ≥ M
10 c0ex ⊢ 0 ∈ V
11 10 fvconst2 ⊢ k ∈ ℤ ≥ M → ℤ ≥ M × 0 ⁡ k = 0
12 9 11 syl ⊢ φ ∧ k ∈ Z → ℤ ≥ M × 0 ⁡ k = 0
13 0re ⊢ 0 ∈ ℝ
14 12 13 eqeltrdi ⊢ φ ∧ k ∈ Z → ℤ ≥ M × 0 ⁡ k ∈ ℝ
15 12 5 eqbrtrd ⊢ φ ∧ k ∈ Z → ℤ ≥ M × 0 ⁡ k ≤ F ⁡ k
16 1 2 7 3 14 4 15 iserle ⊢ φ → 0 ≤ A