Theorem esummono

Description: Extended sum is monotonic. (Contributed by Thierry Arnoux, 19-Oct-2017)

	Ref	Expression
Hypotheses	esummono.f	$$⊢Ⅎk\phi$$
	esummono.c	$$⊢\phi \to C\in V$$
	esummono.b	$$⊢\left(\phi \wedge k\in C\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
	esummono.a	$$⊢\phi \to A\subseteq C$$
Assertion	esummono	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B\le \underset{k\in C}{{\sum }^{*}}B$$

Proof

Step	Hyp	Ref	Expression
1		esummono.f	$$⊢Ⅎk\phi$$
2		esummono.c	$$⊢\phi \to C\in V$$
3		esummono.b	$$⊢\left(\phi \wedge k\in C\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
4		esummono.a	$$⊢\phi \to A\subseteq C$$
5	2	difexd	$$⊢\phi \to C\setminus A\in \mathrm{V}$$
6		simpr	$$⊢\left(\phi \wedge k\in \left(C\setminus A\right)\right)\to k\in \left(C\setminus A\right)$$
7	6	eldifad	$$⊢\left(\phi \wedge k\in \left(C\setminus A\right)\right)\to k\in C$$
8	7 3	syldan	$$⊢\left(\phi \wedge k\in \left(C\setminus A\right)\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
9	8	ex	$$⊢\phi \to \left(k\in \left(C\setminus A\right)\to B\in \left[0,\mathrm{+\infty }\right]\right)$$
10	1 9	ralrimi	$$⊢\phi \to \forall k\in \left(C\setminus A\right)B\in \left[0,\mathrm{+\infty }\right]$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}k\left(C\setminus A\right)$$
12	11	esumcl	$$⊢\left(C\setminus A\in \mathrm{V}\wedge \forall k\in \left(C\setminus A\right)B\in \left[0,\mathrm{+\infty }\right]\right)\to \underset{k\in C\setminus A}{{\sum }^{*}}B\in \left[0,\mathrm{+\infty }\right]$$
13	5 10 12	syl2anc	$$⊢\phi \to \underset{k\in C\setminus A}{{\sum }^{*}}B\in \left[0,\mathrm{+\infty }\right]$$
14		elxrge0	$$⊢\underset{k\in C\setminus A}{{\sum }^{*}}B\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(\underset{k\in C\setminus A}{{\sum }^{*}}B\in {ℝ}^{*}\wedge 0\le \underset{k\in C\setminus A}{{\sum }^{*}}B\right)$$
15	14	simprbi	$$⊢\underset{k\in C\setminus A}{{\sum }^{*}}B\in \left[0,\mathrm{+\infty }\right]\to 0\le \underset{k\in C\setminus A}{{\sum }^{*}}B$$
16	13 15	syl	$$⊢\phi \to 0\le \underset{k\in C\setminus A}{{\sum }^{*}}B$$
17		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
18	2 4	ssexd	$$⊢\phi \to A\in \mathrm{V}$$
19	4	sselda	$$⊢\left(\phi \wedge k\in A\right)\to k\in C$$
20	19 3	syldan	$$⊢\left(\phi \wedge k\in A\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
21	20	ex	$$⊢\phi \to \left(k\in A\to B\in \left[0,\mathrm{+\infty }\right]\right)$$
22	1 21	ralrimi	$$⊢\phi \to \forall k\in AB\in \left[0,\mathrm{+\infty }\right]$$
23		nfcv	$$⊢\underset{\_}{Ⅎ}kA$$
24	23	esumcl	$$⊢\left(A\in \mathrm{V}\wedge \forall k\in AB\in \left[0,\mathrm{+\infty }\right]\right)\to \underset{k\in A}{{\sum }^{*}}B\in \left[0,\mathrm{+\infty }\right]$$
25	18 22 24	syl2anc	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B\in \left[0,\mathrm{+\infty }\right]$$
26	17 25	sselid	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B\in {ℝ}^{*}$$
27	17 13	sselid	$$⊢\phi \to \underset{k\in C\setminus A}{{\sum }^{*}}B\in {ℝ}^{*}$$
28		xraddge02	$$⊢\left(\underset{k\in A}{{\sum }^{*}}B\in {ℝ}^{*}\wedge \underset{k\in C\setminus A}{{\sum }^{*}}B\in {ℝ}^{*}\right)\to \left(0\le \underset{k\in C\setminus A}{{\sum }^{*}}B\to \underset{k\in A}{{\sum }^{*}}B\le \underset{k\in A}{{\sum }^{*}}B{+}_{𝑒}\underset{k\in C\setminus A}{{\sum }^{*}}B\right)$$
29	26 27 28	syl2anc	$$⊢\phi \to \left(0\le \underset{k\in C\setminus A}{{\sum }^{*}}B\to \underset{k\in A}{{\sum }^{*}}B\le \underset{k\in A}{{\sum }^{*}}B{+}_{𝑒}\underset{k\in C\setminus A}{{\sum }^{*}}B\right)$$
30	16 29	mpd	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B\le \underset{k\in A}{{\sum }^{*}}B{+}_{𝑒}\underset{k\in C\setminus A}{{\sum }^{*}}B$$
31		disjdif	$$⊢A\cap \left(C\setminus A\right)=\varnothing$$
32	31	a1i	$$⊢\phi \to A\cap \left(C\setminus A\right)=\varnothing$$
33	1 23 11 18 5 32 20 8	esumsplit	$$⊢\phi \to \underset{k\in A\cup \left(C\setminus A\right)}{{\sum }^{*}}B=\underset{k\in A}{{\sum }^{*}}B{+}_{𝑒}\underset{k\in C\setminus A}{{\sum }^{*}}B$$
34		undif	$$⊢A\subseteq C\leftrightarrow A\cup \left(C\setminus A\right)=C$$
35	4 34	sylib	$$⊢\phi \to A\cup \left(C\setminus A\right)=C$$
36	1 35	esumeq1d	$$⊢\phi \to \underset{k\in A\cup \left(C\setminus A\right)}{{\sum }^{*}}B=\underset{k\in C}{{\sum }^{*}}B$$
37	33 36	eqtr3d	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B{+}_{𝑒}\underset{k\in C\setminus A}{{\sum }^{*}}B=\underset{k\in C}{{\sum }^{*}}B$$
38	30 37	breqtrd	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B\le \underset{k\in C}{{\sum }^{*}}B$$