Metamath Proof Explorer

Theorem dvfsumlem2

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

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

Proof

Step Hyp Ref Expression
1 dvfsum.s 
 |-  S = ( T (,) +oo )
2 dvfsum.z 
 |-  Z = ( ZZ>= ` M )
3 dvfsum.m 
 |-  ( ph -> M e. ZZ )
4 dvfsum.d 
 |-  ( ph -> D e. RR )
5 dvfsum.md 
 |-  ( ph -> M <_ ( D + 1 ) )
6 dvfsum.t 
 |-  ( ph -> T e. RR )
7 dvfsum.a 
 |-  ( ( ph /\ x e. S ) -> A e. RR )
8 dvfsum.b1 
 |-  ( ( ph /\ x e. S ) -> B e. V )
9 dvfsum.b2 
 |-  ( ( ph /\ x e. Z ) -> B e. RR )
10 dvfsum.b3 
 |-  ( ph -> ( RR _D ( x e. S |-> A ) ) = ( x e. S |-> B ) )
11 dvfsum.c 
 |-  ( x = k -> B = C )
12 dvfsum.u 
 |-  ( ph -> U e. RR* )
13 dvfsum.l 
 |-  ( ( ph /\ ( x e. S /\ k e. S ) /\ ( D <_ x /\ x <_ k /\ k <_ U ) ) -> C <_ B )
14 dvfsum.h 
 |-  H = ( x e. S |-> ( ( ( x - ( |_ ` x ) ) x. B ) + ( sum_ k e. ( M ... ( |_ ` x ) ) C - A ) ) )
15 dvfsumlem1.1 
 |-  ( ph -> X e. S )
16 dvfsumlem1.2 
 |-  ( ph -> Y e. S )
17 dvfsumlem1.3 
 |-  ( ph -> D <_ X )
18 dvfsumlem1.4 
 |-  ( ph -> X <_ Y )
19 dvfsumlem1.5 
 |-  ( ph -> Y <_ U )
20 dvfsumlem1.6 
 |-  ( ph -> Y <_ ( ( |_ ` X ) + 1 ) )
21 ioossre 
 |-  ( T (,) +oo ) C_ RR
22 1 21 eqsstri 
 |-  S C_ RR
23 22 16 sselid 
 |-  ( ph -> Y e. RR )
24 15 1 eleqtrdi 
 |-  ( ph -> X e. ( T (,) +oo ) )
25 6 rexrd 
 |-  ( ph -> T e. RR* )
26 elioopnf 
 |-  ( T e. RR* -> ( X e. ( T (,) +oo ) <-> ( X e. RR /\ T < X ) ) )
27 25 26 syl 
 |-  ( ph -> ( X e. ( T (,) +oo ) <-> ( X e. RR /\ T < X ) ) )
28 24 27 mpbid 
 |-  ( ph -> ( X e. RR /\ T < X ) )
29 28 simpld 
 |-  ( ph -> X e. RR )
30 reflcl 
 |-  ( X e. RR -> ( |_ ` X ) e. RR )
31 29 30 syl 
 |-  ( ph -> ( |_ ` X ) e. RR )
32 23 31 resubcld 
 |-  ( ph -> ( Y - ( |_ ` X ) ) e. RR )
33 csbeq1 
 |-  ( y = Y -> [_ y / x ]_ B = [_ Y / x ]_ B )
34 33 eleq1d 
 |-  ( y = Y -> ( [_ y / x ]_ B e. RR <-> [_ Y / x ]_ B e. RR ) )
35 22 a1i 
 |-  ( ph -> S C_ RR )
36 35 7 8 10 dvmptrecl 
 |-  ( ( ph /\ x e. S ) -> B e. RR )
37 36 fmpttd 
 |-  ( ph -> ( x e. S |-> B ) : S --> RR )
38 nfcv 
 |-  F/_ y B
39 nfcsb1v 
 |-  F/_ x [_ y / x ]_ B
40 csbeq1a 
 |-  ( x = y -> B = [_ y / x ]_ B )
41 38 39 40 cbvmpt 
 |-  ( x e. S |-> B ) = ( y e. S |-> [_ y / x ]_ B )
42 41 fmpt 
 |-  ( A. y e. S [_ y / x ]_ B e. RR <-> ( x e. S |-> B ) : S --> RR )
43 37 42 sylibr 
 |-  ( ph -> A. y e. S [_ y / x ]_ B e. RR )
44 34 43 16 rspcdva 
 |-  ( ph -> [_ Y / x ]_ B e. RR )
45 32 44 remulcld 
 |-  ( ph -> ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) e. RR )
46 csbeq1 
 |-  ( y = Y -> [_ y / x ]_ A = [_ Y / x ]_ A )
47 46 eleq1d 
 |-  ( y = Y -> ( [_ y / x ]_ A e. RR <-> [_ Y / x ]_ A e. RR ) )
48 7 fmpttd 
 |-  ( ph -> ( x e. S |-> A ) : S --> RR )
49 nfcv 
 |-  F/_ y A
50 nfcsb1v 
 |-  F/_ x [_ y / x ]_ A
51 csbeq1a 
 |-  ( x = y -> A = [_ y / x ]_ A )
52 49 50 51 cbvmpt 
 |-  ( x e. S |-> A ) = ( y e. S |-> [_ y / x ]_ A )
53 52 fmpt 
 |-  ( A. y e. S [_ y / x ]_ A e. RR <-> ( x e. S |-> A ) : S --> RR )
54 48 53 sylibr 
 |-  ( ph -> A. y e. S [_ y / x ]_ A e. RR )
55 47 54 16 rspcdva 
 |-  ( ph -> [_ Y / x ]_ A e. RR )
56 45 55 resubcld 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) e. RR )
57 29 31 resubcld 
 |-  ( ph -> ( X - ( |_ ` X ) ) e. RR )
