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

Theorem taylthlem2 20291
Description: Lemma for taylth 20292. (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 10238 . . . . . . . . . . . . 13  |-  1  e.  NN0
4 nn0uz 10521 . . . . . . . . . . . . 13  |-  NN0  =  ( ZZ>= `  0 )
53, 4eleqtri 2509 . . . . . . . . . . . 12  |-  1  e.  ( ZZ>= `  0 )
6 fzss1 11092 . . . . . . . . . . . 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 11190 . . . . . . . . . . . 12  |-  ( M  e.  ( 1..^ N )  ->  ( M  +  1 )  e.  ( 1 ... N
) )
108, 9syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( M  +  1 )  e.  ( 1 ... N ) )
117, 10sseldi 3347 . . . . . . . . . 10  |-  ( ph  ->  ( M  +  1 )  e.  ( 0 ... N ) )
12 fznn0sub2 11087 . . . . . . . . . 10  |-  ( ( M  +  1 )  e.  ( 0 ... N )  ->  ( N  -  ( M  +  1 ) )  e.  ( 0 ... N ) )
1311, 12syl 16 . . . . . . . . 9  |-  ( ph  ->  ( N  -  ( M  +  1 ) )  e.  ( 0 ... N ) )
14 elfznn0 11084 . . . . . . . . 9  |-  ( ( N  -  ( M  +  1 ) )  e.  ( 0 ... N )  ->  ( N  -  ( M  +  1 ) )  e.  NN0 )
1513, 14syl 16 . . . . . . . 8  |-  ( ph  ->  ( N  -  ( M  +  1 ) )  e.  NN0 )
16 dvnfre 19839 . . . . . . . 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 1185 . . . . . . 7  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) : dom  (
( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) --> RR )
18 reex 9082 . . . . . . . . . . . . 13  |-  RR  e.  _V
1918prid1 3913 . . . . . . . . . . . 12  |-  RR  e.  { RR ,  CC }
2019a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  RR  e.  { RR ,  CC } )
21 cnex 9072 . . . . . . . . . . . . 13  |-  CC  e.  _V
2221a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  CC  e.  _V )
2318a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  RR  e.  _V )
24 ax-resscn 9048 . . . . . . . . . . . . 13  |-  RR  C_  CC
25 fss 5600 . . . . . . . . . . . . 13  |-  ( ( F : A --> RR  /\  RR  C_  CC )  ->  F : A --> CC )
262, 24, 25sylancl 645 . . . . . . . . . . . 12  |-  ( ph  ->  F : A --> CC )
27 elpm2r 7035 . . . . . . . . . . . 12  |-  ( ( ( CC  e.  _V  /\  RR  e.  _V )  /\  ( F : A --> CC  /\  A  C_  RR ) )  ->  F  e.  ( CC  ^pm  RR ) )
2822, 23, 26, 1, 27syl22anc 1186 . . . . . . . . . . 11  |-  ( ph  ->  F  e.  ( CC 
^pm  RR ) )
29 dvnbss 19815 . . . . . . . . . . 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 1185 . . . . . . . . . 10  |-  ( ph  ->  dom  ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) )  C_  dom  F )
31 fdm 5596 . . . . . . . . . . 11  |-  ( F : A --> RR  ->  dom 
F  =  A )
322, 31syl 16 . . . . . . . . . 10  |-  ( ph  ->  dom  F  =  A )
3330, 32sseqtrd 3385 . . . . . . . . 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 19817 . . . . . . . . . . 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 1185 . . . . . . . . . 10  |-  ( ph  ->  dom  ( ( RR  D n F ) `
 N )  C_  dom  ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) )
3734, 36eqsstr3d 3384 . . . . . . . . 9  |-  ( ph  ->  A  C_  dom  ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) )
3833, 37eqssd 3366 . . . . . . . 8  |-  ( ph  ->  dom  ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) )  =  A )
3938feq2d 5582 . . . . . . 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 203 . . . . . 6  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) : A --> RR )
4140ffvelrnda 5871 . . . . 5  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  y )  e.  RR )
421sselda 3349 . . . . . 6  |-  ( (
ph  /\  y  e.  A )  ->  y  e.  RR )
43 fvres 5746 . . . . . . . 8  |-  ( y  e.  RR  ->  (
( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) )  |`  RR ) `  y )  =  ( ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) `
 y ) )
4443adantl 454 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) )  |`  RR ) `  y )  =  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y ) )
45 resubdrg 16751 . . . . . . . . . . . 12  |-  ( RR  e.  (SubRing ` fld )  /\  (flds  RR )  e.  DivRing )
4645simpli 446 . . . . . . . . . . 11  |-  RR  e.  (SubRing ` fld )
4746a1i 11 . . . . . . . . . 10  |-  ( ph  ->  RR  e.  (SubRing ` fld ) )
48 taylth.n . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  NN )
4948nnnn0d 10275 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  NN0 )
50 taylth.b . . . . . . . . . . . . 13  |-  ( ph  ->  B  e.  A )
5150, 34eleqtrrd 2514 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  dom  (
( RR  D n F ) `  N
) )
52 taylth.t . . . . . . . . . . . 12  |-  T  =  ( N ( RR Tayl  F ) B )
531, 50sseldd 3350 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  RR )
542adantr 453 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  F : A --> RR )
551adantr 453 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  A  C_  RR )
56 elfznn0 11084 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( 0 ... N )  ->  k  e.  NN0 )
5756adantl 454 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  k  e.  NN0 )
58 dvnfre 19839 . . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
( RR  D n F ) `  k
) : dom  (
( RR  D n F ) `  k
) --> RR )
6019a1i 11 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  RR  e.  { RR ,  CC } )
6128adantr 453 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  F  e.  ( CC  ^pm  RR ) )
62 simpr 449 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  k  e.  ( 0 ... N
) )
63 dvn2bss 19817 . . . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  dom  ( ( RR  D n F ) `  N
)  C_  dom  ( ( RR  D n F ) `  k ) )
6551adantr 453 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  B  e.  dom  ( ( RR  D n F ) `
 N ) )
6664, 65sseldd 3350 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  B  e.  dom  ( ( RR  D n F ) `
 k ) )
