MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  taylthlem2 Unicode version

Theorem taylthlem2 19753
Description: Lemma for taylth 19754. (Contributed by Mario Carneiro, 1-Jan-2017.)
Hypotheses
Ref Expression
taylth.f  |-  ( ph  ->  F : A --> RR )
taylth.a  |-  ( ph  ->  A  C_  RR )
taylth.d  |-  ( ph  ->  dom  ( ( RR  D n F ) `
 N )  =  A )
taylth.n  |-  ( ph  ->  N  e.  NN )
taylth.b  |-  ( ph  ->  B  e.  A )
taylth.t  |-  T  =  ( N ( RR Tayl  F ) B )
taylthlem2.m  |-  ( ph  ->  M  e.  ( 1..^ N ) )
taylthlem2.i  |-  ( ph  ->  0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( RR  D n F ) `  ( N  -  M )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  M ) ) `
 x ) )  /  ( ( x  -  B ) ^ M ) ) ) lim
CC  B ) )
Assertion
Ref Expression
taylthlem2  |-  ( ph  ->  0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) `
 x ) )  /  ( ( x  -  B ) ^
( M  +  1 ) ) ) ) lim
CC  B ) )
Distinct variable groups:    x, A    x, B    x, F    x, M    x, T    x, N    ph, x

Proof of Theorem taylthlem2
Dummy variables  y 
k are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 taylth.a . . 3  |-  ( ph  ->  A  C_  RR )
2 taylth.f . . . . . . . 8  |-  ( ph  ->  F : A --> RR )
3 1nn0 9981 . . . . . . . . . . . . 13  |-  1  e.  NN0
4 nn0uz 10262 . . . . . . . . . . . . 13  |-  NN0  =  ( ZZ>= `  0 )
53, 4eleqtri 2355 . . . . . . . . . . . 12  |-  1  e.  ( ZZ>= `  0 )
6 fzss1 10830 . . . . . . . . . . . 12  |-  ( 1  e.  ( ZZ>= `  0
)  ->  ( 1 ... N )  C_  ( 0 ... N
) )
75, 6ax-mp 8 . . . . . . . . . . 11  |-  ( 1 ... N )  C_  ( 0 ... N
)
8 taylthlem2.m . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  ( 1..^ N ) )
9 fzofzp1 10916 . . . . . . . . . . . 12  |-  ( M  e.  ( 1..^ N )  ->  ( M  +  1 )  e.  ( 1 ... N
) )
108, 9syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( M  +  1 )  e.  ( 1 ... N ) )
117, 10sseldi 3178 . . . . . . . . . 10  |-  ( ph  ->  ( M  +  1 )  e.  ( 0 ... N ) )
12 fznn0sub2 10825 . . . . . . . . . 10  |-  ( ( M  +  1 )  e.  ( 0 ... N )  ->  ( N  -  ( M  +  1 ) )  e.  ( 0 ... N ) )
1311, 12syl 15 . . . . . . . . 9  |-  ( ph  ->  ( N  -  ( M  +  1 ) )  e.  ( 0 ... N ) )
14 elfznn0 10822 . . . . . . . . 9  |-  ( ( N  -  ( M  +  1 ) )  e.  ( 0 ... N )  ->  ( N  -  ( M  +  1 ) )  e.  NN0 )
1513, 14syl 15 . . . . . . . 8  |-  ( ph  ->  ( N  -  ( M  +  1 ) )  e.  NN0 )
16 dvnfre 19301 . . . . . . . 8  |-  ( ( F : A --> RR  /\  A  C_  RR  /\  ( N  -  ( M  +  1 ) )  e.  NN0 )  -> 
( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) : dom  (
( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) --> RR )
172, 1, 15, 16syl3anc 1182 . . . . . . 7  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) : dom  (
( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) --> RR )
18 reex 8828 . . . . . . . . . . . . 13  |-  RR  e.  _V
1918prid1 3734 . . . . . . . . . . . 12  |-  RR  e.  { RR ,  CC }
2019a1i 10 . . . . . . . . . . 11  |-  ( ph  ->  RR  e.  { RR ,  CC } )
21 cnex 8818 . . . . . . . . . . . . 13  |-  CC  e.  _V
2221a1i 10 . . . . . . . . . . . 12  |-  ( ph  ->  CC  e.  _V )
2318a1i 10 . . . . . . . . . . . 12  |-  ( ph  ->  RR  e.  _V )
24 ax-resscn 8794 . . . . . . . . . . . . 13  |-  RR  C_  CC
25 fss 5397 . . . . . . . . . . . . 13  |-  ( ( F : A --> RR  /\  RR  C_  CC )  ->  F : A --> CC )
262, 24, 25sylancl 643 . . . . . . . . . . . 12  |-  ( ph  ->  F : A --> CC )
27 elpm2r 6788 . . . . . . . . . . . 12  |-  ( ( ( CC  e.  _V  /\  RR  e.  _V )  /\  ( F : A --> CC  /\  A  C_  RR ) )  ->  F  e.  ( CC  ^pm  RR ) )
2822, 23, 26, 1, 27syl22anc 1183 . . . . . . . . . . 11  |-  ( ph  ->  F  e.  ( CC 
^pm  RR ) )
29 dvnbss 19277 . . . . . . . . . . 11  |-  ( ( RR  e.  { RR ,  CC }  /\  F  e.  ( CC  ^pm  RR )  /\  ( N  -  ( M  +  1
) )  e.  NN0 )  ->  dom  ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) )  C_  dom  F )
3020, 28, 15, 29syl3anc 1182 . . . . . . . . . 10  |-  ( ph  ->  dom  ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) )  C_  dom  F )
31 fdm 5393 . . . . . . . . . . 11  |-  ( F : A --> RR  ->  dom 
F  =  A )
322, 31syl 15 . . . . . . . . . 10  |-  ( ph  ->  dom  F  =  A )
3330, 32sseqtrd 3214 . . . . . . . . 9  |-  ( ph  ->  dom  ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) )  C_  A )
34 taylth.d . . . . . . . . . 10  |-  ( ph  ->  dom  ( ( RR  D n F ) `
 N )  =  A )
35 dvn2bss 19279 . . . . . . . . . . 11  |-  ( ( RR  e.  { RR ,  CC }  /\  F  e.  ( CC  ^pm  RR )  /\  ( N  -  ( M  +  1
) )  e.  ( 0 ... N ) )  ->  dom  ( ( RR  D n F ) `  N ) 
C_  dom  ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) ) )
3620, 28, 13, 35syl3anc 1182 . . . . . . . . . 10  |-  ( ph  ->  dom  ( ( RR  D n F ) `
 N )  C_  dom  ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) )
3734, 36eqsstr3d 3213 . . . . . . . . 9  |-  ( ph  ->  A  C_  dom  ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) )
3833, 37eqssd 3196 . . . . . . . 8  |-  ( ph  ->  dom  ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) )  =  A )
3938feq2d 5380 . . . . . . 7  |-  ( ph  ->  ( ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) ) : dom  ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) ) --> RR  <->  ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) : A --> RR ) )
4017, 39mpbid 201 . . . . . 6  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) : A --> RR )
4140ffvelrnda 5665 . . . . 5  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  y )  e.  RR )
421sselda 3180 . . . . . 6  |-  ( (
ph  /\  y  e.  A )  ->  y  e.  RR )
43 fvres 5542 . . . . . . . 8  |-  ( y  e.  RR  ->  (
( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) )  |`  RR ) `  y )  =  ( ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) `
 y ) )
4443adantl 452 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) )  |`  RR ) `  y )  =  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y ) )
45 resubdrg 16423 . . . . . . . . . . . 12  |-  ( RR  e.  (SubRing ` fld )  /\  (flds  RR )  e.  DivRing )
4645simpli 444 . . . . . . . . . . 11  |-  RR  e.  (SubRing ` fld )
4746a1i 10 . . . . . . . . . 10  |-  ( ph  ->  RR  e.  (SubRing ` fld ) )
48 taylth.n . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  NN )
4948nnnn0d 10018 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  NN0 )
50 taylth.b . . . . . . . . . . . . 13  |-  ( ph  ->  B  e.  A )
5150, 34eleqtrrd 2360 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  dom  (
( RR  D n F ) `  N
) )
52 taylth.t . . . . . . . . . . . 12  |-  T  =  ( N ( RR Tayl  F ) B )
531, 50sseldd 3181 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  RR )
542adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  F : A --> RR )
551adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  A  C_  RR )
56 elfznn0 10822 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( 0 ... N )  ->  k  e.  NN0 )
5756adantl 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  k  e.  NN0 )
58 dvnfre 19301 . . . . . . . . . . . . . . 15  |-  ( ( F : A --> RR  /\  A  C_  RR  /\  k  e.  NN0 )  ->  (
( RR  D n F ) `  k
) : dom  (
( RR  D n F ) `  k
) --> RR )
5954, 55, 57, 58syl3anc 1182 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
( RR  D n F ) `  k
) : dom  (
( RR  D n F ) `  k
) --> RR )
6019a1i 10 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  RR  e.  { RR ,  CC } )
6128adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  F  e.  ( CC  ^pm  RR ) )
62 simpr 447 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  k  e.  ( 0 ... N
) )
63 dvn2bss 19279 . . . . . . . . . . . . . . . 16  |-  ( ( RR  e.  { RR ,  CC }  /\  F  e.  ( CC  ^pm  RR )  /\  k  e.  ( 0 ... N ) )  ->  dom  ( ( RR  D n F ) `  N ) 
C_  dom  ( ( RR  D n F ) `
 k ) )
6460, 61, 62, 63syl3anc 1182 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  dom  ( ( RR  D n F ) `  N
)  C_  dom  ( ( RR  D n F ) `  k ) )
6551adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  B  e.  dom  ( ( RR  D n F ) `
 N ) )