58 csbeq1 
 |-  ( y = X -> [_ y / x ]_ B = [_ X / x ]_ B )
59 58 eleq1d 
 |-  ( y = X -> ( [_ y / x ]_ B e. RR <-> [_ X / x ]_ B e. RR ) )
60 59 43 15 rspcdva 
 |-  ( ph -> [_ X / x ]_ B e. RR )
61 57 60 remulcld 
 |-  ( ph -> ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) e. RR )
62 csbeq1 
 |-  ( y = X -> [_ y / x ]_ A = [_ X / x ]_ A )
63 62 eleq1d 
 |-  ( y = X -> ( [_ y / x ]_ A e. RR <-> [_ X / x ]_ A e. RR ) )
64 63 54 15 rspcdva 
 |-  ( ph -> [_ X / x ]_ A e. RR )
65 61 64 resubcld 
 |-  ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) e. RR )
66 fzfid 
 |-  ( ph -> ( M ... ( |_ ` X ) ) e. Fin )
67 9 ralrimiva 
 |-  ( ph -> A. x e. Z B e. RR )
68 elfzuz 
 |-  ( k e. ( M ... ( |_ ` X ) ) -> k e. ( ZZ>= ` M ) )
69 68 2 eleqtrrdi 
 |-  ( k e. ( M ... ( |_ ` X ) ) -> k e. Z )
70 11 eleq1d 
 |-  ( x = k -> ( B e. RR <-> C e. RR ) )
71 70 rspccva 
 |-  ( ( A. x e. Z B e. RR /\ k e. Z ) -> C e. RR )
72 67 69 71 syl2an 
 |-  ( ( ph /\ k e. ( M ... ( |_ ` X ) ) ) -> C e. RR )
73 66 72 fsumrecl 
 |-  ( ph -> sum_ k e. ( M ... ( |_ ` X ) ) C e. RR )
74 57 44 remulcld 
 |-  ( ph -> ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) e. RR )
75 74 64 resubcld 
 |-  ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ X / x ]_ A ) e. RR )
76 23 29 resubcld 
 |-  ( ph -> ( Y - X ) e. RR )
77 44 76 remulcld 
 |-  ( ph -> ( [_ Y / x ]_ B x. ( Y - X ) ) e. RR )
78 44 recnd 
 |-  ( ph -> [_ Y / x ]_ B e. CC )
79 23 recnd 
 |-  ( ph -> Y e. CC )
80 29 recnd 
 |-  ( ph -> X e. CC )
81 78 79 80 subdid 
 |-  ( ph -> ( [_ Y / x ]_ B x. ( Y - X ) ) = ( ( [_ Y / x ]_ B x. Y ) - ( [_ Y / x ]_ B x. X ) ) )
82 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
83 82 mulcn 
 |-  x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
84 pnfxr 
 |-  +oo e. RR*
85 84 a1i 
 |-  ( ph -> +oo e. RR* )
86 28 simprd 
 |-  ( ph -> T < X )
87 23 ltpnfd 
 |-  ( ph -> Y < +oo )
88 iccssioo 
 |-  ( ( ( T e. RR* /\ +oo e. RR* ) /\ ( T < X /\ Y < +oo ) ) -> ( X [,] Y ) C_ ( T (,) +oo ) )
89 25 85 86 87 88 syl22anc 
 |-  ( ph -> ( X [,] Y ) C_ ( T (,) +oo ) )
90 89 21 sstrdi 
 |-  ( ph -> ( X [,] Y ) C_ RR )
91 ax-resscn 
 |-  RR C_ CC
92 90 91 sstrdi 
 |-  ( ph -> ( X [,] Y ) C_ CC )
93 91 a1i 
 |-  ( ph -> RR C_ CC )
94 cncfmptc 
 |-  ( ( [_ Y / x ]_ B e. RR /\ ( X [,] Y ) C_ CC /\ RR C_ CC ) -> ( y e. ( X [,] Y ) |-> [_ Y / x ]_ B ) e. ( ( X [,] Y ) -cn-> RR ) )
95 44 92 93 94 syl3anc 
 |-  ( ph -> ( y e. ( X [,] Y ) |-> [_ Y / x ]_ B ) e. ( ( X [,] Y ) -cn-> RR ) )
96 cncfmptid 
 |-  ( ( ( X [,] Y ) C_ RR /\ RR C_ CC ) -> ( y e. ( X [,] Y ) |-> y ) e. ( ( X [,] Y ) -cn-> RR ) )
97 90 91 96 sylancl 
 |-  ( ph -> ( y e. ( X [,] Y ) |-> y ) e. ( ( X [,] Y ) -cn-> RR ) )
98 remulcl 
 |-  ( ( [_ Y / x ]_ B e. RR /\ y e. RR ) -> ( [_ Y / x ]_ B x. y ) e. RR )
99 82 83 95 97 91 98 cncfmpt2ss 
 |-  ( ph -> ( y e. ( X [,] Y ) |-> ( [_ Y / x ]_ B x. y ) ) e. ( ( X [,] Y ) -cn-> RR ) )
100 reelprrecn 
 |-  RR e. { RR , CC }
101 100 a1i 
 |-  ( ph -> RR e. { RR , CC } )
102 ioossicc 
 |-  ( X (,) Y ) C_ ( X [,] Y )
