Metamath Proof Explorer

Theorem serge0

Description: A finite sum of nonnegative terms is nonnegative. (Contributed by Mario Carneiro, 8-Feb-2014) (Revised by Mario Carneiro, 27-May-2014)

Ref Expression
Hypotheses serge0.1 ⊢ φ → N ∈ ℤ ≥ M
serge0.2 ⊢ φ ∧ k ∈ M … N → F ⁡ k ∈ ℝ
serge0.3 ⊢ φ ∧ k ∈ M … N → 0 ≤ F ⁡ k
Assertion serge0 ⊢ φ → 0 ≤ seq M + F ⁡ N

Proof

Step Hyp Ref Expression
1 serge0.1 ⊢ φ → N ∈ ℤ ≥ M
2 serge0.2 ⊢ φ ∧ k ∈ M … N → F ⁡ k ∈ ℝ
3 serge0.3 ⊢ φ ∧ k ∈ M … N → 0 ≤ F ⁡ k
4 breq2 ⊢ x = F ⁡ k → 0 ≤ x ↔ 0 ≤ F ⁡ k
5 4 2 3 elrabd ⊢ φ ∧ k ∈ M … N → F ⁡ k ∈ x ∈ ℝ | 0 ≤ x
6 breq2 ⊢ x = k → 0 ≤ x ↔ 0 ≤ k
7 6 elrab ⊢ k ∈ x ∈ ℝ | 0 ≤ x ↔ k ∈ ℝ ∧ 0 ≤ k
8 breq2 ⊢ x = y → 0 ≤ x ↔ 0 ≤ y
9 8 elrab ⊢ y ∈ x ∈ ℝ | 0 ≤ x ↔ y ∈ ℝ ∧ 0 ≤ y
10 breq2 ⊢ x = k + y → 0 ≤ x ↔ 0 ≤ k + y
11 readdcl ⊢ k ∈ ℝ ∧ y ∈ ℝ → k + y ∈ ℝ
12 11 ad2ant2r ⊢ k ∈ ℝ ∧ 0 ≤ k ∧ y ∈ ℝ ∧ 0 ≤ y → k + y ∈ ℝ
13 addge0 ⊢ k ∈ ℝ ∧ y ∈ ℝ ∧ 0 ≤ k ∧ 0 ≤ y → 0 ≤ k + y
14 13 an4s ⊢ k ∈ ℝ ∧ 0 ≤ k ∧ y ∈ ℝ ∧ 0 ≤ y → 0 ≤ k + y
15 10 12 14 elrabd ⊢ k ∈ ℝ ∧ 0 ≤ k ∧ y ∈ ℝ ∧ 0 ≤ y → k + y ∈ x ∈ ℝ | 0 ≤ x
16 7 9 15 syl2anb ⊢ k ∈ x ∈ ℝ | 0 ≤ x ∧ y ∈ x ∈ ℝ | 0 ≤ x → k + y ∈ x ∈ ℝ | 0 ≤ x
17 16 adantl ⊢ φ ∧ k ∈ x ∈ ℝ | 0 ≤ x ∧ y ∈ x ∈ ℝ | 0 ≤ x → k + y ∈ x ∈ ℝ | 0 ≤ x
18 1 5 17 seqcl ⊢ φ → seq M + F ⁡ N ∈ x ∈ ℝ | 0 ≤ x
19 breq2 ⊢ x = seq M + F ⁡ N → 0 ≤ x ↔ 0 ≤ seq M + F ⁡ N
20 19 elrab ⊢ seq M + F ⁡ N ∈ x ∈ ℝ | 0 ≤ x ↔ seq M + F ⁡ N ∈ ℝ ∧ 0 ≤ seq M + F ⁡ N
21 20 simprbi ⊢ seq M + F ⁡ N ∈ x ∈ ℝ | 0 ≤ x → 0 ≤ seq M + F ⁡ N
22 18 21 syl ⊢ φ → 0 ≤ seq M + F ⁡ N