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

Metamath Proof Explorer

Theorem fsumless

Description: A shorter sum of nonnegative terms is smaller than a longer one. (Contributed by NM, 26-Dec-2005) (Proof shortened by Mario Carneiro, 24-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 fsumge0.1 ⊢ φ → A ∈ Fin
2 fsumge0.2 ⊢ φ ∧ k ∈ A → B ∈ ℝ
3 fsumge0.3 ⊢ φ ∧ k ∈ A → 0 ≤ B
4 fsumless.4 ⊢ φ → C ⊆ A
5 difss ⊢ A ∖ C ⊆ A
6 ssfi ⊢ A ∈ Fin ∧ A ∖ C ⊆ A → A ∖ C ∈ Fin
7 1 5 6 sylancl ⊢ φ → A ∖ C ∈ Fin
8 eldifi ⊢ k ∈ A ∖ C → k ∈ A
9 8 2 sylan2 ⊢ φ ∧ k ∈ A ∖ C → B ∈ ℝ
10 8 3 sylan2 ⊢ φ ∧ k ∈ A ∖ C → 0 ≤ B
11 7 9 10 fsumge0 ⊢ φ → 0 ≤ ∑ k ∈ A ∖ C B
12 1 4 ssfid ⊢ φ → C ∈ Fin
13 4 sselda ⊢ φ ∧ k ∈ C → k ∈ A
14 13 2 syldan ⊢ φ ∧ k ∈ C → B ∈ ℝ
15 12 14 fsumrecl ⊢ φ → ∑ k ∈ C B ∈ ℝ
16 7 9 fsumrecl ⊢ φ → ∑ k ∈ A ∖ C B ∈ ℝ
17 15 16 addge01d ⊢ φ → 0 ≤ ∑ k ∈ A ∖ C B ↔ ∑ k ∈ C B ≤ ∑ k ∈ C B + ∑ k ∈ A ∖ C B
18 11 17 mpbid ⊢ φ → ∑ k ∈ C B ≤ ∑ k ∈ C B + ∑ k ∈ A ∖ C B
19 disjdif ⊢ C ∩ A ∖ C = ∅
20 19 a1i ⊢ φ → C ∩ A ∖ C = ∅
21 undif ⊢ C ⊆ A ↔ C ∪ A ∖ C = A
22 4 21 sylib ⊢ φ → C ∪ A ∖ C = A
23 22 eqcomd ⊢ φ → A = C ∪ A ∖ C
24 2 recnd ⊢ φ ∧ k ∈ A → B ∈ ℂ
25 20 23 1 24 fsumsplit ⊢ φ → ∑ k ∈ A B = ∑ k ∈ C B + ∑ k ∈ A ∖ C B
26 18 25 breqtrrd ⊢ φ → ∑ k ∈ C B ≤ ∑ k ∈ A B