103 102 90 sstrid 
 |-  ( ph -> ( X (,) Y ) C_ RR )
104 103 sselda 
 |-  ( ( ph /\ y e. ( X (,) Y ) ) -> y e. RR )
105 104 recnd 
 |-  ( ( ph /\ y e. ( X (,) Y ) ) -> y e. CC )
106 1cnd 
 |-  ( ( ph /\ y e. ( X (,) Y ) ) -> 1 e. CC )
107 simpr 
 |-  ( ( ph /\ y e. RR ) -> y e. RR )
108 107 recnd 
 |-  ( ( ph /\ y e. RR ) -> y e. CC )
109 1cnd 
 |-  ( ( ph /\ y e. RR ) -> 1 e. CC )
110 101 dvmptid 
 |-  ( ph -> ( RR _D ( y e. RR |-> y ) ) = ( y e. RR |-> 1 ) )
111 82 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
112 iooretop 
 |-  ( X (,) Y ) e. ( topGen ` ran (,) )
113 112 a1i 
 |-  ( ph -> ( X (,) Y ) e. ( topGen ` ran (,) ) )
114 101 108 109 110 103 111 82 113 dvmptres 
 |-  ( ph -> ( RR _D ( y e. ( X (,) Y ) |-> y ) ) = ( y e. ( X (,) Y ) |-> 1 ) )
115 101 105 106 114 78 dvmptcmul 
 |-  ( ph -> ( RR _D ( y e. ( X (,) Y ) |-> ( [_ Y / x ]_ B x. y ) ) ) = ( y e. ( X (,) Y ) |-> ( [_ Y / x ]_ B x. 1 ) ) )
116 78 mulid1d 
 |-  ( ph -> ( [_ Y / x ]_ B x. 1 ) = [_ Y / x ]_ B )
117 116 mpteq2dv 
 |-  ( ph -> ( y e. ( X (,) Y ) |-> ( [_ Y / x ]_ B x. 1 ) ) = ( y e. ( X (,) Y ) |-> [_ Y / x ]_ B ) )
118 115 117 eqtrd 
 |-  ( ph -> ( RR _D ( y e. ( X (,) Y ) |-> ( [_ Y / x ]_ B x. y ) ) ) = ( y e. ( X (,) Y ) |-> [_ Y / x ]_ B ) )
119 89 1 sseqtrrdi 
 |-  ( ph -> ( X [,] Y ) C_ S )
120 119 resmptd 
 |-  ( ph -> ( ( y e. S |-> [_ y / x ]_ A ) |` ( X [,] Y ) ) = ( y e. ( X [,] Y ) |-> [_ y / x ]_ A ) )
121 7 recnd 
 |-  ( ( ph /\ x e. S ) -> A e. CC )
122 121 fmpttd 
 |-  ( ph -> ( x e. S |-> A ) : S --> CC )
123 10 dmeqd 
 |-  ( ph -> dom ( RR _D ( x e. S |-> A ) ) = dom ( x e. S |-> B ) )
124 8 ralrimiva 
 |-  ( ph -> A. x e. S B e. V )
125 dmmptg 
 |-  ( A. x e. S B e. V -> dom ( x e. S |-> B ) = S )
126 124 125 syl 
 |-  ( ph -> dom ( x e. S |-> B ) = S )
127 123 126 eqtrd 
 |-  ( ph -> dom ( RR _D ( x e. S |-> A ) ) = S )
128 dvcn 
 |-  ( ( ( 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 ) )
129 93 122 35 127 128 syl31anc 
 |-  ( ph -> ( x e. S |-> A ) e. ( S -cn-> CC ) )
130 cncffvrn 
 |-  ( ( 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 ) )
131 91 129 130 sylancr 
 |-  ( ph -> ( ( x e. S |-> A ) e. ( S -cn-> RR ) <-> ( x e. S |-> A ) : S --> RR ) )
132 48 131 mpbird 
 |-  ( ph -> ( x e. S |-> A ) e. ( S -cn-> RR ) )
133 52 132 eqeltrrid 
 |-  ( ph -> ( y e. S |-> [_ y / x ]_ A ) e. ( S -cn-> RR ) )
134 rescncf 
 |-  ( ( 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 ) ) )
135 119 133 134 sylc 
 |-  ( ph -> ( ( y e. S |-> [_ y / x ]_ A ) |` ( X [,] Y ) ) e. ( ( X [,] Y ) -cn-> RR ) )
136 120 135 eqeltrrd 
 |-  ( ph -> ( y e. ( X [,] Y ) |-> [_ y / x ]_ A ) e. ( ( X [,] Y ) -cn-> RR ) )
137 54 r19.21bi 
 |-  ( ( ph /\ y e. S ) -> [_ y / x ]_ A e. RR )
138 137 recnd 
 |-  ( ( ph /\ y e. S ) -> [_ y / x ]_ A e. CC )
139 43 r19.21bi 
 |-  ( ( ph /\ y e. S ) -> [_ y / x ]_ B e. RR )
140 52 oveq2i 
 |-  ( RR _D ( x e. S |-> A ) ) = ( RR _D ( y e. S |-> [_ y / x ]_ A ) )
141 10 140 41 3eqtr3g 
 |-  ( ph -> ( RR _D ( y e. S |-> [_ y / x ]_ A ) ) = ( y e. S |-> [_ y / x ]_ B ) )
142 102 119 sstrid 
 |-  ( ph -> ( X (,) Y ) C_ S )
