Metamath Proof Explorer

Theorem serle

Description: Comparison of partial sums of two infinite series of reals. (Contributed by NM, 27-Dec-2005) (Revised by Mario Carneiro, 27-May-2014)

Ref Expression
Hypotheses serge0.1 ⊢φ→N∈ℤ≥M
serge0.2 ⊢φ∧k∈M…N→F⁡k∈ℝ
serle.3 ⊢φ∧k∈M…N→G⁡k∈ℝ
serle.4 ⊢φ∧k∈M…N→F⁡k≤G⁡k
Assertion serle ⊢φ→seqM+F⁡N≤seqM+G⁡N

Proof

Step Hyp Ref Expression
1 serge0.1 ⊢φ→N∈ℤ≥M
2 serge0.2 ⊢φ∧k∈M…N→F⁡k∈ℝ
3 serle.3 ⊢φ∧k∈M…N→G⁡k∈ℝ
4 serle.4 ⊢φ∧k∈M…N→F⁡k≤G⁡k
5 fveq2 ⊢x=k→G⁡x=G⁡k
6 fveq2 ⊢x=k→F⁡x=F⁡k
7 5 6 oveq12d ⊢x=k→G⁡x−F⁡x=G⁡k−F⁡k
8 eqid ⊢x∈V⟼G⁡x−F⁡x=x∈V⟼G⁡x−F⁡x
9 ovex ⊢G⁡k−F⁡k∈V
10 7 8 9 fvmpt ⊢k∈V→x∈V⟼G⁡x−F⁡x⁡k=G⁡k−F⁡k
11 10 elv ⊢x∈V⟼G⁡x−F⁡x⁡k=G⁡k−F⁡k
12 3 2 resubcld ⊢φ∧k∈M…N→G⁡k−F⁡k∈ℝ
13 11 12 eqeltrid ⊢φ∧k∈M…N→x∈V⟼G⁡x−F⁡x⁡k∈ℝ
14 3 2 subge0d ⊢φ∧k∈M…N→0≤G⁡k−F⁡k↔F⁡k≤G⁡k
15 4 14 mpbird ⊢φ∧k∈M…N→0≤G⁡k−F⁡k
16 15 11 breqtrrdi ⊢φ∧k∈M…N→0≤x∈V⟼G⁡x−F⁡x⁡k
17 1 13 16 serge0 ⊢φ→0≤seqM+x∈V⟼G⁡x−F⁡x⁡N
18 3 recnd ⊢φ∧k∈M…N→G⁡k∈ℂ
19 2 recnd ⊢φ∧k∈M…N→F⁡k∈ℂ
20 11 a1i ⊢φ∧k∈M…N→x∈V⟼G⁡x−F⁡x⁡k=G⁡k−F⁡k
21 1 18 19 20 sersub ⊢φ→seqM+x∈V⟼G⁡x−F⁡x⁡N=seqM+G⁡N−seqM+F⁡N
22 17 21 breqtrd ⊢φ→0≤seqM+G⁡N−seqM+F⁡N
23 readdcl ⊢k∈ℝ∧x∈ℝ→k+x∈ℝ
24 23 adantl ⊢φ∧k∈ℝ∧x∈ℝ→k+x∈ℝ
25 1 3 24 seqcl ⊢φ→seqM+G⁡N∈ℝ
26 1 2 24 seqcl ⊢φ→seqM+F⁡N∈ℝ
27 25 26 subge0d ⊢φ→0≤seqM+G⁡N−seqM+F⁡N↔seqM+F⁡N≤seqM+G⁡N
28 22 27 mpbid ⊢φ→seqM+F⁡N≤seqM+G⁡N