Theorem esummono

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

	Ref	Expression
Hypotheses	esummono.f	|- F/ k ph
	esummono.c	|- ( ph -> C e. V )
	esummono.b	|- ( ( ph /\ k e. C ) -> B e. ( 0 [,] +oo ) )
	esummono.a	|- ( ph -> A C_ C )
Assertion	esummono	|- ( ph -> sum* k e. A B <_ sum* k e. C B )

Proof

Step	Hyp	Ref	Expression
1		esummono.f	|- F/ k ph
2		esummono.c	|- ( ph -> C e. V )
3		esummono.b	|- ( ( ph /\ k e. C ) -> B e. ( 0 [,] +oo ) )
4		esummono.a	|- ( ph -> A C_ C )
5	2	difexd	|- ( ph -> ( C \ A ) e. _V )
6		simpr	|- ( ( ph /\ k e. ( C \ A ) ) -> k e. ( C \ A ) )
7	6	eldifad	|- ( ( ph /\ k e. ( C \ A ) ) -> k e. C )
8	7 3	syldan	|- ( ( ph /\ k e. ( C \ A ) ) -> B e. ( 0 [,] +oo ) )
9	8	ex	|- ( ph -> ( k e. ( C \ A ) -> B e. ( 0 [,] +oo ) ) )
10	1 9	ralrimi	|- ( ph -> A. k e. ( C \ A ) B e. ( 0 [,] +oo ) )
11		nfcv	|- F/_ k ( C \ A )
12	11	esumcl	|- ( ( ( C \ A ) e. _V /\ A. k e. ( C \ A ) B e. ( 0 [,] +oo ) ) -> sum* k e. ( C \ A ) B e. ( 0 [,] +oo ) )
13	5 10 12	syl2anc	|- ( ph -> sum* k e. ( C \ A ) B e. ( 0 [,] +oo ) )
14		elxrge0	|- ( sum* k e. ( C \ A ) B e. ( 0 [,] +oo ) <-> ( sum* k e. ( C \ A ) B e. RR* /\ 0 <_ sum* k e. ( C \ A ) B ) )
15	14	simprbi	|- ( sum* k e. ( C \ A ) B e. ( 0 [,] +oo ) -> 0 <_ sum* k e. ( C \ A ) B )
16	13 15	syl	|- ( ph -> 0 <_ sum* k e. ( C \ A ) B )
17		iccssxr	|- ( 0 [,] +oo ) C_ RR*
18	2 4	ssexd	|- ( ph -> A e. _V )
19	4	sselda	|- ( ( ph /\ k e. A ) -> k e. C )
20	19 3	syldan	|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
21	20	ex	|- ( ph -> ( k e. A -> B e. ( 0 [,] +oo ) ) )
22	1 21	ralrimi	|- ( ph -> A. k e. A B e. ( 0 [,] +oo ) )
23		nfcv	|- F/_ k A
24	23	esumcl	|- ( ( A e. _V /\ A. k e. A B e. ( 0 [,] +oo ) ) -> sum* k e. A B e. ( 0 [,] +oo ) )
25	18 22 24	syl2anc	|- ( ph -> sum* k e. A B e. ( 0 [,] +oo ) )
26	17 25	sselid	|- ( ph -> sum* k e. A B e. RR* )
27	17 13	sselid	|- ( ph -> sum* k e. ( C \ A ) B e. RR* )
28		xraddge02	|- ( ( sum* k e. A B e. RR* /\ sum* k e. ( C \ A ) B e. RR* ) -> ( 0 <_ sum* k e. ( C \ A ) B -> sum* k e. A B <_ ( sum* k e. A B +e sum* k e. ( C \ A ) B ) ) )
29	26 27 28	syl2anc	|- ( ph -> ( 0 <_ sum* k e. ( C \ A ) B -> sum* k e. A B <_ ( sum* k e. A B +e sum* k e. ( C \ A ) B ) ) )
30	16 29	mpd	|- ( ph -> sum* k e. A B <_ ( sum* k e. A B +e sum* k e. ( C \ A ) B ) )
31		disjdif	|- ( A i^i ( C \ A ) ) = (/)
32	31	a1i	|- ( ph -> ( A i^i ( C \ A ) ) = (/) )
33	1 23 11 18 5 32 20 8	esumsplit	|- ( ph -> sum* k e. ( A u. ( C \ A ) ) B = ( sum* k e. A B +e sum* k e. ( C \ A ) B ) )
34		undif	|- ( A C_ C <-> ( A u. ( C \ A ) ) = C )
35	4 34	sylib	|- ( ph -> ( A u. ( C \ A ) ) = C )
36	1 35	esumeq1d	|- ( ph -> sum* k e. ( A u. ( C \ A ) ) B = sum* k e. C B )
37	33 36	eqtr3d	|- ( ph -> ( sum* k e. A B +e sum* k e. ( C \ A ) B ) = sum* k e. C B )
38	30 37	breqtrd	|- ( ph -> sum* k e. A B <_ sum* k e. C B )