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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 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 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ≤ 𝐴 )