6759, 66ffvelrnd 5872 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
( ( RR  D n F ) `  k
) `  B )  e.  RR )
68 faccl 11577 . . . . . . . . . . . . . 14  |-  ( k  e.  NN0  ->  ( ! `
 k )  e.  NN )
6957, 68syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  ( ! `  k )  e.  NN )
7067, 69nndivred 10049 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
( ( ( RR  D n F ) `
 k ) `  B )  /  ( ! `  k )
)  e.  RR )
7120, 26, 1, 49, 51, 52, 47, 53, 70taylply2 20285 . . . . . . . . . . 11  |-  ( ph  ->  ( T  e.  (Poly `  RR )  /\  (deg `  T )  <_  N
) )
7271simpld 447 . . . . . . . . . 10  |-  ( ph  ->  T  e.  (Poly `  RR ) )
73 dvnply2 20205 . . . . . . . . . 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 1185 . . . . . . . . 9  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) )  e.  (Poly `  RR ) )
75 plyreres 20201 . . . . . . . . 9  |-  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) )  e.  (Poly `  RR )  ->  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) )  |`  RR ) : RR --> RR )
7674, 75syl 16 . . . . . . . 8  |-  ( ph  ->  ( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) )  |`  RR ) : RR --> RR )
7776ffvelrnda 5871 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) )  |`  RR ) `  y )  e.  RR )
7844, 77eqeltrrd 2512 . . . . . 6  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y )  e.  RR )
7942, 78syldan 458 . . . . 5  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y )  e.  RR )
8041, 79resubcld 9466 . . . 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 2437 . . . 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 5894 . . 3  |-  ( ph  ->  ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 y )  -  ( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) `  y ) ) ) : A --> RR )
8353adantr 453 . . . . . 6  |-  ( (
ph  /\  y  e.  A )  ->  B  e.  RR )
8442, 83resubcld 9466 . . . . 5  |-  ( (
ph  /\  y  e.  A )  ->  (
y  -  B )  e.  RR )
85 elfzouz 11145 . . . . . . . . . 10  |-  ( M  e.  ( 1..^ N )  ->  M  e.  ( ZZ>= `  1 )
)
868, 85syl 16 . . . . . . . . 9  |-  ( ph  ->  M  e.  ( ZZ>= ` 
1 ) )
87 nnuz 10522 . . . . . . . . 9  |-  NN  =  ( ZZ>= `  1 )
8886, 87syl6eleqr 2528 . . . . . . . 8  |-  ( ph  ->  M  e.  NN )
8988nnnn0d 10275 . . . . . . 7  |-  ( ph  ->  M  e.  NN0 )
9089adantr 453 . . . . . 6  |-  ( (
ph  /\  y  e.  A )  ->  M  e.  NN0 )
913a1i 11 . . . . . 6  |-  ( (
ph  /\  y  e.  A )  ->  1  e.  NN0 )
9290, 91nn0addcld 10279 . . . . 5  |-  ( (
ph  /\  y  e.  A )  ->  ( M  +  1 )  e.  NN0 )
9384, 92reexpcld 11541 . . . 4  |-  ( (
ph  /\  y  e.  A )  ->  (
( y  -  B
) ^ ( M  +  1 ) )  e.  RR )
94 eqid 2437 . . . 4  |-  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  + 
1 ) ) )  =  ( y  e.  A  |->  ( ( y  -  B ) ^
( M  +  1 ) ) )
9593, 94fmptd 5894 . . 3  |-  ( ph  ->  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) ) : A --> RR )
96 retop 18796 . . . . . 6  |-  ( topGen ` 
ran  (,) )  e.  Top
97 uniretop 18797 . . . . . . 7  |-  RR  =  U. ( topGen `  ran  (,) )
9897ntrss2 17122 . . . . . 6  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  A  C_  RR )  ->  ( ( int `  ( topGen ` 
ran  (,) ) ) `  A )  C_  A
)
9996, 1, 98sylancr 646 . . . . 5  |-  ( ph  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  A )  C_  A )
10048nncnd 10017 . . . . . . . . . . 11  |-  ( ph  ->  N  e.  CC )
10188nncnd 10017 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  CC )
102 ax-1cn 9049 . . . . . . . . . . . 12  |-  1  e.  CC
103102a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  1  e.  CC )
104100, 101, 103nppcan2d 9438 . . . . . . . . . 10  |-  ( ph  ->  ( ( N  -  ( M  +  1
) )  +  1 )  =  ( N  -  M ) )
105104fveq2d 5733 . . . . . . . . 9  |-  ( ph  ->  ( ( RR  D n F ) `  (
( N  -  ( M  +  1 ) )  +  1 ) )  =  ( ( RR  D n F ) `  ( N  -  M ) ) )
10624a1i 11 . . . . . . . . . 10  |-  ( ph  ->  RR  C_  CC )
107 dvnp1 19812 . . . . . . . . . 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 1185 . . . . . . . . 9  |-  ( ph  ->  ( ( RR  D n F ) `  (
( N  -  ( M  +  1 ) )  +  1 ) )  =  ( RR 
_D  ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) ) ) )
109105, 108eqtr3d 2471 . . . . . . . 8  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  M )
)  =  ( RR 
_D  ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) ) ) )
110109dmeqd 5073 . . . . . . 7  |-  ( ph  ->  dom  ( ( RR  D n F ) `
 ( N  -  M ) )  =  dom  ( RR  _D  ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) ) )
111 fzonnsub 11161 . . . . . . . . . . . 12  |-  ( M  e.  ( 1..^ N )  ->  ( N  -  M )  e.  NN )
1128, 111syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( N  -  M
)  e.  NN )
113112nnnn0d 10275 . . . . . . . . . 10  |-  ( ph  ->  ( N  -  M
)  e.  NN0 )
114 dvnbss 19815 . . . . . . . . . 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 1185 . . . . . . . . 9  |-  ( ph  ->  dom  ( ( RR  D n F ) `
 ( N  -  M ) )  C_  dom  F )
