Metamath Proof Explorer


Theorem taylthlem2

Description: Lemma for taylth . (Contributed by Mario Carneiro, 1-Jan-2017)

Ref Expression
Hypotheses taylth.f
|- ( ph -> F : A --> RR )
taylth.a
|- ( ph -> A C_ RR )
taylth.d
|- ( ph -> dom ( ( RR Dn 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 Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ) limCC B ) )
Assertion taylthlem2
|- ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` x ) ) / ( ( x - B ) ^ ( M + 1 ) ) ) ) limCC B ) )

Proof

Step Hyp Ref Expression
1 taylth.f
 |-  ( ph -> F : A --> RR )
2 taylth.a
 |-  ( ph -> A C_ RR )
3 taylth.d
 |-  ( ph -> dom ( ( RR Dn F ) ` N ) = A )
4 taylth.n
 |-  ( ph -> N e. NN )
5 taylth.b
 |-  ( ph -> B e. A )
6 taylth.t
 |-  T = ( N ( RR Tayl F ) B )
7 taylthlem2.m
 |-  ( ph -> M e. ( 1 ..^ N ) )
8 taylthlem2.i
 |-  ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ) limCC B ) )
9 fz1ssfz0
 |-  ( 1 ... N ) C_ ( 0 ... N )
10 fzofzp1
 |-  ( M e. ( 1 ..^ N ) -> ( M + 1 ) e. ( 1 ... N ) )
11 7 10 syl
 |-  ( ph -> ( M + 1 ) e. ( 1 ... N ) )
12 9 11 sselid
 |-  ( ph -> ( M + 1 ) e. ( 0 ... N ) )
13 fznn0sub2
 |-  ( ( M + 1 ) e. ( 0 ... N ) -> ( N - ( M + 1 ) ) e. ( 0 ... N ) )
14 12 13 syl
 |-  ( ph -> ( N - ( M + 1 ) ) e. ( 0 ... N ) )
15 elfznn0
 |-  ( ( N - ( M + 1 ) ) e. ( 0 ... N ) -> ( N - ( M + 1 ) ) e. NN0 )
16 14 15 syl
 |-  ( ph -> ( N - ( M + 1 ) ) e. NN0 )
17 dvnfre
 |-  ( ( F : A --> RR /\ A C_ RR /\ ( N - ( M + 1 ) ) e. NN0 ) -> ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) : dom ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) --> RR )
18 1 2 16 17 syl3anc
 |-  ( ph -> ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) : dom ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) --> RR )
19 reelprrecn
 |-  RR e. { RR , CC }
20 19 a1i
 |-  ( ph -> RR e. { RR , CC } )
21 cnex
 |-  CC e. _V
22 21 a1i
 |-  ( ph -> CC e. _V )
23 reex
 |-  RR e. _V
24 23 a1i
 |-  ( ph -> RR e. _V )
25 ax-resscn
 |-  RR C_ CC
26 fss
 |-  ( ( F : A --> RR /\ RR C_ CC ) -> F : A --> CC )
27 1 25 26 sylancl
 |-  ( ph -> F : A --> CC )
28 elpm2r
 |-  ( ( ( CC e. _V /\ RR e. _V ) /\ ( F : A --> CC /\ A C_ RR ) ) -> F e. ( CC ^pm RR ) )
29 22 24 27 2 28 syl22anc
 |-  ( ph -> F e. ( CC ^pm RR ) )
30 dvnbss
 |-  ( ( RR e. { RR , CC } /\ F e. ( CC ^pm RR ) /\ ( N - ( M + 1 ) ) e. NN0 ) -> dom ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) C_ dom F )
31 20 29 16 30 syl3anc
 |-  ( ph -> dom ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) C_ dom F )
32 1 31 fssdmd
 |-  ( ph -> dom ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) C_ A )
33 dvn2bss
 |-  ( ( RR e. { RR , CC } /\ F e. ( CC ^pm RR ) /\ ( N - ( M + 1 ) ) e. ( 0 ... N ) ) -> dom ( ( RR Dn F ) ` N ) C_ dom ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) )
34 20 29 14 33 syl3anc
 |-  ( ph -> dom ( ( RR Dn F ) ` N ) C_ dom ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) )
35 3 34 eqsstrrd
 |-  ( ph -> A C_ dom ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) )
36 32 35 eqssd
 |-  ( ph -> dom ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) = A )
37 36 feq2d
 |-  ( ph -> ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) : dom ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) --> RR <-> ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) : A --> RR ) )
38 18 37 mpbid
 |-  ( ph -> ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) : A --> RR )
39 38 ffvelrnda
 |-  ( ( ph /\ y e. A ) -> ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) e. RR )
40 2 sselda
 |-  ( ( ph /\ y e. A ) -> y e. RR )
41 fvres
 |-  ( y e. RR -> ( ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) |` RR ) ` y ) = ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) )
42 41 adantl
 |-  ( ( ph /\ y e. RR ) -> ( ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) |` RR ) ` y ) = ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) )
43 resubdrg
 |-  ( RR e. ( SubRing ` CCfld ) /\ RRfld e. DivRing )
44 43 simpli
 |-  RR e. ( SubRing ` CCfld )
45 44 a1i
 |-  ( ph -> RR e. ( SubRing ` CCfld ) )
46 4 nnnn0d
 |-  ( ph -> N e. NN0 )
47 5 3 eleqtrrd
 |-  ( ph -> B e. dom ( ( RR Dn F ) ` N ) )
48 2 5 sseldd
 |-  ( ph -> B e. RR )
49 elfznn0
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
50 dvnfre
 |-  ( ( F : A --> RR /\ A C_ RR /\ k e. NN0 ) -> ( ( RR Dn F ) ` k ) : dom ( ( RR Dn F ) ` k ) --> RR )
51 1 2 49 50 syl2an3an
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( RR Dn F ) ` k ) : dom ( ( RR Dn F ) ` k ) --> RR )
52 simpr
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> k e. ( 0 ... N ) )
53 dvn2bss
 |-  ( ( RR e. { RR , CC } /\ F e. ( CC ^pm RR ) /\ k e. ( 0 ... N ) ) -> dom ( ( RR Dn F ) ` N ) C_ dom ( ( RR Dn F ) ` k ) )