6664, 65sseldd 3181 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  B  e.  dom  ( ( RR  D n F ) `
 k ) )
6759, 66ffvelrnd 5666 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
( ( RR  D n F ) `  k
) `  B )  e.  RR )
68 faccl 11298 . . . . . . . . . . . . . 14  |-  ( k  e.  NN0  ->  ( ! `
 k )  e.  NN )
6957, 68syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  ( ! `  k )  e.  NN )
7067, 69nndivred 9794 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
( ( ( RR  D n F ) `
 k ) `  B )  /  ( ! `  k )
)  e.  RR )
7120, 26, 1, 49, 51, 52, 47, 53, 70taylply2 19747 . . . . . . . . . . 11  |-  ( ph  ->  ( T  e.  (Poly `  RR )  /\  (deg `  T )  <_  N
) )
7271simpld 445 . . . . . . . . . 10  |-  ( ph  ->  T  e.  (Poly `  RR ) )
73 dvnply2 19667 . . . . . . . . . 10  |-  ( ( RR  e.  (SubRing ` fld )  /\  T  e.  (Poly `  RR )  /\  ( N  -  ( M  +  1 ) )  e.  NN0 )  ->  ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) )  e.  (Poly `  RR ) )
7447, 72, 15, 73syl3anc 1182 . . . . . . . . 9  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) )  e.  (Poly `  RR ) )
75 plyreres 19663 . . . . . . . . 9  |-  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) )  e.  (Poly `  RR )  ->  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) )  |`  RR ) : RR --> RR )
7674, 75syl 15 . . . . . . . 8  |-  ( ph  ->  ( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) )  |`  RR ) : RR --> RR )
7776ffvelrnda 5665 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) )  |`  RR ) `  y )  e.  RR )
7844, 77eqeltrrd 2358 . . . . . 6  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y )  e.  RR )
7942, 78syldan 456 . . . . 5  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y )  e.  RR )
8041, 79resubcld 9211 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y ) )  e.  RR )
81 eqid 2283 . . . 4  |-  ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) `
 y ) ) )  =  ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) `
 y ) ) )
8280, 81fmptd 5684 . . 3  |-  ( ph  ->  ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 y )  -  ( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) `  y ) ) ) : A --> RR )
8353adantr 451 . . . . . 6  |-  ( (
ph  /\  y  e.  A )  ->  B  e.  RR )
8442, 83resubcld 9211 . . . . 5  |-  ( (
ph  /\  y  e.  A )  ->  (
y  -  B )  e.  RR )
85 elfzouz 10879 . . . . . . . . . 10  |-  ( M  e.  ( 1..^ N )  ->  M  e.  ( ZZ>= `  1 )
)
868, 85syl 15 . . . . . . . . 9  |-  ( ph  ->  M  e.  ( ZZ>= ` 
1 ) )
87 nnuz 10263 . . . . . . . . 9  |-  NN  =  ( ZZ>= `  1 )
8886, 87syl6eleqr 2374 . . . . . . . 8  |-  ( ph  ->  M  e.  NN )
8988nnnn0d 10018 . . . . . . 7  |-  ( ph  ->  M  e.  NN0 )
9089adantr 451 . . . . . 6  |-  ( (
ph  /\  y  e.  A )  ->  M  e.  NN0 )
913a1i 10 . . . . . 6  |-  ( (
ph  /\  y  e.  A )  ->  1  e.  NN0 )
9290, 91nn0addcld 10022 . . . . 5  |-  ( (
ph  /\  y  e.  A )  ->  ( M  +  1 )  e.  NN0 )
9384, 92reexpcld 11262 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  (
( y  -  B
) ^ ( M  +  1 ) )  e.  RR )
94 eqid 2283 . . . 4  |-  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  + 
1 ) ) )  =  ( y  e.  A  |->  ( ( y  -  B ) ^
( M  +  1 ) ) )
9593, 94fmptd 5684 . . 3  |-  ( ph  ->  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) ) : A --> RR )
96 retop 18270 . . . . . 6  |-  ( topGen ` 
ran  (,) )  e.  Top
97 uniretop 18271 . . . . . . 7  |-  RR  =  U. ( topGen `  ran  (,) )
9897ntrss2 16794 . . . . . 6  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  A  C_  RR )  ->  ( ( int `  ( topGen ` 
ran  (,) ) ) `  A )  C_  A
)
9996, 1, 98sylancr 644 . . . . 5  |-  ( ph  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  A )  C_  A )
10048nncnd 9762 . . . . . . . . . . 11  |-  ( ph  ->  N  e.  CC )
10188nncnd 9762 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  CC )
102 ax-1cn 8795 . . . . . . . . . . . 12  |-  1  e.  CC
103102a1i 10 . . . . . . . . . . 11  |-  ( ph  ->  1  e.  CC )
104100, 101, 103nppcan2d 9183 . . . . . . . . . 10  |-  ( ph  ->  ( ( N  -  ( M  +  1
) )  +  1 )  =  ( N  -  M ) )
105104fveq2d 5529 . . . . . . . . 9  |-  ( ph  ->  ( ( RR  D n F ) `  (
( N  -  ( M  +  1 ) )  +  1 ) )  =  ( ( RR  D n F ) `  ( N  -  M ) ) )
10624a1i 10 . . . . . . . . . 10  |-  ( ph  ->  RR  C_  CC )
107 dvnp1 19274 . . . . . . . . . 10  |-  ( ( RR  C_  CC  /\  F  e.  ( CC  ^pm  RR )  /\  ( N  -  ( M  +  1
) )  e.  NN0 )  ->  ( ( RR  D n F ) `
 ( ( N  -  ( M  + 
1 ) )  +  1 ) )  =  ( RR  _D  (
( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) ) )
108106, 28, 15, 107syl3anc 1182 . . . . . . . . 9  |-  ( ph  ->  ( ( RR  D n F ) `  (
( N  -  ( M  +  1 ) )  +  1 ) )  =  ( RR 
_D  ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) ) ) )
109105, 108eqtr3d 2317 . . . . . . . 8  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  M )
)  =  ( RR 
_D  ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) ) ) )
110109dmeqd 4881 . . . . . . 7  |-  ( ph  ->  dom  ( ( RR  D n F ) `
 ( N  -  M ) )  =  dom  ( RR  _D  ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) ) )
111 fzonnsub 10894 . . . . . . . . . . . 12  |-  ( M  e.  ( 1..^ N )  ->  ( N  -  M )  e.  NN )
1128, 111syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( N  -  M
)  e.  NN )
113112nnnn0d 10018 . . . . . . . . . 10  |-  ( ph  ->  ( N  -  M
)  e.  NN0 )
114 dvnbss 19277 . . . . . . . . . 10  |-  ( ( RR  e.  { RR ,  CC }  /\  F  e.  ( CC  ^pm  RR )  /\  ( N  -  M )  e.  NN0 )  ->  dom  ( ( RR  D n F ) `
 ( N  -  M ) )  C_  dom  F )
11520, 28, 113, 114syl3anc 1182 . . . . . . . . 9  |-  ( ph  ->  dom  ( ( RR  D n F ) `
 ( N  -  M ) )  C_  dom  F )