143 101 138 139 141 142 111 82 113 dvmptres 
 |-  ( ph -> ( RR _D ( y e. ( X (,) Y ) |-> [_ y / x ]_ A ) ) = ( y e. ( X (,) Y ) |-> [_ y / x ]_ B ) )
144 102 sseli 
 |-  ( y e. ( X (,) Y ) -> y e. ( X [,] Y ) )
145 simpl 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> ph )
146 119 sselda 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> y e. S )
147 16 adantr 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> Y e. S )
148 4 adantr 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> D e. RR )
149 29 adantr 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> X e. RR )
150 elicc2 
 |-  ( ( X e. RR /\ Y e. RR ) -> ( y e. ( X [,] Y ) <-> ( y e. RR /\ X <_ y /\ y <_ Y ) ) )
151 29 23 150 syl2anc 
 |-  ( ph -> ( y e. ( X [,] Y ) <-> ( y e. RR /\ X <_ y /\ y <_ Y ) ) )
152 151 biimpa 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> ( y e. RR /\ X <_ y /\ y <_ Y ) )
153 152 simp1d 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> y e. RR )
154 17 adantr 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> D <_ X )
155 152 simp2d 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> X <_ y )
156 148 149 153 154 155 letrd 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> D <_ y )
157 152 simp3d 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> y <_ Y )
158 19 adantr 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> Y <_ U )
159 simp2r 
 |-  ( ( ph /\ ( y e. S /\ Y e. S ) /\ ( D <_ y /\ y <_ Y /\ Y <_ U ) ) -> Y e. S )
160 eleq1 
 |-  ( k = Y -> ( k e. S <-> Y e. S ) )
161 160 anbi2d 
 |-  ( k = Y -> ( ( y e. S /\ k e. S ) <-> ( y e. S /\ Y e. S ) ) )
162 breq2 
 |-  ( k = Y -> ( y <_ k <-> y <_ Y ) )
163 breq1 
 |-  ( k = Y -> ( k <_ U <-> Y <_ U ) )
164 162 163 3anbi23d 
 |-  ( k = Y -> ( ( D <_ y /\ y <_ k /\ k <_ U ) <-> ( D <_ y /\ y <_ Y /\ Y <_ U ) ) )
165 161 164 3anbi23d 
 |-  ( 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 ) ) ) )
166 vex 
 |-  k e. _V
167 166 11 csbie 
 |-  [_ k / x ]_ B = C
168 csbeq1 
 |-  ( k = Y -> [_ k / x ]_ B = [_ Y / x ]_ B )
169 167 168 eqtr3id 
 |-  ( k = Y -> C = [_ Y / x ]_ B )
170 169 breq1d 
 |-  ( k = Y -> ( C <_ [_ y / x ]_ B <-> [_ Y / x ]_ B <_ [_ y / x ]_ B ) )
171 165 170 imbi12d 
 |-  ( 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 ) ) )
172 nfv 
 |-  F/ x ( ph /\ ( y e. S /\ k e. S ) /\ ( D <_ y /\ y <_ k /\ k <_ U ) )
173 nfcv 
 |-  F/_ x C
174 nfcv 
 |-  F/_ x <_
175 173 174 39 nfbr 
 |-  F/ x C <_ [_ y / x ]_ B
176 172 175 nfim 
 |-  F/ x ( ( ph /\ ( y e. S /\ k e. S ) /\ ( D <_ y /\ y <_ k /\ k <_ U ) ) -> C <_ [_ y / x ]_ B )
177 eleq1 
 |-  ( x = y -> ( x e. S <-> y e. S ) )
178 177 anbi1d 
 |-  ( x = y -> ( ( x e. S /\ k e. S ) <-> ( y e. S /\ k e. S ) ) )
179 breq2 
 |-  ( x = y -> ( D <_ x <-> D <_ y ) )
180 breq1 
 |-  ( x = y -> ( x <_ k <-> y <_ k ) )
181 179 180 3anbi12d 
 |-  ( x = y -> ( ( D <_ x /\ x <_ k /\ k <_ U ) <-> ( D <_ y /\ y <_ k /\ k <_ U ) ) )
182 178 181 3anbi23d 
 |-  ( 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 ) ) ) )
183 40 breq2d 
 |-  ( x = y -> ( C <_ B <-> C <_ [_ y / x ]_ B ) )
184 182 183 imbi12d 
 |-  ( 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 ) ) )
185 176 184 13 chvarfv 
 |-  ( ( ph /\ ( y e. S /\ k e. S ) /\ ( D <_ y /\ y <_ k /\ k <_ U ) ) -> C <_ [_ y / x ]_ B )
186 171 185 vtoclg 
 |-  ( Y e. S -> ( ( ph /\ ( y e. S /\ Y e. S ) /\ ( D <_ y /\ y <_ Y /\ Y <_ U ) ) -> [_ Y / x ]_ B <_ [_ y / x ]_ B ) )
187 159 186 mpcom 
 |-  ( ( ph /\ ( y e. S /\ Y e. S ) /\ ( D <_ y /\ y <_ Y /\ Y <_ U ) ) -> [_ Y / x ]_ B <_ [_ y / x ]_ B )
188 145 146 147 156 157 158 187 syl123anc 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> [_ Y / x ]_ B <_ [_ y / x ]_ B )
189 144 188 sylan2 
 |-  ( ( ph /\ y e. ( X (,) Y ) ) -> [_ Y / x ]_ B <_ [_ y / x ]_ B )
190 29 rexrd 
 |-  ( ph -> X e. RR* )
191 23 rexrd 
 |-  ( ph -> Y e. RR* )
192 lbicc2 
 |-  ( ( X e. RR* /\ Y e. RR* /\ X <_ Y ) -> X e. ( X [,] Y ) )
