Metamath Proof Explorer

Theorem dvfsumlem2

Description: Lemma for dvfsumrlim . (Contributed by Mario Carneiro, 17-May-2016) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

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 mpomulcn 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
84 csbeq1 
 |-  ( z = Y -> [_ z / x ]_ B = [_ Y / x ]_ B )
85 84 eleq1d 
 |-  ( z = Y -> ( [_ z / x ]_ B e. RR <-> [_ Y / x ]_ B e. RR ) )
86 nfcv 
 |-  F/_ z B
87 nfcsb1v 
 |-  F/_ x [_ z / x ]_ B
88 csbeq1a 
 |-  ( x = z -> B = [_ z / x ]_ B )
89 86 87 88 cbvmpt 
 |-  ( x e. S |-> B ) = ( z e. S |-> [_ z / x ]_ B )
90 89 fmpt 
 |-  ( A. z e. S [_ z / x ]_ B e. RR <-> ( x e. S |-> B ) : S --> RR )
91 37 90 sylibr 
 |-  ( ph -> A. z e. S [_ z / x ]_ B e. RR )
92 85 91 16 rspcdva 
 |-  ( ph -> [_ Y / x ]_ B e. RR )
93 pnfxr 
 |-  +oo e. RR*
94 93 a1i 
 |-  ( ph -> +oo e. RR* )
95 28 simprd 
 |-  ( ph -> T < X )
96 23 ltpnfd 
 |-  ( ph -> Y < +oo )
97 iccssioo 
 |-  ( ( ( T e. RR* /\ +oo e. RR* ) /\ ( T < X /\ Y < +oo ) ) -> ( X [,] Y ) C_ ( T (,) +oo ) )
98 25 94 95 96 97 syl22anc 
 |-  ( ph -> ( X [,] Y ) C_ ( T (,) +oo ) )
99 98 21 sstrdi 
 |-  ( ph -> ( X [,] Y ) C_ RR )
100 ax-resscn 
 |-  RR C_ CC
101 99 100 sstrdi 
 |-  ( ph -> ( X [,] Y ) C_ CC )
102 100 a1i 
 |-  ( ph -> RR C_ CC )
103 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 ) )
104 92 101 102 103 syl3anc 
 |-  ( ph -> ( y e. ( X [,] Y ) |-> [_ Y / x ]_ B ) e. ( ( X [,] Y ) -cn-> RR ) )
105 cncfmptid 
 |-  ( ( ( X [,] Y ) C_ RR /\ RR C_ CC ) -> ( y e. ( X [,] Y ) |-> y ) e. ( ( X [,] Y ) -cn-> RR ) )
106 99 100 105 sylancl 
 |-  ( ph -> ( y e. ( X [,] Y ) |-> y ) e. ( ( X [,] Y ) -cn-> RR ) )
107 remulcl 
 |-  ( ( [_ Y / x ]_ B e. RR /\ y e. RR ) -> ( [_ Y / x ]_ B x. y ) e. RR )
108 simpl 
 |-  ( ( [_ Y / x ]_ B e. RR /\ y e. RR ) -> [_ Y / x ]_ B e. RR )
109 108 recnd 
 |-  ( ( [_ Y / x ]_ B e. RR /\ y e. RR ) -> [_ Y / x ]_ B e. CC )
110 simpr 
 |-  ( ( [_ Y / x ]_ B e. RR /\ y e. RR ) -> y e. RR )
111 110 recnd 
 |-  ( ( [_ Y / x ]_ B e. RR /\ y e. RR ) -> y e. CC )
112 109 111 jca 
 |-  ( ( [_ Y / x ]_ B e. RR /\ y e. RR ) -> ( [_ Y / x ]_ B e. CC /\ y e. CC ) )
113 ovmpot 
 |-  ( ( [_ Y / x ]_ B e. CC /\ y e. CC ) -> ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) = ( [_ Y / x ]_ B x. y ) )
114 113 eqcomd 
 |-  ( ( [_ Y / x ]_ B e. CC /\ y e. CC ) -> ( [_ Y / x ]_ B x. y ) = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) )
115 112 114 syl 
 |-  ( ( [_ Y / x ]_ B e. RR /\ y e. RR ) -> ( [_ Y / x ]_ B x. y ) = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) )
116 115 eleq1d 
 |-  ( ( [_ Y / x ]_ B e. RR /\ y e. RR ) -> ( ( [_ Y / x ]_ B x. y ) e. RR <-> ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) e. RR ) )
117 116 biimpd 
 |-  ( ( [_ Y / x ]_ B e. RR /\ y e. RR ) -> ( ( [_ Y / x ]_ B x. y ) e. RR -> ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) e. RR ) )
118 107 117 mpd 
 |-  ( ( [_ Y / x ]_ B e. RR /\ y e. RR ) -> ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) e. RR )
119 82 83 104 106 100 118 cncfmpt2ss 
 |-  ( ph -> ( y e. ( X [,] Y ) |-> ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) e. ( ( X [,] Y ) -cn-> RR ) )
120 df-mpt 
 |-  ( y e. ( X [,] Y ) |-> ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) = { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) }
121 120 eleq1i 
 |-  ( ( y e. ( X [,] Y ) |-> ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) e. ( ( X [,] Y ) -cn-> RR ) <-> { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } e. ( ( X [,] Y ) -cn-> RR ) )
122 121 biimpi 
 |-  ( ( y e. ( X [,] Y ) |-> ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) e. ( ( X [,] Y ) -cn-> RR ) -> { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } e. ( ( X [,] Y ) -cn-> RR ) )
123 119 122 syl 
 |-  ( ph -> { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } e. ( ( X [,] Y ) -cn-> RR ) )
124 idd 
 |-  ( ph -> ( y e. ( X [,] Y ) -> y e. ( X [,] Y ) ) )
125 124 a1dd 
 |-  ( ph -> ( y e. ( X [,] Y ) -> ( w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) -> y e. ( X [,] Y ) ) ) )
126 125 impd 
 |-  ( ph -> ( ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) -> y e. ( X [,] Y ) ) )
127 csbeq1 
 |-  ( m = Y -> [_ m / x ]_ B = [_ Y / x ]_ B )
128 127 eleq1d 
 |-  ( m = Y -> ( [_ m / x ]_ B e. RR <-> [_ Y / x ]_ B e. RR ) )
129 nfcv 
 |-  F/_ m B
