Metamath Proof Explorer

Theorem taylthlem1

Description: Lemma for taylth . This is the main part of Taylor's theorem, except for the induction step, which is supposed to be proven using L'Hôpital's rule. However, since our proof of L'Hôpital assumes that S = RR , we can only do this part generically, and for taylth itself we must restrict to RR . (Contributed by Mario Carneiro, 1-Jan-2017)

Ref Expression
Hypotheses taylthlem1.s 
|- ( ph -> S e. { RR , CC } )
taylthlem1.f 
|- ( ph -> F : A --> CC )
taylthlem1.a 
|- ( ph -> A C_ S )
taylthlem1.d 
|- ( ph -> dom ( ( S Dn F ) ` N ) = A )
taylthlem1.n 
|- ( ph -> N e. NN )
taylthlem1.b 
|- ( ph -> B e. A )
taylthlem1.t 
|- T = ( N ( S Tayl F ) B )
taylthlem1.r 
|- R = ( x e. ( A \ { B } ) |-> ( ( ( F ` x ) - ( T ` x ) ) / ( ( x - B ) ^ N ) ) )
taylthlem1.i 
|- ( ( ph /\ ( n e. ( 1 ..^ N ) /\ 0 e. ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - n ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - n ) ) ` y ) ) / ( ( y - B ) ^ n ) ) ) limCC B ) ) ) -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) ` x ) ) / ( ( x - B ) ^ ( n + 1 ) ) ) ) limCC B ) )
Assertion taylthlem1 
|- ( ph -> 0 e. ( R limCC B ) )

Proof

Step Hyp Ref Expression
1 taylthlem1.s 
 |-  ( ph -> S e. { RR , CC } )
2 taylthlem1.f 
 |-  ( ph -> F : A --> CC )
3 taylthlem1.a 
 |-  ( ph -> A C_ S )
4 taylthlem1.d 
 |-  ( ph -> dom ( ( S Dn F ) ` N ) = A )
5 taylthlem1.n 
 |-  ( ph -> N e. NN )
6 taylthlem1.b 
 |-  ( ph -> B e. A )
7 taylthlem1.t 
 |-  T = ( N ( S Tayl F ) B )
8 taylthlem1.r 
 |-  R = ( x e. ( A \ { B } ) |-> ( ( ( F ` x ) - ( T ` x ) ) / ( ( x - B ) ^ N ) ) )
9 taylthlem1.i 
 |-  ( ( ph /\ ( n e. ( 1 ..^ N ) /\ 0 e. ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - n ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - n ) ) ` y ) ) / ( ( y - B ) ^ n ) ) ) limCC B ) ) ) -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) ` x ) ) / ( ( x - B ) ^ ( n + 1 ) ) ) ) limCC B ) )
10 elfz1end 
 |-  ( N e. NN <-> N e. ( 1 ... N ) )
11 5 10 sylib 
 |-  ( ph -> N e. ( 1 ... N ) )
12 oveq2 
 |-  ( m = 1 -> ( N - m ) = ( N - 1 ) )
13 12 fveq2d 
 |-  ( m = 1 -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - 1 ) ) )
14 13 fveq1d 
 |-  ( m = 1 -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) )
15 12 fveq2d 
 |-  ( m = 1 -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - 1 ) ) )
16 15 fveq1d 
 |-  ( m = 1 -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) )
17 14 16 oveq12d 
 |-  ( m = 1 -> ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) = ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) )
18 oveq2 
 |-  ( m = 1 -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ 1 ) )
19 17 18 oveq12d 
 |-  ( m = 1 -> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) = ( ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) / ( ( x - B ) ^ 1 ) ) )
20 19 mpteq2dv 
 |-  ( m = 1 -> ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) = ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) / ( ( x - B ) ^ 1 ) ) ) )
21 20 oveq1d 
 |-  ( m = 1 -> ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) limCC B ) = ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) / ( ( x - B ) ^ 1 ) ) ) limCC B ) )
22 21 eleq2d 
 |-  ( m = 1 -> ( 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) limCC B ) <-> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) / ( ( x - B ) ^ 1 ) ) ) limCC B ) ) )
23 22 imbi2d 
 |-  ( m = 1 -> ( ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) limCC B ) ) <-> ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) / ( ( x - B ) ^ 1 ) ) ) limCC B ) ) ) )
24 oveq2 
 |-  ( m = n -> ( N - m ) = ( N - n ) )
25 24 fveq2d 
 |-  ( m = n -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - n ) ) )
26 25 fveq1d 
 |-  ( m = n -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - n ) ) ` x ) )
27 24 fveq2d 
 |-  ( m = n -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - n ) ) )
28 27 fveq1d 
 |-  ( m = n -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - n ) ) ` x ) )
29 26 28 oveq12d 
 |-  ( m = n -> ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) = ( ( ( ( S Dn F ) ` ( N - n ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - n ) ) ` x ) ) )
30 oveq2 
 |-  ( m = n -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ n ) )