193 190 191 18 192 syl3anc 
 |-  ( ph -> X e. ( X [,] Y ) )
194 ubicc2 
 |-  ( ( X e. RR* /\ Y e. RR* /\ X <_ Y ) -> Y e. ( X [,] Y ) )
195 190 191 18 194 syl3anc 
 |-  ( ph -> Y e. ( X [,] Y ) )
196 oveq2 
 |-  ( y = X -> ( [_ Y / x ]_ B x. y ) = ( [_ Y / x ]_ B x. X ) )
197 oveq2 
 |-  ( y = Y -> ( [_ Y / x ]_ B x. y ) = ( [_ Y / x ]_ B x. Y ) )
198 29 23 99 118 136 143 189 193 195 18 196 62 197 46 dvle 
 |-  ( ph -> ( ( [_ Y / x ]_ B x. Y ) - ( [_ Y / x ]_ B x. X ) ) <_ ( [_ Y / x ]_ A - [_ X / x ]_ A ) )
199 81 198 eqbrtrd 
 |-  ( ph -> ( [_ Y / x ]_ B x. ( Y - X ) ) <_ ( [_ Y / x ]_ A - [_ X / x ]_ A ) )
200 77 55 64 199 lesubd 
 |-  ( ph -> [_ X / x ]_ A <_ ( [_ Y / x ]_ A - ( [_ Y / x ]_ B x. ( Y - X ) ) ) )
201 74 recnd 
 |-  ( ph -> ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) e. CC )
202 45 recnd 
 |-  ( ph -> ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) e. CC )
203 55 recnd 
 |-  ( ph -> [_ Y / x ]_ A e. CC )
204 201 202 203 subsubd 
 |-  ( 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 ) )
205 202 201 negsubdi2d 
 |-  ( 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 ) ) )
206 31 recnd 
 |-  ( ph -> ( |_ ` X ) e. CC )
207 79 80 206 nnncan2d 
 |-  ( ph -> ( ( Y - ( |_ ` X ) ) - ( X - ( |_ ` X ) ) ) = ( Y - X ) )
208 207 oveq1d 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - ( X - ( |_ ` X ) ) ) x. [_ Y / x ]_ B ) = ( ( Y - X ) x. [_ Y / x ]_ B ) )
209 32 recnd 
 |-  ( ph -> ( Y - ( |_ ` X ) ) e. CC )
210 57 recnd 
 |-  ( ph -> ( X - ( |_ ` X ) ) e. CC )
211 209 210 78 subdird 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - ( X - ( |_ ` X ) ) ) x. [_ Y / x ]_ B ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) ) )
212 76 recnd 
 |-  ( ph -> ( Y - X ) e. CC )
213 212 78 mulcomd 
 |-  ( ph -> ( ( Y - X ) x. [_ Y / x ]_ B ) = ( [_ Y / x ]_ B x. ( Y - X ) ) )
214 208 211 213 3eqtr3d 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) ) = ( [_ Y / x ]_ B x. ( Y - X ) ) )
215 214 negeqd 
 |-  ( ph -> -u ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) ) = -u ( [_ Y / x ]_ B x. ( Y - X ) ) )
216 205 215 eqtr3d 
 |-  ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) ) = -u ( [_ Y / x ]_ B x. ( Y - X ) ) )
217 216 oveq1d 
 |-  ( 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 ) )
218 77 recnd 
 |-  ( ph -> ( [_ Y / x ]_ B x. ( Y - X ) ) e. CC )
219 218 203 negsubdid 
 |-  ( ph -> -u ( ( [_ Y / x ]_ B x. ( Y - X ) ) - [_ Y / x ]_ A ) = ( -u ( [_ Y / x ]_ B x. ( Y - X ) ) + [_ Y / x ]_ A ) )
220 217 219 eqtr4d 
 |-  ( 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 ) )
221 218 203 negsubdi2d 
 |-  ( ph -> -u ( ( [_ Y / x ]_ B x. ( Y - X ) ) - [_ Y / x ]_ A ) = ( [_ Y / x ]_ A - ( [_ Y / x ]_ B x. ( Y - X ) ) ) )
222 204 220 221 3eqtrd 
 |-  ( 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 ) ) ) )
223 200 222 breqtrrd 
 |-  ( ph -> [_ X / x ]_ A <_ ( ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) ) )
224 64 74 56 223 lesubd 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) <_ ( ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ X / x ]_ A ) )
225 flle 
 |-  ( X e. RR -> ( |_ ` X ) <_ X )
226 29 225 syl 
 |-  ( ph -> ( |_ ` X ) <_ X )
227 29 31 subge0d 
 |-  ( ph -> ( 0 <_ ( X - ( |_ ` X ) ) <-> ( |_ ` X ) <_ X ) )
228 226 227 mpbird 
 |-  ( ph -> 0 <_ ( X - ( |_ ` X ) ) )
229 58 breq2d 
 |-  ( y = X -> ( [_ Y / x ]_ B <_ [_ y / x ]_ B <-> [_ Y / x ]_ B <_ [_ X / x ]_ B ) )
230 188 ralrimiva 
 |-  ( ph -> A. y e. ( X [,] Y ) [_ Y / x ]_ B <_ [_ y / x ]_ B )
231 229 230 193 rspcdva 
 |-  ( ph -> [_ Y / x ]_ B <_ [_ X / x ]_ B )
232 44 60 57 228 231 lemul2ad 
 |-  ( ph -> ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) <_ ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) )