116115, 32sseqtrd 3385 . . . . . . . 8  |-  ( ph  ->  dom  ( ( RR  D n F ) `
 ( N  -  M ) )  C_  A )
117 elfzofz 11155 . . . . . . . . . . . . 13  |-  ( M  e.  ( 1..^ N )  ->  M  e.  ( 1 ... N
) )
1188, 117syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  M  e.  ( 1 ... N ) )
1197, 118sseldi 3347 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  ( 0 ... N ) )
120 fznn0sub2 11087 . . . . . . . . . . 11  |-  ( M  e.  ( 0 ... N )  ->  ( N  -  M )  e.  ( 0 ... N
) )
121119, 120syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( N  -  M
)  e.  ( 0 ... N ) )
122 dvn2bss 19817 . . . . . . . . . 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 1185 . . . . . . . . 9  |-  ( ph  ->  dom  ( ( RR  D n F ) `
 N )  C_  dom  ( ( RR  D n F ) `  ( N  -  M )
) )
12434, 123eqsstr3d 3384 . . . . . . . 8  |-  ( ph  ->  A  C_  dom  ( ( RR  D n F ) `  ( N  -  M ) ) )
125116, 124eqssd 3366 . . . . . . 7  |-  ( ph  ->  dom  ( ( RR  D n F ) `
 ( N  -  M ) )  =  A )
126110, 125eqtr3d 2471 . . . . . 6  |-  ( ph  ->  dom  ( RR  _D  ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) )  =  A )
127 fss 5600 . . . . . . . 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 645 . . . . . . 7  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) : A --> CC )
129 eqid 2437 . . . . . . . 8  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
130129tgioo2 18835 . . . . . . 7  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
131106, 128, 1, 130, 129dvbssntr 19788 . . . . . 6  |-  ( ph  ->  dom  ( RR  _D  ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) )  C_  (
( int `  ( topGen `
 ran  (,) )
) `  A )
)
132126, 131eqsstr3d 3384 . . . . 5  |-  ( ph  ->  A  C_  ( ( int `  ( topGen `  ran  (,) ) ) `  A
) )
13399, 132eqssd 3366 . . . 4  |-  ( ph  ->  ( ( int `  ( topGen `
 ran  (,) )
) `  A )  =  A )
13497isopn3 17131 . . . . 5  |-  ( ( ( topGen `  ran  (,) )  e.  Top  /\  A  C_  RR )  ->  ( A  e.  ( topGen `  ran  (,) )  <->  ( ( int `  ( topGen `  ran  (,) )
) `  A )  =  A ) )
13596, 1, 134sylancr 646 . . . 4  |-  ( ph  ->  ( A  e.  (
topGen `  ran  (,) )  <->  ( ( int `  ( topGen `
 ran  (,) )
) `  A )  =  A ) )
136133, 135mpbird 225 . . 3  |-  ( ph  ->  A  e.  ( topGen ` 
ran  (,) ) )
137 eqid 2437 . . 3  |-  ( A 
\  { B }
)  =  ( A 
\  { B }
)
138 difss 3475 . . . 4  |-  ( A 
\  { B }
)  C_  A
13941recnd 9115 . . . . . . 7  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  y )  e.  CC )
140 dvnf 19814 . . . . . . . . . 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 1185 . . . . . . . . 9  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  M )
) : dom  (
( RR  D n F ) `  ( N  -  M )
) --> CC )
142125feq2d 5582 . . . . . . . . 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 203 . . . . . . . 8  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  M )
) : A --> CC )
144143ffvelrnda 5871 . . . . . . 7  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( RR  D n F ) `  ( N  -  M )
) `  y )  e.  CC )
145 dvnfre 19839 . . . . . . . . . . 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 1185 . . . . . . . . . 10  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  M )
) : dom  (
( RR  D n F ) `  ( N  -  M )
) --> RR )
147125feq2d 5582 . . . . . . . . . 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 203 . . . . . . . . 9  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  M )
) : A --> RR )
149148feqmptd 5780 . . . . . . . 8  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  M )
)  =  ( y  e.  A  |->  ( ( ( RR  D n F ) `  ( N  -  M )
) `  y )
) )
15040feqmptd 5780 . . . . . . . . 9  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) )  =  ( y  e.  A  |->  ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  y ) ) )
151150oveq2d 6098 . . . . . . . 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 2478 . . . . . . 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 9115 . . . . . . 7  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y )  e.  CC )
154 fvex 5743 . . . . . . . 8  |-  ( ( ( CC  D n T ) `  ( N  -  M )
) `  y )  e.  _V
155154a1i 11 . . . . . . 7  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( CC  D n T ) `  ( N  -  M )
) `  y )  e.  _V )
15678recnd 9115 . . . . . . . 8  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y )  e.  CC )
157 recn 9081 . . . . . . . . 9  |-  ( y  e.  RR  ->  y  e.  CC )
158 dvnply2 20205 . . . . . . . . . . . 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 1185 . . . . . . . . . . 11  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  M )
)  e.  (Poly `  RR ) )
160 plyf 20118 . . . . . . . . . . 11  |-  ( ( ( CC  D n T ) `  ( N  -  M )
)  e.  (Poly `  RR )  ->  ( ( CC  D n T ) `  ( N  -  M ) ) : CC --> CC )
161159, 160syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  M )
) : CC --> CC )
162161ffvelrnda 5871 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( ( CC  D n T ) `  ( N  -  M )
) `  y )  e.  CC )
163157, 162sylan2 462 . . . . . . . 8  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( ( CC  D n T ) `  ( N  -  M )
) `  y )  e.  CC )
164129cnfldtopon 18818 . . . . . . . . . 10  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
165 toponmax 16994 . . . . . . . . . 10  |-  ( (
TopOpen ` fld )  e.  (TopOn `  CC )  ->  CC  e.  ( TopOpen ` fld ) )
166164, 165mp1i 12 . . . . . . . . 9  |-  ( ph  ->  CC  e.  ( TopOpen ` fld )
)
167 df-ss 3335 . . . . . . . . . 10  |-  ( RR  C_  CC  <->  ( RR  i^i  CC )  =  RR )
168106, 167sylib 190 . . . . . . . . 9  |-  ( ph  ->  ( RR  i^i  CC )  =  RR )
169 plyf 20118 . . . . . . . . . . 11  |-  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) )  e.  (Poly `  RR )  ->  ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) : CC --> CC )
17074, 169syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) : CC --> CC )
171170ffvelrnda 5871 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y )  e.  CC )
172104fveq2d 5733 . . . . . . . . . . 11  |-  ( ph  ->  ( ( CC  D n T ) `  (
( N  -  ( M  +  1 ) )  +  1 ) )  =  ( ( CC  D n T ) `  ( N  -  M ) ) )
173 ssid 3368 . . . . . . . . . . . . 13  |-  CC  C_  CC
174173a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  CC  C_  CC )
175 mapsspm 7048 . . . . . . . . . . . . 13  |-  ( CC 
^m  CC )  C_  ( CC  ^pm  CC )
176 plyf 20118 . . . . . . . . . . . . . . 15  |-  ( T  e.  (Poly `  RR )  ->  T : CC --> CC )
17772, 176syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  T : CC --> CC )
17821, 21elmap 7043 . . . . . . . . . . . . . 14  |-  ( T  e.  ( CC  ^m  CC )  <->  T : CC --> CC )
179177, 178sylibr 205 . . . . . . . . . . . . 13  |-  ( ph  ->  T  e.  ( CC 
^m  CC ) )
180175, 179sseldi 3347 . . . . . . . . . . . 12  |-  ( ph  ->  T  e.  ( CC 
^pm  CC ) )
181 dvnp1 19812 . . . . . . . . . . . 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 1185 . . . . . . . . . . 11  |-  ( ph  ->  ( ( CC  D n T ) `  (
( N  -  ( M  +  1 ) )  +  1 ) )  =  ( CC 
_D  ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) ) )
183172, 182eqtr3d 2471 . . . . . . . . . 10  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  M )
)  =  ( CC 
_D  ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) ) )
184161feqmptd 5780 . . . . . . . . . 10  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  M )
)  =  ( y  e.  CC  |->  ( ( ( CC  D n T ) `  ( N  -  M )
) `  y )
) )
185170feqmptd 5780 . . . . . . . . . . 11  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) )  =  ( y  e.  CC  |->  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y ) ) )
186185oveq2d 6098 . . . . . . . . . 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 2478 . . . . . . . . 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 19843 . . . . . . . 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 19850 . . . . . . 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 19854 . . . . . 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 5073 . . . . 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 6107 . . . . . 6  |-  ( ( ( ( RR  D n F ) `  ( N  -  M )
) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  M ) ) `
 y ) )  e.  _V
193 eqid 2437 . . . . . 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 5575 . . . . 5  |-  dom  (
y  e.  A  |->  ( ( ( ( RR  D n F ) `
 ( N  -  M ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  M )
) `  y )
) )  =  A
195191, 194syl6eq 2485 . . . 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 3398 . . 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 449 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  CC )  ->  y  e.  CC )
19853adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  CC )  ->  B  e.  RR )
199198recnd 9115 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  CC )  ->  B  e.  CC )
200197, 199subcld 9412 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  CC )  ->  ( y  -  B )  e.  CC )
20189adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  CC )  ->  M  e. 
NN0 )
2023a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  CC )  ->  1  e. 
NN0 )
203201, 202nn0addcld 10279 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  CC )  ->  ( M  +  1 )  e. 
NN0 )
204200, 203expcld 11524 . . . . . . . 8  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( y  -  B ) ^ ( M  + 
1 ) )  e.  CC )
205157, 204sylan2 462 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( y  -  B ) ^ ( M  + 
1 ) )  e.  CC )
206101adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  CC )  ->  M  e.  CC )
207102a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  CC )  ->  1  e.  CC )
208206, 207addcld 9108 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  CC )  ->  ( M  +  1 )  e.  CC )
209200, 201expcld 11524 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( y  -  B ) ^ M )  e.  CC )
210208, 209mulcld 9109 . . . . . . . 8  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) )  e.  CC )
211157, 210sylan2 462 . . . . . . 7  |-  ( (
ph  /\  y  e.  RR )  ->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) )  e.  CC )
21221prid2 3914 . . . . . . . . . . 11  |-  CC  e.  { RR ,  CC }
213212a1i 11 . . . . . . . . . 10  |-  ( ph  ->  CC  e.  { RR ,  CC } )
214 simpr 449 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  CC )  ->  x  e.  CC )
215 elfznn 11081 . . . . . . . . . . . . . 14  |-  ( ( M  +  1 )  e.  ( 1 ... N )  ->  ( M  +  1 )  e.  NN )
21610, 215syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( M  +  1 )  e.  NN )
217216nnnn0d 10275 . . . . . . . . . . . 12  |-  ( ph  ->  ( M  +  1 )  e.  NN0 )
218217adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  CC )  ->  ( M  +  1 )  e. 
NN0 )
219214, 218expcld 11524 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  CC )  ->  ( x ^ ( M  + 
1 ) )  e.  CC )
220 ovex 6107 . . . . . . . . . . 11  |-  ( ( M  +  1 )  x.  ( x ^ M ) )  e. 
_V
221220a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  CC )  ->  ( ( M  +  1 )  x.  ( x ^ M ) )  e. 
_V )
222213dvmptid 19844 . . . . . . . . . . . 12  |-  ( ph  ->  ( CC  _D  (
y  e.  CC  |->  y ) )  =  ( y  e.  CC  |->  1 ) )
223 0cn 9085 . . . . . . . . . . . . 13  |-  0  e.  CC
224223a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  CC )  ->  0  e.  CC )
22553recnd 9115 . . . . . . . . . . . . 13  |-  ( ph  ->  B  e.  CC )
226213, 225dvmptc 19845 . . . . . . . . . . . 12  |-  ( ph  ->  ( CC  _D  (
y  e.  CC  |->  B ) )  =  ( y  e.  CC  |->  0 ) )
227213, 197, 207, 222, 199, 224, 226dvmptsub 19854 . . . . . . . . . . 11  |-  ( ph  ->  ( CC  _D  (
y  e.  CC  |->  ( y  -  B ) ) )  =  ( y  e.  CC  |->  ( 1  -  0 ) ) )
228102subid1i 9373 . . . . . . . . . . . 12  |-  ( 1  -  0 )  =  1
229228mpteq2i 4293 . . . . . . . . . . 11  |-  ( y  e.  CC  |->  ( 1  -  0 ) )  =  ( y  e.  CC  |->  1 )
230227, 229syl6eq 2485 . . . . . . . . . 10  |-  ( ph  ->  ( CC  _D  (
y  e.  CC  |->  ( y  -  B ) ) )  =  ( y  e.  CC  |->  1 ) )
231 dvexp 19840 . . . . . . . . . . . 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 16 . . . . . . . . . . 11  |-  ( ph  ->  ( CC  _D  (
x  e.  CC  |->  ( x ^ ( M  +  1 ) ) ) )  =  ( x  e.  CC  |->  ( ( M  +  1 )  x.  ( x ^ ( ( M  +  1 )  - 
1 ) ) ) ) )
233101, 103pncand 9413 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( M  + 
1 )  -  1 )  =  M )
234233oveq2d 6098 . . . . . . . . . . . . 13  |-  ( ph  ->  ( x ^ (
( M  +  1 )  -  1 ) )  =  ( x ^ M ) )
235234oveq2d 6098 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( M  + 
1 )  x.  (
x ^ ( ( M  +  1 )  -  1 ) ) )  =  ( ( M  +  1 )  x.  ( x ^ M ) ) )
236235mpteq2dv 4297 . . . . . . . . . . 11  |-  ( ph  ->  ( x  e.  CC  |->  ( ( M  + 
1 )  x.  (
x ^ ( ( M  +  1 )  -  1 ) ) ) )  =  ( x  e.  CC  |->  ( ( M  +  1 )  x.  ( x ^ M ) ) ) )
237232, 236eqtrd 2469 . . . . . . . . . 10  |-  ( ph  ->  ( CC  _D  (
x  e.  CC  |->  ( x ^ ( M  +  1 ) ) ) )  =  ( x  e.  CC  |->  ( ( M  +  1 )  x.  ( x ^ M ) ) ) )
238 oveq1 6089 . . . . . . . . . 10  |-  ( x  =  ( y  -  B )  ->  (
x ^ ( M  +  1 ) )  =  ( ( y  -  B ) ^
( M  +  1 ) ) )
239 oveq1 6089 . . . . . . . . . . 11  |-  ( x  =  ( y  -  B )  ->  (
x ^ M )  =  ( ( y  -  B ) ^ M ) )
240239oveq2d 6098 . . . . . . . . . 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 19859 . . . . . . . . 9  |-  ( ph  ->  ( CC  _D  (
y  e.  CC  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) ) )  =  ( y  e.  CC  |->  ( ( ( M  + 
1 )  x.  (
( y  -  B
) ^ M ) )  x.  1 ) ) )
242210mulid1d 9106 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) )  x.  1 )  =  ( ( M  + 
1 )  x.  (
( y  -  B
) ^ M ) ) )
243242mpteq2dva 4296 . . . . . . . . 9  |-  ( ph  ->  ( y  e.  CC  |->  ( ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M
) )  x.  1 ) )  =  ( y  e.  CC  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) ) )
244241, 243eqtrd 2469 . . . . . . . 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 19843 . . . . . . 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 19850 . . . . . 6  |-  ( ph  ->  ( RR  _D  (
y  e.  A  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) ) )  =  ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) ) )
247246dmeqd 5073 . . . . 5  |-  ( ph  ->  dom  ( RR  _D  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) ) )  =  dom  ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M
) ) ) )
248 ovex 6107 . . . . . 6  |-  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) )  e. 
_V
249 eqid 2437 . . . . . 6  |-  ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) )  =  ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M
) ) )
250248, 249dmmpti 5575 . . . . 5  |-  dom  (
y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) )  =  A
251247, 250syl6eq 2485 . . . 4  |-  ( ph  ->  dom  ( RR  _D  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) ) )  =  A )
252138, 251syl5sseqr 3398 . . 3  |-  ( ph  ->  ( A  \  { B } )  C_  dom  ( RR  _D  (
y  e.  A  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) ) ) )
25320, 26, 1, 13, 51, 52dvntaylp0 20289 . . . . . 6  |-  ( ph  ->  ( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) `  B )  =  ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  B ) )
254253oveq2d 6098 . . . . 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 5872 . . . . . 6  |-  ( ph  ->  ( ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) ) `  B )  e.  CC )
256255subidd 9400 . . . . 5  |-  ( ph  ->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 B )  -  ( ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) ) `  B ) )  =  0 )
257254, 256eqtrd 2469 . . . 4  |-  ( ph  ->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 B )  -  ( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) `  B ) )  =  0 )
258129subcn 18897 . . . . . . 7  |-  -  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) )
259258a1i 11 . . . . . 6  |-  ( ph  ->  -  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)  Cn  ( TopOpen ` fld )
) )
260 dvcn 19808 . . . . . . . 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 1188 . . . . . . 7  |-  ( ph  ->  ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) )  e.  ( A
-cn-> CC ) )
262150, 261eqeltrrd 2512 . . . . . 6  |-  ( ph  ->  ( y  e.  A  |->  ( ( ( RR  D n F ) `
 ( N  -  ( M  +  1
) ) ) `  y ) )  e.  ( A -cn-> CC ) )
263 plycn 20180 . . . . . . . 8  |-  ( ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) )  e.  (Poly `  RR )  ->  ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) )  e.  ( CC -cn-> CC ) )
26474, 263syl 16 . . . . . . 7  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) )  e.  ( CC
-cn-> CC ) )
2651, 24syl6ss 3361 . . . . . . . 8  |-  ( ph  ->  A  C_  CC )
266 cncfmptid 18943 . . . . . . . 8  |-  ( ( A  C_  CC  /\  CC  C_  CC )  ->  (
y  e.  A  |->  y )  e.  ( A
-cn-> CC ) )
267265, 173, 266sylancl 645 . . . . . . 7  |-  ( ph  ->  ( y  e.  A  |->  y )  e.  ( A -cn-> CC ) )
268264, 267cncfmpt1f 18944 . . . . . 6  |-  ( ph  ->  ( y  e.  A  |->  ( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
) ) ) `  y ) )  e.  ( A -cn-> CC ) )
269129, 259, 262, 268cncfmpt2f 18945 . . . . 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 5729 . . . . . 6  |-  ( y  =  B  ->  (
( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  y )  =  ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 B ) )
271 fveq2 5729 . . . . . 6  |-  ( y  =  B  ->  (
( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y )  =  ( ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) `
 B ) )
272270, 271oveq12d 6100 . . . . 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 19778 . . . 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 2512 . . 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 9400 . . . . . 6  |-  ( ph  ->  ( B  -  B
)  =  0 )
276275oveq1d 6097 . . . . 5  |-  ( ph  ->  ( ( B  -  B ) ^ ( M  +  1 ) )  =  ( 0 ^ ( M  + 
1 ) ) )
2772160expd 11540 . . . . 5  |-  ( ph  ->  ( 0 ^ ( M  +  1 ) )  =  0 )
278276, 277eqtrd 2469 . . . 4  |-  ( ph  ->  ( ( B  -  B ) ^ ( M  +  1 ) )  =  0 )
279265sselda 3349 . . . . . . . 8  |-  ( (
ph  /\  y  e.  A )  ->  y  e.  CC )
280279, 204syldan 458 . . . . . . 7  |-  ( (
ph  /\  y  e.  A )  ->  (
( y  -  B
) ^ ( M  +  1 ) )  e.  CC )
281280, 94fmptd 5894 . . . . . 6  |-  ( ph  ->  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) ) : A --> CC )
282 dvcn 19808 . . . . . 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 1188 . . . . 5  |-  ( ph  ->  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) )  e.  ( A -cn-> CC ) )
284 oveq1 6089 . . . . . 6  |-  ( y  =  B  ->  (
y  -  B )  =  ( B  -  B ) )
285284oveq1d 6097 . . . . 5  |-  ( y  =  B  ->  (
( y  -  B
) ^ ( M  +  1 ) )  =  ( ( B  -  B ) ^
( M  +  1 ) ) )
286283, 50, 285cnmptlimc 19778 . . . 4  |-  ( ph  ->  ( ( B  -  B ) ^ ( M  +  1 ) )  e.  ( ( y  e.  A  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) ) lim CC  B ) )
287278, 286eqeltrrd 2512 . . 3  |-  ( ph  ->  0  e.  ( ( y  e.  A  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) ) lim CC  B ) )
288265ssdifssd 3486 . . . . . . . . . 10  |-  ( ph  ->  ( A  \  { B } )  C_  CC )
289288sselda 3349 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
y  e.  CC )
290225adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  ->  B  e.  CC )
291289, 290subcld 9412 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( y  -  B
)  e.  CC )
292 eldifsni 3929 . . . . . . . . . 10  |-  ( y  e.  ( A  \  { B } )  -> 
y  =/=  B )
293292adantl 454 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
y  =/=  B )
294289, 290, 293subne0d 9421 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( y  -  B
)  =/=  0 )
295216adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( M  +  1 )  e.  NN )
296295nnzd 10375 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( M  +  1 )  e.  ZZ )
297291, 294, 296expne0d 11530 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( ( y  -  B ) ^ ( M  +  1 ) )  =/=  0 )
298297necomd 2688 . . . . . 6  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
0  =/=  ( ( y  -  B ) ^ ( M  + 
1 ) ) )
299298neneqd 2618 . . . . 5  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  ->  -.  0  =  (
( y  -  B
) ^ ( M  +  1 ) ) )
300299nrexdv 2810 . . . 4  |-  ( ph  ->  -.  E. y  e.  ( A  \  { B } ) 0  =  ( ( y  -  B ) ^ ( M  +  1 ) ) )
301 df-ima 4892 . . . . . 6  |-  ( ( y  e.  A  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) ) " ( A 
\  { B }
) )  =  ran  ( ( y  e.  A  |->  ( ( y  -  B ) ^
( M  +  1 ) ) )  |`  ( A  \  { B } ) )
302301eleq2i 2501 . . . . 5  |-  ( 0  e.  ( ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  + 
1 ) ) )
" ( A  \  { B } ) )  <->  0  e.  ran  (
( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) )  |`  ( A  \  { B }
) ) )
303 resmpt 5192 . . . . . . 7  |-  ( ( A  \  { B } )  C_  A  ->  ( ( y  e.  A  |->  ( ( y  -  B ) ^
( M  +  1 ) ) )  |`  ( A  \  { B } ) )  =  ( y  e.  ( A  \  { B } )  |->  ( ( y  -  B ) ^ ( M  + 
1 ) ) ) )
304138, 303ax-mp 8 . . . . . 6  |-  ( ( y  e.  A  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) )  |`  ( A  \  { B } ) )  =  ( y  e.  ( A  \  { B } )  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) )
305 ovex 6107 . . . . . 6  |-  ( ( y  -  B ) ^ ( M  + 
1 ) )  e. 
_V
306304, 305elrnmpti 5122 . . . . 5  |-  ( 0  e.  ran  ( ( y  e.  A  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) )  |`  ( A  \  { B } ) )  <->  E. y  e.  ( A  \  { B } ) 0  =  ( ( y  -  B ) ^ ( M  +  1 ) ) )
307302, 306bitri 242 . . . 4  |-  ( 0  e.  ( ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  + 
1 ) ) )
" ( A  \  { B } ) )  <->  E. y  e.  ( A  \  { B }
) 0  =  ( ( y  -  B
) ^ ( M  +  1 ) ) )
308300, 307sylnibr 298 . . 3  |-  ( ph  ->  -.  0  e.  ( ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) ) " ( A  \  { B }
) ) )
309101adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  ->  M  e.  CC )
310102a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
1  e.  CC )
311309, 310addcld 9108 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( M  +  1 )  e.  CC )
312289, 209syldan 458 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( ( y  -  B ) ^ M
)  e.  CC )
313295nnne0d 10045 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( M  +  1 )  =/=  0 )
31488adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  ->  M  e.  NN )
315314nnzd 10375 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  ->  M  e.  ZZ )
316291, 294, 315expne0d 11530 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( ( y  -  B ) ^ M
)  =/=  0 )
317311, 312, 313, 316mulne0d 9675 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
( ( M  + 
1 )  x.  (
( y  -  B
) ^ M ) )  =/=  0 )
318317necomd 2688 . . . . . 6  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  -> 
0  =/=  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) )
319318neneqd 2618 . . . . 5  |-  ( (
ph  /\  y  e.  ( A  \  { B } ) )  ->  -.  0  =  (
( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) )
320319nrexdv 2810 . . . 4  |-  ( ph  ->  -.  E. y  e.  ( A  \  { B } ) 0  =  ( ( M  + 
1 )  x.  (
( y  -  B
) ^ M ) ) )
321246imaeq1d 5203 . . . . . . 7  |-  ( ph  ->  ( ( RR  _D  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) ) ) "
( A  \  { B } ) )  =  ( ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M
) ) ) "
( A  \  { B } ) ) )
322 df-ima 4892 . . . . . . 7  |-  ( ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) ) " ( A 
\  { B }
) )  =  ran  ( ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M
) ) )  |`  ( A  \  { B } ) )
323321, 322syl6eq 2485 . . . . . 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 } ) ) )
324323eleq2d 2504 . . . . 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 } ) ) ) )
325 resmpt 5192 . . . . . . 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 ) ) ) )
326138, 325ax-mp 8 . . . . . 6  |-  ( ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) )  |`  ( A  \  { B } ) )  =  ( y  e.  ( A  \  { B } )  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M ) ) )
327326, 248elrnmpti 5122 . . . . 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 ) ) )
328324, 327syl6bb 254 . . . 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 ) ) ) )
329320, 328mtbird 294 . . 3  |-  ( ph  ->  -.  0  e.  ( ( RR  _D  (
y  e.  A  |->  ( ( y  -  B
) ^ ( M  +  1 ) ) ) ) " ( A  \  { B }
) ) )
330 eldifi 3470 . . . . . . . 8  |-  ( x  e.  ( A  \  { B } )  ->  x  e.  A )
331143ffvelrnda 5871 . . . . . . . 8  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( RR  D n F ) `  ( N  -  M )
) `  x )  e.  CC )
332330, 331sylan2 462 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( ( RR  D n F ) `
 ( N  -  M ) ) `  x )  e.  CC )
