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 ⊢φ→seqM+F∈dom⁡⇝
isumle.9 ⊢φ→seqM+G∈dom⁡⇝
Assertion isumle ⊢φ→∑k∈ZA≤∑k∈ZB

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 ⊢φ→seqM+F∈dom⁡⇝
9 isumle.9 ⊢φ→seqM+G∈dom⁡⇝
10 climdm ⊢seqM+F∈dom⁡⇝↔seqM+F⇝⇝⁡seqM+F
11 8 10 sylib ⊢φ→seqM+F⇝⇝⁡seqM+F
12 climdm ⊢seqM+G∈dom⁡⇝↔seqM+G⇝⇝⁡seqM+G
13 9 12 sylib ⊢φ→seqM+G⇝⇝⁡seqM+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 ⊢φ→⇝⁡seqM+F≤⇝⁡seqM+G
18 4 recnd ⊢φ∧k∈Z→A∈ℂ
19 1 2 3 18 isum ⊢φ→∑k∈ZA=⇝⁡seqM+F
20 6 recnd ⊢φ∧k∈Z→B∈ℂ
21 1 2 5 20 isum ⊢φ→∑k∈ZB=⇝⁡seqM+G
22 17 19 21 3brtr4d ⊢φ→∑k∈ZA≤∑k∈ZB