130 nfcsb1v 
 |-  F/_ x [_ m / x ]_ B
131 csbeq1a 
 |-  ( x = m -> B = [_ m / x ]_ B )
132 129 130 131 cbvmpt 
 |-  ( x e. S |-> B ) = ( m e. S |-> [_ m / x ]_ B )
133 132 fmpt 
 |-  ( A. m e. S [_ m / x ]_ B e. RR <-> ( x e. S |-> B ) : S --> RR )
134 37 133 sylibr 
 |-  ( ph -> A. m e. S [_ m / x ]_ B e. RR )
135 128 134 16 rspcdva 
 |-  ( ph -> [_ Y / x ]_ B e. RR )
136 135 recnd 
 |-  ( ph -> [_ Y / x ]_ B e. CC )
137 136 adantr 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> [_ Y / x ]_ B e. CC )
138 elicc2 
 |-  ( ( X e. RR /\ Y e. RR ) -> ( y e. ( X [,] Y ) <-> ( y e. RR /\ X <_ y /\ y <_ Y ) ) )
139 29 23 138 syl2anc 
 |-  ( ph -> ( y e. ( X [,] Y ) <-> ( y e. RR /\ X <_ y /\ y <_ Y ) ) )
140 139 biimpa 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> ( y e. RR /\ X <_ y /\ y <_ Y ) )
141 140 simp1d 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> y e. RR )
142 141 recnd 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> y e. CC )
143 137 142 jca 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> ( [_ Y / x ]_ B e. CC /\ y e. CC ) )
144 143 113 syl 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) = ( [_ Y / x ]_ B x. y ) )
145 144 eqeq2d 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> ( w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) <-> w = ( [_ Y / x ]_ B x. y ) ) )
146 145 biimpd 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> ( w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) -> w = ( [_ Y / x ]_ B x. y ) ) )
147 146 ex 
 |-  ( ph -> ( y e. ( X [,] Y ) -> ( w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) -> w = ( [_ Y / x ]_ B x. y ) ) ) )
148 147 impd 
 |-  ( ph -> ( ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) -> w = ( [_ Y / x ]_ B x. y ) ) )
149 126 148 jcad 
 |-  ( ph -> ( ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) -> ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B x. y ) ) ) )
150 124 a1dd 
 |-  ( ph -> ( y e. ( X [,] Y ) -> ( w = ( [_ Y / x ]_ B x. y ) -> y e. ( X [,] Y ) ) ) )
151 150 impd 
 |-  ( ph -> ( ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B x. y ) ) -> y e. ( X [,] Y ) ) )
152 csbeq1 
 |-  ( k = Y -> [_ k / x ]_ B = [_ Y / x ]_ B )
153 152 eleq1d 
 |-  ( k = Y -> ( [_ k / x ]_ B e. RR <-> [_ Y / x ]_ B e. RR ) )
154 nfcv 
 |-  F/_ k B
155 nfcsb1v 
 |-  F/_ x [_ k / x ]_ B
156 csbeq1a 
 |-  ( x = k -> B = [_ k / x ]_ B )
157 154 155 156 cbvmpt 
 |-  ( x e. S |-> B ) = ( k e. S |-> [_ k / x ]_ B )
158 157 fmpt 
 |-  ( A. k e. S [_ k / x ]_ B e. RR <-> ( x e. S |-> B ) : S --> RR )
159 37 158 sylibr 
 |-  ( ph -> A. k e. S [_ k / x ]_ B e. RR )
160 153 159 16 rspcdva 
 |-  ( ph -> [_ Y / x ]_ B e. RR )
161 160 recnd 
 |-  ( ph -> [_ Y / x ]_ B e. CC )
162 161 adantr 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> [_ Y / x ]_ B e. CC )
163 162 142 jca 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> ( [_ Y / x ]_ B e. CC /\ y e. CC ) )
164 163 114 syl 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> ( [_ Y / x ]_ B x. y ) = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) )
165 164 eqeq2d 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> ( w = ( [_ Y / x ]_ B x. y ) <-> w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) )
166 165 biimpd 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> ( w = ( [_ Y / x ]_ B x. y ) -> w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) )
167 166 ex 
 |-  ( ph -> ( y e. ( X [,] Y ) -> ( w = ( [_ Y / x ]_ B x. y ) -> w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) ) )
168 167 impd 
 |-  ( ph -> ( ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B x. y ) ) -> w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) )
169 151 168 jcad 
 |-  ( ph -> ( ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B x. y ) ) -> ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) ) )
170 149 169 impbid 
 |-  ( ph -> ( ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) <-> ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B x. y ) ) ) )
171 170 opabbidv 
 |-  ( ph -> { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } = { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B x. y ) ) } )
172 df-mpt 
 |-  ( y e. ( X [,] Y ) |-> ( [_ Y / x ]_ B x. y ) ) = { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B x. y ) ) }
173 172 eqcomi 
 |-  { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B x. y ) ) } = ( y e. ( X [,] Y ) |-> ( [_ Y / x ]_ B x. y ) )
174 173 eqeq2i 
 |-  ( { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } = { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B x. y ) ) } <-> { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } = ( y e. ( X [,] Y ) |-> ( [_ Y / x ]_ B x. y ) ) )
175 174 biimpi 
 |-  ( { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } = { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B x. y ) ) } -> { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } = ( y e. ( X [,] Y ) |-> ( [_ Y / x ]_ B x. y ) ) )
176 171 175 syl 
 |-  ( ph -> { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } = ( y e. ( X [,] Y ) |-> ( [_ Y / x ]_ B x. y ) ) )
177 176 eleq1d 
 |-  ( ph -> ( { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } e. ( ( X [,] Y ) -cn-> RR ) <-> ( y e. ( X [,] Y ) |-> ( [_ Y / x ]_ B x. y ) ) e. ( ( X [,] Y ) -cn-> RR ) ) )
178 177 biimpd 
 |-  ( ph -> ( { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ Y / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } e. ( ( X [,] Y ) -cn-> RR ) -> ( y e. ( X [,] Y ) |-> ( [_ Y / x ]_ B x. y ) ) e. ( ( X [,] Y ) -cn-> RR ) ) )
179 123 178 mpd 
 |-  ( ph -> ( y e. ( X [,] Y ) |-> ( [_ Y / x ]_ B x. y ) ) e. ( ( X [,] Y ) -cn-> RR ) )
