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	⊢ ( 𝜑 → 𝐶 ≤ Σ 𝑘 ∈ 𝐴 𝐵 )