54 19 29 52 53 mp3an2ani
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> dom ( ( RR Dn F ) ` N ) C_ dom ( ( RR Dn F ) ` k ) )
55 47 adantr
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> B e. dom ( ( RR Dn F ) ` N ) )
56 54 55 sseldd
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> B e. dom ( ( RR Dn F ) ` k ) )
57 51 56 ffvelrnd
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( RR Dn F ) ` k ) ` B ) e. RR )
58 49 adantl
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> k e. NN0 )
59 58 faccld
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ! ` k ) e. NN )
60 57 59 nndivred
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( ( ( RR Dn F ) ` k ) ` B ) / ( ! ` k ) ) e. RR )
61 20 27 2 46 47 6 45 48 60 taylply2
 |-  ( ph -> ( T e. ( Poly ` RR ) /\ ( deg ` T ) <_ N ) )
62 61 simpld
 |-  ( ph -> T e. ( Poly ` RR ) )
63 dvnply2
 |-  ( ( RR e. ( SubRing ` CCfld ) /\ T e. ( Poly ` RR ) /\ ( N - ( M + 1 ) ) e. NN0 ) -> ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) e. ( Poly ` RR ) )
64 45 62 16 63 syl3anc
 |-  ( ph -> ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) e. ( Poly ` RR ) )
65 plyreres
 |-  ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) e. ( Poly ` RR ) -> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) |` RR ) : RR --> RR )
66 64 65 syl
 |-  ( ph -> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) |` RR ) : RR --> RR )
67 66 ffvelrnda
 |-  ( ( ph /\ y e. RR ) -> ( ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) |` RR ) ` y ) e. RR )
68 42 67 eqeltrrd
 |-  ( ( ph /\ y e. RR ) -> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) e. RR )
69 40 68 syldan
 |-  ( ( ph /\ y e. A ) -> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) e. RR )
70 39 69 resubcld
 |-  ( ( ph /\ y e. A ) -> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) e. RR )
71 70 fmpttd
 |-  ( ph -> ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) : A --> RR )
72 48 adantr
 |-  ( ( ph /\ y e. A ) -> B e. RR )
73 40 72 resubcld
 |-  ( ( ph /\ y e. A ) -> ( y - B ) e. RR )
74 elfzouz
 |-  ( M e. ( 1 ..^ N ) -> M e. ( ZZ>= ` 1 ) )
75 7 74 syl
 |-  ( ph -> M e. ( ZZ>= ` 1 ) )
76 nnuz
 |-  NN = ( ZZ>= ` 1 )
77 75 76 eleqtrrdi
 |-  ( ph -> M e. NN )
78 77 nnnn0d
 |-  ( ph -> M e. NN0 )
79 78 adantr
 |-  ( ( ph /\ y e. A ) -> M e. NN0 )
80 1nn0
 |-  1 e. NN0
81 80 a1i
 |-  ( ( ph /\ y e. A ) -> 1 e. NN0 )
82 79 81 nn0addcld
 |-  ( ( ph /\ y e. A ) -> ( M + 1 ) e. NN0 )
83 73 82 reexpcld
 |-  ( ( ph /\ y e. A ) -> ( ( y - B ) ^ ( M + 1 ) ) e. RR )
84 83 fmpttd
 |-  ( ph -> ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) : A --> RR )
85 retop
 |-  ( topGen ` ran (,) ) e. Top
86 uniretop
 |-  RR = U. ( topGen ` ran (,) )
87 86 ntrss2
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ A C_ RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) C_ A )
88 85 2 87 sylancr
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) C_ A )
89 4 nncnd
 |-  ( ph -> N e. CC )
90 77 nncnd
 |-  ( ph -> M e. CC )
91 1cnd
 |-  ( ph -> 1 e. CC )
92 89 90 91 nppcan2d
 |-  ( ph -> ( ( N - ( M + 1 ) ) + 1 ) = ( N - M ) )
93 92 fveq2d
 |-  ( ph -> ( ( RR Dn F ) ` ( ( N - ( M + 1 ) ) + 1 ) ) = ( ( RR Dn F ) ` ( N - M ) ) )
94 25 a1i
 |-  ( ph -> RR C_ CC )
95 dvnp1
 |-  ( ( RR C_ CC /\ F e. ( CC ^pm RR ) /\ ( N - ( M + 1 ) ) e. NN0 ) -> ( ( RR Dn F ) ` ( ( N - ( M + 1 ) ) + 1 ) ) = ( RR _D ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ) )
96 94 29 16 95 syl3anc
 |-  ( ph -> ( ( RR Dn F ) ` ( ( N - ( M + 1 ) ) + 1 ) ) = ( RR _D ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ) )
97 93 96 eqtr3d
 |-  ( ph -> ( ( RR Dn F ) ` ( N - M ) ) = ( RR _D ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ) )
98 97 dmeqd
 |-  ( ph -> dom ( ( RR Dn F ) ` ( N - M ) ) = dom ( RR _D ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ) )
99 fzonnsub
 |-  ( M e. ( 1 ..^ N ) -> ( N - M ) e. NN )
100 7 99 syl
 |-  ( ph -> ( N - M ) e. NN )
101 100 nnnn0d
 |-  ( ph -> ( N - M ) e. NN0 )
102 dvnbss
 |-  ( ( RR e. { RR , CC } /\ F e. ( CC ^pm RR ) /\ ( N - M ) e. NN0 ) -> dom ( ( RR Dn F ) ` ( N - M ) ) C_ dom F )
103 20 29 101 102 syl3anc
 |-  ( ph -> dom ( ( RR Dn F ) ` ( N - M ) ) C_ dom F )
104 1 103 fssdmd
 |-  ( ph -> dom ( ( RR Dn F ) ` ( N - M ) ) C_ A )
105 elfzofz
 |-  ( M e. ( 1 ..^ N ) -> M e. ( 1 ... N ) )
106 7 105 syl
 |-  ( ph -> M e. ( 1 ... N ) )
107 9 106 sselid
 |-  ( ph -> M e. ( 0 ... N ) )