180 reelprrecn 
 |-  RR e. { RR , CC }
181 180 a1i 
 |-  ( ph -> RR e. { RR , CC } )
182 ioossicc 
 |-  ( X (,) Y ) C_ ( X [,] Y )
183 182 99 sstrid 
 |-  ( ph -> ( X (,) Y ) C_ RR )
184 183 sselda 
 |-  ( ( ph /\ y e. ( X (,) Y ) ) -> y e. RR )
185 184 recnd 
 |-  ( ( ph /\ y e. ( X (,) Y ) ) -> y e. CC )
186 1cnd 
 |-  ( ( ph /\ y e. ( X (,) Y ) ) -> 1 e. CC )
187 simpr 
 |-  ( ( ph /\ y e. RR ) -> y e. RR )
188 187 recnd 
 |-  ( ( ph /\ y e. RR ) -> y e. CC )
189 1cnd 
 |-  ( ( ph /\ y e. RR ) -> 1 e. CC )
190 181 dvmptid 
 |-  ( ph -> ( RR _D ( y e. RR |-> y ) ) = ( y e. RR |-> 1 ) )
191 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
192 iooretop 
 |-  ( X (,) Y ) e. ( topGen ` ran (,) )
193 192 a1i 
 |-  ( ph -> ( X (,) Y ) e. ( topGen ` ran (,) ) )
194 181 188 189 190 183 191 82 193 dvmptres 
 |-  ( ph -> ( RR _D ( y e. ( X (,) Y ) |-> y ) ) = ( y e. ( X (,) Y ) |-> 1 ) )
195 181 185 186 194 78 dvmptcmul 
 |-  ( ph -> ( RR _D ( y e. ( X (,) Y ) |-> ( [_ Y / x ]_ B x. y ) ) ) = ( y e. ( X (,) Y ) |-> ( [_ Y / x ]_ B x. 1 ) ) )
196 78 mulridd 
 |-  ( ph -> ( [_ Y / x ]_ B x. 1 ) = [_ Y / x ]_ B )
197 196 mpteq2dv 
 |-  ( ph -> ( y e. ( X (,) Y ) |-> ( [_ Y / x ]_ B x. 1 ) ) = ( y e. ( X (,) Y ) |-> [_ Y / x ]_ B ) )
198 195 197 eqtrd 
 |-  ( ph -> ( RR _D ( y e. ( X (,) Y ) |-> ( [_ Y / x ]_ B x. y ) ) ) = ( y e. ( X (,) Y ) |-> [_ Y / x ]_ B ) )
199 98 1 sseqtrrdi 
 |-  ( ph -> ( X [,] Y ) C_ S )
200 199 resmptd 
 |-  ( ph -> ( ( y e. S |-> [_ y / x ]_ A ) |` ( X [,] Y ) ) = ( y e. ( X [,] Y ) |-> [_ y / x ]_ A ) )
201 7 recnd 
 |-  ( ( ph /\ x e. S ) -> A e. CC )
202 201 fmpttd 
 |-  ( ph -> ( x e. S |-> A ) : S --> CC )
203 10 dmeqd 
 |-  ( ph -> dom ( RR _D ( x e. S |-> A ) ) = dom ( x e. S |-> B ) )
204 8 ralrimiva 
 |-  ( ph -> A. x e. S B e. V )
205 dmmptg 
 |-  ( A. x e. S B e. V -> dom ( x e. S |-> B ) = S )
206 204 205 syl 
 |-  ( ph -> dom ( x e. S |-> B ) = S )
207 203 206 eqtrd 
 |-  ( ph -> dom ( RR _D ( x e. S |-> A ) ) = S )
208 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 ) )
209 102 202 35 207 208 syl31anc 
 |-  ( ph -> ( x e. S |-> A ) e. ( S -cn-> CC ) )
210 cncfcdm 
 |-  ( ( 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 ) )
211 100 209 210 sylancr 
 |-  ( ph -> ( ( x e. S |-> A ) e. ( S -cn-> RR ) <-> ( x e. S |-> A ) : S --> RR ) )
212 48 211 mpbird 
 |-  ( ph -> ( x e. S |-> A ) e. ( S -cn-> RR ) )
213 52 212 eqeltrrid 
 |-  ( ph -> ( y e. S |-> [_ y / x ]_ A ) e. ( S -cn-> RR ) )
214 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 ) ) )
215 199 213 214 sylc 
 |-  ( ph -> ( ( y e. S |-> [_ y / x ]_ A ) |` ( X [,] Y ) ) e. ( ( X [,] Y ) -cn-> RR ) )
216 200 215 eqeltrrd 
 |-  ( ph -> ( y e. ( X [,] Y ) |-> [_ y / x ]_ A ) e. ( ( X [,] Y ) -cn-> RR ) )
217 54 r19.21bi 
 |-  ( ( ph /\ y e. S ) -> [_ y / x ]_ A e. RR )
218 217 recnd 
 |-  ( ( ph /\ y e. S ) -> [_ y / x ]_ A e. CC )
219 43 r19.21bi 
 |-  ( ( ph /\ y e. S ) -> [_ y / x ]_ B e. RR )
220 52 oveq2i 
 |-  ( RR _D ( x e. S |-> A ) ) = ( RR _D ( y e. S |-> [_ y / x ]_ A ) )
221 10 220 41 3eqtr3g 
 |-  ( ph -> ( RR _D ( y e. S |-> [_ y / x ]_ A ) ) = ( y e. S |-> [_ y / x ]_ B ) )
222 182 199 sstrid 
 |-  ( ph -> ( X (,) Y ) C_ S )
223 181 218 219 221 222 191 82 193 dvmptres 
 |-  ( ph -> ( RR _D ( y e. ( X (,) Y ) |-> [_ y / x ]_ A ) ) = ( y e. ( X (,) Y ) |-> [_ y / x ]_ B ) )
224 182 sseli 
 |-  ( y e. ( X (,) Y ) -> y e. ( X [,] Y ) )
225 simpl 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> ph )
226 199 sselda 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> y e. S )
227 16 adantr 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> Y e. S )
228 4 adantr 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> D e. RR )
229 29 adantr 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> X e. RR )
230 17 adantr 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> D <_ X )
231 140 simp2d 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> X <_ y )
232 228 229 141 230 231 letrd 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> D <_ y )
233 140 simp3d 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> y <_ Y )
234 19 adantr 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> Y <_ U )
235 simp2r 
 |-  ( ( ph /\ ( y e. S /\ Y e. S ) /\ ( D <_ y /\ y <_ Y /\ Y <_ U ) ) -> Y e. S )