3331ssdifssd 3486 . . . . . . . . . 10  |-  ( ph  ->  ( A  \  { B } )  C_  RR )
334333sselda 3349 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  x  e.  RR )
335334recnd 9115 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  x  e.  CC )
336161ffvelrnda 5871 . . . . . . . 8  |-  ( (
ph  /\  x  e.  CC )  ->  ( ( ( CC  D n T ) `  ( N  -  M )
) `  x )  e.  CC )
337335, 336syldan 458 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( ( CC  D n T ) `
 ( N  -  M ) ) `  x )  e.  CC )
338332, 337subcld 9412 . . . . . 6  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( ( ( RR  D n F ) `  ( N  -  M ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  M ) ) `  x ) )  e.  CC )
33953adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  B  e.  RR )
340334, 339resubcld 9466 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( x  -  B
)  e.  RR )
34189adantr 453 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  M  e.  NN0 )
342340, 341reexpcld 11541 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( x  -  B ) ^ M
)  e.  RR )
343342recnd 9115 . . . . . 6  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( x  -  B ) ^ M
)  e.  CC )
344339recnd 9115 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  B  e.  CC )
345335, 344subcld 9412 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( x  -  B
)  e.  CC )
346 eldifsni 3929 . . . . . . . . 9  |-  ( x  e.  ( A  \  { B } )  ->  x  =/=  B )
347346adantl 454 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  x  =/=  B )
348335, 344, 347subne0d 9421 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( x  -  B
)  =/=  0 )
349341nn0zd 10374 . . . . . . 7  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  M  e.  ZZ )
350345, 348, 349expne0d 11530 . . . . . 6  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( x  -  B ) ^ M
)  =/=  0 )
351338, 343, 350divcld 9791 . . . . 5  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( ( ( ( RR  D n F ) `  ( N  -  M )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  M ) ) `
 x ) )  /  ( ( x  -  B ) ^ M ) )  e.  CC )
