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 ⊢φ→seqM+F⇝A
climserle.4 ⊢φ∧k∈Z→F⁡k∈ℝ
climserle.5 ⊢φ∧k∈Z→0≤F⁡k
Assertion climserle ⊢φ→seqM+F⁡N≤A

Proof

Step Hyp Ref Expression
1 clim2ser.1 ⊢Z=ℤ≥M
2 climserle.2 ⊢φ→N∈Z
3 climserle.3 ⊢φ→seqM+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 ⊢φ→seqM+F:Z⟶ℝ
10 9 ffvelcdmda ⊢φ∧j∈Z→seqM+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↔seqM+F⁡j≤seqM+F⁡j+F⁡j+1
26 18 25 mpbid ⊢φ∧j∈Z→seqM+F⁡j≤seqM+F⁡j+F⁡j+1
27 simpr ⊢φ∧j∈Z→j∈Z
28 27 1 eleqtrdi ⊢φ∧j∈Z→j∈ℤ≥M
29 seqp1 ⊢j∈ℤ≥M→seqM+F⁡j+1=seqM+F⁡j+F⁡j+1
30 28 29 syl ⊢φ∧j∈Z→seqM+F⁡j+1=seqM+F⁡j+F⁡j+1
31 26 30 breqtrrd ⊢φ∧j∈Z→seqM+F⁡j≤seqM+F⁡j+1
32 1 2 3 10 31 climub ⊢φ→seqM+F⁡N≤A