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

Metamath Proof Explorer

Theorem fsumge1

Description: A sum of nonnegative numbers is greater than or equal to any one of its terms. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 4-Jun-2014)

Ref Expression
Hypotheses fsumge0.1 ⊢ φ → A ∈ Fin
fsumge0.2 ⊢ φ ∧ k ∈ A → B ∈ ℝ
fsumge0.3 ⊢ φ ∧ k ∈ A → 0 ≤ B
fsumge1.4 ⊢ k = M → B = C
fsumge1.5 ⊢ φ → M ∈ A
Assertion fsumge1 ⊢ φ → C ≤ ∑ 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 fsumge1.4 ⊢ k = M → B = C
5 fsumge1.5 ⊢ φ → M ∈ A
6 4 eleq1d ⊢ k = M → B ∈ ℂ ↔ C ∈ ℂ
7 2 recnd ⊢ φ ∧ k ∈ A → B ∈ ℂ
8 7 ralrimiva ⊢ φ → ∀ k ∈ A B ∈ ℂ
9 6 8 5 rspcdva ⊢ φ → C ∈ ℂ
10 4 sumsn ⊢ M ∈ A ∧ C ∈ ℂ → ∑ k ∈ M B = C
11 5 9 10 syl2anc ⊢ φ → ∑ k ∈ M B = C
12 5 snssd ⊢ φ → M ⊆ A
13 1 2 3 12 fsumless ⊢ φ → ∑ k ∈ M B ≤ ∑ k ∈ A B
14 11 13 eqbrtrrd ⊢ φ → C ≤ ∑ k ∈ A B