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 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fsumge0.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
fsumge0.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ 𝐵 )
fsumge1.4 ⊢ ( 𝑘 = 𝑀 → 𝐵 = 𝐶 )
fsumge1.5 ⊢ ( 𝜑 → 𝑀 ∈ 𝐴 )
Assertion fsumge1 ( 𝜑 → 𝐶 ≤ Σ 𝑘 ∈ 𝐴 𝐵 )

Proof

Step Hyp Ref Expression
1 fsumge0.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 fsumge0.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3 fsumge0.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ 𝐵 )
4 fsumge1.4 ⊢ ( 𝑘 = 𝑀 → 𝐵 = 𝐶 )
5 fsumge1.5 ⊢ ( 𝜑 → 𝑀 ∈ 𝐴 )
6 4 eleq1d ⊢ ( 𝑘 = 𝑀 → ( 𝐵 ∈ ℂ ↔ 𝐶 ∈ ℂ ) )
7 2 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
8 7 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 𝐵 ∈ ℂ )
9 6 8 5 rspcdva ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
10 4 sumsn ⊢ ( ( 𝑀 ∈ 𝐴 ∧ 𝐶 ∈ ℂ ) → Σ 𝑘 ∈ { 𝑀 } 𝐵 = 𝐶 )
11 5 9 10 syl2anc ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑀 } 𝐵 = 𝐶 )
12 5 snssd ⊢ ( 𝜑 → { 𝑀 } ⊆ 𝐴 )
13 1 2 3 12 fsumless ⊢ ( 𝜑 → Σ 𝑘 ∈ { 𝑀 } 𝐵 ≤ Σ 𝑘 ∈ 𝐴 𝐵 )
14 11 13 eqbrtrrd ⊢ ( 𝜑 → 𝐶 ≤ Σ 𝑘 ∈ 𝐴 𝐵 )