Theorem taylthlem1 23058

Description: Lemma for taylth 23060. 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 23060 itself we must restrict to RR. (Contributed by Mario Carneiro, 1-Jan-2017.)

Hypotheses

Ref	Expression
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 ) ) ) lim CC 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 ) ) ) ) lim CC B ) )

Assertion

Ref	Expression
taylthlem1	|- ( ph -> 0 e. ( R lim CC B ) )

Distinct variable groups:   x, n, y, A   B, n, x, y   n, F, x, y   ph, n, x, y   n, N, x, y   S, n, x, y   T, n, x, y

Allowed substitution hints:   R( x, y, n)

Proof of Theorem taylthlem1

Dummy variable m is distinct from all other variables.

Step	Hyp	Ref	Expression
1		taylthlem1.n	. . . 4 |- ( ph -> N e. NN )
2		elfz1end 11767	. . . 4 |- ( N e. NN <-> N e. ( 1 ... N ) )
3	1, 2	sylib 196	. . 3 |- ( ph -> N e. ( 1 ... N ) )
4		oveq2 6285	. . . . . . . . . . . 12 |- ( m = 1 -> ( N - m ) = ( N - 1 ) )
5	4	fveq2d 5852	. . . . . . . . . . 11 |- ( m = 1 -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - 1 ) ) )
6	5	fveq1d 5850	. . . . . . . . . 10 |- ( m = 1 -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) )
7	4	fveq2d 5852	. . . . . . . . . . 11 |- ( m = 1 -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - 1 ) ) )
8	7	fveq1d 5850	. . . . . . . . . 10 |- ( m = 1 -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) )
9	6, 8	oveq12d 6295	. . . . . . . . 9 |- ( 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 ) ) )
10		oveq2 6285	. . . . . . . . 9 |- ( m = 1 -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ 1 ) )
11	9, 10	oveq12d 6295	. . . . . . . 8 |- ( 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 ) ) )
12	11	mpteq2dv 4481	. . . . . . 7 |- ( 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 ) ) ) )
13	12	oveq1d 6292	. . . . . 6 |- ( m = 1 -> ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) lim CC B ) = ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) / ( ( x - B ) ^ 1 ) ) ) lim CC B ) )
14	13	eleq2d 2472	. . . . 5 |- ( m = 1 -> ( 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) lim CC B ) <-> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) / ( ( x - B ) ^ 1 ) ) ) lim CC B ) ) )
15	14	imbi2d 314	. . . 4 |- ( m = 1 -> ( ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) lim CC B ) ) <-> ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) / ( ( x - B ) ^ 1 ) ) ) lim CC B ) ) ) )
16		oveq2 6285	. . . . . . . . . . . . 13 |- ( m = n -> ( N - m ) = ( N - n ) )
17	16	fveq2d 5852	. . . . . . . . . . . 12 |- ( m = n -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - n ) ) )
18	17	fveq1d 5850	. . . . . . . . . . 11 |- ( m = n -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - n ) ) ` x ) )
19	16	fveq2d 5852	. . . . . . . . . . . 12 |- ( m = n -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - n ) ) )
20	19	fveq1d 5850	. . . . . . . . . . 11 |- ( m = n -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - n ) ) ` x ) )
21	18, 20	oveq12d 6295	. . . . . . . . . 10 |- ( 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 ) ) )
22		oveq2 6285	. . . . . . . . . 10 |- ( m = n -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ n ) )
23	21, 22	oveq12d 6295	. . . . . . . . 9 |- ( 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 ) ) )
24	23	mpteq2dv 4481	. . . . . . . 8 |- ( 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 ) ) ) )
25		fveq2 5848	. . . . . . . . . . 11 |- ( x = y -> ( ( ( S Dn F ) ` ( N - n ) ) ` x ) = ( ( ( S Dn F ) ` ( N - n ) ) ` y ) )
26		fveq2 5848	. . . . . . . . . . 11 |- ( x = y -> ( ( ( CC Dn T ) ` ( N - n ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - n ) ) ` y ) )
27	25, 26	oveq12d 6295	. . . . . . . . . 10 |- ( 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 ) ) )
28		oveq1 6284	. . . . . . . . . . 11 |- ( x = y -> ( x - B ) = ( y - B ) )
29	28	oveq1d 6292	. . . . . . . . . 10 |- ( x = y -> ( ( x - B ) ^ n ) = ( ( y - B ) ^ n ) )
30	27, 29	oveq12d 6295	. . . . . . . . 9 |- ( 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 ) ) )
31	30	cbvmptv 4486	. . . . . . . 8 |- ( 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 ) ) )
32	24, 31	syl6eq 2459	. . . . . . 7 |- ( 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 ) ) ) )
33	32	oveq1d 6292	. . . . . 6 |- ( m = n -> ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) lim CC B ) = ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - n ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - n ) ) ` y ) ) / ( ( y - B ) ^ n ) ) ) lim CC B ) )
34	33	eleq2d 2472	. . . . 5 |- ( m = n -> ( 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) lim CC B ) <-> 0 e. ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - n ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - n ) ) ` y ) ) / ( ( y - B ) ^ n ) ) ) lim CC B ) ) )
35	34	imbi2d 314	. . . 4 |- ( m = n -> ( ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) lim CC B ) ) <-> ( ph -> 0 e. ( ( y e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - n ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - n ) ) ` y ) ) / ( ( y - B ) ^ n ) ) ) lim CC B ) ) ) )
36		oveq2 6285	. . . . . . . . . . . 12 |- ( m = ( n + 1 ) -> ( N - m ) = ( N - ( n + 1 ) ) )
37	36	fveq2d 5852	. . . . . . . . . . 11 |- ( m = ( n + 1 ) -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) )
38	37	fveq1d 5850	. . . . . . . . . 10 |- ( m = ( n + 1 ) -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) ` x ) )
39	36	fveq2d 5852	. . . . . . . . . . 11 |- ( m = ( n + 1 ) -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) )
40	39	fveq1d 5850	. . . . . . . . . 10 |- ( m = ( n + 1 ) -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) ` x ) )
41	38, 40	oveq12d 6295	. . . . . . . . 9 |- ( 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 ) ) )
42		oveq2 6285	. . . . . . . . 9 |- ( m = ( n + 1 ) -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ ( n + 1 ) ) )
43	41, 42	oveq12d 6295	. . . . . . . 8 |- ( 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 ) ) ) )
44	43	mpteq2dv 4481	. . . . . . 7 |- ( 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 ) ) ) ) )
45	44	oveq1d 6292	. . . . . 6 |- ( m = ( n + 1 ) -> ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) lim CC B ) = ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) ` x ) ) / ( ( x - B ) ^ ( n + 1 ) ) ) ) lim CC B ) )
46	45	eleq2d 2472	. . . . 5 |- ( m = ( n + 1 ) -> ( 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) lim CC 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 ) ) ) ) lim CC B ) ) )
47	46	imbi2d 314	. . . 4 |- ( 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 ) ) ) lim CC 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 ) ) ) ) lim CC B ) ) ) )
48		oveq2 6285	. . . . . . . . . . . 12 |- ( m = N -> ( N - m ) = ( N - N ) )
49	48	fveq2d 5852	. . . . . . . . . . 11 |- ( m = N -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - N ) ) )
50	49	fveq1d 5850	. . . . . . . . . 10 |- ( m = N -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - N ) ) ` x ) )
51	48	fveq2d 5852	. . . . . . . . . . 11 |- ( m = N -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - N ) ) )
52	51	fveq1d 5850	. . . . . . . . . 10 |- ( m = N -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) )
53	50, 52	oveq12d 6295	. . . . . . . . 9 |- ( 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 ) ) )
54		oveq2 6285	. . . . . . . . 9 |- ( m = N -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ N ) )
55	53, 54	oveq12d 6295	. . . . . . . 8 |- ( 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 ) ) )
56	55	mpteq2dv 4481	. . . . . . 7 |- ( 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 ) ) ) )
57	56	oveq1d 6292	. . . . . 6 |- ( m = N -> ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) lim CC B ) = ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) / ( ( x - B ) ^ N ) ) ) lim CC B ) )
58	57	eleq2d 2472	. . . . 5 |- ( m = N -> ( 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) lim CC B ) <-> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) / ( ( x - B ) ^ N ) ) ) lim CC B ) ) )
59	58	imbi2d 314	. . . 4 |- ( m = N -> ( ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - m ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) ) / ( ( x - B ) ^ m ) ) ) lim CC B ) ) <-> ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) / ( ( x - B ) ^ N ) ) ) lim CC B ) ) ) )
60		taylthlem1.b	. . . . . . . . . . . 12 |- ( ph -> B e. A )
61		fveq2 5848	. . . . . . . . . . . . . 14 |- ( y = B -> ( ( ( S Dn F ) ` N ) ` y ) = ( ( ( S Dn F ) ` N ) ` B ) )
62		fveq2 5848	. . . . . . . . . . . . . 14 |- ( y = B -> ( ( ( CC Dn T ) ` N ) ` y ) = ( ( ( CC Dn T ) ` N ) ` B ) )
63	61, 62	oveq12d 6295	. . . . . . . . . . . . 13 |- ( y = B -> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) = ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( CC Dn T ) ` N ) ` B ) ) )
64		eqid 2402	. . . . . . . . . . . . 13 |- ( 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 ) ) )
65		ovex 6305	. . . . . . . . . . . . 13 |- ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( CC Dn T ) ` N ) ` B ) ) e. _V
66	63, 64, 65	fvmpt 5931	. . . . . . . . . . . 12 |- ( 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 ) ) )
67	60, 66	syl 17	. . . . . . . . . . 11 |- ( 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 ) ) )
68		taylthlem1.s	. . . . . . . . . . . . 13 |- ( ph -> S e. { RR , CC } )
69		taylthlem1.f	. . . . . . . . . . . . 13 |- ( ph -> F : A --> CC )
70		taylthlem1.a	. . . . . . . . . . . . 13 |- ( ph -> A C_ S )
71	1	nnnn0d 10892	. . . . . . . . . . . . . . 15 |- ( ph -> N e. NN0 )
72		nn0uz 11160	. . . . . . . . . . . . . . 15 |- NN0 = ( ZZ>= ` 0 )
73	71, 72	syl6eleq 2500	. . . . . . . . . . . . . 14 |- ( ph -> N e. ( ZZ>= ` 0 ) )
74		eluzfz2b 11747	. . . . . . . . . . . . . 14 |- ( N e. ( ZZ>= ` 0 ) <-> N e. ( 0 ... N ) )
75	73, 74	sylib 196	. . . . . . . . . . . . 13 |- ( ph -> N e. ( 0 ... N ) )
76		taylthlem1.d	. . . . . . . . . . . . . 14 |- ( ph -> dom ( ( S Dn F ) ` N ) = A )
77	60, 76	eleqtrrd 2493	. . . . . . . . . . . . 13 |- ( ph -> B e. dom ( ( S Dn F ) ` N ) )
78		taylthlem1.t	. . . . . . . . . . . . 13 |- T = ( N ( S Tayl F ) B )
79	68, 69, 70, 75, 77, 78	dvntaylp0 23057	. . . . . . . . . . . 12 |- ( ph -> ( ( ( CC Dn T ) ` N ) ` B ) = ( ( ( S Dn F ) ` N ) ` B ) )
80	79	oveq2d 6293	. . . . . . . . . . 11 |- ( ph -> ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( CC Dn T ) ` N ) ` B ) ) = ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( S Dn F ) ` N ) ` B ) ) )
81		cnex 9602	. . . . . . . . . . . . . . . 16 |- CC e. _V
82	81	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> CC e. _V )
83		elpm2r 7473	. . . . . . . . . . . . . . 15 |- ( ( ( CC e. _V /\ S e. { RR , CC } ) /\ ( F : A --> CC /\ A C_ S ) ) -> F e. ( CC ^pm S ) )
84	82, 68, 69, 70, 83	syl22anc 1231	. . . . . . . . . . . . . 14 |- ( ph -> F e. ( CC ^pm S ) )
85		dvnf 22620	. . . . . . . . . . . . . 14 |- ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ N e. NN0 ) -> ( ( S Dn F ) ` N ) : dom ( ( S Dn F ) ` N ) --> CC )
86	68, 84, 71, 85	syl3anc 1230	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` N ) : dom ( ( S Dn F ) ` N ) --> CC )
87	86, 77	ffvelrnd 6009	. . . . . . . . . . . 12 |- ( ph -> ( ( ( S Dn F ) ` N ) ` B ) e. CC )
88	87	subidd 9954	. . . . . . . . . . 11 |- ( ph -> ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( S Dn F ) ` N ) ` B ) ) = 0 )
89	67, 80, 88	3eqtrd 2447	. . . . . . . . . 10 |- ( ph -> ( ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) ` B ) = 0 )
90		funmpt 5604	. . . . . . . . . . 11 |- Fun ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) )
91		ovex 6305	. . . . . . . . . . . . 13 |- ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) e. _V
92	91, 64	dmmpti 5692	. . . . . . . . . . . 12 |- dom ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) = A
93	60, 92	syl6eleqr 2501	. . . . . . . . . . 11 |- ( ph -> B e. dom ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) )
94		funbrfvb 5890	. . . . . . . . . . 11 |- ( ( 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 ) )
95	90, 93, 94	sylancr 661	. . . . . . . . . 10 |- ( 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 ) )
96	89, 95	mpbid 210	. . . . . . . . 9 |- ( ph -> B ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) 0 )
97		nnm1nn0 10877	. . . . . . . . . . . . . . 15 |- ( N e. NN -> ( N - 1 ) e. NN0 )
98	1, 97	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> ( N - 1 ) e. NN0 )
99		dvnf 22620	. . . . . . . . . . . . . 14 |- ( ( 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 )
100	68, 84, 98, 99	syl3anc 1230	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) : dom ( ( S Dn F ) ` ( N - 1 ) ) --> CC )
101		dvnbss 22621	. . . . . . . . . . . . . . . . 17 |- ( ( S e. { RR , CC } /\ F e. ( CC ^pm S ) /\ ( N - 1 ) e. NN0 ) -> dom ( ( S Dn F ) ` ( N - 1 ) ) C_ dom F )
102	68, 84, 98, 101	syl3anc 1230	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( ( S Dn F ) ` ( N - 1 ) ) C_ dom F )
103		fdm 5717	. . . . . . . . . . . . . . . . 17 |- ( F : A --> CC -> dom F = A )
104	69, 103	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> dom F = A )
105	102, 104	sseqtrd 3477	. . . . . . . . . . . . . . 15 |- ( ph -> dom ( ( S Dn F ) ` ( N - 1 ) ) C_ A )
106		fzo0end 11939	. . . . . . . . . . . . . . . . . 18 |- ( N e. NN -> ( N - 1 ) e. ( 0..^ N ) )
107		elfzofz 11872	. . . . . . . . . . . . . . . . . 18 |- ( ( N - 1 ) e. ( 0..^ N ) -> ( N - 1 ) e. ( 0 ... N ) )
108	1, 106, 107	3syl 20	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( N - 1 ) e. ( 0 ... N ) )
109		dvn2bss 22623	. . . . . . . . . . . . . . . . 17 |- ( ( 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	68, 84, 108, 109	syl3anc 1230	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( ( S Dn F ) ` N ) C_ dom ( ( S Dn F ) ` ( N - 1 ) ) )
111	76, 110	eqsstr3d 3476	. . . . . . . . . . . . . . 15 |- ( ph -> A C_ dom ( ( S Dn F ) ` ( N - 1 ) ) )
112	105, 111	eqssd 3458	. . . . . . . . . . . . . 14 |- ( ph -> dom ( ( S Dn F ) ` ( N - 1 ) ) = A )
113	112	feq2d 5700	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( S Dn F ) ` ( N - 1 ) ) : dom ( ( S Dn F ) ` ( N - 1 ) ) --> CC <-> ( ( S Dn F ) ` ( N - 1 ) ) : A --> CC ) )
114	100, 113	mpbid 210	. . . . . . . . . . . 12 |- ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) : A --> CC )
115	114	ffvelrnda 6008	. . . . . . . . . . 11 |- ( ( ph /\ y e. A ) -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) e. CC )
116	76	feq2d 5700	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( S Dn F ) ` N ) : dom ( ( S Dn F ) ` N ) --> CC <-> ( ( S Dn F ) ` N ) : A --> CC ) )
117	86, 116	mpbid 210	. . . . . . . . . . . 12 |- ( ph -> ( ( S Dn F ) ` N ) : A --> CC )
118	117	ffvelrnda 6008	. . . . . . . . . . 11 |- ( ( ph /\ y e. A ) -> ( ( ( S Dn F ) ` N ) ` y ) e. CC )
119	1	nncnd 10591	. . . . . . . . . . . . . . 15 |- ( ph -> N e. CC )
120		1cnd 9641	. . . . . . . . . . . . . . 15 |- ( ph -> 1 e. CC )
121	119, 120	npcand 9970	. . . . . . . . . . . . . 14 |- ( ph -> ( ( N - 1 ) + 1 ) = N )
122	121	fveq2d 5852	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` ( ( N - 1 ) + 1 ) ) = ( ( S Dn F ) ` N ) )
123		recnprss 22598	. . . . . . . . . . . . . . 15 |- ( S e. { RR , CC } -> S C_ CC )
124	68, 123	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> S C_ CC )
125		dvnp1 22618	. . . . . . . . . . . . . 14 |- ( ( 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, 84, 98, 125	syl3anc 1230	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` ( ( N - 1 ) + 1 ) ) = ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) )
127	122, 126	eqtr3d 2445	. . . . . . . . . . . 12 |- ( ph -> ( ( S Dn F ) ` N ) = ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) )
128	117	feqmptd 5901	. . . . . . . . . . . 12 |- ( ph -> ( ( S Dn F ) ` N ) = ( y e. A |-> ( ( ( S Dn F ) ` N ) ` y ) ) )
129	114	feqmptd 5901	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) = ( y e. A |-> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) ) )
130	129	oveq2d 6293	. . . . . . . . . . . 12 |- ( ph -> ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) = ( S _D ( y e. A |-> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) ) ) )
131	127, 128, 130	3eqtr3rd 2452	. . . . . . . . . . 11 |- ( ph -> ( S _D ( y e. A |-> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) ) ) = ( y e. A |-> ( ( ( S Dn F ) ` N ) ` y ) ) )
132	70, 124	sstrd 3451	. . . . . . . . . . . . 13 |- ( ph -> A C_ CC )
133	132	sselda 3441	. . . . . . . . . . . 12 |- ( ( ph /\ y e. A ) -> y e. CC )
134		1nn0 10851	. . . . . . . . . . . . . . . 16 |- 1 e. NN0
135	134	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 1 e. NN0 )
136		elpm2r 7473	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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	82, 68, 114, 70, 136	syl22anc 1231	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) e. ( CC ^pm S ) )
138		dvn1 22619	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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 659	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) = ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) )
140	126, 122	eqtr3d 2445	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) = ( ( S Dn F ) ` N ) )
141	139, 140	eqtrd 2443	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) = ( ( S Dn F ) ` N ) )
142	141	dmeqd 5025	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) = dom ( ( S Dn F ) ` N ) )
143	77, 142	eleqtrrd 2493	. . . . . . . . . . . . . . 15 |- ( ph -> B e. dom ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) )
144		eqid 2402	. . . . . . . . . . . . . . 15 |- ( 1 ( S Tayl ( ( S Dn F ) ` ( N - 1 ) ) ) B ) = ( 1 ( S Tayl ( ( S Dn F ) ` ( N - 1 ) ) ) B )
145	68, 114, 70, 135, 143, 144	taylpf 23051	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 ( S Tayl ( ( S Dn F ) ` ( N - 1 ) ) ) B ) : CC --> CC )
146	120, 119	pncan3d 9969	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 + ( N - 1 ) ) = N )
147	146	oveq1d 6292	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) = ( N ( S Tayl F ) B ) )
148	147, 78	syl6reqr 2462	. . . . . . . . . . . . . . . . . 18 |- ( ph -> T = ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) )
149	148	oveq2d 6293	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( CC Dn T ) = ( CC Dn ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) ) )
150	149	fveq1d 5850	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) = ( ( CC Dn ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) ) ` ( N - 1 ) ) )
151	146	fveq2d 5852	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( S Dn F ) ` ( 1 + ( N - 1 ) ) ) = ( ( S Dn F ) ` N ) )
152	151	dmeqd 5025	. . . . . . . . . . . . . . . . . 18 |- ( ph -> dom ( ( S Dn F ) ` ( 1 + ( N - 1 ) ) ) = dom ( ( S Dn F ) ` N ) )
153	77, 152	eleqtrrd 2493	. . . . . . . . . . . . . . . . 17 |- ( ph -> B e. dom ( ( S Dn F ) ` ( 1 + ( N - 1 ) ) ) )
154	68, 69, 70, 98, 135, 153	dvntaylp 23056	. . . . . . . . . . . . . . . 16 |- ( 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 2443	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) = ( 1 ( S Tayl ( ( S Dn F ) ` ( N - 1 ) ) ) B ) )
156	155	feq1d 5699	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( CC Dn T ) ` ( N - 1 ) ) : CC --> CC <-> ( 1 ( S Tayl ( ( S Dn F ) ` ( N - 1 ) ) ) B ) : CC --> CC ) )
157	145, 156	mpbird 232	. . . . . . . . . . . . 13 |- ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) : CC --> CC )
158	157	ffvelrnda 6008	. . . . . . . . . . . 12 |- ( ( ph /\ y e. CC ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) e. CC )
159	133, 158	syldan 468	. . . . . . . . . . 11 |- ( ( ph /\ y e. A ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) e. CC )
160		0nn0 10850	. . . . . . . . . . . . . . . 16 |- 0 e. NN0
161	160	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 0 e. NN0 )
162		elpm2r 7473	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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	82, 68, 117, 70, 162	syl22anc 1231	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( S Dn F ) ` N ) e. ( CC ^pm S ) )
164		dvn0 22617	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 659	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( S Dn ( ( S Dn F ) ` N ) ) ` 0 ) = ( ( S Dn F ) ` N ) )
166	165	dmeqd 5025	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( ( S Dn ( ( S Dn F ) ` N ) ) ` 0 ) = dom ( ( S Dn F ) ` N ) )
167	77, 166	eleqtrrd 2493	. . . . . . . . . . . . . . 15 |- ( ph -> B e. dom ( ( S Dn ( ( S Dn F ) ` N ) ) ` 0 ) )
168		eqid 2402	. . . . . . . . . . . . . . 15 |- ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) = ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B )
169	68, 117, 70, 161, 167, 168	taylpf 23051	. . . . . . . . . . . . . 14 |- ( ph -> ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) : CC --> CC )
170	119	addid2d 9814	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 0 + N ) = N )
171	170	oveq1d 6292	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( 0 + N ) ( S Tayl F ) B ) = ( N ( S Tayl F ) B ) )
172	171, 78	syl6eqr 2461	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( 0 + N ) ( S Tayl F ) B ) = T )
173	172	oveq2d 6293	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( CC Dn ( ( 0 + N ) ( S Tayl F ) B ) ) = ( CC Dn T ) )
174	173	fveq1d 5850	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( CC Dn ( ( 0 + N ) ( S Tayl F ) B ) ) ` N ) = ( ( CC Dn T ) ` N ) )
175	170	fveq2d 5852	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( S Dn F ) ` ( 0 + N ) ) = ( ( S Dn F ) ` N ) )
176	175	dmeqd 5025	. . . . . . . . . . . . . . . . . 18 |- ( ph -> dom ( ( S Dn F ) ` ( 0 + N ) ) = dom ( ( S Dn F ) ` N ) )
177	77, 176	eleqtrrd 2493	. . . . . . . . . . . . . . . . 17 |- ( ph -> B e. dom ( ( S Dn F ) ` ( 0 + N ) ) )
178	68, 69, 70, 71, 161, 177	dvntaylp 23056	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( CC Dn ( ( 0 + N ) ( S Tayl F ) B ) ) ` N ) = ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) )
179	174, 178	eqtr3d 2445	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` N ) = ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) )
180	179	feq1d 5699	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( CC Dn T ) ` N ) : CC --> CC <-> ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) : CC --> CC ) )
181	169, 180	mpbird 232	. . . . . . . . . . . . 13 |- ( ph -> ( ( CC Dn T ) ` N ) : CC --> CC )
182	181	ffvelrnda 6008	. . . . . . . . . . . 12 |- ( ( ph /\ y e. CC ) -> ( ( ( CC Dn T ) ` N ) ` y ) e. CC )
183	133, 182	syldan 468	. . . . . . . . . . 11 |- ( ( ph /\ y e. A ) -> ( ( ( CC Dn T ) ` N ) ` y ) e. CC )
184	124	sselda 3441	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. S ) -> y e. CC )
185	184, 158	syldan 468	. . . . . . . . . . . 12 |- ( ( ph /\ y e. S ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) e. CC )
186	184, 182	syldan 468	. . . . . . . . . . . 12 |- ( ( ph /\ y e. S ) -> ( ( ( CC Dn T ) ` N ) ` y ) e. CC )
187		eqid 2402	. . . . . . . . . . . . 13 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
188	187	cnfldtopon 21580	. . . . . . . . . . . . . 14 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
189		toponmax 19719	. . . . . . . . . . . . . 14 |- ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) -> CC e. ( TopOpen ` ℂfld ) )
190	188, 189	mp1i 13	. . . . . . . . . . . . 13 |- ( ph -> CC e. ( TopOpen ` ℂfld ) )
191		df-ss 3427	. . . . . . . . . . . . . 14 |- ( S C_ CC <-> ( S i^i CC ) = S )
192	124, 191	sylib 196	. . . . . . . . . . . . 13 |- ( ph -> ( S i^i CC ) = S )
193		ssid 3460	. . . . . . . . . . . . . . . . 17 |- CC C_ CC
194	193	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> CC C_ CC )
195		mapsspm 7489	. . . . . . . . . . . . . . . . 17 |- ( CC ^m CC ) C_ ( CC ^pm CC )
196	68, 69, 70, 71, 77, 78	taylpf 23051	. . . . . . . . . . . . . . . . . 18 |- ( ph -> T : CC --> CC )
197	81, 81	elmap 7484	. . . . . . . . . . . . . . . . . 18 |- ( T e. ( CC ^m CC ) <-> T : CC --> CC )
198	196, 197	sylibr 212	. . . . . . . . . . . . . . . . 17 |- ( ph -> T e. ( CC ^m CC ) )
199	195, 198	sseldi 3439	. . . . . . . . . . . . . . . 16 |- ( ph -> T e. ( CC ^pm CC ) )
200		dvnp1 22618	. . . . . . . . . . . . . . . 16 |- ( ( 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, 98, 200	syl3anc 1230	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` ( ( N - 1 ) + 1 ) ) = ( CC _D ( ( CC Dn T ) ` ( N - 1 ) ) ) )
202	121	fveq2d 5852	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` ( ( N - 1 ) + 1 ) ) = ( ( CC Dn T ) ` N ) )
203	201, 202	eqtr3d 2445	. . . . . . . . . . . . . 14 |- ( ph -> ( CC _D ( ( CC Dn T ) ` ( N - 1 ) ) ) = ( ( CC Dn T ) ` N ) )
204	157	feqmptd 5901	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) = ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) )
205	204	oveq2d 6293	. . . . . . . . . . . . . 14 |- ( ph -> ( CC _D ( ( CC Dn T ) ` ( N - 1 ) ) ) = ( CC _D ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) )
206	181	feqmptd 5901	. . . . . . . . . . . . . 14 |- ( ph -> ( ( CC Dn T ) ` N ) = ( y e. CC |-> ( ( ( CC Dn T ) ` N ) ` y ) ) )
207	203, 205, 206	3eqtr3d 2451	. . . . . . . . . . . . 13 |- ( ph -> ( CC _D ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) = ( y e. CC |-> ( ( ( CC Dn T ) ` N ) ` y ) ) )
208	187, 68, 190, 192, 158, 182, 207	dvmptres3 22649	. . . . . . . . . . . 12 |- ( ph -> ( S _D ( y e. S |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) = ( y e. S |-> ( ( ( CC Dn T ) ` N ) ` y ) ) )
209		eqid 2402	. . . . . . . . . . . 12 |- ( ( TopOpen ` ℂfld ) ↾t S ) = ( ( TopOpen ` ℂfld ) ↾t S )
210		resttopon 19953	. . . . . . . . . . . . . . . 16 |- ( ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) /\ S C_ CC ) -> ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) )
211	188, 124, 210	sylancr 661	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) )
212		topontop 19717	. . . . . . . . . . . . . . 15 |- ( ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) -> ( ( TopOpen ` ℂfld ) ↾t S ) e. Top )
213	211, 212	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t S ) e. Top )
214		toponuni 19718	. . . . . . . . . . . . . . . 16 |- ( ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) -> S = U. ( ( TopOpen ` ℂfld ) ↾t S ) )
215	211, 214	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> S = U. ( ( TopOpen ` ℂfld ) ↾t S ) )
216	70, 215	sseqtrd 3477	. . . . . . . . . . . . . 14 |- ( ph -> A C_ U. ( ( TopOpen ` ℂfld ) ↾t S ) )
217		eqid 2402	. . . . . . . . . . . . . . 15 |- U. ( ( TopOpen ` ℂfld ) ↾t S ) = U. ( ( TopOpen ` ℂfld ) ↾t S )
218	217	ntrss2 19848	. . . . . . . . . . . . . 14 |- ( ( ( ( TopOpen ` ℂfld ) ↾t S ) e. Top /\ A C_ U. ( ( TopOpen ` ℂfld ) ↾t S ) ) -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` A ) C_ A )
219	213, 216, 218	syl2anc 659	. . . . . . . . . . . . 13 |- ( ph -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` A ) C_ A )
220	140	dmeqd 5025	. . . . . . . . . . . . . . 15 |- ( ph -> dom ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) = dom ( ( S Dn F ) ` N ) )
221	220, 76	eqtrd 2443	. . . . . . . . . . . . . 14 |- ( ph -> dom ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) = A )
222	124, 114, 70, 209, 187	dvbssntr 22594	. . . . . . . . . . . . . 14 |- ( ph -> dom ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` A ) )
223	221, 222	eqsstr3d 3476	. . . . . . . . . . . . 13 |- ( ph -> A C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` A ) )
224	219, 223	eqssd 3458	. . . . . . . . . . . 12 |- ( ph -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` A ) = A )
225	68, 185, 186, 208, 70, 209, 187, 224	dvmptres2 22655	. . . . . . . . . . 11 |- ( ph -> ( S _D ( y e. A |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) = ( y e. A |-> ( ( ( CC Dn T ) ` N ) ` y ) ) )
226	68, 115, 118, 131, 159, 183, 225	dvmptsub 22660	. . . . . . . . . 10 |- ( 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 4405	. . . . . . . . 9 |- ( 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	96, 227	mpbird 232	. . . . . . . 8 |- ( ph -> B ( S _D ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ) 0 )
229		eqid 2402	. . . . . . . . 9 |- ( 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 9966	. . . . . . . . . 10 |- ( ( ph /\ y e. A ) -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) e. CC )
231		eqid 2402	. . . . . . . . . 10 |- ( 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 ) ) )
232	230, 231	fmptd 6032	. . . . . . . . 9 |- ( ph -> ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) : A --> CC )
233	209, 187, 229, 124, 232, 70	eldv 22592	. . . . . . . 8 |- ( ph -> ( B ( S _D ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ) 0 <-> ( B e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾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 ) ) ) lim CC B ) ) ) )
234	228, 233	mpbid 210	. . . . . . 7 |- ( ph -> ( B e. ( ( int ` ( ( TopOpen ` ℂfld ) ↾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 ) ) ) lim CC B ) ) )
235	234	simprd 461	. . . . . 6 |- ( 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 ) ) ) lim CC B ) )
236		eldifi 3564	. . . . . . . . . 10 |- ( x e. ( A \ { B } ) -> x e. A )
237		fveq2 5848	. . . . . . . . . . . . . 14 |- ( y = x -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) )
238		fveq2 5848	. . . . . . . . . . . . . 14 |- ( y = x -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) = ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) )
239	237, 238	oveq12d 6295	. . . . . . . . . . . . 13 |- ( 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 ) ) )
240		ovex 6305	. . . . . . . . . . . . 13 |- ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) e. _V
241	239, 231, 240	fvmpt 5931	. . . . . . . . . . . 12 |- ( 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 5848	. . . . . . . . . . . . . . . 16 |- ( y = B -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) )
243		fveq2 5848	. . . . . . . . . . . . . . . 16 |- ( y = B -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) = ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) )
244	242, 243	oveq12d 6295	. . . . . . . . . . . . . . 15 |- ( 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 6305	. . . . . . . . . . . . . . 15 |- ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) ) e. _V
246	244, 231, 245	fvmpt 5931	. . . . . . . . . . . . . 14 |- ( 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	60, 246	syl 17	. . . . . . . . . . . . 13 |- ( 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	68, 69, 70, 108, 77, 78	dvntaylp0 23057	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) )
249	248	oveq2d 6293	. . . . . . . . . . . . 13 |- ( 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, 60	ffvelrnd 6009	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) e. CC )
251	250	subidd 9954	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) - ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) ) = 0 )
252	247, 249, 251	3eqtrd 2447	. . . . . . . . . . . 12 |- ( ph -> ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` B ) = 0 )
253	241, 252	oveqan12rd 6297	. . . . . . . . . . 11 |- ( ( 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 6008	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) e. CC )
255	132	sselda 3441	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. A ) -> x e. CC )
256	157	ffvelrnda 6008	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. CC ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) e. CC )
257	255, 256	syldan 468	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) e. CC )
258	254, 257	subcld 9966	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) e. CC )
259	258	subid1d 9955	. . . . . . . . . . 11 |- ( ( 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 2444	. . . . . . . . . 10 |- ( ( 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	236, 260	sylan2 472	. . . . . . . . 9 |- ( ( 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 3580	. . . . . . . . . . . 12 |- ( ph -> ( A \ { B } ) C_ CC )
263	262	sselda 3441	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( A \ { B } ) ) -> x e. CC )
264	132, 60	sseldd 3442	. . . . . . . . . . . 12 |- ( ph -> B e. CC )
265	264	adantr 463	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( A \ { B } ) ) -> B e. CC )
266	263, 265	subcld 9966	. . . . . . . . . 10 |- ( ( ph /\ x e. ( A \ { B } ) ) -> ( x - B ) e. CC )
267	266	exp1d 12347	. . . . . . . . 9 |- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( x - B ) ^ 1 ) = ( x - B ) )
268	261, 267	oveq12d 6295	. . . . . . . 8 |- ( ( 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 4480	. . . . . . 7 |- ( 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 6292	. . . . . 6 |- ( ph -> ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) / ( ( x - B ) ^ 1 ) ) ) lim CC 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 ) ) ) lim CC B ) )
271	235, 270	eleqtrrd 2493	. . . . 5 |- ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) / ( ( x - B ) ^ 1 ) ) ) lim CC B ) )
272	271	a1i 11	. . . 4 |- ( 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 ) ) ) lim CC B ) ) )
273		taylthlem1.i	. . . . . . 7 |- ( ( 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 ) ) ) lim CC 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 ) ) ) ) lim CC B ) )
274	273	expr 613	. . . . . 6 |- ( ( 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 ) ) ) lim CC 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 ) ) ) ) lim CC B ) ) )
275	274	expcom 433	. . . . 5 |- ( 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 ) ) ) lim CC 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 ) ) ) ) lim CC B ) ) ) )
276	275	a2d 26	. . . 4 |- ( 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 ) ) ) lim CC 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 ) ) ) ) lim CC B ) ) ) )
277	15, 35, 47, 59, 272, 276	fzind2 11959	. . 3 |- ( 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 ) ) ) lim CC B ) ) )
278	3, 277	mpcom 34	. 2 |- ( ph -> 0 e. ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) / ( ( x - B ) ^ N ) ) ) lim CC B ) )
279	119	subidd 9954	. . . . . . . . . 10 |- ( ph -> ( N - N ) = 0 )
280	279	fveq2d 5852	. . . . . . . . 9 |- ( ph -> ( ( S Dn F ) ` ( N - N ) ) = ( ( S Dn F ) ` 0 ) )
281		dvn0 22617	. . . . . . . . . 10 |- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = F )
282	124, 84, 281	syl2anc 659	. . . . . . . . 9 |- ( ph -> ( ( S Dn F ) ` 0 ) = F )
283	280, 282	eqtrd 2443	. . . . . . . 8 |- ( ph -> ( ( S Dn F ) ` ( N - N ) ) = F )
284	283	fveq1d 5850	. . . . . . 7 |- ( ph -> ( ( ( S Dn F ) ` ( N - N ) ) ` x ) = ( F ` x ) )
285	279	fveq2d 5852	. . . . . . . . 9 |- ( ph -> ( ( CC Dn T ) ` ( N - N ) ) = ( ( CC Dn T ) ` 0 ) )
286		dvn0 22617	. . . . . . . . . 10 |- ( ( CC C_ CC /\ T e. ( CC ^pm CC ) ) -> ( ( CC Dn T ) ` 0 ) = T )
287	193, 199, 286	sylancr 661	. . . . . . . . 9 |- ( ph -> ( ( CC Dn T ) ` 0 ) = T )
288	285, 287	eqtrd 2443	. . . . . . . 8 |- ( ph -> ( ( CC Dn T ) ` ( N - N ) ) = T )
289	288	fveq1d 5850	. . . . . . 7 |- ( ph -> ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) = ( T ` x ) )
290	284, 289	oveq12d 6295	. . . . . 6 |- ( ph -> ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) = ( ( F ` x ) - ( T ` x ) ) )
291	290	oveq1d 6292	. . . . 5 |- ( ph -> ( ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) / ( ( x - B ) ^ N ) ) = ( ( ( F ` x ) - ( T ` x ) ) / ( ( x - B ) ^ N ) ) )
292	291	mpteq2dv 4481	. . . 4 |- ( 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 ) ) ) )
293		taylthlem1.r	. . . 4 |- R = ( x e. ( A \ { B } ) |-> ( ( ( F ` x ) - ( T ` x ) ) / ( ( x - B ) ^ N ) ) )
294	292, 293	syl6eqr 2461	. . 3 |- ( ph -> ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) / ( ( x - B ) ^ N ) ) ) = R )
295	294	oveq1d 6292	. 2 |- ( ph -> ( ( x e. ( A \ { B } ) |-> ( ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) / ( ( x - B ) ^ N ) ) ) lim CC B ) = ( R lim CC B ) )
296	278, 295	eleqtrd 2492	1 |- ( ph -> 0 e. ( R lim CC B ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 367   = wceq 1405   e. wcel 1842   _Vcvv 3058   \ cdif 3410   i^i cin 3412   C_ wss 3413   {csn 3971   {cpr 3973   U.cuni 4190   class class class wbr 4394   |-> cmpt 4452   dom cdm 4822   Fun wfun 5562   -->wf 5564   ` cfv 5568  (class class class)co 6277   ^m cmap 7456   ^pm cpm 7457   CCcc 9519   RRcr 9520   0cc0 9521   1c1 9522   + caddc 9524   - cmin 9840   / cdiv 10246   NNcn 10575   NN0cn0 10835   ZZ>=cuz 11126   ...cfz 11724  ..^cfzo 11852   ^cexp 12208   ↾_t crest 15033   TopOpenctopn 15034  ℂ_fldccnfld 18738   Topctop 19684  TopOnctopon 19685   intcnt 19808   lim CC climc 22556   _D cdv 22557   Dncdvn 22558   Tayl ctayl 23038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573  ax-inf2 8090  ax-cnex 9577  ax-resscn 9578  ax-1cn 9579  ax-icn 9580  ax-addcl 9581  ax-addrcl 9582  ax-mulcl 9583  ax-mulrcl 9584  ax-mulcom 9585  ax-addass 9586  ax-mulass 9587  ax-distr 9588  ax-i2m1 9589  ax-1ne0 9590  ax-1rid 9591  ax-rnegex 9592  ax-rrecex 9593  ax-cnre 9594  ax-pre-lttri 9595  ax-pre-lttrn 9596  ax-pre-ltadd 9597  ax-pre-mulgt0 9598  ax-pre-sup 9599  ax-addf 9600  ax-mulf 9601

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 975  df-3an 976  df-tru 1408  df-fal 1411  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-nel 2601  df-ral 2758  df-rex 2759  df-reu 2760  df-rmo 2761  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-pss 3429  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-tp 3976  df-op 3978  df-uni 4191  df-int 4227  df-iun 4272  df-iin 4273  df-br 4395  df-opab 4453  df-mpt 4454  df-tr 4489  df-eprel 4733  df-id 4737  df-po 4743  df-so 4744  df-fr 4781  df-se 4782  df-we 4783  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-res 4834  df-ima 4835  df-pred 5366  df-ord 5412  df-on 5413  df-lim 5414  df-suc 5415  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-f1 5573  df-fo 5574  df-f1o 5575  df-fv 5576  df-isom 5577  df-riota 6239  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-of 6520  df-om 6683  df-1st 6783  df-2nd 6784  df-supp 6902  df-wrecs 7012  df-recs 7074  df-rdg 7112  df-1o 7166  df-2o 7167  df-oadd 7170  df-er 7347  df-map 7458  df-pm 7459  df-ixp 7507  df-en 7554  df-dom 7555  df-sdom 7556  df-fin 7557  df-fsupp 7863  df-fi 7904  df-sup 7934  df-oi 7968  df-card 8351  df-cda 8579  df-pnf 9659  df-mnf 9660  df-xr 9661  df-ltxr 9662  df-le 9663  df-sub 9842  df-neg 9843  df-div 10247  df-nn 10576  df-2 10634  df-3 10635  df-4 10636  df-5 10637  df-6 10638  df-7 10639  df-8 10640  df-9 10641  df-10 10642  df-n0 10836  df-z 10905  df-dec 11019  df-uz 11127  df-q 11227  df-rp 11265  df-xneg 11370  df-xadd 11371  df-xmul 11372  df-icc 11588  df-fz 11725  df-fzo 11853  df-seq 12150  df-exp 12209  df-fac 12396  df-hash 12451  df-cj 13079  df-re 13080  df-im 13081  df-sqrt 13215  df-abs 13216  df-clim 13458  df-sum 13656  df-struct 14841  df-ndx 14842  df-slot 14843  df-base 14844  df-sets 14845  df-ress 14846  df-plusg 14920  df-mulr 14921  df-starv 14922  df-sca 14923  df-vsca 14924  df-ip 14925  df-tset 14926  df-ple 14927  df-ds 14929  df-unif 14930  df-hom 14931  df-cco 14932  df-rest 15035  df-topn 15036  df-0g 15054  df-gsum 15055  df-topgen 15056  df-pt 15057  df-prds 15060  df-xrs 15114  df-qtop 15119  df-imas 15120  df-xps 15122  df-mre 15198  df-mrc 15199  df-acs 15201  df-mgm 16194  df-sgrp 16233  df-mnd 16243  df-submnd 16289  df-grp 16379  df-minusg 16380  df-mulg 16382  df-cntz 16677  df-cmn 17122  df-abl 17123  df-mgp 17460  df-ur 17472  df-ring 17518  df-cring 17519  df-psmet 18729  df-xmet 18730  df-met 18731  df-bl 18732  df-mopn 18733  df-fbas 18734  df-fg 18735  df-cnfld 18739  df-top 19689  df-bases 19691  df-topon 19692  df-topsp 19693  df-cld 19810  df-ntr 19811  df-cls 19812  df-nei 19890  df-lp 19928  df-perf 19929  df-cn 20019  df-cnp 20020  df-haus 20107  df-tx 20353  df-hmeo 20546  df-fil 20637  df-fm 20729  df-flim 20730  df-flf 20731  df-tsms 20915  df-xms 21113  df-ms 21114  df-tms 21115  df-cncf 21672  df-limc 22560  df-dv 22561  df-dvn 22562  df-tayl 23040

This theorem is referenced by:  taylth  23060