Theorem dvfsum2 23797

Description: The reverse of dvfsumrlim 23794, when comparing a finite sum of increasing terms to an integral. In this case there is no point in stating the limit properties, because the terms of the sum aren't approaching zero, but there is nevertheless still a natural asymptotic statement that can be made. (Contributed by Mario Carneiro, 20-May-2016.)

Hypotheses

Ref	Expression
dvfsum2.s	|- S = ( T (,) +oo )
dvfsum2.z	|- Z = ( ZZ>= ` M )
dvfsum2.m	|- ( ph -> M e. ZZ )
dvfsum2.d	|- ( ph -> D e. RR )
dvfsum2.u	|- ( ph -> U e. RR* )
dvfsum2.md	|- ( ph -> M <_ ( D + 1 ) )
dvfsum2.t	|- ( ph -> T e. RR )
dvfsum2.a	|- ( ( ph /\ x e. S ) -> A e. RR )
dvfsum2.b1	|- ( ( ph /\ x e. S ) -> B e. V )
dvfsum2.b2	|- ( ( ph /\ x e. Z ) -> B e. RR )
dvfsum2.b3	|- ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )
dvfsum2.c	|- ( x = k -> B = C )
dvfsum2.l	|- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> B <_ C )
dvfsum2.g	|- G = ( x e. S |-> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) )
dvfsum2.0	|- ( ( ph /\ ( x e. S /\ D <_ x ) ) -> 0 <_ B )
dvfsum2.1	|- ( ph -> X e. S )
dvfsum2.2	|- ( ph -> Y e. S )
dvfsum2.3	|- ( ph -> D <_ X )
dvfsum2.4	|- ( ph -> X <_ Y )
dvfsum2.5	|- ( ph -> Y <_ U )
dvfsum2.e	|- ( x = Y -> B = E )

Assertion

Ref	Expression
dvfsum2	|- ( ph -> ( abs ` ( ( G ` Y ) - ( G ` X ) ) ) <_ E )

Distinct variable groups:   B, k   x, C   x, k, D   ph, k, x   x, E   k, M, x   S, k, x   k, X, x   k, Y, x   x, T   U, k, x   x, V   x, Z

Allowed substitution hints:   A( x, k)   B( x)   C( k)   T( k)   E( k)   G( x, k)   V( k)   Z( k)

Proof of Theorem dvfsum2