31 29 30 oveq12d 
 |-  ( m = n -> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) = ( ( ( ( ( S Dn F ) ` ( N - n ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - n ) ) ` x ) ) / ( ( x - B ) ^ n ) ) )
32 31 mpteq2dv 
 |-  ( m = n -> ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) = ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - n ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - n ) ) ` x ) ) / ( ( x - B ) ^ n ) ) ) )
33 fveq2 
 |-  ( x = y -> ( ( ( S Dn F ) ` ( N - n ) ) ` x ) = ( ( ( S Dn F ) ` ( N - n ) ) ` y ) )
34 fveq2 
 |-  ( x = y -> ( ( ( CC Dn T ) ` ( N - n ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - n ) ) ` y ) )
35 33 34 oveq12d 
 |-  ( x = y -> ( ( ( ( S Dn F ) ` ( N - n ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - n ) ) ` x ) ) = ( ( ( ( S Dn F ) ` ( N - n ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - n ) ) ` y ) ) )
36 oveq1 
 |-  ( x = y -> ( x - B ) = ( y - B ) )
37 36 oveq1d 
 |-  ( x = y -> ( ( x - B ) ^ n ) = ( ( y - B ) ^ n ) )
38 35 37 oveq12d 
 |-  ( x = y -> ( ( ( ( ( S Dn F ) ` ( N - n ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - n ) ) ` x ) ) / ( ( x - B ) ^ n ) ) = ( ( ( ( ( S Dn F ) ` ( N - n ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - n ) ) ` y ) ) / ( ( y - B ) ^ n ) ) )
39 38 cbvmptv 
 |-  ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - n ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - n ) ) ` x ) ) / ( ( x - B ) ^ n ) ) ) = ( y e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - n ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - n ) ) ` y ) ) / ( ( y - B ) ^ n ) ) )
40 32 39 eqtrdi 
 |-  ( m = n -> ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) = ( y e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - n ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - n ) ) ` y ) ) / ( ( y - B ) ^ n ) ) ) )
41 40 oveq1d 
 |-  ( m = n -> ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) limCC B ) = ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - n ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - n ) ) ` y ) ) / ( ( y - B ) ^ n ) ) ) limCC B ) )
42 41 eleq2d 
 |-  ( m = n -> ( 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) limCC B ) <-> 0 e. ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - n ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - n ) ) ` y ) ) / ( ( y - B ) ^ n ) ) ) limCC B ) ) )
43 42 imbi2d 
 |-  ( m = n -> ( ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) limCC B ) ) <-> ( ph -> 0 e. ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - n ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - n ) ) ` y ) ) / ( ( y - B ) ^ n ) ) ) limCC B ) ) ) )
44 oveq2 
 |-  ( m = ( n + 1 ) -> ( N - m ) = ( N - ( n + 1 ) ) )
45 44 fveq2d 
 |-  ( m = ( n + 1 ) -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) )
46 45 fveq1d 
 |-  ( m = ( n + 1 ) -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) ` x ) )
47 44 fveq2d 
 |-  ( m = ( n + 1 ) -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) )
48 47 fveq1d 
 |-  ( m = ( n + 1 ) -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) ` x ) )
49 46 48 oveq12d 
 |-  ( m = ( n + 1 ) -> ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) = ( ( ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) ` x ) ) )
50 oveq2 
 |-  ( m = ( n + 1 ) -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ ( n + 1 ) ) )
51 49 50 oveq12d 
 |-  ( m = ( n + 1 ) -> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) = ( ( ( ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) ` x ) ) / ( ( x - B ) ^ ( n + 1 ) ) ) )
52 51 mpteq2dv 
 |-  ( m = ( n + 1 ) -> ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) = ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) ` x ) ) / ( ( x - B ) ^ ( n + 1 ) ) ) ) )
53 52 oveq1d 
 |-  ( m = ( n + 1 ) -> ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) limCC B ) = ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) ` x ) ) / ( ( x - B ) ^ ( n + 1 ) ) ) ) limCC B ) )
54 53 eleq2d 
 |-  ( m = ( n + 1 ) -> ( 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) limCC B ) <-> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) ` x ) ) / ( ( x - B ) ^ ( n + 1 ) ) ) ) limCC B ) ) )
55 54 imbi2d 
 |-  ( m = ( n + 1 ) -> ( ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) limCC B ) ) <-> ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) ` x ) ) / ( ( x - B ) ^ ( n + 1 ) ) ) ) limCC B ) ) ) )
56 oveq2 
 |-  ( m = N -> ( N - m ) = ( N - N ) )
57 56 fveq2d 
 |-  ( m = N -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - N ) ) )
58 57 fveq1d 
 |-  ( m = N -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - N ) ) ` x ) )
59 56 fveq2d 
 |-  ( m = N -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - N ) ) )
60 59 fveq1d 
 |-  ( m = N -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) )
61 58 60 oveq12d 
 |-  ( m = N -> ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) = ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) )
62 oveq2 
 |-  ( m = N -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ N ) )
63 61 62 oveq12d 
 |-  ( m = N -> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) = ( ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) / ( ( x - B ) ^ N ) ) )
