Theorem dvfsumlem2 19864

Description: Lemma for dvfsumrlim 19868. (Contributed by Mario Carneiro, 17-May-2016.)

Hypotheses

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

Assertion

Ref	Expression
dvfsumlem2	|- ( ph -> ( ( H ` Y ) <_ ( H ` X ) /\ ( ( H ` X ) - [_ X / x ]_ B ) <_ ( ( H ` Y ) - [_ Y / x ]_ B ) ) )

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

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

Proof of Theorem dvfsumlem2

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dvfsum.s	. . . . . . . . 9 |- S = ( T (,) +oo )
2		ioossre 10928	. . . . . . . . 9 |- ( T (,) +oo ) C_ RR
3	1, 2	eqsstri 3338	. . . . . . . 8 |- S C_ RR
4		dvfsumlem1.2	. . . . . . . 8 |- ( ph -> Y e. S )
5	3, 4	sseldi 3306	. . . . . . 7 |- ( ph -> Y e. RR )
6		dvfsumlem1.1	. . . . . . . . . . 11 |- ( ph -> X e. S )
7	6, 1	syl6eleq 2494	. . . . . . . . . 10 |- ( ph -> X e. ( T (,) +oo ) )
8		dvfsum.t	. . . . . . . . . . . 12 |- ( ph -> T e. RR )
9	8	rexrd 9090	. . . . . . . . . . 11 |- ( ph -> T e. RR* )
10		elioopnf 10954	. . . . . . . . . . 11 |- ( T e. RR* -> ( X e. ( T (,) +oo ) <-> ( X e. RR /\ T < X ) ) )
11	9, 10	syl 16	. . . . . . . . . 10 |- ( ph -> ( X e. ( T (,) +oo ) <-> ( X e. RR /\ T < X ) ) )
12	7, 11	mpbid 202	. . . . . . . . 9 |- ( ph -> ( X e. RR /\ T < X ) )
13	12	simpld 446	. . . . . . . 8 |- ( ph -> X e. RR )
14		reflcl 11160	. . . . . . . 8 |- ( X e. RR -> ( |_ ` X ) e. RR )
15	13, 14	syl 16	. . . . . . 7 |- ( ph -> ( |_ ` X ) e. RR )
16	5, 15	resubcld 9421	. . . . . 6 |- ( ph -> ( Y - ( |_ ` X ) ) e. RR )
17	13	rexrd 9090	. . . . . . . 8 |- ( ph -> X e. RR* )
18	5	rexrd 9090	. . . . . . . 8 |- ( ph -> Y e. RR* )
19		dvfsumlem1.4	. . . . . . . 8 |- ( ph -> X <_ Y )
20		ubicc2 10970	. . . . . . . 8 |- ( ( X e. RR* /\ Y e. RR* /\ X <_ Y ) -> Y e. ( X [,] Y ) )
21	17, 18, 19, 20	syl3anc 1184	. . . . . . 7 |- ( ph -> Y e. ( X [,] Y ) )
22		pnfxr 10669	. . . . . . . . . . . . 13 |- +oo e. RR*
23	22	a1i 11	. . . . . . . . . . . 12 |- ( ph -> +oo e. RR* )
24	12	simprd 450	. . . . . . . . . . . 12 |- ( ph -> T < X )
25		ltpnf 10677	. . . . . . . . . . . . 13 |- ( Y e. RR -> Y < +oo )
26	5, 25	syl 16	. . . . . . . . . . . 12 |- ( ph -> Y < +oo )
27		iccssioo 10935	. . . . . . . . . . . 12 |- ( ( ( T e. RR* /\ +oo e. RR* ) /\ ( T < X /\ Y < +oo ) ) -> ( X [,] Y ) C_ ( T (,) +oo ) )
28	9, 23, 24, 26, 27	syl22anc 1185	. . . . . . . . . . 11 |- ( ph -> ( X [,] Y ) C_ ( T (,) +oo ) )
29	28, 1	syl6sseqr 3355	. . . . . . . . . 10 |- ( ph -> ( X [,] Y ) C_ S )
30	29	sselda 3308	. . . . . . . . 9 |- ( ( ph /\ y e. ( X [,] Y ) ) -> y e. S )
31	3	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> S C_ RR )
32		dvfsum.a	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. S ) -> A e. RR )
33		dvfsum.b1	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. S ) -> B e. V )
34		dvfsum.b3	. . . . . . . . . . . . 13 |- ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )
35	31, 32, 33, 34	dvmptrecl 19861	. . . . . . . . . . . 12 |- ( ( ph /\ x e. S ) -> B e. RR )
36		eqid 2404	. . . . . . . . . . . 12 |- ( x e. S |-> B ) = ( x e. S |-> B )
37	35, 36	fmptd 5852	. . . . . . . . . . 11 |- ( ph -> ( x e. S |-> B ) : S --> RR )
38		nfcv 2540	. . . . . . . . . . . . 13 |- F/_ y B
39		nfcsb1v 3243	. . . . . . . . . . . . 13 |- F/_ x [_ y / x ]_ B
40		csbeq1a 3219	. . . . . . . . . . . . 13 |- ( x = y -> B = [_ y / x ]_ B )
41	38, 39, 40	cbvmpt 4259	. . . . . . . . . . . 12 |- ( x e. S |-> B ) = ( y e. S |-> [_ y / x ]_ B )
42	41	fmpt 5849	. . . . . . . . . . 11 |- ( A. y e. S [_ y / x ]_ B e. RR <-> ( x e. S |-> B ) : S --> RR )
43	37, 42	sylibr 204	. . . . . . . . . 10 |- ( ph -> A. y e. S [_ y / x ]_ B e. RR )
44	43	r19.21bi 2764	. . . . . . . . 9 |- ( ( ph /\ y e. S ) -> [_ y / x ]_ B e. RR )
45	30, 44	syldan 457	. . . . . . . 8 |- ( ( ph /\ y e. ( X [,] Y ) ) -> [_ y / x ]_ B e. RR )
46	45	ralrimiva 2749	. . . . . . 7 |- ( ph -> A. y e. ( X [,] Y ) [_ y / x ]_ B e. RR )
47		csbeq1 3214	. . . . . . . . 9 |- ( y = Y -> [_ y / x ]_ B = [_ Y / x ]_ B )
48	47	eleq1d 2470	. . . . . . . 8 |- ( y = Y -> ( [_ y / x ]_ B e. RR <-> [_ Y / x ]_ B e. RR ) )
49	48	rspcv 3008	. . . . . . 7 |- ( Y e. ( X [,] Y ) -> ( A. y e. ( X [,] Y ) [_ y / x ]_ B e. RR -> [_ Y / x ]_ B e. RR ) )
50	21, 46, 49	sylc 58	. . . . . 6 |- ( ph -> [_ Y / x ]_ B e. RR )
51	16, 50	remulcld 9072	. . . . 5 |- ( ph -> ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) e. RR )
52		eqid 2404	. . . . . . . . . . 11 |- ( x e. S |-> A ) = ( x e. S |-> A )
53	32, 52	fmptd 5852	. . . . . . . . . 10 |- ( ph -> ( x e. S |-> A ) : S --> RR )
54		nfcv 2540	. . . . . . . . . . . 12 |- F/_ y A
55		nfcsb1v 3243	. . . . . . . . . . . 12 |- F/_ x [_ y / x ]_ A
56		csbeq1a 3219	. . . . . . . . . . . 12 |- ( x = y -> A = [_ y / x ]_ A )
57	54, 55, 56	cbvmpt 4259	. . . . . . . . . . 11 |- ( x e. S |-> A ) = ( y e. S |-> [_ y / x ]_ A )
58	57	fmpt 5849	. . . . . . . . . 10 |- ( A. y e. S [_ y / x ]_ A e. RR <-> ( x e. S |-> A ) : S --> RR )
59	53, 58	sylibr 204	. . . . . . . . 9 |- ( ph -> A. y e. S [_ y / x ]_ A e. RR )
60	59	r19.21bi 2764	. . . . . . . 8 |- ( ( ph /\ y e. S ) -> [_ y / x ]_ A e. RR )
61	30, 60	syldan 457	. . . . . . 7 |- ( ( ph /\ y e. ( X [,] Y ) ) -> [_ y / x ]_ A e. RR )
62	61	ralrimiva 2749	. . . . . 6 |- ( ph -> A. y e. ( X [,] Y ) [_ y / x ]_ A e. RR )
63		csbeq1 3214	. . . . . . . 8 |- ( y = Y -> [_ y / x ]_ A = [_ Y / x ]_ A )
64	63	eleq1d 2470	. . . . . . 7 |- ( y = Y -> ( [_ y / x ]_ A e. RR <-> [_ Y / x ]_ A e. RR ) )
65	64	rspcv 3008	. . . . . 6 |- ( Y e. ( X [,] Y ) -> ( A. y e. ( X [,] Y ) [_ y / x ]_ A e. RR -> [_ Y / x ]_ A e. RR ) )
66	21, 62, 65	sylc 58	. . . . 5 |- ( ph -> [_ Y / x ]_ A e. RR )
67	51, 66	resubcld 9421	. . . 4 |- ( ph -> ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) e. RR )
68	13, 15	resubcld 9421	. . . . . 6 |- ( ph -> ( X - ( |_ ` X ) ) e. RR )
69		lbicc2 10969	. . . . . . . 8 |- ( ( X e. RR* /\ Y e. RR* /\ X <_ Y ) -> X e. ( X [,] Y ) )
70	17, 18, 19, 69	syl3anc 1184	. . . . . . 7 |- ( ph -> X e. ( X [,] Y ) )
71		csbeq1 3214	. . . . . . . . 9 |- ( y = X -> [_ y / x ]_ B = [_ X / x ]_ B )
72	71	eleq1d 2470	. . . . . . . 8 |- ( y = X -> ( [_ y / x ]_ B e. RR <-> [_ X / x ]_ B e. RR ) )
73	72	rspcv 3008	. . . . . . 7 |- ( X e. ( X [,] Y ) -> ( A. y e. ( X [,] Y ) [_ y / x ]_ B e. RR -> [_ X / x ]_ B e. RR ) )
74	70, 46, 73	sylc 58	. . . . . 6 |- ( ph -> [_ X / x ]_ B e. RR )
75	68, 74	remulcld 9072	. . . . 5 |- ( ph -> ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) e. RR )
76		csbeq1 3214	. . . . . . . 8 |- ( y = X -> [_ y / x ]_ A = [_ X / x ]_ A )
77	76	eleq1d 2470	. . . . . . 7 |- ( y = X -> ( [_ y / x ]_ A e. RR <-> [_ X / x ]_ A e. RR ) )
78	77	rspcv 3008	. . . . . 6 |- ( X e. ( X [,] Y ) -> ( A. y e. ( X [,] Y ) [_ y / x ]_ A e. RR -> [_ X / x ]_ A e. RR ) )
79	70, 62, 78	sylc 58	. . . . 5 |- ( ph -> [_ X / x ]_ A e. RR )
80	75, 79	resubcld 9421	. . . 4 |- ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) e. RR )
81		fzfid 11267	. . . . 5 |- ( ph -> ( M ... ( |_ ` X ) ) e. Fin )
82		dvfsum.b2	. . . . . . 7 |- ( ( ph /\ x e. Z ) -> B e. RR )
83	82	ralrimiva 2749	. . . . . 6 |- ( ph -> A. x e. Z B e. RR )
84		elfzuz 11011	. . . . . . 7 |- ( k e. ( M ... ( |_ ` X ) ) -> k e. ( ZZ>= ` M ) )
85		dvfsum.z	. . . . . . 7 |- Z = ( ZZ>= ` M )
86	84, 85	syl6eleqr 2495	. . . . . 6 |- ( k e. ( M ... ( |_ ` X ) ) -> k e. Z )
87		dvfsum.c	. . . . . . . 8 |- ( x = k -> B = C )
88	87	eleq1d 2470	. . . . . . 7 |- ( x = k -> ( B e. RR <-> C e. RR ) )
89	88	rspccva 3011	. . . . . 6 |- ( ( A. x e. Z B e. RR /\ k e. Z ) -> C e. RR )
90	83, 86, 89	syl2an 464	. . . . 5 |- ( ( ph /\ k e. ( M ... ( |_ ` X ) ) ) -> C e. RR )
91	81, 90	fsumrecl 12483	. . . 4 |- ( ph -> sum_ k e. ( M ... ( |_ ` X ) ) C e. RR )
92	68, 50	remulcld 9072	. . . . . 6 |- ( ph -> ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) e. RR )
93	92, 79	resubcld 9421	. . . . 5 |- ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ X / x ]_ A ) e. RR )
94	5, 13	resubcld 9421	. . . . . . . . 9 |- ( ph -> ( Y - X ) e. RR )
95	50, 94	remulcld 9072	. . . . . . . 8 |- ( ph -> ( [_ Y / x ]_ B x. ( Y - X ) ) e. RR )
96	50	recnd 9070	. . . . . . . . . 10 |- ( ph -> [_ Y / x ]_ B e. CC )
97	5	recnd 9070	. . . . . . . . . 10 |- ( ph -> Y e. CC )
98	13	recnd 9070	. . . . . . . . . 10 |- ( ph -> X e. CC )
99	96, 97, 98	subdid 9445	. . . . . . . . 9 |- ( ph -> ( [_ Y / x ]_ B x. ( Y - X ) ) = ( ( [_ Y / x ]_ B x. Y ) - ( [_ Y / x ]_ B x. X ) ) )
100		eqid 2404	. . . . . . . . . . 11 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
101	100	mulcn 18850	. . . . . . . . . . 11 |- x. e. ( ( ( TopOpen ` ℂfld ) tX ( TopOpen ` ℂfld ) ) Cn ( TopOpen ` ℂfld ) )
102	28, 2	syl6ss 3320	. . . . . . . . . . . . 13 |- ( ph -> ( X [,] Y ) C_ RR )
103		ax-resscn 9003	. . . . . . . . . . . . 13 |- RR C_ CC
104	102, 103	syl6ss 3320	. . . . . . . . . . . 12 |- ( ph -> ( X [,] Y ) C_ CC )
105	103	a1i 11	. . . . . . . . . . . 12 |- ( ph -> RR C_ CC )
106		cncfmptc 18894	. . . . . . . . . . . 12 |- ( ( [_ Y / x ]_ B e. RR /\ ( X [,] Y ) C_ CC /\ RR C_ CC ) -> ( y e. ( X [,] Y ) |-> [_ Y / x ]_ B ) e. ( ( X [,] Y ) -cn-> RR ) )
107	50, 104, 105, 106	syl3anc 1184	. . . . . . . . . . 11 |- ( ph -> ( y e. ( X [,] Y ) |-> [_ Y / x ]_ B ) e. ( ( X [,] Y ) -cn-> RR ) )
108		cncfmptid 18895	. . . . . . . . . . . 12 |- ( ( ( X [,] Y ) C_ RR /\ RR C_ CC ) -> ( y e. ( X [,] Y ) |-> y ) e. ( ( X [,] Y ) -cn-> RR ) )
109	102, 103, 108	sylancl 644	. . . . . . . . . . 11 |- ( ph -> ( y e. ( X [,] Y ) |-> y ) e. ( ( X [,] Y ) -cn-> RR ) )
110		remulcl 9031	. . . . . . . . . . 11 |- ( ( [_ Y / x ]_ B e. RR /\ y e. RR ) -> ( [_ Y / x ]_ B x. y ) e. RR )
111	100, 101, 107, 109, 103, 110	cncfmpt2ss 18898	. . . . . . . . . 10 |- ( ph -> ( y e. ( X [,] Y ) |-> ( [_ Y / x ]_ B x. y ) ) e. ( ( X [,] Y ) -cn-> RR ) )
112		reex 9037	. . . . . . . . . . . . . 14 |- RR e. _V
113	112	prid1 3872	. . . . . . . . . . . . 13 |- RR e. { RR , CC }
114	113	a1i 11	. . . . . . . . . . . 12 |- ( ph -> RR e. { RR , CC } )
115		ioossicc 10952	. . . . . . . . . . . . . . 15 |- ( X (,) Y ) C_ ( X [,] Y )
116	115, 102	syl5ss 3319	. . . . . . . . . . . . . 14 |- ( ph -> ( X (,) Y ) C_ RR )
117	116	sselda 3308	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( X (,) Y ) ) -> y e. RR )
118	117	recnd 9070	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( X (,) Y ) ) -> y e. CC )
119		ax-1cn 9004	. . . . . . . . . . . . 13 |- 1 e. CC
120	119	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( X (,) Y ) ) -> 1 e. CC )
121		simpr 448	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. RR ) -> y e. RR )
122	121	recnd 9070	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. RR ) -> y e. CC )
123	119	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. RR ) -> 1 e. CC )
124	114	dvmptid 19796	. . . . . . . . . . . . 13 |- ( ph -> ( RR _D ( y e. RR |-> y ) ) = ( y e. RR |-> 1 ) )
125	100	tgioo2 18787	. . . . . . . . . . . . 13 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
126		iooretop 18753	. . . . . . . . . . . . . 14 |- ( X (,) Y ) e. ( topGen ` ran (,) )
127	126	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> ( X (,) Y ) e. ( topGen ` ran (,) ) )
128	114, 122, 123, 124, 116, 125, 100, 127	dvmptres 19802	. . . . . . . . . . . 12 |- ( ph -> ( RR _D ( y e. ( X (,) Y ) |-> y ) ) = ( y e. ( X (,) Y ) |-> 1 ) )
129	114, 118, 120, 128, 96	dvmptcmul 19803	. . . . . . . . . . 11 |- ( ph -> ( RR _D ( y e. ( X (,) Y ) |-> ( [_ Y / x ]_ B x. y ) ) ) = ( y e. ( X (,) Y ) |-> ( [_ Y / x ]_ B x. 1 ) ) )
130	96	mulid1d 9061	. . . . . . . . . . . 12 |- ( ph -> ( [_ Y / x ]_ B x. 1 ) = [_ Y / x ]_ B )
131	130	mpteq2dv 4256	. . . . . . . . . . 11 |- ( ph -> ( y e. ( X (,) Y ) |-> ( [_ Y / x ]_ B x. 1 ) ) = ( y e. ( X (,) Y ) |-> [_ Y / x ]_ B ) )
132	129, 131	eqtrd 2436	. . . . . . . . . 10 |- ( ph -> ( RR _D ( y e. ( X (,) Y ) |-> ( [_ Y / x ]_ B x. y ) ) ) = ( y e. ( X (,) Y ) |-> [_ Y / x ]_ B ) )
133		resmpt 5150	. . . . . . . . . . . 12 |- ( ( X [,] Y ) C_ S -> ( ( y e. S |-> [_ y / x ]_ A ) |` ( X [,] Y ) ) = ( y e. ( X [,] Y ) |-> [_ y / x ]_ A ) )
134	29, 133	syl 16	. . . . . . . . . . 11 |- ( ph -> ( ( y e. S |-> [_ y / x ]_ A ) |` ( X [,] Y ) ) = ( y e. ( X [,] Y ) |-> [_ y / x ]_ A ) )
135	32	recnd 9070	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. S ) -> A e. CC )
136	135, 52	fmptd 5852	. . . . . . . . . . . . . . . 16 |- ( ph -> ( x e. S |-> A ) : S --> CC )
137	34	dmeqd 5031	. . . . . . . . . . . . . . . . 17 |- ( ph -> dom ( RR _D ( x e. S |-> A ) ) = dom ( x e. S |-> B ) )
138	33	ralrimiva 2749	. . . . . . . . . . . . . . . . . 18 |- ( ph -> A. x e. S B e. V )
139		dmmptg 5326	. . . . . . . . . . . . . . . . . 18 |- ( A. x e. S B e. V -> dom ( x e. S |-> B ) = S )
140	138, 139	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> dom ( x e. S |-> B ) = S )
141	137, 140	eqtrd 2436	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( RR _D ( x e. S |-> A ) ) = S )
142		dvcn 19760	. . . . . . . . . . . . . . . 16 |- ( ( ( RR C_ CC /\ ( x e. S |-> A ) : S --> CC /\ S C_ RR ) /\ dom ( RR _D ( x e. S |-> A ) ) = S ) -> ( x e. S |-> A ) e. ( S -cn-> CC ) )
143	105, 136, 31, 141, 142	syl31anc 1187	. . . . . . . . . . . . . . 15 |- ( ph -> ( x e. S |-> A ) e. ( S -cn-> CC ) )
144		cncffvrn 18881	. . . . . . . . . . . . . . 15 |- ( ( RR C_ CC /\ ( x e. S |-> A ) e. ( S -cn-> CC ) ) -> ( ( x e. S |-> A ) e. ( S -cn-> RR ) <-> ( x e. S |-> A ) : S --> RR ) )
145	103, 143, 144	sylancr 645	. . . . . . . . . . . . . 14 |- ( ph -> ( ( x e. S |-> A ) e. ( S -cn-> RR ) <-> ( x e. S |-> A ) : S --> RR ) )
146	53, 145	mpbird 224	. . . . . . . . . . . . 13 |- ( ph -> ( x e. S |-> A ) e. ( S -cn-> RR ) )
147	57, 146	syl5eqelr 2489	. . . . . . . . . . . 12 |- ( ph -> ( y e. S |-> [_ y / x ]_ A ) e. ( S -cn-> RR ) )
148		rescncf 18880	. . . . . . . . . . . 12 |- ( ( X [,] Y ) C_ S -> ( ( y e. S |-> [_ y / x ]_ A ) e. ( S -cn-> RR ) -> ( ( y e. S |-> [_ y / x ]_ A ) |` ( X [,] Y ) ) e. ( ( X [,] Y ) -cn-> RR ) ) )
149	29, 147, 148	sylc 58	. . . . . . . . . . 11 |- ( ph -> ( ( y e. S |-> [_ y / x ]_ A ) |` ( X [,] Y ) ) e. ( ( X [,] Y ) -cn-> RR ) )
150	134, 149	eqeltrrd 2479	. . . . . . . . . 10 |- ( ph -> ( y e. ( X [,] Y ) |-> [_ y / x ]_ A ) e. ( ( X [,] Y ) -cn-> RR ) )
151	60	recnd 9070	. . . . . . . . . . 11 |- ( ( ph /\ y e. S ) -> [_ y / x ]_ A e. CC )
152	57	oveq2i 6051	. . . . . . . . . . . 12 |- ( RR _D ( x e. S |-> A ) ) = ( RR _D ( y e. S |-> [_ y / x ]_ A ) )
153	34, 152, 41	3eqtr3g 2459	. . . . . . . . . . 11 |- ( ph -> ( RR _D ( y e. S |-> [_ y / x ]_ A ) ) = ( y e. S |-> [_ y / x ]_ B ) )
154	115, 29	syl5ss 3319	. . . . . . . . . . 11 |- ( ph -> ( X (,) Y ) C_ S )
155	114, 151, 44, 153, 154, 125, 100, 127	dvmptres 19802	. . . . . . . . . 10 |- ( ph -> ( RR _D ( y e. ( X (,) Y ) |-> [_ y / x ]_ A ) ) = ( y e. ( X (,) Y ) |-> [_ y / x ]_ B ) )
156	115	sseli 3304	. . . . . . . . . . 11 |- ( y e. ( X (,) Y ) -> y e. ( X [,] Y ) )
157		simpl 444	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( X [,] Y ) ) -> ph )
158	4	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( X [,] Y ) ) -> Y e. S )
159		dvfsum.d	. . . . . . . . . . . . . 14 |- ( ph -> D e. RR )
160	159	adantr 452	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( X [,] Y ) ) -> D e. RR )
161	13	adantr 452	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( X [,] Y ) ) -> X e. RR )
162		elicc2 10931	. . . . . . . . . . . . . . . 16 |- ( ( X e. RR /\ Y e. RR ) -> ( y e. ( X [,] Y ) <-> ( y e. RR /\ X <_ y /\ y <_ Y ) ) )
163	13, 5, 162	syl2anc 643	. . . . . . . . . . . . . . 15 |- ( ph -> ( y e. ( X [,] Y ) <-> ( y e. RR /\ X <_ y /\ y <_ Y ) ) )
164	163	biimpa 471	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( X [,] Y ) ) -> ( y e. RR /\ X <_ y /\ y <_ Y ) )
165	164	simp1d 969	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( X [,] Y ) ) -> y e. RR )
166		dvfsumlem1.3	. . . . . . . . . . . . . 14 |- ( ph -> D <_ X )
167	166	adantr 452	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( X [,] Y ) ) -> D <_ X )
168	164	simp2d 970	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( X [,] Y ) ) -> X <_ y )
169	160, 161, 165, 167, 168	letrd 9183	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( X [,] Y ) ) -> D <_ y )
170	164	simp3d 971	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( X [,] Y ) ) -> y <_ Y )
171		dvfsumlem1.5	. . . . . . . . . . . . 13 |- ( ph -> Y <_ U )
172	171	adantr 452	. . . . . . . . . . . 12 |- ( ( ph /\ y e. ( X [,] Y ) ) -> Y <_ U )
173		simp2r 984	. . . . . . . . . . . . 13 |- ( ( ph /\ ( y e. S /\ Y e. S ) /\ ( D <_ y /\ y <_ Y /\ Y <_ U ) ) -> Y e. S )
174		eleq1 2464	. . . . . . . . . . . . . . . . 17 |- ( k = Y -> ( k e. S <-> Y e. S ) )
175	174	anbi2d 685	. . . . . . . . . . . . . . . 16 |- ( k = Y -> ( ( y e. S /\ k e. S ) <-> ( y e. S /\ Y e. S ) ) )
176		breq2 4176	. . . . . . . . . . . . . . . . 17 |- ( k = Y -> ( y <_ k <-> y <_ Y ) )
177		breq1 4175	. . . . . . . . . . . . . . . . 17 |- ( k = Y -> ( k <_ U <-> Y <_ U ) )
178	176, 177	3anbi23d 1257	. . . . . . . . . . . . . . . 16 |- ( k = Y -> ( ( D <_ y /\ y <_ k /\ k <_ U ) <-> ( D <_ y /\ y <_ Y /\ Y <_ U ) ) )
179	175, 178	3anbi23d 1257	. . . . . . . . . . . . . . 15 |- ( k = Y -> ( ( ph /\ ( y e. S /\ k e. S ) /\ ( D <_ y /\ y <_ k /\ k <_ U ) ) <-> ( ph /\ ( y e. S /\ Y e. S ) /\ ( D <_ y /\ y <_ Y /\ Y <_ U ) ) ) )
180		vex 2919	. . . . . . . . . . . . . . . . . 18 |- k e. _V
181		nfcv 2540	. . . . . . . . . . . . . . . . . 18 |- F/_ x C
182	180, 181, 87	csbief 3252	. . . . . . . . . . . . . . . . 17 |- [_ k / x ]_ B = C
183		csbeq1 3214	. . . . . . . . . . . . . . . . 17 |- ( k = Y -> [_ k / x ]_ B = [_ Y / x ]_ B )
184	182, 183	syl5eqr 2450	. . . . . . . . . . . . . . . 16 |- ( k = Y -> C = [_ Y / x ]_ B )
185	184	breq1d 4182	. . . . . . . . . . . . . . 15 |- ( k = Y -> ( C <_ [_ y / x ]_ B <-> [_ Y / x ]_ B <_ [_ y / x ]_ B ) )
186	179, 185	imbi12d 312	. . . . . . . . . . . . . 14 |- ( k = Y -> ( ( ( ph /\ ( y e. S /\ k e. S ) /\ ( D <_ y /\ y <_ k /\ k <_ U ) ) -> C <_ [_ y / x ]_ B ) <-> ( ( ph /\ ( y e. S /\ Y e. S ) /\ ( D <_ y /\ y <_ Y /\ Y <_ U ) ) -> [_ Y / x ]_ B <_ [_ y / x ]_ B ) ) )
187		nfv 1626	. . . . . . . . . . . . . . . 16 |- F/ x ( ph /\ ( y e. S /\ k e. S ) /\ ( D <_ y /\ y <_ k /\ k <_ U ) )
188		nfcv 2540	. . . . . . . . . . . . . . . . 17 |- F/_ x <_
189	181, 188, 39	nfbr 4216	. . . . . . . . . . . . . . . 16 |- F/ x C <_ [_ y / x ]_ B
190	187, 189	nfim 1828	. . . . . . . . . . . . . . 15 |- F/ x ( ( ph /\ ( y e. S /\ k e. S ) /\ ( D <_ y /\ y <_ k /\ k <_ U ) ) -> C <_ [_ y / x ]_ B )
191		eleq1 2464	. . . . . . . . . . . . . . . . . 18 |- ( x = y -> ( x e. S <-> y e. S ) )
192	191	anbi1d 686	. . . . . . . . . . . . . . . . 17 |- ( x = y -> ( ( x e. S /\ k e. S ) <-> ( y e. S /\ k e. S ) ) )
193		breq2 4176	. . . . . . . . . . . . . . . . . 18 |- ( x = y -> ( D <_ x <-> D <_ y ) )
194		breq1 4175	. . . . . . . . . . . . . . . . . 18 |- ( x = y -> ( x <_ k <-> y <_ k ) )
195	193, 194	3anbi12d 1255	. . . . . . . . . . . . . . . . 17 |- ( x = y -> ( ( D <_ x /\ x <_ k /\ k <_ U ) <-> ( D <_ y /\ y <_ k /\ k <_ U ) ) )
196	192, 195	3anbi23d 1257	. . . . . . . . . . . . . . . 16 |- ( x = y -> ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) <-> ( ph /\ ( y e. S /\ k e. S ) /\ ( D <_ y /\ y <_ k /\ k <_ U ) ) ) )
197	40	breq2d 4184	. . . . . . . . . . . . . . . 16 |- ( x = y -> ( C <_ B <-> C <_ [_ y / x ]_ B ) )
198	196, 197	imbi12d 312	. . . . . . . . . . . . . . 15 |- ( x = y -> ( ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> C <_ B ) <-> ( ( ph /\ ( y e. S /\ k e. S ) /\ ( D <_ y /\ y <_ k /\ k <_ U ) ) -> C <_ [_ y / x ]_ B ) ) )
199		dvfsum.l	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> C <_ B )
200	190, 198, 199	chvar 2039	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( y e. S /\ k e. S ) /\ ( D <_ y /\ y <_ k /\ k <_ U ) ) -> C <_ [_ y / x ]_ B )
201	186, 200	vtoclg 2971	. . . . . . . . . . . . 13 |- ( Y e. S -> ( ( ph /\ ( y e. S /\ Y e. S ) /\ ( D <_ y /\ y <_ Y /\ Y <_ U ) ) -> [_ Y / x ]_ B <_ [_ y / x ]_ B ) )
202	173, 201	mpcom 34	. . . . . . . . . . . 12 |- ( ( ph /\ ( y e. S /\ Y e. S ) /\ ( D <_ y /\ y <_ Y /\ Y <_ U ) ) -> [_ Y / x ]_ B <_ [_ y / x ]_ B )
203	157, 30, 158, 169, 170, 172, 202	syl123anc 1201	. . . . . . . . . . 11 |- ( ( ph /\ y e. ( X [,] Y ) ) -> [_ Y / x ]_ B <_ [_ y / x ]_ B )
204	156, 203	sylan2 461	. . . . . . . . . 10 |- ( ( ph /\ y e. ( X (,) Y ) ) -> [_ Y / x ]_ B <_ [_ y / x ]_ B )
205		oveq2 6048	. . . . . . . . . 10 |- ( y = X -> ( [_ Y / x ]_ B x. y ) = ( [_ Y / x ]_ B x. X ) )
206		oveq2 6048	. . . . . . . . . 10 |- ( y = Y -> ( [_ Y / x ]_ B x. y ) = ( [_ Y / x ]_ B x. Y ) )
207	13, 5, 111, 132, 150, 155, 204, 70, 21, 19, 205, 76, 206, 63	dvle 19844	. . . . . . . . 9 |- ( ph -> ( ( [_ Y / x ]_ B x. Y ) - ( [_ Y / x ]_ B x. X ) ) <_ ( [_ Y / x ]_ A - [_ X / x ]_ A ) )
208	99, 207	eqbrtrd 4192	. . . . . . . 8 |- ( ph -> ( [_ Y / x ]_ B x. ( Y - X ) ) <_ ( [_ Y / x ]_ A - [_ X / x ]_ A ) )
209	95, 66, 79, 208	lesubd 9586	. . . . . . 7 |- ( ph -> [_ X / x ]_ A <_ ( [_ Y / x ]_ A - ( [_ Y / x ]_ B x. ( Y - X ) ) ) )
210	92	recnd 9070	. . . . . . . . 9 |- ( ph -> ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) e. CC )
211	51	recnd 9070	. . . . . . . . 9 |- ( ph -> ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) e. CC )
212	66	recnd 9070	. . . . . . . . 9 |- ( ph -> [_ Y / x ]_ A e. CC )
213	210, 211, 212	subsubd 9395	. . . . . . . 8 |- ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) ) = ( ( ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) ) + [_ Y / x ]_ A ) )
214	211, 210	negsubdi2d 9383	. . . . . . . . . . 11 |- ( ph -> -u ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) ) = ( ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) ) )
215	15	recnd 9070	. . . . . . . . . . . . . . 15 |- ( ph -> ( |_ ` X ) e. CC )
216	97, 98, 215	nnncan2d 9402	. . . . . . . . . . . . . 14 |- ( ph -> ( ( Y - ( |_ ` X ) ) - ( X - ( |_ ` X ) ) ) = ( Y - X ) )
217	216	oveq1d 6055	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( Y - ( |_ ` X ) ) - ( X - ( |_ ` X ) ) ) x. [_ Y / x ]_ B ) = ( ( Y - X ) x. [_ Y / x ]_ B ) )
218	16	recnd 9070	. . . . . . . . . . . . . 14 |- ( ph -> ( Y - ( |_ ` X ) ) e. CC )
219	68	recnd 9070	. . . . . . . . . . . . . 14 |- ( ph -> ( X - ( |_ ` X ) ) e. CC )
220	218, 219, 96	subdird 9446	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( Y - ( |_ ` X ) ) - ( X - ( |_ ` X ) ) ) x. [_ Y / x ]_ B ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) ) )
221	94	recnd 9070	. . . . . . . . . . . . . 14 |- ( ph -> ( Y - X ) e. CC )
222	221, 96	mulcomd 9065	. . . . . . . . . . . . 13 |- ( ph -> ( ( Y - X ) x. [_ Y / x ]_ B ) = ( [_ Y / x ]_ B x. ( Y - X ) ) )
223	217, 220, 222	3eqtr3d 2444	. . . . . . . . . . . 12 |- ( ph -> ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) ) = ( [_ Y / x ]_ B x. ( Y - X ) ) )
224	223	negeqd 9256	. . . . . . . . . . 11 |- ( ph -> -u ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) ) = -u ( [_ Y / x ]_ B x. ( Y - X ) ) )
225	214, 224	eqtr3d 2438	. . . . . . . . . 10 |- ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) ) = -u ( [_ Y / x ]_ B x. ( Y - X ) ) )
226	225	oveq1d 6055	. . . . . . . . 9 |- ( ph -> ( ( ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) ) + [_ Y / x ]_ A ) = ( -u ( [_ Y / x ]_ B x. ( Y - X ) ) + [_ Y / x ]_ A ) )
227	95	recnd 9070	. . . . . . . . . 10 |- ( ph -> ( [_ Y / x ]_ B x. ( Y - X ) ) e. CC )
228	227, 212	negsubdid 9382	. . . . . . . . 9 |- ( ph -> -u ( ( [_ Y / x ]_ B x. ( Y - X ) ) - [_ Y / x ]_ A ) = ( -u ( [_ Y / x ]_ B x. ( Y - X ) ) + [_ Y / x ]_ A ) )
229	226, 228	eqtr4d 2439	. . . . . . . 8 |- ( ph -> ( ( ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) ) + [_ Y / x ]_ A ) = -u ( ( [_ Y / x ]_ B x. ( Y - X ) ) - [_ Y / x ]_ A ) )
230	227, 212	negsubdi2d 9383	. . . . . . . 8 |- ( ph -> -u ( ( [_ Y / x ]_ B x. ( Y - X ) ) - [_ Y / x ]_ A ) = ( [_ Y / x ]_ A - ( [_ Y / x ]_ B x. ( Y - X ) ) ) )
231	213, 229, 230	3eqtrd 2440	. . . . . . 7 |- ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) ) = ( [_ Y / x ]_ A - ( [_ Y / x ]_ B x. ( Y - X ) ) ) )
232	209, 231	breqtrrd 4198	. . . . . 6 |- ( ph -> [_ X / x ]_ A <_ ( ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) ) )
233	79, 92, 67, 232	lesubd 9586	. . . . 5 |- ( ph -> ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) <_ ( ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ X / x ]_ A ) )
234		flle 11163	. . . . . . . . 9 |- ( X e. RR -> ( |_ ` X ) <_ X )
235	13, 234	syl 16	. . . . . . . 8 |- ( ph -> ( |_ ` X ) <_ X )
236	13, 15	subge0d 9572	. . . . . . . 8 |- ( ph -> ( 0 <_ ( X - ( |_ ` X ) ) <-> ( |_ ` X ) <_ X ) )
237	235, 236	mpbird 224	. . . . . . 7 |- ( ph -> 0 <_ ( X - ( |_ ` X ) ) )
238	203	ralrimiva 2749	. . . . . . . 8 |- ( ph -> A. y e. ( X [,] Y ) [_ Y / x ]_ B <_ [_ y / x ]_ B )
239	71	breq2d 4184	. . . . . . . . 9 |- ( y = X -> ( [_ Y / x ]_ B <_ [_ y / x ]_ B <-> [_ Y / x ]_ B <_ [_ X / x ]_ B ) )
240	239	rspcv 3008	. . . . . . . 8 |- ( X e. ( X [,] Y ) -> ( A. y e. ( X [,] Y ) [_ Y / x ]_ B <_ [_ y / x ]_ B -> [_ Y / x ]_ B <_ [_ X / x ]_ B ) )
241	70, 238, 240	sylc 58	. . . . . . 7 |- ( ph -> [_ Y / x ]_ B <_ [_ X / x ]_ B )
242	50, 74, 68, 237, 241	lemul2ad 9907	. . . . . 6 |- ( ph -> ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) <_ ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) )
243	92, 75, 79, 242	lesub1dd 9598	. . . . 5 |- ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ X / x ]_ A ) <_ ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) )
244	67, 93, 80, 233, 243	letrd 9183	. . . 4 |- ( ph -> ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) <_ ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) )
245	67, 80, 91, 244	leadd1dd 9596	. . 3 |- ( ph -> ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) <_ ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) )
246		dvfsum.m	. . . 4 |- ( ph -> M e. ZZ )
247		dvfsum.md	. . . 4 |- ( ph -> M <_ ( D + 1 ) )
248		dvfsum.u	. . . 4 |- ( ph -> U e. RR* )
249		dvfsum.h	. . . 4 |- H = ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) )
250		dvfsumlem1.6	. . . 4 |- ( ph -> Y <_ ( ( |_ ` X ) + 1 ) )
251	1, 85, 246, 159, 247, 8, 32, 33, 82, 34, 87, 248, 199, 249, 6, 4, 166, 19, 171, 250	dvfsumlem1 19863	. . 3 |- ( ph -> ( H ` Y ) = ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) )
252	13	leidd 9549	. . . 4 |- ( ph -> X <_ X )
253	17, 18, 248, 19, 171	xrletrd 10708	. . . 4 |- ( ph -> X <_ U )
254		fllep1 11165	. . . . 5 |- ( X e. RR -> X <_ ( ( |_ ` X ) + 1 ) )
255	13, 254	syl 16	. . . 4 |- ( ph -> X <_ ( ( |_ ` X ) + 1 ) )
256	1, 85, 246, 159, 247, 8, 32, 33, 82, 34, 87, 248, 199, 249, 6, 6, 166, 252, 253, 255	dvfsumlem1 19863	. . 3 |- ( ph -> ( H ` X ) = ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) )
257	245, 251, 256	3brtr4d 4202	. 2 |- ( ph -> ( H ` Y ) <_ ( H ` X ) )
258	80, 74	resubcld 9421	. . . . 5 |- ( ph -> ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) - [_ X / x ]_ B ) e. RR )
259	67, 50	resubcld 9421	. . . . 5 |- ( ph -> ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) - [_ Y / x ]_ B ) e. RR )
260		peano2rem 9323	. . . . . . . . . . 11 |- ( ( X - ( |_ ` X ) ) e. RR -> ( ( X - ( |_ ` X ) ) - 1 ) e. RR )
261	68, 260	syl 16	. . . . . . . . . 10 |- ( ph -> ( ( X - ( |_ ` X ) ) - 1 ) e. RR )
262	261, 74	remulcld 9072	. . . . . . . . 9 |- ( ph -> ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) e. RR )
263	262, 79	resubcld 9421	. . . . . . . 8 |- ( ph -> ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) e. RR )
264		peano2rem 9323	. . . . . . . . . . 11 |- ( ( Y - ( |_ ` X ) ) e. RR -> ( ( Y - ( |_ ` X ) ) - 1 ) e. RR )
265	16, 264	syl 16	. . . . . . . . . 10 |- ( ph -> ( ( Y - ( |_ ` X ) ) - 1 ) e. RR )
266	265, 74	remulcld 9072	. . . . . . . . 9 |- ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) e. RR )
267	266, 66	resubcld 9421	. . . . . . . 8 |- ( ph -> ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ Y / x ]_ A ) e. RR )
268	265, 50	remulcld 9072	. . . . . . . . 9 |- ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) e. RR )
269	268, 66	resubcld 9421	. . . . . . . 8 |- ( ph -> ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) e. RR )
270	262	recnd 9070	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) e. CC )
271	266	recnd 9070	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) e. CC )
272	270, 271	subcld 9367	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) ) e. CC )
273	272, 212	addcomd 9224	. . . . . . . . . . . 12 |- ( ph -> ( ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) ) + [_ Y / x ]_ A ) = ( [_ Y / x ]_ A + ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) ) ) )
274	270, 271, 212	subsubd 9395	. . . . . . . . . . . 12 |- ( ph -> ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ Y / x ]_ A ) ) = ( ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) ) + [_ Y / x ]_ A ) )
275	212, 271, 270	subsub2d 9396	. . . . . . . . . . . 12 |- ( ph -> ( [_ Y / x ]_ A - ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) ) ) = ( [_ Y / x ]_ A + ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) ) ) )
276	273, 274, 275	3eqtr4d 2446	. . . . . . . . . . 11 |- ( ph -> ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ Y / x ]_ A ) ) = ( [_ Y / x ]_ A - ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) ) ) )
277	119	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> 1 e. CC )
278	218, 219, 277	nnncan2d 9402	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) - ( ( X - ( |_ ` X ) ) - 1 ) ) = ( ( Y - ( |_ ` X ) ) - ( X - ( |_ ` X ) ) ) )
279	278, 216	eqtrd 2436	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) - ( ( X - ( |_ ` X ) ) - 1 ) ) = ( Y - X ) )
280	279	oveq1d 6055	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( ( Y - ( |_ ` X ) ) - 1 ) - ( ( X - ( |_ ` X ) ) - 1 ) ) x. [_ X / x ]_ B ) = ( ( Y - X ) x. [_ X / x ]_ B ) )
281	265	recnd 9070	. . . . . . . . . . . . . 14 |- ( ph -> ( ( Y - ( |_ ` X ) ) - 1 ) e. CC )
282	261	recnd 9070	. . . . . . . . . . . . . 14 |- ( ph -> ( ( X - ( |_ ` X ) ) - 1 ) e. CC )
283	74	recnd 9070	. . . . . . . . . . . . . 14 |- ( ph -> [_ X / x ]_ B e. CC )
284	281, 282, 283	subdird 9446	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( ( Y - ( |_ ` X ) ) - 1 ) - ( ( X - ( |_ ` X ) ) - 1 ) ) x. [_ X / x ]_ B ) = ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) ) )
285	221, 283	mulcomd 9065	. . . . . . . . . . . . 13 |- ( ph -> ( ( Y - X ) x. [_ X / x ]_ B ) = ( [_ X / x ]_ B x. ( Y - X ) ) )
286	280, 284, 285	3eqtr3d 2444	. . . . . . . . . . . 12 |- ( ph -> ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) ) = ( [_ X / x ]_ B x. ( Y - X ) ) )
287	286	oveq2d 6056	. . . . . . . . . . 11 |- ( ph -> ( [_ Y / x ]_ A - ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) ) ) = ( [_ Y / x ]_ A - ( [_ X / x ]_ B x. ( Y - X ) ) ) )
288	276, 287	eqtrd 2436	. . . . . . . . . 10 |- ( ph -> ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ Y / x ]_ A ) ) = ( [_ Y / x ]_ A - ( [_ X / x ]_ B x. ( Y - X ) ) ) )
289	74, 94	remulcld 9072	. . . . . . . . . . 11 |- ( ph -> ( [_ X / x ]_ B x. ( Y - X ) ) e. RR )
290		cncfmptc 18894	. . . . . . . . . . . . . . 15 |- ( ( [_ X / x ]_ B e. RR /\ ( X [,] Y ) C_ CC /\ RR C_ CC ) -> ( y e. ( X [,] Y ) |-> [_ X / x ]_ B ) e. ( ( X [,] Y ) -cn-> RR ) )
291	74, 104, 105, 290	syl3anc 1184	. . . . . . . . . . . . . 14 |- ( ph -> ( y e. ( X [,] Y ) |-> [_ X / x ]_ B ) e. ( ( X [,] Y ) -cn-> RR ) )
292		remulcl 9031	. . . . . . . . . . . . . 14 |- ( ( [_ X / x ]_ B e. RR /\ y e. RR ) -> ( [_ X / x ]_ B x. y ) e. RR )
293	100, 101, 291, 109, 103, 292	cncfmpt2ss 18898	. . . . . . . . . . . . 13 |- ( ph -> ( y e. ( X [,] Y ) |-> ( [_ X / x ]_ B x. y ) ) e. ( ( X [,] Y ) -cn-> RR ) )
294	114, 118, 120, 128, 283	dvmptcmul 19803	. . . . . . . . . . . . . 14 |- ( ph -> ( RR _D ( y e. ( X (,) Y ) |-> ( [_ X / x ]_ B x. y ) ) ) = ( y e. ( X (,) Y ) |-> ( [_ X / x ]_ B x. 1 ) ) )
295	283	mulid1d 9061	. . . . . . . . . . . . . . 15 |- ( ph -> ( [_ X / x ]_ B x. 1 ) = [_ X / x ]_ B )
296	295	mpteq2dv 4256	. . . . . . . . . . . . . 14 |- ( ph -> ( y e. ( X (,) Y ) |-> ( [_ X / x ]_ B x. 1 ) ) = ( y e. ( X (,) Y ) |-> [_ X / x ]_ B ) )
297	294, 296	eqtrd 2436	. . . . . . . . . . . . 13 |- ( ph -> ( RR _D ( y e. ( X (,) Y ) |-> ( [_ X / x ]_ B x. y ) ) ) = ( y e. ( X (,) Y ) |-> [_ X / x ]_ B ) )
298	6	adantr 452	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. ( X [,] Y ) ) -> X e. S )
299	165	rexrd 9090	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. ( X [,] Y ) ) -> y e. RR* )
300	18	adantr 452	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. ( X [,] Y ) ) -> Y e. RR* )
301	248	adantr 452	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. ( X [,] Y ) ) -> U e. RR* )
302	299, 300, 301, 170, 172	xrletrd 10708	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. ( X [,] Y ) ) -> y <_ U )
303		vex 2919	. . . . . . . . . . . . . . . 16 |- y e. _V
304		eleq1 2464	. . . . . . . . . . . . . . . . . . 19 |- ( k = y -> ( k e. S <-> y e. S ) )
305	304	anbi2d 685	. . . . . . . . . . . . . . . . . 18 |- ( k = y -> ( ( X e. S /\ k e. S ) <-> ( X e. S /\ y e. S ) ) )
306		breq2 4176	. . . . . . . . . . . . . . . . . . 19 |- ( k = y -> ( X <_ k <-> X <_ y ) )
307		breq1 4175	. . . . . . . . . . . . . . . . . . 19 |- ( k = y -> ( k <_ U <-> y <_ U ) )
308	306, 307	3anbi23d 1257	. . . . . . . . . . . . . . . . . 18 |- ( k = y -> ( ( D <_ X /\ X <_ k /\ k <_ U ) <-> ( D <_ X /\ X <_ y /\ y <_ U ) ) )
309	305, 308	3anbi23d 1257	. . . . . . . . . . . . . . . . 17 |- ( k = y -> ( ( ph /\ ( X e. S /\ k e. S ) /\ ( D <_ X /\ X <_ k /\ k <_ U ) ) <-> ( ph /\ ( X e. S /\ y e. S ) /\ ( D <_ X /\ X <_ y /\ y <_ U ) ) ) )
310		csbeq1 3214	. . . . . . . . . . . . . . . . . . 19 |- ( k = y -> [_ k / x ]_ B = [_ y / x ]_ B )
311	182, 310	syl5eqr 2450	. . . . . . . . . . . . . . . . . 18 |- ( k = y -> C = [_ y / x ]_ B )
312	311	breq1d 4182	. . . . . . . . . . . . . . . . 17 |- ( k = y -> ( C <_ [_ X / x ]_ B <-> [_ y / x ]_ B <_ [_ X / x ]_ B ) )
313	309, 312	imbi12d 312	. . . . . . . . . . . . . . . 16 |- ( k = y -> ( ( ( ph /\ ( X e. S /\ k e. S ) /\ ( D <_ X /\ X <_ k /\ k <_ U ) ) -> C <_ [_ X / x ]_ B ) <-> ( ( ph /\ ( X e. S /\ y e. S ) /\ ( D <_ X /\ X <_ y /\ y <_ U ) ) -> [_ y / x ]_ B <_ [_ X / x ]_ B ) ) )
314		simp2l 983	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ( X e. S /\ k e. S ) /\ ( D <_ X /\ X <_ k /\ k <_ U ) ) -> X e. S )
315		nfcv 2540	. . . . . . . . . . . . . . . . . 18 |- F/_ x X
316		nfv 1626	. . . . . . . . . . . . . . . . . . 19 |- F/ x ( ph /\ ( X e. S /\ k e. S ) /\ ( D <_ X /\ X <_ k /\ k <_ U ) )
317		nfcsb1v 3243	. . . . . . . . . . . . . . . . . . . 20 |- F/_ x [_ X / x ]_ B
318	181, 188, 317	nfbr 4216	. . . . . . . . . . . . . . . . . . 19 |- F/ x C <_ [_ X / x ]_ B
319	316, 318	nfim 1828	. . . . . . . . . . . . . . . . . 18 |- F/ x ( ( ph /\ ( X e. S /\ k e. S ) /\ ( D <_ X /\ X <_ k /\ k <_ U ) ) -> C <_ [_ X / x ]_ B )
320		eleq1 2464	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = X -> ( x e. S <-> X e. S ) )
321	320	anbi1d 686	. . . . . . . . . . . . . . . . . . . 20 |- ( x = X -> ( ( x e. S /\ k e. S ) <-> ( X e. S /\ k e. S ) ) )
322		breq2 4176	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = X -> ( D <_ x <-> D <_ X ) )
323		breq1 4175	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = X -> ( x <_ k <-> X <_ k ) )
324	322, 323	3anbi12d 1255	. . . . . . . . . . . . . . . . . . . 20 |- ( x = X -> ( ( D <_ x /\ x <_ k /\ k <_ U ) <-> ( D <_ X /\ X <_ k /\ k <_ U ) ) )
325	321, 324	3anbi23d 1257	. . . . . . . . . . . . . . . . . . 19 |- ( x = X -> ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) <-> ( ph /\ ( X e. S /\ k e. S ) /\ ( D <_ X /\ X <_ k /\ k <_ U ) ) ) )
326		csbeq1a 3219	. . . . . . . . . . . . . . . . . . . 20 |- ( x = X -> B = [_ X / x ]_ B )
327	326	breq2d 4184	. . . . . . . . . . . . . . . . . . 19 |- ( x = X -> ( C <_ B <-> C <_ [_ X / x ]_ B ) )
328	325, 327	imbi12d 312	. . . . . . . . . . . . . . . . . 18 |- ( x = X -> ( ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> C <_ B ) <-> ( ( ph /\ ( X e. S /\ k e. S ) /\ ( D <_ X /\ X <_ k /\ k <_ U ) ) -> C <_ [_ X / x ]_ B ) ) )
329	315, 319, 328, 199	vtoclgf 2970	. . . . . . . . . . . . . . . . 17 |- ( X e. S -> ( ( ph /\ ( X e. S /\ k e. S ) /\ ( D <_ X /\ X <_ k /\ k <_ U ) ) -> C <_ [_ X / x ]_ B ) )
330	314, 329	mpcom 34	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( X e. S /\ k e. S ) /\ ( D <_ X /\ X <_ k /\ k <_ U ) ) -> C <_ [_ X / x ]_ B )
331	303, 313, 330	vtocl 2966	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( X e. S /\ y e. S ) /\ ( D <_ X /\ X <_ y /\ y <_ U ) ) -> [_ y / x ]_ B <_ [_ X / x ]_ B )
332	157, 298, 30, 167, 168, 302, 331	syl123anc 1201	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( X [,] Y ) ) -> [_ y / x ]_ B <_ [_ X / x ]_ B )
333	156, 332	sylan2 461	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. ( X (,) Y ) ) -> [_ y / x ]_ B <_ [_ X / x ]_ B )
334		oveq2 6048	. . . . . . . . . . . . 13 |- ( y = X -> ( [_ X / x ]_ B x. y ) = ( [_ X / x ]_ B x. X ) )
335		oveq2 6048	. . . . . . . . . . . . 13 |- ( y = Y -> ( [_ X / x ]_ B x. y ) = ( [_ X / x ]_ B x. Y ) )
336	13, 5, 150, 155, 293, 297, 333, 70, 21, 19, 76, 334, 63, 335	dvle 19844	. . . . . . . . . . . 12 |- ( ph -> ( [_ Y / x ]_ A - [_ X / x ]_ A ) <_ ( ( [_ X / x ]_ B x. Y ) - ( [_ X / x ]_ B x. X ) ) )
337	283, 97, 98	subdid 9445	. . . . . . . . . . . 12 |- ( ph -> ( [_ X / x ]_ B x. ( Y - X ) ) = ( ( [_ X / x ]_ B x. Y ) - ( [_ X / x ]_ B x. X ) ) )
338	336, 337	breqtrrd 4198	. . . . . . . . . . 11 |- ( ph -> ( [_ Y / x ]_ A - [_ X / x ]_ A ) <_ ( [_ X / x ]_ B x. ( Y - X ) ) )
339	66, 79, 289, 338	subled 9585	. . . . . . . . . 10 |- ( ph -> ( [_ Y / x ]_ A - ( [_ X / x ]_ B x. ( Y - X ) ) ) <_ [_ X / x ]_ A )
340	288, 339	eqbrtrd 4192	. . . . . . . . 9 |- ( ph -> ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ Y / x ]_ A ) ) <_ [_ X / x ]_ A )
341	262, 267, 79, 340	subled 9585	. . . . . . . 8 |- ( ph -> ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) <_ ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ Y / x ]_ A ) )
342	265	renegcld 9420	. . . . . . . . . . . 12 |- ( ph -> -u ( ( Y - ( |_ ` X ) ) - 1 ) e. RR )
343		1re 9046	. . . . . . . . . . . . . . . . 17 |- 1 e. RR
344	343	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> 1 e. RR )
345	5, 15, 344	lesubadd2d 9581	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( Y - ( |_ ` X ) ) <_ 1 <-> Y <_ ( ( |_ ` X ) + 1 ) ) )
346	250, 345	mpbird 224	. . . . . . . . . . . . . 14 |- ( ph -> ( Y - ( |_ ` X ) ) <_ 1 )
347	16, 344	suble0d 9573	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) <_ 0 <-> ( Y - ( |_ ` X ) ) <_ 1 ) )
348	346, 347	mpbird 224	. . . . . . . . . . . . 13 |- ( ph -> ( ( Y - ( |_ ` X ) ) - 1 ) <_ 0 )
349	265	le0neg1d 9554	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) <_ 0 <-> 0 <_ -u ( ( Y - ( |_ ` X ) ) - 1 ) ) )
350	348, 349	mpbid 202	. . . . . . . . . . . 12 |- ( ph -> 0 <_ -u ( ( Y - ( |_ ` X ) ) - 1 ) )
351	50, 74, 342, 350, 241	lemul2ad 9907	. . . . . . . . . . 11 |- ( ph -> ( -u ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) <_ ( -u ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) )
352	281, 96	mulneg1d 9442	. . . . . . . . . . 11 |- ( ph -> ( -u ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) = -u ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) )
353	281, 283	mulneg1d 9442	. . . . . . . . . . 11 |- ( ph -> ( -u ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) = -u ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) )
354	351, 352, 353	3brtr3d 4201	. . . . . . . . . 10 |- ( ph -> -u ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) <_ -u ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) )
355	266, 268	lenegd 9561	. . . . . . . . . 10 |- ( ph -> ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) <_ ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) <-> -u ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) <_ -u ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) ) )
356	354, 355	mpbird 224	. . . . . . . . 9 |- ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) <_ ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) )
357	266, 268, 66, 356	lesub1dd 9598	. . . . . . . 8 |- ( ph -> ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ Y / x ]_ A ) <_ ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) )
358	263, 267, 269, 341, 357	letrd 9183	. . . . . . 7 |- ( ph -> ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) <_ ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) )
359	219, 277, 283	subdird 9446	. . . . . . . . 9 |- ( ph -> ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) = ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - ( 1 x. [_ X / x ]_ B ) ) )
360	283	mulid2d 9062	. . . . . . . . . 10 |- ( ph -> ( 1 x. [_ X / x ]_ B ) = [_ X / x ]_ B )
361	360	oveq2d 6056	. . . . . . . . 9 |- ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - ( 1 x. [_ X / x ]_ B ) ) = ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ B ) )
362	359, 361	eqtrd 2436	. . . . . . . 8 |- ( ph -> ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) = ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ B ) )
363	362	oveq1d 6055	. . . . . . 7 |- ( ph -> ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) = ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ B ) - [_ X / x ]_ A ) )
364	218, 277, 96	subdird 9446	. . . . . . . . 9 |- ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( 1 x. [_ Y / x ]_ B ) ) )
365	96	mulid2d 9062	. . . . . . . . . 10 |- ( ph -> ( 1 x. [_ Y / x ]_ B ) = [_ Y / x ]_ B )
366	365	oveq2d 6056	. . . . . . . . 9 |- ( ph -> ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( 1 x. [_ Y / x ]_ B ) ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ B ) )
367	364, 366	eqtrd 2436	. . . . . . . 8 |- ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ B ) )
368	367	oveq1d 6055	. . . . . . 7 |- ( ph -> ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) = ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ B ) - [_ Y / x ]_ A ) )
369	358, 363, 368	3brtr3d 4201	. . . . . 6 |- ( ph -> ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ B ) - [_ X / x ]_ A ) <_ ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ B ) - [_ Y / x ]_ A ) )
370	75	recnd 9070	. . . . . . 7 |- ( ph -> ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) e. CC )
371	79	recnd 9070	. . . . . . 7 |- ( ph -> [_ X / x ]_ A e. CC )
372	370, 371, 283	sub32d 9399	. . . . . 6 |- ( ph -> ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) - [_ X / x ]_ B ) = ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ B ) - [_ X / x ]_ A ) )
373	211, 212, 96	sub32d 9399	. . . . . 6 |- ( ph -> ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) - [_ Y / x ]_ B ) = ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ B ) - [_ Y / x ]_ A ) )
374	369, 372, 373	3brtr4d 4202	. . . . 5 |- ( ph -> ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) - [_ X / x ]_ B ) <_ ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) - [_ Y / x ]_ B ) )
375	258, 259, 91, 374	leadd1dd 9596	. . . 4 |- ( ph -> ( ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) - [_ X / x ]_ B ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) <_ ( ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) - [_ Y / x ]_ B ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) )
376	80	recnd 9070	. . . . 5 |- ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) e. CC )
377	91	recnd 9070	. . . . 5 |- ( ph -> sum_ k e. ( M ... ( |_ ` X ) ) C e. CC )
378	376, 377, 283	addsubd 9388	. . . 4 |- ( ph -> ( ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) - [_ X / x ]_ B ) = ( ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) - [_ X / x ]_ B ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) )
379	67	recnd 9070	. . . . 5 |- ( ph -> ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) e. CC )
380	379, 377, 96	addsubd 9388	. . . 4 |- ( ph -> ( ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) - [_ Y / x ]_ B ) = ( ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) - [_ Y / x ]_ B ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) )
381	375, 378, 380	3brtr4d 4202	. . 3 |- ( ph -> ( ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) - [_ X / x ]_ B ) <_ ( ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) - [_ Y / x ]_ B ) )
382	256	oveq1d 6055	. . 3 |- ( ph -> ( ( H ` X ) - [_ X / x ]_ B ) = ( ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) - [_ X / x ]_ B ) )
383	251	oveq1d 6055	. . 3 |- ( ph -> ( ( H ` Y ) - [_ Y / x ]_ B ) = ( ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) - [_ Y / x ]_ B ) )
384	381, 382, 383	3brtr4d 4202	. 2 |- ( ph -> ( ( H ` X ) - [_ X / x ]_ B ) <_ ( ( H ` Y ) - [_ Y / x ]_ B ) )
385	257, 384	jca 519	1 |- ( ph -> ( ( H ` Y ) <_ ( H ` X ) /\ ( ( H ` X ) - [_ X / x ]_ B ) <_ ( ( H ` Y ) - [_ Y / x ]_ B ) ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   A.wral 2666   [_csb 3211   C_ wss 3280   {cpr 3775   class class class wbr 4172   e. cmpt 4226   dom cdm 4837   ran crn 4838   |` cres 4839   -->wf 5409   ` cfv 5413  (class class class)co 6040   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947   + caddc 8949   x. cmul 8951   +oocpnf 9073   RR*cxr 9075   < clt 9076   <_ cle 9077   - cmin 9247   -ucneg 9248   ZZcz 10238   ZZ>=cuz 10444   (,)cioo 10872   [,]cicc 10875   ...cfz 10999   |_cfl 11156   sum_csu 12434   TopOpenctopn 13604   topGenctg 13620  ℂ_fldccnfld 16658   -cn->ccncf 18859   _D cdv 19703

This theorem is referenced by:  dvfsumlem3  19865

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024  ax-addf 9025  ax-mulf 9026

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-iin 4056  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-2o 6684  df-oadd 6687  df-er 6864  df-map 6979  df-pm 6980  df-ixp 7023  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-fi 7374  df-sup 7404  df-oi 7435  df-card 7782  df-cda 8004  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-4 10016  df-5 10017  df-6 10018  df-7 10019  df-8 10020  df-9 10021  df-10 10022  df-n0 10178  df-z 10239  df-dec 10339  df-uz 10445  df-q 10531  df-rp 10569  df-xneg 10666  df-xadd 10667  df-xmul 10668  df-ioo 10876  df-ico 10878  df-icc 10879  df-fz 11000  df-fzo 11091  df-fl 11157  df-seq 11279  df-exp 11338  df-hash 11574  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-clim 12237  df-sum 12435  df-struct 13426  df-ndx 13427  df-slot 13428  df-base 13429  df-sets 13430  df-ress 13431  df-plusg 13497  df-mulr 13498  df-starv 13499  df-sca 13500  df-vsca 13501  df-tset 13503  df-ple 13504  df-ds 13506  df-unif 13507  df-hom 13508  df-cco 13509  df-rest 13605  df-topn 13606  df-topgen 13622  df-pt 13623  df-prds 13626  df-xrs 13681  df-0g 13682  df-gsum 13683  df-qtop 13688  df-imas 13689  df-xps 13691  df-mre 13766  df-mrc 13767  df-acs 13769  df-mnd 14645  df-submnd 14694  df-mulg 14770  df-cntz 15071  df-cmn 15369  df-psmet 16649  df-xmet 16650  df-met 16651  df-bl 16652  df-mopn 16653  df-fbas 16654  df-fg 16655  df-cnfld 16659  df-top 16918  df-bases 16920  df-topon 16921  df-topsp 16922  df-cld 17038  df-ntr 17039  df-cls 17040  df-nei 17117  df-lp 17155  df-perf 17156  df-cn 17245  df-cnp 17246  df-haus 17333  df-cmp 17404  df-tx 17547  df-hmeo 17740  df-fil 17831  df-fm 17923  df-flim 17924  df-flf 17925  df-xms 18303  df-ms 18304  df-tms 18305  df-cncf 18861  df-limc 19706  df-dv 19707