Theorem 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	$$⊢Ⅎk\phi$$
	fsumge0.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	fsumge0.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℝ$$
	fsumge0.l	$$⊢\left(\phi \wedge k\in A\right)\to 0\le B$$
	fsumless.c	$$⊢\phi \to C\subseteq A$$
Assertion	fsumlessf	$$⊢\phi \to \sum _{k\in C}B\le \sum _{k\in A}B$$

Proof

Step	Hyp	Ref	Expression
1		fsumlessf.k	$$⊢Ⅎk\phi$$
2		fsumge0.a	$$⊢\phi \to A\in \mathrm{Fin}$$
3		fsumge0.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℝ$$
4		fsumge0.l	$$⊢\left(\phi \wedge k\in A\right)\to 0\le B$$
5		fsumless.c	$$⊢\phi \to C\subseteq A$$
6		nfv	$$⊢Ⅎkj\in A$$
7	1 6	nfan	$$⊢Ⅎk\left(\phi \wedge j\in A\right)$$
8		nfcsb1v	$$⊢\underset{\_}{Ⅎ}k⦋j/k⦌B$$
9	8	nfel1	$$⊢Ⅎk⦋j/k⦌B\in ℝ$$
10	7 9	nfim	$$⊢Ⅎk\left(\left(\phi \wedge j\in A\right)\to ⦋j/k⦌B\in ℝ\right)$$
11		eleq1w	$$⊢k=j\to \left(k\in A\leftrightarrow j\in A\right)$$
12	11	anbi2d	$$⊢k=j\to \left(\left(\phi \wedge k\in A\right)\leftrightarrow \left(\phi \wedge j\in A\right)\right)$$
13		csbeq1a	$$⊢k=j\to B=⦋j/k⦌B$$
14	13	eleq1d	$$⊢k=j\to \left(B\in ℝ\leftrightarrow ⦋j/k⦌B\in ℝ\right)$$
15	12 14	imbi12d	$$⊢k=j\to \left(\left(\left(\phi \wedge k\in A\right)\to B\in ℝ\right)\leftrightarrow \left(\left(\phi \wedge j\in A\right)\to ⦋j/k⦌B\in ℝ\right)\right)$$
16	10 15 3	chvarfv	$$⊢\left(\phi \wedge j\in A\right)\to ⦋j/k⦌B\in ℝ$$
17		nfcv	$$⊢\underset{\_}{Ⅎ}k0$$
18		nfcv	$$⊢\underset{\_}{Ⅎ}k\le$$
19	17 18 8	nfbr	$$⊢Ⅎk0\le ⦋j/k⦌B$$
20	7 19	nfim	$$⊢Ⅎk\left(\left(\phi \wedge j\in A\right)\to 0\le ⦋j/k⦌B\right)$$
21	13	breq2d	$$⊢k=j\to \left(0\le B\leftrightarrow 0\le ⦋j/k⦌B\right)$$
22	12 21	imbi12d	$$⊢k=j\to \left(\left(\left(\phi \wedge k\in A\right)\to 0\le B\right)\leftrightarrow \left(\left(\phi \wedge j\in A\right)\to 0\le ⦋j/k⦌B\right)\right)$$
23	20 22 4	chvarfv	$$⊢\left(\phi \wedge j\in A\right)\to 0\le ⦋j/k⦌B$$
24	2 16 23 5	fsumless	$$⊢\phi \to \sum _{j\in C}⦋j/k⦌B\le \sum _{j\in A}⦋j/k⦌B$$
25		nfcv	$$⊢\underset{\_}{Ⅎ}jC$$
26		nfcv	$$⊢\underset{\_}{Ⅎ}kC$$
27		nfcv	$$⊢\underset{\_}{Ⅎ}jB$$
28	13 25 26 27 8	cbvsum	$$⊢\sum _{k\in C}B=\sum _{j\in C}⦋j/k⦌B$$
29		nfcv	$$⊢\underset{\_}{Ⅎ}jA$$
30		nfcv	$$⊢\underset{\_}{Ⅎ}kA$$
31	13 29 30 27 8	cbvsum	$$⊢\sum _{k\in A}B=\sum _{j\in A}⦋j/k⦌B$$
32	28 31	breq12i	$$⊢\sum _{k\in C}B\le \sum _{k\in A}B\leftrightarrow \sum _{j\in C}⦋j/k⦌B\le \sum _{j\in A}⦋j/k⦌B$$
33	24 32	sylibr	$$⊢\phi \to \sum _{k\in C}B\le \sum _{k\in A}B$$