64 63 mpteq2dv 
 |-  ( m = N -> ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) = ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) / ( ( x - B ) ^ N ) ) ) )
65 64 oveq1d 
 |-  ( m = N -> ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) limCC B ) = ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) / ( ( x - B ) ^ N ) ) ) limCC B ) )
66 65 eleq2d 
 |-  ( m = N -> ( 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) limCC B ) <-> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) / ( ( x - B ) ^ N ) ) ) limCC B ) ) )
67 66 imbi2d 
 |-  ( m = N -> ( ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) limCC B ) ) <-> ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) / ( ( x - B ) ^ N ) ) ) limCC B ) ) ) )
68 fveq2 
 |-  ( y = B -> ( ( ( S Dn F ) ` N ) ` y ) = ( ( ( S Dn F ) ` N ) ` B ) )
69 fveq2 
 |-  ( y = B -> ( ( ( CC Dn T ) ` N ) ` y ) = ( ( ( CC Dn T ) ` N ) ` B ) )
70 68 69 oveq12d 
 |-  ( y = B -> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) = ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( CC Dn T ) ` N ) ` B ) ) )
71 eqid 
 |-  ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) = ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) )
72 ovex 
 |-  ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( CC Dn T ) ` N ) ` B ) ) e. _V
73 70 71 72 fvmpt 
 |-  ( B e. A -> ( ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) ` B ) = ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( CC Dn T ) ` N ) ` B ) ) )
74 6 73 syl 
 |-  ( ph -> ( ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) ` B ) = ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( CC Dn T ) ` N ) ` B ) ) )
75 5 nnnn0d 
 |-  ( ph -> N e. NN0 )
76 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
77 75 76 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 0 ) )
78 eluzfz2b 
 |-  ( N e. ( ZZ>= ` 0 ) <-> N e. ( 0 ... N ) )
79 77 78 sylib 
 |-  ( ph -> N e. ( 0 ... N ) )
80 6 4 eleqtrrd 
 |-  ( ph -> B e. dom ( ( S Dn F ) ` N ) )
81 1 2 3 79 80 7 dvntaylp0 
 |-  ( ph -> ( ( ( CC Dn T ) ` N ) ` B ) = ( ( ( S Dn F ) ` N ) ` B ) )
82 81 oveq2d 
 |-  ( ph -> ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( CC Dn T ) ` N ) ` B ) ) = ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( S Dn F ) ` N ) ` B ) ) )
83 cnex 
 |-  CC e. _V
84 83 a1i 
 |-  ( ph -> CC e. _V )
85 elpm2r 
 |-  ( ( ( CC e. _V /\ S e. { RR , CC } ) /\ ( F : A --> CC /\ A C_ S ) ) -> F e. ( CC ^pm S ) )
86 84 1 2 3 85 syl22anc 
 |-  ( ph -> F e. ( CC ^pm S ) )
87 dvnf 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> ( ( S Dn F ) ` N ) : dom ( ( S Dn F ) ` N ) --> CC )
88 1 86 75 87 syl3anc 
 |-  ( ph -> ( ( S Dn F ) ` N ) : dom ( ( S Dn F ) ` N ) --> CC )
89 88 80 ffvelrnd 
 |-  ( ph -> ( ( ( S Dn F ) ` N ) ` B ) e. CC )
90 89 subidd 
 |-  ( ph -> ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( S Dn F ) ` N ) ` B ) ) = 0 )
91 74 82 90 3eqtrd 
 |-  ( ph -> ( ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) ` B ) = 0 )
92 funmpt 
 |-  Fun ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) )
93 ovex 
 |-  ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) e. _V
94 93 71 dmmpti 
 |-  dom ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) = A
95 6 94 eleqtrrdi 
 |-  ( ph -> B e. dom ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) )
96 funbrfvb 
 |-  ( ( Fun ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) /\ B e. dom ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) ) -> ( ( ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) ` B ) = 0 <-> B ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) 0 ) )
97 92 95 96 sylancr 
 |-  ( ph -> ( ( ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) ` B ) = 0 <-> B ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) 0 ) )
98 91 97 mpbid 
 |-  ( ph -> B ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) 0 )
99 nnm1nn0 
 |-  ( N e. NN -> ( N - 1 ) e. NN0 )
100 5 99 syl 
 |-  ( ph -> ( N - 1 ) e. NN0 )
101 dvnf 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ ( N - 1 ) e. NN0 ) -> ( ( S Dn F ) ` ( N - 1 ) ) : dom ( ( S Dn F ) ` ( N - 1 ) ) --> CC )
102 1 86 100 101 syl3anc 
 |-  ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) : dom ( ( S Dn F ) ` ( N - 1 ) ) --> CC )
103 dvnbss 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ ( N - 1 ) e. NN0 ) -> dom ( ( S Dn F ) ` ( N - 1 ) ) C_ dom F )
104 1 86 100 103 syl3anc 
 |-  ( ph -> dom ( ( S Dn F ) ` ( N - 1 ) ) C_ dom F )
