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 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
serge0.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
serle.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
serle.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐺 ‘ 𝑘 ) )
Assertion serle ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ≤ ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 serge0.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 serge0.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
3 serle.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
4 serle.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐺 ‘ 𝑘 ) )
5 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑘 ) )
6 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑘 ) )
7 5 6 oveq12d ⊢ ( 𝑥 = 𝑘 → ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐺 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑘 ) ) )
8 eqid ⊢ ( 𝑥 ∈ V ↦ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ V ↦ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) )
9 ovex ⊢ ( ( 𝐺 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑘 ) ) ∈ V
10 7 8 9 fvmpt ⊢ ( 𝑘 ∈ V → ( ( 𝑥 ∈ V ↦ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( ( 𝐺 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑘 ) ) )
11 10 elv ⊢ ( ( 𝑥 ∈ V ↦ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( ( 𝐺 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑘 ) )
12 3 2 resubcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝐺 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑘 ) ) ∈ ℝ )
13 11 12 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑥 ∈ V ↦ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝑘 ) ∈ ℝ )
14 3 2 subge0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 0 ≤ ( ( 𝐺 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑘 ) ) ↔ ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐺 ‘ 𝑘 ) ) )
15 4 14 mpbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 0 ≤ ( ( 𝐺 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑘 ) ) )
16 15 11 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 0 ≤ ( ( 𝑥 ∈ V ↦ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝑘 ) )
17 1 13 16 serge0 ⊢ ( 𝜑 → 0 ≤ ( seq 𝑀 ( + , ( 𝑥 ∈ V ↦ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ) ) ‘ 𝑁 ) )
18 3 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐺 ‘ 𝑘 ) ∈ ℂ )
19 2 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
20 11 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑥 ∈ V ↦ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( ( 𝐺 ‘ 𝑘 ) − ( 𝐹 ‘ 𝑘 ) ) )
21 1 18 19 20 sersub ⊢ ( 𝜑 → ( seq 𝑀 ( + , ( 𝑥 ∈ V ↦ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐹 ‘ 𝑥 ) ) ) ) ‘ 𝑁 ) = ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
22 17 21 breqtrd ⊢ ( 𝜑 → 0 ≤ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) )
23 readdcl ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑘 + 𝑥 ) ∈ ℝ )
24 23 adantl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ ) ) → ( 𝑘 + 𝑥 ) ∈ ℝ )
25 1 3 24 seqcl ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ∈ ℝ )
26 1 2 24 seqcl ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ∈ ℝ )
27 25 26 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) − ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ≤ ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) ) )
28 22 27 mpbid ⊢ ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) ≤ ( seq 𝑀 ( + , 𝐺 ) ‘ 𝑁 ) )