108 fznn0sub2
 |-  ( M e. ( 0 ... N ) -> ( N - M ) e. ( 0 ... N ) )
109 107 108 syl
 |-  ( ph -> ( N - M ) e. ( 0 ... N ) )
110 dvn2bss
 |-  ( ( RR e. { RR , CC } /\ F e. ( CC ^pm RR ) /\ ( N - M ) e. ( 0 ... N ) ) -> dom ( ( RR Dn F ) ` N ) C_ dom ( ( RR Dn F ) ` ( N - M ) ) )
111 20 29 109 110 syl3anc
 |-  ( ph -> dom ( ( RR Dn F ) ` N ) C_ dom ( ( RR Dn F ) ` ( N - M ) ) )
112 3 111 eqsstrrd
 |-  ( ph -> A C_ dom ( ( RR Dn F ) ` ( N - M ) ) )
113 104 112 eqssd
 |-  ( ph -> dom ( ( RR Dn F ) ` ( N - M ) ) = A )
114 98 113 eqtr3d
 |-  ( ph -> dom ( RR _D ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ) = A )
115 fss
 |-  ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) : A --> RR /\ RR C_ CC ) -> ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) : A --> CC )
116 38 25 115 sylancl
 |-  ( ph -> ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) : A --> CC )
117 eqid
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
118 117 tgioo2
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
119 94 116 2 118 117 dvbssntr
 |-  ( ph -> dom ( RR _D ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ) C_ ( ( int ` ( topGen ` ran (,) ) ) ` A ) )
120 114 119 eqsstrrd
 |-  ( ph -> A C_ ( ( int ` ( topGen ` ran (,) ) ) ` A ) )
121 88 120 eqssd
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) = A )
122 86 isopn3
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ A C_ RR ) -> ( A e. ( topGen ` ran (,) ) <-> ( ( int ` ( topGen ` ran (,) ) ) ` A ) = A ) )
123 85 2 122 sylancr
 |-  ( ph -> ( A e. ( topGen ` ran (,) ) <-> ( ( int ` ( topGen ` ran (,) ) ) ` A ) = A ) )
124 121 123 mpbird
 |-  ( ph -> A e. ( topGen ` ran (,) ) )
125 eqid
 |-  ( A \ { B } ) = ( A \ { B } )
126 difss
 |-  ( A \ { B } ) C_ A
127 39 recnd
 |-  ( ( ph /\ y e. A ) -> ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) e. CC )
128 dvnf
 |-  ( ( RR e. { RR , CC } /\ F e. ( CC ^pm RR ) /\ ( N - M ) e. NN0 ) -> ( ( RR Dn F ) ` ( N - M ) ) : dom ( ( RR Dn F ) ` ( N - M ) ) --> CC )
129 20 29 101 128 syl3anc
 |-  ( ph -> ( ( RR Dn F ) ` ( N - M ) ) : dom ( ( RR Dn F ) ` ( N - M ) ) --> CC )
130 113 feq2d
 |-  ( ph -> ( ( ( RR Dn F ) ` ( N - M ) ) : dom ( ( RR Dn F ) ` ( N - M ) ) --> CC <-> ( ( RR Dn F ) ` ( N - M ) ) : A --> CC ) )
131 129 130 mpbid
 |-  ( ph -> ( ( RR Dn F ) ` ( N - M ) ) : A --> CC )
132 131 ffvelrnda
 |-  ( ( ph /\ y e. A ) -> ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) e. CC )
133 dvnfre
 |-  ( ( F : A --> RR /\ A C_ RR /\ ( N - M ) e. NN0 ) -> ( ( RR Dn F ) ` ( N - M ) ) : dom ( ( RR Dn F ) ` ( N - M ) ) --> RR )
134 1 2 101 133 syl3anc
 |-  ( ph -> ( ( RR Dn F ) ` ( N - M ) ) : dom ( ( RR Dn F ) ` ( N - M ) ) --> RR )
135 113 feq2d
 |-  ( ph -> ( ( ( RR Dn F ) ` ( N - M ) ) : dom ( ( RR Dn F ) ` ( N - M ) ) --> RR <-> ( ( RR Dn F ) ` ( N - M ) ) : A --> RR ) )
136 134 135 mpbid
 |-  ( ph -> ( ( RR Dn F ) ` ( N - M ) ) : A --> RR )
137 136 feqmptd
 |-  ( ph -> ( ( RR Dn F ) ` ( N - M ) ) = ( y e. A |-> ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) ) )
138 38 feqmptd
 |-  ( ph -> ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) = ( y e. A |-> ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) ) )
139 138 oveq2d
 |-  ( ph -> ( RR _D ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ) = ( RR _D ( y e. A |-> ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) )
140 97 137 139 3eqtr3rd
 |-  ( ph -> ( RR _D ( y e. A |-> ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) = ( y e. A |-> ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) ) )
141 69 recnd
 |-  ( ( ph /\ y e. A ) -> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) e. CC )
142 fvexd
 |-  ( ( ph /\ y e. A ) -> ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) e. _V )
143 68 recnd
 |-  ( ( ph /\ y e. RR ) -> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) e. CC )
144 recn
 |-  ( y e. RR -> y e. CC )
145 dvnply2
 |-  ( ( RR e. ( SubRing ` CCfld ) /\ T e. ( Poly ` RR ) /\ ( N - M ) e. NN0 ) -> ( ( CC Dn T ) ` ( N - M ) ) e. ( Poly ` RR ) )
146 45 62 101 145 syl3anc
 |-  ( ph -> ( ( CC Dn T ) ` ( N - M ) ) e. ( Poly ` RR ) )
147 plyf
 |-  ( ( ( CC Dn T ) ` ( N - M ) ) e. ( Poly ` RR ) -> ( ( CC Dn T ) ` ( N - M ) ) : CC --> CC )
148 146 147 syl
 |-  ( ph -> ( ( CC Dn T ) ` ( N - M ) ) : CC --> CC )
149 148 ffvelrnda
 |-  ( ( ph /\ y e. CC ) -> ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) e. CC )
150 144 149 sylan2
 |-  ( ( ph /\ y e. RR ) -> ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) e. CC )