105 2 104 fssdmd 
 |-  ( ph -> dom ( ( S Dn F ) ` ( N - 1 ) ) C_ A )
106 fzo0end 
 |-  ( N e. NN -> ( N - 1 ) e. ( 0 ..^ N ) )
107 elfzofz 
 |-  ( ( N - 1 ) e. ( 0 ..^ N ) -> ( N - 1 ) e. ( 0 ... N ) )
108 5 106 107 3syl 
 |-  ( ph -> ( N - 1 ) e. ( 0 ... N ) )
109 dvn2bss 
 |-  ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ ( N - 1 ) e. ( 0 ... N ) ) -> dom ( ( S Dn F ) ` N ) C_ dom ( ( S Dn F ) ` ( N - 1 ) ) )
110 1 86 108 109 syl3anc 
 |-  ( ph -> dom ( ( S Dn F ) ` N ) C_ dom ( ( S Dn F ) ` ( N - 1 ) ) )
111 4 110 eqsstrrd 
 |-  ( ph -> A C_ dom ( ( S Dn F ) ` ( N - 1 ) ) )
112 105 111 eqssd 
 |-  ( ph -> dom ( ( S Dn F ) ` ( N - 1 ) ) = A )
113 112 feq2d 
 |-  ( ph -> ( ( ( S Dn F ) ` ( N - 1 ) ) : dom ( ( S Dn F ) ` ( N - 1 ) ) --> CC <-> ( ( S Dn F ) ` ( N - 1 ) ) : A --> CC ) )
114 102 113 mpbid 
 |-  ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) : A --> CC )
115 114 ffvelrnda 
 |-  ( ( ph /\ y e. A ) -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) e. CC )
116 4 feq2d 
 |-  ( ph -> ( ( ( S Dn F ) ` N ) : dom ( ( S Dn F ) ` N ) --> CC <-> ( ( S Dn F ) ` N ) : A --> CC ) )
117 88 116 mpbid 
 |-  ( ph -> ( ( S Dn F ) ` N ) : A --> CC )
118 117 ffvelrnda 
 |-  ( ( ph /\ y e. A ) -> ( ( ( S Dn F ) ` N ) ` y ) e. CC )
119 5 nncnd 
 |-  ( ph -> N e. CC )
120 1cnd 
 |-  ( ph -> 1 e. CC )
121 119 120 npcand 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
122 121 fveq2d 
 |-  ( ph -> ( ( S Dn F ) ` ( ( N - 1 ) + 1 ) ) = ( ( S Dn F ) ` N ) )
123 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
124 1 123 syl 
 |-  ( ph -> S C_ CC )
125 dvnp1 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) /\ ( N - 1 ) e. NN0 ) -> ( ( S Dn F ) ` ( ( N - 1 ) + 1 ) ) = ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) )
126 124 86 100 125 syl3anc 
 |-  ( ph -> ( ( S Dn F ) ` ( ( N - 1 ) + 1 ) ) = ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) )
127 122 126 eqtr3d 
 |-  ( ph -> ( ( S Dn F ) ` N ) = ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) )
128 117 feqmptd 
 |-  ( ph -> ( ( S Dn F ) ` N ) = ( y e. A |-> ( ( ( S Dn F ) ` N ) ` y ) ) )
129 114 feqmptd 
 |-  ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) = ( y e. A |-> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) ) )
130 129 oveq2d 
 |-  ( ph -> ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) = ( S _D ( y e. A |-> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) ) ) )
131 127 128 130 3eqtr3rd 
 |-  ( ph -> ( S _D ( y e. A |-> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) ) ) = ( y e. A |-> ( ( ( S Dn F ) ` N ) ` y ) ) )
132 3 124 sstrd 
 |-  ( ph -> A C_ CC )
133 132 sselda 
 |-  ( ( ph /\ y e. A ) -> y e. CC )
134 1nn0 
 |-  1 e. NN0
135 134 a1i 
 |-  ( ph -> 1 e. NN0 )
136 elpm2r 
 |-  ( ( ( CC e. _V /\ S e. { RR , CC } ) /\ ( ( ( S Dn F ) ` ( N - 1 ) ) : A --> CC /\ A C_ S ) ) -> ( ( S Dn F ) ` ( N - 1 ) ) e. ( CC ^pm S ) )
137 84 1 114 3 136 syl22anc 
 |-  ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) e. ( CC ^pm S ) )
138 dvn1 
 |-  ( ( S C_ CC /\ ( ( S Dn F ) ` ( N - 1 ) ) e. ( CC ^pm S ) ) -> ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) = ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) )
139 124 137 138 syl2anc 
 |-  ( ph -> ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) = ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) )
140 126 122 eqtr3d 
 |-  ( ph -> ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) = ( ( S Dn F ) ` N ) )
141 139 140 eqtrd 
 |-  ( ph -> ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) = ( ( S Dn F ) ` N ) )
142 141 dmeqd 
 |-  ( ph -> dom ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) = dom ( ( S Dn F ) ` N ) )
