Metamath Proof Explorer

Theorem taylthlem2

Description: Lemma for taylth . (Contributed by Mario Carneiro, 1-Jan-2017) Avoid ax-mulf . (Revised by GG, 19-Apr-2025)

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 ffvelcdmda 
 |-  ( ( 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 ffvelcdmd 
 |-  ( ( 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 ffvelcdmda 
 |-  ( ( 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 tgioo4 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
118 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
119 94 116 2 117 118 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 ffvelcdmda 
 |-  ( ( 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 ffvelcdmda 
 |-  ( ( 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 118 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 dfss2 
 |-  ( 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 ffvelcdmda 
 |-  ( ( 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 118 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 117 118 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 mulridd 
 |-  ( ( 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 118 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 117 118 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 ffvelcdmd 
 |-  ( 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 118 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 118 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 ffvelcdmda 
 |-  ( ( 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 ffvelcdmda 
 |-  ( ( 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 118 mpomulcn 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) 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 
 |-  ( ( ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) /\ <. 0 , ( 1 / ( M + 1 ) ) >. e. ( CC X. CC ) ) -> ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) CnP ( TopOpen ` CCfld ) ) ` <. 0 , ( 1 / ( M + 1 ) ) >. ) )
359 353 356 358 sylancr 
 |-  ( ph -> ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) CnP ( TopOpen ` CCfld ) ) ` <. 0 , ( 1 / ( M + 1 ) ) >. ) )
360 336 339 161 161 118 342 8 352 359 limccnp2 
 |-  ( ph -> ( 0 ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) limCC B ) )
361 0cnd 
 |-  ( ph -> 0 e. CC )
362 361 338 jca 
 |-  ( ph -> ( 0 e. CC /\ ( 1 / ( M + 1 ) ) e. CC ) )
363 ovmpot 
 |-  ( ( 0 e. CC /\ ( 1 / ( M + 1 ) ) e. CC ) -> ( 0 ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) = ( 0 x. ( 1 / ( M + 1 ) ) ) )
364 362 363 syl 
 |-  ( ph -> ( 0 ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) = ( 0 x. ( 1 / ( M + 1 ) ) ) )
365 df-mpt 
 |-  ( x e. ( A \ { B } ) |-> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) = { <. x , z >. | ( x e. ( A \ { B } ) /\ z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) }
366 365 a1i 
 |-  ( ph -> ( x e. ( A \ { B } ) |-> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) = { <. x , z >. | ( x e. ( A \ { B } ) /\ z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) } )
367 idd 
 |-  ( ph -> ( x e. ( A \ { B } ) -> x e. ( A \ { B } ) ) )
368 367 adantrd 
 |-  ( ph -> ( ( x e. ( A \ { B } ) /\ z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) -> x e. ( A \ { B } ) ) )
369 336 339 jca 
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) e. CC /\ ( 1 / ( M + 1 ) ) e. CC ) )
370 ovmpot 
 |-  ( ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) e. CC /\ ( 1 / ( M + 1 ) ) e. CC ) -> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) )
371 369 370 syl 
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) )
372 eqeq2 
 |-  ( ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) -> ( z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) <-> z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) )
373 372 biimpd 
 |-  ( ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) -> ( z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) -> z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) )
374 371 373 syl 
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) -> z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) )
375 374 ex 
 |-  ( ph -> ( x e. ( A \ { B } ) -> ( z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) -> z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) ) )
376 375 impd 
 |-  ( ph -> ( ( x e. ( A \ { B } ) /\ z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) -> z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) )
377 368 376 jcad 
 |-  ( ph -> ( ( x e. ( A \ { B } ) /\ z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) -> ( x e. ( A \ { B } ) /\ z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) ) )
378 367 adantrd 
 |-  ( ph -> ( ( x e. ( A \ { B } ) /\ z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) -> x e. ( A \ { B } ) ) )
379 370 eqcomd 
 |-  ( ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) e. CC /\ ( 1 / ( M + 1 ) ) e. CC ) -> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) )
380 369 379 syl 
 |-  ( ( 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 Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) )
381 eqeq2 
 |-  ( ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) -> ( z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) <-> z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) )
382 381 biimpd 
 |-  ( ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) -> ( z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) -> z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) )
383 380 382 syl 
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) -> z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) )
384 383 ex 
 |-  ( ph -> ( x e. ( A \ { B } ) -> ( z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) -> z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) ) )
385 384 impd 
 |-  ( ph -> ( ( x e. ( A \ { B } ) /\ z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) -> z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) )
386 378 385 jcad 
 |-  ( ph -> ( ( x e. ( A \ { B } ) /\ z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) -> ( x e. ( A \ { B } ) /\ z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) ) )
387 377 386 impbid 
 |-  ( ph -> ( ( x e. ( A \ { B } ) /\ z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) <-> ( x e. ( A \ { B } ) /\ z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) ) )
388 387 opabbidv 
 |-  ( ph -> { <. x , z >. | ( x e. ( A \ { B } ) /\ z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) } = { <. x , z >. | ( x e. ( A \ { B } ) /\ z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) } )
389 366 388 eqtrd 
 |-  ( ph -> ( x e. ( A \ { B } ) |-> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) = { <. x , z >. | ( x e. ( A \ { B } ) /\ z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) } )
390 df-mpt 
 |-  ( x e. ( A \ { B } ) |-> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) = { <. x , z >. | ( x e. ( A \ { B } ) /\ z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) }
391 390 eqcomi 
 |-  { <. x , z >. | ( x e. ( A \ { B } ) /\ z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) } = ( x e. ( A \ { B } ) |-> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) )