116115, 32sseqtrd 3214 . . . . . . . 8  |-  ( ph  ->  dom  ( ( RR  D n F ) `
 ( N  -  M ) )  C_  A )
117 elfzofz 10889 . . . . . . . . . . . . 13  |-  ( M  e.  ( 1..^ N )  ->  M  e.  ( 1 ... N
) )
1188, 117syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  ( 1 ... N ) )
1197, 118sseldi 3178 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  ( 0 ... N ) )
120 fznn0sub2 10825 . . . . . . . . . . 11  |-  ( M  e.  ( 0 ... N )  ->  ( N  -  M )  e.  ( 0 ... N
) )
121119, 120syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( N  -  M
)  e.  ( 0 ... N ) )
122 dvn2bss 19279 . . . . . . . . . 10  |-  ( ( RR  e.  { RR ,  CC }  /\  F  e.  ( CC  ^pm  RR )  /\  ( N  -  M )  e.  ( 0 ... N ) )  ->  dom  ( ( RR  D n F ) `  N ) 
C_  dom  ( ( RR  D n F ) `
 ( N  -  M ) ) )
12320, 28, 121, 122syl3anc 1182 . . . . . . . . 9  |-  ( ph  ->  dom  ( ( RR  D n F ) `
 N )  C_  dom  ( ( RR  D n F ) `  ( N  -  M )
) )
12434, 123eqsstr3d 3213 . . . . . . . 8  |-  ( ph  ->  A  C_  dom  ( ( RR  D n F ) `  ( N  -  M ) ) )
125116, 124eqssd 3196 . . . . . . 7  |-  ( ph  ->  dom  ( ( RR  D n F ) `
 ( N  -  M ) )  =  A )
126110, 125eqtr3d 2317 . . . . . 6  |-  ( ph  ->  dom  ( RR  _D  ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) )  =  A )
127 fss 5397 . . . . . . . 8  |-  ( ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) : A --> RR  /\  RR  C_  CC )  -> 
( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) : A --> CC )
12840, 24, 127sylancl 643 . . . . . . 7  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) : A --> CC )
129 eqid 2283 . . . . . . . 8  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
130129tgioo2 18309 . . . . . . 7  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
131106, 128, 1, 130, 129dvbssntr 19250 . . . . . 6  |-  ( ph  ->  dom  ( RR  _D  ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) )  C_  (
( int `  ( topGen `
 ran  (,) )
) `  A )
)
132126, 131eqsstr3d 3213 . . . . 5  |-  ( ph  ->  A  C_  ( ( int `  ( topGen `  ran  (,) ) ) `  A
) )
13399, 132eqssd 3196 . . . 4  |-  ( ph  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  A )  =  A )
13497isopn3 16803 . . . . 5  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  A  C_  RR )  ->  ( A  e.  ( topGen `  ran  (,) )  <->  ( ( int `  ( topGen `  ran  (,) )
) `  A )  =  A ) )
13596, 1, 134sylancr 644 . . . 4  |-  ( ph  ->  ( A  e.  (
topGen `  ran  (,) )  <->  ( ( int `  ( topGen `
 ran  (,) )
) `  A )  =  A ) )
136133, 135mpbird 223 . . 3  |-  ( ph  ->  A  e.  ( topGen ` 
ran  (,) ) )
137 eqid 2283 . . 3  |-  ( A 
\  { B }
)  =  ( A 
\  { B }
)
138 difss 3303 . . . 4  |-  ( A 
\  { B }
)  C_  A
13941recnd 8861 . . . . . . 7  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  y )  e.  CC )
140 dvnf 19276 . . . . . . . . . 10  |-  ( ( RR  e.  { RR ,  CC }  /\  F  e.  ( CC  ^pm  RR )  /\  ( N  -  M )  e.  NN0 )  ->  ( ( RR  D n F ) `
 ( N  -  M ) ) : dom  ( ( RR  D n F ) `
 ( N  -  M ) ) --> CC )
14120, 28, 113, 140syl3anc 1182 . . . . . . . . 9  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  M )
) : dom  (
( RR  D n F ) `  ( N  -  M )
) --> CC )
142125feq2d 5380 . . . . . . . . 9  |-  ( ph  ->  ( ( ( RR  D n F ) `
 ( N  -  M ) ) : dom  ( ( RR  D n F ) `
 ( N  -  M ) ) --> CC  <->  ( ( RR  D n F ) `  ( N  -  M )
) : A --> CC ) )
143141, 142mpbid 201 . . . . . . . 8  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  M )
) : A --> CC )
144143ffvelrnda 5665 . . . . . . 7  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( RR  D n F ) `  ( N  -  M )
) `  y )  e.  CC )
145 dvnfre 19301 . . . . . . . . . . 11  |-  ( ( F : A --> RR  /\  A  C_  RR  /\  ( N  -  M )  e.  NN0 )  ->  (
( RR  D n F ) `  ( N  -  M )
) : dom  (
( RR  D n F ) `  ( N  -  M )
) --> RR )
1462, 1, 113, 145syl3anc 1182 . . . . . . . . . 10  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  M )
) : dom  (
( RR  D n F ) `  ( N  -  M )
) --> RR )
147125feq2d 5380 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( RR  D n F ) `
 ( N  -  M ) ) : dom  ( ( RR  D n F ) `
 ( N  -  M ) ) --> RR  <->  ( ( RR  D n F ) `  ( N  -  M )
) : A --> RR ) )
148146, 147mpbid 201 . . . . . . . . 9  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  M )
) : A --> RR )
149148feqmptd 5575 . . . . . . . 8  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  M )
)  =  ( y  e.  A  |->  ( ( ( RR  D n F ) `  ( N  -  M )
) `  y )
) )
15040feqmptd 5575 . . . . . . . . 9  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) )  =  ( y  e.  A  |->  ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  y ) ) )
151150oveq2d 5874 . . . . . . . 8  |-  ( ph  ->  ( RR  _D  (
( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) )  =  ( RR  _D  ( y  e.  A  |->  ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  y ) ) ) )
152109, 149, 1513eqtr3rd 2324 . . . . . . 7  |-  ( ph  ->  ( RR  _D  (
y  e.  A  |->  ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  y ) ) )  =  ( y  e.  A  |->  ( ( ( RR  D n F ) `  ( N  -  M )
) `  y )
) )
15379recnd 8861 . . . . . . 7  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y )  e.  CC )
154 fvex 5539 . . . . . . . 8  |-  ( ( ( CC  D n T ) `  ( N  -  M )
) `  y )  e.  _V
155154a1i 10 . . . . . . 7  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( CC  D n T ) `  ( N  -  M )
) `  y )  e.  _V )
15678recnd 8861 . . . . . . . 8  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y )  e.  CC )
157 recn 8827 . . . . . . . . 9  |-  ( y  e.  RR  ->  y  e.  CC )
158 dvnply2 19667 . . . . . . . . . . . 12  |-  ( ( RR  e.  (SubRing ` fld )  /\  T  e.  (Poly `  RR )  /\  ( N  -  M
)  e.  NN0 )  ->  ( ( CC  D n T ) `  ( N  -  M )
)  e.  (Poly `  RR ) )
15947, 72, 113, 158syl3anc 1182 . . . . . . . . . . 11  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  M )
)  e.  (Poly `  RR ) )
160 plyf 19580 . . . . . . . . . . 11  |-  ( ( ( CC  D n T ) `  ( N  -  M )
)  e.  (Poly `  RR )  ->  ( ( CC  D n T ) `  ( N  -  M ) ) : CC --> CC )
161159, 160syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  M )
) : CC --> CC )
162161ffvelrnda 5665 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( ( CC  D n T ) `  ( N  -  M )
) `  y )  e.  CC )
163157, 162sylan2 460 . . . . . . . 8  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( ( CC  D n T ) `  ( N  -  M )
) `  y )  e.  CC )
164129cnfldtopon 18292 . . . . . . . . . 10  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
165 toponmax 16666 . . . . . . . . . 10  |-  ( (
TopOpen ` fld )  e.  (TopOn `  CC )  ->  CC  e.  ( TopOpen ` fld ) )
166164, 165mp1i 11 . . . . . . . . 9  |-  ( ph  ->  CC  e.  ( TopOpen ` fld )
)
167 df-ss 3166 . . . . . . . . . 10  |-  ( RR  C_  CC  <->  ( RR  i^i  CC )  =  RR )
168106, 167sylib 188 . . . . . . . . 9  |-  ( ph  ->  ( RR  i^i  CC )  =  RR )
169 plyf 19580 . . . . . . . . . . 11  |-  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) )  e.  (Poly `  RR )  ->  ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) : CC --> CC )
17074, 169syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) : CC --> CC )
171170ffvelrnda 5665 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y )  e.  CC )
172104fveq2d 5529 . . . . . . . . . . 11  |-  ( ph  ->  ( ( CC  D n T ) `  (
( N  -  ( M  +  1 ) )  +  1 ) )  =  ( ( CC  D n T ) `  ( N  -  M ) ) )
173 ssid 3197 . . . . . . . . . . . . 13  |-  CC  C_  CC
174173a1i 10 . . . . . . . . . . . 12  |-  ( ph  ->  CC  C_  CC )
175 mapsspm 6801 . . . . . . . . . . . . 13  |-  ( CC 
^m  CC )  C_  ( CC  ^pm  CC )
176 plyf 19580 . . . . . . . . . . . . . . 15  |-  ( T  e.  (Poly `  RR )  ->  T : CC --> CC )
17772, 176syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  T : CC --> CC )
17821, 21elmap 6796 . . . . . . . . . . . . . 14  |-  ( T  e.  ( CC  ^m  CC )  <->  T : CC --> CC )
179177, 178sylibr 203 . . . . . . . . . . . . 13  |-  ( ph  ->  T  e.  ( CC 
^m  CC ) )
180175, 179sseldi 3178 . . . . . . . . . . . 12  |-  ( ph  ->  T  e.  ( CC 
^pm  CC ) )
181 dvnp1 19274 . . . . . . . . . . . 12  |-  ( ( CC  C_  CC  /\  T  e.  ( CC  ^pm  CC )  /\  ( N  -  ( M  +  1
) )  e.  NN0 )  ->  ( ( CC  D n T ) `
 ( ( N  -  ( M  + 
1 ) )  +  1 ) )  =  ( CC  _D  (
( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) ) )
182174, 180, 15, 181syl3anc 1182 . . . . . . . . . . 11  |-  ( ph  ->  ( ( CC  D n T ) `  (
( N  -  ( M  +  1 ) )  +  1 ) )  =  ( CC 
_D  ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) ) )
183172, 182eqtr3d 2317 . . . . . . . . . 10  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  M )
)  =  ( CC 
_D  ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) ) )
184161feqmptd 5575 . . . . . . . . . 10  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  M )
)  =  ( y  e.  CC  |->  ( ( ( CC  D n T ) `  ( N  -  M )
) `  y )
) )
185170feqmptd 5575 . . . . . . . . . . 11  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) )  =  ( y  e.  CC  |->  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y ) ) )
186185oveq2d 5874 . . . . . . . . . 10  |-  ( ph  ->  ( CC  _D  (
( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) )  =  ( CC  _D  ( y  e.  CC  |->  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y ) ) ) )
187183, 184, 1863eqtr3rd 2324 . . . . . . . . 9  |-  ( ph  ->  ( CC  _D  (
y  e.  CC  |->  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y ) ) )  =  ( y  e.  CC  |->  ( ( ( CC  D n T ) `  ( N  -  M )
) `  y )
) )
188129, 20, 166, 168, 171, 162, 187dvmptres3 19305 . . . . . . . 8  |-  ( ph  ->  ( RR  _D  (
y  e.  RR  |->  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y ) ) )  =  ( y  e.  RR  |->  ( ( ( CC  D n T ) `  ( N  -  M )
) `  y )
) )
18920, 156, 163, 188, 1, 130, 129, 136dvmptres 19312 . . . . . . 7  |-  ( ph  ->  ( RR  _D  (
y  e.  A  |->  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y ) ) )  =  ( y  e.  A  |->  ( ( ( CC  D n T ) `  ( N  -  M )
) `  y )
) )
19020, 139, 144, 152, 153, 155, 189dvmptsub 19316 . . . . . 6  |-  ( ph  ->  ( RR  _D  (
y  e.  A  |->  ( ( ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y ) ) ) )  =  ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  M ) ) `
 y )  -  ( ( ( CC  D n T ) `
 ( N  -  M ) ) `  y ) ) ) )
191190dmeqd 4881 . . . . 5  |-  ( ph  ->  dom  ( RR  _D  ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 y )  -  ( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) `  y ) ) ) )  =  dom  (
y  e.  A  |->  ( ( ( ( RR  D n F ) `
 ( N  -  M ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  M )
) `  y )
) ) )
192 ovex 5883 . . . . . 6  |-  ( ( ( ( RR  D n F ) `  ( N  -  M )
) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  M ) ) `
 y ) )  e.  _V
193 eqid 2283 . . . . . 6  |-  ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  M )
) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  M ) ) `
 y ) ) )  =  ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  M )
) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  M ) ) `
 y ) ) )