143 80 142 eleqtrrd 
 |-  ( ph -> B e. dom ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) )
144 eqid 
 |-  ( 1 ( S Tayl ( ( S Dn F ) ` ( N - 1 ) ) ) B ) = ( 1 ( S Tayl ( ( S Dn F ) ` ( N - 1 ) ) ) B )
145 1 114 3 135 143 144 taylpf 
 |-  ( ph -> ( 1 ( S Tayl ( ( S Dn F ) ` ( N - 1 ) ) ) B ) : CC --> CC )
146 120 119 pncan3d 
 |-  ( ph -> ( 1 + ( N - 1 ) ) = N )
147 146 oveq1d 
 |-  ( ph -> ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) = ( N ( S Tayl F ) B ) )
148 7 147 eqtr4id 
 |-  ( ph -> T = ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) )
149 148 oveq2d 
 |-  ( ph -> ( CC Dn T ) = ( CC Dn ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) ) )
150 149 fveq1d 
 |-  ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) = ( ( CC Dn ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) ) ` ( N - 1 ) ) )
151 146 fveq2d 
 |-  ( ph -> ( ( S Dn F ) ` ( 1 + ( N - 1 ) ) ) = ( ( S Dn F ) ` N ) )
152 151 dmeqd 
 |-  ( ph -> dom ( ( S Dn F ) ` ( 1 + ( N - 1 ) ) ) = dom ( ( S Dn F ) ` N ) )
153 80 152 eleqtrrd 
 |-  ( ph -> B e. dom ( ( S Dn F ) ` ( 1 + ( N - 1 ) ) ) )
154 1 2 3 100 135 153 dvntaylp 
 |-  ( ph -> ( ( CC Dn ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) ) ` ( N - 1 ) ) = ( 1 ( S Tayl ( ( S Dn F ) ` ( N - 1 ) ) ) B ) )
155 150 154 eqtrd 
 |-  ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) = ( 1 ( S Tayl ( ( S Dn F ) ` ( N - 1 ) ) ) B ) )
156 155 feq1d 
 |-  ( ph -> ( ( ( CC Dn T ) ` ( N - 1 ) ) : CC --> CC <-> ( 1 ( S Tayl ( ( S Dn F ) ` ( N - 1 ) ) ) B ) : CC --> CC ) )
157 145 156 mpbird 
 |-  ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) : CC --> CC )
158 157 ffvelrnda 
 |-  ( ( ph /\ y e. CC ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) e. CC )
159 133 158 syldan 
 |-  ( ( ph /\ y e. A ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) e. CC )
160 0nn0 
 |-  0 e. NN0
161 160 a1i 
 |-  ( ph -> 0 e. NN0 )
162 elpm2r 
 |-  ( ( ( CC e. _V /\ S e. { RR , CC } ) /\ ( ( ( S Dn F ) ` N ) : A --> CC /\ A C_ S ) ) -> ( ( S Dn F ) ` N ) e. ( CC ^pm S ) )
163 84 1 117 3 162 syl22anc 
 |-  ( ph -> ( ( S Dn F ) ` N ) e. ( CC ^pm S ) )
164 dvn0 
 |-  ( ( S C_ CC /\ ( ( S Dn F ) ` N ) e. ( CC ^pm S ) ) -> ( ( S Dn ( ( S Dn F ) ` N ) ) ` 0 ) = ( ( S Dn F ) ` N ) )
165 124 163 164 syl2anc 
 |-  ( ph -> ( ( S Dn ( ( S Dn F ) ` N ) ) ` 0 ) = ( ( S Dn F ) ` N ) )
166 165 dmeqd 
 |-  ( ph -> dom ( ( S Dn ( ( S Dn F ) ` N ) ) ` 0 ) = dom ( ( S Dn F ) ` N ) )
167 80 166 eleqtrrd 
 |-  ( ph -> B e. dom ( ( S Dn ( ( S Dn F ) ` N ) ) ` 0 ) )
168 eqid 
 |-  ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) = ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B )
169 1 117 3 161 167 168 taylpf 
 |-  ( ph -> ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) : CC --> CC )
170 119 addid2d 
 |-  ( ph -> ( 0 + N ) = N )
171 170 oveq1d 
 |-  ( ph -> ( ( 0 + N ) ( S Tayl F ) B ) = ( N ( S Tayl F ) B ) )
172 171 7 eqtr4di 
 |-  ( ph -> ( ( 0 + N ) ( S Tayl F ) B ) = T )
173 172 oveq2d 
 |-  ( ph -> ( CC Dn ( ( 0 + N ) ( S Tayl F ) B ) ) = ( CC Dn T ) )
174 173 fveq1d 
 |-  ( ph -> ( ( CC Dn ( ( 0 + N ) ( S Tayl F ) B ) ) ` N ) = ( ( CC Dn T ) ` N ) )
175 170 fveq2d 
 |-  ( ph -> ( ( S Dn F ) ` ( 0 + N ) ) = ( ( S Dn F ) ` N ) )
176 175 dmeqd 
 |-  ( ph -> dom ( ( S Dn F ) ` ( 0 + N ) ) = dom ( ( S Dn F ) ` N ) )
177 80 176 eleqtrrd 
 |-  ( ph -> B e. dom ( ( S Dn F ) ` ( 0 + N ) ) )
178 1 2 3 75 161 177 dvntaylp 
 |-  ( ph -> ( ( CC Dn ( ( 0 + N ) ( S Tayl F ) B ) ) ` N ) = ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) )
179 174 178 eqtr3d 
 |-  ( ph -> ( ( CC Dn T ) ` N ) = ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) )