151 117 cnfldtopon
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
152 toponmax
 |-  ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) -> CC e. ( TopOpen ` CCfld ) )
153 151 152 mp1i
 |-  ( ph -> CC e. ( TopOpen ` CCfld ) )
154 df-ss
 |-  ( RR C_ CC <-> ( RR i^i CC ) = RR )
155 94 154 sylib
 |-  ( ph -> ( RR i^i CC ) = RR )
156 plyf
 |-  ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) e. ( Poly ` RR ) -> ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) : CC --> CC )
157 64 156 syl
 |-  ( ph -> ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) : CC --> CC )
158 157 ffvelrnda
 |-  ( ( ph /\ y e. CC ) -> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) e. CC )
159 92 fveq2d
 |-  ( ph -> ( ( CC Dn T ) ` ( ( N - ( M + 1 ) ) + 1 ) ) = ( ( CC Dn T ) ` ( N - M ) ) )
160 ssid
 |-  CC C_ CC
161 160 a1i
 |-  ( ph -> CC C_ CC )
162 mapsspm
 |-  ( CC ^m CC ) C_ ( CC ^pm CC )
163 plyf
 |-  ( T e. ( Poly ` RR ) -> T : CC --> CC )
164 62 163 syl
 |-  ( ph -> T : CC --> CC )
165 21 21 elmap
 |-  ( T e. ( CC ^m CC ) <-> T : CC --> CC )
166 164 165 sylibr
 |-  ( ph -> T e. ( CC ^m CC ) )
167 162 166 sselid
 |-  ( ph -> T e. ( CC ^pm CC ) )
168 dvnp1
 |-  ( ( CC C_ CC /\ T e. ( CC ^pm CC ) /\ ( N - ( M + 1 ) ) e. NN0 ) -> ( ( CC Dn T ) ` ( ( N - ( M + 1 ) ) + 1 ) ) = ( CC _D ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ) )
169 161 167 16 168 syl3anc
 |-  ( ph -> ( ( CC Dn T ) ` ( ( N - ( M + 1 ) ) + 1 ) ) = ( CC _D ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ) )
170 159 169 eqtr3d
 |-  ( ph -> ( ( CC Dn T ) ` ( N - M ) ) = ( CC _D ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ) )
171 148 feqmptd
 |-  ( ph -> ( ( CC Dn T ) ` ( N - M ) ) = ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) )
172 157 feqmptd
 |-  ( ph -> ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) = ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) )
173 172 oveq2d
 |-  ( ph -> ( CC _D ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ) = ( CC _D ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) )
174 170 171 173 3eqtr3rd
 |-  ( ph -> ( CC _D ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) = ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) )
175 117 20 153 155 158 149 174 dvmptres3
 |-  ( ph -> ( RR _D ( y e. RR |-> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) = ( y e. RR |-> ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) )
176 20 143 150 175 2 118 117 124 dvmptres
 |-  ( ph -> ( RR _D ( y e. A |-> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) = ( y e. A |-> ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) )
177 20 127 132 140 141 142 176 dvmptsub
 |-  ( ph -> ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) = ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) ) )
178 177 dmeqd
 |-  ( ph -> dom ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) = dom ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) ) )
179 ovex
 |-  ( ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) e. _V
180 eqid
 |-  ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) ) = ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) )
181 179 180 dmmpti
 |-  dom ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) ) = A
182 178 181 eqtrdi
 |-  ( ph -> dom ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) = A )
183 126 182 sseqtrrid
 |-  ( ph -> ( A \ { B } ) C_ dom ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) )
184 simpr
 |-  ( ( ph /\ y e. CC ) -> y e. CC )
185 48 adantr
 |-  ( ( ph /\ y e. CC ) -> B e. RR )
186 185 recnd
 |-  ( ( ph /\ y e. CC ) -> B e. CC )
187 184 186 subcld
 |-  ( ( ph /\ y e. CC ) -> ( y - B ) e. CC )
188 78 adantr
 |-  ( ( ph /\ y e. CC ) -> M e. NN0 )
189 80 a1i
 |-  ( ( ph /\ y e. CC ) -> 1 e. NN0 )
190 188 189 nn0addcld
 |-  ( ( ph /\ y e. CC ) -> ( M + 1 ) e. NN0 )
191 187 190 expcld
 |-  ( ( ph /\ y e. CC ) -> ( ( y - B ) ^ ( M + 1 ) ) e. CC )
192 144 191 sylan2
 |-  ( ( ph /\ y e. RR ) -> ( ( y - B ) ^ ( M + 1 ) ) e. CC )
193 90 adantr
 |-  ( ( ph /\ y e. CC ) -> M e. CC )
194 1cnd
 |-  ( ( ph /\ y e. CC ) -> 1 e. CC )
195 193 194 addcld
 |-  ( ( ph /\ y e. CC ) -> ( M + 1 ) e. CC )
196 187 188 expcld
 |-  ( ( ph /\ y e. CC ) -> ( ( y - B ) ^ M ) e. CC )
197 195 196 mulcld
 |-  ( ( ph /\ y e. CC ) -> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) e. CC )
198 144 197 sylan2
 |-  ( ( ph /\ y e. RR ) -> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) e. CC )
199 21 prid2
 |-  CC e. { RR , CC }
200 199 a1i
 |-  ( ph -> CC e. { RR , CC } )
201 simpr
 |-  ( ( ph /\ x e. CC ) -> x e. CC )
202 elfznn
 |-  ( ( M + 1 ) e. ( 1 ... N ) -> ( M + 1 ) e. NN )
203 11 202 syl
 |-  ( ph -> ( M + 1 ) e. NN )
204 203 nnnn0d
 |-  ( ph -> ( M + 1 ) e. NN0 )
205 204 adantr
 |-  ( ( ph /\ x e. CC ) -> ( M + 1 ) e. NN0 )
206 201 205 expcld
 |-  ( ( ph /\ x e. CC ) -> ( x ^ ( M + 1 ) ) e. CC )
207 ovexd
 |-  ( ( ph /\ x e. CC ) -> ( ( M + 1 ) x. ( x ^ M ) ) e. _V )
208 200 dvmptid
 |-  ( ph -> ( CC _D ( y e. CC |-> y ) ) = ( y e. CC |-> 1 ) )