236 eleq1 
 |-  ( k = Y -> ( k e. S <-> Y e. S ) )
237 236 anbi2d 
 |-  ( k = Y -> ( ( y e. S /\ k e. S ) <-> ( y e. S /\ Y e. S ) ) )
238 breq2 
 |-  ( k = Y -> ( y <_ k <-> y <_ Y ) )
239 breq1 
 |-  ( k = Y -> ( k <_ U <-> Y <_ U ) )
240 238 239 3anbi23d 
 |-  ( k = Y -> ( ( D <_ y /\ y <_ k /\ k <_ U ) <-> ( D <_ y /\ y <_ Y /\ Y <_ U ) ) )
241 237 240 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 ) ) ) )
242 vex 
 |-  k e. _V
243 242 11 csbie 
 |-  [_ k / x ]_ B = C
244 243 152 eqtr3id 
 |-  ( k = Y -> C = [_ Y / x ]_ B )
245 244 breq1d 
 |-  ( k = Y -> ( C <_ [_ y / x ]_ B <-> [_ Y / x ]_ B <_ [_ y / x ]_ B ) )
246 241 245 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 ) ) )
247 nfv 
 |-  F/ x ( ph /\ ( y e. S /\ k e. S ) /\ ( D <_ y /\ y <_ k /\ k <_ U ) )
248 nfcv 
 |-  F/_ x C
249 nfcv 
 |-  F/_ x <_
250 248 249 39 nfbr 
 |-  F/ x C <_ [_ y / x ]_ B
251 247 250 nfim 
 |-  F/ x ( ( ph /\ ( y e. S /\ k e. S ) /\ ( D <_ y /\ y <_ k /\ k <_ U ) ) -> C <_ [_ y / x ]_ B )
252 eleq1 
 |-  ( x = y -> ( x e. S <-> y e. S ) )
253 252 anbi1d 
 |-  ( x = y -> ( ( x e. S /\ k e. S ) <-> ( y e. S /\ k e. S ) ) )
254 breq2 
 |-  ( x = y -> ( D <_ x <-> D <_ y ) )
255 breq1 
 |-  ( x = y -> ( x <_ k <-> y <_ k ) )
256 254 255 3anbi12d 
 |-  ( x = y -> ( ( D <_ x /\ x <_ k /\ k <_ U ) <-> ( D <_ y /\ y <_ k /\ k <_ U ) ) )
257 253 256 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 ) ) ) )
258 40 breq2d 
 |-  ( x = y -> ( C <_ B <-> C <_ [_ y / x ]_ B ) )
259 257 258 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 ) ) )
260 251 259 13 chvarfv 
 |-  ( ( ph /\ ( y e. S /\ k e. S ) /\ ( D <_ y /\ y <_ k /\ k <_ U ) ) -> C <_ [_ y / x ]_ B )
261 246 260 vtoclg 
 |-  ( Y e. S -> ( ( ph /\ ( y e. S /\ Y e. S ) /\ ( D <_ y /\ y <_ Y /\ Y <_ U ) ) -> [_ Y / x ]_ B <_ [_ y / x ]_ B ) )
262 235 261 mpcom 
 |-  ( ( ph /\ ( y e. S /\ Y e. S ) /\ ( D <_ y /\ y <_ Y /\ Y <_ U ) ) -> [_ Y / x ]_ B <_ [_ y / x ]_ B )
263 225 226 227 232 233 234 262 syl123anc 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> [_ Y / x ]_ B <_ [_ y / x ]_ B )
264 224 263 sylan2 
 |-  ( ( ph /\ y e. ( X (,) Y ) ) -> [_ Y / x ]_ B <_ [_ y / x ]_ B )
265 29 rexrd 
 |-  ( ph -> X e. RR* )
266 23 rexrd 
 |-  ( ph -> Y e. RR* )
267 lbicc2 
 |-  ( ( X e. RR* /\ Y e. RR* /\ X <_ Y ) -> X e. ( X [,] Y ) )
268 265 266 18 267 syl3anc 
 |-  ( ph -> X e. ( X [,] Y ) )
269 ubicc2 
 |-  ( ( X e. RR* /\ Y e. RR* /\ X <_ Y ) -> Y e. ( X [,] Y ) )
270 265 266 18 269 syl3anc 
 |-  ( ph -> Y e. ( X [,] Y ) )
271 oveq2 
 |-  ( y = X -> ( [_ Y / x ]_ B x. y ) = ( [_ Y / x ]_ B x. X ) )
272 oveq2 
 |-  ( y = Y -> ( [_ Y / x ]_ B x. y ) = ( [_ Y / x ]_ B x. Y ) )
273 29 23 179 198 216 223 264 268 270 18 271 62 272 46 dvle 
 |-  ( ph -> ( ( [_ Y / x ]_ B x. Y ) - ( [_ Y / x ]_ B x. X ) ) <_ ( [_ Y / x ]_ A - [_ X / x ]_ A ) )
274 81 273 eqbrtrd 
 |-  ( ph -> ( [_ Y / x ]_ B x. ( Y - X ) ) <_ ( [_ Y / x ]_ A - [_ X / x ]_ A ) )
275 77 55 64 274 lesubd 
 |-  ( ph -> [_ X / x ]_ A <_ ( [_ Y / x ]_ A - ( [_ Y / x ]_ B x. ( Y - X ) ) ) )
276 74 recnd 
 |-  ( ph -> ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) e. CC )
277 45 recnd 
 |-  ( ph -> ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) e. CC )
278 55 recnd 
 |-  ( ph -> [_ Y / x ]_ A e. CC )
279 276 277 278 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 ) )
280 277 276 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 ) ) )
281 31 recnd 
 |-  ( ph -> ( |_ ` X ) e. CC )
282 79 80 281 nnncan2d 
 |-  ( ph -> ( ( Y - ( |_ ` X ) ) - ( X - ( |_ ` X ) ) ) = ( Y - X ) )
283 282 oveq1d 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - ( X - ( |_ ` X ) ) ) x. [_ Y / x ]_ B ) = ( ( Y - X ) x. [_ Y / x ]_ B ) )
284 32 recnd 
 |-  ( ph -> ( Y - ( |_ ` X ) ) e. CC )
285 57 recnd 
 |-  ( ph -> ( X - ( |_ ` X ) ) e. CC )
