Theorem taylthlem1 21837

Description: Lemma for taylth 21839. 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 21839 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 11478	. . . 4 |- ( N e. NN <-> N e. ( 1 ... N ) )
3	1, 2	sylib 196	. . 3 |- ( ph -> N e. ( 1 ... N ) )
4		oveq2 6098	. . . . . . . . . . . 12 |- ( m = 1 -> ( N - m ) = ( N - 1 ) )
5	4	fveq2d 5694	. . . . . . . . . . 11 |- ( m = 1 -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - 1 ) ) )
6	5	fveq1d 5692	. . . . . . . . . 10 |- ( m = 1 -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) )
7	4	fveq2d 5694	. . . . . . . . . . 11 |- ( m = 1 -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - 1 ) ) )
8	7	fveq1d 5692	. . . . . . . . . 10 |- ( m = 1 -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) )
9	6, 8	oveq12d 6108	. . . . . . . . 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 6098	. . . . . . . . 9 |- ( m = 1 -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ 1 ) )
11	9, 10	oveq12d 6108	. . . . . . . 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 4378	. . . . . . 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 6105	. . . . . 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 2509	. . . . 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 6098	. . . . . . . . . . . . 13 |- ( m = n -> ( N - m ) = ( N - n ) )
17	16	fveq2d 5694	. . . . . . . . . . . 12 |- ( m = n -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - n ) ) )
18	17	fveq1d 5692	. . . . . . . . . . 11 |- ( m = n -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - n ) ) ` x ) )
19	16	fveq2d 5694	. . . . . . . . . . . 12 |- ( m = n -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - n ) ) )
20	19	fveq1d 5692	. . . . . . . . . . 11 |- ( m = n -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - n ) ) ` x ) )
21	18, 20	oveq12d 6108	. . . . . . . . . 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 6098	. . . . . . . . . 10 |- ( m = n -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ n ) )
23	21, 22	oveq12d 6108	. . . . . . . . 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 4378	. . . . . . . 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 5690	. . . . . . . . . . 11 |- ( x = y -> ( ( ( S Dn F ) ` ( N - n ) ) ` x ) = ( ( ( S Dn F ) ` ( N - n ) ) ` y ) )
26		fveq2 5690	. . . . . . . . . . 11 |- ( x = y -> ( ( ( CC Dn T ) ` ( N - n ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - n ) ) ` y ) )
27	25, 26	oveq12d 6108	. . . . . . . . . 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 6097	. . . . . . . . . . 11 |- ( x = y -> ( x - B ) = ( y - B ) )
29	28	oveq1d 6105	. . . . . . . . . 10 |- ( x = y -> ( ( x - B ) ^ n ) = ( ( y - B ) ^ n ) )
30	27, 29	oveq12d 6108	. . . . . . . . 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 4382	. . . . . . . 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 2490	. . . . . . 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 6105	. . . . . 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 2509	. . . . 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 6098	. . . . . . . . . . . 12 |- ( m = ( n + 1 ) -> ( N - m ) = ( N - ( n + 1 ) ) )
37	36	fveq2d 5694	. . . . . . . . . . 11 |- ( m = ( n + 1 ) -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) )
38	37	fveq1d 5692	. . . . . . . . . 10 |- ( m = ( n + 1 ) -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) ` x ) )
39	36	fveq2d 5694	. . . . . . . . . . 11 |- ( m = ( n + 1 ) -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) )
40	39	fveq1d 5692	. . . . . . . . . 10 |- ( m = ( n + 1 ) -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) ` x ) )
41	38, 40	oveq12d 6108	. . . . . . . . 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 6098	. . . . . . . . 9 |- ( m = ( n + 1 ) -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ ( n + 1 ) ) )
43	41, 42	oveq12d 6108	. . . . . . . 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 4378	. . . . . . 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 6105	. . . . . 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 2509	. . . . 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 6098	. . . . . . . . . . . 12 |- ( m = N -> ( N - m ) = ( N - N ) )
49	48	fveq2d 5694	. . . . . . . . . . 11 |- ( m = N -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - N ) ) )
50	49	fveq1d 5692	. . . . . . . . . 10 |- ( m = N -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - N ) ) ` x ) )
51	48	fveq2d 5694	. . . . . . . . . . 11 |- ( m = N -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - N ) ) )
52	51	fveq1d 5692	. . . . . . . . . 10 |- ( m = N -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) )
53	50, 52	oveq12d 6108	. . . . . . . . 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 6098	. . . . . . . . 9 |- ( m = N -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ N ) )
55	53, 54	oveq12d 6108	. . . . . . . 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 4378	. . . . . . 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 6105	. . . . . 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 2509	. . . . 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 5690	. . . . . . . . . . . . . 14 |- ( y = B -> ( ( ( S Dn F ) ` N ) ` y ) = ( ( ( S Dn F ) ` N ) ` B ) )
62		fveq2 5690	. . . . . . . . . . . . . 14 |- ( y = B -> ( ( ( CC Dn T ) ` N ) ` y ) = ( ( ( CC Dn T ) ` N ) ` B ) )
63	61, 62	oveq12d 6108	. . . . . . . . . . . . 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 2442	. . . . . . . . . . . . 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 6115	. . . . . . . . . . . . 13 |- ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( CC Dn T ) ` N ) ` B ) ) e. _V
66	63, 64, 65	fvmpt 5773	. . . . . . . . . . . 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 10635	. . . . . . . . . . . . . . 15 |- ( ph -> N e. NN0 )
72		nn0uz 10894	. . . . . . . . . . . . . . 15 |- NN0 = ( ZZ>= ` 0 )
73	71, 72	syl6eleq 2532	. . . . . . . . . . . . . 14 |- ( ph -> N e. ( ZZ>= ` 0 ) )
74		eluzfz2b 11459	. . . . . . . . . . . . . 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 2519	. . . . . . . . . . . . 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 21836	. . . . . . . . . . . 12 |- ( ph -> ( ( ( CC Dn T ) ` N ) ` B ) = ( ( ( S Dn F ) ` N ) ` B ) )
80	79	oveq2d 6106	. . . . . . . . . . 11 |- ( ph -> ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( CC Dn T ) ` N ) ` B ) ) = ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( S Dn F ) ` N ) ` B ) ) )
81		cnex 9362	. . . . . . . . . . . . . . . 16 |- CC e. _V
82	81	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> CC e. _V )
83		elpm2r 7229	. . . . . . . . . . . . . . 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 1219	. . . . . . . . . . . . . 14 |- ( ph -> F e. ( CC ^pm S ) )
85		dvnf 21400	. . . . . . . . . . . . . 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 1218	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` N ) : dom ( ( S Dn F ) ` N ) --> CC )
87	86, 77	ffvelrnd 5843	. . . . . . . . . . . 12 |- ( ph -> ( ( ( S Dn F ) ` N ) ` B ) e. CC )
88	87	subidd 9706	. . . . . . . . . . 11 |- ( ph -> ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( S Dn F ) ` N ) ` B ) ) = 0 )
89	67, 80, 88	3eqtrd 2478	. . . . . . . . . 10 |- ( ph -> ( ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) ` B ) = 0 )
90		funmpt 5453	. . . . . . . . . . 11 |- Fun ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) )
91		ovex 6115	. . . . . . . . . . . . 13 |- ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) e. _V
92	91, 64	dmmpti 5539	. . . . . . . . . . . 12 |- dom ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) = A
93	60, 92	syl6eleqr 2533	. . . . . . . . . . 11 |- ( ph -> B e. dom ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) )
94		funbrfvb 5733	. . . . . . . . . . 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 663	. . . . . . . . . 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 10620	. . . . . . . . . . . . . . 15 |- ( N e. NN -> ( N - 1 ) e. NN0 )
98	1, 97	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> ( N - 1 ) e. NN0 )
99		dvnf 21400	. . . . . . . . . . . . . 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 1218	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) : dom ( ( S Dn F ) ` ( N - 1 ) ) --> CC )
101		dvnbss 21401	. . . . . . . . . . . . . . . . 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 1218	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( ( S Dn F ) ` ( N - 1 ) ) C_ dom F )
103		fdm 5562	. . . . . . . . . . . . . . . . 17 |- ( F : A --> CC -> dom F = A )
104	69, 103	syl 16	. . . . . . . . . . . . . . . 16 |- ( ph -> dom F = A )
105	102, 104	sseqtrd 3391	. . . . . . . . . . . . . . 15 |- ( ph -> dom ( ( S Dn F ) ` ( N - 1 ) ) C_ A )
106		fzo0end 11618	. . . . . . . . . . . . . . . . . 18 |- ( N e. NN -> ( N - 1 ) e. ( 0..^ N ) )
107		elfzofz 11566	. . . . . . . . . . . . . . . . . 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 21403	. . . . . . . . . . . . . . . . 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 1218	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( ( S Dn F ) ` N ) C_ dom ( ( S Dn F ) ` ( N - 1 ) ) )
111	76, 110	eqsstr3d 3390	. . . . . . . . . . . . . . 15 |- ( ph -> A C_ dom ( ( S Dn F ) ` ( N - 1 ) ) )
112	105, 111	eqssd 3372	. . . . . . . . . . . . . 14 |- ( ph -> dom ( ( S Dn F ) ` ( N - 1 ) ) = A )
113	112	feq2d 5546	. . . . . . . . . . . . 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 5842	. . . . . . . . . . 11 |- ( ( ph /\ y e. A ) -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) e. CC )
116	76	feq2d 5546	. . . . . . . . . . . . 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 5842	. . . . . . . . . . 11 |- ( ( ph /\ y e. A ) -> ( ( ( S Dn F ) ` N ) ` y ) e. CC )
119	1	nncnd 10337	. . . . . . . . . . . . . . 15 |- ( ph -> N e. CC )
120		1cnd 9401	. . . . . . . . . . . . . . 15 |- ( ph -> 1 e. CC )
121	119, 120	npcand 9722	. . . . . . . . . . . . . 14 |- ( ph -> ( ( N - 1 ) + 1 ) = N )
122	121	fveq2d 5694	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` ( ( N - 1 ) + 1 ) ) = ( ( S Dn F ) ` N ) )
123		recnprss 21378	. . . . . . . . . . . . . . 15 |- ( S e. { RR , CC } -> S C_ CC )
124	68, 123	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> S C_ CC )
125		dvnp1 21398	. . . . . . . . . . . . . 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 1218	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` ( ( N - 1 ) + 1 ) ) = ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) )
127	122, 126	eqtr3d 2476	. . . . . . . . . . . 12 |- ( ph -> ( ( S Dn F ) ` N ) = ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) )
128	117	feqmptd 5743	. . . . . . . . . . . 12 |- ( ph -> ( ( S Dn F ) ` N ) = ( y e. A |-> ( ( ( S Dn F ) ` N ) ` y ) ) )
129	114	feqmptd 5743	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) = ( y e. A |-> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) ) )
130	129	oveq2d 6106	. . . . . . . . . . . 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 2483	. . . . . . . . . . 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 3365	. . . . . . . . . . . . 13 |- ( ph -> A C_ CC )
133	132	sselda 3355	. . . . . . . . . . . 12 |- ( ( ph /\ y e. A ) -> y e. CC )
134		1nn0 10594	. . . . . . . . . . . . . . . 16 |- 1 e. NN0
135	134	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 1 e. NN0 )
136		elpm2r 7229	. . . . . . . . . . . . . . . . . . . 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 1219	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) e. ( CC ^pm S ) )
138		dvn1 21399	. . . . . . . . . . . . . . . . . . 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 661	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) = ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) )
140	126, 122	eqtr3d 2476	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) = ( ( S Dn F ) ` N ) )
141	139, 140	eqtrd 2474	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) = ( ( S Dn F ) ` N ) )
142	141	dmeqd 5041	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) = dom ( ( S Dn F ) ` N ) )
143	77, 142	eleqtrrd 2519	. . . . . . . . . . . . . . 15 |- ( ph -> B e. dom ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) )
144		eqid 2442	. . . . . . . . . . . . . . 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 21830	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 ( S Tayl ( ( S Dn F ) ` ( N - 1 ) ) ) B ) : CC --> CC )
146	120, 119	pncan3d 9721	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 + ( N - 1 ) ) = N )
147	146	oveq1d 6105	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) = ( N ( S Tayl F ) B ) )
148	147, 78	syl6reqr 2493	. . . . . . . . . . . . . . . . . 18 |- ( ph -> T = ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) )
149	148	oveq2d 6106	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( CC Dn T ) = ( CC Dn ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) ) )
150	149	fveq1d 5692	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) = ( ( CC Dn ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) ) ` ( N - 1 ) ) )
151	146	fveq2d 5694	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( S Dn F ) ` ( 1 + ( N - 1 ) ) ) = ( ( S Dn F ) ` N ) )
152	151	dmeqd 5041	. . . . . . . . . . . . . . . . . 18 |- ( ph -> dom ( ( S Dn F ) ` ( 1 + ( N - 1 ) ) ) = dom ( ( S Dn F ) ` N ) )
153	77, 152	eleqtrrd 2519	. . . . . . . . . . . . . . . . 17 |- ( ph -> B e. dom ( ( S Dn F ) ` ( 1 + ( N - 1 ) ) ) )
154	68, 69, 70, 98, 135, 153	dvntaylp 21835	. . . . . . . . . . . . . . . 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 2474	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) = ( 1 ( S Tayl ( ( S Dn F ) ` ( N - 1 ) ) ) B ) )
156	155	feq1d 5545	. . . . . . . . . . . . . 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 5842	. . . . . . . . . . . 12 |- ( ( ph /\ y e. CC ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) e. CC )
159	133, 158	syldan 470	. . . . . . . . . . 11 |- ( ( ph /\ y e. A ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) e. CC )
160		0nn0 10593	. . . . . . . . . . . . . . . 16 |- 0 e. NN0
161	160	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 0 e. NN0 )
162		elpm2r 7229	. . . . . . . . . . . . . . . . . . 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 1219	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( S Dn F ) ` N ) e. ( CC ^pm S ) )
164		dvn0 21397	. . . . . . . . . . . . . . . . . 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 661	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( S Dn ( ( S Dn F ) ` N ) ) ` 0 ) = ( ( S Dn F ) ` N ) )
166	165	dmeqd 5041	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( ( S Dn ( ( S Dn F ) ` N ) ) ` 0 ) = dom ( ( S Dn F ) ` N ) )
167	77, 166	eleqtrrd 2519	. . . . . . . . . . . . . . 15 |- ( ph -> B e. dom ( ( S Dn ( ( S Dn F ) ` N ) ) ` 0 ) )
168		eqid 2442	. . . . . . . . . . . . . . 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 21830	. . . . . . . . . . . . . 14 |- ( ph -> ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) : CC --> CC )
170	119	addid2d 9569	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 0 + N ) = N )
171	170	oveq1d 6105	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( 0 + N ) ( S Tayl F ) B ) = ( N ( S Tayl F ) B ) )
172	171, 78	syl6eqr 2492	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( 0 + N ) ( S Tayl F ) B ) = T )
173	172	oveq2d 6106	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( CC Dn ( ( 0 + N ) ( S Tayl F ) B ) ) = ( CC Dn T ) )
174	173	fveq1d 5692	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( CC Dn ( ( 0 + N ) ( S Tayl F ) B ) ) ` N ) = ( ( CC Dn T ) ` N ) )
175	170	fveq2d 5694	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( S Dn F ) ` ( 0 + N ) ) = ( ( S Dn F ) ` N ) )
176	175	dmeqd 5041	. . . . . . . . . . . . . . . . . 18 |- ( ph -> dom ( ( S Dn F ) ` ( 0 + N ) ) = dom ( ( S Dn F ) ` N ) )
177	77, 176	eleqtrrd 2519	. . . . . . . . . . . . . . . . 17 |- ( ph -> B e. dom ( ( S Dn F ) ` ( 0 + N ) ) )
178	68, 69, 70, 71, 161, 177	dvntaylp 21835	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( CC Dn ( ( 0 + N ) ( S Tayl F ) B ) ) ` N ) = ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) )
179	174, 178	eqtr3d 2476	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` N ) = ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) )
180	179	feq1d 5545	. . . . . . . . . . . . . 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 5842	. . . . . . . . . . . 12 |- ( ( ph /\ y e. CC ) -> ( ( ( CC Dn T ) ` N ) ` y ) e. CC )
183	133, 182	syldan 470	. . . . . . . . . . 11 |- ( ( ph /\ y e. A ) -> ( ( ( CC Dn T ) ` N ) ` y ) e. CC )
184	124	sselda 3355	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. S ) -> y e. CC )
185	184, 158	syldan 470	. . . . . . . . . . . 12 |- ( ( ph /\ y e. S ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) e. CC )
186	184, 182	syldan 470	. . . . . . . . . . . 12 |- ( ( ph /\ y e. S ) -> ( ( ( CC Dn T ) ` N ) ` y ) e. CC )
187		eqid 2442	. . . . . . . . . . . . 13 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
188	187	cnfldtopon 20361	. . . . . . . . . . . . . 14 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
189		toponmax 18532	. . . . . . . . . . . . . 14 |- ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) -> CC e. ( TopOpen ` ℂfld ) )
190	188, 189	mp1i 12	. . . . . . . . . . . . 13 |- ( ph -> CC e. ( TopOpen ` ℂfld ) )
191		df-ss 3341	. . . . . . . . . . . . . 14 |- ( S C_ CC <-> ( S i^i CC ) = S )
192	124, 191	sylib 196	. . . . . . . . . . . . 13 |- ( ph -> ( S i^i CC ) = S )
193		ssid 3374	. . . . . . . . . . . . . . . . 17 |- CC C_ CC
194	193	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> CC C_ CC )
195		mapsspm 7245	. . . . . . . . . . . . . . . . 17 |- ( CC ^m CC ) C_ ( CC ^pm CC )
196	68, 69, 70, 71, 77, 78	taylpf 21830	. . . . . . . . . . . . . . . . . 18 |- ( ph -> T : CC --> CC )
197	81, 81	elmap 7240	. . . . . . . . . . . . . . . . . 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 3353	. . . . . . . . . . . . . . . 16 |- ( ph -> T e. ( CC ^pm CC ) )
200		dvnp1 21398	. . . . . . . . . . . . . . . 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 1218	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` ( ( N - 1 ) + 1 ) ) = ( CC _D ( ( CC Dn T ) ` ( N - 1 ) ) ) )
202	121	fveq2d 5694	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` ( ( N - 1 ) + 1 ) ) = ( ( CC Dn T ) ` N ) )
203	201, 202	eqtr3d 2476	. . . . . . . . . . . . . 14 |- ( ph -> ( CC _D ( ( CC Dn T ) ` ( N - 1 ) ) ) = ( ( CC Dn T ) ` N ) )
204	157	feqmptd 5743	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) = ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) )
205	204	oveq2d 6106	. . . . . . . . . . . . . 14 |- ( ph -> ( CC _D ( ( CC Dn T ) ` ( N - 1 ) ) ) = ( CC _D ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) )
206	181	feqmptd 5743	. . . . . . . . . . . . . 14 |- ( ph -> ( ( CC Dn T ) ` N ) = ( y e. CC |-> ( ( ( CC Dn T ) ` N ) ` y ) ) )
207	203, 205, 206	3eqtr3d 2482	. . . . . . . . . . . . 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 21429	. . . . . . . . . . . 12 |- ( ph -> ( S _D ( y e. S |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) = ( y e. S |-> ( ( ( CC Dn T ) ` N ) ` y ) ) )
209		eqid 2442	. . . . . . . . . . . 12 |- ( ( TopOpen ` ℂfld ) ↾t S ) = ( ( TopOpen ` ℂfld ) ↾t S )
210		resttopon 18764	. . . . . . . . . . . . . . . 16 |- ( ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) /\ S C_ CC ) -> ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) )
211	188, 124, 210	sylancr 663	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) )
212		topontop 18530	. . . . . . . . . . . . . . 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 18531	. . . . . . . . . . . . . . . 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 3391	. . . . . . . . . . . . . 14 |- ( ph -> A C_ U. ( ( TopOpen ` ℂfld ) ↾t S ) )
217		eqid 2442	. . . . . . . . . . . . . . 15 |- U. ( ( TopOpen ` ℂfld ) ↾t S ) = U. ( ( TopOpen ` ℂfld ) ↾t S )
218	217	ntrss2 18660	. . . . . . . . . . . . . 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 661	. . . . . . . . . . . . 13 |- ( ph -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` A ) C_ A )
220	140	dmeqd 5041	. . . . . . . . . . . . . . 15 |- ( ph -> dom ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) = dom ( ( S Dn F ) ` N ) )
221	220, 76	eqtrd 2474	. . . . . . . . . . . . . 14 |- ( ph -> dom ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) = A )
222	124, 114, 70, 209, 187	dvbssntr 21374	. . . . . . . . . . . . . 14 |- ( ph -> dom ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` A ) )
223	221, 222	eqsstr3d 3390	. . . . . . . . . . . . 13 |- ( ph -> A C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` A ) )
224	219, 223	eqssd 3372	. . . . . . . . . . . 12 |- ( ph -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` A ) = A )
225	68, 185, 186, 208, 70, 209, 187, 224	dvmptres2 21435	. . . . . . . . . . 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 21440	. . . . . . . . . 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 4302	. . . . . . . . 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 2442	. . . . . . . . 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 9718	. . . . . . . . . 10 |- ( ( ph /\ y e. A ) -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) e. CC )
231		eqid 2442	. . . . . . . . . 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 5866	. . . . . . . . 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 21372	. . . . . . . 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 463	. . . . . 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 3477	. . . . . . . . . 10 |- ( x e. ( A \ { B } ) -> x e. A )
237		fveq2 5690	. . . . . . . . . . . . . 14 |- ( y = x -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) )
238		fveq2 5690	. . . . . . . . . . . . . 14 |- ( y = x -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) = ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) )
239	237, 238	oveq12d 6108	. . . . . . . . . . . . 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 6115	. . . . . . . . . . . . 13 |- ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) e. _V
241	239, 231, 240	fvmpt 5773	. . . . . . . . . . . 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 5690	. . . . . . . . . . . . . . . 16 |- ( y = B -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) )
243		fveq2 5690	. . . . . . . . . . . . . . . 16 |- ( y = B -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) = ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) )
244	242, 243	oveq12d 6108	. . . . . . . . . . . . . . 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 6115	. . . . . . . . . . . . . . 15 |- ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) ) e. _V
246	244, 231, 245	fvmpt 5773	. . . . . . . . . . . . . 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 21836	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) )
249	248	oveq2d 6106	. . . . . . . . . . . . 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 5843	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) e. CC )
251	250	subidd 9706	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) - ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) ) = 0 )
252	247, 249, 251	3eqtrd 2478	. . . . . . . . . . . 12 |- ( ph -> ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` B ) = 0 )
253	241, 252	oveqan12rd 6110	. . . . . . . . . . 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 5842	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) e. CC )
255	132	sselda 3355	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. A ) -> x e. CC )
256	157	ffvelrnda 5842	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. CC ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) e. CC )
257	255, 256	syldan 470	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) e. CC )
258	254, 257	subcld 9718	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) e. CC )
259	258	subid1d 9707	. . . . . . . . . . 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 2475	. . . . . . . . . 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 474	. . . . . . . . 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 3493	. . . . . . . . . . . 12 |- ( ph -> ( A \ { B } ) C_ CC )
263	262	sselda 3355	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( A \ { B } ) ) -> x e. CC )
264	132, 60	sseldd 3356	. . . . . . . . . . . 12 |- ( ph -> B e. CC )
265	264	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( A \ { B } ) ) -> B e. CC )
266	263, 265	subcld 9718	. . . . . . . . . 10 |- ( ( ph /\ x e. ( A \ { B } ) ) -> ( x - B ) e. CC )
267	266	exp1d 12002	. . . . . . . . 9 |- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( x - B ) ^ 1 ) = ( x - B ) )
268	261, 267	oveq12d 6108	. . . . . . . 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 4377	. . . . . . 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 6105	. . . . . 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 2519	. . . . 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 615	. . . . . 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 11636	. . 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 9706	. . . . . . . . . 10 |- ( ph -> ( N - N ) = 0 )
280	279	fveq2d 5694	. . . . . . . . 9 |- ( ph -> ( ( S Dn F ) ` ( N - N ) ) = ( ( S Dn F ) ` 0 ) )
281		dvn0 21397	. . . . . . . . . 10 |- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = F )
282	124, 84, 281	syl2anc 661	. . . . . . . . 9 |- ( ph -> ( ( S Dn F ) ` 0 ) = F )
283	280, 282	eqtrd 2474	. . . . . . . 8 |- ( ph -> ( ( S Dn F ) ` ( N - N ) ) = F )
284	283	fveq1d 5692	. . . . . . 7 |- ( ph -> ( ( ( S Dn F ) ` ( N - N ) ) ` x ) = ( F ` x ) )
285	279	fveq2d 5694	. . . . . . . . 9 |- ( ph -> ( ( CC Dn T ) ` ( N - N ) ) = ( ( CC Dn T ) ` 0 ) )
286		dvn0 21397	. . . . . . . . . 10 |- ( ( CC C_ CC /\ T e. ( CC ^pm CC ) ) -> ( ( CC Dn T ) ` 0 ) = T )
287	193, 199, 286	sylancr 663	. . . . . . . . 9 |- ( ph -> ( ( CC Dn T ) ` 0 ) = T )
288	285, 287	eqtrd 2474	. . . . . . . 8 |- ( ph -> ( ( CC Dn T ) ` ( N - N ) ) = T )
289	288	fveq1d 5692	. . . . . . 7 |- ( ph -> ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) = ( T ` x ) )
290	284, 289	oveq12d 6108	. . . . . 6 |- ( ph -> ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) = ( ( F ` x ) - ( T ` x ) ) )
291	290	oveq1d 6105	. . . . 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 4378	. . . 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 2492	. . 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 6105	. 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 2518	1 |- ( ph -> 0 e. ( R lim CC B ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1369   e. wcel 1756   _Vcvv 2971   \ cdif 3324   i^i cin 3326   C_ wss 3327   {csn 3876   {cpr 3878   U.cuni 4090   class class class wbr 4291   e. cmpt 4349   dom cdm 4839   Fun wfun 5411   -->wf 5413   ` cfv 5417  (class class class)co 6090   ^m cmap 7213   ^pm cpm 7214   CCcc 9279   RRcr 9280   0cc0 9281   1c1 9282   + caddc 9284   - cmin 9594   / cdiv 9992   NNcn 10321   NN0cn0 10578   ZZ>=cuz 10860   ...cfz 11436  ..^cfzo 11547   ^cexp 11864   ↾_t crest 14358   TopOpenctopn 14359  ℂ_fldccnfld 17817   Topctop 18497  TopOnctopon 18498   intcnt 18620   lim CC climc 21336   _D cdv 21337   Dncdvn 21338   Tayl ctayl 21817

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4402  ax-sep 4412  ax-nul 4420  ax-pow 4469  ax-pr 4530  ax-un 6371  ax-inf2 7846  ax-cnex 9337  ax-resscn 9338  ax-1cn 9339  ax-icn 9340  ax-addcl 9341  ax-addrcl 9342  ax-mulcl 9343  ax-mulrcl 9344  ax-mulcom 9345  ax-addass 9346  ax-mulass 9347  ax-distr 9348  ax-i2m1 9349  ax-1ne0 9350  ax-1rid 9351  ax-rnegex 9352  ax-rrecex 9353  ax-cnre 9354  ax-pre-lttri 9355  ax-pre-lttrn 9356  ax-pre-ltadd 9357  ax-pre-mulgt0 9358  ax-pre-sup 9359  ax-addf 9360  ax-mulf 9361

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-nel 2608  df-ral 2719  df-rex 2720  df-reu 2721  df-rmo 2722  df-rab 2723  df-v 2973  df-sbc 3186  df-csb 3288  df-dif 3330  df-un 3332  df-in 3334  df-ss 3341  df-pss 3343  df-nul 3637  df-if 3791  df-pw 3861  df-sn 3877  df-pr 3879  df-tp 3881  df-op 3883  df-uni 4091  df-int 4128  df-iun 4172  df-iin 4173  df-br 4292  df-opab 4350  df-mpt 4351  df-tr 4385  df-eprel 4631  df-id 4635  df-po 4640  df-so 4641  df-fr 4678  df-se 4679  df-we 4680  df-ord 4721  df-on 4722  df-lim 4723  df-suc 4724  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-iota 5380  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-isom 5426  df-riota 6051  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-of 6319  df-om 6476  df-1st 6576  df-2nd 6577  df-supp 6690  df-recs 6831  df-rdg 6865  df-1o 6919  df-2o 6920  df-oadd 6923  df-er 7100  df-map 7215  df-pm 7216  df-ixp 7263  df-en 7310  df-dom 7311  df-sdom 7312  df-fin 7313  df-fsupp 7620  df-fi 7660  df-sup 7690  df-oi 7723  df-card 8108  df-cda 8336  df-pnf 9419  df-mnf 9420  df-xr 9421  df-ltxr 9422  df-le 9423  df-sub 9596  df-neg 9597  df-div 9993  df-nn 10322  df-2 10379  df-3 10380  df-4 10381  df-5 10382  df-6 10383  df-7 10384  df-8 10385  df-9 10386  df-10 10387  df-n0 10579  df-z 10646  df-dec 10755  df-uz 10861  df-q 10953  df-rp 10991  df-xneg 11088  df-xadd 11089  df-xmul 11090  df-icc 11306  df-fz 11437  df-fzo 11548  df-seq 11806  df-exp 11865  df-fac 12051  df-hash 12103  df-cj 12587  df-re 12588  df-im 12589  df-sqr 12723  df-abs 12724  df-clim 12965  df-sum 13163  df-struct 14175  df-ndx 14176  df-slot 14177  df-base 14178  df-sets 14179  df-ress 14180  df-plusg 14250  df-mulr 14251  df-starv 14252  df-sca 14253  df-vsca 14254  df-ip 14255  df-tset 14256  df-ple 14257  df-ds 14259  df-unif 14260  df-hom 14261  df-cco 14262  df-rest 14360  df-topn 14361  df-0g 14379  df-gsum 14380  df-topgen 14381  df-pt 14382  df-prds 14385  df-xrs 14439  df-qtop 14444  df-imas 14445  df-xps 14447  df-mre 14523  df-mrc 14524  df-acs 14526  df-mnd 15414  df-submnd 15464  df-grp 15544  df-minusg 15545  df-mulg 15547  df-cntz 15834  df-cmn 16278  df-abl 16279  df-mgp 16591  df-ur 16603  df-rng 16646  df-cring 16647  df-psmet 17808  df-xmet 17809  df-met 17810  df-bl 17811  df-mopn 17812  df-fbas 17813  df-fg 17814  df-cnfld 17818  df-top 18502  df-bases 18504  df-topon 18505  df-topsp 18506  df-cld 18622  df-ntr 18623  df-cls 18624  df-nei 18701  df-lp 18739  df-perf 18740  df-cn 18830  df-cnp 18831  df-haus 18918  df-tx 19134  df-hmeo 19327  df-fil 19418  df-fm 19510  df-flim 19511  df-flf 19512  df-tsms 19696  df-xms 19894  df-ms 19895  df-tms 19896  df-cncf 20453  df-limc 21340  df-dv 21341  df-dvn 21342  df-tayl 21819

This theorem is referenced by:  taylth  21839