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