286 284 285 78 subdird 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - ( X - ( |_ ` X ) ) ) x. [_ Y / x ]_ B ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) ) )
287 76 recnd 
 |-  ( ph -> ( Y - X ) e. CC )
288 287 78 mulcomd 
 |-  ( ph -> ( ( Y - X ) x. [_ Y / x ]_ B ) = ( [_ Y / x ]_ B x. ( Y - X ) ) )
289 283 286 288 3eqtr3d 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) ) = ( [_ Y / x ]_ B x. ( Y - X ) ) )
290 289 negeqd 
 |-  ( ph -> -u ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) ) = -u ( [_ Y / x ]_ B x. ( Y - X ) ) )
291 280 290 eqtr3d 
 |-  ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) ) = -u ( [_ Y / x ]_ B x. ( Y - X ) ) )
292 291 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 ) )
293 77 recnd 
 |-  ( ph -> ( [_ Y / x ]_ B x. ( Y - X ) ) e. CC )
294 293 278 negsubdid 
 |-  ( ph -> -u ( ( [_ Y / x ]_ B x. ( Y - X ) ) - [_ Y / x ]_ A ) = ( -u ( [_ Y / x ]_ B x. ( Y - X ) ) + [_ Y / x ]_ A ) )
295 292 294 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 ) )
296 293 278 negsubdi2d 
 |-  ( ph -> -u ( ( [_ Y / x ]_ B x. ( Y - X ) ) - [_ Y / x ]_ A ) = ( [_ Y / x ]_ A - ( [_ Y / x ]_ B x. ( Y - X ) ) ) )
297 279 295 296 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 ) ) ) )
298 275 297 breqtrrd 
 |-  ( ph -> [_ X / x ]_ A <_ ( ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) ) )
299 64 74 56 298 lesubd 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) <_ ( ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ X / x ]_ A ) )
300 flle 
 |-  ( X e. RR -> ( |_ ` X ) <_ X )
301 29 300 syl 
 |-  ( ph -> ( |_ ` X ) <_ X )
302 29 31 subge0d 
 |-  ( ph -> ( 0 <_ ( X - ( |_ ` X ) ) <-> ( |_ ` X ) <_ X ) )
303 301 302 mpbird 
 |-  ( ph -> 0 <_ ( X - ( |_ ` X ) ) )
304 58 breq2d 
 |-  ( y = X -> ( [_ Y / x ]_ B <_ [_ y / x ]_ B <-> [_ Y / x ]_ B <_ [_ X / x ]_ B ) )
305 263 ralrimiva 
 |-  ( ph -> A. y e. ( X [,] Y ) [_ Y / x ]_ B <_ [_ y / x ]_ B )
306 304 305 268 rspcdva 
 |-  ( ph -> [_ Y / x ]_ B <_ [_ X / x ]_ B )
307 44 60 57 303 306 lemul2ad 
 |-  ( ph -> ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) <_ ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) )
308 74 61 64 307 lesub1dd 
 |-  ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ X / x ]_ A ) <_ ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) )
309 56 75 65 299 308 letrd 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) <_ ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) )
310 56 65 73 309 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 ) )
311 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 ) )
312 29 leidd 
 |-  ( ph -> X <_ X )
313 265 266 12 18 19 xrletrd 
 |-  ( ph -> X <_ U )
314 fllep1 
 |-  ( X e. RR -> X <_ ( ( |_ ` X ) + 1 ) )
315 29 314 syl 
 |-  ( ph -> X <_ ( ( |_ ` X ) + 1 ) )
316 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 15 17 312 313 315 dvfsumlem1 
 |-  ( ph -> ( H ` X ) = ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) + sum_ k e. ( M ... ( |_ ` X ) ) C ) )
317 310 311 316 3brtr4d 
 |-  ( ph -> ( H ` Y ) <_ ( H ` X ) )
318 65 60 resubcld 
 |-  ( ph -> ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) - [_ X / x ]_ B ) e. RR )
319 56 44 resubcld 
 |-  ( ph -> ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) - [_ Y / x ]_ B ) e. RR )
320 peano2rem 
 |-  ( ( X - ( |_ ` X ) ) e. RR -> ( ( X - ( |_ ` X ) ) - 1 ) e. RR )
321 57 320 syl 
 |-  ( ph -> ( ( X - ( |_ ` X ) ) - 1 ) e. RR )
322 321 60 remulcld 
 |-  ( ph -> ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) e. RR )
323 322 64 resubcld 
 |-  ( ph -> ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) e. RR )
324 peano2rem 
 |-  ( ( Y - ( |_ ` X ) ) e. RR -> ( ( Y - ( |_ ` X ) ) - 1 ) e. RR )
325 32 324 syl 
 |-  ( ph -> ( ( Y - ( |_ ` X ) ) - 1 ) e. RR )
326 325 60 remulcld 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) e. RR )
327 326 55 resubcld 
 |-  ( ph -> ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ Y / x ]_ A ) e. RR )
328 325 44 remulcld 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) e. RR )
329 328 55 resubcld 
 |-  ( ph -> ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) e. RR )
330 322 recnd 
 |-  ( ph -> ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) e. CC )
331 326 recnd 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) e. CC )
332 330 331 subcld 
 |-  ( ph -> ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) ) e. CC )
333 332 278 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 ) ) ) )
334 330 331 278 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 ) )
335 278 331 330 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 ) ) ) )
336 333 334 335 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 ) ) ) )
337 1cnd 
 |-  ( ph -> 1 e. CC )
338 284 285 337 nnncan2d 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) - ( ( X - ( |_ ` X ) ) - 1 ) ) = ( ( Y - ( |_ ` X ) ) - ( X - ( |_ ` X ) ) ) )
339 338 282 eqtrd 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) - ( ( X - ( |_ ` X ) ) - 1 ) ) = ( Y - X ) )
340 339 oveq1d 
 |-  ( ph -> ( ( ( ( Y - ( |_ ` X ) ) - 1 ) - ( ( X - ( |_ ` X ) ) - 1 ) ) x. [_ X / x ]_ B ) = ( ( Y - X ) x. [_ X / x ]_ B ) )