392 391 a1i 
 |-  ( ph -> { <. x , z >. | ( x e. ( A \ { B } ) /\ z = ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) } = ( x e. ( A \ { B } ) |-> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) )
393 389 392 eqtrd 
 |-  ( ph -> ( x e. ( A \ { B } ) |-> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) = ( x e. ( A \ { B } ) |-> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) x. ( 1 / ( M + 1 ) ) ) ) )
394 393 oveq1d 
 |-  ( ph -> ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) limCC B ) = ( ( 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 ) )
395 364 394 jca 
 |-  ( ph -> ( ( 0 ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) = ( 0 x. ( 1 / ( M + 1 ) ) ) /\ ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) limCC B ) = ( ( 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 ) ) )
396 eleq12 
 |-  ( ( ( 0 ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) = ( 0 x. ( 1 / ( M + 1 ) ) ) /\ ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) limCC B ) = ( ( 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 ) ) -> ( ( 0 ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) limCC B ) <-> ( 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 ) ) )
397 395 396 syl 
 |-  ( ph -> ( ( 0 ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) limCC B ) <-> ( 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 ) ) )
398 397 biimpd 
 |-  ( ph -> ( ( 0 ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) / ( ( x - B ) ^ M ) ) ( u e. CC , v e. CC |-> ( u x. v ) ) ( 1 / ( M + 1 ) ) ) ) limCC B ) -> ( 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 ) ) )
399 360 398 mpd 
 |-  ( 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 ) )
400 338 mul02d 
 |-  ( ph -> ( 0 x. ( 1 / ( M + 1 ) ) ) = 0 )
401 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 ) )
402 fveq2 
 |-  ( y = x -> ( ( ( RR Dn F ) ` ( N - M ) ) ` y ) = ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) )
403 fveq2 
 |-  ( y = x -> ( ( ( CC Dn T ) ` ( N - M ) ) ` y ) = ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) )
404 402 403 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 ) ) )
405 ovex 
 |-  ( ( ( ( RR Dn F ) ` ( N - M ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - M ) ) ` x ) ) e. _V
406 404 180 405 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 ) ) )
407 315 406 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 ) ) )
408 401 407 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 ) ) )
409 231 fveq1d 
 |-  ( ph -> ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) ` x ) = ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) ` x ) )
410 oveq1 
 |-  ( y = x -> ( y - B ) = ( x - B ) )
411 410 oveq1d 
 |-  ( y = x -> ( ( y - B ) ^ M ) = ( ( x - B ) ^ M ) )
412 411 oveq2d 
 |-  ( y = x -> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) = ( ( M + 1 ) x. ( ( x - B ) ^ M ) ) )
413 ovex 
 |-  ( ( M + 1 ) x. ( ( x - B ) ^ M ) ) e. _V
414 412 234 413 fvmpt 
 |-  ( x e. A -> ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) ` x ) = ( ( M + 1 ) x. ( ( x - B ) ^ M ) ) )
415 315 414 syl 
 |-  ( x e. ( A \ { B } ) -> ( ( y e. A |-> ( ( M + 1 ) x. ( ( y - B ) ^ M ) ) ) ` x ) = ( ( M + 1 ) x. ( ( x - B ) ^ M ) ) )
416 409 415 sylan9eq 
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) ` x ) = ( ( M + 1 ) x. ( ( x - B ) ^ M ) ) )
417 203 adantr 
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( M + 1 ) e. NN )
418 417 nncnd 
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( M + 1 ) e. CC )
419 418 328 mulcomd 
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( M + 1 ) x. ( ( x - B ) ^ M ) ) = ( ( ( x - B ) ^ M ) x. ( M + 1 ) ) )
420 416 419 eqtrd 
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( RR _D ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ) ` x ) = ( ( ( x - B ) ^ M ) x. ( M + 1 ) ) )
421 408 420 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 ) ) ) )
422 417 nnne0d 
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( M + 1 ) =/= 0 )
423 323 328 418 335 422 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 ) ) ) )
424 336 418 422 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 ) ) ) )
425 421 423 424 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 ) ) )
426 425 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 ) ) ) )
427 426 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 ) )
428 399 400 427 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 ) )
429 2 71 84 124 5 125 183 237 259 272 293 314 428 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 ) )
430 315 adantl 
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> x e. A )
431 fveq2 
 |-  ( y = x -> ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` y ) = ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` x ) )
432 fveq2 
 |-  ( y = x -> ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` y ) = ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` x ) )
433 431 432 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 ) ) )
434 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 ) ) )
435 ovex 
 |-  ( ( ( ( RR Dn F ) ` ( N - ( M + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( M + 1 ) ) ) ` x ) ) e. _V
436 433 434 435 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 ) ) )
437 430 436 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 ) ) )
438 410 oveq1d 
 |-  ( y = x -> ( ( y - B ) ^ ( M + 1 ) ) = ( ( x - B ) ^ ( M + 1 ) ) )
439 eqid 
 |-  ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) = ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) )
440 ovex 
 |-  ( ( x - B ) ^ ( M + 1 ) ) e. _V
441 438 439 440 fvmpt 
 |-  ( x e. A -> ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ` x ) = ( ( x - B ) ^ ( M + 1 ) ) )
442 430 441 syl 
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( y e. A |-> ( ( y - B ) ^ ( M + 1 ) ) ) ` x ) = ( ( x - B ) ^ ( M + 1 ) ) )
443 437 442 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 ) ) ) )
444 443 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 ) ) ) ) )
445 444 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 ) )
446 429 445 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 ) )