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 ⊢ Z = ℤ ≥ M
climserle.2 ⊢ φ → N ∈ Z
climserle.3 ⊢ φ → seq M + F ⇝ A
climserle.4 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ
climserle.5 ⊢ φ ∧ k ∈ Z → 0 ≤ F ⁡ k
Assertion climserle ⊢ φ → seq M + F ⁡ N ≤ A

Proof

Step Hyp Ref Expression
1 clim2ser.1 ⊢ Z = ℤ ≥ M
2 climserle.2 ⊢ φ → N ∈ Z
3 climserle.3 ⊢ φ → seq M + F ⇝ A
4 climserle.4 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ
5 climserle.5 ⊢ φ ∧ k ∈ Z → 0 ≤ F ⁡ k
6 2 1 eleqtrdi ⊢ φ → N ∈ ℤ ≥ M
7 eluzel2 ⊢ N ∈ ℤ ≥ M → M ∈ ℤ
8 6 7 syl ⊢ φ → M ∈ ℤ
9 1 8 4 serfre ⊢ φ → seq M + F : Z ⟶ ℝ
10 9 ffvelrnda ⊢ φ ∧ j ∈ Z → seq M + F ⁡ j ∈ ℝ
11 1 peano2uzs ⊢ j ∈ Z → j + 1 ∈ Z
12 fveq2 ⊢ k = j + 1 → F ⁡ k = F ⁡ j + 1
13 12 breq2d ⊢ k = j + 1 → 0 ≤ F ⁡ k ↔ 0 ≤ F ⁡ j + 1
14 13 imbi2d ⊢ k = j + 1 → φ → 0 ≤ F ⁡ k ↔ φ → 0 ≤ F ⁡ j + 1
15 5 expcom ⊢ k ∈ Z → φ → 0 ≤ F ⁡ k
16 14 15 vtoclga ⊢ j + 1 ∈ Z → φ → 0 ≤ F ⁡ j + 1
17 16 impcom ⊢ φ ∧ j + 1 ∈ Z → 0 ≤ F ⁡ j + 1
18 11 17 sylan2 ⊢ φ ∧ j ∈ Z → 0 ≤ F ⁡ j + 1
19 12 eleq1d ⊢ k = j + 1 → F ⁡ k ∈ ℝ ↔ F ⁡ j + 1 ∈ ℝ
20 19 imbi2d ⊢ k = j + 1 → φ → F ⁡ k ∈ ℝ ↔ φ → F ⁡ j + 1 ∈ ℝ
21 4 expcom ⊢ k ∈ Z → φ → F ⁡ k ∈ ℝ
22 20 21 vtoclga ⊢ j + 1 ∈ Z → φ → F ⁡ j + 1 ∈ ℝ
23 22 impcom ⊢ φ ∧ j + 1 ∈ Z → F ⁡ j + 1 ∈ ℝ
24 11 23 sylan2 ⊢ φ ∧ j ∈ Z → F ⁡ j + 1 ∈ ℝ
25 10 24 addge01d ⊢ φ ∧ j ∈ Z → 0 ≤ F ⁡ j + 1 ↔ seq M + F ⁡ j ≤ seq M + F ⁡ j + F ⁡ j + 1
26 18 25 mpbid ⊢ φ ∧ j ∈ Z → seq M + F ⁡ j ≤ seq M + F ⁡ j + F ⁡ j + 1
27 simpr ⊢ φ ∧ j ∈ Z → j ∈ Z
28 27 1 eleqtrdi ⊢ φ ∧ j ∈ Z → j ∈ ℤ ≥ M
29 seqp1 ⊢ j ∈ ℤ ≥ M → seq M + F ⁡ j + 1 = seq M + F ⁡ j + F ⁡ j + 1
30 28 29 syl ⊢ φ ∧ j ∈ Z → seq M + F ⁡ j + 1 = seq M + F ⁡ j + F ⁡ j + 1
31 26 30 breqtrrd ⊢ φ ∧ j ∈ Z → seq M + F ⁡ j ≤ seq M + F ⁡ j + 1
32 1 2 3 10 31 climub ⊢ φ → seq M + F ⁡ N ≤ A