180 179 feq1d 
 |-  ( ph -> ( ( ( CC Dn T ) ` N ) : CC --> CC <-> ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) : CC --> CC ) )
181 169 180 mpbird 
 |-  ( ph -> ( ( CC Dn T ) ` N ) : CC --> CC )
182 181 ffvelrnda 
 |-  ( ( ph /\ y e. CC ) -> ( ( ( CC Dn T ) ` N ) ` y ) e. CC )
183 133 182 syldan 
 |-  ( ( ph /\ y e. A ) -> ( ( ( CC Dn T ) ` N ) ` y ) e. CC )
184 124 sselda 
 |-  ( ( ph /\ y e. S ) -> y e. CC )
185 184 158 syldan 
 |-  ( ( ph /\ y e. S ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) e. CC )
186 184 182 syldan 
 |-  ( ( ph /\ y e. S ) -> ( ( ( CC Dn T ) ` N ) ` y ) e. CC )
187 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
188 187 cnfldtopon 
 |-  ( TopOpen ` CCfld ) e. ( TopOn ` CC )
189 toponmax 
 |-  ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) -> CC e. ( TopOpen ` CCfld ) )
190 188 189 mp1i 
 |-  ( ph -> CC e. ( TopOpen ` CCfld ) )
191 df-ss 
 |-  ( S C_ CC <-> ( S i^i CC ) = S )
192 124 191 sylib 
 |-  ( ph -> ( S i^i CC ) = S )
193 ssid 
 |-  CC C_ CC
194 193 a1i 
 |-  ( ph -> CC C_ CC )
195 mapsspm 
 |-  ( CC ^m CC ) C_ ( CC ^pm CC )
196 1 2 3 75 80 7 taylpf 
 |-  ( ph -> T : CC --> CC )
197 83 83 elmap 
 |-  ( T e. ( CC ^m CC ) <-> T : CC --> CC )
198 196 197 sylibr 
 |-  ( ph -> T e. ( CC ^m CC ) )
199 195 198 sseldi 
 |-  ( ph -> T e. ( CC ^pm CC ) )
200 dvnp1 
 |-  ( ( CC C_ CC /\ T e. ( CC ^pm CC ) /\ ( N - 1 ) e. NN0 ) -> ( ( CC Dn T ) ` ( ( N - 1 ) + 1 ) ) = ( CC _D ( ( CC Dn T ) ` ( N - 1 ) ) ) )
201 194 199 100 200 syl3anc 
 |-  ( ph -> ( ( CC Dn T ) ` ( ( N - 1 ) + 1 ) ) = ( CC _D ( ( CC Dn T ) ` ( N - 1 ) ) ) )
202 121 fveq2d 
 |-  ( ph -> ( ( CC Dn T ) ` ( ( N - 1 ) + 1 ) ) = ( ( CC Dn T ) ` N ) )
203 201 202 eqtr3d 
 |-  ( ph -> ( CC _D ( ( CC Dn T ) ` ( N - 1 ) ) ) = ( ( CC Dn T ) ` N ) )
204 157 feqmptd 
 |-  ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) = ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) )
205 204 oveq2d 
 |-  ( ph -> ( CC _D ( ( CC Dn T ) ` ( N - 1 ) ) ) = ( CC _D ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) )
206 181 feqmptd 
 |-  ( ph -> ( ( CC Dn T ) ` N ) = ( y e. CC |-> ( ( ( CC Dn T ) ` N ) ` y ) ) )
207 203 205 206 3eqtr3d 
 |-  ( ph -> ( CC _D ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) = ( y e. CC |-> ( ( ( CC Dn T ) ` N ) ` y ) ) )
208 187 1 190 192 158 182 207 dvmptres3 
 |-  ( ph -> ( S _D ( y e. S |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) = ( y e. S |-> ( ( ( CC Dn T ) ` N ) ` y ) ) )
209 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t S ) = ( ( TopOpen ` CCfld ) |`t S )
210 resttopon 
 |-  ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ S C_ CC ) -> ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) )
211 188 124 210 sylancr 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) )
212 topontop 
 |-  ( ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) -> ( ( TopOpen ` CCfld ) |`t S ) e. Top )