233 74 61 64 232 lesub1dd 
 |-  ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ X / x ]_ A ) <_ ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) )
234 56 75 65 224 233 letrd 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) <_ ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) )
235 56 65 73 234 leadd1dd 
 |-  ( 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 ) )
236 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 dvfsumlem1 
 |-  ( ph -> ( H ` Y ) = ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) )
237 29 leidd 
 |-  ( ph -> X <_ X )
238 190 191 12 18 19 xrletrd 
 |-  ( ph -> X <_ U )
239 fllep1 
 |-  ( X e. RR -> X <_ ( ( |_ ` X ) + 1 ) )
240 29 239 syl 
 |-  ( ph -> X <_ ( ( |_ ` X ) + 1 ) )
241 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 15 17 237 238 240 dvfsumlem1 
 |-  ( ph -> ( H ` X ) = ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) )
242 235 236 241 3brtr4d 
 |-  ( ph -> ( H ` Y ) <_ ( H ` X ) )
243 65 60 resubcld 
 |-  ( ph -> ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) - [_ X / x ]_ B ) e. RR )
244 56 44 resubcld 
 |-  ( ph -> ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) - [_ Y / x ]_ B ) e. RR )
245 peano2rem 
 |-  ( ( X - ( |_ ` X ) ) e. RR -> ( ( X - ( |_ ` X ) ) - 1 ) e. RR )
246 57 245 syl 
 |-  ( ph -> ( ( X - ( |_ ` X ) ) - 1 ) e. RR )
247 246 60 remulcld 
 |-  ( ph -> ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) e. RR )
248 247 64 resubcld 
 |-  ( ph -> ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) e. RR )
249 peano2rem 
 |-  ( ( Y - ( |_ ` X ) ) e. RR -> ( ( Y - ( |_ ` X ) ) - 1 ) e. RR )
250 32 249 syl 
 |-  ( ph -> ( ( Y - ( |_ ` X ) ) - 1 ) e. RR )
251 250 60 remulcld 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) e. RR )
252 251 55 resubcld 
 |-  ( ph -> ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ Y / x ]_ A ) e. RR )
253 250 44 remulcld 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) e. RR )
254 253 55 resubcld 
 |-  ( ph -> ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) e. RR )
255 247 recnd 
 |-  ( ph -> ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) e. CC )
256 251 recnd 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) e. CC )
257 255 256 subcld 
 |-  ( ph -> ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) ) e. CC )
258 257 203 addcomd 
 |-  ( 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 ) ) ) )
259 255 256 203 subsubd 
 |-  ( 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 ) )
260 203 256 255 subsub2d 
 |-  ( 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 ) ) ) )
261 258 259 260 3eqtr4d 
 |-  ( 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 ) ) ) )
262 1cnd 
 |-  ( ph -> 1 e. CC )
263 209 210 262 nnncan2d 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) - ( ( X - ( |_ ` X ) ) - 1 ) ) = ( ( Y - ( |_ ` X ) ) - ( X - ( |_ ` X ) ) ) )
264 263 207 eqtrd 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) - ( ( X - ( |_ ` X ) ) - 1 ) ) = ( Y - X ) )
265 264 oveq1d 
 |-  ( ph -> ( ( ( ( Y - ( |_ ` X ) ) - 1 ) - ( ( X - ( |_ ` X ) ) - 1 ) ) x. [_ X / x ]_ B ) = ( ( Y - X ) x. [_ X / x ]_ B ) )
266 250 recnd 
 |-  ( ph -> ( ( Y - ( |_ ` X ) ) - 1 ) e. CC )
267 246 recnd 
 |-  ( ph -> ( ( X - ( |_ ` X ) ) - 1 ) e. CC )
268 60 recnd 
 |-  ( ph -> [_ X / x ]_ B e. CC )
269 266 267 268 subdird 
 |-  ( 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 ) ) )
270 212 268 mulcomd 
 |-  ( ph -> ( ( Y - X ) x. [_ X / x ]_ B ) = ( [_ X / x ]_ B x. ( Y - X ) ) )
271 265 269 270 3eqtr3d 
 |-  ( ph -> ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) ) = ( [_ X / x ]_ B x. ( Y - X ) ) )
272 271 oveq2d 
 |-  ( 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 ) ) ) )
273 261 272 eqtrd 
 |-  ( 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 ) ) ) )
274 60 76 remulcld 
 |-  ( ph -> ( [_ X / x ]_ B x. ( Y - X ) ) e. RR )
275 cncfmptc 
 |-  ( ( [_ X / x ]_ B e. RR /\ ( X [,] Y ) C_ CC /\ RR C_ CC ) -> ( y e. ( X [,] Y ) |-> [_ X / x ]_ B ) e. ( ( X [,] Y ) -cn-> RR ) )
276 60 92 93 275 syl3anc 
 |-  ( ph -> ( y e. ( X [,] Y ) |-> [_ X / x ]_ B ) e. ( ( X [,] Y ) -cn-> RR ) )
277 remulcl 
 |-  ( ( [_ X / x ]_ B e. RR /\ y e. RR ) -> ( [_ X / x ]_ B x. y ) e. RR )
278 82 83 276 97 91 277 cncfmpt2ss 
 |-  ( ph -> ( y e. ( X [,] Y ) |-> ( [_ X / x ]_ B x. y ) ) e. ( ( X [,] Y ) -cn-> RR ) )
279 101 105 106 114 268 dvmptcmul 
 |-  ( ph -> ( RR _D ( y e. ( X (,) Y ) |-> ( [_ X / x ]_ B x. y ) ) ) = ( y e. ( X (,) Y ) |-> ( [_ X / x ]_ B x. 1 ) ) )
