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 ⊢ φ → seq M + F ⁡ N ≤ seq M + 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 ≤ seq M + 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 ⊢ φ → seq M + x ∈ V ⟼ G ⁡ x − F ⁡ x ⁡ N = seq M + G ⁡ N − seq M + F ⁡ N
22 17 21 breqtrd ⊢ φ → 0 ≤ seq M + G ⁡ N − seq M + F ⁡ N
23 readdcl ⊢ k ∈ ℝ ∧ x ∈ ℝ → k + x ∈ ℝ
24 23 adantl ⊢ φ ∧ k ∈ ℝ ∧ x ∈ ℝ → k + x ∈ ℝ
25 1 3 24 seqcl ⊢ φ → seq M + G ⁡ N ∈ ℝ
26 1 2 24 seqcl ⊢ φ → seq M + F ⁡ N ∈ ℝ
27 25 26 subge0d ⊢ φ → 0 ≤ seq M + G ⁡ N − seq M + F ⁡ N ↔ seq M + F ⁡ N ≤ seq M + G ⁡ N
28 22 27 mpbid ⊢ φ → seq M + F ⁡ N ≤ seq M + G ⁡ N