213 211 212 syl 
 |-  ( ph -> ( ( TopOpen ` CCfld ) |`t S ) e. Top )
214 toponuni 
 |-  ( ( ( TopOpen ` CCfld ) |`t S ) e. ( TopOn ` S ) -> S = U. ( ( TopOpen ` CCfld ) |`t S ) )
215 211 214 syl 
 |-  ( ph -> S = U. ( ( TopOpen ` CCfld ) |`t S ) )
216 3 215 sseqtrd 
 |-  ( ph -> A C_ U. ( ( TopOpen ` CCfld ) |`t S ) )
217 eqid 
 |-  U. ( ( TopOpen ` CCfld ) |`t S ) = U. ( ( TopOpen ` CCfld ) |`t S )
218 217 ntrss2 
 |-  ( ( ( ( TopOpen ` CCfld ) |`t S ) e. Top /\ A C_ U. ( ( TopOpen ` CCfld ) |`t S ) ) -> ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` A ) C_ A )
219 213 216 218 syl2anc 
 |-  ( ph -> ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` A ) C_ A )
220 140 dmeqd 
 |-  ( ph -> dom ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) = dom ( ( S Dn F ) ` N ) )
221 220 4 eqtrd 
 |-  ( ph -> dom ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) = A )
222 124 114 3 209 187 dvbssntr 
 |-  ( ph -> dom ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) C_ ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` A ) )
223 221 222 eqsstrrd 
 |-  ( ph -> A C_ ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` A ) )
224 219 223 eqssd 
 |-  ( ph -> ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` A ) = A )
225 1 185 186 208 3 209 187 224 dvmptres2 
 |-  ( ph -> ( S _D ( y e. A |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) = ( y e. A |-> ( ( ( CC Dn T ) ` N ) ` y ) ) )
226 1 115 118 131 159 183 225 dvmptsub 
 |-  ( ph -> ( S _D ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ) = ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) )
227 226 breqd 
 |-  ( ph -> ( B ( S _D ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ) 0 <-> B ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) 0 ) )
228 98 227 mpbird 
 |-  ( ph -> B ( S _D ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ) 0 )
229 eqid 
 |-  ( x e. ( A \ { B } ) |-> ( ( ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` x ) - ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` B ) ) / ( x - B ) ) ) = ( x e. ( A \ { B } ) |-> ( ( ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` x ) - ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` B ) ) / ( x - B ) ) )
230 115 159 subcld 
 |-  ( ( ph /\ y e. A ) -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) e. CC )
231 230 fmpttd 
 |-  ( ph -> ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) : A --> CC )
232 209 187 229 124 231 3 eldv 
 |-  ( ph -> ( B ( S _D ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ) 0 <-> ( B e. ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` A ) /\ 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` x ) - ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` B ) ) / ( x - B ) ) ) limCC B ) ) ) )
233 228 232 mpbid 
 |-  ( ph -> ( B e. ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` A ) /\ 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` x ) - ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` B ) ) / ( x - B ) ) ) limCC B ) ) )
234 233 simprd 
 |-  ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` x ) - ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` B ) ) / ( x - B ) ) ) limCC B ) )
235 eldifi 
 |-  ( x e. ( A \ { B } ) -> x e. A )
236 fveq2 
 |-  ( y = x -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) )
237 fveq2 
 |-  ( y = x -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) = ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) )
238 236 237 oveq12d 
 |-  ( y = x -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) = ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) )
239 eqid 
 |-  ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) = ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) )
240 ovex 
 |-  ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) e. _V
241 238 239 240 fvmpt 
 |-  ( x e. A -> ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` x ) = ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) )
242 fveq2 
 |-  ( y = B -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) )
243 fveq2 
 |-  ( y = B -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) = ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) )
244 242 243 oveq12d 
 |-  ( y = B -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) = ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) ) )
245 ovex 
 |-  ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) ) e. _V
246 244 239 245 fvmpt 
 |-  ( B e. A -> ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` B ) = ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) ) )
247 6 246 syl 
 |-  ( ph -> ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` B ) = ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) ) )
248 1 2 3 108 80 7 dvntaylp0 
 |-  ( ph -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) )
249 248 oveq2d 
 |-  ( ph -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) ) = ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) - ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) ) )
250 114 6 ffvelrnd 
 |-  ( ph -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) e. CC )
251 250 subidd 
 |-  ( ph -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) - ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) ) = 0 )
