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

Metamath Proof Explorer

Theorem fsumlt

Description: If every term in one finite sum is less than the corresponding term in another, then the first sum is less than the second. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 3-Jun-2014)

Ref Expression
Hypotheses fsumlt.1 ⊢ φ → A ∈ Fin
fsumlt.2 ⊢ φ → A ≠ ∅
fsumlt.3 ⊢ φ ∧ k ∈ A → B ∈ ℝ
fsumlt.4 ⊢ φ ∧ k ∈ A → C ∈ ℝ
fsumlt.5 ⊢ φ ∧ k ∈ A → B < C
Assertion fsumlt ⊢ φ → ∑ k ∈ A B < ∑ k ∈ A C

Proof

Step Hyp Ref Expression
1 fsumlt.1 ⊢ φ → A ∈ Fin
2 fsumlt.2 ⊢ φ → A ≠ ∅
3 fsumlt.3 ⊢ φ ∧ k ∈ A → B ∈ ℝ
4 fsumlt.4 ⊢ φ ∧ k ∈ A → C ∈ ℝ
5 fsumlt.5 ⊢ φ ∧ k ∈ A → B < C
6 difrp ⊢ B ∈ ℝ ∧ C ∈ ℝ → B < C ↔ C − B ∈ ℝ +
7 3 4 6 syl2anc ⊢ φ ∧ k ∈ A → B < C ↔ C − B ∈ ℝ +
8 5 7 mpbid ⊢ φ ∧ k ∈ A → C − B ∈ ℝ +
9 1 2 8 fsumrpcl ⊢ φ → ∑ k ∈ A C − B ∈ ℝ +
10 9 rpgt0d ⊢ φ → 0 < ∑ k ∈ A C − B
11 4 recnd ⊢ φ ∧ k ∈ A → C ∈ ℂ
12 3 recnd ⊢ φ ∧ k ∈ A → B ∈ ℂ
13 1 11 12 fsumsub ⊢ φ → ∑ k ∈ A C − B = ∑ k ∈ A C − ∑ k ∈ A B
14 10 13 breqtrd ⊢ φ → 0 < ∑ k ∈ A C − ∑ k ∈ A B
15 1 3 fsumrecl ⊢ φ → ∑ k ∈ A B ∈ ℝ
16 1 4 fsumrecl ⊢ φ → ∑ k ∈ A C ∈ ℝ
17 15 16 posdifd ⊢ φ → ∑ k ∈ A B < ∑ k ∈ A C ↔ 0 < ∑ k ∈ A C − ∑ k ∈ A B
18 14 17 mpbird ⊢ φ → ∑ k ∈ A B < ∑ k ∈ A C