Theorem taylthlem1 21722

Description: Lemma for taylth 21724. 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 21724 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 11465	. . . 4 |- ( N e. NN <-> N e. ( 1 ... N ) )
3	1, 2	sylib 196	. . 3 |- ( ph -> N e. ( 1 ... N ) )
4		oveq2 6088	. . . . . . . . . . . 12 |- ( m = 1 -> ( N - m ) = ( N - 1 ) )
5	4	fveq2d 5683	. . . . . . . . . . 11 |- ( m = 1 -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - 1 ) ) )
6	5	fveq1d 5681	. . . . . . . . . 10 |- ( m = 1 -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) )
7	4	fveq2d 5683	. . . . . . . . . . 11 |- ( m = 1 -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - 1 ) ) )
8	7	fveq1d 5681	. . . . . . . . . 10 |- ( m = 1 -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) )
9	6, 8	oveq12d 6098	. . . . . . . . 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 6088	. . . . . . . . 9 |- ( m = 1 -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ 1 ) )
11	9, 10	oveq12d 6098	. . . . . . . 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 4367	. . . . . . 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 6095	. . . . . 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 2500	. . . . 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 316	. . . 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 6088	. . . . . . . . . . . . 13 |- ( m = n -> ( N - m ) = ( N - n ) )
17	16	fveq2d 5683	. . . . . . . . . . . 12 |- ( m = n -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - n ) ) )
18	17	fveq1d 5681	. . . . . . . . . . 11 |- ( m = n -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - n ) ) ` x ) )
19	16	fveq2d 5683	. . . . . . . . . . . 12 |- ( m = n -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - n ) ) )
20	19	fveq1d 5681	. . . . . . . . . . 11 |- ( m = n -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - n ) ) ` x ) )
21	18, 20	oveq12d 6098	. . . . . . . . . 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 6088	. . . . . . . . . 10 |- ( m = n -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ n ) )
23	21, 22	oveq12d 6098	. . . . . . . . 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 4367	. . . . . . . 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 5679	. . . . . . . . . . 11 |- ( x = y -> ( ( ( S Dn F ) ` ( N - n ) ) ` x ) = ( ( ( S Dn F ) ` ( N - n ) ) ` y ) )
26		fveq2 5679	. . . . . . . . . . 11 |- ( x = y -> ( ( ( CC Dn T ) ` ( N - n ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - n ) ) ` y ) )
27	25, 26	oveq12d 6098	. . . . . . . . . 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 6087	. . . . . . . . . . 11 |- ( x = y -> ( x - B ) = ( y - B ) )
29	28	oveq1d 6095	. . . . . . . . . 10 |- ( x = y -> ( ( x - B ) ^ n ) = ( ( y - B ) ^ n ) )
30	27, 29	oveq12d 6098	. . . . . . . . 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 4371	. . . . . . . 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 2481	. . . . . . 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 6095	. . . . . 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 2500	. . . . 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 316	. . . 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 6088	. . . . . . . . . . . 12 |- ( m = ( n + 1 ) -> ( N - m ) = ( N - ( n + 1 ) ) )
37	36	fveq2d 5683	. . . . . . . . . . 11 |- ( m = ( n + 1 ) -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) )
38	37	fveq1d 5681	. . . . . . . . . 10 |- ( m = ( n + 1 ) -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) ` x ) )
39	36	fveq2d 5683	. . . . . . . . . . 11 |- ( m = ( n + 1 ) -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) )
40	39	fveq1d 5681	. . . . . . . . . 10 |- ( m = ( n + 1 ) -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) ` x ) )
41	38, 40	oveq12d 6098	. . . . . . . . 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 6088	. . . . . . . . 9 |- ( m = ( n + 1 ) -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ ( n + 1 ) ) )
43	41, 42	oveq12d 6098	. . . . . . . 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 4367	. . . . . . 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 6095	. . . . . 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 2500	. . . . 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 316	. . . 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 6088	. . . . . . . . . . . 12 |- ( m = N -> ( N - m ) = ( N - N ) )
49	48	fveq2d 5683	. . . . . . . . . . 11 |- ( m = N -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - N ) ) )
50	49	fveq1d 5681	. . . . . . . . . 10 |- ( m = N -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - N ) ) ` x ) )
51	48	fveq2d 5683	. . . . . . . . . . 11 |- ( m = N -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - N ) ) )
52	51	fveq1d 5681	. . . . . . . . . 10 |- ( m = N -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) )
53	50, 52	oveq12d 6098	. . . . . . . . 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 6088	. . . . . . . . 9 |- ( m = N -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ N ) )
55	53, 54	oveq12d 6098	. . . . . . . 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 4367	. . . . . . 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 6095	. . . . . 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 2500	. . . . 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 316	. . . 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 5679	. . . . . . . . . . . . . 14 |- ( y = B -> ( ( ( S Dn F ) ` N ) ` y ) = ( ( ( S Dn F ) ` N ) ` B ) )
62		fveq2 5679	. . . . . . . . . . . . . 14 |- ( y = B -> ( ( ( CC Dn T ) ` N ) ` y ) = ( ( ( CC Dn T ) ` N ) ` B ) )
63	61, 62	oveq12d 6098	. . . . . . . . . . . . 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 2433	. . . . . . . . . . . . 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 6105	. . . . . . . . . . . . 13 |- ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( CC Dn T ) ` N ) ` B ) ) e. _V
66	63, 64, 65	fvmpt 5762	. . . . . . . . . . . 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 16	. . . . . . . . . . 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 10623	. . . . . . . . . . . . . . 15 |- ( ph -> N e. NN0 )
72		nn0uz 10882	. . . . . . . . . . . . . . 15 |- NN0 = ( ZZ>= ` 0 )
73	71, 72	syl6eleq 2523	. . . . . . . . . . . . . 14 |- ( ph -> N e. ( ZZ>= ` 0 ) )
74		eluzfz2b 11446	. . . . . . . . . . . . . 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 2510	. . . . . . . . . . . . 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 21721	. . . . . . . . . . . 12 |- ( ph -> ( ( ( CC Dn T ) ` N ) ` B ) = ( ( ( S Dn F ) ` N ) ` B ) )
80	79	oveq2d 6096	. . . . . . . . . . 11 |- ( ph -> ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( CC Dn T ) ` N ) ` B ) ) = ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( S Dn F ) ` N ) ` B ) ) )
81		cnex 9350	. . . . . . . . . . . . . . . 16 |- CC e. _V
82	81	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> CC e. _V )
83		elpm2r 7218	. . . . . . . . . . . . . . 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 1212	. . . . . . . . . . . . . 14 |- ( ph -> F e. ( CC ^pm S ) )
85		dvnf 21242	. . . . . . . . . . . . . 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 1211	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` N ) : dom ( ( S Dn F ) ` N ) --> CC )
87	86, 77	ffvelrnd 5832	. . . . . . . . . . . 12 |- ( ph -> ( ( ( S Dn F ) ` N ) ` B ) e. CC )
88	87	subidd 9694	. . . . . . . . . . 11 |- ( ph -> ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( S Dn F ) ` N ) ` B ) ) = 0 )
89	67, 80, 88	3eqtrd 2469	. . . . . . . . . 10 |- ( ph -> ( ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) ` B ) = 0 )
90		funmpt 5442	. . . . . . . . . . 11 |- Fun ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) )
91		ovex 6105	. . . . . . . . . . . . 13 |- ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) e. _V
92	91, 64	dmmpti 5528	. . . . . . . . . . . 12 |- dom ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) = A
93	60, 92	syl6eleqr 2524	. . . . . . . . . . 11 |- ( ph -> B e. dom ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) )
94		funbrfvb 5722	. . . . . . . . . . 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 656	. . . . . . . . . 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 10608	. . . . . . . . . . . . . . 15 |- ( N e. NN -> ( N - 1 ) e. NN0 )
98	1, 97	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> ( N - 1 ) e. NN0 )
99		dvnf 21242	. . . . . . . . . . . . . 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 1211	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) : dom ( ( S Dn F ) ` ( N - 1 ) ) --> CC )
101		dvnbss 21243	. . . . . . . . . . . . . . . . 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 1211	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( ( S Dn F ) ` ( N - 1 ) ) C_ dom F )
103		fdm 5551	. . . . . . . . . . . . . . . . 17 |- ( F : A --> CC -> dom F = A )
104	69, 103	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> dom F = A )
105	102, 104	sseqtrd 3380	. . . . . . . . . . . . . . 15 |- ( ph -> dom ( ( S Dn F ) ` ( N - 1 ) ) C_ A )
106		fzo0end 11602	. . . . . . . . . . . . . . . . . 18 |- ( N e. NN -> ( N - 1 ) e. ( 0..^ N ) )
107		elfzofz 11550	. . . . . . . . . . . . . . . . . 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 21245	. . . . . . . . . . . . . . . . 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 1211	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( ( S Dn F ) ` N ) C_ dom ( ( S Dn F ) ` ( N - 1 ) ) )
111	76, 110	eqsstr3d 3379	. . . . . . . . . . . . . . 15 |- ( ph -> A C_ dom ( ( S Dn F ) ` ( N - 1 ) ) )
112	105, 111	eqssd 3361	. . . . . . . . . . . . . 14 |- ( ph -> dom ( ( S Dn F ) ` ( N - 1 ) ) = A )
113	112	feq2d 5535	. . . . . . . . . . . . 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 5831	. . . . . . . . . . 11 |- ( ( ph /\ y e. A ) -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) e. CC )
116	76	feq2d 5535	. . . . . . . . . . . . 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 5831	. . . . . . . . . . 11 |- ( ( ph /\ y e. A ) -> ( ( ( S Dn F ) ` N ) ` y ) e. CC )
119	1	nncnd 10325	. . . . . . . . . . . . . . 15 |- ( ph -> N e. CC )
120		1cnd 9389	. . . . . . . . . . . . . . 15 |- ( ph -> 1 e. CC )
121	119, 120	npcand 9710	. . . . . . . . . . . . . 14 |- ( ph -> ( ( N - 1 ) + 1 ) = N )
122	121	fveq2d 5683	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` ( ( N - 1 ) + 1 ) ) = ( ( S Dn F ) ` N ) )
123		recnprss 21220	. . . . . . . . . . . . . . 15 |- ( S e. { RR , CC } -> S C_ CC )
124	68, 123	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> S C_ CC )
125		dvnp1 21240	. . . . . . . . . . . . . 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 1211	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` ( ( N - 1 ) + 1 ) ) = ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) )
127	122, 126	eqtr3d 2467	. . . . . . . . . . . 12 |- ( ph -> ( ( S Dn F ) ` N ) = ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) )
128	117	feqmptd 5732	. . . . . . . . . . . 12 |- ( ph -> ( ( S Dn F ) ` N ) = ( y e. A |-> ( ( ( S Dn F ) ` N ) ` y ) ) )
129	114	feqmptd 5732	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) = ( y e. A |-> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) ) )
130	129	oveq2d 6096	. . . . . . . . . . . 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 2474	. . . . . . . . . . 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 3354	. . . . . . . . . . . . 13 |- ( ph -> A C_ CC )
133	132	sselda 3344	. . . . . . . . . . . 12 |- ( ( ph /\ y e. A ) -> y e. CC )
134		1nn0 10582	. . . . . . . . . . . . . . . 16 |- 1 e. NN0
135	134	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 1 e. NN0 )
136		elpm2r 7218	. . . . . . . . . . . . . . . . . . . 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 1212	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) e. ( CC ^pm S ) )
138		dvn1 21241	. . . . . . . . . . . . . . . . . . 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 654	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) = ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) )
140	126, 122	eqtr3d 2467	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) = ( ( S Dn F ) ` N ) )
141	139, 140	eqtrd 2465	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) = ( ( S Dn F ) ` N ) )
142	141	dmeqd 5029	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) = dom ( ( S Dn F ) ` N ) )
143	77, 142	eleqtrrd 2510	. . . . . . . . . . . . . . 15 |- ( ph -> B e. dom ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) )
144		eqid 2433	. . . . . . . . . . . . . . 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 21715	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 ( S Tayl ( ( S Dn F ) ` ( N - 1 ) ) ) B ) : CC --> CC )
146	120, 119	pncan3d 9709	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 + ( N - 1 ) ) = N )
147	146	oveq1d 6095	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) = ( N ( S Tayl F ) B ) )
148	147, 78	syl6reqr 2484	. . . . . . . . . . . . . . . . . 18 |- ( ph -> T = ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) )
149	148	oveq2d 6096	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( CC Dn T ) = ( CC Dn ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) ) )
150	149	fveq1d 5681	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) = ( ( CC Dn ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) ) ` ( N - 1 ) ) )
151	146	fveq2d 5683	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( S Dn F ) ` ( 1 + ( N - 1 ) ) ) = ( ( S Dn F ) ` N ) )
152	151	dmeqd 5029	. . . . . . . . . . . . . . . . . 18 |- ( ph -> dom ( ( S Dn F ) ` ( 1 + ( N - 1 ) ) ) = dom ( ( S Dn F ) ` N ) )
153	77, 152	eleqtrrd 2510	. . . . . . . . . . . . . . . . 17 |- ( ph -> B e. dom ( ( S Dn F ) ` ( 1 + ( N - 1 ) ) ) )
154	68, 69, 70, 98, 135, 153	dvntaylp 21720	. . . . . . . . . . . . . . . 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 2465	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) = ( 1 ( S Tayl ( ( S Dn F ) ` ( N - 1 ) ) ) B ) )
156	155	feq1d 5534	. . . . . . . . . . . . . 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 5831	. . . . . . . . . . . 12 |- ( ( ph /\ y e. CC ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) e. CC )
159	133, 158	syldan 467	. . . . . . . . . . 11 |- ( ( ph /\ y e. A ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) e. CC )
160		0nn0 10581	. . . . . . . . . . . . . . . 16 |- 0 e. NN0
161	160	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 0 e. NN0 )
162		elpm2r 7218	. . . . . . . . . . . . . . . . . . 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 1212	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( S Dn F ) ` N ) e. ( CC ^pm S ) )
164		dvn0 21239	. . . . . . . . . . . . . . . . . 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 654	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( S Dn ( ( S Dn F ) ` N ) ) ` 0 ) = ( ( S Dn F ) ` N ) )
166	165	dmeqd 5029	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( ( S Dn ( ( S Dn F ) ` N ) ) ` 0 ) = dom ( ( S Dn F ) ` N ) )
167	77, 166	eleqtrrd 2510	. . . . . . . . . . . . . . 15 |- ( ph -> B e. dom ( ( S Dn ( ( S Dn F ) ` N ) ) ` 0 ) )
168		eqid 2433	. . . . . . . . . . . . . . 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 21715	. . . . . . . . . . . . . 14 |- ( ph -> ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) : CC --> CC )
170	119	addid2d 9557	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 0 + N ) = N )
171	170	oveq1d 6095	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( 0 + N ) ( S Tayl F ) B ) = ( N ( S Tayl F ) B ) )
172	171, 78	syl6eqr 2483	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( 0 + N ) ( S Tayl F ) B ) = T )
173	172	oveq2d 6096	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( CC Dn ( ( 0 + N ) ( S Tayl F ) B ) ) = ( CC Dn T ) )
174	173	fveq1d 5681	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( CC Dn ( ( 0 + N ) ( S Tayl F ) B ) ) ` N ) = ( ( CC Dn T ) ` N ) )
175	170	fveq2d 5683	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( S Dn F ) ` ( 0 + N ) ) = ( ( S Dn F ) ` N ) )
176	175	dmeqd 5029	. . . . . . . . . . . . . . . . . 18 |- ( ph -> dom ( ( S Dn F ) ` ( 0 + N ) ) = dom ( ( S Dn F ) ` N ) )
177	77, 176	eleqtrrd 2510	. . . . . . . . . . . . . . . . 17 |- ( ph -> B e. dom ( ( S Dn F ) ` ( 0 + N ) ) )
178	68, 69, 70, 71, 161, 177	dvntaylp 21720	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( CC Dn ( ( 0 + N ) ( S Tayl F ) B ) ) ` N ) = ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) )
179	174, 178	eqtr3d 2467	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` N ) = ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) )
180	179	feq1d 5534	. . . . . . . . . . . . . 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 5831	. . . . . . . . . . . 12 |- ( ( ph /\ y e. CC ) -> ( ( ( CC Dn T ) ` N ) ` y ) e. CC )
183	133, 182	syldan 467	. . . . . . . . . . 11 |- ( ( ph /\ y e. A ) -> ( ( ( CC Dn T ) ` N ) ` y ) e. CC )
184	124	sselda 3344	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. S ) -> y e. CC )
185	184, 158	syldan 467	. . . . . . . . . . . 12 |- ( ( ph /\ y e. S ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) e. CC )
186	184, 182	syldan 467	. . . . . . . . . . . 12 |- ( ( ph /\ y e. S ) -> ( ( ( CC Dn T ) ` N ) ` y ) e. CC )
187		eqid 2433	. . . . . . . . . . . . 13 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
188	187	cnfldtopon 20203	. . . . . . . . . . . . . 14 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
189		toponmax 18374	. . . . . . . . . . . . . 14 |- ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) -> CC e. ( TopOpen ` ℂfld ) )
190	188, 189	mp1i 12	. . . . . . . . . . . . 13 |- ( ph -> CC e. ( TopOpen ` ℂfld ) )
191		df-ss 3330	. . . . . . . . . . . . . 14 |- ( S C_ CC <-> ( S i^i CC ) = S )
192	124, 191	sylib 196	. . . . . . . . . . . . 13 |- ( ph -> ( S i^i CC ) = S )
193		ssid 3363	. . . . . . . . . . . . . . . . 17 |- CC C_ CC
194	193	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> CC C_ CC )
195		mapsspm 7234	. . . . . . . . . . . . . . . . 17 |- ( CC ^m CC ) C_ ( CC ^pm CC )
196	68, 69, 70, 71, 77, 78	taylpf 21715	. . . . . . . . . . . . . . . . . 18 |- ( ph -> T : CC --> CC )
197	81, 81	elmap 7229	. . . . . . . . . . . . . . . . . 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 3342	. . . . . . . . . . . . . . . 16 |- ( ph -> T e. ( CC ^pm CC ) )
200		dvnp1 21240	. . . . . . . . . . . . . . . 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 1211	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` ( ( N - 1 ) + 1 ) ) = ( CC _D ( ( CC Dn T ) ` ( N - 1 ) ) ) )
202	121	fveq2d 5683	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` ( ( N - 1 ) + 1 ) ) = ( ( CC Dn T ) ` N ) )
203	201, 202	eqtr3d 2467	. . . . . . . . . . . . . 14 |- ( ph -> ( CC _D ( ( CC Dn T ) ` ( N - 1 ) ) ) = ( ( CC Dn T ) ` N ) )
204	157	feqmptd 5732	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) = ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) )
205	204	oveq2d 6096	. . . . . . . . . . . . . 14 |- ( ph -> ( CC _D ( ( CC Dn T ) ` ( N - 1 ) ) ) = ( CC _D ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) )
206	181	feqmptd 5732	. . . . . . . . . . . . . 14 |- ( ph -> ( ( CC Dn T ) ` N ) = ( y e. CC |-> ( ( ( CC Dn T ) ` N ) ` y ) ) )
207	203, 205, 206	3eqtr3d 2473	. . . . . . . . . . . . 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 21271	. . . . . . . . . . . 12 |- ( ph -> ( S _D ( y e. S |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) = ( y e. S |-> ( ( ( CC Dn T ) ` N ) ` y ) ) )
209		eqid 2433	. . . . . . . . . . . 12 |- ( ( TopOpen ` ℂfld ) ↾t S ) = ( ( TopOpen ` ℂfld ) ↾t S )
210		resttopon 18606	. . . . . . . . . . . . . . . 16 |- ( ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) /\ S C_ CC ) -> ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) )
211	188, 124, 210	sylancr 656	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) )
212		topontop 18372	. . . . . . . . . . . . . . 15 |- ( ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) -> ( ( TopOpen ` ℂfld ) ↾t S ) e. Top )
213	211, 212	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t S ) e. Top )
214		toponuni 18373	. . . . . . . . . . . . . . . 16 |- ( ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) -> S = U. ( ( TopOpen ` ℂfld ) ↾t S ) )
215	211, 214	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> S = U. ( ( TopOpen ` ℂfld ) ↾t S ) )
216	70, 215	sseqtrd 3380	. . . . . . . . . . . . . 14 |- ( ph -> A C_ U. ( ( TopOpen ` ℂfld ) ↾t S ) )
217		eqid 2433	. . . . . . . . . . . . . . 15 |- U. ( ( TopOpen ` ℂfld ) ↾t S ) = U. ( ( TopOpen ` ℂfld ) ↾t S )
218	217	ntrss2 18502	. . . . . . . . . . . . . 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 654	. . . . . . . . . . . . 13 |- ( ph -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` A ) C_ A )
220	140	dmeqd 5029	. . . . . . . . . . . . . . 15 |- ( ph -> dom ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) = dom ( ( S Dn F ) ` N ) )
221	220, 76	eqtrd 2465	. . . . . . . . . . . . . 14 |- ( ph -> dom ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) = A )
222	124, 114, 70, 209, 187	dvbssntr 21216	. . . . . . . . . . . . . 14 |- ( ph -> dom ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` A ) )
223	221, 222	eqsstr3d 3379	. . . . . . . . . . . . 13 |- ( ph -> A C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` A ) )
224	219, 223	eqssd 3361	. . . . . . . . . . . 12 |- ( ph -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` A ) = A )
225	68, 185, 186, 208, 70, 209, 187, 224	dvmptres2 21277	. . . . . . . . . . 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 21282	. . . . . . . . . 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 4291	. . . . . . . . 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 2433	. . . . . . . . 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 9706	. . . . . . . . . 10 |- ( ( ph /\ y e. A ) -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) e. CC )
231		eqid 2433	. . . . . . . . . 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 5855	. . . . . . . . 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 21214	. . . . . . . 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 460	. . . . . 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 3466	. . . . . . . . . 10 |- ( x e. ( A \ { B } ) -> x e. A )
237		fveq2 5679	. . . . . . . . . . . . . 14 |- ( y = x -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) )
238		fveq2 5679	. . . . . . . . . . . . . 14 |- ( y = x -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) = ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) )
239	237, 238	oveq12d 6098	. . . . . . . . . . . . 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 6105	. . . . . . . . . . . . 13 |- ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) e. _V
241	239, 231, 240	fvmpt 5762	. . . . . . . . . . . 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 5679	. . . . . . . . . . . . . . . 16 |- ( y = B -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) )
243		fveq2 5679	. . . . . . . . . . . . . . . 16 |- ( y = B -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) = ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) )
244	242, 243	oveq12d 6098	. . . . . . . . . . . . . . 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 6105	. . . . . . . . . . . . . . 15 |- ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) ) e. _V
246	244, 231, 245	fvmpt 5762	. . . . . . . . . . . . . 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 16	. . . . . . . . . . . . 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 21721	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) )
249	248	oveq2d 6096	. . . . . . . . . . . . 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 5832	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) e. CC )
251	250	subidd 9694	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) - ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) ) = 0 )
252	247, 249, 251	3eqtrd 2469	. . . . . . . . . . . 12 |- ( ph -> ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` B ) = 0 )
253	241, 252	oveqan12rd 6100	. . . . . . . . . . 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 5831	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) e. CC )
255	132	sselda 3344	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. A ) -> x e. CC )
256	157	ffvelrnda 5831	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. CC ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) e. CC )
257	255, 256	syldan 467	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) e. CC )
258	254, 257	subcld 9706	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) e. CC )
259	258	subid1d 9695	. . . . . . . . . . 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 2466	. . . . . . . . . 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 471	. . . . . . . . 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 3482	. . . . . . . . . . . 12 |- ( ph -> ( A \ { B } ) C_ CC )
263	262	sselda 3344	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( A \ { B } ) ) -> x e. CC )
264	132, 60	sseldd 3345	. . . . . . . . . . . 12 |- ( ph -> B e. CC )
265	264	adantr 462	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( A \ { B } ) ) -> B e. CC )
266	263, 265	subcld 9706	. . . . . . . . . 10 |- ( ( ph /\ x e. ( A \ { B } ) ) -> ( x - B ) e. CC )
267	266	exp1d 11986	. . . . . . . . 9 |- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( x - B ) ^ 1 ) = ( x - B ) )
268	261, 267	oveq12d 6098	. . . . . . . 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 4366	. . . . . . 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 6095	. . . . . 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 2510	. . . . 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 610	. . . . . 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 435	. . . . 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 11620	. . 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 36	. 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 9694	. . . . . . . . . 10 |- ( ph -> ( N - N ) = 0 )
280	279	fveq2d 5683	. . . . . . . . 9 |- ( ph -> ( ( S Dn F ) ` ( N - N ) ) = ( ( S Dn F ) ` 0 ) )
281		dvn0 21239	. . . . . . . . . 10 |- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = F )
282	124, 84, 281	syl2anc 654	. . . . . . . . 9 |- ( ph -> ( ( S Dn F ) ` 0 ) = F )
283	280, 282	eqtrd 2465	. . . . . . . 8 |- ( ph -> ( ( S Dn F ) ` ( N - N ) ) = F )
284	283	fveq1d 5681	. . . . . . 7 |- ( ph -> ( ( ( S Dn F ) ` ( N - N ) ) ` x ) = ( F ` x ) )
285	279	fveq2d 5683	. . . . . . . . 9 |- ( ph -> ( ( CC Dn T ) ` ( N - N ) ) = ( ( CC Dn T ) ` 0 ) )
286		dvn0 21239	. . . . . . . . . 10 |- ( ( CC C_ CC /\ T e. ( CC ^pm CC ) ) -> ( ( CC Dn T ) ` 0 ) = T )
287	193, 199, 286	sylancr 656	. . . . . . . . 9 |- ( ph -> ( ( CC Dn T ) ` 0 ) = T )
288	285, 287	eqtrd 2465	. . . . . . . 8 |- ( ph -> ( ( CC Dn T ) ` ( N - N ) ) = T )
289	288	fveq1d 5681	. . . . . . 7 |- ( ph -> ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) = ( T ` x ) )
290	284, 289	oveq12d 6098	. . . . . 6 |- ( ph -> ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) = ( ( F ` x ) - ( T ` x ) ) )
291	290	oveq1d 6095	. . . . 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 4367	. . . 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 2483	. . 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 6095	. 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 2509	1 |- ( ph -> 0 e. ( R lim CC B ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1362   e. wcel 1755   _Vcvv 2962   \ cdif 3313   i^i cin 3315   C_ wss 3316   {csn 3865   {cpr 3867   U.cuni 4079   class class class wbr 4280   e. cmpt 4338   dom cdm 4827   Fun wfun 5400   -->wf 5402   ` cfv 5406  (class class class)co 6080   ^m cmap 7202   ^pm cpm 7203   CCcc 9267   RRcr 9268   0cc0 9269   1c1 9270   + caddc 9272   - cmin 9582   / cdiv 9980   NNcn 10309   NN0cn0 10566   ZZ>=cuz 10848   ...cfz 11423  ..^cfzo 11531   ^cexp 11848   ↾_t crest 14341   TopOpenctopn 14342  ℂ_fldccnfld 17661   Topctop 18339  TopOnctopon 18340   intcnt 18462   lim CC climc 21178   _D cdv 21179   Dncdvn 21180   Tayl ctayl 21702

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-rep 4391  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-inf2 7835  ax-cnex 9325  ax-resscn 9326  ax-1cn 9327  ax-icn 9328  ax-addcl 9329  ax-addrcl 9330  ax-mulcl 9331  ax-mulrcl 9332  ax-mulcom 9333  ax-addass 9334  ax-mulass 9335  ax-distr 9336  ax-i2m1 9337  ax-1ne0 9338  ax-1rid 9339  ax-rnegex 9340  ax-rrecex 9341  ax-cnre 9342  ax-pre-lttri 9343  ax-pre-lttrn 9344  ax-pre-ltadd 9345  ax-pre-mulgt0 9346  ax-pre-sup 9347  ax-addf 9348  ax-mulf 9349

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-fal 1368  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-nel 2599  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-int 4117  df-iun 4161  df-iin 4162  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-se 4667  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-isom 5415  df-riota 6039  df-ov 6083  df-oprab 6084  df-mpt2 6085  df-of 6309  df-om 6466  df-1st 6566  df-2nd 6567  df-supp 6680  df-recs 6818  df-rdg 6852  df-1o 6908  df-2o 6909  df-oadd 6912  df-er 7089  df-map 7204  df-pm 7205  df-ixp 7252  df-en 7299  df-dom 7300  df-sdom 7301  df-fin 7302  df-fsupp 7609  df-fi 7649  df-sup 7679  df-oi 7712  df-card 8097  df-cda 8325  df-pnf 9407  df-mnf 9408  df-xr 9409  df-ltxr 9410  df-le 9411  df-sub 9584  df-neg 9585  df-div 9981  df-nn 10310  df-2 10367  df-3 10368  df-4 10369  df-5 10370  df-6 10371  df-7 10372  df-8 10373  df-9 10374  df-10 10375  df-n0 10567  df-z 10634  df-dec 10743  df-uz 10849  df-q 10941  df-rp 10979  df-xneg 11076  df-xadd 11077  df-xmul 11078  df-icc 11294  df-fz 11424  df-fzo 11532  df-seq 11790  df-exp 11849  df-fac 12035  df-hash 12087  df-cj 12571  df-re 12572  df-im 12573  df-sqr 12707  df-abs 12708  df-clim 12949  df-sum 13147  df-struct 14158  df-ndx 14159  df-slot 14160  df-base 14161  df-sets 14162  df-ress 14163  df-plusg 14233  df-mulr 14234  df-starv 14235  df-sca 14236  df-vsca 14237  df-ip 14238  df-tset 14239  df-ple 14240  df-ds 14242  df-unif 14243  df-hom 14244  df-cco 14245  df-rest 14343  df-topn 14344  df-0g 14362  df-gsum 14363  df-topgen 14364  df-pt 14365  df-prds 14368  df-xrs 14422  df-qtop 14427  df-imas 14428  df-xps 14430  df-mre 14506  df-mrc 14507  df-acs 14509  df-mnd 15397  df-submnd 15447  df-grp 15524  df-minusg 15525  df-mulg 15527  df-cntz 15814  df-cmn 16258  df-abl 16259  df-mgp 16565  df-rng 16579  df-cring 16580  df-ur 16581  df-psmet 17652  df-xmet 17653  df-met 17654  df-bl 17655  df-mopn 17656  df-fbas 17657  df-fg 17658  df-cnfld 17662  df-top 18344  df-bases 18346  df-topon 18347  df-topsp 18348  df-cld 18464  df-ntr 18465  df-cls 18466  df-nei 18543  df-lp 18581  df-perf 18582  df-cn 18672  df-cnp 18673  df-haus 18760  df-tx 18976  df-hmeo 19169  df-fil 19260  df-fm 19352  df-flim 19353  df-flf 19354  df-tsms 19538  df-xms 19736  df-ms 19737  df-tms 19738  df-cncf 20295  df-limc 21182  df-dv 21183  df-dvn 21184  df-tayl 21704

This theorem is referenced by:  taylth  21724