209 0cnd
 |-  ( ( ph /\ y e. CC ) -> 0 e. CC )
210 48 recnd
 |-  ( ph -> B e. CC )
211 200 210 dvmptc
 |-  ( ph -> ( CC _D ( y e. CC |-> B ) ) = ( y e. CC |-> 0 ) )
212 200 184 194 208 186 209 211 dvmptsub
 |-  ( ph -> ( CC _D ( y e. CC |-> ( y - B ) ) ) = ( y e. CC |-> ( 1 - 0 ) ) )
213 1m0e1
 |-  ( 1 - 0 ) = 1
214 213 mpteq2i
 |-  ( y e. CC |-> ( 1 - 0 ) ) = ( y e. CC |-> 1 )
215 212 214 eqtrdi
 |-  ( ph -> ( CC _D ( y e. CC |-> ( y - B ) ) ) = ( y e. CC |-> 1 ) )
216 dvexp
 |-  ( ( M + 1 ) e. NN -> ( CC _D ( x e. CC |-> ( x ^ ( M + 1 ) ) ) ) = ( x e. CC |-> ( ( M + 1 ) x. ( x ^ ( ( M + 1 ) - 1 ) ) ) ) )
217 203 216 syl
 |-  ( ph -> ( CC _D ( x e. CC |-> ( x ^ ( M + 1 ) ) ) ) = ( x e. CC |-> ( ( M + 1 ) x. ( x ^ ( ( M + 1 ) - 1 ) ) ) ) )
218 90 91 pncand
 |-  ( ph -> ( ( M + 1 ) - 1 ) = M )
219 218 oveq2d
 |-  ( ph -> ( x ^ ( ( M + 1 ) - 1 ) ) = ( x ^ M ) )
220 219 oveq2d
 |-  ( ph -> ( ( M + 1 ) x. ( x ^ ( ( M + 1 ) - 1 ) ) ) = ( ( M + 1 ) x. ( x ^ M ) ) )
221 220 mpteq2dv
 |-  ( ph -> ( x e. CC |-> ( ( M + 1 ) x. ( x ^ ( ( M + 1 ) - 1 ) ) ) ) = ( x e. CC |-> ( ( M + 1 ) x. ( x ^ M ) ) ) )
222 217 221 eqtrd
 |-  ( ph -> ( CC _D ( x e. CC |-> ( x ^ ( M + 1 ) ) ) ) = ( x e. CC |-> ( ( M + 1 ) x. ( x ^ M ) ) ) )
223 oveq1
 |-  ( x = ( y - B ) -> ( x ^ ( M + 1 ) ) = ( ( y - B ) ^ ( M + 1 ) ) )
224 oveq1
 |-  ( x = ( y - B ) -> ( x ^ M ) = ( ( y - B ) ^ M ) )
225 224 oveq2d
 |-  ( x = ( y - B ) -> ( ( M + 1 ) x. ( x ^ M ) ) = ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) )
226 200 200 187 194 206 207 215 222 223 225 dvmptco
 |-  ( ph -> ( CC _D ( y e. CC |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) = ( y e. CC |-> ( ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) x. 1 ) ) )
227 197 mulid1d
 |-  ( ( ph /\ y e. CC ) -> ( ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) x. 1 ) = ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) )
228 227 mpteq2dva
 |-  ( ph -> ( y e. CC |-> ( ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) x. 1 ) ) = ( y e. CC |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) )
229 226 228 eqtrd
 |-  ( ph -> ( CC _D ( y e. CC |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) = ( y e. CC |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) )
230 117 20 153 155 191 197 229 dvmptres3
 |-  ( ph -> ( RR _D ( y e. RR |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) = ( y e. RR |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) )
231 20 192 198 230 2 118 117 124 dvmptres
 |-  ( ph -> ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) = ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) )
232 231 dmeqd
 |-  ( ph -> dom ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) = dom ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) )
233 ovex
 |-  ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) e. _V
234 eqid
 |-  ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) = ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) )
235 233 234 dmmpti
 |-  dom ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) = A
236 232 235 eqtrdi
 |-  ( ph -> dom ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) = A )
237 126 236 sseqtrrid
 |-  ( ph -> ( A \ { B } ) C_ dom ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) )
238 20 27 2 14 47 6 dvntaylp0
 |-  ( ph -> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` B ) = ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) )
239 238 oveq2d
 |-  ( ph -> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` B ) ) = ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) - ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) ) )
240 116 5 ffvelrnd
 |-  ( ph -> ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) e. CC )
241 240 subidd
 |-  ( ph -> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) - ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) ) = 0 )
242 239 241 eqtrd
 |-  ( ph -> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` B ) ) = 0 )
243 117 subcn
 |-  - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
244 243 a1i
 |-  ( ph -> - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
245 dvcn
 |-  ( ( ( RR C_ CC /\ ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) : A --> CC /\ A C_ RR ) /\ dom ( RR _D ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ) = A ) -> ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) e. ( A -cn-> CC ) )
246 94 116 2 114 245 syl31anc
 |-  ( ph -> ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) e. ( A -cn-> CC ) )
247 138 246 eqeltrrd
 |-  ( ph -> ( y e. A |-> ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) ) e. ( A -cn-> CC ) )
248 plycn
 |-  ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) e. ( Poly ` RR ) -> ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) e. ( CC -cn-> CC ) )
249 64 248 syl
 |-  ( ph -> ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) e. ( CC -cn-> CC ) )
250 2 25 sstrdi
 |-  ( ph -> A C_ CC )
251 cncfmptid
 |-  ( ( A C_ CC /\ CC C_ CC ) -> ( y e. A |-> y ) e. ( A -cn-> CC ) )
252 250 160 251 sylancl
 |-  ( ph -> ( y e. A |-> y ) e. ( A -cn-> CC ) )
253 249 252 cncfmpt1f
 |-  ( ph -> ( y e. A |-> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) e. ( A -cn-> CC ) )
254 117 244 247 253 cncfmpt2f
 |-  ( ph -> ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) e. ( A -cn-> CC ) )
255 fveq2
 |-  ( y = B -> ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) = ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) )