280 268 mulid1d 
 |-  ( ph -> ( [_ X / x ]_ B x. 1 ) = [_ X / x ]_ B )
281 280 mpteq2dv 
 |-  ( ph -> ( y e. ( X (,) Y ) |-> ( [_ X / x ]_ B x. 1 ) ) = ( y e. ( X (,) Y ) |-> [_ X / x ]_ B ) )
282 279 281 eqtrd 
 |-  ( ph -> ( RR _D ( y e. ( X (,) Y ) |-> ( [_ X / x ]_ B x. y ) ) ) = ( y e. ( X (,) Y ) |-> [_ X / x ]_ B ) )
283 15 adantr 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> X e. S )
284 153 rexrd 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> y e. RR* )
285 191 adantr 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> Y e. RR* )
286 12 adantr 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> U e. RR* )
287 284 285 286 157 158 xrletrd 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> y <_ U )
288 vex 
 |-  y e. _V
289 eleq1 
 |-  ( k = y -> ( k e. S <-> y e. S ) )
290 289 anbi2d 
 |-  ( k = y -> ( ( X e. S /\ k e. S ) <-> ( X e. S /\ y e. S ) ) )
291 breq2 
 |-  ( k = y -> ( X <_ k <-> X <_ y ) )
292 breq1 
 |-  ( k = y -> ( k <_ U <-> y <_ U ) )
293 291 292 3anbi23d 
 |-  ( k = y -> ( ( D <_ X /\ X <_ k /\ k <_ U ) <-> ( D <_ X /\ X <_ y /\ y <_ U ) ) )
294 290 293 3anbi23d 
 |-  ( 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 ) ) ) )
295 csbeq1 
 |-  ( k = y -> [_ k / x ]_ B = [_ y / x ]_ B )
296 167 295 eqtr3id 
 |-  ( k = y -> C = [_ y / x ]_ B )
297 296 breq1d 
 |-  ( k = y -> ( C <_ [_ X / x ]_ B <-> [_ y / x ]_ B <_ [_ X / x ]_ B ) )
298 294 297 imbi12d 
 |-  ( 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 ) ) )
299 simp2l 
 |-  ( ( ph /\ ( X e. S /\ k e. S ) /\ ( D <_ X /\ X <_ k /\ k <_ U ) ) -> X e. S )
300 nfv 
 |-  F/ x ( ph /\ ( X e. S /\ k e. S ) /\ ( D <_ X /\ X <_ k /\ k <_ U ) )
301 nfcsb1v 
 |-  F/_ x [_ X / x ]_ B
302 173 174 301 nfbr 
 |-  F/ x C <_ [_ X / x ]_ B
303 300 302 nfim 
 |-  F/ x ( ( ph /\ ( X e. S /\ k e. S ) /\ ( D <_ X /\ X <_ k /\ k <_ U ) ) -> C <_ [_ X / x ]_ B )
304 eleq1 
 |-  ( x = X -> ( x e. S <-> X e. S ) )
305 304 anbi1d 
 |-  ( x = X -> ( ( x e. S /\ k e. S ) <-> ( X e. S /\ k e. S ) ) )
306 breq2 
 |-  ( x = X -> ( D <_ x <-> D <_ X ) )
307 breq1 
 |-  ( x = X -> ( x <_ k <-> X <_ k ) )
308 306 307 3anbi12d 
 |-  ( x = X -> ( ( D <_ x /\ x <_ k /\ k <_ U ) <-> ( D <_ X /\ X <_ k /\ k <_ U ) ) )
309 305 308 3anbi23d 
 |-  ( 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 ) ) ) )
310 csbeq1a 
 |-  ( x = X -> B = [_ X / x ]_ B )
311 310 breq2d 
 |-  ( x = X -> ( C <_ B <-> C <_ [_ X / x ]_ B ) )
312 309 311 imbi12d 
 |-  ( 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 ) ) )
313 303 312 13 vtoclg1f 
 |-  ( X e. S -> ( ( ph /\ ( X e. S /\ k e. S ) /\ ( D <_ X /\ X <_ k /\ k <_ U ) ) -> C <_ [_ X / x ]_ B ) )
314 299 313 mpcom 
 |-  ( ( ph /\ ( X e. S /\ k e. S ) /\ ( D <_ X /\ X <_ k /\ k <_ U ) ) -> C <_ [_ X / x ]_ B )
315 288 298 314 vtocl 
 |-  ( ( ph /\ ( X e. S /\ y e. S ) /\ ( D <_ X /\ X <_ y /\ y <_ U ) ) -> [_ y / x ]_ B <_ [_ X / x ]_ B )
316 145 283 146 154 155 287 315 syl123anc 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> [_ y / x ]_ B <_ [_ X / x ]_ B )
317 144 316 sylan2 
 |-  ( ( ph /\ y e. ( X (,) Y ) ) -> [_ y / x ]_ B <_ [_ X / x ]_ B )
318 oveq2 
 |-  ( y = X -> ( [_ X / x ]_ B x. y ) = ( [_ X / x ]_ B x. X ) )
319 oveq2 
 |-  ( y = Y -> ( [_ X / x ]_ B x. y ) = ( [_ X / x ]_ B x. Y ) )
320 29 23 136 143 278 282 317 193 195 18 62 318 46 319 dvle 
 |-  ( ph -> ( [_ Y / x ]_ A - [_ X / x ]_ A ) <_ ( ( [_ X / x ]_ B x. Y ) - ( [_ X / x ]_ B x. X ) ) )
