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
|
sseldi |
|- ( 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
|
syl5eqr |
|- ( 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
|
syl5eqr |
|- ( 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 ) ) ) |