Theorem taylthlem1 23407

Description: Lemma for taylth 23409. 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 23409 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 11855	. . . 4 |- ( N e. NN <-> N e. ( 1 ... N ) )
3	1, 2	sylib 201	. . 3 |- ( ph -> N e. ( 1 ... N ) )
4		oveq2 6316	. . . . . . . . . . . 12 |- ( m = 1 -> ( N - m ) = ( N - 1 ) )
5	4	fveq2d 5883	. . . . . . . . . . 11 |- ( m = 1 -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - 1 ) ) )
6	5	fveq1d 5881	. . . . . . . . . 10 |- ( m = 1 -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) )
7	4	fveq2d 5883	. . . . . . . . . . 11 |- ( m = 1 -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - 1 ) ) )
8	7	fveq1d 5881	. . . . . . . . . 10 |- ( m = 1 -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) )
9	6, 8	oveq12d 6326	. . . . . . . . 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 6316	. . . . . . . . 9 |- ( m = 1 -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ 1 ) )
11	9, 10	oveq12d 6326	. . . . . . . 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 4483	. . . . . . 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 6323	. . . . . 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 2534	. . . . 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 323	. . . 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 6316	. . . . . . . . . . . . 13 |- ( m = n -> ( N - m ) = ( N - n ) )
17	16	fveq2d 5883	. . . . . . . . . . . 12 |- ( m = n -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - n ) ) )
18	17	fveq1d 5881	. . . . . . . . . . 11 |- ( m = n -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - n ) ) ` x ) )
19	16	fveq2d 5883	. . . . . . . . . . . 12 |- ( m = n -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - n ) ) )
20	19	fveq1d 5881	. . . . . . . . . . 11 |- ( m = n -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - n ) ) ` x ) )
21	18, 20	oveq12d 6326	. . . . . . . . . 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 6316	. . . . . . . . . 10 |- ( m = n -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ n ) )
23	21, 22	oveq12d 6326	. . . . . . . . 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 4483	. . . . . . . 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 5879	. . . . . . . . . . 11 |- ( x = y -> ( ( ( S Dn F ) ` ( N - n ) ) ` x ) = ( ( ( S Dn F ) ` ( N - n ) ) ` y ) )
26		fveq2 5879	. . . . . . . . . . 11 |- ( x = y -> ( ( ( CC Dn T ) ` ( N - n ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - n ) ) ` y ) )
27	25, 26	oveq12d 6326	. . . . . . . . . 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 6315	. . . . . . . . . . 11 |- ( x = y -> ( x - B ) = ( y - B ) )
29	28	oveq1d 6323	. . . . . . . . . 10 |- ( x = y -> ( ( x - B ) ^ n ) = ( ( y - B ) ^ n ) )
30	27, 29	oveq12d 6326	. . . . . . . . 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 4488	. . . . . . . 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 2521	. . . . . . 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 6323	. . . . . 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 2534	. . . . 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 323	. . . 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 6316	. . . . . . . . . . . 12 |- ( m = ( n + 1 ) -> ( N - m ) = ( N - ( n + 1 ) ) )
37	36	fveq2d 5883	. . . . . . . . . . 11 |- ( m = ( n + 1 ) -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) )
38	37	fveq1d 5881	. . . . . . . . . 10 |- ( m = ( n + 1 ) -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - ( n + 1 ) ) ) ` x ) )
39	36	fveq2d 5883	. . . . . . . . . . 11 |- ( m = ( n + 1 ) -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) )
40	39	fveq1d 5881	. . . . . . . . . 10 |- ( m = ( n + 1 ) -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - ( n + 1 ) ) ) ` x ) )
41	38, 40	oveq12d 6326	. . . . . . . . 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 6316	. . . . . . . . 9 |- ( m = ( n + 1 ) -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ ( n + 1 ) ) )
43	41, 42	oveq12d 6326	. . . . . . . 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 4483	. . . . . . 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 6323	. . . . . 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 2534	. . . . 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 323	. . . 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 6316	. . . . . . . . . . . 12 |- ( m = N -> ( N - m ) = ( N - N ) )
49	48	fveq2d 5883	. . . . . . . . . . 11 |- ( m = N -> ( ( S Dn F ) ` ( N - m ) ) = ( ( S Dn F ) ` ( N - N ) ) )
50	49	fveq1d 5881	. . . . . . . . . 10 |- ( m = N -> ( ( ( S Dn F ) ` ( N - m ) ) ` x ) = ( ( ( S Dn F ) ` ( N - N ) ) ` x ) )
51	48	fveq2d 5883	. . . . . . . . . . 11 |- ( m = N -> ( ( CC Dn T ) ` ( N - m ) ) = ( ( CC Dn T ) ` ( N - N ) ) )
52	51	fveq1d 5881	. . . . . . . . . 10 |- ( m = N -> ( ( ( CC Dn T ) ` ( N - m ) ) ` x ) = ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) )
53	50, 52	oveq12d 6326	. . . . . . . . 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 6316	. . . . . . . . 9 |- ( m = N -> ( ( x - B ) ^ m ) = ( ( x - B ) ^ N ) )
55	53, 54	oveq12d 6326	. . . . . . . 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 4483	. . . . . . 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 6323	. . . . . 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 2534	. . . . 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 323	. . . 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 5879	. . . . . . . . . . . . . 14 |- ( y = B -> ( ( ( S Dn F ) ` N ) ` y ) = ( ( ( S Dn F ) ` N ) ` B ) )
62		fveq2 5879	. . . . . . . . . . . . . 14 |- ( y = B -> ( ( ( CC Dn T ) ` N ) ` y ) = ( ( ( CC Dn T ) ` N ) ` B ) )
63	61, 62	oveq12d 6326	. . . . . . . . . . . . 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 2471	. . . . . . . . . . . . 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 6336	. . . . . . . . . . . . 13 |- ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( CC Dn T ) ` N ) ` B ) ) e. _V
66	63, 64, 65	fvmpt 5963	. . . . . . . . . . . 12 |- ( B e. A -> ( ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) ` B ) = ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( CC Dn T ) ` N ) ` B ) ) )
67	60, 66	syl 17	. . . . . . . . . . 11 |- ( ph -> ( ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) ` B ) = ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( CC Dn T ) ` N ) ` B ) ) )
68		taylthlem1.s	. . . . . . . . . . . . 13 |- ( ph -> S e. { RR , CC } )
69		taylthlem1.f	. . . . . . . . . . . . 13 |- ( ph -> F : A --> CC )
70		taylthlem1.a	. . . . . . . . . . . . 13 |- ( ph -> A C_ S )
71	1	nnnn0d 10949	. . . . . . . . . . . . . . 15 |- ( ph -> N e. NN0 )
72		nn0uz 11217	. . . . . . . . . . . . . . 15 |- NN0 = ( ZZ>= ` 0 )
73	71, 72	syl6eleq 2559	. . . . . . . . . . . . . 14 |- ( ph -> N e. ( ZZ>= ` 0 ) )
74		eluzfz2b 11834	. . . . . . . . . . . . . 14 |- ( N e. ( ZZ>= ` 0 ) <-> N e. ( 0 ... N ) )
75	73, 74	sylib 201	. . . . . . . . . . . . 13 |- ( ph -> N e. ( 0 ... N ) )
76		taylthlem1.d	. . . . . . . . . . . . . 14 |- ( ph -> dom ( ( S Dn F ) ` N ) = A )
77	60, 76	eleqtrrd 2552	. . . . . . . . . . . . 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 23406	. . . . . . . . . . . 12 |- ( ph -> ( ( ( CC Dn T ) ` N ) ` B ) = ( ( ( S Dn F ) ` N ) ` B ) )
80	79	oveq2d 6324	. . . . . . . . . . 11 |- ( ph -> ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( CC Dn T ) ` N ) ` B ) ) = ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( S Dn F ) ` N ) ` B ) ) )
81		cnex 9638	. . . . . . . . . . . . . . . 16 |- CC e. _V
82	81	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> CC e. _V )
83		elpm2r 7507	. . . . . . . . . . . . . . 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 1293	. . . . . . . . . . . . . 14 |- ( ph -> F e. ( CC ^pm S ) )
85		dvnf 22960	. . . . . . . . . . . . . 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 1292	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` N ) : dom ( ( S Dn F ) ` N ) --> CC )
87	86, 77	ffvelrnd 6038	. . . . . . . . . . . 12 |- ( ph -> ( ( ( S Dn F ) ` N ) ` B ) e. CC )
88	87	subidd 9993	. . . . . . . . . . 11 |- ( ph -> ( ( ( ( S Dn F ) ` N ) ` B ) - ( ( ( S Dn F ) ` N ) ` B ) ) = 0 )
89	67, 80, 88	3eqtrd 2509	. . . . . . . . . 10 |- ( ph -> ( ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) ` B ) = 0 )
90		funmpt 5625	. . . . . . . . . . 11 |- Fun ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) )
91		ovex 6336	. . . . . . . . . . . . 13 |- ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) e. _V
92	91, 64	dmmpti 5717	. . . . . . . . . . . 12 |- dom ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) = A
93	60, 92	syl6eleqr 2560	. . . . . . . . . . 11 |- ( ph -> B e. dom ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) )
94		funbrfvb 5921	. . . . . . . . . . 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 676	. . . . . . . . . 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 215	. . . . . . . . 9 |- ( ph -> B ( y e. A |-> ( ( ( ( S Dn F ) ` N ) ` y ) - ( ( ( CC Dn T ) ` N ) ` y ) ) ) 0 )
97		nnm1nn0 10935	. . . . . . . . . . . . . . 15 |- ( N e. NN -> ( N - 1 ) e. NN0 )
98	1, 97	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> ( N - 1 ) e. NN0 )
99		dvnf 22960	. . . . . . . . . . . . . 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 1292	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) : dom ( ( S Dn F ) ` ( N - 1 ) ) --> CC )
101		dvnbss 22961	. . . . . . . . . . . . . . . . 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 1292	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( ( S Dn F ) ` ( N - 1 ) ) C_ dom F )
103		fdm 5745	. . . . . . . . . . . . . . . . 17 |- ( F : A --> CC -> dom F = A )
104	69, 103	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> dom F = A )
105	102, 104	sseqtrd 3454	. . . . . . . . . . . . . . 15 |- ( ph -> dom ( ( S Dn F ) ` ( N - 1 ) ) C_ A )
106		fzo0end 12032	. . . . . . . . . . . . . . . . . 18 |- ( N e. NN -> ( N - 1 ) e. ( 0..^ N ) )
107		elfzofz 11962	. . . . . . . . . . . . . . . . . 18 |- ( ( N - 1 ) e. ( 0..^ N ) -> ( N - 1 ) e. ( 0 ... N ) )
108	1, 106, 107	3syl 18	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( N - 1 ) e. ( 0 ... N ) )
109		dvn2bss 22963	. . . . . . . . . . . . . . . . 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 1292	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( ( S Dn F ) ` N ) C_ dom ( ( S Dn F ) ` ( N - 1 ) ) )
111	76, 110	eqsstr3d 3453	. . . . . . . . . . . . . . 15 |- ( ph -> A C_ dom ( ( S Dn F ) ` ( N - 1 ) ) )
112	105, 111	eqssd 3435	. . . . . . . . . . . . . 14 |- ( ph -> dom ( ( S Dn F ) ` ( N - 1 ) ) = A )
113	112	feq2d 5725	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( S Dn F ) ` ( N - 1 ) ) : dom ( ( S Dn F ) ` ( N - 1 ) ) --> CC <-> ( ( S Dn F ) ` ( N - 1 ) ) : A --> CC ) )
114	100, 113	mpbid 215	. . . . . . . . . . . 12 |- ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) : A --> CC )
115	114	ffvelrnda 6037	. . . . . . . . . . 11 |- ( ( ph /\ y e. A ) -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) e. CC )
116	76	feq2d 5725	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( S Dn F ) ` N ) : dom ( ( S Dn F ) ` N ) --> CC <-> ( ( S Dn F ) ` N ) : A --> CC ) )
117	86, 116	mpbid 215	. . . . . . . . . . . 12 |- ( ph -> ( ( S Dn F ) ` N ) : A --> CC )
118	117	ffvelrnda 6037	. . . . . . . . . . 11 |- ( ( ph /\ y e. A ) -> ( ( ( S Dn F ) ` N ) ` y ) e. CC )
119	1	nncnd 10647	. . . . . . . . . . . . . . 15 |- ( ph -> N e. CC )
120		1cnd 9677	. . . . . . . . . . . . . . 15 |- ( ph -> 1 e. CC )
121	119, 120	npcand 10009	. . . . . . . . . . . . . 14 |- ( ph -> ( ( N - 1 ) + 1 ) = N )
122	121	fveq2d 5883	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` ( ( N - 1 ) + 1 ) ) = ( ( S Dn F ) ` N ) )
123		recnprss 22938	. . . . . . . . . . . . . . 15 |- ( S e. { RR , CC } -> S C_ CC )
124	68, 123	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> S C_ CC )
125		dvnp1 22958	. . . . . . . . . . . . . 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 1292	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` ( ( N - 1 ) + 1 ) ) = ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) )
127	122, 126	eqtr3d 2507	. . . . . . . . . . . 12 |- ( ph -> ( ( S Dn F ) ` N ) = ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) )
128	117	feqmptd 5932	. . . . . . . . . . . 12 |- ( ph -> ( ( S Dn F ) ` N ) = ( y e. A |-> ( ( ( S Dn F ) ` N ) ` y ) ) )
129	114	feqmptd 5932	. . . . . . . . . . . . 13 |- ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) = ( y e. A |-> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) ) )
130	129	oveq2d 6324	. . . . . . . . . . . 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 2514	. . . . . . . . . . 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 3428	. . . . . . . . . . . . 13 |- ( ph -> A C_ CC )
133	132	sselda 3418	. . . . . . . . . . . 12 |- ( ( ph /\ y e. A ) -> y e. CC )
134		1nn0 10909	. . . . . . . . . . . . . . . 16 |- 1 e. NN0
135	134	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 1 e. NN0 )
136		elpm2r 7507	. . . . . . . . . . . . . . . . . . . 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 1293	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( S Dn F ) ` ( N - 1 ) ) e. ( CC ^pm S ) )
138		dvn1 22959	. . . . . . . . . . . . . . . . . . 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 673	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) = ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) )
140	126, 122	eqtr3d 2507	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) = ( ( S Dn F ) ` N ) )
141	139, 140	eqtrd 2505	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) = ( ( S Dn F ) ` N ) )
142	141	dmeqd 5042	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) = dom ( ( S Dn F ) ` N ) )
143	77, 142	eleqtrrd 2552	. . . . . . . . . . . . . . 15 |- ( ph -> B e. dom ( ( S Dn ( ( S Dn F ) ` ( N - 1 ) ) ) ` 1 ) )
144		eqid 2471	. . . . . . . . . . . . . . 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 23400	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 ( S Tayl ( ( S Dn F ) ` ( N - 1 ) ) ) B ) : CC --> CC )
146	120, 119	pncan3d 10008	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 + ( N - 1 ) ) = N )
147	146	oveq1d 6323	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) = ( N ( S Tayl F ) B ) )
148	147, 78	syl6reqr 2524	. . . . . . . . . . . . . . . . . 18 |- ( ph -> T = ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) )
149	148	oveq2d 6324	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( CC Dn T ) = ( CC Dn ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) ) )
150	149	fveq1d 5881	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) = ( ( CC Dn ( ( 1 + ( N - 1 ) ) ( S Tayl F ) B ) ) ` ( N - 1 ) ) )
151	146	fveq2d 5883	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( S Dn F ) ` ( 1 + ( N - 1 ) ) ) = ( ( S Dn F ) ` N ) )
152	151	dmeqd 5042	. . . . . . . . . . . . . . . . . 18 |- ( ph -> dom ( ( S Dn F ) ` ( 1 + ( N - 1 ) ) ) = dom ( ( S Dn F ) ` N ) )
153	77, 152	eleqtrrd 2552	. . . . . . . . . . . . . . . . 17 |- ( ph -> B e. dom ( ( S Dn F ) ` ( 1 + ( N - 1 ) ) ) )
154	68, 69, 70, 98, 135, 153	dvntaylp 23405	. . . . . . . . . . . . . . . 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 2505	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) = ( 1 ( S Tayl ( ( S Dn F ) ` ( N - 1 ) ) ) B ) )
156	155	feq1d 5724	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( CC Dn T ) ` ( N - 1 ) ) : CC --> CC <-> ( 1 ( S Tayl ( ( S Dn F ) ` ( N - 1 ) ) ) B ) : CC --> CC ) )
157	145, 156	mpbird 240	. . . . . . . . . . . . 13 |- ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) : CC --> CC )
158	157	ffvelrnda 6037	. . . . . . . . . . . 12 |- ( ( ph /\ y e. CC ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) e. CC )
159	133, 158	syldan 478	. . . . . . . . . . 11 |- ( ( ph /\ y e. A ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) e. CC )
160		0nn0 10908	. . . . . . . . . . . . . . . 16 |- 0 e. NN0
161	160	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> 0 e. NN0 )
162		elpm2r 7507	. . . . . . . . . . . . . . . . . . 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 1293	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( S Dn F ) ` N ) e. ( CC ^pm S ) )
164		dvn0 22957	. . . . . . . . . . . . . . . . . 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 673	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( S Dn ( ( S Dn F ) ` N ) ) ` 0 ) = ( ( S Dn F ) ` N ) )
166	165	dmeqd 5042	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( ( S Dn ( ( S Dn F ) ` N ) ) ` 0 ) = dom ( ( S Dn F ) ` N ) )
167	77, 166	eleqtrrd 2552	. . . . . . . . . . . . . . 15 |- ( ph -> B e. dom ( ( S Dn ( ( S Dn F ) ` N ) ) ` 0 ) )
168		eqid 2471	. . . . . . . . . . . . . . 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 23400	. . . . . . . . . . . . . 14 |- ( ph -> ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) : CC --> CC )
170	119	addid2d 9852	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 0 + N ) = N )
171	170	oveq1d 6323	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( 0 + N ) ( S Tayl F ) B ) = ( N ( S Tayl F ) B ) )
172	171, 78	syl6eqr 2523	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( 0 + N ) ( S Tayl F ) B ) = T )
173	172	oveq2d 6324	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( CC Dn ( ( 0 + N ) ( S Tayl F ) B ) ) = ( CC Dn T ) )
174	173	fveq1d 5881	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( CC Dn ( ( 0 + N ) ( S Tayl F ) B ) ) ` N ) = ( ( CC Dn T ) ` N ) )
175	170	fveq2d 5883	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( S Dn F ) ` ( 0 + N ) ) = ( ( S Dn F ) ` N ) )
176	175	dmeqd 5042	. . . . . . . . . . . . . . . . . 18 |- ( ph -> dom ( ( S Dn F ) ` ( 0 + N ) ) = dom ( ( S Dn F ) ` N ) )
177	77, 176	eleqtrrd 2552	. . . . . . . . . . . . . . . . 17 |- ( ph -> B e. dom ( ( S Dn F ) ` ( 0 + N ) ) )
178	68, 69, 70, 71, 161, 177	dvntaylp 23405	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( CC Dn ( ( 0 + N ) ( S Tayl F ) B ) ) ` N ) = ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) )
179	174, 178	eqtr3d 2507	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` N ) = ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) )
180	179	feq1d 5724	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( CC Dn T ) ` N ) : CC --> CC <-> ( 0 ( S Tayl ( ( S Dn F ) ` N ) ) B ) : CC --> CC ) )
181	169, 180	mpbird 240	. . . . . . . . . . . . 13 |- ( ph -> ( ( CC Dn T ) ` N ) : CC --> CC )
182	181	ffvelrnda 6037	. . . . . . . . . . . 12 |- ( ( ph /\ y e. CC ) -> ( ( ( CC Dn T ) ` N ) ` y ) e. CC )
183	133, 182	syldan 478	. . . . . . . . . . 11 |- ( ( ph /\ y e. A ) -> ( ( ( CC Dn T ) ` N ) ` y ) e. CC )
184	124	sselda 3418	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. S ) -> y e. CC )
185	184, 158	syldan 478	. . . . . . . . . . . 12 |- ( ( ph /\ y e. S ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) e. CC )
186	184, 182	syldan 478	. . . . . . . . . . . 12 |- ( ( ph /\ y e. S ) -> ( ( ( CC Dn T ) ` N ) ` y ) e. CC )
187		eqid 2471	. . . . . . . . . . . . 13 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
188	187	cnfldtopon 21881	. . . . . . . . . . . . . 14 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
189		toponmax 20020	. . . . . . . . . . . . . 14 |- ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) -> CC e. ( TopOpen ` ℂfld ) )
190	188, 189	mp1i 13	. . . . . . . . . . . . 13 |- ( ph -> CC e. ( TopOpen ` ℂfld ) )
191		df-ss 3404	. . . . . . . . . . . . . 14 |- ( S C_ CC <-> ( S i^i CC ) = S )
192	124, 191	sylib 201	. . . . . . . . . . . . 13 |- ( ph -> ( S i^i CC ) = S )
193		ssid 3437	. . . . . . . . . . . . . . . . 17 |- CC C_ CC
194	193	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> CC C_ CC )
195		mapsspm 7523	. . . . . . . . . . . . . . . . 17 |- ( CC ^m CC ) C_ ( CC ^pm CC )
196	68, 69, 70, 71, 77, 78	taylpf 23400	. . . . . . . . . . . . . . . . . 18 |- ( ph -> T : CC --> CC )
197	81, 81	elmap 7518	. . . . . . . . . . . . . . . . . 18 |- ( T e. ( CC ^m CC ) <-> T : CC --> CC )
198	196, 197	sylibr 217	. . . . . . . . . . . . . . . . 17 |- ( ph -> T e. ( CC ^m CC ) )
199	195, 198	sseldi 3416	. . . . . . . . . . . . . . . 16 |- ( ph -> T e. ( CC ^pm CC ) )
200		dvnp1 22958	. . . . . . . . . . . . . . . 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 1292	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` ( ( N - 1 ) + 1 ) ) = ( CC _D ( ( CC Dn T ) ` ( N - 1 ) ) ) )
202	121	fveq2d 5883	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` ( ( N - 1 ) + 1 ) ) = ( ( CC Dn T ) ` N ) )
203	201, 202	eqtr3d 2507	. . . . . . . . . . . . . 14 |- ( ph -> ( CC _D ( ( CC Dn T ) ` ( N - 1 ) ) ) = ( ( CC Dn T ) ` N ) )
204	157	feqmptd 5932	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( CC Dn T ) ` ( N - 1 ) ) = ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) )
205	204	oveq2d 6324	. . . . . . . . . . . . . 14 |- ( ph -> ( CC _D ( ( CC Dn T ) ` ( N - 1 ) ) ) = ( CC _D ( y e. CC |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) )
206	181	feqmptd 5932	. . . . . . . . . . . . . 14 |- ( ph -> ( ( CC Dn T ) ` N ) = ( y e. CC |-> ( ( ( CC Dn T ) ` N ) ` y ) ) )
207	203, 205, 206	3eqtr3d 2513	. . . . . . . . . . . . 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 22989	. . . . . . . . . . . 12 |- ( ph -> ( S _D ( y e. S |-> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) = ( y e. S |-> ( ( ( CC Dn T ) ` N ) ` y ) ) )
209		eqid 2471	. . . . . . . . . . . 12 |- ( ( TopOpen ` ℂfld ) ↾t S ) = ( ( TopOpen ` ℂfld ) ↾t S )
210		resttopon 20254	. . . . . . . . . . . . . . . 16 |- ( ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) /\ S C_ CC ) -> ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) )
211	188, 124, 210	sylancr 676	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) )
212		topontop 20018	. . . . . . . . . . . . . . 15 |- ( ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) -> ( ( TopOpen ` ℂfld ) ↾t S ) e. Top )
213	211, 212	syl 17	. . . . . . . . . . . . . 14 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t S ) e. Top )
214		toponuni 20019	. . . . . . . . . . . . . . . 16 |- ( ( ( TopOpen ` ℂfld ) ↾t S ) e. (TopOn ` S ) -> S = U. ( ( TopOpen ` ℂfld ) ↾t S ) )
215	211, 214	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> S = U. ( ( TopOpen ` ℂfld ) ↾t S ) )
216	70, 215	sseqtrd 3454	. . . . . . . . . . . . . 14 |- ( ph -> A C_ U. ( ( TopOpen ` ℂfld ) ↾t S ) )
217		eqid 2471	. . . . . . . . . . . . . . 15 |- U. ( ( TopOpen ` ℂfld ) ↾t S ) = U. ( ( TopOpen ` ℂfld ) ↾t S )
218	217	ntrss2 20149	. . . . . . . . . . . . . 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 673	. . . . . . . . . . . . 13 |- ( ph -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` A ) C_ A )
220	140	dmeqd 5042	. . . . . . . . . . . . . . 15 |- ( ph -> dom ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) = dom ( ( S Dn F ) ` N ) )
221	220, 76	eqtrd 2505	. . . . . . . . . . . . . 14 |- ( ph -> dom ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) = A )
222	124, 114, 70, 209, 187	dvbssntr 22934	. . . . . . . . . . . . . 14 |- ( ph -> dom ( S _D ( ( S Dn F ) ` ( N - 1 ) ) ) C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` A ) )
223	221, 222	eqsstr3d 3453	. . . . . . . . . . . . 13 |- ( ph -> A C_ ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` A ) )
224	219, 223	eqssd 3435	. . . . . . . . . . . 12 |- ( ph -> ( ( int ` ( ( TopOpen ` ℂfld ) ↾t S ) ) ` A ) = A )
225	68, 185, 186, 208, 70, 209, 187, 224	dvmptres2 22995	. . . . . . . . . . 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 23000	. . . . . . . . . 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 4406	. . . . . . . . 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 240	. . . . . . . 8 |- ( ph -> B ( S _D ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ) 0 )
229		eqid 2471	. . . . . . . . 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 10005	. . . . . . . . . 10 |- ( ( ph /\ y e. A ) -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) e. CC )
231		eqid 2471	. . . . . . . . . 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 6061	. . . . . . . . 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 22932	. . . . . . . 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 215	. . . . . . 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 470	. . . . . 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 3544	. . . . . . . . . 10 |- ( x e. ( A \ { B } ) -> x e. A )
237		fveq2 5879	. . . . . . . . . . . . . 14 |- ( y = x -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) )
238		fveq2 5879	. . . . . . . . . . . . . 14 |- ( y = x -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) = ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) )
239	237, 238	oveq12d 6326	. . . . . . . . . . . . 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 6336	. . . . . . . . . . . . 13 |- ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) e. _V
241	239, 231, 240	fvmpt 5963	. . . . . . . . . . . 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 5879	. . . . . . . . . . . . . . . 16 |- ( y = B -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) )
243		fveq2 5879	. . . . . . . . . . . . . . . 16 |- ( y = B -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) = ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) )
244	242, 243	oveq12d 6326	. . . . . . . . . . . . . . 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 6336	. . . . . . . . . . . . . . 15 |- ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) ) e. _V
246	244, 231, 245	fvmpt 5963	. . . . . . . . . . . . . 14 |- ( B e. A -> ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` B ) = ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) ) )
247	60, 246	syl 17	. . . . . . . . . . . . 13 |- ( ph -> ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` B ) = ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) ) )
248	68, 69, 70, 108, 77, 78	dvntaylp0 23406	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` B ) = ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) )
249	248	oveq2d 6324	. . . . . . . . . . . . 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 6038	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) e. CC )
251	250	subidd 9993	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) - ( ( ( S Dn F ) ` ( N - 1 ) ) ` B ) ) = 0 )
252	247, 249, 251	3eqtrd 2509	. . . . . . . . . . . 12 |- ( ph -> ( ( y e. A |-> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` y ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` y ) ) ) ` B ) = 0 )
253	241, 252	oveqan12rd 6328	. . . . . . . . . . 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 6037	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) e. CC )
255	132	sselda 3418	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. A ) -> x e. CC )
256	157	ffvelrnda 6037	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. CC ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) e. CC )
257	255, 256	syldan 478	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. A ) -> ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) e. CC )
258	254, 257	subcld 10005	. . . . . . . . . . . 12 |- ( ( ph /\ x e. A ) -> ( ( ( ( S Dn F ) ` ( N - 1 ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - 1 ) ) ` x ) ) e. CC )
259	258	subid1d 9994	. . . . . . . . . . 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 2506	. . . . . . . . . 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 482	. . . . . . . . 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 3560	. . . . . . . . . . . 12 |- ( ph -> ( A \ { B } ) C_ CC )
263	262	sselda 3418	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( A \ { B } ) ) -> x e. CC )
264	132, 60	sseldd 3419	. . . . . . . . . . . 12 |- ( ph -> B e. CC )
265	264	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( A \ { B } ) ) -> B e. CC )
266	263, 265	subcld 10005	. . . . . . . . . 10 |- ( ( ph /\ x e. ( A \ { B } ) ) -> ( x - B ) e. CC )
267	266	exp1d 12449	. . . . . . . . 9 |- ( ( ph /\ x e. ( A \ { B } ) ) -> ( ( x - B ) ^ 1 ) = ( x - B ) )
268	261, 267	oveq12d 6326	. . . . . . . 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 4482	. . . . . . 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 6323	. . . . . 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 2552	. . . . 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 626	. . . . . 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 442	. . . . 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 28	. . . 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 12054	. . 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 9993	. . . . . . . . . 10 |- ( ph -> ( N - N ) = 0 )
280	279	fveq2d 5883	. . . . . . . . 9 |- ( ph -> ( ( S Dn F ) ` ( N - N ) ) = ( ( S Dn F ) ` 0 ) )
281		dvn0 22957	. . . . . . . . . 10 |- ( ( S C_ CC /\ F e. ( CC ^pm S ) ) -> ( ( S Dn F ) ` 0 ) = F )
282	124, 84, 281	syl2anc 673	. . . . . . . . 9 |- ( ph -> ( ( S Dn F ) ` 0 ) = F )
283	280, 282	eqtrd 2505	. . . . . . . 8 |- ( ph -> ( ( S Dn F ) ` ( N - N ) ) = F )
284	283	fveq1d 5881	. . . . . . 7 |- ( ph -> ( ( ( S Dn F ) ` ( N - N ) ) ` x ) = ( F ` x ) )
285	279	fveq2d 5883	. . . . . . . . 9 |- ( ph -> ( ( CC Dn T ) ` ( N - N ) ) = ( ( CC Dn T ) ` 0 ) )
286		dvn0 22957	. . . . . . . . . 10 |- ( ( CC C_ CC /\ T e. ( CC ^pm CC ) ) -> ( ( CC Dn T ) ` 0 ) = T )
287	193, 199, 286	sylancr 676	. . . . . . . . 9 |- ( ph -> ( ( CC Dn T ) ` 0 ) = T )
288	285, 287	eqtrd 2505	. . . . . . . 8 |- ( ph -> ( ( CC Dn T ) ` ( N - N ) ) = T )
289	288	fveq1d 5881	. . . . . . 7 |- ( ph -> ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) = ( T ` x ) )
290	284, 289	oveq12d 6326	. . . . . 6 |- ( ph -> ( ( ( ( S Dn F ) ` ( N - N ) ) ` x ) - ( ( ( CC Dn T ) ` ( N - N ) ) ` x ) ) = ( ( F ` x ) - ( T ` x ) ) )
291	290	oveq1d 6323	. . . . 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 4483	. . . 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 2523	. . 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 6323	. 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 2551	1 |- ( ph -> 0 e. ( R lim CC B ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 376   = wceq 1452   e. wcel 1904   _Vcvv 3031   \ cdif 3387   i^i cin 3389   C_ wss 3390   {csn 3959   {cpr 3961   U.cuni 4190   class class class wbr 4395   |-> cmpt 4454   dom cdm 4839   Fun wfun 5583   -->wf 5585   ` cfv 5589  (class class class)co 6308   ^m cmap 7490   ^pm cpm 7491   CCcc 9555   RRcr 9556   0cc0 9557   1c1 9558   + caddc 9560   - cmin 9880   / cdiv 10291   NNcn 10631   NN0cn0 10893   ZZ>=cuz 11182   ...cfz 11810  ..^cfzo 11942   ^cexp 12310   ↾_t crest 15397   TopOpenctopn 15398  ℂ_fldccnfld 19047   Topctop 19994  TopOnctopon 19995   intcnt 20109   lim CC climc 22896   _D cdv 22897   Dncdvn 22898   Tayl ctayl 23387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635  ax-addf 9636  ax-mulf 9637

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-iin 4272  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  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-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-of 6550  df-om 6712  df-1st 6812  df-2nd 6813  df-supp 6934  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-2o 7201  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-ixp 7541  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-fsupp 7902  df-fi 7943  df-sup 7974  df-inf 7975  df-oi 8043  df-card 8391  df-cda 8616  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-4 10692  df-5 10693  df-6 10694  df-7 10695  df-8 10696  df-9 10697  df-10 10698  df-n0 10894  df-z 10962  df-dec 11075  df-uz 11183  df-q 11288  df-rp 11326  df-xneg 11432  df-xadd 11433  df-xmul 11434  df-icc 11667  df-fz 11811  df-fzo 11943  df-seq 12252  df-exp 12311  df-fac 12498  df-hash 12554  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-clim 13629  df-sum 13830  df-struct 15201  df-ndx 15202  df-slot 15203  df-base 15204  df-sets 15205  df-ress 15206  df-plusg 15281  df-mulr 15282  df-starv 15283  df-sca 15284  df-vsca 15285  df-ip 15286  df-tset 15287  df-ple 15288  df-ds 15290  df-unif 15291  df-hom 15292  df-cco 15293  df-rest 15399  df-topn 15400  df-0g 15418  df-gsum 15419  df-topgen 15420  df-pt 15421  df-prds 15424  df-xrs 15478  df-qtop 15484  df-imas 15485  df-xps 15488  df-mre 15570  df-mrc 15571  df-acs 15573  df-mgm 16566  df-sgrp 16605  df-mnd 16615  df-submnd 16661  df-grp 16751  df-minusg 16752  df-mulg 16754  df-cntz 17049  df-cmn 17510  df-abl 17511  df-mgp 17802  df-ur 17814  df-ring 17860  df-cring 17861  df-psmet 19039  df-xmet 19040  df-met 19041  df-bl 19042  df-mopn 19043  df-fbas 19044  df-fg 19045  df-cnfld 19048  df-top 19998  df-bases 19999  df-topon 20000  df-topsp 20001  df-cld 20111  df-ntr 20112  df-cls 20113  df-nei 20191  df-lp 20229  df-perf 20230  df-cn 20320  df-cnp 20321  df-haus 20408  df-tx 20654  df-hmeo 20847  df-fil 20939  df-fm 21031  df-flim 21032  df-flf 21033  df-tsms 21219  df-xms 21413  df-ms 21414  df-tms 21415  df-cncf 21988  df-limc 22900  df-dv 22901  df-dvn 22902  df-tayl 23389

This theorem is referenced by:  taylth  23409