256 fveq2
 |-  ( y = B -> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) = ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` B ) )
257 255 256 oveq12d
 |-  ( y = B -> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) = ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` B ) ) )
258 254 5 257 cnmptlimc
 |-  ( ph -> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` B ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` B ) ) e. ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) limCC B ) )
259 242 258 eqeltrrd
 |-  ( ph -> 0 e. ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) limCC B ) )
260 210 subidd
 |-  ( ph -> ( B - B ) = 0 )
261 260 oveq1d
 |-  ( ph -> ( ( B - B ) ^ ( M + 1 ) ) = ( 0 ^ ( M + 1 ) ) )
262 203 0expd
 |-  ( ph -> ( 0 ^ ( M + 1 ) ) = 0 )
263 261 262 eqtrd
 |-  ( ph -> ( ( B - B ) ^ ( M + 1 ) ) = 0 )
264 250 sselda
 |-  ( ( ph /\ y e. A ) -> y e. CC )
265 264 191 syldan
 |-  ( ( ph /\ y e. A ) -> ( ( y - B ) ^ ( M + 1 ) ) e. CC )
266 265 fmpttd
 |-  ( ph -> ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) : A --> CC )
267 dvcn
 |-  ( ( ( 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 ) )
268 94 266 2 236 267 syl31anc
 |-  ( ph -> ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) e. ( A -cn-> CC ) )
269 oveq1
 |-  ( y = B -> ( y - B ) = ( B - B ) )
270 269 oveq1d
 |-  ( y = B -> ( ( y - B ) ^ ( M + 1 ) ) = ( ( B - B ) ^ ( M + 1 ) ) )
271 268 5 270 cnmptlimc
 |-  ( ph -> ( ( B - B ) ^ ( M + 1 ) ) e. ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) limCC B ) )
272 263 271 eqeltrrd
 |-  ( ph -> 0 e. ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) limCC B ) )
273 250 ssdifssd
 |-  ( ph -> ( A \ { B } ) C_ CC )
274 273 sselda
 |-  ( ( ph /\ y e. ( A \ { B } ) ) -> y e. CC )
275 210 adantr
 |-  ( ( ph /\ y e. ( A \ { B } ) ) -> B e. CC )
276 274 275 subcld
 |-  ( ( ph /\ y e. ( A \ { B } ) ) -> ( y - B ) e. CC )
277 eldifsni
 |-  ( y e. ( A \ { B } ) -> y =/= B )
278 277 adantl
 |-  ( ( ph /\ y e. ( A \ { B } ) ) -> y =/= B )
279 274 275 278 subne0d
 |-  ( ( ph /\ y e. ( A \ { B } ) ) -> ( y - B ) =/= 0 )
280 203 adantr
 |-  ( ( ph /\ y e. ( A \ { B } ) ) -> ( M + 1 ) e. NN )
281 280 nnzd
 |-  ( ( ph /\ y e. ( A \ { B } ) ) -> ( M + 1 ) e. ZZ )
282 276 279 281 expne0d
 |-  ( ( ph /\ y e. ( A \ { B } ) ) -> ( ( y - B ) ^ ( M + 1 ) ) =/= 0 )
283 282 necomd
 |-  ( ( ph /\ y e. ( A \ { B } ) ) -> 0 =/= ( ( y - B ) ^ ( M + 1 ) ) )
284 283 neneqd
 |-  ( ( ph /\ y e. ( A \ { B } ) ) -> -. 0 = ( ( y - B ) ^ ( M + 1 ) ) )
285 284 nrexdv
 |-  ( ph -> -. E. y e. ( A \ { B } ) 0 = ( ( y - B ) ^ ( M + 1 ) ) )
286 df-ima
 |-  ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) " ( A \ { B } ) ) = ran ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) |` ( A \ { B } ) )
287 286 eleq2i
 |-  ( 0 e. ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) " ( A \ { B } ) ) <-> 0 e. ran ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) |` ( A \ { B } ) ) )
288 resmpt
 |-  ( ( A \ { B } ) C_ A -> ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) |` ( A \ { B } ) ) = ( y e. ( A \ { B } ) |-> ( ( y - B ) ^ ( M + 1 ) ) ) )
289 126 288 ax-mp
 |-  ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) |` ( A \ { B } ) ) = ( y e. ( A \ { B } ) |-> ( ( y - B ) ^ ( M + 1 ) ) )
290 ovex
 |-  ( ( y - B ) ^ ( M + 1 ) ) e. _V
291 289 290 elrnmpti
 |-  ( 0 e. ran ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) |` ( A \ { B } ) ) <-> E. y e. ( A \ { B } ) 0 = ( ( y - B ) ^ ( M + 1 ) ) )
292 287 291 bitri
 |-  ( 0 e. ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) " ( A \ { B } ) ) <-> E. y e. ( A \ { B } ) 0 = ( ( y - B ) ^ ( M + 1 ) ) )
293 285 292 sylnibr
 |-  ( ph -> -. 0 e. ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) " ( A \ { B } ) ) )
294 90 adantr
 |-  ( ( ph /\ y e. ( A \ { B } ) ) -> M e. CC )
295 1cnd
 |-  ( ( ph /\ y e. ( A \ { B } ) ) -> 1 e. CC )
296 294 295 addcld
 |-  ( ( ph /\ y e. ( A \ { B } ) ) -> ( M + 1 ) e. CC )
297 274 196 syldan
 |-  ( ( ph /\ y e. ( A \ { B } ) ) -> ( ( y - B ) ^ M ) e. CC )
298 280 nnne0d
 |-  ( ( ph /\ y e. ( A \ { B } ) ) -> ( M + 1 ) =/= 0 )
299 77 adantr
 |-  ( ( ph /\ y e. ( A \ { B } ) ) -> M e. NN )
300 299 nnzd
 |-  ( ( ph /\ y e. ( A \ { B } ) ) -> M e. ZZ )
301 276 279 300 expne0d
 |-  ( ( ph /\ y e. ( A \ { B } ) ) -> ( ( y - B ) ^ M ) =/= 0 )
302 296 297 298 301 mulne0d
 |-  ( ( ph /\ y e. ( A \ { B } ) ) -> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) =/= 0 )
303 302 necomd
 |-  ( ( ph /\ y e. ( A \ { B } ) ) -> 0 =/= ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) )
304 303 neneqd
 |-  ( ( ph /\ y e. ( A \ { B } ) ) -> -. 0 = ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) )
305 304 nrexdv
 |-  ( ph -> -. E. y e. ( A \ { B } ) 0 = ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) )
306 231 imaeq1d
 |-  ( ph -> ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) " ( A \ { B } ) ) = ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) " ( A \ { B } ) ) )
307 df-ima
 |-  ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) " ( A \ { B } ) ) = ran ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) |` ( A \ { B } ) )
