fsumlessf

Description: A shorter sum of nonnegative terms is smaller than a longer one. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	fsumlessf.k	⊢ Ⅎ 𝑘 𝜑
	fsumge0.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fsumge0.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	fsumge0.l	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ 𝐵 )
	fsumless.c	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
Assertion	fsumlessf	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐶 𝐵 ≤ Σ 𝑘 ∈ 𝐴 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		fsumlessf.k	⊢ Ⅎ 𝑘 𝜑
2		fsumge0.a	⊢ ( 𝜑 → 𝐴 ∈ Fin )
3		fsumge0.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
4		fsumge0.l	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ 𝐵 )
5		fsumless.c	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
6		nfv	⊢ Ⅎ 𝑘 𝑗 ∈ 𝐴
7	1 6	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝐴 )
8		nfcsb1v	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
9	8	nfel1	⊢ Ⅎ 𝑘 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ
10	7 9	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ )
11		eleq1w	⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝐴 ↔ 𝑗 ∈ 𝐴 ) )
12	11	anbi2d	⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ) )
13		csbeq1a	⊢ ( 𝑘 = 𝑗 → 𝐵 = ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
14	13	eleq1d	⊢ ( 𝑘 = 𝑗 → ( 𝐵 ∈ ℝ ↔ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ ) )
15	12 14	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ ) ) )
16	10 15 3	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ∈ ℝ )
17		nfcv	⊢ Ⅎ 𝑘 0
18		nfcv	⊢ Ⅎ 𝑘 ≤
19	17 18 8	nfbr	⊢ Ⅎ 𝑘 0 ≤ ⦋ 𝑗 / 𝑘 ⦌ 𝐵
20	7 19	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 0 ≤ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
21	13	breq2d	⊢ ( 𝑘 = 𝑗 → ( 0 ≤ 𝐵 ↔ 0 ≤ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) )
22	12 21	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ 𝐵 ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 0 ≤ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ) ) )
23	20 22 4	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 0 ≤ ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
24	2 16 23 5	fsumless	⊢ ( 𝜑 → Σ 𝑗 ∈ 𝐶 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ≤ Σ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
25		nfcv	⊢ Ⅎ 𝑗 𝐵
26	13 25 8	cbvsum	⊢ Σ 𝑘 ∈ 𝐶 𝐵 = Σ 𝑗 ∈ 𝐶 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
27	13 25 8	cbvsum	⊢ Σ 𝑘 ∈ 𝐴 𝐵 = Σ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵
28	26 27	breq12i	⊢ ( Σ 𝑘 ∈ 𝐶 𝐵 ≤ Σ 𝑘 ∈ 𝐴 𝐵 ↔ Σ 𝑗 ∈ 𝐶 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 ≤ Σ 𝑗 ∈ 𝐴 ⦋ 𝑗 / 𝑘 ⦌ 𝐵 )
29	24 28	sylibr	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐶 𝐵 ≤ Σ 𝑘 ∈ 𝐴 𝐵 )

Metamath Proof Explorer

Theorem fsumlessf

Proof