Theorem taylthlem1 23305

Description: Lemma for taylth 23307. 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 23307 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 11823	. . . 4 |- ( N e. NN <-> N e. ( 1 ... N ) )
3	1, 2	sylib 199	. . 3 |- ( ph -> N e. ( 1 ... N ) )
4		oveq2 6305	. . . . . . . . . . . 12 |- ( m = 1 -> ( N - m ) = ( N - 1 ) )
5	4	fveq2d 5877	. . . . . . . . . . 11 |- ( m = 1 -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - 1 ) ) )
6	5	fveq1d 5875	. . . . . . . . . 10 |- ( m = 1 -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) )
7	4	fveq2d 5877	. . . . . . . . . . 11 |- ( m = 1 -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - 1 ) ) )
8	7	fveq1d 5875	. . . . . . . . . 10 |- ( m = 1 -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) )
9	6, 8	oveq12d 6315	. . . . . . . . 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 6305	. . . . . . . . 9 |- ( m = 1 -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ 1 ) )
11	9, 10	oveq12d 6315	. . . . . . . 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 4505	. . . . . . 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 6312	. . . . . 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 2490	. . . . 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 317	. . . 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 6305	. . . . . . . . . . . . 13 |- ( m = n -> ( N - m ) = ( N - n ) )
17	16	fveq2d 5877	. . . . . . . . . . . 12 |- ( m = n -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - n ) ) )
18	17	fveq1d 5875	. . . . . . . . . . 11 |- ( m = n -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - n ) ) ` x ) )
19	16	fveq2d 5877	. . . . . . . . . . . 12 |- ( m = n -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - n ) ) )
20	19	fveq1d 5875	. . . . . . . . . . 11 |- ( m = n -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - n ) ) ` x ) )
21	18, 20	oveq12d 6315	. . . . . . . . . 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 6305	. . . . . . . . . 10 |- ( m = n -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ n ) )
23	21, 22	oveq12d 6315	. . . . . . . . 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 4505	. . . . . . . 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 5873	. . . . . . . . . . 11 |- ( x = y -> ( ( ( S Dn F ) ` ( N - n ) ) ` x ) = ( ( ( S Dn F ) ` ( N - n ) ) ` y ) )
26		fveq2 5873	. . . . . . . . . . 11 |- ( x = y -> ( ( ( CC Dn T ) ` ( N - n ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - n ) ) ` y ) )
27	25, 26	oveq12d 6315	. . . . . . . . . 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 6304	. . . . . . . . . . 11 |- ( x = y -> ( x - B ) = ( y - B ) )
29	28	oveq1d 6312	. . . . . . . . . 10 |- ( x = y -> ( ( x - B ) ^ n ) = ( ( y - B ) ^ n ) )
30	27, 29	oveq12d 6315	. . . . . . . . 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 4510	. . . . . . . 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 2477	. . . . . . 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 6312	. . . . . 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 2490	. . . . 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 317	. . . 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 6305	. . . . . . . . . . . 12 |- ( m = ( n + 1 ) -> ( N - m ) = ( N - ( n + 1 ) ) )
37	36	fveq2d 5877	. . . . . . . . . . 11 |- ( m = ( n + 1 ) -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) )
38	37	fveq1d 5875	. . . . . . . . . 10 |- ( m = ( n + 1 ) -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) ` x ) )
39	36	fveq2d 5877	. . . . . . . . . . 11 |- ( m = ( n + 1 ) -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) )
40	39	fveq1d 5875	. . . . . . . . . 10 |- ( m = ( n + 1 ) -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) ` x ) )
41	38, 40	oveq12d 6315	. . . . . . . . 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 6305	. . . . . . . . 9 |- ( m = ( n + 1 ) -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ ( n + 1 ) ) )
43	41, 42	oveq12d 6315	. . . . . . . 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 4505	. . . . . . 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 6312	. . . . . 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 2490	. . . . 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 317	. . . 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 6305	. . . . . . . . . . . 12 |- ( m = N -> ( N - m ) = ( N - N ) )
49	48	fveq2d 5877	. . . . . . . . . . 11 |- ( m = N -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - N ) ) )
50	49	fveq1d 5875	. . . . . . . . . 10 |- ( m = N -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - N ) ) ` x ) )
51	48	fveq2d 5877	. . . . . . . . . . 11 |- ( m = N -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - N ) ) )
52	51	fveq1d 5875	. . . . . . . . . 10 |- ( m = N -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) )
53	50, 52	oveq12d 6315	. . . . . . . . 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 6305	. . . . . . . . 9 |- ( m = N -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ N ) )
55	53, 54	oveq12d 6315	. . . . . . . 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 4505	. . . . . . 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 6312	. . . . . 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 2490	. . . . 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 317	. . . 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 5873	. . . . . . . . . . . . . 14 |- ( y = B -> ( ( ( S Dn F ) ` N ) ` y ) = ( ( ( S Dn F ) ` N ) ` B ) )
62		fveq2 5873	. . . . . . . . . . . . . 14 |- ( y = B -> ( ( ( CC Dn T ) ` N ) ` y ) = ( ( ( CC Dn T ) ` N ) ` B ) )
63	61, 62	oveq12d 6315	. . . . . . . . . . . . 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 2420	. . . . . . . . . . . . 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 6325	. . . . . . . . . . . . 13 |- ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( CC Dn T ) ` N ) ` B ) ) e. _V
66	63, 64, 65	fvmpt 5956	. . . . . . . . . . . 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 10921	. . . . . . . . . . . . . . 15 |- ( ph -> N e. NN0 )
72		nn0uz 11189	. . . . . . . . . . . . . . 15 |- NN0 = ( ZZ>= ` 0 )
73	71, 72	syl6eleq 2518	. . . . . . . . . . . . . 14 |- ( ph -> N e. ( ZZ>= ` 0 ) )
74		eluzfz2b 11802	. . . . . . . . . . . . . 14 |- ( N e. ( ZZ>= ` 0 ) <-> N e. ( 0 ... N ) )
75	73, 74	sylib 199	. . . . . . . . . . . . 13 |- ( ph -> N e. ( 0 ... N ) )
76		taylthlem1.d	. . . . . . . . . . . . . 14 |- ( ph -> dom ( ( S Dn F ) ` N ) = A )
77	60, 76	eleqtrrd 2511	. . . . . . . . . . . . 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 23304	. . . . . . . . . . . 12 |- ( ph -> ( ( ( CC Dn T ) ` N ) ` B ) = ( ( ( S Dn F ) ` N ) ` B ) )
80	79	oveq2d 6313	. . . . . . . . . . 11 |- ( ph -> ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( CC Dn T ) ` N ) ` B ) ) = ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( S Dn F ) ` N ) ` B ) ) )
81		cnex 9616	. . . . . . . . . . . . . . . 16 |- CC e. _V
82	81	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> CC e. _V )
83		elpm2r 7489	. . . . . . . . . . . . . . 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 1265	. . . . . . . . . . . . . 14 |- ( ph -> F e. ( CC ^pm S ) )
85		dvnf 22858	. . . . . . . . . . . . . 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 1264	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` N ) : dom ( ( S Dn F ) ` N ) --> CC )
87	86, 77	ffvelrnd 6030	. . . . . . . . . . . 12 |- ( ph -> ( ( ( S Dn F ) ` N ) ` B ) e. CC )
88	87	subidd 9970	. . . . . . . . . . 11 |- ( ph -> ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( S Dn F ) ` N ) ` B ) ) = 0 )
89	67, 80, 88	3eqtrd 2465	. . . . . . . . . 10 |- ( ph -> ( ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) ` B ) = 0 )
90		funmpt 5629	. . . . . . . . . . 11 |- Fun ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) )
91		ovex 6325	. . . . . . . . . . . . 13 |- ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) e. _V
92	91, 64	dmmpti 5717	. . . . . . . . . . . 12 |- dom ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) = A
93	60, 92	syl6eleqr 2519	. . . . . . . . . . 11 |- ( ph -> B e. dom ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) )
94		funbrfvb 5915	. . . . . . . . . . 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 667	. . . . . . . . . 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 213	. . . . . . . . 9 |- ( ph -> B ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) 0 )
97		nnm1nn0 10907	. . . . . . . . . . . . . . 15 |- ( N e. NN -> ( N - 1 ) e. NN0 )
98	1, 97	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> ( N - 1 ) e. NN0 )
99		dvnf 22858	. . . . . . . . . . . . . 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 1264	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) : dom ( ( S Dn F ) ` ( N - 1 ) ) --> CC )
101		dvnbss 22859	. . . . . . . . . . . . . . . . 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 1264	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( ( S Dn F ) ` ( N - 1 ) ) C_ dom F )
103		fdm 5742	. . . . . . . . . . . . . . . . 17 |- ( F : A --> CC -> dom F = A )
104	69, 103	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> dom F = A )
105	102, 104	sseqtrd 3497	. . . . . . . . . . . . . . 15 |- ( ph -> dom ( ( S Dn F ) ` ( N - 1 ) ) C_ A )
106		fzo0end 11996	. . . . . . . . . . . . . . . . . 18 |- ( N e. NN -> ( N - 1 ) e. ( 0..^ N ) )
107		elfzofz 11929	. . . . . . . . . . . . . . . . . 18 |- ( ( N - 1 ) e. ( 0..^ N ) -> ( N - 1 ) e. ( 0 ... N ) )
108	1, 106, 107	3syl 18	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( N - 1 ) e. ( 0 ... N ) )
109		dvn2bss 22861	. . . . . . . . . . . . . . . . 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 1264	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( ( S Dn F ) ` N ) C_ dom ( ( S Dn F ) ` ( N - 1 ) ) )
111	76, 110	eqsstr3d 3496	. . . . . . . . . . . . . . 15 |- ( ph -> A C_ dom ( ( S Dn F ) ` ( N - 1 ) ) )
112	105, 111	eqssd 3478	. . . . . . . . . . . . . 14 |- ( ph -> dom ( ( S Dn F ) ` ( N - 1 ) ) = A )
113	112	feq2d 5725	. . . . . . . . . . . . 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 213	. . . . . . . . . . . 12 |- ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) : A --> CC )
115	114	ffvelrnda 6029	. . . . . . . . . . 11 |- ( ( ph /\ y e. A ) -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) e. CC )
116	76	feq2d 5725	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( S Dn F ) ` N ) : dom ( ( S Dn F ) ` N ) --> CC <-> ( ( S Dn F ) ` N ) : A --> CC ) )
117	86, 116	mpbid 213	. . . . . . . . . . . 12 |- ( ph -> ( ( S Dn F ) ` N ) : A --> CC )
118	117	ffvelrnda 6029	. . . . . . . . . . 11 |- ( ( ph /\ y e. A ) -> ( ( ( S Dn F ) ` N ) ` y ) e. CC )
119	1	nncnd 10621	. . . . . . . . . . . . . . 15 |- ( ph -> N e. CC )
120		1cnd 9655	. . . . . . . . . . . . . . 15 |- ( ph -> 1 e. CC )
121	119, 120	npcand 9986	. . . . . . . . . . . . . 14 |- ( ph -> ( ( N - 1 ) + 1 ) = N )
122	121	fveq2d 5877	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` ( ( N - 1 ) + 1 ) ) = ( ( S Dn F ) ` N ) )
123		recnprss 22836	. . . . . . . . . . . . . . 15 |- ( S e. { RR , CC } -> S C_ CC )
124	68, 123	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> S C_ CC )
125		dvnp1 22856	. . . . . . . . . . . . . 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 1264	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` ( ( N - 1 ) + 1 ) ) = ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) )
127	122, 126	eqtr3d 2463	. . . . . . . . . . . 12 |- ( ph -> ( ( S Dn F ) ` N ) = ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) )
128	117	feqmptd 5926	. . . . . . . . . . . 12 |- ( ph -> ( ( S Dn F ) ` N ) = ( y e. A |-> ( ( ( S Dn F ) ` N ) ` y ) ) )
129	114	feqmptd 5926	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) = ( y e. A |-> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) ) )
130	129	oveq2d 6313	. . . . . . . . . . . 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 2470	. . . . . . . . . . 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 3471	. . . . . . . . . . . . 13 |- ( ph -> A C_ CC )
133	132	sselda 3461	. . . . . . . . . . . 12 |- ( ( ph /\ y e. A ) -> y e. CC )
134		1nn0 10881	. . . . . . . . . . . . . . . 16 |- 1 e. NN0
135	134	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 1 e. NN0 )
136		elpm2r 7489	. . . . . . . . . . . . . . . . . . . 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 1265	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) e. ( CC ^pm S ) )
138		dvn1 22857	. . . . . . . . . . . . . . . . . . 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 665	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) = ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) )
140	126, 122	eqtr3d 2463	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) = ( ( S Dn F ) ` N ) )
141	139, 140	eqtrd 2461	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) = ( ( S Dn F ) ` N ) )
142	141	dmeqd 5049	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) = dom ( ( S Dn F ) ` N ) )
143	77, 142	eleqtrrd 2511	. . . . . . . . . . . . . . 15 |- ( ph -> B e. dom ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) )
144		eqid 2420	. . . . . . . . . . . . . . 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 23298	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 ( S Tayl ( ( S Dn F ) ` ( N - 1 ) ) ) B ) : CC --> CC )
146	120, 119	pncan3d 9985	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 + ( N - 1 ) ) = N )
147	146	oveq1d 6312	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) = ( N ( S Tayl F ) B ) )
148	147, 78	syl6reqr 2480	. . . . . . . . . . . . . . . . . 18 |- ( ph -> T = ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) )
149	148	oveq2d 6313	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( CC Dn T ) = ( CC Dn ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) ) )
150	149	fveq1d 5875	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) = ( ( CC Dn ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) ) ` ( N - 1 ) ) )
151	146	fveq2d 5877	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( S Dn F ) ` ( 1 + ( N - 1 ) ) ) = ( ( S Dn F ) ` N ) )
152	151	dmeqd 5049	. . . . . . . . . . . . . . . . . 18 |- ( ph -> dom ( ( S Dn F ) ` ( 1 + ( N - 1 ) ) ) = dom ( ( S Dn F ) ` N ) )
153	77, 152	eleqtrrd 2511	. . . . . . . . . . . . . . . . 17 |- ( ph -> B e. dom ( ( S Dn F ) ` ( 1 + ( N - 1 ) ) ) )
154	68, 69, 70, 98, 135, 153	dvntaylp 23303	. . . . . . . . . . . . . . . 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 2461	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) = ( 1 ( S Tayl ( ( S Dn F ) ` ( N - 1 ) ) ) B ) )
156	155	feq1d 5724	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( CC Dn T ) ` ( N - 1 ) ) : CC --> CC <-> ( 1 ( S Tayl ( ( S Dn F ) ` ( N - 1 ) ) ) B ) : CC --> CC ) )
157	145, 156	mpbird 235	. . . . . . . . . . . . 13 |- ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) : CC --> CC )
158	157	ffvelrnda 6029	. . . . . . . . . . . 12 |- ( ( ph /\ y e. CC ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) e. CC )
159	133, 158	syldan 472	. . . . . . . . . . 11 |- ( ( ph /\ y e. A ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) e. CC )
160		0nn0 10880	. . . . . . . . . . . . . . . 16 |- 0 e. NN0
161	160	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 0 e. NN0 )
162		elpm2r 7489	. . . . . . . . . . . . . . . . . . 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 1265	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( S Dn F ) ` N ) e. ( CC ^pm S ) )
164		dvn0 22855	. . . . . . . . . . . . . . . . . 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 665	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( S Dn ( ( S Dn F ) ` N ) ) ` 0 ) = ( ( S Dn F ) ` N ) )
166	165	dmeqd 5049	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( ( S Dn ( ( S Dn F ) ` N ) ) ` 0 ) = dom ( ( S Dn F ) ` N ) )
167	77, 166	eleqtrrd 2511	. . . . . . . . . . . . . . 15 |- ( ph -> B e. dom ( ( S Dn ( ( S Dn F ) ` N ) ) ` 0 ) )
168		eqid 2420	. . . . . . . . . . . . . . 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 23298	. . . . . . . . . . . . . 14 |- ( ph -> ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) : CC --> CC )
170	119	addid2d 9830	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 0 + N ) = N )
171	170	oveq1d 6312	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( 0 + N ) ( S Tayl F ) B ) = ( N ( S Tayl F ) B ) )
172	171, 78	syl6eqr 2479	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( 0 + N ) ( S Tayl F ) B ) = T )
173	172	oveq2d 6313	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( CC Dn ( ( 0 + N ) ( S Tayl F ) B ) ) = ( CC Dn T ) )
174	173	fveq1d 5875	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( CC Dn ( ( 0 + N ) ( S Tayl F ) B ) ) ` N ) = ( ( CC Dn T ) ` N ) )
175	170	fveq2d 5877	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( S Dn F ) ` ( 0 + N ) ) = ( ( S Dn F ) ` N ) )
176	175	dmeqd 5049	. . . . . . . . . . . . . . . . . 18 |- ( ph -> dom ( ( S Dn F ) ` ( 0 + N ) ) = dom ( ( S Dn F ) ` N ) )
177	77, 176	eleqtrrd 2511	. . . . . . . . . . . . . . . . 17 |- ( ph -> B e. dom ( ( S Dn F ) ` ( 0 + N ) ) )
178	68, 69, 70, 71, 161, 177	dvntaylp 23303	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( CC Dn ( ( 0 + N ) ( S Tayl F ) B ) ) ` N ) = ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) )
179	174, 178	eqtr3d 2463	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` N ) = ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) )
180	179	feq1d 5724	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( CC Dn T ) ` N ) : CC --> CC <-> ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) : CC --> CC ) )
181	169, 180	mpbird 235	. . . . . . . . . . . . 13 |- ( ph -> ( ( CC Dn T ) ` N ) : CC --> CC )
182	181	ffvelrnda 6029	. . . . . . . . . . . 12 |- ( ( ph /\ y e. CC ) -> ( ( ( CC Dn T ) ` N ) ` y ) e. CC )
183	133, 182	syldan 472	. . . . . . . . . . 11 |- ( ( ph /\ y e. A ) -> ( ( ( CC Dn T ) ` N ) ` y ) e. CC )
184	124	sselda 3461	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. S ) -> y e. CC )
185	184, 158	syldan 472	. . . . . . . . . . . 12 |- ( ( ph /\ y e. S ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) e. CC )
186	184, 182	syldan 472	. . . . . . . . . . . 12 |- ( ( ph /\ y e. S ) -> ( ( ( CC Dn T ) ` N ) ` y ) e. CC )
187		eqid 2420	. . . . . . . . . . . . 13 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
188	187	cnfldtopon 21780	. . . . . . . . . . . . . 14 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
189		toponmax 19920	. . . . . . . . . . . . . 14 |- ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) -> CC e. ( TopOpen ` ℂfld ) )
190	188, 189	mp1i 13	. . . . . . . . . . . . 13 |- ( ph -> CC e. ( TopOpen ` ℂfld ) )
191		df-ss 3447	. . . . . . . . . . . . . 14 |- ( S C_ CC <-> ( S i^i CC ) = S )
192	124, 191	sylib 199	. . . . . . . . . . . . 13 |- ( ph -> ( S i^i CC ) = S )
193		ssid 3480	. . . . . . . . . . . . . . . . 17 |- CC C_ CC
194	193	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> CC C_ CC )
195		mapsspm 7505	. . . . . . . . . . . . . . . . 17 |- ( CC ^m CC ) C_ ( CC ^pm CC )
196	68, 69, 70, 71, 77, 78	taylpf 23298	. . . . . . . . . . . . . . . . . 18 |- ( ph -> T : CC --> CC )
197	81, 81	elmap 7500	. . . . . . . . . . . . . . . . . 18 |- ( T e. ( CC ^m CC ) <-> T : CC --> CC )
198	196, 197	sylibr 215	. . . . . . . . . . . . . . . . 17 |- ( ph -> T e. ( CC ^m CC ) )
199	195, 198	sseldi 3459	. . . . . . . . . . . . . . . 16 |- ( ph -> T e. ( CC ^pm CC ) )
200		dvnp1 22856	. . . . . . . . . . . . . . . 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 1264	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` ( ( N - 1 ) + 1 ) ) = ( CC _D ( ( CC Dn T ) ` ( N - 1 ) ) ) )
202	121	fveq2d 5877	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` ( ( N - 1 ) + 1 ) ) = ( ( CC Dn T ) ` N ) )
203	201, 202	eqtr3d 2463	. . . . . . . . . . . . . 14 |- ( ph -> ( CC _D ( ( CC Dn T ) ` ( N - 1 ) ) ) = ( ( CC Dn T ) ` N ) )
204	157	feqmptd 5926	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) = ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) )
205	204	oveq2d 6313	. . . . . . . . . . . . . 14 |- ( ph -> ( CC _D ( ( CC Dn T ) ` ( N - 1 ) ) ) = ( CC _D ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) )
206	181	feqmptd 5926	. . . . . . . . . . . . . 14 |- ( ph -> ( ( CC Dn T ) ` N ) = ( y e. CC |-> ( ( ( CC Dn T ) ` N ) ` y ) ) )
207	203, 205, 206	3eqtr3d 2469	. . . . . . . . . . . . 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 22887	. . . . . . . . . . . 12 |- ( ph -> ( S _D ( y e. S |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) = ( y e. S |-> ( ( ( CC Dn T ) ` N ) ` y ) ) )
209		eqid 2420	. . . . . . . . . . . 12 |- ( ( TopOpen ` ℂfld ) ↾t S ) = ( ( TopOpen ` ℂfld ) ↾t S )
210		resttopon 20154	. . . . . . . . . . . . . . . 16 |- ( ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) /\ S C_ CC ) -> ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) )
211	188, 124, 210	sylancr 667	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) )
212		topontop 19918	. . . . . . . . . . . . . . 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 19919	. . . . . . . . . . . . . . . 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 3497	. . . . . . . . . . . . . 14 |- ( ph -> A C_ U. ( ( TopOpen ` ℂfld ) ↾t S ) )
217		eqid 2420	. . . . . . . . . . . . . . 15 |- U. ( ( TopOpen ` ℂfld ) ↾t S ) = U. ( ( TopOpen ` ℂfld ) ↾t S )
218	217	ntrss2 20049	. . . . . . . . . . . . . 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 665	. . . . . . . . . . . . 13 |- ( ph -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` A ) C_ A )
220	140	dmeqd 5049	. . . . . . . . . . . . . . 15 |- ( ph -> dom ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) = dom ( ( S Dn F ) ` N ) )
221	220, 76	eqtrd 2461	. . . . . . . . . . . . . 14 |- ( ph -> dom ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) = A )
222	124, 114, 70, 209, 187	dvbssntr 22832	. . . . . . . . . . . . . 14 |- ( ph -> dom ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` A ) )
223	221, 222	eqsstr3d 3496	. . . . . . . . . . . . 13 |- ( ph -> A C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` A ) )
224	219, 223	eqssd 3478	. . . . . . . . . . . 12 |- ( ph -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` A ) = A )
225	68, 185, 186, 208, 70, 209, 187, 224	dvmptres2 22893	. . . . . . . . . . 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 22898	. . . . . . . . . 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 4428	. . . . . . . . 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 235	. . . . . . . 8 |- ( ph -> B ( S _D ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ) 0 )
229		eqid 2420	. . . . . . . . 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 9982	. . . . . . . . . 10 |- ( ( ph /\ y e. A ) -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) e. CC )
231		eqid 2420	. . . . . . . . . 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 6053	. . . . . . . . 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 22830	. . . . . . . 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 213	. . . . . . 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 464	. . . . . 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 3584	. . . . . . . . . 10 |- ( x e. ( A \ { B } ) -> x e. A )
237		fveq2 5873	. . . . . . . . . . . . . 14 |- ( y = x -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) )
238		fveq2 5873	. . . . . . . . . . . . . 14 |- ( y = x -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) = ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) )
239	237, 238	oveq12d 6315	. . . . . . . . . . . . 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 6325	. . . . . . . . . . . . 13 |- ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) e. _V
241	239, 231, 240	fvmpt 5956	. . . . . . . . . . . 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 5873	. . . . . . . . . . . . . . . 16 |- ( y = B -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) )
243		fveq2 5873	. . . . . . . . . . . . . . . 16 |- ( y = B -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) = ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) )
244	242, 243	oveq12d 6315	. . . . . . . . . . . . . . 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 6325	. . . . . . . . . . . . . . 15 |- ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) ) e. _V
246	244, 231, 245	fvmpt 5956	. . . . . . . . . . . . . 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 23304	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) )
249	248	oveq2d 6313	. . . . . . . . . . . . 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 6030	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) e. CC )
251	250	subidd 9970	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) - ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) ) = 0 )
252	247, 249, 251	3eqtrd 2465	. . . . . . . . . . . 12 |- ( ph -> ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` B ) = 0 )
253	241, 252	oveqan12rd 6317	. . . . . . . . . . 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 6029	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) e. CC )
255	132	sselda 3461	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. A ) -> x e. CC )
256	157	ffvelrnda 6029	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. CC ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) e. CC )
257	255, 256	syldan 472	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) e. CC )
258	254, 257	subcld 9982	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) e. CC )
259	258	subid1d 9971	. . . . . . . . . . 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 2462	. . . . . . . . . 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 476	. . . . . . . . 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 3600	. . . . . . . . . . . 12 |- ( ph -> ( A \ { B } ) C_ CC )
263	262	sselda 3461	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( A \ { B } ) ) -> x e. CC )
264	132, 60	sseldd 3462	. . . . . . . . . . . 12 |- ( ph -> B e. CC )
265	264	adantr 466	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( A \ { B } ) ) -> B e. CC )
266	263, 265	subcld 9982	. . . . . . . . . 10 |- ( ( ph /\ x e. ( A \ { B } ) ) -> ( x - B ) e. CC )
267	266	exp1d 12404	. . . . . . . . 9 |- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( x - B ) ^ 1 ) = ( x - B ) )
268	261, 267	oveq12d 6315	. . . . . . . 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 4504	. . . . . . 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 6312	. . . . . 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 2511	. . . . 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 618	. . . . . 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 436	. . . . 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 29	. . . 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 12016	. . 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 37	. 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 9970	. . . . . . . . . 10 |- ( ph -> ( N - N ) = 0 )
280	279	fveq2d 5877	. . . . . . . . 9 |- ( ph -> ( ( S Dn F ) ` ( N - N ) ) = ( ( S Dn F ) ` 0 ) )
281		dvn0 22855	. . . . . . . . . 10 |- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = F )
282	124, 84, 281	syl2anc 665	. . . . . . . . 9 |- ( ph -> ( ( S Dn F ) ` 0 ) = F )
283	280, 282	eqtrd 2461	. . . . . . . 8 |- ( ph -> ( ( S Dn F ) ` ( N - N ) ) = F )
284	283	fveq1d 5875	. . . . . . 7 |- ( ph -> ( ( ( S Dn F ) ` ( N - N ) ) ` x ) = ( F ` x ) )
285	279	fveq2d 5877	. . . . . . . . 9 |- ( ph -> ( ( CC Dn T ) ` ( N - N ) ) = ( ( CC Dn T ) ` 0 ) )
286		dvn0 22855	. . . . . . . . . 10 |- ( ( CC C_ CC /\ T e. ( CC ^pm CC ) ) -> ( ( CC Dn T ) ` 0 ) = T )
287	193, 199, 286	sylancr 667	. . . . . . . . 9 |- ( ph -> ( ( CC Dn T ) ` 0 ) = T )
288	285, 287	eqtrd 2461	. . . . . . . 8 |- ( ph -> ( ( CC Dn T ) ` ( N - N ) ) = T )
289	288	fveq1d 5875	. . . . . . 7 |- ( ph -> ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) = ( T ` x ) )
290	284, 289	oveq12d 6315	. . . . . 6 |- ( ph -> ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) = ( ( F ` x ) - ( T ` x ) ) )
291	290	oveq1d 6312	. . . . 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 4505	. . . 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 2479	. . 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 6312	. 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 2510	1 |- ( ph -> 0 e. ( R lim CC B ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   = wceq 1437   e. wcel 1867   _Vcvv 3078   \ cdif 3430   i^i cin 3432   C_ wss 3433   {csn 3993   {cpr 3995   U.cuni 4213   class class class wbr 4417   |-> cmpt 4476   dom cdm 4846   Fun wfun 5587   -->wf 5589   ` cfv 5593  (class class class)co 6297   ^m cmap 7472   ^pm cpm 7473   CCcc 9533   RRcr 9534   0cc0 9535   1c1 9536   + caddc 9538   - cmin 9856   / cdiv 10265   NNcn 10605   NN0cn0 10865   ZZ>=cuz 11155   ...cfz 11778  ..^cfzo 11909   ^cexp 12265   ↾_t crest 15297   TopOpenctopn 15298  ℂ_fldccnfld 18948   Topctop 19894  TopOnctopon 19895   intcnt 20009   lim CC climc 22794   _D cdv 22795   Dncdvn 22796   Tayl ctayl 23285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-rep 4530  ax-sep 4540  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6589  ax-inf2 8144  ax-cnex 9591  ax-resscn 9592  ax-1cn 9593  ax-icn 9594  ax-addcl 9595  ax-addrcl 9596  ax-mulcl 9597  ax-mulrcl 9598  ax-mulcom 9599  ax-addass 9600  ax-mulass 9601  ax-distr 9602  ax-i2m1 9603  ax-1ne0 9604  ax-1rid 9605  ax-rnegex 9606  ax-rrecex 9607  ax-cnre 9608  ax-pre-lttri 9609  ax-pre-lttrn 9610  ax-pre-ltadd 9611  ax-pre-mulgt0 9612  ax-pre-sup 9613  ax-addf 9614  ax-mulf 9615

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-reu 2780  df-rmo 2781  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-int 4250  df-iun 4295  df-iin 4296  df-br 4418  df-opab 4477  df-mpt 4478  df-tr 4513  df-eprel 4757  df-id 4761  df-po 4767  df-so 4768  df-fr 4805  df-se 4806  df-we 4807  df-xp 4852  df-rel 4853  df-cnv 4854  df-co 4855  df-dm 4856  df-rn 4857  df-res 4858  df-ima 4859  df-pred 5391  df-ord 5437  df-on 5438  df-lim 5439  df-suc 5440  df-iota 5557  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-isom 5602  df-riota 6259  df-ov 6300  df-oprab 6301  df-mpt2 6302  df-of 6537  df-om 6699  df-1st 6799  df-2nd 6800  df-supp 6918  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-2o 7183  df-oadd 7186  df-er 7363  df-map 7474  df-pm 7475  df-ixp 7523  df-en 7570  df-dom 7571  df-sdom 7572  df-fin 7573  df-fsupp 7882  df-fi 7923  df-sup 7954  df-inf 7955  df-oi 8023  df-card 8370  df-cda 8594  df-pnf 9673  df-mnf 9674  df-xr 9675  df-ltxr 9676  df-le 9677  df-sub 9858  df-neg 9859  df-div 10266  df-nn 10606  df-2 10664  df-3 10665  df-4 10666  df-5 10667  df-6 10668  df-7 10669  df-8 10670  df-9 10671  df-10 10672  df-n0 10866  df-z 10934  df-dec 11048  df-uz 11156  df-q 11261  df-rp 11299  df-xneg 11405  df-xadd 11406  df-xmul 11407  df-icc 11638  df-fz 11779  df-fzo 11910  df-seq 12207  df-exp 12266  df-fac 12453  df-hash 12509  df-cj 13141  df-re 13142  df-im 13143  df-sqrt 13277  df-abs 13278  df-clim 13530  df-sum 13731  df-struct 15101  df-ndx 15102  df-slot 15103  df-base 15104  df-sets 15105  df-ress 15106  df-plusg 15181  df-mulr 15182  df-starv 15183  df-sca 15184  df-vsca 15185  df-ip 15186  df-tset 15187  df-ple 15188  df-ds 15190  df-unif 15191  df-hom 15192  df-cco 15193  df-rest 15299  df-topn 15300  df-0g 15318  df-gsum 15319  df-topgen 15320  df-pt 15321  df-prds 15324  df-xrs 15378  df-qtop 15384  df-imas 15385  df-xps 15388  df-mre 15470  df-mrc 15471  df-acs 15473  df-mgm 16466  df-sgrp 16505  df-mnd 16515  df-submnd 16561  df-grp 16651  df-minusg 16652  df-mulg 16654  df-cntz 16949  df-cmn 17410  df-abl 17411  df-mgp 17702  df-ur 17714  df-ring 17760  df-cring 17761  df-psmet 18940  df-xmet 18941  df-met 18942  df-bl 18943  df-mopn 18944  df-fbas 18945  df-fg 18946  df-cnfld 18949  df-top 19898  df-bases 19899  df-topon 19900  df-topsp 19901  df-cld 20011  df-ntr 20012  df-cls 20013  df-nei 20091  df-lp 20129  df-perf 20130  df-cn 20220  df-cnp 20221  df-haus 20308  df-tx 20554  df-hmeo 20747  df-fil 20838  df-fm 20930  df-flim 20931  df-flf 20932  df-tsms 21118  df-xms 21312  df-ms 21313  df-tms 21314  df-cncf 21887  df-limc 22798  df-dv 22799  df-dvn 22800  df-tayl 23287

This theorem is referenced by:  taylth  23307