308 306 307 eqtrdi
 |-  ( ph -> ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) " ( A \ { B } ) ) = ran ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) |` ( A \ { B } ) ) )
309 308 eleq2d
 |-  ( 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 } ) ) ) )
310 resmpt
 |-  ( ( 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 ) ) ) )
311 126 310 ax-mp
 |-  ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) |` ( A \ { B } ) ) = ( y e. ( A \ { B } ) |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) )
312 311 233 elrnmpti
 |-  ( 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 ) ) )
313 309 312 bitrdi
 |-  ( 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 ) ) ) )
314 305 313 mtbird
 |-  ( ph -> -. 0 e. ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) " ( A \ { B } ) ) )
315 eldifi
 |-  ( x e. ( A \ { B } ) -> x e. A )
316 131 ffvelrnda
 |-  ( ( ph /\ x e. A ) -> ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) e. CC )
317 315 316 sylan2
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) e. CC )
318 2 ssdifssd
 |-  ( ph -> ( A \ { B } ) C_ RR )
319 318 sselda
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> x e. RR )
320 319 recnd
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> x e. CC )
321 148 ffvelrnda
 |-  ( ( ph /\ x e. CC ) -> ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) e. CC )
322 320 321 syldan
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) e. CC )
323 317 322 subcld
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) e. CC )
324 48 adantr
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> B e. RR )
325 319 324 resubcld
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( x - B ) e. RR )
326 78 adantr
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> M e. NN0 )
327 325 326 reexpcld
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( x - B ) ^ M ) e. RR )
328 327 recnd
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( x - B ) ^ M ) e. CC )
329 324 recnd
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> B e. CC )
330 320 329 subcld
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( x - B ) e. CC )
331 eldifsni
 |-  ( x e. ( A \ { B } ) -> x =/= B )
332 331 adantl
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> x =/= B )
333 320 329 332 subne0d
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( x - B ) =/= 0 )
334 326 nn0zd
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> M e. ZZ )
335 330 333 334 expne0d
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( x - B ) ^ M ) =/= 0 )
336 323 328 335 divcld
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) e. CC )
337 203 nnrecred
 |-  ( ph -> ( 1 / ( M + 1 ) ) e. RR )
338 337 recnd
 |-  ( ph -> ( 1 / ( M + 1 ) ) e. CC )
339 338 adantr
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( 1 / ( M + 1 ) ) e. CC )
340 txtopon
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) -> ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) e. ( TopOn ` ( CC X. CC ) ) )
341 151 151 340 mp2an
 |-  ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) e. ( TopOn ` ( CC X. CC ) )
342 341 toponrestid
 |-  ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) = ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) |`t ( CC X. CC ) )
343 limcresi
 |-  ( ( x e. A |-> ( 1 / ( M + 1 ) ) ) limCC B ) C_ ( ( ( x e. A |-> ( 1 / ( M + 1 ) ) ) |` ( A \ { B } ) ) limCC B )
344 resmpt
 |-  ( ( A \ { B } ) C_ A -> ( ( x e. A |-> ( 1 / ( M + 1 ) ) ) |` ( A \ { B } ) ) = ( x e. ( A \ { B } ) |-> ( 1 / ( M + 1 ) ) ) )
345 126 344 ax-mp
 |-  ( ( x e. A |-> ( 1 / ( M + 1 ) ) ) |` ( A \ { B } ) ) = ( x e. ( A \ { B } ) |-> ( 1 / ( M + 1 ) ) )
346 345 oveq1i
 |-  ( ( ( x e. A |-> ( 1 / ( M + 1 ) ) ) |` ( A \ { B } ) ) limCC B ) = ( ( x e. ( A \ { B } ) |-> ( 1 / ( M + 1 ) ) ) limCC B )
347 343 346 sseqtri
 |-  ( ( x e. A |-> ( 1 / ( M + 1 ) ) ) limCC B ) C_ ( ( x e. ( A \ { B } ) |-> ( 1 / ( M + 1 ) ) ) limCC B )
348 cncfmptc
 |-  ( ( ( 1 / ( M + 1 ) ) e. RR /\ A C_ CC /\ RR C_ CC ) -> ( x e. A |-> ( 1 / ( M + 1 ) ) ) e. ( A -cn-> RR ) )
349 337 250 94 348 syl3anc
 |-  ( ph -> ( x e. A |-> ( 1 / ( M + 1 ) ) ) e. ( A -cn-> RR ) )
350 eqidd
 |-  ( x = B -> ( 1 / ( M + 1 ) ) = ( 1 / ( M + 1 ) ) )
351 349 5 350 cnmptlimc
 |-  ( ph -> ( 1 / ( M + 1 ) ) e. ( ( x e. A |-> ( 1 / ( M + 1 ) ) ) limCC B ) )
352 347 351 sselid
 |-  ( ph -> ( 1 / ( M + 1 ) ) e. ( ( x e. ( A \ { B } ) |-> ( 1 / ( M + 1 ) ) ) limCC B ) )
353 117 mulcn
 |-  x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
354 0cn
 |-  0 e. CC
355 opelxpi
 |-  ( ( 0 e. CC /\ ( 1 / ( M + 1 ) ) e. CC ) -> <. 0 , ( 1 / ( M + 1 ) ) >. e. ( CC X. CC ) )
356 354 338 355 sylancr
 |-  ( ph -> <. 0 , ( 1 / ( M + 1 ) ) >. e. ( CC X. CC ) )
357 341 toponunii
 |-  ( CC X. CC ) = U. ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) )