341 325 recnd 
 |-  ( ph -> ( ( Y - ( |_ ` X ) ) - 1 ) e. CC )
342 321 recnd 
 |-  ( ph -> ( ( X - ( |_ ` X ) ) - 1 ) e. CC )
343 60 recnd 
 |-  ( ph -> [_ X / x ]_ B e. CC )
344 341 342 343 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 ) ) )
345 287 343 mulcomd 
 |-  ( ph -> ( ( Y - X ) x. [_ X / x ]_ B ) = ( [_ X / x ]_ B x. ( Y - X ) ) )
346 340 344 345 3eqtr3d 
 |-  ( ph -> ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) ) = ( [_ X / x ]_ B x. ( Y - X ) ) )
347 346 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 ) ) ) )
348 336 347 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 ) ) ) )
349 60 76 remulcld 
 |-  ( ph -> ( [_ X / x ]_ B x. ( Y - X ) ) e. RR )
350 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 ) )
351 60 101 102 350 syl3anc 
 |-  ( ph -> ( y e. ( X [,] Y ) |-> [_ X / x ]_ B ) e. ( ( X [,] Y ) -cn-> RR ) )
352 remulcl 
 |-  ( ( [_ X / x ]_ B e. RR /\ y e. RR ) -> ( [_ X / x ]_ B x. y ) e. RR )
353 simpl 
 |-  ( ( [_ X / x ]_ B e. RR /\ y e. RR ) -> [_ X / x ]_ B e. RR )
354 353 recnd 
 |-  ( ( [_ X / x ]_ B e. RR /\ y e. RR ) -> [_ X / x ]_ B e. CC )
355 simpr 
 |-  ( ( [_ X / x ]_ B e. RR /\ y e. RR ) -> y e. RR )
356 355 recnd 
 |-  ( ( [_ X / x ]_ B e. RR /\ y e. RR ) -> y e. CC )
357 354 356 jca 
 |-  ( ( [_ X / x ]_ B e. RR /\ y e. RR ) -> ( [_ X / x ]_ B e. CC /\ y e. CC ) )
358 ovmpot 
 |-  ( ( [_ X / x ]_ B e. CC /\ y e. CC ) -> ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) = ( [_ X / x ]_ B x. y ) )
359 358 eqcomd 
 |-  ( ( [_ X / x ]_ B e. CC /\ y e. CC ) -> ( [_ X / x ]_ B x. y ) = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) )
360 357 359 syl 
 |-  ( ( [_ X / x ]_ B e. RR /\ y e. RR ) -> ( [_ X / x ]_ B x. y ) = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) )
361 360 eleq1d 
 |-  ( ( [_ X / x ]_ B e. RR /\ y e. RR ) -> ( ( [_ X / x ]_ B x. y ) e. RR <-> ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) e. RR ) )
362 361 biimpd 
 |-  ( ( [_ X / x ]_ B e. RR /\ y e. RR ) -> ( ( [_ X / x ]_ B x. y ) e. RR -> ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) e. RR ) )
363 352 362 mpd 
 |-  ( ( [_ X / x ]_ B e. RR /\ y e. RR ) -> ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) e. RR )
364 82 83 351 106 100 363 cncfmpt2ss 
 |-  ( ph -> ( y e. ( X [,] Y ) |-> ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) e. ( ( X [,] Y ) -cn-> RR ) )
365 df-mpt 
 |-  ( y e. ( X [,] Y ) |-> ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) = { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) }
366 365 eleq1i 
 |-  ( ( y e. ( X [,] Y ) |-> ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) e. ( ( X [,] Y ) -cn-> RR ) <-> { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } e. ( ( X [,] Y ) -cn-> RR ) )
367 366 biimpi 
 |-  ( ( y e. ( X [,] Y ) |-> ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) e. ( ( X [,] Y ) -cn-> RR ) -> { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } e. ( ( X [,] Y ) -cn-> RR ) )
368 364 367 syl 
 |-  ( ph -> { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } e. ( ( X [,] Y ) -cn-> RR ) )
369 124 a1dd 
 |-  ( ph -> ( y e. ( X [,] Y ) -> ( w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) -> y e. ( X [,] Y ) ) ) )
370 369 impd 
 |-  ( ph -> ( ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) -> y e. ( X [,] Y ) ) )
371 343 adantr 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> [_ X / x ]_ B e. CC )
372 371 142 jca 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> ( [_ X / x ]_ B e. CC /\ y e. CC ) )
373 372 358 syl 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) = ( [_ X / x ]_ B x. y ) )
374 373 eqeq2d 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> ( w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) <-> w = ( [_ X / x ]_ B x. y ) ) )
375 374 biimpd 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> ( w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) -> w = ( [_ X / x ]_ B x. y ) ) )
376 375 ex 
 |-  ( ph -> ( y e. ( X [,] Y ) -> ( w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) -> w = ( [_ X / x ]_ B x. y ) ) ) )
377 376 impd 
 |-  ( ph -> ( ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) -> w = ( [_ X / x ]_ B x. y ) ) )
378 370 377 jcad 
 |-  ( ph -> ( ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) -> ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B x. y ) ) ) )
379 124 a1dd 
 |-  ( ph -> ( y e. ( X [,] Y ) -> ( w = ( [_ X / x ]_ B x. y ) -> y e. ( X [,] Y ) ) ) )
380 379 impd 
 |-  ( ph -> ( ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B x. y ) ) -> y e. ( X [,] Y ) ) )
381 372 359 syl 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> ( [_ X / x ]_ B x. y ) = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) )
382 381 eqeq2d 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> ( w = ( [_ X / x ]_ B x. y ) <-> w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) )
383 382 biimpd 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> ( w = ( [_ X / x ]_ B x. y ) -> w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) )
384 383 ex 
 |-  ( ph -> ( y e. ( X [,] Y ) -> ( w = ( [_ X / x ]_ B x. y ) -> w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) ) )
385 384 impd 
 |-  ( ph -> ( ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B x. y ) ) -> w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) )
386 380 385 jcad 
 |-  ( ph -> ( ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B x. y ) ) -> ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) ) )
387 378 386 impbid 
 |-  ( ph -> ( ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) <-> ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B x. y ) ) ) )
388 387 opabbidv 
 |-  ( ph -> { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } = { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B x. y ) ) } )
389 df-mpt 
 |-  ( y e. ( X [,] Y ) |-> ( [_ X / x ]_ B x. y ) ) = { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B x. y ) ) }
