Metamath Proof Explorer


Theorem climserle

Description: The partial sums of a converging infinite series with nonnegative terms are bounded by its limit. (Contributed by NM, 27-Dec-2005) (Revised by Mario Carneiro, 9-Feb-2014)

Ref Expression
Hypotheses clim2ser.1 𝑍 = ( ℤ𝑀 )
climserle.2 ( 𝜑𝑁𝑍 )
climserle.3 ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ 𝐴 )
climserle.4 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℝ )
climserle.5 ( ( 𝜑𝑘𝑍 ) → 0 ≤ ( 𝐹𝑘 ) )
Assertion climserle ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ≤ 𝐴 )

Proof

Step Hyp Ref Expression
1 clim2ser.1 𝑍 = ( ℤ𝑀 )
2 climserle.2 ( 𝜑𝑁𝑍 )
3 climserle.3 ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ 𝐴 )
4 climserle.4 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℝ )
5 climserle.5 ( ( 𝜑𝑘𝑍 ) → 0 ≤ ( 𝐹𝑘 ) )
6 2 1 eleqtrdi ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
7 eluzel2 ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑀 ∈ ℤ )
8 6 7 syl ( 𝜑𝑀 ∈ ℤ )
9 1 8 4 serfre ( 𝜑 → seq 𝑀 ( + , 𝐹 ) : 𝑍 ⟶ ℝ )
10 9 ffvelrnda ( ( 𝜑𝑗𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ∈ ℝ )
11 1 peano2uzs ( 𝑗𝑍 → ( 𝑗 + 1 ) ∈ 𝑍 )
12 fveq2 ( 𝑘 = ( 𝑗 + 1 ) → ( 𝐹𝑘 ) = ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
13 12 breq2d ( 𝑘 = ( 𝑗 + 1 ) → ( 0 ≤ ( 𝐹𝑘 ) ↔ 0 ≤ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) )
14 13 imbi2d ( 𝑘 = ( 𝑗 + 1 ) → ( ( 𝜑 → 0 ≤ ( 𝐹𝑘 ) ) ↔ ( 𝜑 → 0 ≤ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) )
15 5 expcom ( 𝑘𝑍 → ( 𝜑 → 0 ≤ ( 𝐹𝑘 ) ) )
16 14 15 vtoclga ( ( 𝑗 + 1 ) ∈ 𝑍 → ( 𝜑 → 0 ≤ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) )
17 16 impcom ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ 𝑍 ) → 0 ≤ ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
18 11 17 sylan2 ( ( 𝜑𝑗𝑍 ) → 0 ≤ ( 𝐹 ‘ ( 𝑗 + 1 ) ) )
19 12 eleq1d ( 𝑘 = ( 𝑗 + 1 ) → ( ( 𝐹𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∈ ℝ ) )
20 19 imbi2d ( 𝑘 = ( 𝑗 + 1 ) → ( ( 𝜑 → ( 𝐹𝑘 ) ∈ ℝ ) ↔ ( 𝜑 → ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∈ ℝ ) ) )
21 4 expcom ( 𝑘𝑍 → ( 𝜑 → ( 𝐹𝑘 ) ∈ ℝ ) )
22 20 21 vtoclga ( ( 𝑗 + 1 ) ∈ 𝑍 → ( 𝜑 → ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∈ ℝ ) )
23 22 impcom ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ 𝑍 ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
24 11 23 sylan2 ( ( 𝜑𝑗𝑍 ) → ( 𝐹 ‘ ( 𝑗 + 1 ) ) ∈ ℝ )
25 10 24 addge01d ( ( 𝜑𝑗𝑍 ) → ( 0 ≤ ( 𝐹 ‘ ( 𝑗 + 1 ) ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ≤ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) + ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) ) )
26 18 25 mpbid ( ( 𝜑𝑗𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ≤ ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) + ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) )
27 simpr ( ( 𝜑𝑗𝑍 ) → 𝑗𝑍 )
28 27 1 eleqtrdi ( ( 𝜑𝑗𝑍 ) → 𝑗 ∈ ( ℤ𝑀 ) )
29 seqp1 ( 𝑗 ∈ ( ℤ𝑀 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑗 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) + ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) )
30 28 29 syl ( ( 𝜑𝑗𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑗 + 1 ) ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) + ( 𝐹 ‘ ( 𝑗 + 1 ) ) ) )
31 26 30 breqtrrd ( ( 𝜑𝑗𝑍 ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑗 ) ≤ ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑗 + 1 ) ) )
32 1 2 3 10 31 climub ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ≤ 𝐴 )