Theorem dvfsum2 21348

Description: The reverse of dvfsumrlim 21345, 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 11779	. . . . . . . 8 |- ( ph -> ( M ... ( |_ ` Y ) ) e. Fin )
3		dvfsum2.b2	. . . . . . . . . 10 |- ( ( ph /\ x e. Z ) -> B e. RR )
4	3	ralrimiva 2789	. . . . . . . . 9 |- ( ph -> A. x e. Z B e. RR )
5		elfzuz 11436	. . . . . . . . . 10 |- ( k e. ( M ... ( |_ ` Y ) ) -> k e. ( ZZ>= ` M ) )
6		dvfsum2.z	. . . . . . . . . 10 |- Z = ( ZZ>= ` M )
7	5, 6	syl6eleqr 2524	. . . . . . . . 9 |- ( k e. ( M ... ( |_ ` Y ) ) -> k e. Z )
8		dvfsum2.c	. . . . . . . . . . 11 |- ( x = k -> B = C )
9	8	eleq1d 2499	. . . . . . . . . 10 |- ( x = k -> ( B e. RR <-> C e. RR ) )
10	9	rspccva 3061	. . . . . . . . 9 |- ( ( A. x e. Z B e. RR /\ k e. Z ) -> C e. RR )
11	4, 7, 10	syl2an 474	. . . . . . . 8 |- ( ( ph /\ k e. ( M ... ( |_ ` Y ) ) ) -> C e. RR )
12	2, 11	fsumrecl 13195	. . . . . . 7 |- ( ph -> sum_ k e. ( M ... ( |_ ` Y ) ) C e. RR )
13		dvfsum2.a	. . . . . . . . 9 |- ( ( ph /\ x e. S ) -> A e. RR )
14	13	ralrimiva 2789	. . . . . . . 8 |- ( ph -> A. x e. S A e. RR )
15		nfcsb1v 3292	. . . . . . . . . 10 |- F/_ x [_ Y / x ]_ A
16	15	nfel1 2579	. . . . . . . . 9 |- F/ x [_ Y / x ]_ A e. RR
17		csbeq1a 3285	. . . . . . . . . 10 |- ( x = Y -> A = [_ Y / x ]_ A )
18	17	eleq1d 2499	. . . . . . . . 9 |- ( x = Y -> ( A e. RR <-> [_ Y / x ]_ A e. RR ) )
19	16, 18	rspc 3056	. . . . . . . 8 |- ( Y e. S -> ( A. x e. S A e. RR -> [_ Y / x ]_ A e. RR ) )
20	1, 14, 19	sylc 60	. . . . . . 7 |- ( ph -> [_ Y / x ]_ A e. RR )
21	12, 20	resubcld 9764	. . . . . 6 |- ( ph -> ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) e. RR )
22		nfcv 2569	. . . . . . 7 |- F/_ x Y
23		nfcv 2569	. . . . . . . 8 |- F/_ x sum_ k e. ( M ... ( |_ ` Y ) ) C
24		nfcv 2569	. . . . . . . 8 |- F/_ x -
25	23, 24, 15	nfov 6103	. . . . . . 7 |- F/_ x ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A )
26		fveq2 5679	. . . . . . . . . 10 |- ( x = Y -> ( |_ ` x ) = ( |_ ` Y ) )
27	26	oveq2d 6096	. . . . . . . . 9 |- ( x = Y -> ( M ... ( |_ ` x ) ) = ( M ... ( |_ ` Y ) ) )
28	27	sumeq1d 13162	. . . . . . . 8 |- ( x = Y -> sum_ k e. ( M ... ( |_ ` x ) ) C = sum_ k e. ( M ... ( |_ ` Y ) ) C )
29	28, 17	oveq12d 6098	. . . . . . 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 5778	. . . . . 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 654	. . . . 5 |- ( ph -> ( G ` Y ) = ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) )
33		dvfsum2.1	. . . . . 6 |- ( ph -> X e. S )
34		fzfid 11779	. . . . . . . 8 |- ( ph -> ( M ... ( |_ ` X ) ) e. Fin )
35		elfzuz 11436	. . . . . . . . . 10 |- ( k e. ( M ... ( |_ ` X ) ) -> k e. ( ZZ>= ` M ) )
36	35, 6	syl6eleqr 2524	. . . . . . . . 9 |- ( k e. ( M ... ( |_ ` X ) ) -> k e. Z )
37	4, 36, 10	syl2an 474	. . . . . . . 8 |- ( ( ph /\ k e. ( M ... ( |_ ` X ) ) ) -> C e. RR )
38	34, 37	fsumrecl 13195	. . . . . . 7 |- ( ph -> sum_ k e. ( M ... ( |_ ` X ) ) C e. RR )
39		nfcsb1v 3292	. . . . . . . . . 10 |- F/_ x [_ X / x ]_ A
40	39	nfel1 2579	. . . . . . . . 9 |- F/ x [_ X / x ]_ A e. RR
41		csbeq1a 3285	. . . . . . . . . 10 |- ( x = X -> A = [_ X / x ]_ A )
42	41	eleq1d 2499	. . . . . . . . 9 |- ( x = X -> ( A e. RR <-> [_ X / x ]_ A e. RR ) )
43	40, 42	rspc 3056	. . . . . . . 8 |- ( X e. S -> ( A. x e. S A e. RR -> [_ X / x ]_ A e. RR ) )
44	33, 14, 43	sylc 60	. . . . . . 7 |- ( ph -> [_ X / x ]_ A e. RR )
45	38, 44	resubcld 9764	. . . . . 6 |- ( ph -> ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) e. RR )
46		nfcv 2569	. . . . . . 7 |- F/_ x X
47		nfcv 2569	. . . . . . . 8 |- F/_ x sum_ k e. ( M ... ( |_ ` X ) ) C
48	47, 24, 39	nfov 6103	. . . . . . 7 |- F/_ x ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A )
49		fveq2 5679	. . . . . . . . . 10 |- ( x = X -> ( |_ ` x ) = ( |_ ` X ) )
50	49	oveq2d 6096	. . . . . . . . 9 |- ( x = X -> ( M ... ( |_ ` x ) ) = ( M ... ( |_ ` X ) ) )
51	50	sumeq1d 13162	. . . . . . . 8 |- ( x = X -> sum_ k e. ( M ... ( |_ ` x ) ) C = sum_ k e. ( M ... ( |_ ` X ) ) C )
52	51, 41	oveq12d 6098	. . . . . . 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 5778	. . . . . 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 654	. . . . 5 |- ( ph -> ( G ` X ) = ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) )
55	32, 54	oveq12d 6098	. . . 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 5683	. . 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 9400	. . . 4 |- ( ph -> ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) e. CC )
58	45	recnd 9400	. . . 4 |- ( ph -> ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) e. CC )
59	57, 58	abssubd 12923	. . 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 2465	. 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 11345	. . . . . . . . . 10 |- ( T (,) +oo ) C_ RR
63	61, 62	eqsstri 3374	. . . . . . . . 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 21338	. . . . . . 7 |- ( ( ph /\ x e. S ) -> B e. RR )
68	67	ralrimiva 2789	. . . . . 6 |- ( ph -> A. x e. S B e. RR )
69		dvfsum2.e	. . . . . . . 8 |- ( x = Y -> B = E )
70	69	eleq1d 2499	. . . . . . 7 |- ( x = Y -> ( B e. RR <-> E e. RR ) )
71	70	rspcv 3058	. . . . . 6 |- ( Y e. S -> ( A. x e. S B e. RR -> E e. RR ) )
72	1, 68, 71	sylc 60	. . . . 5 |- ( ph -> E e. RR )
73	21, 72	resubcld 9764	. . . 4 |- ( ph -> ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) - E ) e. RR )
74	63, 33	sseldi 3342	. . . . . . . 8 |- ( ph -> X e. RR )
75		reflcl 11630	. . . . . . . . 9 |- ( X e. RR -> ( |_ ` X ) e. RR )
76	74, 75	syl 16	. . . . . . . 8 |- ( ph -> ( |_ ` X ) e. RR )
77	74, 76	resubcld 9764	. . . . . . 7 |- ( ph -> ( X - ( |_ ` X ) ) e. RR )
78		nfv 1672	. . . . . . . . . 10 |- F/ m B e. RR
79		nfcsb1v 3292	. . . . . . . . . . 11 |- F/_ x [_ m / x ]_ B
80	79	nfel1 2579	. . . . . . . . . 10 |- F/ x [_ m / x ]_ B e. RR
81		csbeq1a 3285	. . . . . . . . . . 11 |- ( x = m -> B = [_ m / x ]_ B )
82	81	eleq1d 2499	. . . . . . . . . 10 |- ( x = m -> ( B e. RR <-> [_ m / x ]_ B e. RR ) )
83	78, 80, 82	cbvral 2933	. . . . . . . . 9 |- ( A. x e. S B e. RR <-> A. m e. S [_ m / x ]_ B e. RR )
84	68, 83	sylib 196	. . . . . . . 8 |- ( ph -> A. m e. S [_ m / x ]_ B e. RR )
85		csbeq1 3279	. . . . . . . . . 10 |- ( m = X -> [_ m / x ]_ B = [_ X / x ]_ B )
86	85	eleq1d 2499	. . . . . . . . 9 |- ( m = X -> ( [_ m / x ]_ B e. RR <-> [_ X / x ]_ B e. RR ) )
87	86	rspcv 3058	. . . . . . . 8 |- ( X e. S -> ( A. m e. S [_ m / x ]_ B e. RR -> [_ X / x ]_ B e. RR ) )
88	33, 84, 87	sylc 60	. . . . . . 7 |- ( ph -> [_ X / x ]_ B e. RR )
89	77, 88	remulcld 9402	. . . . . 6 |- ( ph -> ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) e. RR )
90	89, 45	readdcld 9401	. . . . 5 |- ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) e. RR )
91	90, 88	resubcld 9764	. . . 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 3342	. . . . . . . . 9 |- ( ph -> Y e. RR )
93		reflcl 11630	. . . . . . . . . 10 |- ( Y e. RR -> ( |_ ` Y ) e. RR )
94	92, 93	syl 16	. . . . . . . . 9 |- ( ph -> ( |_ ` Y ) e. RR )
95	92, 94	resubcld 9764	. . . . . . . 8 |- ( ph -> ( Y - ( |_ ` Y ) ) e. RR )
96	95, 72	remulcld 9402	. . . . . . 7 |- ( ph -> ( ( Y - ( |_ ` Y ) ) x. E ) e. RR )
97	96, 21	readdcld 9401	. . . . . 6 |- ( ph -> ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) e. RR )
98	97, 72	resubcld 9764	. . . . 5 |- ( ph -> ( ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) - E ) e. RR )
99		fracge0 11638	. . . . . . . . 9 |- ( Y e. RR -> 0 <_ ( Y - ( |_ ` Y ) ) )
100	92, 99	syl 16	. . . . . . . 8 |- ( ph -> 0 <_ ( Y - ( |_ ` Y ) ) )
101		dvfsum2.0	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. S /\ D <_ x ) ) -> 0 <_ B )
102	101	expr 610	. . . . . . . . . 10 |- ( ( ph /\ x e. S ) -> ( D <_ x -> 0 <_ B ) )
103	102	ralrimiva 2789	. . . . . . . . 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 9516	. . . . . . . . 9 |- ( ph -> D <_ Y )
108		breq2 4284	. . . . . . . . . . 11 |- ( x = Y -> ( D <_ x <-> D <_ Y ) )
109	69	breq2d 4292	. . . . . . . . . . 11 |- ( x = Y -> ( 0 <_ B <-> 0 <_ E ) )
110	108, 109	imbi12d 320	. . . . . . . . . 10 |- ( x = Y -> ( ( D <_ x -> 0 <_ B ) <-> ( D <_ Y -> 0 <_ E ) ) )
111	110	rspcv 3058	. . . . . . . . 9 |- ( Y e. S -> ( A. x e. S ( D <_ x -> 0 <_ B ) -> ( D <_ Y -> 0 <_ E ) ) )
112	1, 103, 107, 111	syl3c 61	. . . . . . . 8 |- ( ph -> 0 <_ E )
113	95, 72, 100, 112	mulge0d 9904	. . . . . . 7 |- ( ph -> 0 <_ ( ( Y - ( |_ ` Y ) ) x. E ) )
114	21, 96	addge02d 9916	. . . . . . 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 210	. . . . . 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 9943	. . . . 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 9763	. . . . . . . . . . 11 |- ( ( ph /\ x e. S ) -> -u A e. RR )
121	67	renegcld 9763	. . . . . . . . . . 11 |- ( ( ph /\ x e. S ) -> -u B e. RR )
122	3	renegcld 9763	. . . . . . . . . . 11 |- ( ( ph /\ x e. Z ) -> -u B e. RR )
123		reelprrecn 9362	. . . . . . . . . . . . 13 |- RR e. { RR , CC }
124	123	a1i 11	. . . . . . . . . . . 12 |- ( ph -> RR e. { RR , CC } )
125	13	recnd 9400	. . . . . . . . . . . 12 |- ( ( ph /\ x e. S ) -> A e. CC )
126	124, 125, 65, 66	dvmptneg 21282	. . . . . . . . . . 11 |- ( ph -> ( RR _D ( x e. S |-> -u A ) ) = ( x e. S |-> -u B ) )
127	8	negeqd 9592	. . . . . . . . . . 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 709	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. S /\ k e. S ) ) -> B e. RR )
131	130	3adant3 1001	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> B e. RR )
132		simp2r 1008	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> k e. S )
133	68	3ad2ant1 1002	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> A. x e. S B e. RR )
134	9	rspcv 3058	. . . . . . . . . . . . . 14 |- ( k e. S -> ( A. x e. S B e. RR -> C e. RR ) )
135	132, 133, 134	sylc 60	. . . . . . . . . . . . 13 |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> C e. RR )
136	131, 135	lenegd 9906	. . . . . . . . . . . 12 |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> ( B <_ C <-> -u C <_ -u B ) )
137	129, 136	mpbid 210	. . . . . . . . . . 11 |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> -u C <_ -u B )
138		eqid 2433	. . . . . . . . . . 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 21342	. . . . . . . . . 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 460	. . . . . . . . 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 9400	. . . . . . . . . . . . . . . 16 |- ( ph -> ( X - ( |_ ` X ) ) e. CC )
143	88	recnd 9400	. . . . . . . . . . . . . . . 16 |- ( ph -> [_ X / x ]_ B e. CC )
144	142, 143	mulneg2d 9786	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( X - ( |_ ` X ) ) x. -u [_ X / x ]_ B ) = -u ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) )
145	38	recnd 9400	. . . . . . . . . . . . . . . . 17 |- ( ph -> sum_ k e. ( M ... ( |_ ` X ) ) C e. CC )
146	44	recnd 9400	. . . . . . . . . . . . . . . . 17 |- ( ph -> [_ X / x ]_ A e. CC )
147	145, 146	neg2subd 9724	. . . . . . . . . . . . . . . 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 9400	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. ( M ... ( |_ ` X ) ) ) -> C e. CC )
149	34, 148	fsumneg 13237	. . . . . . . . . . . . . . . . 17 |- ( ph -> sum_ k e. ( M ... ( |_ ` X ) ) -u C = -u sum_ k e. ( M ... ( |_ ` X ) ) C )
150	149	oveq1d 6095	. . . . . . . . . . . . . . . 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 9723	. . . . . . . . . . . . . . . 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 2475	. . . . . . . . . . . . . . 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 6098	. . . . . . . . . . . . . 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 9400	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) e. CC )
155	154, 58	negdid 9720	. . . . . . . . . . . . . 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 2468	. . . . . . . . . . . . 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 9763	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) e. RR )
158	156, 157	eqeltrd 2507	. . . . . . . . . . . 12 |- ( ph -> ( ( ( X - ( |_ ` X ) ) x. -u [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) -u C - -u [_ X / x ]_ A ) ) e. RR )
159		nfcv 2569	. . . . . . . . . . . . . . 15 |- F/_ x ( X - ( |_ ` X ) )
160		nfcv 2569	. . . . . . . . . . . . . . 15 |- F/_ x x.
161		nfcsb1v 3292	. . . . . . . . . . . . . . . 16 |- F/_ x [_ X / x ]_ B
162	161	nfneg 9594	. . . . . . . . . . . . . . 15 |- F/_ x -u [_ X / x ]_ B
163	159, 160, 162	nfov 6103	. . . . . . . . . . . . . 14 |- F/_ x ( ( X - ( |_ ` X ) ) x. -u [_ X / x ]_ B )
164		nfcv 2569	. . . . . . . . . . . . . 14 |- F/_ x +
165		nfcv 2569	. . . . . . . . . . . . . . 15 |- F/_ x sum_ k e. ( M ... ( |_ ` X ) ) -u C
166	39	nfneg 9594	. . . . . . . . . . . . . . 15 |- F/_ x -u [_ X / x ]_ A
167	165, 24, 166	nfov 6103	. . . . . . . . . . . . . 14 |- F/_ x ( sum_ k e. ( M ... ( |_ ` X ) ) -u C - -u [_ X / x ]_ A )
168	163, 164, 167	nfov 6103	. . . . . . . . . . . . 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 6098	. . . . . . . . . . . . . . 15 |- ( x = X -> ( x - ( |_ ` x ) ) = ( X - ( |_ ` X ) ) )
171		csbeq1a 3285	. . . . . . . . . . . . . . . 16 |- ( x = X -> B = [_ X / x ]_ B )
172	171	negeqd 9592	. . . . . . . . . . . . . . 15 |- ( x = X -> -u B = -u [_ X / x ]_ B )
173	170, 172	oveq12d 6098	. . . . . . . . . . . . . 14 |- ( x = X -> ( ( x - ( |_ ` x ) ) x. -u B ) = ( ( X - ( |_ ` X ) ) x. -u [_ X / x ]_ B ) )
174	50	sumeq1d 13162	. . . . . . . . . . . . . . 15 |- ( x = X -> sum_ k e. ( M ... ( |_ ` x ) ) -u C = sum_ k e. ( M ... ( |_ ` X ) ) -u C )
175	41	negeqd 9592	. . . . . . . . . . . . . . 15 |- ( x = X -> -u A = -u [_ X / x ]_ A )
176	174, 175	oveq12d 6098	. . . . . . . . . . . . . 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 6098	. . . . . . . . . . . . 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 5778	. . . . . . . . . . . 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 654	. . . . . . . . . . 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 2465	. . . . . . . . . 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 9595	. . . . . . . . . . 11 |- ( X e. S -> [_ X / x ]_ -u B = -u [_ X / x ]_ B )
182	33, 181	syl 16	. . . . . . . . . 10 |- ( ph -> [_ X / x ]_ -u B = -u [_ X / x ]_ B )
183	180, 182	oveq12d 6098	. . . . . . . . 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 9400	. . . . . . . . . . . . . . . 16 |- ( ph -> ( Y - ( |_ ` Y ) ) e. CC )
185	72	recnd 9400	. . . . . . . . . . . . . . . 16 |- ( ph -> E e. CC )
186	184, 185	mulneg2d 9786	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( Y - ( |_ ` Y ) ) x. -u E ) = -u ( ( Y - ( |_ ` Y ) ) x. E ) )
187	12	recnd 9400	. . . . . . . . . . . . . . . . 17 |- ( ph -> sum_ k e. ( M ... ( |_ ` Y ) ) C e. CC )
188	20	recnd 9400	. . . . . . . . . . . . . . . . 17 |- ( ph -> [_ Y / x ]_ A e. CC )
189	187, 188	neg2subd 9724	. . . . . . . . . . . . . . . 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 9400	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. ( M ... ( |_ ` Y ) ) ) -> C e. CC )
191	2, 190	fsumneg 13237	. . . . . . . . . . . . . . . . 17 |- ( ph -> sum_ k e. ( M ... ( |_ ` Y ) ) -u C = -u sum_ k e. ( M ... ( |_ ` Y ) ) C )
192	191	oveq1d 6095	. . . . . . . . . . . . . . . 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 9723	. . . . . . . . . . . . . . . 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 2475	. . . . . . . . . . . . . . 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 6098	. . . . . . . . . . . . . 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 9400	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( Y - ( |_ ` Y ) ) x. E ) e. CC )
197	196, 57	negdid 9720	. . . . . . . . . . . . . 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 2468	. . . . . . . . . . . . 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 9763	. . . . . . . . . . . . 13 |- ( ph -> -u ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) e. RR )
200	198, 199	eqeltrd 2507	. . . . . . . . . . . 12 |- ( ph -> ( ( ( Y - ( |_ ` Y ) ) x. -u E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) -u C - -u [_ Y / x ]_ A ) ) e. RR )
201		nfcv 2569	. . . . . . . . . . . . . 14 |- F/_ x ( ( Y - ( |_ ` Y ) ) x. -u E )
202		nfcv 2569	. . . . . . . . . . . . . . 15 |- F/_ x sum_ k e. ( M ... ( |_ ` Y ) ) -u C
203	15	nfneg 9594	. . . . . . . . . . . . . . 15 |- F/_ x -u [_ Y / x ]_ A
204	202, 24, 203	nfov 6103	. . . . . . . . . . . . . 14 |- F/_ x ( sum_ k e. ( M ... ( |_ ` Y ) ) -u C - -u [_ Y / x ]_ A )
205	201, 164, 204	nfov 6103	. . . . . . . . . . . . 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 6098	. . . . . . . . . . . . . . 15 |- ( x = Y -> ( x - ( |_ ` x ) ) = ( Y - ( |_ ` Y ) ) )
208	69	negeqd 9592	. . . . . . . . . . . . . . 15 |- ( x = Y -> -u B = -u E )
209	207, 208	oveq12d 6098	. . . . . . . . . . . . . 14 |- ( x = Y -> ( ( x - ( |_ ` x ) ) x. -u B ) = ( ( Y - ( |_ ` Y ) ) x. -u E ) )
210	27	sumeq1d 13162	. . . . . . . . . . . . . . 15 |- ( x = Y -> sum_ k e. ( M ... ( |_ ` x ) ) -u C = sum_ k e. ( M ... ( |_ ` Y ) ) -u C )
211	17	negeqd 9592	. . . . . . . . . . . . . . 15 |- ( x = Y -> -u A = -u [_ Y / x ]_ A )
212	210, 211	oveq12d 6098	. . . . . . . . . . . . . 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 6098	. . . . . . . . . . . . 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 5778	. . . . . . . . . . . 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 654	. . . . . . . . . . 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 2465	. . . . . . . . . 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 463	. . . . . . . . . . 11 |- ( ( ph /\ x = Y ) -> -u B = -u E )
218	1, 217	csbied 3302	. . . . . . . . . 10 |- ( ph -> [_ Y / x ]_ -u B = -u E )
219	216, 218	oveq12d 6098	. . . . . . . . 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 4309	. . . . . . . 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 9400	. . . . . . . . 9 |- ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) + ( sum_ k e. ( M ... ( |_ ` X ) ) C - [_ X / x ]_ A ) ) e. CC )
222	221, 143	neg2subd 9724	. . . . . . . 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 9400	. . . . . . . . 9 |- ( ph -> ( ( ( Y - ( |_ ` Y ) ) x. E ) + ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) ) e. CC )
224	223, 185	neg2subd 9724	. . . . . . . 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 4309	. . . . . . 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 9723	. . . . . . 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 9723	. . . . . . 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 4310	. . . . . 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 9906	. . . . . 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 232	. . . . 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 9516	. . . 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 9389	. . . . . . . 8 |- ( ph -> 1 e. RR )
233		nfv 1672	. . . . . . . . . . 11 |- F/ x D <_ X
234		nfcv 2569	. . . . . . . . . . . 12 |- F/_ x 0
235		nfcv 2569	. . . . . . . . . . . 12 |- F/_ x <_
236	234, 235, 161	nfbr 4324	. . . . . . . . . . 11 |- F/ x 0 <_ [_ X / x ]_ B
237	233, 236	nfim 1851	. . . . . . . . . 10 |- F/ x ( D <_ X -> 0 <_ [_ X / x ]_ B )
238		breq2 4284	. . . . . . . . . . 11 |- ( x = X -> ( D <_ x <-> D <_ X ) )
239	171	breq2d 4292	. . . . . . . . . . 11 |- ( x = X -> ( 0 <_ B <-> 0 <_ [_ X / x ]_ B ) )
240	238, 239	imbi12d 320	. . . . . . . . . 10 |- ( x = X -> ( ( D <_ x -> 0 <_ B ) <-> ( D <_ X -> 0 <_ [_ X / x ]_ B ) ) )
241	237, 240	rspc 3056	. . . . . . . . 9 |- ( X e. S -> ( A. x e. S ( D <_ x -> 0 <_ B ) -> ( D <_ X -> 0 <_ [_ X / x ]_ B ) ) )
242	33, 103, 105, 241	syl3c 61	. . . . . . . 8 |- ( ph -> 0 <_ [_ X / x ]_ B )
243		fracle1 11637	. . . . . . . . 9 |- ( X e. RR -> ( X - ( |_ ` X ) ) <_ 1 )
244	74, 243	syl 16	. . . . . . . 8 |- ( ph -> ( X - ( |_ ` X ) ) <_ 1 )
245	77, 232, 88, 242, 244	lemul1ad 10260	. . . . . . 7 |- ( ph -> ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) <_ ( 1 x. [_ X / x ]_ B ) )
246	143	mulid2d 9392	. . . . . . 7 |- ( ph -> ( 1 x. [_ X / x ]_ B ) = [_ X / x ]_ B )
247	245, 246	breqtrd 4304	. . . . . 6 |- ( ph -> ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) <_ [_ X / x ]_ B )
248	89, 88, 45, 247	leadd1dd 9941	. . . . 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 9926	. . . . 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 232	. . . 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 9516	. . 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 9401	. . . 4 |- ( ph -> ( ( sum_ k e. ( M ... ( |_ ` Y ) ) C - [_ Y / x ]_ A ) + E ) e. RR )
253		fracge0 11638	. . . . . . 7 |- ( X e. RR -> 0 <_ ( X - ( |_ ` X ) ) )
254	74, 253	syl 16	. . . . . 6 |- ( ph -> 0 <_ ( X - ( |_ ` X ) ) )
255	77, 88, 254, 242	mulge0d 9904	. . . . 5 |- ( ph -> 0 <_ ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) )
256	45, 89	addge02d 9916	. . . . 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 210	. . . 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 456	. . . . . . 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 4309	. . . . . 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 9906	. . . . . 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 232	. . . . 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 11637	. . . . . . . . . 10 |- ( Y e. RR -> ( Y - ( |_ ` Y ) ) <_ 1 )
263	92, 262	syl 16	. . . . . . . . 9 |- ( ph -> ( Y - ( |_ ` Y ) ) <_ 1 )
264	95, 232, 72, 112, 263	lemul1ad 10260	. . . . . . . 8 |- ( ph -> ( ( Y - ( |_ ` Y ) ) x. E ) <_ ( 1 x. E ) )
265	185	mulid2d 9392	. . . . . . . 8 |- ( ph -> ( 1 x. E ) = E )
266	264, 265	breqtrd 4304	. . . . . . 7 |- ( ph -> ( ( Y - ( |_ ` Y ) ) x. E ) <_ E )
267	96, 72, 21, 266	leadd1dd 9941	. . . . . 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 9559	. . . . . 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 4304	. . . . 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 9516	. . . 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 9516	. . 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 12905	. . 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 906	. 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 4300	1 |- ( ph -> ( abs ` ( ( G ` Y ) - ( G ` X ) ) ) <_ E )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 958   = wceq 1362   e. wcel 1755   A.wral 2705   [_csb 3276   C_ wss 3316   {cpr 3867   class class class wbr 4280   e. cmpt 4338   ` cfv 5406  (class class class)co 6080   CCcc 9268   RRcr 9269   0cc0 9270   1c1 9271   + caddc 9273   x. cmul 9275   +oocpnf 9403   RR*cxr 9405   <_ cle 9407   - cmin 9583   -ucneg 9584   ZZcz 10634   ZZ>=cuz 10849   (,)cioo 11288   ...cfz 11424   |_cfl 11624   abscabs 12707   sum_csu 13147   _D cdv 21180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-rep 4391  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-inf2 7835  ax-cnex 9326  ax-resscn 9327  ax-1cn 9328  ax-icn 9329  ax-addcl 9330  ax-addrcl 9331  ax-mulcl 9332  ax-mulrcl 9333  ax-mulcom 9334  ax-addass 9335  ax-mulass 9336  ax-distr 9337  ax-i2m1 9338  ax-1ne0 9339  ax-1rid 9340  ax-rnegex 9341  ax-rrecex 9342  ax-cnre 9343  ax-pre-lttri 9344  ax-pre-lttrn 9345  ax-pre-ltadd 9346  ax-pre-mulgt0 9347  ax-pre-sup 9348  ax-addf 9349  ax-mulf 9350

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-fal 1368  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-int 4117  df-iun 4161  df-iin 4162  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-se 4667  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-isom 5415  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-of 6309  df-om 6466  df-1st 6566  df-2nd 6567  df-supp 6680  df-recs 6818  df-rdg 6852  df-1o 6908  df-2o 6909  df-oadd 6912  df-er 7089  df-map 7204  df-pm 7205  df-ixp 7252  df-en 7299  df-dom 7300  df-sdom 7301  df-fin 7302  df-fsupp 7609  df-fi 7649  df-sup 7679  df-oi 7712  df-card 8097  df-cda 8325  df-pnf 9408  df-mnf 9409  df-xr 9410  df-ltxr 9411  df-le 9412  df-sub 9585  df-neg 9586  df-div 9982  df-nn 10311  df-2 10368  df-3 10369  df-4 10370  df-5 10371  df-6 10372  df-7 10373  df-8 10374  df-9 10375  df-10 10376  df-n0 10568  df-z 10635  df-dec 10744  df-uz 10850  df-q 10942  df-rp 10980  df-xneg 11077  df-xadd 11078  df-xmul 11079  df-ioo 11292  df-ico 11294  df-icc 11295  df-fz 11425  df-fzo 11533  df-fl 11626  df-seq 11791  df-exp 11850  df-hash 12088  df-cj 12572  df-re 12573  df-im 12574  df-sqr 12708  df-abs 12709  df-clim 12950  df-sum 13148  df-struct 14159  df-ndx 14160  df-slot 14161  df-base 14162  df-sets 14163  df-ress 14164  df-plusg 14234  df-mulr 14235  df-starv 14236  df-sca 14237  df-vsca 14238  df-ip 14239  df-tset 14240  df-ple 14241  df-ds 14243  df-unif 14244  df-hom 14245  df-cco 14246  df-rest 14344  df-topn 14345  df-0g 14363  df-gsum 14364  df-topgen 14365  df-pt 14366  df-prds 14369  df-xrs 14423  df-qtop 14428  df-imas 14429  df-xps 14431  df-mre 14507  df-mrc 14508  df-acs 14510  df-mnd 15398  df-submnd 15448  df-mulg 15528  df-cntz 15815  df-cmn 16259  df-psmet 17653  df-xmet 17654  df-met 17655  df-bl 17656  df-mopn 17657  df-fbas 17658  df-fg 17659  df-cnfld 17663  df-top 18345  df-bases 18347  df-topon 18348  df-topsp 18349  df-cld 18465  df-ntr 18466  df-cls 18467  df-nei 18544  df-lp 18582  df-perf 18583  df-cn 18673  df-cnp 18674  df-haus 18761  df-cmp 18832  df-tx 18977  df-hmeo 19170  df-fil 19261  df-fm 19353  df-flim 19354  df-flf 19355  df-xms 19737  df-ms 19738  df-tms 19739  df-cncf 20296  df-limc 21183  df-dv 21184

This theorem is referenced by:  logfacbnd3  22447  log2sumbnd  22678