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

Proof

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