321 268 79 80 subdid 
 |-  ( ph -> ( [_ X / x ]_ B x. ( Y - X ) ) = ( ( [_ X / x ]_ B x. Y ) - ( [_ X / x ]_ B x. X ) ) )
322 320 321 breqtrrd 
 |-  ( ph -> ( [_ Y / x ]_ A - [_ X / x ]_ A ) <_ ( [_ X / x ]_ B x. ( Y - X ) ) )
323 55 64 274 322 subled 
 |-  ( ph -> ( [_ Y / x ]_ A - ( [_ X / x ]_ B x. ( Y - X ) ) ) <_ [_ X / x ]_ A )
324 273 323 eqbrtrd 
 |-  ( ph -> ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ Y / x ]_ A ) ) <_ [_ X / x ]_ A )
325 247 252 64 324 subled 
 |-  ( ph -> ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) <_ ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ Y / x ]_ A ) )
326 250 renegcld 
 |-  ( ph -> -u ( ( Y - ( |_ ` X ) ) - 1 ) e. RR )
327 1red 
 |-  ( ph -> 1 e. RR )
328 23 31 327 lesubadd2d 
 |-  ( ph -> ( ( Y - ( |_ ` X ) ) <_ 1 <-> Y <_ ( ( |_ ` X ) + 1 ) ) )
329 20 328 mpbird 
 |-  ( ph -> ( Y - ( |_ ` X ) ) <_ 1 )
330 32 327 suble0d 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) <_ 0 <-> ( Y - ( |_ ` X ) ) <_ 1 ) )
331 329 330 mpbird 
 |-  ( ph -> ( ( Y - ( |_ ` X ) ) - 1 ) <_ 0 )
332 250 le0neg1d 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) <_ 0 <-> 0 <_ -u ( ( Y - ( |_ ` X ) ) - 1 ) ) )
333 331 332 mpbid 
 |-  ( ph -> 0 <_ -u ( ( Y - ( |_ ` X ) ) - 1 ) )
334 44 60 326 333 231 lemul2ad 
 |-  ( ph -> ( -u ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) <_ ( -u ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) )
335 266 78 mulneg1d 
 |-  ( ph -> ( -u ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) = -u ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) )
336 266 268 mulneg1d 
 |-  ( ph -> ( -u ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) = -u ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) )
337 334 335 336 3brtr3d 
 |-  ( ph -> -u ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) <_ -u ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) )
338 251 253 lenegd 
 |-  ( 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 ) ) )
339 337 338 mpbird 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) <_ ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) )
340 251 253 55 339 lesub1dd 
 |-  ( ph -> ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ Y / x ]_ A ) <_ ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) )
341 248 252 254 325 340 letrd 
 |-  ( ph -> ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) <_ ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) )
342 210 262 268 subdird 
 |-  ( ph -> ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) = ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - ( 1 x. [_ X / x ]_ B ) ) )
343 268 mulid2d 
 |-  ( ph -> ( 1 x. [_ X / x ]_ B ) = [_ X / x ]_ B )
344 343 oveq2d 
 |-  ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - ( 1 x. [_ X / x ]_ B ) ) = ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ B ) )
345 342 344 eqtrd 
 |-  ( ph -> ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) = ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ B ) )
346 345 oveq1d 
 |-  ( ph -> ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) = ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ B ) - [_ X / x ]_ A ) )
347 209 262 78 subdird 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( 1 x. [_ Y / x ]_ B ) ) )
348 78 mulid2d 
 |-  ( ph -> ( 1 x. [_ Y / x ]_ B ) = [_ Y / x ]_ B )
349 348 oveq2d 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( 1 x. [_ Y / x ]_ B ) ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ B ) )
350 347 349 eqtrd 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ B ) )
351 350 oveq1d 
 |-  ( ph -> ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) = ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ B ) - [_ Y / x ]_ A ) )
352 341 346 351 3brtr3d 
 |-  ( 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 ) )
353 61 recnd 
 |-  ( ph -> ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) e. CC )
354 64 recnd 
 |-  ( ph -> [_ X / x ]_ A e. CC )
355 353 354 268 sub32d 
 |-  ( 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 ) )
356 202 203 78 sub32d 
 |-  ( 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 ) )
357 352 355 356 3brtr4d 
 |-  ( 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 ) )
358 243 244 73 357 leadd1dd 
 |-  ( 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 ) )
359 65 recnd 
 |-  ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) e. CC )
360 73 recnd 
 |-  ( ph -> sum_ k e. ( M ... ( |_ ` X ) ) C e. CC )
361 359 360 268 addsubd 
 |-  ( 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 ) )
362 56 recnd 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) e. CC )
363 362 360 78 addsubd 
 |-  ( 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 ) )
364 358 361 363 3brtr4d 
 |-  ( 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 ) )
365 241 oveq1d 
 |-  ( ph -> ( ( H ` X ) - [_ X / x ]_ B ) = ( ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) - [_ X / x ]_ B ) )
366 236 oveq1d 
 |-  ( ph -> ( ( H ` Y ) - [_ Y / x ]_ B ) = ( ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) - [_ Y / x ]_ B ) )
367 364 365 366 3brtr4d 
 |-  ( ph -> ( ( H ` X ) - [_ X / x ]_ B ) <_ ( ( H ` Y ) - [_ Y / x ]_ B ) )
368 242 367 jca 
 |-  ( ph -> ( ( H ` Y ) <_ ( H ` X ) /\ ( ( H ` X ) - [_ X / x ]_ B ) <_ ( ( H ` Y ) - [_ Y / x ]_ B ) ) )