Dummy variable m is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dvfsum2.2	. . . . . 6 |- ( ph -> Y e. S )
2		fzfid 12772	. . . . . . . 8 |- ( ph -> ( M ... ( |_ ` Y ) ) e. Fin )
3		dvfsum2.b2	. . . . . . . . . 10 |- ( ( ph /\ x e. Z ) -> B e. RR )
4	3	ralrimiva 2966	. . . . . . . . 9 |- ( ph -> A. x e. Z B e. RR )
5		elfzuz 12338	. . . . . . . . . 10 |- ( k e. ( M ... ( |_ ` Y ) ) -> k e. ( ZZ>= ` M ) )
6		dvfsum2.z	. . . . . . . . . 10 |- Z = ( ZZ>= ` M )
7	5, 6	syl6eleqr 2712	. . . . . . . . 9 |- ( k e. ( M ... ( |_ ` Y ) ) -> k e. Z )
8		dvfsum2.c	. . . . . . . . . . 11 |- ( x = k -> B = C )
9	8	eleq1d 2686	. . . . . . . . . 10 |- ( x = k -> ( B e. RR <-> C e. RR ) )
10	9	rspccva 3308	. . . . . . . . 9 |- ( ( A. x e. Z B e. RR /\ k e. Z ) -> C e. RR )
11	4, 7, 10	syl2an 494	. . . . . . . 8 |- ( ( ph /\ k e. ( M ... ( |_ ` Y ) ) ) -> C e. RR )
12	2, 11	fsumrecl 14465	. . . . . . 7 |- ( ph -> sum_ k e. ( M ... ( |_ ` Y ) ) C e. RR )
13		dvfsum2.a	. . . . . . . . 9 |- ( ( ph /\ x e. S ) -> A e. RR )
14	13	ralrimiva 2966	. . . . . . . 8 |- ( ph -> A. x e. S A e. RR )
15		nfcsb1v 3549	. . . . . . . . . 10 |- F/_ x [_ Y / x ]_ A
16	15	nfel1 2779	. . . . . . . . 9 |- F/ x [_ Y / x ]_ A e. RR
17		csbeq1a 3542	. . . . . . . . . 10 |- ( x = Y -> A = [_ Y / x ]_ A )
18	17	eleq1d 2686	. . . . . . . . 9 |- ( x = Y -> ( A e. RR <-> [_ Y / x ]_ A e. RR ) )
19	16, 18	rspc 3303	. . . . . . . 8 |- ( Y e. S -> ( A. x e. S A e. RR -> [_ Y / x ]_ A e. RR ) )
20	1, 14, 19	sylc 65	. . . . . . 7 |- ( ph -> [_ Y / x ]_ A e. RR )
21	12, 20	resubcld 10458	. . . . . 6 |- ( ph -> ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) e. RR )
22		nfcv 2764	. . . . . . 7 |- F/_ x Y
23		nfcv 2764	. . . . . . . 8 |- F/_ x sum_ k e. ( M ... ( |_ ` Y ) ) C
24		nfcv 2764	. . . . . . . 8 |- F/_ x -
25	23, 24, 15	nfov 6676	. . . . . . 7 |- F/_ x ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A )
26		fveq2 6191	. . . . . . . . . 10 |- ( x = Y -> ( |_ ` x ) = ( |_ ` Y ) )
27	26	oveq2d 6666	. . . . . . . . 9 |- ( x = Y -> ( M ... ( |_ ` x ) ) = ( M ... ( |_ ` Y ) ) )
28	27	sumeq1d 14431	. . . . . . . 8 |- ( x = Y -> sum_ k e. ( M ... ( |_ ` x ) ) C = sum_ k e. ( M ... ( |_ ` Y ) ) C )
29	28, 17	oveq12d 6668	. . . . . . 7 |- ( x = Y -> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) = ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) )
30		dvfsum2.g	. . . . . . 7 |- G = ( x e. S |-> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) )
31	22, 25, 29, 30	fvmptf 6301	. . . . . 6 |- ( ( Y e. S /\ ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) e. RR ) -> ( G ` Y ) = ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) )
32	1, 21, 31	syl2anc 693	. . . . 5 |- ( ph -> ( G ` Y ) = ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) )
33		dvfsum2.1	. . . . . 6 |- ( ph -> X e. S )
34		fzfid 12772	. . . . . . . 8 |- ( ph -> ( M ... ( |_ ` X ) ) e. Fin )
35		elfzuz 12338	. . . . . . . . . 10 |- ( k e. ( M ... ( |_ ` X ) ) -> k e. ( ZZ>= ` M ) )
36	35, 6	syl6eleqr 2712	. . . . . . . . 9 |- ( k e. ( M ... ( |_ ` X ) ) -> k e. Z )
37	4, 36, 10	syl2an 494	. . . . . . . 8 |- ( ( ph /\ k e. ( M ... ( |_ ` X ) ) ) -> C e. RR )
38	34, 37	fsumrecl 14465	. . . . . . 7 |- ( ph -> sum_ k e. ( M ... ( |_ ` X ) ) C e. RR )
39		nfcsb1v 3549	. . . . . . . . . 10 |- F/_ x [_ X / x ]_ A
40	39	nfel1 2779	. . . . . . . . 9 |- F/ x [_ X / x ]_ A e. RR
41		csbeq1a 3542	. . . . . . . . . 10 |- ( x = X -> A = [_ X / x ]_ A )
42	41	eleq1d 2686	. . . . . . . . 9 |- ( x = X -> ( A e. RR <-> [_ X / x ]_ A e. RR ) )
43	40, 42	rspc 3303	. . . . . . . 8 |- ( X e. S -> ( A. x e. S A e. RR -> [_ X / x ]_ A e. RR ) )
44	33, 14, 43	sylc 65	. . . . . . 7 |- ( ph -> [_ X / x ]_ A e. RR )
45	38, 44	resubcld 10458	. . . . . 6 |- ( ph -> ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) e. RR )
46		nfcv 2764	. . . . . . 7 |- F/_ x X
47		nfcv 2764	. . . . . . . 8 |- F/_ x sum_ k e. ( M ... ( |_ ` X ) ) C
48	47, 24, 39	nfov 6676	. . . . . . 7 |- F/_ x ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A )
49		fveq2 6191	. . . . . . . . . 10 |- ( x = X -> ( |_ ` x ) = ( |_ ` X ) )
50	49	oveq2d 6666	. . . . . . . . 9 |- ( x = X -> ( M ... ( |_ ` x ) ) = ( M ... ( |_ ` X ) ) )
51	50	sumeq1d 14431	. . . . . . . 8 |- ( x = X -> sum_ k e. ( M ... ( |_ ` x ) ) C = sum_ k e. ( M ... ( |_ ` X ) ) C )
52	51, 41	oveq12d 6668	. . . . . . 7 |- ( x = X -> ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) = ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) )
53	46, 48, 52, 30	fvmptf 6301	. . . . . 6 |- ( ( X e. S /\ ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) e. RR ) -> ( G ` X ) = ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) )
54	33, 45, 53	syl2anc 693	. . . . 5 |- ( ph -> ( G ` X ) = ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) )
55	32, 54	oveq12d 6668	. . . 4 |- ( ph -> ( ( G ` Y ) - ( G ` X ) ) = ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) - ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) )
56	55	fveq2d 6195	. . 3 |- ( ph -> ( abs ` ( ( G ` Y ) - ( G ` X ) ) ) = ( abs ` ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) - ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) ) )
57	21	recnd 10068	. . . 4 |- ( ph -> ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) e. CC )
58	45	recnd 10068	. . . 4 |- ( ph -> ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) e. CC )
59	57, 58	abssubd 14192	. . 3 |- ( ph -> ( abs ` ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) - ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) ) = ( abs ` ( ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) - ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) ) )
60	56, 59	eqtrd 2656	. 2 |- ( ph -> ( abs ` ( ( G ` Y ) - ( G ` X ) ) ) = ( abs ` ( ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) - ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) ) )
61		dvfsum2.s	. . . . . . . . . 10 |- S = ( T (,) +oo )
62		ioossre 12235	. . . . . . . . . 10 |- ( T (,) +oo ) C_ RR
63	61, 62	eqsstri 3635	. . . . . . . . 9 |- S C_ RR
64	63	a1i 11	. . . . . . . 8 |- ( ph -> S C_ RR )
65		dvfsum2.b1	. . . . . . . 8 |- ( ( ph /\ x e. S ) -> B e. V )
66		dvfsum2.b3	. . . . . . . 8 |- ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )
67	64, 13, 65, 66	dvmptrecl 23787	. . . . . . 7 |- ( ( ph /\ x e. S ) -> B e. RR )
68	67	ralrimiva 2966	. . . . . 6 |- ( ph -> A. x e. S B e. RR )
69		dvfsum2.e	. . . . . . . 8 |- ( x = Y -> B = E )
70	69	eleq1d 2686	. . . . . . 7 |- ( x = Y -> ( B e. RR <-> E e. RR ) )
71	70	rspcv 3305	. . . . . 6 |- ( Y e. S -> ( A. x e. S B e. RR -> E e. RR ) )
72	1, 68, 71	sylc 65	. . . . 5 |- ( ph -> E e. RR )
73	21, 72	resubcld 10458	. . . 4 |- ( ph -> ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) - E ) e. RR )
74	63, 33	sseldi 3601	. . . . . . . 8 |- ( ph -> X e. RR )
75		reflcl 12597	. . . . . . . . 9 |- ( X e. RR -> ( |_ ` X ) e. RR )
76	74, 75	syl 17	. . . . . . . 8 |- ( ph -> ( |_ ` X ) e. RR )
77	74, 76	resubcld 10458	. . . . . . 7 |- ( ph -> ( X - ( |_ ` X ) ) e. RR )
78		nfv 1843	. . . . . . . . . 10 |- F/ m B e. RR
79		nfcsb1v 3549	. . . . . . . . . . 11 |- F/_ x [_ m / x ]_ B
80	79	nfel1 2779	. . . . . . . . . 10 |- F/ x [_ m / x ]_ B e. RR
81		csbeq1a 3542	. . . . . . . . . . 11 |- ( x = m -> B = [_ m / x ]_ B )
82	81	eleq1d 2686	. . . . . . . . . 10 |- ( x = m -> ( B e. RR <-> [_ m / x ]_ B e. RR ) )
83	78, 80, 82	cbvral 3167	. . . . . . . . 9 |- ( A. x e. S B e. RR <-> A. m e. S [_ m / x ]_ B e. RR )
84	68, 83	sylib 208	. . . . . . . 8 |- ( ph -> A. m e. S [_ m / x ]_ B e. RR )
85		csbeq1 3536	. . . . . . . . . 10 |- ( m = X -> [_ m / x ]_ B = [_ X / x ]_ B )
86	85	eleq1d 2686	. . . . . . . . 9 |- ( m = X -> ( [_ m / x ]_ B e. RR <-> [_ X / x ]_ B e. RR ) )
87	86	rspcv 3305	. . . . . . . 8 |- ( X e. S -> ( A. m e. S [_ m / x ]_ B e. RR -> [_ X / x ]_ B e. RR ) )
88	33, 84, 87	sylc 65	. . . . . . 7 |- ( ph -> [_ X / x ]_ B e. RR )
89	77, 88	remulcld 10070	. . . . . 6 |- ( ph -> ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) e. RR )
90	89, 45	readdcld 10069	. . . . 5 |- ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) e. RR )
91	90, 88	resubcld 10458	. . . 4 |- ( ph -> ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) - [_ X / x ]_ B ) e. RR )
92	63, 1	sseldi 3601	. . . . . . . . 9 |- ( ph -> Y e. RR )
93		reflcl 12597	. . . . . . . . . 10 |- ( Y e. RR -> ( |_ ` Y ) e. RR )
94	92, 93	syl 17	. . . . . . . . 9 |- ( ph -> ( |_ ` Y ) e. RR )
95	92, 94	resubcld 10458	. . . . . . . 8 |- ( ph -> ( Y - ( |_ ` Y ) ) e. RR )
96	95, 72	remulcld 10070	. . . . . . 7 |- ( ph -> ( ( Y - ( |_ ` Y ) ) x. E ) e. RR )
97	96, 21	readdcld 10069	. . . . . 6 |- ( ph -> ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) e. RR )
98	97, 72	resubcld 10458	. . . . 5 |- ( ph -> ( ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) - E ) e. RR )
99		fracge0 12605	. . . . . . . . 9 |- ( Y e. RR -> 0 <_ ( Y - ( |_ ` Y ) ) )
100	92, 99	syl 17	. . . . . . . 8 |- ( ph -> 0 <_ ( Y - ( |_ ` Y ) ) )
101		dvfsum2.0	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. S /\ D <_ x ) ) -> 0 <_ B )
102	101	expr 643	. . . . . . . . . 10 |- ( ( ph /\ x e. S ) -> ( D <_ x -> 0 <_ B ) )
103	102	ralrimiva 2966	. . . . . . . . 9 |- ( ph -> A. x e. S ( D <_ x -> 0 <_ B ) )
104		dvfsum2.d	. . . . . . . . . 10 |- ( ph -> D e. RR )
105		dvfsum2.3	. . . . . . . . . 10 |- ( ph -> D <_ X )
106		dvfsum2.4	. . . . . . . . . 10 |- ( ph -> X <_ Y )
107	104, 74, 92, 105, 106	letrd 10194	. . . . . . . . 9 |- ( ph -> D <_ Y )
108		breq2 4657	. . . . . . . . . . 11 |- ( x = Y -> ( D <_ x <-> D <_ Y ) )
109	69	breq2d 4665	. . . . . . . . . . 11 |- ( x = Y -> ( 0 <_ B <-> 0 <_ E ) )
110	108, 109	imbi12d 334	. . . . . . . . . 10 |- ( x = Y -> ( ( D <_ x -> 0 <_ B ) <-> ( D <_ Y -> 0 <_ E ) ) )
111	110	rspcv 3305	. . . . . . . . 9 |- ( Y e. S -> ( A. x e. S ( D <_ x -> 0 <_ B ) -> ( D <_ Y -> 0 <_ E ) ) )
112	1, 103, 107, 111	syl3c 66	. . . . . . . 8 |- ( ph -> 0 <_ E )
113	95, 72, 100, 112	mulge0d 10604	. . . . . . 7 |- ( ph -> 0 <_ ( ( Y - ( |_ ` Y ) ) x. E ) )
114	21, 96	addge02d 10616	. . . . . . 7 |- ( ph -> ( 0 <_ ( ( Y - ( |_ ` Y ) ) x. E ) <-> ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) <_ ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) ) )
115	113, 114	mpbid 222	. . . . . 6 |- ( ph -> ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) <_ ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) )
116	21, 97, 72, 115	lesub1dd 10643	. . . . 5 |- ( ph -> ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) - E ) <_ ( ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) - E ) )
117		dvfsum2.m	. . . . . . . . . . 11 |- ( ph -> M e. ZZ )
118		dvfsum2.md	. . . . . . . . . . 11 |- ( ph -> M <_ ( D + 1 ) )
119		dvfsum2.t	. . . . . . . . . . 11 |- ( ph -> T e. RR )
120	13	renegcld 10457	. . . . . . . . . . 11 |- ( ( ph /\ x e. S ) -> -u A e. RR )
121	67	renegcld 10457	. . . . . . . . . . 11 |- ( ( ph /\ x e. S ) -> -u B e. RR )
122	3	renegcld 10457	. . . . . . . . . . 11 |- ( ( ph /\ x e. Z ) -> -u B e. RR )
123		reelprrecn 10028	. . . . . . . . . . . . 13 |- RR e. { RR , CC }
124	123	a1i 11	. . . . . . . . . . . 12 |- ( ph -> RR e. { RR , CC } )
125	13	recnd 10068	. . . . . . . . . . . 12 |- ( ( ph /\ x e. S ) -> A e. CC )
126	124, 125, 65, 66	dvmptneg 23729	. . . . . . . . . . 11 |- ( ph -> ( RR _D ( x e. S |-> -u A ) ) = ( x e. S |-> -u B ) )
127	8	negeqd 10275	. . . . . . . . . . 11 |- ( x = k -> -u B = -u C )
128		dvfsum2.u	. . . . . . . . . . 11 |- ( ph -> U e. RR* )
129		dvfsum2.l	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> B <_ C )
130	67	adantrr 753	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. S /\ k e. S ) ) -> B e. RR )
131	130	3adant3 1081	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> B e. RR )
132		simp2r 1088	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> k e. S )
133	68	3ad2ant1 1082	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> A. x e. S B e. RR )
134	9	rspcv 3305	. . . . . . . . . . . . . 14 |- ( k e. S -> ( A. x e. S B e. RR -> C e. RR ) )
135	132, 133, 134	sylc 65	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> C e. RR )
136	131, 135	lenegd 10606	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> ( B <_ C <-> -u C <_ -u B ) )
137	129, 136	mpbid 222	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> -u C <_ -u B )
138		eqid 2622	. . . . . . . . . . 11 |- ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. -u B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) ) ) = ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. -u B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) ) )
139		dvfsum2.5	. . . . . . . . . . 11 |- ( ph -> Y <_ U )
140	61, 6, 117, 104, 118, 119, 120, 121, 122, 126, 127, 128, 137, 138, 33, 1, 105, 106, 139	dvfsumlem3 23791	. . . . . . . . . 10 |- ( ph -> ( ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. -u B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) ) ) ` Y ) <_ ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. -u B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) ) ) ` X ) /\ ( ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. -u B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) ) ) ` X ) - [_ X / x ]_ -u B ) <_ ( ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. -u B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) ) ) ` Y ) - [_ Y / x ]_ -u B ) ) )
141	140	simprd 479	. . . . . . . . 9 |- ( ph -> ( ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. -u B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) ) ) ` X ) - [_ X / x ]_ -u B ) <_ ( ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. -u B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) ) ) ` Y ) - [_ Y / x ]_ -u B ) )
142	77	recnd 10068	. . . . . . . . . . . . . . . 16 |- ( ph -> ( X - ( |_ ` X ) ) e. CC )
143	88	recnd 10068	. . . . . . . . . . . . . . . 16 |- ( ph -> [_ X / x ]_ B e. CC )
144	142, 143	mulneg2d 10484	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( X - ( |_ ` X ) ) x. -u [_ X / x ]_ B ) = -u ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) )
145	38	recnd 10068	. . . . . . . . . . . . . . . . 17 |- ( ph -> sum_ k e. ( M ... ( |_ ` X ) ) C e. CC )
146	44	recnd 10068	. . . . . . . . . . . . . . . . 17 |- ( ph -> [_ X / x ]_ A e. CC )
147	145, 146	neg2subd 10409	. . . . . . . . . . . . . . . 16 |- ( ph -> ( -u sum_ k e. ( M ... ( |_ ` X ) ) C - -u [_ X / x ]_ A ) = ( [_ X / x ]_ A - sum_ k e. ( M ... ( |_ ` X ) ) C ) )
148	37	recnd 10068	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. ( M ... ( |_ ` X ) ) ) -> C e. CC )
149	34, 148	fsumneg 14519	. . . . . . . . . . . . . . . . 17 |- ( ph -> sum_ k e. ( M ... ( |_ ` X ) ) -u C = -u sum_ k e. ( M ... ( |_ ` X ) ) C )
150	149	oveq1d 6665	. . . . . . . . . . . . . . . 16 |- ( ph -> ( sum_ k e. ( M ... ( |_ ` X ) ) -u C - -u [_ X / x ]_ A ) = ( -u sum_ k e. ( M ... ( |_ ` X ) ) C - -u [_ X / x ]_ A ) )
151	145, 146	negsubdi2d 10408	. . . . . . . . . . . . . . . 16 |- ( ph -> -u ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) = ( [_ X / x ]_ A - sum_ k e. ( M ... ( |_ ` X ) ) C ) )
152	147, 150, 151	3eqtr4d 2666	. . . . . . . . . . . . . . 15 |- ( ph -> ( sum_ k e. ( M ... ( |_ ` X ) ) -u C - -u [_ X / x ]_ A ) = -u ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) )
153	144, 152	oveq12d 6668	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( X - ( |_ ` X ) ) x. -u [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) -u C - -u [_ X / x ]_ A ) ) = ( -u ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + -u ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) )
154	89	recnd 10068	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) e. CC )
155	154, 58	negdid 10405	. . . . . . . . . . . . . 14 |- ( ph -> -u ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) = ( -u ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + -u ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) )
156	153, 155	eqtr4d 2659	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( X - ( |_ ` X ) ) x. -u [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) -u C - -u [_ X / x ]_ A ) ) = -u ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) )
157	90	renegcld 10457	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) e. RR )
158	156, 157	eqeltrd 2701	. . . . . . . . . . . 12 |- ( ph -> ( ( ( X - ( |_ ` X ) ) x. -u [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) -u C - -u [_ X / x ]_ A ) ) e. RR )
159		nfcv 2764	. . . . . . . . . . . . . . 15 |- F/_ x ( X - ( |_ ` X ) )
160		nfcv 2764	. . . . . . . . . . . . . . 15 |- F/_ x x.
161		nfcsb1v 3549	. . . . . . . . . . . . . . . 16 |- F/_ x [_ X / x ]_ B
162	161	nfneg 10277	. . . . . . . . . . . . . . 15 |- F/_ x -u [_ X / x ]_ B
163	159, 160, 162	nfov 6676	. . . . . . . . . . . . . 14 |- F/_ x ( ( X - ( |_ ` X ) ) x. -u [_ X / x ]_ B )
164		nfcv 2764	. . . . . . . . . . . . . 14 |- F/_ x +
165		nfcv 2764	. . . . . . . . . . . . . . 15 |- F/_ x sum_ k e. ( M ... ( |_ ` X ) ) -u C
166	39	nfneg 10277	. . . . . . . . . . . . . . 15 |- F/_ x -u [_ X / x ]_ A
167	165, 24, 166	nfov 6676	. . . . . . . . . . . . . 14 |- F/_ x ( sum_ k e. ( M ... ( |_ ` X ) ) -u C - -u [_ X / x ]_ A )
168	163, 164, 167	nfov 6676	. . . . . . . . . . . . 13 |- F/_ x ( ( ( X - ( |_ ` X ) ) x. -u [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) -u C - -u [_ X / x ]_ A ) )
169		id 22	. . . . . . . . . . . . . . . 16 |- ( x = X -> x = X )
170	169, 49	oveq12d 6668	. . . . . . . . . . . . . . 15 |- ( x = X -> ( x - ( |_ ` x ) ) = ( X - ( |_ ` X ) ) )
171		csbeq1a 3542	. . . . . . . . . . . . . . . 16 |- ( x = X -> B = [_ X / x ]_ B )
172	171	negeqd 10275	. . . . . . . . . . . . . . 15 |- ( x = X -> -u B = -u [_ X / x ]_ B )
173	170, 172	oveq12d 6668	. . . . . . . . . . . . . 14 |- ( x = X -> ( ( x - ( |_ ` x ) ) x. -u B ) = ( ( X - ( |_ ` X ) ) x. -u [_ X / x ]_ B ) )
174	50	sumeq1d 14431	. . . . . . . . . . . . . . 15 |- ( x = X -> sum_ k e. ( M ... ( |_ ` x ) ) -u C = sum_ k e. ( M ... ( |_ ` X ) ) -u C )
175	41	negeqd 10275	. . . . . . . . . . . . . . 15 |- ( x = X -> -u A = -u [_ X / x ]_ A )
176	174, 175	oveq12d 6668	. . . . . . . . . . . . . 14 |- ( x = X -> ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) = ( sum_ k e. ( M ... ( |_ ` X ) ) -u C - -u [_ X / x ]_ A ) )
177	173, 176	oveq12d 6668	. . . . . . . . . . . . 13 |- ( x = X -> ( ( ( x - ( |_ ` x ) ) x. -u B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) ) = ( ( ( X - ( |_ ` X ) ) x. -u [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) -u C - -u [_ X / x ]_ A ) ) )
178	46, 168, 177, 138	fvmptf 6301	. . . . . . . . . . . 12 |- ( ( X e. S /\ ( ( ( X - ( |_ ` X ) ) x. -u [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) -u C - -u [_ X / x ]_ A ) ) e. RR ) -> ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. -u B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) ) ) ` X ) = ( ( ( X - ( |_ ` X ) ) x. -u [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) -u C - -u [_ X / x ]_ A ) ) )
179	33, 158, 178	syl2anc 693	. . . . . . . . . . 11 |- ( ph -> ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. -u B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) ) ) ` X ) = ( ( ( X - ( |_ ` X ) ) x. -u [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) -u C - -u [_ X / x ]_ A ) ) )
180	179, 156	eqtrd 2656	. . . . . . . . . 10 |- ( ph -> ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. -u B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) ) ) ` X ) = -u ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) )
181		csbnegg 10278	. . . . . . . . . . 11 |- ( X e. S -> [_ X / x ]_ -u B = -u [_ X / x ]_ B )
182	33, 181	syl 17	. . . . . . . . . 10 |- ( ph -> [_ X / x ]_ -u B = -u [_ X / x ]_ B )
183	180, 182	oveq12d 6668	. . . . . . . . 9 |- ( ph -> ( ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. -u B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) ) ) ` X ) - [_ X / x ]_ -u B ) = ( -u ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) - -u [_ X / x ]_ B ) )
184	95	recnd 10068	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Y - ( |_ ` Y ) ) e. CC )
185	72	recnd 10068	. . . . . . . . . . . . . . . 16 |- ( ph -> E e. CC )
186	184, 185	mulneg2d 10484	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( Y - ( |_ ` Y ) ) x. -u E ) = -u ( ( Y - ( |_ ` Y ) ) x. E ) )
187	12	recnd 10068	. . . . . . . . . . . . . . . . 17 |- ( ph -> sum_ k e. ( M ... ( |_ ` Y ) ) C e. CC )
188	20	recnd 10068	. . . . . . . . . . . . . . . . 17 |- ( ph -> [_ Y / x ]_ A e. CC )
189	187, 188	neg2subd 10409	. . . . . . . . . . . . . . . 16 |- ( ph -> ( -u sum_ k e. ( M ... ( |_ ` Y ) ) C - -u [_ Y / x ]_ A ) = ( [_ Y / x ]_ A - sum_ k e. ( M ... ( |_ ` Y ) ) C ) )
190	11	recnd 10068	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. ( M ... ( |_ ` Y ) ) ) -> C e. CC )
191	2, 190	fsumneg 14519	. . . . . . . . . . . . . . . . 17 |- ( ph -> sum_ k e. ( M ... ( |_ ` Y ) ) -u C = -u sum_ k e. ( M ... ( |_ ` Y ) ) C )
192	191	oveq1d 6665	. . . . . . . . . . . . . . . 16 |- ( ph -> ( sum_ k e. ( M ... ( |_ ` Y ) ) -u C - -u [_ Y / x ]_ A ) = ( -u sum_ k e. ( M ... ( |_ ` Y ) ) C - -u [_ Y / x ]_ A ) )
193	187, 188	negsubdi2d 10408	. . . . . . . . . . . . . . . 16 |- ( ph -> -u ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) = ( [_ Y / x ]_ A - sum_ k e. ( M ... ( |_ ` Y ) ) C ) )
194	189, 192, 193	3eqtr4d 2666	. . . . . . . . . . . . . . 15 |- ( ph -> ( sum_ k e. ( M ... ( |_ ` Y ) ) -u C - -u [_ Y / x ]_ A ) = -u ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) )
195	186, 194	oveq12d 6668	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( Y - ( |_ ` Y ) ) x. -u E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) -u C - -u [_ Y / x ]_ A ) ) = ( -u ( ( Y - ( |_ ` Y ) ) x. E ) + -u ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) )
196	96	recnd 10068	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( Y - ( |_ ` Y ) ) x. E ) e. CC )
197	196, 57	negdid 10405	. . . . . . . . . . . . . 14 |- ( ph -> -u ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) = ( -u ( ( Y - ( |_ ` Y ) ) x. E ) + -u ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) )
198	195, 197	eqtr4d 2659	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( Y - ( |_ ` Y ) ) x. -u E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) -u C - -u [_ Y / x ]_ A ) ) = -u ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) )
199	97	renegcld 10457	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) e. RR )
200	198, 199	eqeltrd 2701	. . . . . . . . . . . 12 |- ( ph -> ( ( ( Y - ( |_ ` Y ) ) x. -u E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) -u C - -u [_ Y / x ]_ A ) ) e. RR )
201		nfcv 2764	. . . . . . . . . . . . . 14 |- F/_ x ( ( Y - ( |_ ` Y ) ) x. -u E )
202		nfcv 2764	. . . . . . . . . . . . . . 15 |- F/_ x sum_ k e. ( M ... ( |_ ` Y ) ) -u C
203	15	nfneg 10277	. . . . . . . . . . . . . . 15 |- F/_ x -u [_ Y / x ]_ A
204	202, 24, 203	nfov 6676	. . . . . . . . . . . . . 14 |- F/_ x ( sum_ k e. ( M ... ( |_ ` Y ) ) -u C - -u [_ Y / x ]_ A )
205	201, 164, 204	nfov 6676	. . . . . . . . . . . . 13 |- F/_ x ( ( ( Y - ( |_ ` Y ) ) x. -u E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) -u C - -u [_ Y / x ]_ A ) )
206		id 22	. . . . . . . . . . . . . . . 16 |- ( x = Y -> x = Y )
207	206, 26	oveq12d 6668	. . . . . . . . . . . . . . 15 |- ( x = Y -> ( x - ( |_ ` x ) ) = ( Y - ( |_ ` Y ) ) )
208	69	negeqd 10275	. . . . . . . . . . . . . . 15 |- ( x = Y -> -u B = -u E )
209	207, 208	oveq12d 6668	. . . . . . . . . . . . . 14 |- ( x = Y -> ( ( x - ( |_ ` x ) ) x. -u B ) = ( ( Y - ( |_ ` Y ) ) x. -u E ) )
210	27	sumeq1d 14431	. . . . . . . . . . . . . . 15 |- ( x = Y -> sum_ k e. ( M ... ( |_ ` x ) ) -u C = sum_ k e. ( M ... ( |_ ` Y ) ) -u C )
211	17	negeqd 10275	. . . . . . . . . . . . . . 15 |- ( x = Y -> -u A = -u [_ Y / x ]_ A )
212	210, 211	oveq12d 6668	. . . . . . . . . . . . . 14 |- ( x = Y -> ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) = ( sum_ k e. ( M ... ( |_ ` Y ) ) -u C - -u [_ Y / x ]_ A ) )
213	209, 212	oveq12d 6668	. . . . . . . . . . . . 13 |- ( x = Y -> ( ( ( x - ( |_ ` x ) ) x. -u B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) ) = ( ( ( Y - ( |_ ` Y ) ) x. -u E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) -u C - -u [_ Y / x ]_ A ) ) )
214	22, 205, 213, 138	fvmptf 6301	. . . . . . . . . . . 12 |- ( ( Y e. S /\ ( ( ( Y - ( |_ ` Y ) ) x. -u E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) -u C - -u [_ Y / x ]_ A ) ) e. RR ) -> ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. -u B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) ) ) ` Y ) = ( ( ( Y - ( |_ ` Y ) ) x. -u E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) -u C - -u [_ Y / x ]_ A ) ) )
215	1, 200, 214	syl2anc 693	. . . . . . . . . . 11 |- ( ph -> ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. -u B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) ) ) ` Y ) = ( ( ( Y - ( |_ ` Y ) ) x. -u E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) -u C - -u [_ Y / x ]_ A ) ) )
216	215, 198	eqtrd 2656	. . . . . . . . . 10 |- ( ph -> ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. -u B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) ) ) ` Y ) = -u ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) )
217	208	adantl 482	. . . . . . . . . . 11 |- ( ( ph /\ x = Y ) -> -u B = -u E )
218	1, 217	csbied 3560	. . . . . . . . . 10 |- ( ph -> [_ Y / x ]_ -u B = -u E )
219	216, 218	oveq12d 6668	. . . . . . . . 9 |- ( ph -> ( ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. -u B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) ) ) ` Y ) - [_ Y / x ]_ -u B ) = ( -u ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) - -u E ) )
220	141, 183, 219	3brtr3d 4684	. . . . . . . 8 |- ( ph -> ( -u ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) - -u [_ X / x ]_ B ) <_ ( -u ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) - -u E ) )
221	90	recnd 10068	. . . . . . . . 9 |- ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) e. CC )
222	221, 143	neg2subd 10409	. . . . . . . 8 |- ( ph -> ( -u ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) - -u [_ X / x ]_ B ) = ( [_ X / x ]_ B - ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) ) )
223	97	recnd 10068	. . . . . . . . 9 |- ( ph -> ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) e. CC )
224	223, 185	neg2subd 10409	. . . . . . . 8 |- ( ph -> ( -u ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) - -u E ) = ( E - ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) ) )
225	220, 222, 224	3brtr3d 4684	. . . . . . 7 |- ( ph -> ( [_ X / x ]_ B - ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) ) <_ ( E - ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) ) )
226	221, 143	negsubdi2d 10408	. . . . . . 7 |- ( ph -> -u ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) - [_ X / x ]_ B ) = ( [_ X / x ]_ B - ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) ) )
227	223, 185	negsubdi2d 10408	. . . . . . 7 |- ( ph -> -u ( ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) - E ) = ( E - ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) ) )
228	225, 226, 227	3brtr4d 4685	. . . . . 6 |- ( ph -> -u ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) - [_ X / x ]_ B ) <_ -u ( ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) - E ) )
229	98, 91	lenegd 10606	. . . . . 6 |- ( ph -> ( ( ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) - E ) <_ ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) - [_ X / x ]_ B ) <-> -u ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) - [_ X / x ]_ B ) <_ -u ( ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) - E ) ) )
230	228, 229	mpbird 247	. . . . 5 |- ( ph -> ( ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) - E ) <_ ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) - [_ X / x ]_ B ) )
231	73, 98, 91, 116, 230	letrd 10194	. . . 4 |- ( ph -> ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) - E ) <_ ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) - [_ X / x ]_ B ) )
232		1red 10055	. . . . . . . 8 |- ( ph -> 1 e. RR )
233		nfv 1843	. . . . . . . . . . 11 |- F/ x D <_ X
234		nfcv 2764	. . . . . . . . . . . 12 |- F/_ x 0
235		nfcv 2764	. . . . . . . . . . . 12 |- F/_ x <_
236	234, 235, 161	nfbr 4699	. . . . . . . . . . 11 |- F/ x 0 <_ [_ X / x ]_ B
237	233, 236	nfim 1825	. . . . . . . . . 10 |- F/ x ( D <_ X -> 0 <_ [_ X / x ]_ B )
238		breq2 4657	. . . . . . . . . . 11 |- ( x = X -> ( D <_ x <-> D <_ X ) )
239	171	breq2d 4665	. . . . . . . . . . 11 |- ( x = X -> ( 0 <_ B <-> 0 <_ [_ X / x ]_ B ) )
240	238, 239	imbi12d 334	. . . . . . . . . 10 |- ( x = X -> ( ( D <_ x -> 0 <_ B ) <-> ( D <_ X -> 0 <_ [_ X / x ]_ B ) ) )
241	237, 240	rspc 3303	. . . . . . . . 9 |- ( X e. S -> ( A. x e. S ( D <_ x -> 0 <_ B ) -> ( D <_ X -> 0 <_ [_ X / x ]_ B ) ) )
242	33, 103, 105, 241	syl3c 66	. . . . . . . 8 |- ( ph -> 0 <_ [_ X / x ]_ B )
243		fracle1 12604	. . . . . . . . 9 |- ( X e. RR -> ( X - ( |_ ` X ) ) <_ 1 )
244	74, 243	syl 17	. . . . . . . 8 |- ( ph -> ( X - ( |_ ` X ) ) <_ 1 )
245	77, 232, 88, 242, 244	lemul1ad 10963	. . . . . . 7 |- ( ph -> ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) <_ ( 1 x. [_ X / x ]_ B ) )
246	143	mulid2d 10058	. . . . . . 7 |- ( ph -> ( 1 x. [_ X / x ]_ B ) = [_ X / x ]_ B )
247	245, 246	breqtrd 4679	. . . . . 6 |- ( ph -> ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) <_ [_ X / x ]_ B )
248	89, 88, 45, 247	leadd1dd 10641	. . . . 5 |- ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) <_ ( [_ X / x ]_ B + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) )
249	90, 88, 45	lesubadd2d 10626	. . . . 5 |- ( ph -> ( ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) - [_ X / x ]_ B ) <_ ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) <-> ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) <_ ( [_ X / x ]_ B + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) ) )
250	248, 249	mpbird 247	. . . 4 |- ( ph -> ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) - [_ X / x ]_ B ) <_ ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) )
251	73, 91, 45, 231, 250	letrd 10194	. . 3 |- ( ph -> ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) - E ) <_ ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) )
252	21, 72	readdcld 10069	. . . 4 |- ( ph -> ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) + E ) e. RR )
253		fracge0 12605	. . . . . . 7 |- ( X e. RR -> 0 <_ ( X - ( |_ ` X ) ) )
254	74, 253	syl 17	. . . . . 6 |- ( ph -> 0 <_ ( X - ( |_ ` X ) ) )
255	77, 88, 254, 242	mulge0d 10604	. . . . 5 |- ( ph -> 0 <_ ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) )
256	45, 89	addge02d 10616	. . . . 5 |- ( ph -> ( 0 <_ ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) <-> ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) <_ ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) ) )
257	255, 256	mpbid 222	. . . 4 |- ( ph -> ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) <_ ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) )
258	140	simpld 475	. . . . . . 7 |- ( ph -> ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. -u B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) ) ) ` Y ) <_ ( ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. -u B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) -u C - -u A ) ) ) ` X ) )
259	258, 216, 180	3brtr3d 4684	. . . . . 6 |- ( ph -> -u ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) <_ -u ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) )
260	90, 97	lenegd 10606	. . . . . 6 |- ( ph -> ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) <_ ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) <-> -u ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) <_ -u ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) ) )
261	259, 260	mpbird 247	. . . . 5 |- ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) <_ ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) )
262		fracle1 12604	. . . . . . . . . 10 |- ( Y e. RR -> ( Y - ( |_ ` Y ) ) <_ 1 )
263	92, 262	syl 17	. . . . . . . . 9 |- ( ph -> ( Y - ( |_ ` Y ) ) <_ 1 )
264	95, 232, 72, 112, 263	lemul1ad 10963	. . . . . . . 8 |- ( ph -> ( ( Y - ( |_ ` Y ) ) x. E ) <_ ( 1 x. E ) )
265	185	mulid2d 10058	. . . . . . . 8 |- ( ph -> ( 1 x. E ) = E )
266	264, 265	breqtrd 4679	. . . . . . 7 |- ( ph -> ( ( Y - ( |_ ` Y ) ) x. E ) <_ E )
267	96, 72, 21, 266	leadd1dd 10641	. . . . . 6 |- ( ph -> ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) <_ ( E + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) )
268	185, 57	addcomd 10238	. . . . . 6 |- ( ph -> ( E + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) = ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) + E ) )
269	267, 268	breqtrd 4679	. . . . 5 |- ( ph -> ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) <_ ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) + E ) )
270	90, 97, 252, 261, 269	letrd 10194	. . . 4 |- ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) <_ ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) + E ) )
271	45, 90, 252, 257, 270	letrd 10194	. . 3 |- ( ph -> ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) <_ ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) + E ) )
272	45, 21, 72	absdifled 14173	. . 3 |- ( ph -> ( ( abs ` ( ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) - ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) ) <_ E <-> ( ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) - E ) <_ ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) /\ ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) <_ ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) + E ) ) ) )
273	251, 271, 272	mpbir2and 957	. 2 |- ( ph -> ( abs ` ( ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) - ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) ) <_ E )
274	60, 273	eqbrtrd 4675	1 |- ( ph -> ( abs ` ( ( G ` Y ) - ( G ` X ) ) ) <_ E )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   [_csb 3533   C_ wss 3574   {cpr 4179   class class class wbr 4653   |-> cmpt 4729   ` cfv 5888  (class class class)co 6650   CCcc 9934   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   x. cmul 9941   +oocpnf 10071   RR*cxr 10073   <_ cle 10075   - cmin 10266   -ucneg 10267   ZZcz 11377   ZZ>=cuz 11687   (,)cioo 12175   ...cfz 12326   |_cfl 12591   abscabs 13974   sum_csu 14416   _D cdv 23627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014  ax-addf 10015  ax-mulf 10016

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-fi 8317  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-q 11789  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-ioo 12179  df-ico 12181  df-icc 12182  df-fz 12327  df-fzo 12466  df-fl 12593  df-seq 12802  df-exp 12861  df-hash 13118  df-cj 13839  df-re 13840  df-im 13841  df-sqrt 13975  df-abs 13976  df-clim 14219  df-sum 14417  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-hom 15966  df-cco 15967  df-rest 16083  df-topn 16084  df-0g 16102  df-gsum 16103  df-topgen 16104  df-pt 16105  df-prds 16108  df-xrs 16162  df-qtop 16167  df-imas 16168  df-xps 16170  df-mre 16246  df-mrc 16247  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-submnd 17336  df-mulg 17541  df-cntz 17750  df-cmn 18195  df-psmet 19738  df-xmet 19739  df-met 19740  df-bl 19741  df-mopn 19742  df-fbas 19743  df-fg 19744  df-cnfld 19747  df-top 20699  df-topon 20716  df-topsp 20737  df-bases 20750  df-cld 20823  df-ntr 20824  df-cls 20825  df-nei 20902  df-lp 20940  df-perf 20941  df-cn 21031  df-cnp 21032  df-haus 21119  df-cmp 21190  df-tx 21365  df-hmeo 21558  df-fil 21650  df-fm 21742  df-flim 21743  df-flf 21744  df-xms 22125  df-ms 22126  df-tms 22127  df-cncf 22681  df-limc 23630  df-dv 23631

This theorem is referenced by:  logfacbnd3  24948  log2sumbnd  25233