194192, 193dmmpti 5373 . . . . 5  |-  dom  (
y  e.  A  |->  ( ( ( ( RR  D n F ) `
 ( N  -  M ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  M )
) `  y )
) )  =  A
195191, 194syl6eq 2331 . . . 4  |-  ( ph  ->  dom  ( RR  _D  ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 y )  -  ( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) `  y ) ) ) )  =  A )
196138, 195syl5sseqr 3227 . . 3  |-  ( ph  ->  ( A  \  { B } )  C_  dom  ( RR  _D  (
y  e.  A  |->  ( ( ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y ) ) ) ) )
197 simpr 447 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  CC )  ->  y  e.  CC )
19853adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  CC )  ->  B  e.  RR )
199198recnd 8861 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  CC )  ->  B  e.  CC )
200197, 199subcld 9157 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  CC )  ->  ( y  -  B )  e.  CC )
20189adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  CC )  ->  M  e. 
NN0 )
2023a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  CC )  ->  1  e. 
NN0 )
203201, 202nn0addcld 10022 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  CC )  ->  ( M  +  1 )  e. 
NN0 )
204200, 203expcld 11245 . . . . . . . 8  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( y  -  B ) ^ ( M  + 
1 ) )  e.  CC )
205157, 204sylan2 460 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( y  -  B ) ^ ( M  + 
1 ) )  e.  CC )
206101adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  CC )  ->  M  e.  CC )
207102a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  CC )  ->  1  e.  CC )
208206, 207addcld 8854 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  CC )  ->  ( M  +  1 )  e.  CC )
209200, 201expcld 11245 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( y  -  B ) ^ M )  e.  CC )
210208, 209mulcld 8855 . . . . . . . 8  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) )  e.  CC )
211157, 210sylan2 460 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) )  e.  CC )
21221prid2 3735 . . . . . . . . . . 11  |-  CC  e.  { RR ,  CC }
213212a1i 10 . . . . . . . . . 10  |-  ( ph  ->  CC  e.  { RR ,  CC } )
214 simpr 447 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  CC )  ->  x  e.  CC )
215 elfznn 10819 . . . . . . . . . . . . . 14  |-  ( ( M  +  1 )  e.  ( 1 ... N )  ->  ( M  +  1 )  e.  NN )
21610, 215syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( M  +  1 )  e.  NN )
217216nnnn0d 10018 . . . . . . . . . . . 12  |-  ( ph  ->  ( M  +  1 )  e.  NN0 )
218217adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  CC )  ->  ( M  +  1 )  e. 
NN0 )
219214, 218expcld 11245 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  CC )  ->  ( x ^ ( M  + 
1 ) )  e.  CC )
220 ovex 5883 . . . . . . . . . . 11  |-  ( ( M  +  1 )  x.  ( x ^ M ) )  e. 
_V
221220a1i 10 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  CC )  ->  ( ( M  +  1 )  x.  ( x ^ M ) )  e. 
_V )
222213dvmptid 19306 . . . . . . . . . . . 12  |-  ( ph  ->  ( CC  _D  (
y  e.  CC  |->  y ) )  =  ( y  e.  CC  |->  1 ) )
223 0cn 8831 . . . . . . . . . . . . 13  |-  0  e.  CC
224223a1i 10 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  CC )  ->  0  e.  CC )
22553recnd 8861 . . . . . . . . . . . . 13  |-  ( ph  ->  B  e.  CC )
226213, 225dvmptc 19307 . . . . . . . . . . . 12  |-  ( ph  ->  ( CC  _D  (
y  e.  CC  |->  B ) )  =  ( y  e.  CC  |->  0 ) )
227213, 197, 207, 222, 199, 224, 226dvmptsub 19316 . . . . . . . . . . 11  |-  ( ph  ->  ( CC  _D  (
y  e.  CC  |->  ( y  -  B ) ) )  =  ( y  e.  CC  |->  ( 1  -  0 ) ) )
228102subid1i 9118 . . . . . . . . . . . 12  |-  ( 1  -  0 )  =  1
229228mpteq2i 4103 . . . . . . . . . . 11  |-  ( y  e.  CC  |->  ( 1  -  0 ) )  =  ( y  e.  CC  |->  1 )
230227, 229syl6eq 2331 . . . . . . . . . 10  |-  ( ph  ->  ( CC  _D  (
y  e.  CC  |->  ( y  -  B ) ) )  =  ( y  e.  CC  |->  1 ) )
231 dvexp 19302 . . . . . . . . . . . 12  |-  ( ( M  +  1 )  e.  NN  ->  ( CC  _D  ( x  e.  CC  |->  ( x ^
( M  +  1 ) ) ) )  =  ( x  e.  CC  |->  ( ( M  +  1 )  x.  ( x ^ (
( M  +  1 )  -  1 ) ) ) ) )
232216, 231syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( CC  _D  (
x  e.  CC  |->  ( x ^ ( M  +  1 ) ) ) )  =  ( x  e.  CC  |->  ( ( M  +  1 )  x.  ( x ^ ( ( M  +  1 )  - 
1 ) ) ) ) )
233101, 103pncand 9158 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( M  + 
1 )  -  1 )  =  M )
234233oveq2d 5874 . . . . . . . . . . . . 13  |-  ( ph  ->  ( x ^ (
( M  +  1 )  -  1 ) )  =  ( x ^ M ) )
235234oveq2d 5874 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( M  + 
1 )  x.  (
x ^ ( ( M  +  1 )  -  1 ) ) )  =  ( ( M  +  1 )  x.  ( x ^ M ) ) )
236235mpteq2dv 4107 . . . . . . . . . . 11  |-  ( ph  ->  ( x  e.  CC  |->  ( ( M  + 
1 )  x.  (
x ^ ( ( M  +  1 )  -  1 ) ) ) )  =  ( x  e.  CC  |->  ( ( M  +  1 )  x.  ( x ^ M ) ) ) )
237232, 236eqtrd 2315 . . . . . . . . . 10  |-  ( ph  ->  ( CC  _D  (
x  e.  CC  |->  ( x ^ ( M  +  1 ) ) ) )  =  ( x  e.  CC  |->  ( ( M  +  1 )  x.  ( x ^ M ) ) ) )
238 oveq1 5865 . . . . . . . . . 10  |-  ( x  =  ( y  -  B )  ->  (
x ^ ( M  +  1 ) )  =  ( ( y  -  B ) ^
( M  +  1 ) ) )
239 oveq1 5865 . . . . . . . . . . 11  |-  ( x  =  ( y  -  B )  ->  (
x ^ M )  =  ( ( y  -  B ) ^ M ) )
240239oveq2d 5874 . . . . . . . . . 10  |-  ( x  =  ( y  -  B )  ->  (
( M  +  1 )  x.  ( x ^ M ) )  =  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M
) ) )
241213, 213, 200, 207, 219, 221, 230, 237, 238, 240dvmptco 19321 . . . . . . . . 9  |-  ( ph  ->  ( CC  _D  (
y  e.  CC  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) ) )  =  ( y  e.  CC  |->  ( ( ( M  + 
1 )  x.  (
( y  -  B
) ^ M ) )  x.  1 ) ) )
242210mulid1d 8852 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) )  x.  1 )  =  ( ( M  + 
1 )  x.  (
( y  -  B
) ^ M ) ) )
243242mpteq2dva 4106 . . . . . . . . 9  |-  ( ph  ->  ( y  e.  CC  |->  ( ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M
) )  x.  1 ) )  =  ( y  e.  CC  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) ) )
244241, 243eqtrd 2315 . . . . . . . 8  |-  ( ph  ->  ( CC  _D  (
y  e.  CC  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) ) )  =  ( y  e.  CC  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) ) )
245129, 20, 166, 168, 204, 210, 244dvmptres3 19305 . . . . . . 7  |-  ( ph  ->  ( RR  _D  (
y  e.  RR  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) ) )  =  ( y  e.  RR  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) ) )
24620, 205, 211, 245, 1, 130, 129, 136dvmptres 19312 . . . . . 6  |-  ( ph  ->  ( RR  _D  (
y  e.  A  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) ) )  =  ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) ) )
247246dmeqd 4881 . . . . 5  |-  ( ph  ->  dom  ( RR  _D  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) ) )  =  dom  ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M
) ) ) )
248 ovex 5883 . . . . . 6  |-  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) )  e. 
_V
249 eqid 2283 . . . . . 6  |-  ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) )  =  ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M
) ) )
250248, 249dmmpti 5373 . . . . 5  |-  dom  (
y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) )  =  A
251247, 250syl6eq 2331 . . . 4  |-  ( ph  ->  dom  ( RR  _D  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) ) )  =  A )
252138, 251syl5sseqr 3227 . . 3  |-  ( ph  ->  ( A  \  { B } )  C_  dom  ( RR  _D  (
y  e.  A  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) ) ) )
25320, 26, 1, 13, 51, 52dvntaylp0 19751 . . . . . 6  |-  ( ph  ->  ( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) `  B )  =  ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  B ) )
254253oveq2d 5874 . . . . 5  |-  ( ph  ->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 B )  -  ( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) `  B ) )  =  ( ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 B )  -  ( ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) ) `  B ) ) )
255128, 50ffvelrnd 5666 . . . . . 6  |-  ( ph  ->  ( ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) ) `  B )  e.  CC )
256255subidd 9145 . . . . 5  |-  ( ph  ->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 B )  -  ( ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) ) `  B ) )  =  0 )
257254, 256eqtrd 2315 . . . 4  |-  ( ph  ->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 B )  -  ( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) `  B ) )  =  0 )
258129subcn 18370 . . . . . . 7  |-  -  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) )
259258a1i 10 . . . . . 6  |-  ( ph  ->  -  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)  Cn  ( TopOpen ` fld )
) )
260 dvcn 19270 . . . . . . . 8  |-  ( ( ( RR  C_  CC  /\  ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) : A --> CC  /\  A  C_  RR )  /\  dom  ( RR  _D  (
( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) )  =  A )  ->  ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) )  e.  ( A -cn-> CC ) )
261106, 128, 1, 126, 260syl31anc 1185 . . . . . . 7  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) )  e.  ( A
-cn-> CC ) )
262150, 261eqeltrrd 2358 . . . . . 6  |-  ( ph  ->  ( y  e.  A  |->  ( ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) ) `  y ) )  e.  ( A -cn-> CC ) )
263 plycn 19642 . . . . . . . 8  |-  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) )  e.  (Poly `  RR )  ->  ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) )  e.  ( CC -cn-> CC ) )
26474, 263syl 15 . . . . . . 7  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) )  e.  ( CC
-cn-> CC ) )
2651, 24syl6ss 3191 . . . . . . . 8  |-  ( ph  ->  A  C_  CC )
266 cncfmptid 18416 . . . . . . . 8  |-  ( ( A  C_  CC  /\  CC  C_  CC )  ->  (
y  e.  A  |->  y )  e.  ( A
-cn-> CC ) )
267265, 174, 266syl2anc 642 . . . . . . 7  |-  ( ph  ->  ( y  e.  A  |->  y )  e.  ( A -cn-> CC ) )
268264, 267cncfmpt1f 18417 . . . . . 6  |-  ( ph  ->  ( y  e.  A  |->  ( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) `  y ) )  e.  ( A -cn-> CC ) )
269129, 259, 262, 268cncfmpt2f 18418 . . . . 5  |-  ( ph  ->  ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 y )  -  ( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) `  y ) ) )  e.  ( A -cn-> CC ) )
270 fveq2 5525 . . . . . 6  |-  ( y  =  B  ->  (
( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  y )  =  ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 B ) )
271 fveq2 5525 . . . . . 6  |-  ( y  =  B  ->  (
( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y )  =  ( ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) `
 B ) )
272270, 271oveq12d 5876 . . . . 5  |-  ( y  =  B  ->  (
( ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y ) )  =  ( ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  B )  -  ( ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) `
 B ) ) )