390 389 eqcomi 
 |-  { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B x. y ) ) } = ( y e. ( X [,] Y ) |-> ( [_ X / x ]_ B x. y ) )
391 390 eqeq2i 
 |-  ( { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } = { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B x. y ) ) } <-> { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } = ( y e. ( X [,] Y ) |-> ( [_ X / x ]_ B x. y ) ) )
392 391 biimpi 
 |-  ( { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } = { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B x. y ) ) } -> { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } = ( y e. ( X [,] Y ) |-> ( [_ X / x ]_ B x. y ) ) )
393 388 392 syl 
 |-  ( ph -> { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } = ( y e. ( X [,] Y ) |-> ( [_ X / x ]_ B x. y ) ) )
394 393 eleq1d 
 |-  ( ph -> ( { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } e. ( ( X [,] Y ) -cn-> RR ) <-> ( y e. ( X [,] Y ) |-> ( [_ X / x ]_ B x. y ) ) e. ( ( X [,] Y ) -cn-> RR ) ) )
395 394 biimpd 
 |-  ( ph -> ( { <. y , w >. | ( y e. ( X [,] Y ) /\ w = ( [_ X / x ]_ B ( u e. CC , v e. CC |-> ( u x. v ) ) y ) ) } e. ( ( X [,] Y ) -cn-> RR ) -> ( y e. ( X [,] Y ) |-> ( [_ X / x ]_ B x. y ) ) e. ( ( X [,] Y ) -cn-> RR ) ) )
396 368 395 mpd 
 |-  ( ph -> ( y e. ( X [,] Y ) |-> ( [_ X / x ]_ B x. y ) ) e. ( ( X [,] Y ) -cn-> RR ) )
397 181 185 186 194 343 dvmptcmul 
 |-  ( ph -> ( RR _D ( y e. ( X (,) Y ) |-> ( [_ X / x ]_ B x. y ) ) ) = ( y e. ( X (,) Y ) |-> ( [_ X / x ]_ B x. 1 ) ) )
398 343 mulridd 
 |-  ( ph -> ( [_ X / x ]_ B x. 1 ) = [_ X / x ]_ B )
399 398 mpteq2dv 
 |-  ( ph -> ( y e. ( X (,) Y ) |-> ( [_ X / x ]_ B x. 1 ) ) = ( y e. ( X (,) Y ) |-> [_ X / x ]_ B ) )
400 397 399 eqtrd 
 |-  ( ph -> ( RR _D ( y e. ( X (,) Y ) |-> ( [_ X / x ]_ B x. y ) ) ) = ( y e. ( X (,) Y ) |-> [_ X / x ]_ B ) )
401 15 adantr 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> X e. S )
402 141 rexrd 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> y e. RR* )
403 266 adantr 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> Y e. RR* )
404 12 adantr 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> U e. RR* )
405 402 403 404 233 234 xrletrd 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> y <_ U )
406 vex 
 |-  y e. _V
407 eleq1 
 |-  ( k = y -> ( k e. S <-> y e. S ) )
408 407 anbi2d 
 |-  ( k = y -> ( ( X e. S /\ k e. S ) <-> ( X e. S /\ y e. S ) ) )
409 breq2 
 |-  ( k = y -> ( X <_ k <-> X <_ y ) )
410 breq1 
 |-  ( k = y -> ( k <_ U <-> y <_ U ) )
411 409 410 3anbi23d 
 |-  ( k = y -> ( ( D <_ X /\ X <_ k /\ k <_ U ) <-> ( D <_ X /\ X <_ y /\ y <_ U ) ) )
412 408 411 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 ) ) ) )
413 csbeq1 
 |-  ( k = y -> [_ k / x ]_ B = [_ y / x ]_ B )
414 243 413 eqtr3id 
 |-  ( k = y -> C = [_ y / x ]_ B )
415 414 breq1d 
 |-  ( k = y -> ( C <_ [_ X / x ]_ B <-> [_ y / x ]_ B <_ [_ X / x ]_ B ) )
416 412 415 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 ) ) )
417 simp2l 
 |-  ( ( ph /\ ( X e. S /\ k e. S ) /\ ( D <_ X /\ X <_ k /\ k <_ U ) ) -> X e. S )
418 nfv 
 |-  F/ x ( ph /\ ( X e. S /\ k e. S ) /\ ( D <_ X /\ X <_ k /\ k <_ U ) )
419 nfcsb1v 
 |-  F/_ x [_ X / x ]_ B
420 248 249 419 nfbr 
 |-  F/ x C <_ [_ X / x ]_ B
421 418 420 nfim 
 |-  F/ x ( ( ph /\ ( X e. S /\ k e. S ) /\ ( D <_ X /\ X <_ k /\ k <_ U ) ) -> C <_ [_ X / x ]_ B )
422 eleq1 
 |-  ( x = X -> ( x e. S <-> X e. S ) )
423 422 anbi1d 
 |-  ( x = X -> ( ( x e. S /\ k e. S ) <-> ( X e. S /\ k e. S ) ) )
424 breq2 
 |-  ( x = X -> ( D <_ x <-> D <_ X ) )
425 breq1 
 |-  ( x = X -> ( x <_ k <-> X <_ k ) )
426 424 425 3anbi12d 
 |-  ( x = X -> ( ( D <_ x /\ x <_ k /\ k <_ U ) <-> ( D <_ X /\ X <_ k /\ k <_ U ) ) )
427 423 426 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 ) ) ) )
428 csbeq1a 
 |-  ( x = X -> B = [_ X / x ]_ B )
429 428 breq2d 
 |-  ( x = X -> ( C <_ B <-> C <_ [_ X / x ]_ B ) )
430 427 429 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 ) ) )
431 421 430 13 vtoclg1f 
 |-  ( X e. S -> ( ( ph /\ ( X e. S /\ k e. S ) /\ ( D <_ X /\ X <_ k /\ k <_ U ) ) -> C <_ [_ X / x ]_ B ) )
432 417 431 mpcom 
 |-  ( ( ph /\ ( X e. S /\ k e. S ) /\ ( D <_ X /\ X <_ k /\ k <_ U ) ) -> C <_ [_ X / x ]_ B )
433 406 416 432 vtocl 
 |-  ( ( ph /\ ( X e. S /\ y e. S ) /\ ( D <_ X /\ X <_ y /\ y <_ U ) ) -> [_ y / x ]_ B <_ [_ X / x ]_ B )