352216nnrecred 10046 . . . . . . 7  |-  ( ph  ->  ( 1  /  ( M  +  1 ) )  e.  RR )
353352recnd 9115 . . . . . 6  |-  ( ph  ->  ( 1  /  ( M  +  1 ) )  e.  CC )
354353adantr 453 . . . . 5  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( 1  /  ( M  +  1 ) )  e.  CC )
355 txtopon 17624 . . . . . . . 8  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  ( TopOpen
` fld
)  e.  (TopOn `  CC ) )  ->  (
( TopOpen ` fld )  tX  ( TopOpen ` fld )
)  e.  (TopOn `  ( CC  X.  CC ) ) )
356164, 164, 355mp2an 655 . . . . . . 7  |-  ( (
TopOpen ` fld )  tX  ( TopOpen ` fld )
)  e.  (TopOn `  ( CC  X.  CC ) )
357356toponunii 16998 . . . . . . . 8  |-  ( CC 
X.  CC )  = 
U. ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )
358357restid 13662 . . . . . . 7  |-  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)  e.  (TopOn `  ( CC  X.  CC ) )  ->  (
( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)t  ( CC  X.  CC ) )  =  ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
) )
359356, 358ax-mp 8 . . . . . 6  |-  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)t  ( CC  X.  CC ) )  =  ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)
360359eqcomi 2441 . . . . 5  |-  ( (
TopOpen ` fld )  tX  ( TopOpen ` fld )
)  =  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)t  ( CC  X.  CC ) )
361 taylthlem2.i . . . . 5  |-  ( 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 ) )
362 limcresi 19773 . . . . . . 7  |-  ( ( x  e.  A  |->  ( 1  /  ( M  +  1 ) ) ) lim CC  B ) 
C_  ( ( ( x  e.  A  |->  ( 1  /  ( M  +  1 ) ) )  |`  ( A  \  { B } ) ) lim CC  B )
363 resmpt 5192 . . . . . . . . 9  |-  ( ( A  \  { B } )  C_  A  ->  ( ( x  e.  A  |->  ( 1  / 
( M  +  1 ) ) )  |`  ( A  \  { B } ) )  =  ( x  e.  ( A  \  { B } )  |->  ( 1  /  ( M  + 
1 ) ) ) )
364138, 363ax-mp 8 . . . . . . . 8  |-  ( ( x  e.  A  |->  ( 1  /  ( M  +  1 ) ) )  |`  ( A  \  { B } ) )  =  ( x  e.  ( A  \  { B } )  |->  ( 1  /  ( M  +  1 ) ) )
365364oveq1i 6092 . . . . . . 7  |-  ( ( ( x  e.  A  |->  ( 1  /  ( M  +  1 ) ) )  |`  ( A  \  { B }
) ) lim CC  B
)  =  ( ( x  e.  ( A 
\  { B }
)  |->  ( 1  / 
( M  +  1 ) ) ) lim CC  B )
366362, 365sseqtri 3381 . . . . . 6  |-  ( ( x  e.  A  |->  ( 1  /  ( M  +  1 ) ) ) lim CC  B ) 
C_  ( ( x  e.  ( A  \  { B } )  |->  ( 1  /  ( M  +  1 ) ) ) lim CC  B )
367 cncfmptc 18942 . . . . . . . 8  |-  ( ( ( 1  /  ( M  +  1 ) )  e.  RR  /\  A  C_  CC  /\  RR  C_  CC )  ->  (
x  e.  A  |->  ( 1  /  ( M  +  1 ) ) )  e.  ( A
-cn-> RR ) )
368352, 265, 106, 367syl3anc 1185 . . . . . . 7  |-  ( ph  ->  ( x  e.  A  |->  ( 1  /  ( M  +  1 ) ) )  e.  ( A -cn-> RR ) )
369 eqidd 2438 . . . . . . 7  |-  ( x  =  B  ->  (
1  /  ( M  +  1 ) )  =  ( 1  / 
( M  +  1 ) ) )
370368, 50, 369cnmptlimc 19778 . . . . . 6  |-  ( ph  ->  ( 1  /  ( M  +  1 ) )  e.  ( ( x  e.  A  |->  ( 1  /  ( M  +  1 ) ) ) lim CC  B ) )
371366, 370sseldi 3347 . . . . 5  |-  ( ph  ->  ( 1  /  ( M  +  1 ) )  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( 1  / 
( M  +  1 ) ) ) lim CC  B ) )
372129mulcn 18898 . . . . . 6  |-  x.  e.  ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld ) )  Cn  ( TopOpen
` fld
) )
373 opelxpi 4911 . . . . . . 7  |-  ( ( 0  e.  CC  /\  ( 1  /  ( M  +  1 ) )  e.  CC )  ->  <. 0 ,  ( 1  /  ( M  +  1 ) )
>.  e.  ( CC  X.  CC ) )
374223, 353, 373sylancr 646 . . . . . 6  |-  ( ph  -> 
<. 0 ,  ( 1  /  ( M  +  1 ) )
>.  e.  ( CC  X.  CC ) )
375357cncnpi 17343 . . . . . 6  |-  ( (  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 ) ) >.
) )
376372, 374, 375sylancr 646 . . . . 5  |-  ( ph  ->  x.  e.  ( ( ( ( TopOpen ` fld )  tX  ( TopOpen ` fld )
)  CnP  ( TopOpen ` fld )
) `  <. 0 ,  ( 1  /  ( M  +  1 ) ) >. ) )
377351, 354, 174, 174, 129, 360, 361, 371, 376limccnp2 19780 . . . 4  |-  ( 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 ) )
378353mul02d 9265 . . . 4  |-  ( ph  ->  ( 0  x.  (
1  /  ( M  +  1 ) ) )  =  0 )
379190fveq1d 5731 . . . . . . . . 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 ) )
380 fveq2 5729 . . . . . . . . . . . 12  |-  ( y  =  x  ->  (
( ( RR  D n F ) `  ( N  -  M )
) `  y )  =  ( ( ( RR  D n F ) `  ( N  -  M ) ) `
 x ) )
381 fveq2 5729 . . . . . . . . . . . 12  |-  ( y  =  x  ->  (
( ( CC  D n T ) `  ( N  -  M )
) `  y )  =  ( ( ( CC  D n T ) `  ( N  -  M ) ) `
 x ) )
382380, 381oveq12d 6100 . . . . . . . . . . 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 ) ) )
383 ovex 6107 . . . . . . . . . . 11  |-  ( ( ( ( RR  D n F ) `  ( N  -  M )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  M ) ) `
 x ) )  e.  _V
384382, 193, 383fvmpt 5807 . . . . . . . . . 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 ) ) )
385330, 384syl 16 . . . . . . . . 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 ) ) )
386379, 385sylan9eq 2489 . . . . . . . 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 ) ) )
387246fveq1d 5731 . . . . . . . . . 10  |-  ( ph  ->  ( ( RR  _D  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) ) ) `  x )  =  ( ( y  e.  A  |->  ( ( M  + 
1 )  x.  (
( y  -  B
) ^ M ) ) ) `  x
) )
388 oveq1 6089 . . . . . . . . . . . . . 14  |-  ( y  =  x  ->  (
y  -  B )  =  ( x  -  B ) )
389388oveq1d 6097 . . . . . . . . . . . . 13  |-  ( y  =  x  ->  (
( y  -  B
) ^ M )  =  ( ( x  -  B ) ^ M ) )
390389oveq2d 6098 . . . . . . . . . . . 12  |-  ( y  =  x  ->  (
( M  +  1 )  x.  ( ( y  -  B ) ^ M ) )  =  ( ( M  +  1 )  x.  ( ( x  -  B ) ^ M
) ) )
391 ovex 6107 . . . . . . . . . . . 12  |-  ( ( M  +  1 )  x.  ( ( x  -  B ) ^ M ) )  e. 
_V
392390, 249, 391fvmpt 5807 . . . . . . . . . . 11  |-  ( x  e.  A  ->  (
( y  e.  A  |->  ( ( M  + 
1 )  x.  (
( y  -  B
) ^ M ) ) ) `  x
)  =  ( ( M  +  1 )  x.  ( ( x  -  B ) ^ M ) ) )
393330, 392syl 16 . . . . . . . . . 10  |-  ( x  e.  ( A  \  { B } )  -> 
( ( y  e.  A  |->  ( ( M  +  1 )  x.  ( ( y  -  B ) ^ M
) ) ) `  x )  =  ( ( M  +  1 )  x.  ( ( x  -  B ) ^ M ) ) )
394387, 393sylan9eq 2489 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( RR  _D  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) ) ) `  x )  =  ( ( M  +  1 )  x.  ( ( x  -  B ) ^ M ) ) )
395216adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( M  +  1 )  e.  NN )
396395nncnd 10017 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( M  +  1 )  e.  CC )
397396, 343mulcomd 9110 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( M  + 
1 )  x.  (
( x  -  B
) ^ M ) )  =  ( ( ( x  -  B
) ^ M )  x.  ( M  + 
1 ) ) )
398394, 397eqtrd 2469 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( RR  _D  ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) ) ) `  x )  =  ( ( ( x  -  B ) ^ M
)  x.  ( M  +  1 ) ) )
399386, 398oveq12d 6100 . . . . . . 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 ) ) ) )
400395nnne0d 10045 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( M  +  1 )  =/=  0 )
401338, 343, 396, 350, 400divdiv1d 9822 . . . . . . 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 ) ) ) )
402351, 396, 400divrecd 9794 . . . . . . 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 ) ) ) )
403399, 401, 4023eqtr2rd 2476 . . . . . 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 ) ) )
404403mpteq2dva 4296 . . . . 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 ) ) ) )
405404oveq1d 6097 . . . 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
) )
406377, 378, 4053eltr3d 2517 . . 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
) )
4071, 82, 95, 136, 50, 137, 196, 252, 274, 287, 308, 329, 406lhop 19901 . 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
) )
408330adantl 454 . . . . . 6  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  x  e.  A )
409 fveq2 5729 . . . . . . . 8  |-  ( y  =  x  ->  (
( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  y )  =  ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 x ) )
410 fveq2 5729 . . . . . . . 8  |-  ( y  =  x  ->  (
( ( CC  D n T ) `  ( N  -  ( M  +  1 ) ) ) `  y )  =  ( ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) `
 x ) )
411409, 410oveq12d 6100 . . . . . . 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 ) ) )
412 ovex 6107 . . . . . . 7  |-  ( ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) `
 x ) )  e.  _V
