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		difexg	$$⊢C\in V\to C\setminus A\in \mathrm{V}$$
6	2 5	syl	$$⊢\phi \to C\setminus A\in \mathrm{V}$$
7		simpr	$$⊢\left(\phi \wedge k\in \left(C\setminus A\right)\right)\to k\in \left(C\setminus A\right)$$
8	7	eldifad	$$⊢\left(\phi \wedge k\in \left(C\setminus A\right)\right)\to k\in C$$
9	8 3	syldan	$$⊢\left(\phi \wedge k\in \left(C\setminus A\right)\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
10	9	ex	$$⊢\phi \to \left(k\in \left(C\setminus A\right)\to B\in \left[0,\mathrm{+\infty }\right]\right)$$
11	1 10	ralrimi	$$⊢\phi \to \forall k\in \left(C\setminus A\right)B\in \left[0,\mathrm{+\infty }\right]$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}k\left(C\setminus A\right)$$
13	12	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]$$
14	6 11 13	syl2anc	$$⊢\phi \to \underset{k\in C\setminus A}{{\sum }^{*}}B\in \left[0,\mathrm{+\infty }\right]$$
15		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)$$
16	15	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$$
17	14 16	syl	$$⊢\phi \to 0\le \underset{k\in C\setminus A}{{\sum }^{*}}B$$
18		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
19	2 4	ssexd	$$⊢\phi \to A\in \mathrm{V}$$
20	4	sselda	$$⊢\left(\phi \wedge k\in A\right)\to k\in C$$
21	20 3	syldan	$$⊢\left(\phi \wedge k\in A\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
22	21	ex	$$⊢\phi \to \left(k\in A\to B\in \left[0,\mathrm{+\infty }\right]\right)$$
23	1 22	ralrimi	$$⊢\phi \to \forall k\in AB\in \left[0,\mathrm{+\infty }\right]$$
24		nfcv	$$⊢\underset{\_}{Ⅎ}kA$$
25	24	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]$$
26	19 23 25	syl2anc	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B\in \left[0,\mathrm{+\infty }\right]$$
27	18 26	sseldi	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B\in {ℝ}^{*}$$
28	18 14	sseldi	$$⊢\phi \to \underset{k\in C\setminus A}{{\sum }^{*}}B\in {ℝ}^{*}$$
29		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)$$
30	27 28 29	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)$$
31	17 30	mpd	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B\le \underset{k\in A}{{\sum }^{*}}B{+}_{𝑒}\underset{k\in C\setminus A}{{\sum }^{*}}B$$
32		disjdif	$$⊢A\cap \left(C\setminus A\right)=\varnothing$$
33	32	a1i	$$⊢\phi \to A\cap \left(C\setminus A\right)=\varnothing$$
34	1 24 12 19 6 33 21 9	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$$
35		undif	$$⊢A\subseteq C\leftrightarrow A\cup \left(C\setminus A\right)=C$$
36	4 35	sylib	$$⊢\phi \to A\cup \left(C\setminus A\right)=C$$
37	1 36	esumeq1d	$$⊢\phi \to \underset{k\in A\cup \left(C\setminus A\right)}{{\sum }^{*}}B=\underset{k\in C}{{\sum }^{*}}B$$
38	34 37	eqtr3d	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B{+}_{𝑒}\underset{k\in C\setminus A}{{\sum }^{*}}B=\underset{k\in C}{{\sum }^{*}}B$$
39	31 38	breqtrd	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B\le \underset{k\in C}{{\sum }^{*}}B$$