358 357 cncnpi
 |-  ( ( x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) /\ <. 0 , ( 1 / ( M + 1 ) ) >. e. ( CC X. CC ) ) -> x. e. ( ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) CnP ( TopOpen ` CCfld ) ) ` <. 0 , ( 1 / ( M + 1 ) ) >. ) )
359 353 356 358 sylancr
 |-  ( ph -> x. e. ( ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) CnP ( TopOpen ` CCfld ) ) ` <. 0 , ( 1 / ( M + 1 ) ) >. ) )
360 336 339 161 161 117 342 8 352 359 limccnp2
 |-  ( ph -> ( 0 x. ( 1 / ( M + 1 ) ) ) e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) limCC B ) )
361 338 mul02d
 |-  ( ph -> ( 0 x. ( 1 / ( M + 1 ) ) ) = 0 )
362 177 fveq1d
 |-  ( ph -> ( ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) ` x ) = ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) ) ` x ) )
363 fveq2
 |-  ( y = x -> ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) = ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) )
364 fveq2
 |-  ( y = x -> ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) = ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) )
365 363 364 oveq12d
 |-  ( y = x -> ( ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) = ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) )
366 ovex
 |-  ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) e. _V
367 365 180 366 fvmpt
 |-  ( x e. A -> ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) ) ` x ) = ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) )
368 315 367 syl
 |-  ( x e. ( A \ { B } ) -> ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) ) ) ` x ) = ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) )
369 362 368 sylan9eq
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) ` x ) = ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) )
370 231 fveq1d
 |-  ( ph -> ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) ` x ) = ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) ` x ) )
371 oveq1
 |-  ( y = x -> ( y - B ) = ( x - B ) )
372 371 oveq1d
 |-  ( y = x -> ( ( y - B ) ^ M ) = ( ( x - B ) ^ M ) )
373 372 oveq2d
 |-  ( y = x -> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) = ( ( M + 1 ) x. ( ( x - B ) ^ M ) ) )
374 ovex
 |-  ( ( M + 1 ) x. ( ( x - B ) ^ M ) ) e. _V
375 373 234 374 fvmpt
 |-  ( x e. A -> ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) ` x ) = ( ( M + 1 ) x. ( ( x - B ) ^ M ) ) )
376 315 375 syl
 |-  ( x e. ( A \ { B } ) -> ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) ` x ) = ( ( M + 1 ) x. ( ( x - B ) ^ M ) ) )
377 370 376 sylan9eq
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) ` x ) = ( ( M + 1 ) x. ( ( x - B ) ^ M ) ) )
378 203 adantr
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( M + 1 ) e. NN )
379 378 nncnd
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( M + 1 ) e. CC )
380 379 328 mulcomd
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( M + 1 ) x. ( ( x - B ) ^ M ) ) = ( ( ( x - B ) ^ M ) x. ( M + 1 ) ) )
381 377 380 eqtrd
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) ` x ) = ( ( ( x - B ) ^ M ) x. ( M + 1 ) ) )
382 369 381 oveq12d
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) ` x ) / ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) ` x ) ) = ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( ( x - B ) ^ M ) x. ( M + 1 ) ) ) )
383 378 nnne0d
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( M + 1 ) =/= 0 )
384 323 328 379 335 383 divdiv1d
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) / ( M + 1 ) ) = ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( ( x - B ) ^ M ) x. ( M + 1 ) ) ) )
385 336 379 383 divrecd
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) / ( M + 1 ) ) = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) )
386 382 384 385 3eqtr2rd
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) = ( ( ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) ` x ) / ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) ` x ) ) )
387 386 mpteq2dva
 |-  ( ph -> ( x e. ( A \ { B } ) |-> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) = ( x e. ( A \ { B } ) |-> ( ( ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) ` x ) / ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) ` x ) ) ) )
388 387 oveq1d
 |-  ( ph -> ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) limCC B ) = ( ( x e. ( A \ { B } ) |-> ( ( ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) ` x ) / ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) ` x ) ) ) limCC B ) )
389 360 361 388 3eltr3d
 |-  ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( RR _D ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ) ` x ) / ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) ` x ) ) ) limCC B ) )
390 2 71 84 124 5 125 183 237 259 272 293 314 389 lhop
 |-  ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ` x ) / ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ` x ) ) ) limCC B ) )
391 315 adantl
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> x e. A )
392 fveq2
 |-  ( y = x -> ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) = ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` x ) )
393 fveq2
 |-  ( y = x -> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) = ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` x ) )
394 392 393 oveq12d
 |-  ( y = x -> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) = ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` x ) ) )
395 eqid
 |-  ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) = ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) )
396 ovex
 |-  ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` x ) ) e. _V
397 394 395 396 fvmpt
 |-  ( x e. A -> ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ` x ) = ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` x ) ) )
398 391 397 syl
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ` x ) = ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` x ) ) )
399 371 oveq1d
 |-  ( y = x -> ( ( y - B ) ^ ( M + 1 ) ) = ( ( x - B ) ^ ( M + 1 ) ) )
400 eqid
 |-  ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) = ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) )
401 ovex
 |-  ( ( x - B ) ^ ( M + 1 ) ) e. _V
402 399 400 401 fvmpt
 |-  ( x e. A -> ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ` x ) = ( ( x - B ) ^ ( M + 1 ) ) )
403 391 402 syl
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ` x ) = ( ( x - B ) ^ ( M + 1 ) ) )
404 398 403 oveq12d
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ` x ) / ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ` x ) ) = ( ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` x ) ) / ( ( x - B ) ^ ( M + 1 ) ) ) )
405 404 mpteq2dva
 |-  ( ph -> ( x e. ( A \ { B } ) |-> ( ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ` x ) / ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ` x ) ) ) = ( x e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` x ) ) / ( ( x - B ) ^ ( M + 1 ) ) ) ) )
406 405 oveq1d
 |-  ( ph -> ( ( x e. ( A \ { B } ) |-> ( ( ( y e. A |-> ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) ) ) ` x ) / ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ` x ) ) ) limCC B ) = ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` x ) ) / ( ( x - B ) ^ ( M + 1 ) ) ) ) limCC B ) )
407 390 406 eleqtrd
 |-  ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` x ) ) / ( ( x - B ) ^ ( M + 1 ) ) ) ) limCC B ) )