413411, 81, 412fvmpt 5807 . . . . . 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 ) ) )
414408, 413syl 16 . . . . 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 ) ) )
415388oveq1d 6097 . . . . . . 7  |-  ( y  =  x  ->  (
( y  -  B
) ^ ( M  +  1 ) )  =  ( ( x  -  B ) ^
( M  +  1 ) ) )
416 ovex 6107 . . . . . . 7  |-  ( ( x  -  B ) ^ ( M  + 
1 ) )  e. 
_V
417415, 94, 416fvmpt 5807 . . . . . 6  |-  ( x  e.  A  ->  (
( y  e.  A  |->  ( ( y  -  B ) ^ ( M  +  1 ) ) ) `  x
)  =  ( ( x  -  B ) ^ ( M  + 
1 ) ) )
418408, 417syl 16 . . . . 5  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( y  e.  A  |->  ( ( y  -  B ) ^
( M  +  1 ) ) ) `  x )  =  ( ( x  -  B
) ^ ( M  +  1 ) ) )
419414, 418oveq12d 6100 . . . 4  |-  ( (
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 )  /  ( ( y  e.  A  |->  ( ( y  -  B ) ^ ( M  + 
1 ) ) ) `
 x ) )  =  ( ( ( ( ( RR  D n F ) `  ( N  -  ( M  +  1 ) ) ) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  ( M  + 
1 ) ) ) `
 x ) )  /  ( ( x  -  B ) ^
( M  +  1 ) ) ) )
420419mpteq2dva 4296 . . 3  |-  ( ph  ->  ( x  e.  ( A  \  { B } )  |->  ( ( ( y  e.  A  |->  ( ( ( ( RR  D n F ) `  ( N  -  ( M  + 
1 ) ) ) `
 y )  -  ( ( ( CC  D n T ) `
 ( N  -  ( M  +  1
)