273269, 50, 272cnmptlimc 19240 . . . 4  |-  ( ph  ->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 B )  -  ( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) `  B ) )  e.  ( ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) `
 y ) ) ) lim CC  B ) )
274257, 273eqeltrrd 2358 . . 3  |-  ( ph  ->  0  e.  ( ( y  e.  A  |->  ( ( ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y ) ) ) lim CC  B
) )
275225subidd 9145 . . . . . 6  |-  ( ph  ->  ( B  -  B
)  =  0 )
276275oveq1d 5873 . . . . 5  |-  ( ph  ->  ( ( B  -  B ) ^ ( M  +  1 ) )  =  ( 0 ^ ( M  + 
1 ) ) )
2772160expd 11261 . . . . 5  |-  ( ph  ->  ( 0 ^ ( M  +  1 ) )  =  0 )
278276, 277eqtrd 2315 . . . 4  |-  ( ph  ->  ( ( B  -  B ) ^ ( M  +  1 ) )  =  0 )
279265sselda 3180 . . . . . . . 8  |-  ( (
ph  /\  y  e.  A )  ->  y  e.  CC )
280279, 204syldan 456 . . . . . . 7  |-  ( (
ph  /\  y  e.  A )  ->  (
( y  -  B
) ^ ( M  +  1 ) )  e.  CC )
281280, 94fmptd 5684 . . . . . 6  |-  ( ph  ->  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) ) : A --> CC )
282 dvcn 19270 . . . . . 6  |-  ( ( ( RR  C_  CC  /\  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) ) : A --> CC  /\  A  C_  RR )  /\  dom  ( RR 
_D  ( y  e.  A  |->  ( ( y  -  B ) ^
( M  +  1 ) ) ) )  =  A )  -> 
( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) )  e.  ( A -cn-> CC ) )
283106, 281, 1, 251, 282syl31anc 1185 . . . . 5  |-  ( ph  ->  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) )  e.  ( A -cn-> CC ) )
284 oveq1 5865 . . . . . 6  |-  ( y  =  B  ->  (
y  -  B )  =  ( B  -  B ) )
285284oveq1d 5873 . . . . 5  |-  ( y  =  B  ->  (
( y  -  B
) ^ ( M  +  1 ) )  =  ( ( B  -  B ) ^
( M  +  1 ) ) )
286283, 50, 285cnmptlimc 19240 . . . 4  |-  ( ph  ->  ( ( B  -  B ) ^ ( M  +  1 ) )  e.  ( ( y  e.  A  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) ) lim CC  B ) )
287278, 286eqeltrrd 2358 . . 3  |-  ( ph  ->  0  e.  ( ( y  e.  A  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) ) lim CC  B ) )
288138, 265syl5ss 3190 . . . . . . . . . 10  |-  ( ph  ->  ( A  \  { B } )  C_  CC )
289288sselda 3180 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
y  e.  CC )
290225adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  ->  B  e.  CC )
291289, 290subcld 9157 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( y  -  B
)  e.  CC )
292 eldifsni 3750 . . . . . . . . . 10  |-  ( y  e.  ( A  \  { B } )  -> 
y  =/=  B )
293292adantl 452 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
y  =/=  B )
294 subeq0 9073 . . . . . . . . . . 11  |-  ( ( y  e.  CC  /\  B  e.  CC )  ->  ( ( y  -  B )  =  0  <-> 
y  =  B ) )
295289, 290, 294syl2anc 642 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( ( y  -  B )  =  0  <-> 
y  =  B ) )
296295necon3bid 2481 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( ( y  -  B )  =/=  0  <->  y  =/=  B ) )
297293, 296mpbird 223 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( y  -  B
)  =/=  0 )
298216adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( M  +  1 )  e.  NN )
299298nnzd 10116 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( M  +  1 )  e.  ZZ )
300291, 297, 299expne0d 11251 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( ( y  -  B ) ^ ( M  +  1 ) )  =/=  0 )
301300necomd 2529 . . . . . 6  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
0  =/=  ( ( y  -  B ) ^ ( M  + 
1 ) ) )
302301neneqd 2462 . . . . 5  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  ->  -.  0  =  (
( y  -  B
) ^ ( M  +  1 ) ) )
303302nrexdv 2646 . . . 4  |-  ( ph  ->  -.  E. y  e.  ( A  \  { B } ) 0  =  ( ( y  -  B ) ^ ( M  +  1 ) ) )
304 df-ima 4702 . . . . . 6  |-  ( ( y  e.  A  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) ) " ( A 
\  { B }
) )  =  ran  ( ( y  e.  A  |->  ( ( y  -  B ) ^
( M  +  1 ) ) )  |`  ( A  \  { B } ) )
305304eleq2i 2347 . . . . 5  |-  ( 0  e.  ( ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  + 
1 ) ) )
" ( A  \  { B } ) )  <->  0  e.  ran  (
( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) )  |`  ( A  \  { B }
) ) )
306 resmpt 5000 . . . . . . 7  |-  ( ( A  \  { B } )  C_  A  ->  ( ( y  e.  A  |->  ( ( y  -  B ) ^
( M  +  1 ) ) )  |`  ( A  \  { B } ) )  =  ( y  e.  ( A  \  { B } )  |->  ( ( y  -  B ) ^ ( M  + 
1 ) ) ) )
307138, 306ax-mp 8 . . . . . 6  |-  ( ( y  e.  A  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) )  |`  ( A  \  { B } ) )  =  ( y  e.  ( A  \  { B } )  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) )
308 ovex 5883 . . . . . 6  |-  ( ( y  -  B ) ^ ( M  + 
1 ) )  e. 
_V
309307, 308elrnmpti 4930 . . . . 5  |-  ( 0  e.  ran  ( ( y  e.  A  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) )  |`  ( A  \  { B } ) )  <->  E. y  e.  ( A  \  { B } ) 0  =  ( ( y  -  B ) ^ ( M  +  1 ) ) )
310305, 309bitri 240 . . . 4  |-  ( 0  e.  ( ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  + 
1 ) ) )
" ( A  \  { B } ) )  <->  E. y  e.  ( A  \  { B }
) 0  =  ( ( y  -  B
) ^ ( M  +  1 ) ) )
311303, 310sylnibr 296 . . 3  |-  ( ph  ->  -.  0  e.  ( ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) ) " ( A  \  { B }
) ) )
312101adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  ->  M  e.  CC )
313102a1i 10 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
1  e.  CC )
314312, 313addcld 8854 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( M  +  1 )  e.  CC )
315289, 209syldan 456 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( ( y  -  B ) ^ M
)  e.  CC )
316298nnne0d 9790 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( M  +  1 )  =/=  0 )
31788adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  ->  M  e.  NN )
318317nnzd 10116 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  ->  M  e.  ZZ )
319291, 297, 318expne0d 11251 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( ( y  -  B ) ^ M
)  =/=  0 )
320314, 315, 316, 319mulne0d 9420 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( ( M  + 
1 )  x.  (
( y  -  B
) ^ M ) )  =/=  0 )
321320necomd 2529 . . . . . 6  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
0  =/=  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) )
322321neneqd 2462 . . . . 5  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  ->  -.  0  =  (
( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) )
323322nrexdv 2646 . . . 4  |-  ( ph  ->  -.  E. y  e.  ( A  \  { B } ) 0  =  ( ( M  + 
1 )  x.  (
( y  -  B
) ^ M ) ) )
324246imaeq1d 5011 . . . . . . 7  |-  ( ph  ->  ( ( RR  _D  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) ) ) "
( A  \  { B } ) )  =  ( ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M
) ) ) "
( A  \  { B } ) ) )
325 df-ima 4702 . . . . . . 7  |-  ( ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) ) " ( A 
\  { B }
) )  =  ran  ( ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M
) ) )  |`  ( A  \  { B } ) )
326324, 325syl6eq 2331 . . . . . 6  |-  ( ph  ->  ( ( RR  _D  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) ) ) "
( A  \  { B } ) )  =  ran  ( ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) )  |`  ( A  \  { B } ) ) )
327326eleq2d 2350 . . . . 5  |-  ( ph  ->  ( 0  e.  ( ( RR  _D  (
y  e.  A  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) ) ) " ( A  \  { B }
) )  <->  0  e.  ran  ( ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M
) ) )  |`  ( A  \  { B } ) ) ) )
328 resmpt 5000 . . . . . . 7  |-  ( ( A  \  { B } )  C_  A  ->  ( ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M
) ) )  |`  ( A  \  { B } ) )  =  ( y  e.  ( A  \  { B } )  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) ) )
329138, 328ax-mp 8 . . . . . 6  |-  ( ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) )  |`  ( A  \  { B } ) )  =  ( y  e.  ( A  \  { B } )  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) )
330329, 248elrnmpti 4930 . . . . 5  |-  ( 0  e.  ran  ( ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) )  |`  ( A  \  { B } ) )  <->  E. y  e.  ( A  \  { B } ) 0  =  ( ( M  + 
1 )  x.  (
( y  -  B
) ^ M ) ) )
331327, 330syl6bb 252 . . . 4  |-  ( ph  ->  ( 0  e.  ( ( RR  _D  (
y  e.  A  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) ) ) " ( A  \  { B }
) )  <->  E. y  e.  ( A  \  { B } ) 0  =  ( ( M  + 
1 )  x.  (
( y  -  B
) ^ M ) ) ) )
332323, 331mtbird 292 . . 3  |-  ( ph  ->  -.  0  e.  ( ( RR  _D  (
y  e.  A  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) ) ) " ( A  \  { B }
) ) )
333216nnrecred 9791 . . . . . . 7  |-  ( ph  ->  ( 1  /  ( M  +  1 ) )  e.  RR )
334333recnd 8861 . . . . . 6  |-  ( ph  ->  ( 1  /  ( M  +  1 ) )  e.  CC )
335334mul02d 9010 . . . . 5  |-  ( ph  ->  ( 0  x.  (
1  /  ( M  +  1 ) ) )  =  0 )
336 eldifi 3298 . . . . . . . . 9  |-  ( x  e.  ( A  \  { B } )  ->  x  e.  A )
337143ffvelrnda 5665 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( RR  D n F ) `  ( N  -  M )
) `  x )  e.  CC )
338336, 337sylan2 460 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( ( RR  D n F ) `
 ( N  -  M ) ) `  x )  e.  CC )
339138, 1syl5ss 3190 . . . . . . . . . . 11  |-  ( ph  ->  ( A  \  { B } )  C_  RR )
340339sselda 3180 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  x  e.  RR )
341340recnd 8861 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  x  e.  CC )
342161ffvelrnda 5665 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  CC )  ->  ( ( ( CC  D n T ) `  ( N  -  M )
) `  x )  e.  CC )
343341, 342syldan 456 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( ( CC  D n T ) `
 ( N  -  M ) ) `  x )  e.  CC )
344338, 343subcld 9157 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( ( ( RR  D n F ) `  ( N  -  M ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  M ) ) `  x ) )  e.  CC )
34553adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  B  e.  RR )
346340, 345resubcld 9211 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( x  -  B
)  e.  RR )
34789adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  M  e.  NN0 )
348346, 347reexpcld 11262 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( x  -  B ) ^ M
)  e.  RR )
349348recnd 8861 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( x  -  B ) ^ M
)  e.  CC )
350345recnd 8861 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  B  e.  CC )
351341, 350subcld 9157 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( x  -  B
)  e.  CC )
352 eldifsni 3750 . . . . . . . . . 10  |-  ( x  e.  ( A  \  { B } )  ->  x  =/=  B )
353352adantl 452 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  x  =/=  B )
354 subeq0 9073 . . . . . . . . . . 11  |-  ( ( x  e.  CC  /\  B  e.  CC )  ->  ( ( x  -  B )  =  0  <-> 
x  =  B ) )
355341, 350, 354syl2anc 642 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( x  -  B )  =  0  <-> 
x  =  B ) )
356355necon3bid 2481 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( x  -  B )  =/=  0  <->  x  =/=  B ) )
357353, 356mpbird 223 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( x  -  B
)  =/=  0 )
358347nn0zd 10115 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  M  e.  ZZ )
359351, 357, 358expne0d 11251 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( x  -  B ) ^ M
)  =/=  0 )
360344, 349, 359divcld 9536 . . . . . 6  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( ( ( ( RR  D n F ) `  ( N  -  M )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  M ) ) `
 x ) )  /  ( ( x  -  B ) ^ M ) )  e.  CC )
361334adantr 451 . . . . . 6  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( 1  /  ( M  +  1 ) )  e.  CC )
362 txtopon 17286 . . . . . . . . 9  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  ( TopOpen
` fld
)  e.  (TopOn `  CC ) )  ->  (
( TopOpen ` fld )  tX  ( TopOpen ` fld )
)  e.  (TopOn `  ( CC  X.  CC ) ) )
363164, 164, 362mp2an 653 . . . . . . . 8  |-  ( (
TopOpen ` fld )  tX  ( TopOpen ` fld )
)  e.  (TopOn `  ( CC  X.  CC ) )
364363toponunii 16670 . . . . . . . . 9  |-  ( CC 
X.  CC )  = 
U. ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )
365364restid 13338 . . . . . . . 8  |-  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)  e.  (TopOn `  ( CC  X.  CC ) )  ->  (
( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)t  ( CC  X.  CC ) )  =  ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
) )
366363, 365ax-mp 8 . . . . . . 7  |-  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)t  ( CC  X.  CC ) )  =  ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)
367366eqcomi 2287 . . . . . 6  |-  ( (
TopOpen ` fld )  tX  ( TopOpen ` fld )
)  =  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)t  ( CC  X.  CC ) )
368 taylthlem2.i . . . . . 6  |-  ( ph  ->  0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( RR  D n F ) `  ( N  -  M )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  M ) ) `
 x ) )  /  ( ( x  -  B ) ^ M ) ) ) lim
