Metamath Proof Explorer

Theorem isumle

Description: Comparison of two infinite sums. (Contributed by Paul Chapman, 13-Nov-2007) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses isumle.1 ⊢ Z = ℤ ≥ M
isumle.2 ⊢ φ → M ∈ ℤ
isumle.3 ⊢ φ ∧ k ∈ Z → F ⁡ k = A
isumle.4 ⊢ φ ∧ k ∈ Z → A ∈ ℝ
isumle.5 ⊢ φ ∧ k ∈ Z → G ⁡ k = B
isumle.6 ⊢ φ ∧ k ∈ Z → B ∈ ℝ
isumle.7 ⊢ φ ∧ k ∈ Z → A ≤ B
isumle.8 ⊢ φ → seq M + F ∈ dom ⁡ ⇝
isumle.9 ⊢ φ → seq M + G ∈ dom ⁡ ⇝
Assertion isumle ⊢ φ → ∑ k ∈ Z A ≤ ∑ k ∈ Z B

Proof

Step Hyp Ref Expression
1 isumle.1 ⊢ Z = ℤ ≥ M
2 isumle.2 ⊢ φ → M ∈ ℤ
3 isumle.3 ⊢ φ ∧ k ∈ Z → F ⁡ k = A
4 isumle.4 ⊢ φ ∧ k ∈ Z → A ∈ ℝ
5 isumle.5 ⊢ φ ∧ k ∈ Z → G ⁡ k = B
6 isumle.6 ⊢ φ ∧ k ∈ Z → B ∈ ℝ
7 isumle.7 ⊢ φ ∧ k ∈ Z → A ≤ B
8 isumle.8 ⊢ φ → seq M + F ∈ dom ⁡ ⇝
9 isumle.9 ⊢ φ → seq M + G ∈ dom ⁡ ⇝
10 climdm ⊢ seq M + F ∈ dom ⁡ ⇝ ↔ seq M + F ⇝ ⇝ ⁡ seq M + F
11 8 10 sylib ⊢ φ → seq M + F ⇝ ⇝ ⁡ seq M + F
12 climdm ⊢ seq M + G ∈ dom ⁡ ⇝ ↔ seq M + G ⇝ ⇝ ⁡ seq M + G
13 9 12 sylib ⊢ φ → seq M + G ⇝ ⇝ ⁡ seq M + G
14 3 4 eqeltrd ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ
15 5 6 eqeltrd ⊢ φ ∧ k ∈ Z → G ⁡ k ∈ ℝ
16 7 3 5 3brtr4d ⊢ φ ∧ k ∈ Z → F ⁡ k ≤ G ⁡ k
17 1 2 11 13 14 15 16 iserle ⊢ φ → ⇝ ⁡ seq M + F ≤ ⇝ ⁡ seq M + G
18 4 recnd ⊢ φ ∧ k ∈ Z → A ∈ ℂ
19 1 2 3 18 isum ⊢ φ → ∑ k ∈ Z A = ⇝ ⁡ seq M + F
20 6 recnd ⊢ φ ∧ k ∈ Z → B ∈ ℂ
21 1 2 5 20 isum ⊢ φ → ∑ k ∈ Z B = ⇝ ⁡ seq M + G
22 17 19 21 3brtr4d ⊢ φ → ∑ k ∈ Z A ≤ ∑ k ∈ Z B