This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fsumle

Description: If all of the terms of finite sums compare, so do the sums. (Contributed by NM, 11-Dec-2005) (Proof shortened by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses fsumle.1 ⊢ φ → A ∈ Fin
fsumle.2 ⊢ φ ∧ k ∈ A → B ∈ ℝ
fsumle.3 ⊢ φ ∧ k ∈ A → C ∈ ℝ
fsumle.4 ⊢ φ ∧ k ∈ A → B ≤ C
Assertion fsumle ⊢ φ → ∑ k ∈ A B ≤ ∑ k ∈ A C

Proof

Step Hyp Ref Expression
1 fsumle.1 ⊢ φ → A ∈ Fin
2 fsumle.2 ⊢ φ ∧ k ∈ A → B ∈ ℝ
3 fsumle.3 ⊢ φ ∧ k ∈ A → C ∈ ℝ
4 fsumle.4 ⊢ φ ∧ k ∈ A → B ≤ C
5 3 2 resubcld ⊢ φ ∧ k ∈ A → C − B ∈ ℝ
6 3 2 subge0d ⊢ φ ∧ k ∈ A → 0 ≤ C − B ↔ B ≤ C
7 4 6 mpbird ⊢ φ ∧ k ∈ A → 0 ≤ C − B
8 1 5 7 fsumge0 ⊢ φ → 0 ≤ ∑ k ∈ A C − B
9 3 recnd ⊢ φ ∧ k ∈ A → C ∈ ℂ
10 2 recnd ⊢ φ ∧ k ∈ A → B ∈ ℂ
11 1 9 10 fsumsub ⊢ φ → ∑ k ∈ A C − B = ∑ k ∈ A C − ∑ k ∈ A B
12 8 11 breqtrd ⊢ φ → 0 ≤ ∑ k ∈ A C − ∑ k ∈ A B
13 1 3 fsumrecl ⊢ φ → ∑ k ∈ A C ∈ ℝ
14 1 2 fsumrecl ⊢ φ → ∑ k ∈ A B ∈ ℝ
15 13 14 subge0d ⊢ φ → 0 ≤ ∑ k ∈ A C − ∑ k ∈ A B ↔ ∑ k ∈ A B ≤ ∑ k ∈ A C
16 12 15 mpbid ⊢ φ → ∑ k ∈ A B ≤ ∑ k ∈ A C