CC  B ) )
369 limcresi 19235 . . . . . . . 8  |-  ( ( x  e.  A  |->  ( 1  /  ( M  +  1 ) ) ) lim CC  B ) 
C_  ( ( ( x  e.  A  |->  ( 1  /  ( M  +  1 ) ) )  |`  ( A  \  { B } ) ) lim CC  B )
370 resmpt 5000 . . . . . . . . . 10  |-  ( ( A  \  { B } )  C_  A  ->  ( ( x  e.  A  |->  ( 1  / 
( M  +  1 ) ) )  |`  ( A  \  { B } ) )  =  ( x  e.  ( A  \  { B } )  |->  ( 1  /  ( M  + 
1 ) ) ) )
371138, 370ax-mp 8 . . . . . . . . 9  |-  ( ( x  e.  A  |->  ( 1  /  ( M  +  1 ) ) )  |`  ( A  \  { B } ) )  =  ( x  e.  ( A  \  { B } )  |->  ( 1  /  ( M  +  1 ) ) )
372371oveq1i 5868 . . . . . . . 8  |-  ( ( ( x  e.  A  |->  ( 1  /  ( M  +  1 ) ) )  |`  ( A  \  { B }
) ) lim CC  B
)  =  ( ( x  e.  ( A 
\  { B }
)  |->  ( 1  / 
( M  +  1 ) ) ) lim CC  B )
373369, 372sseqtri 3210 . . . . . . 7  |-  ( ( x  e.  A  |->  ( 1  /  ( M  +  1 ) ) ) lim CC  B ) 
C_  ( ( x  e.  ( A  \  { B } )  |->  ( 1  /  ( M  +  1 ) ) ) lim CC  B )
374 cncfmptc 18415 . . . . . . . . 9  |-  ( ( ( 1  /  ( M  +  1 ) )  e.  RR  /\  A  C_  CC  /\  RR  C_  CC )  ->  (
x  e.  A  |->  ( 1  /  ( M  +  1 ) ) )  e.  ( A
-cn-> RR ) )
375333, 265, 106, 374syl3anc 1182 . . . . . . . 8  |-  ( ph  ->  ( x  e.  A  |->  ( 1  /  ( M  +  1 ) ) )  e.  ( A -cn-> RR ) )
376 eqidd 2284 . . . . . . . 8  |-  ( x  =  B  ->  (
1  /  ( M  +  1 ) )  =  ( 1  / 
( M  +  1 ) ) )
377375, 50, 376cnmptlimc 19240 . . . . . . 7  |-  ( ph  ->  ( 1  /  ( M  +  1 ) )  e.  ( ( x  e.  A  |->  ( 1  /  ( M  +  1 ) ) ) lim CC  B ) )
378373, 377sseldi 3178 . . . . . 6  |-  ( ph  ->  ( 1  /  ( M  +  1 ) )  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( 1  / 
( M  +  1 ) ) ) lim CC  B ) )
379129mulcn 18371 . . . . . . 7  |-  x.  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) )
380 opelxpi 4721 . . . . . . . 8  |-  ( ( 0  e.  CC  /\  ( 1  /  ( M  +  1 ) )  e.  CC )  ->  <. 0 ,  ( 1  /  ( M  +  1 ) )
>.  e.  ( CC  X.  CC ) )
381223, 334, 380sylancr 644 . . . . . . 7  |-  ( ph  -> 
<. 0 ,  ( 1  /  ( M  +  1 ) )
>.  e.  ( CC  X.  CC ) )
382364cncnpi 17007 . . . . . . 7  |-  ( (  x.  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)  Cn  ( TopOpen ` fld )
)  /\  <. 0 ,  ( 1  /  ( M  +  1 ) ) >.  e.  ( CC  X.  CC ) )  ->  x.  e.  ( ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  CnP  ( TopOpen
` fld
) ) `  <. 0 ,  ( 1  /  ( M  + 
1 ) ) >.
) )
383379, 381, 382sylancr 644 . . . . . 6  |-  ( ph  ->  x.  e.  ( ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)  CnP  ( TopOpen ` fld )
) `  <. 0 ,  ( 1  /  ( M  +  1 ) ) >. ) )
384360, 361, 174, 174, 129, 367, 368, 378, 383limccnp2 19242 . . . . 5  |-  ( ph  ->  ( 0  x.  (
1  /  ( M  +  1 ) ) )  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( ( RR  D n F ) `
 ( N  -  M ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  M )
) `  x )
)  /  ( ( x  -  B ) ^ M ) )  x.  ( 1  / 
( M  +  1 ) ) ) ) lim
CC  B ) )
385335, 384eqeltrrd 2358 . . . 4  |-  ( ph  ->  0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( ( RR  D n F ) `
 ( N  -  M ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  M )
) `  x )
)  /  ( ( x  -  B ) ^ M ) )  x.  ( 1  / 
( M  +  1 ) ) ) ) lim
CC  B ) )
386190fveq1d 5527 . . . . . . . . 9  |-  ( ph  ->  ( ( RR  _D  ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 y )  -  ( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) `  y ) ) ) ) `  x )  =  ( ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  M )
) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  M ) ) `
 y ) ) ) `  x ) )
387 fveq2 5525 . . . . . . . . . . . 12  |-  ( y  =  x  ->  (
( ( RR  D n F ) `  ( N  -  M )
) `  y )  =  ( ( ( RR  D n F ) `  ( N  -  M ) ) `
 x ) )
388 fveq2 5525 . . . . . . . . . . . 12  |-  ( y  =  x  ->  (
( ( CC  D n T ) `  ( N  -  M )
) `  y )  =  ( ( ( CC  D n T ) `  ( N  -  M ) ) `
 x ) )
389387, 388oveq12d 5876 . . . . . . . . . . 11  |-  ( y  =  x  ->  (
( ( ( RR  D n F ) `
 ( N  -  M ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  M )
) `  y )
)  =  ( ( ( ( RR  D n F ) `  ( N  -  M )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  M ) ) `
 x ) ) )
390 ovex 5883 . . . . . . . . . . 11  |-  ( ( ( ( RR  D n F ) `  ( N  -  M )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  M ) ) `
 x ) )  e.  _V
391389, 193, 390fvmpt 5602 . . . . . . . . . 10  |-  ( x  e.  A  ->  (
( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  M ) ) `
 y )  -  ( ( ( CC  D n T ) `
 ( N  -  M ) ) `  y ) ) ) `
 x )  =  ( ( ( ( RR  D n F ) `  ( N  -  M ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  M ) ) `  x ) ) )
392336, 391syl 15 . . . . . . . . 9  |-  ( x  e.  ( A  \  { B } )  -> 
( ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  M )
) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  M ) ) `
 y ) ) ) `  x )  =  ( ( ( ( RR  D n F ) `  ( N  -  M )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  M ) ) `
 x ) ) )
393386, 392sylan9eq 2335 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( RR  _D  ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 y )  -  ( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) `  y ) ) ) ) `  x )  =  ( ( ( ( RR  D n F ) `  ( N  -  M )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  M ) ) `
 x ) ) )
394246fveq1d 5527 . . . . . . . . . 10  |-  ( ph  ->  ( ( RR  _D  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) ) ) `  x )  =  ( ( y  e.  A  |->  ( ( M  + 
1 )  x.  (
( y  -  B
) ^ M ) ) ) `  x
) )
395 oveq1 5865 . . . . . . . . . . . . . 14  |-  ( y  =  x  ->  (
y  -  B )  =  ( x  -  B ) )
396395oveq1d 5873 . . . . . . . . . . . . 13  |-  ( y  =  x  ->  (
( y  -  B
) ^ M )  =  ( ( x  -  B ) ^ M ) )
397396oveq2d 5874 . . . . . . . . . . . 12  |-  ( y  =  x  ->  (
( M  +  1 )  x.  ( ( y  -  B ) ^ M ) )  =  ( ( M  +  1 )  x.  ( ( x  -  B ) ^ M
) ) )
398 ovex 5883 . . . . . . . . . . . 12  |-  ( ( M  +  1 )  x.  ( ( x  -  B ) ^ M ) )  e. 
_V
399397, 249, 398fvmpt 5602 . . . . . . . . . . 11  |-  ( x  e.  A  ->  (
( y  e.  A  |->  ( ( M  + 
1 )  x.  (
( y  -  B
) ^ M ) ) ) `  x
)  =  ( ( M  +  1 )  x.  ( ( x  -  B ) ^ M ) ) )
400336, 399syl 15 . . . . . . . . . 10  |-  ( x  e.  ( A  \  { B } )  -> 
( ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M
) ) ) `  x )  =  ( ( M  +  1 )  x.  ( ( x  -  B ) ^ M ) ) )
401394, 400sylan9eq 2335 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( RR  _D  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) ) ) `  x )  =  ( ( M  +  1 )  x.  ( ( x  -  B ) ^ M ) ) )
402216adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( M  +  1 )  e.  NN )
403402nncnd 9762 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( M  +  1 )  e.  CC )
404403, 349mulcomd 8856 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( M  + 
1 )  x.  (
( x  -  B
) ^ M ) )  =  ( ( ( x  -  B
) ^ M )  x.  ( M  + 
1 ) ) )
405401, 404eqtrd 2315 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( RR  _D  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) ) ) `  x )  =  ( ( ( x  -  B ) ^ M
)  x.  ( M  +  1 ) ) )
406393, 405oveq12d 5876 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( ( RR 
_D  ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) `
 y ) ) ) ) `  x
)  /  ( ( RR  _D  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  + 
1 ) ) ) ) `  x ) )  =  ( ( ( ( ( RR  D n F ) `
 ( N  -  M ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  M )
) `  x )
)  /  ( ( ( x  -  B
) ^ M )  x.  ( M  + 
1 ) ) ) )
407402nnne0d 9790 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( M  +  1 )  =/=  0 )
408344, 349, 403, 359, 407divdiv1d 9567 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( ( ( ( ( RR  D n F ) `  ( N  -  M )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  M ) ) `
 x ) )  /  ( ( x  -  B ) ^ M ) )  / 
( M  +  1 ) )  =  ( ( ( ( ( RR  D n F ) `  ( N  -  M ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  M ) ) `  x ) )  / 
( ( ( x  -  B ) ^ M )  x.  ( M  +  1 ) ) ) )
409360, 403, 407divrecd 9539 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( ( ( ( ( RR  D n F ) `  ( N  -  M )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  M ) ) `
 x ) )  /  ( ( x  -  B ) ^ M ) )  / 
( M  +  1 ) )  =  ( ( ( ( ( ( RR  D n F ) `  ( N  -  M )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  M ) ) `
 x ) )  /  ( ( x  -  B ) ^ M ) )  x.  ( 1  /  ( M  +  1 ) ) ) )