252 247 249 251 3eqtrd 
 |-  ( ph -> ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` B ) = 0 )
253 241 252 oveqan12rd 
 |-  ( ( ph /\ x e. A ) -> ( ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` x ) - ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` B ) ) = ( ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) - 0 ) )
254 114 ffvelrnda 
 |-  ( ( ph /\ x e. A ) -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) e. CC )
255 132 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. CC )
256 157 ffvelrnda 
 |-  ( ( ph /\ x e. CC ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) e. CC )
257 255 256 syldan 
 |-  ( ( ph /\ x e. A ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) e. CC )
258 254 257 subcld 
 |-  ( ( ph /\ x e. A ) -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) e. CC )
259 258 subid1d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) - 0 ) = ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) )
260 253 259 eqtr2d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) = ( ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` x ) - ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` B ) ) )
261 235 260 sylan2 
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) = ( ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` x ) - ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` B ) ) )
262 132 ssdifssd 
 |-  ( ph -> ( A \ { B } ) C_ CC )
263 262 sselda 
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> x e. CC )
264 132 6 sseldd 
 |-  ( ph -> B e. CC )
265 264 adantr 
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> B e. CC )
266 263 265 subcld 
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( x - B ) e. CC )
267 266 exp1d 
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( x - B ) ^ 1 ) = ( x - B ) )
268 261 267 oveq12d 
 |-  ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) / ( ( x - B ) ^ 1 ) ) = ( ( ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` x ) - ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` B ) ) / ( x - B ) ) )
269 268 mpteq2dva 
 |-  ( ph -> ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) / ( ( x - B ) ^ 1 ) ) ) = ( x e. ( A \ { B } ) |-> ( ( ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` x ) - ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` B ) ) / ( x - B ) ) ) )
270 269 oveq1d 
 |-  ( ph -> ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) / ( ( x - B ) ^ 1 ) ) ) limCC B ) = ( ( x e. ( A \ { B } ) |-> ( ( ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` x ) - ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` B ) ) / ( x - B ) ) ) limCC B ) )
271 234 270 eleqtrrd 
 |-  ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) / ( ( x - B ) ^ 1 ) ) ) limCC B ) )
272 271 a1i 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) / ( ( x - B ) ^ 1 ) ) ) limCC B ) ) )
273 9 expr 
 |-  ( ( ph /\ n e. ( 1 ..^ N ) ) -> ( 0 e. ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - n ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - n ) ) ` y ) ) / ( ( y - B ) ^ n ) ) ) limCC B ) -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) ` x ) ) / ( ( x - B ) ^ ( n + 1 ) ) ) ) limCC B ) ) )
274 273 expcom 
 |-  ( n e. ( 1 ..^ N ) -> ( ph -> ( 0 e. ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - n ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - n ) ) ` y ) ) / ( ( y - B ) ^ n ) ) ) limCC B ) -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) ` x ) ) / ( ( x - B ) ^ ( n + 1 ) ) ) ) limCC B ) ) ) )
275 274 a2d 
 |-  ( n e. ( 1 ..^ N ) -> ( ( ph -> 0 e. ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - n ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - n ) ) ` y ) ) / ( ( y - B ) ^ n ) ) ) limCC B ) ) -> ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) ` x ) ) / ( ( x - B ) ^ ( n + 1 ) ) ) ) limCC B ) ) ) )
276 23 43 55 67 272 275 fzind2 
 |-  ( N e. ( 1 ... N ) -> ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) / ( ( x - B ) ^ N ) ) ) limCC B ) ) )
277 11 276 mpcom 
 |-  ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) / ( ( x - B ) ^ N ) ) ) limCC B ) )
278 119 subidd 
 |-  ( ph -> ( N - N ) = 0 )
279 278 fveq2d 
 |-  ( ph -> ( ( S Dn F ) ` ( N - N ) ) = ( ( S Dn F ) ` 0 ) )
280 dvn0 
 |-  ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = F )
281 124 86 280 syl2anc 
 |-  ( ph -> ( ( S Dn F ) ` 0 ) = F )
282 279 281 eqtrd 
 |-  ( ph -> ( ( S Dn F ) ` ( N - N ) ) = F )
283 282 fveq1d 
 |-  ( ph -> ( ( ( S Dn F ) ` ( N - N ) ) ` x ) = ( F ` x ) )
284 278 fveq2d 
 |-  ( ph -> ( ( CC Dn T ) ` ( N - N ) ) = ( ( CC Dn T ) ` 0 ) )
285 dvn0 
 |-  ( ( CC C_ CC /\ T e. ( CC ^pm CC ) ) -> ( ( CC Dn T ) ` 0 ) = T )
286 193 199 285 sylancr 
 |-  ( ph -> ( ( CC Dn T ) ` 0 ) = T )
287 284 286 eqtrd 
 |-  ( ph -> ( ( CC Dn T ) ` ( N - N ) ) = T )
288 287 fveq1d 
 |-  ( ph -> ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) = ( T ` x ) )
289 283 288 oveq12d 
 |-  ( ph -> ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) = ( ( F ` x ) - ( T ` x ) ) )
290 289 oveq1d 
 |-  ( ph -> ( ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) / ( ( x - B ) ^ N ) ) = ( ( ( F ` x ) - ( T ` x ) ) / ( ( x - B ) ^ N ) ) )
291 290 mpteq2dv 
 |-  ( ph -> ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) / ( ( x - B ) ^ N ) ) ) = ( x e. ( A \ { B } ) |-> ( ( ( F ` x ) - ( T ` x ) ) / ( ( x - B ) ^ N ) ) ) )
292 291 8 eqtr4di 
 |-  ( ph -> ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) / ( ( x - B ) ^ N ) ) ) = R )
293 292 oveq1d 
 |-  ( ph -> ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) / ( ( x - B ) ^ N ) ) ) limCC B ) = ( R limCC B ) )
294 277 293 eleqtrd 
 |-  ( ph -> 0 e. ( R limCC B ) )