434 225 401 226 230 231 405 433 syl123anc 
 |-  ( ( ph /\ y e. ( X [,] Y ) ) -> [_ y / x ]_ B <_ [_ X / x ]_ B )
435 224 434 sylan2 
 |-  ( ( ph /\ y e. ( X (,) Y ) ) -> [_ y / x ]_ B <_ [_ X / x ]_ B )
436 oveq2 
 |-  ( y = X -> ( [_ X / x ]_ B x. y ) = ( [_ X / x ]_ B x. X ) )
437 oveq2 
 |-  ( y = Y -> ( [_ X / x ]_ B x. y ) = ( [_ X / x ]_ B x. Y ) )
438 29 23 216 223 396 400 435 268 270 18 62 436 46 437 dvle 
 |-  ( ph -> ( [_ Y / x ]_ A - [_ X / x ]_ A ) <_ ( ( [_ X / x ]_ B x. Y ) - ( [_ X / x ]_ B x. X ) ) )
439 343 79 80 subdid 
 |-  ( ph -> ( [_ X / x ]_ B x. ( Y - X ) ) = ( ( [_ X / x ]_ B x. Y ) - ( [_ X / x ]_ B x. X ) ) )
440 438 439 breqtrrd 
 |-  ( ph -> ( [_ Y / x ]_ A - [_ X / x ]_ A ) <_ ( [_ X / x ]_ B x. ( Y - X ) ) )
441 55 64 349 440 subled 
 |-  ( ph -> ( [_ Y / x ]_ A - ( [_ X / x ]_ B x. ( Y - X ) ) ) <_ [_ X / x ]_ A )
442 348 441 eqbrtrd 
 |-  ( ph -> ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ Y / x ]_ A ) ) <_ [_ X / x ]_ A )
443 322 327 64 442 subled 
 |-  ( ph -> ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) <_ ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ Y / x ]_ A ) )
444 325 renegcld 
 |-  ( ph -> -u ( ( Y - ( |_ ` X ) ) - 1 ) e. RR )
445 1red 
 |-  ( ph -> 1 e. RR )
446 23 31 445 lesubadd2d 
 |-  ( ph -> ( ( Y - ( |_ ` X ) ) <_ 1 <-> Y <_ ( ( |_ ` X ) + 1 ) ) )
447 20 446 mpbird 
 |-  ( ph -> ( Y - ( |_ ` X ) ) <_ 1 )
448 32 445 suble0d 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) <_ 0 <-> ( Y - ( |_ ` X ) ) <_ 1 ) )
449 447 448 mpbird 
 |-  ( ph -> ( ( Y - ( |_ ` X ) ) - 1 ) <_ 0 )
450 325 le0neg1d 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) <_ 0 <-> 0 <_ -u ( ( Y - ( |_ ` X ) ) - 1 ) ) )
451 449 450 mpbid 
 |-  ( ph -> 0 <_ -u ( ( Y - ( |_ ` X ) ) - 1 ) )
452 44 60 444 451 306 lemul2ad 
 |-  ( ph -> ( -u ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) <_ ( -u ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) )
453 341 78 mulneg1d 
 |-  ( ph -> ( -u ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) = -u ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) )
454 341 343 mulneg1d 
 |-  ( ph -> ( -u ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) = -u ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) )
455 452 453 454 3brtr3d 
 |-  ( ph -> -u ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) <_ -u ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) )
456 326 328 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 ) ) )
457 455 456 mpbird 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) <_ ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) )
458 326 328 55 457 lesub1dd 
 |-  ( ph -> ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ Y / x ]_ A ) <_ ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) )
459 323 327 329 443 458 letrd 
 |-  ( ph -> ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) <_ ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) )
460 285 337 343 subdird 
 |-  ( ph -> ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) = ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - ( 1 x. [_ X / x ]_ B ) ) )
461 343 mullidd 
 |-  ( ph -> ( 1 x. [_ X / x ]_ B ) = [_ X / x ]_ B )
462 461 oveq2d 
 |-  ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - ( 1 x. [_ X / x ]_ B ) ) = ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ B ) )
463 460 462 eqtrd 
 |-  ( ph -> ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) = ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ B ) )
464 463 oveq1d 
 |-  ( ph -> ( ( ( ( X - ( |_ ` X ) ) - 1 ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) = ( ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ B ) - [_ X / x ]_ A ) )
465 284 337 78 subdird 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( 1 x. [_ Y / x ]_ B ) ) )
466 78 mullidd 
 |-  ( ph -> ( 1 x. [_ Y / x ]_ B ) = [_ Y / x ]_ B )
467 466 oveq2d 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - ( 1 x. [_ Y / x ]_ B ) ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ B ) )
468 465 467 eqtrd 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) = ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ B ) )
469 468 oveq1d 
 |-  ( ph -> ( ( ( ( Y - ( |_ ` X ) ) - 1 ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) = ( ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ B ) - [_ Y / x ]_ A ) )
470 459 464 469 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 ) )
471 61 recnd 
 |-  ( ph -> ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) e. CC )
472 64 recnd 
 |-  ( ph -> [_ X / x ]_ A e. CC )
473 471 472 343 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 ) )
474 277 278 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 ) )
475 470 473 474 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 ) )
476 318 319 73 475 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 ) )
477 65 recnd 
 |-  ( ph -> ( ( ( X - ( |_ ` X ) ) x. [_ X / x ]_ B ) - [_ X / x ]_ A ) e. CC )
478 73 recnd 
 |-  ( ph -> sum_ k e. ( M ... ( |_ ` X ) ) C e. CC )
479 477 478 343 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 ) )
480 56 recnd 
 |-  ( ph -> ( ( ( Y - ( |_ ` X ) ) x. [_ Y / x ]_ B ) - [_ Y / x ]_ A ) e. CC )
481 480 478 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 ) )
482 476 479 481 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 ) )
483 316 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 ) )
484 311 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 ) )
485 482 483 484 3brtr4d 
 |-  ( ph -> ( ( H ` X ) - [_ X / x ]_ B ) <_ ( ( H ` Y ) - [_ Y / x ]_ B ) )
486 317 485 jca 
 |-  ( ph -> ( ( H ` Y ) <_ ( H ` X ) /\ ( ( H ` X ) - [_ X / x ]_ B ) <_ ( ( H ` Y ) - [_ Y / x ]_ B ) ) )