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≤seqM+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 ⊢φ→seqM+F⁡N∈x∈ℝ|0≤x
19 breq2 ⊢x=seqM+F⁡N→0≤x↔0≤seqM+F⁡N
20 19 elrab ⊢seqM+F⁡N∈x∈ℝ|0≤x↔seqM+F⁡N∈ℝ∧0≤seqM+F⁡N
21 20 simprbi ⊢seqM+F⁡N∈x∈ℝ|0≤x→0≤seqM+F⁡N
22 18 21 syl ⊢φ→0≤seqM+F⁡N