410406, 408, 4093eqtr2rd 2322 . . . . . 6  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( ( ( ( ( RR  D n F ) `  ( N  -  M )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  M ) ) `
 x ) )  /  ( ( x  -  B ) ^ M ) )  x.  ( 1  /  ( M  +  1 ) ) )  =  ( ( ( RR  _D  ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 y )  -  ( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) `  y ) ) ) ) `  x )  /  ( ( RR 
_D  ( y  e.  A  |->  ( ( y  -  B ) ^
( M  +  1 ) ) ) ) `
 x ) ) )
411410mpteq2dva 4106 . . . . 5  |-  ( ph  ->  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( ( RR  D n F ) `  ( N  -  M ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  M ) ) `  x ) )  / 
( ( x  -  B ) ^ M
) )  x.  (
1  /  ( M  +  1 ) ) ) )  =  ( x  e.  ( A 
\  { B }
)  |->  ( ( ( RR  _D  ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) `
 y ) ) ) ) `  x
)  /  ( ( RR  _D  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  + 
1 ) ) ) ) `  x ) ) ) )
412411oveq1d 5873 . . . 4  |-  ( ph  ->  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( ( RR  D n F ) `  ( N  -  M ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  M ) ) `  x ) )  / 
( ( x  -  B ) ^ M
) )  x.  (
1  /  ( M  +  1 ) ) ) ) lim CC  B
)  =  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( RR  _D  ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) `
 y ) ) ) ) `  x
)  /  ( ( RR  _D  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  + 
1 ) ) ) ) `  x ) ) ) lim CC  B
) )
413385, 412eleqtrd 2359 . . 3  |-  ( ph  ->  0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( RR  _D  ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) `
 y ) ) ) ) `  x
)  /  ( ( RR  _D  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  + 
1 ) ) ) ) `  x ) ) ) lim CC  B
) )
4141, 82, 95, 136, 50, 137, 196, 252, 274, 287, 311, 332, 413lhop 19363 . 2  |-  ( ph  ->  0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( y  e.  A  |->  ( ( ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y ) ) ) `  x
)  /  ( ( y  e.  A  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) ) `  x ) ) ) lim CC  B
) )
415336adantl 452 . . . . . 6  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  x  e.  A )
416 fveq2 5525 . . . . . . . 8  |-  ( y  =  x  ->  (
( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  y )  =  ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 x ) )
417 fveq2 5525 . . . . . . . 8  |-  ( y  =  x  ->  (
( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y )  =  ( ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) `
 x ) )
418416, 417oveq12d 5876 . . . . . . 7  |-  ( y  =  x  ->  (
( ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y ) )  =  ( ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) `
 x ) ) )
419 ovex 5883 . . . . . . 7  |-  ( ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) `
 x ) )  e.  _V
420418, 81, 419fvmpt 5602 . . . . . 6  |-  ( x  e.  A  ->  (
( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 y )  -  ( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) `  y ) ) ) `
 x )  =  ( ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) `  x ) ) )
421415, 420syl 15 . . . . 5  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) `
 y ) ) ) `  x )  =  ( ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) `
 x ) ) )
422395oveq1d 5873 . . . . . . 7  |-  ( y  =  x  ->  (
( y  -  B
) ^ ( M  +  1 ) )  =  ( ( x  -  B ) ^
( M  +  1 ) ) )
423 ovex 5883 . . . . . . 7  |-  ( ( x  -  B ) ^ ( M  + 
1 ) )  e. 
_V
424422, 94, 423fvmpt 5602 . . . . . 6  |-  ( x  e.  A  ->