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 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
serge0.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
serge0.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 0 ≤ ( 𝐹 ‘ 𝑘 ) )
Assertion serge0 ( 𝜑 → 0 ≤ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 serge0.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 serge0.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
3 serge0.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 0 ≤ ( 𝐹 ‘ 𝑘 ) )
4 breq2 ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑘 ) → ( 0 ≤ 𝑥 ↔ 0 ≤ ( 𝐹 ‘ 𝑘 ) ) )
5 4 2 3 elrabd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ { 𝑥 ∈ ℝ ∣ 0 ≤ 𝑥 } )
6 breq2 ⊢ ( 𝑥 = 𝑘 → ( 0 ≤ 𝑥 ↔ 0 ≤ 𝑘 ) )
7 6 elrab ⊢ ( 𝑘 ∈ { 𝑥 ∈ ℝ ∣ 0 ≤ 𝑥 } ↔ ( 𝑘 ∈ ℝ ∧ 0 ≤ 𝑘 ) )
8 breq2 ⊢ ( 𝑥 = 𝑦 → ( 0 ≤ 𝑥 ↔ 0 ≤ 𝑦 ) )
9 8 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ ℝ ∣ 0 ≤ 𝑥 } ↔ ( 𝑦 ∈ ℝ ∧ 0 ≤ 𝑦 ) )
10 breq2 ⊢ ( 𝑥 = ( 𝑘 + 𝑦 ) → ( 0 ≤ 𝑥 ↔ 0 ≤ ( 𝑘 + 𝑦 ) ) )
11 readdcl ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑘 + 𝑦 ) ∈ ℝ )
12 11 ad2ant2r ⊢ ( ( ( 𝑘 ∈ ℝ ∧ 0 ≤ 𝑘 ) ∧ ( 𝑦 ∈ ℝ ∧ 0 ≤ 𝑦 ) ) → ( 𝑘 + 𝑦 ) ∈ ℝ )
13 addge0 ⊢ ( ( ( 𝑘 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ∧ ( 0 ≤ 𝑘 ∧ 0 ≤ 𝑦 ) ) → 0 ≤ ( 𝑘 + 𝑦 ) )
14 13 an4s ⊢ ( ( ( 𝑘 ∈ ℝ ∧ 0 ≤ 𝑘 ) ∧ ( 𝑦 ∈ ℝ ∧ 0 ≤ 𝑦 ) ) → 0 ≤ ( 𝑘 + 𝑦 ) )
15 10 12 14 elrabd ⊢ ( ( ( 𝑘 ∈ ℝ ∧ 0 ≤ 𝑘 ) ∧ ( 𝑦 ∈ ℝ ∧ 0 ≤ 𝑦 ) ) → ( 𝑘 + 𝑦 ) ∈ { 𝑥 ∈ ℝ ∣ 0 ≤ 𝑥 } )
16 7 9 15 syl2anb ⊢ ( ( 𝑘 ∈ { 𝑥 ∈ ℝ ∣ 0 ≤ 𝑥 } ∧ 𝑦 ∈ { 𝑥 ∈ ℝ ∣ 0 ≤ 𝑥 } ) → ( 𝑘 + 𝑦 ) ∈ { 𝑥 ∈ ℝ ∣ 0 ≤ 𝑥 } )
17 16 adantl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ { 𝑥 ∈ ℝ ∣ 0 ≤ 𝑥 } ∧ 𝑦 ∈ { 𝑥 ∈ ℝ ∣ 0 ≤ 𝑥 } ) ) → ( 𝑘 + 𝑦 ) ∈ { 𝑥 ∈ ℝ ∣ 0 ≤ 𝑥 } )
18 1 5 17 seqcl ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ { 𝑥 ∈ ℝ ∣ 0 ≤ 𝑥 } )
19 breq2 ⊢ ( 𝑥 = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) → ( 0 ≤ 𝑥 ↔ 0 ≤ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
20 19 elrab ⊢ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ { 𝑥 ∈ ℝ ∣ 0 ≤ 𝑥 } ↔ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ ℝ ∧ 0 ≤ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
21 20 simprbi ⊢ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ { 𝑥 ∈ ℝ ∣ 0 ≤ 𝑥 } → 0 ≤ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
22 18 21 syl ⊢ ( 𝜑 → 0 ≤ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )