MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  taylthlem1 Structured version   Unicode version

Theorem taylthlem1 23305
Description: Lemma for taylth 23307. This is the main part of Taylor's theorem, except for the induction step, which is supposed to be proven using L'Hôpital's rule. However, since our proof of L'Hôpital assumes that  S  =  RR, we can only do this part generically, and for taylth 23307 itself we must restrict to  RR. (Contributed by Mario Carneiro, 1-Jan-2017.)
Hypotheses
Ref Expression
taylthlem1.s  |-  ( ph  ->  S  e.  { RR ,  CC } )
taylthlem1.f  |-  ( ph  ->  F : A --> CC )
taylthlem1.a  |-  ( ph  ->  A  C_  S )
taylthlem1.d  |-  ( ph  ->  dom  ( ( S  Dn F ) `
 N )  =  A )
taylthlem1.n  |-  ( ph  ->  N  e.  NN )
taylthlem1.b  |-  ( ph  ->  B  e.  A )
taylthlem1.t  |-  T  =  ( N ( S Tayl 
F ) B )
taylthlem1.r  |-  R  =  ( x  e.  ( A  \  { B } )  |->  ( ( ( F `  x
)  -  ( T `
 x ) )  /  ( ( x  -  B ) ^ N ) ) )
taylthlem1.i  |-  ( (
ph  /\  ( n  e.  ( 1..^ N )  /\  0  e.  ( ( y  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  -  n ) ) `  y )  -  (
( ( CC  Dn T ) `  ( N  -  n
) ) `  y
) )  /  (
( y  -  B
) ^ n ) ) ) lim CC  B
) ) )  -> 
0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  (
n  +  1 ) ) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  ( n  +  1 ) ) ) `  x ) )  /  ( ( x  -  B ) ^ ( n  + 
1 ) ) ) ) lim CC  B ) )
Assertion
Ref Expression
taylthlem1  |-  ( ph  ->  0  e.  ( R lim
CC  B ) )
Distinct variable groups:    x, n, y, A    B, n, x, y    n, F, x, y    ph, n, x, y   
n, N, x, y    S, n, x, y    T, n, x, y
Allowed substitution hints:    R( x, y, n)

Proof of Theorem taylthlem1
Dummy variable  m is distinct from all other variables.
StepHypRef Expression
1 taylthlem1.n . . . 4  |-  ( ph  ->  N  e.  NN )
2 elfz1end 11823 . . . 4  |-  ( N  e.  NN  <->  N  e.  ( 1 ... N
) )
31, 2sylib 199 . . 3  |-  ( ph  ->  N  e.  ( 1 ... N ) )
4 oveq2 6305 . . . . . . . . . . . 12  |-  ( m  =  1  ->  ( N  -  m )  =  ( N  - 
1 ) )
54fveq2d 5877 . . . . . . . . . . 11  |-  ( m  =  1  ->  (
( S  Dn
F ) `  ( N  -  m )
)  =  ( ( S  Dn F ) `  ( N  -  1 ) ) )
65fveq1d 5875 . . . . . . . . . 10  |-  ( m  =  1  ->  (
( ( S  Dn F ) `  ( N  -  m
) ) `  x
)  =  ( ( ( S  Dn
F ) `  ( N  -  1 ) ) `  x ) )
74fveq2d 5877 . . . . . . . . . . 11  |-  ( m  =  1  ->  (
( CC  Dn
T ) `  ( N  -  m )
)  =  ( ( CC  Dn T ) `  ( N  -  1 ) ) )
87fveq1d 5875 . . . . . . . . . 10  |-  ( m  =  1  ->  (
( ( CC  Dn T ) `  ( N  -  m
) ) `  x
)  =  ( ( ( CC  Dn
T ) `  ( N  -  1 ) ) `  x ) )
96, 8oveq12d 6315 . . . . . . . . 9  |-  ( m  =  1  ->  (
( ( ( S  Dn F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  m
) ) `  x
) )  =  ( ( ( ( S  Dn F ) `
 ( N  - 
1 ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  1
) ) `  x
) ) )
10 oveq2 6305 . . . . . . . . 9  |-  ( m  =  1  ->  (
( x  -  B
) ^ m )  =  ( ( x  -  B ) ^
1 ) )
119, 10oveq12d 6315 . . . . . . . 8  |-  ( m  =  1  ->  (
( ( ( ( S  Dn F ) `  ( N  -  m ) ) `
 x )  -  ( ( ( CC  Dn T ) `
 ( N  -  m ) ) `  x ) )  / 
( ( x  -  B ) ^ m
) )  =  ( ( ( ( ( S  Dn F ) `  ( N  -  1 ) ) `
 x )  -  ( ( ( CC  Dn T ) `
 ( N  - 
1 ) ) `  x ) )  / 
( ( x  -  B ) ^ 1 ) ) )
1211mpteq2dv 4505 . . . . . . 7  |-  ( m  =  1  ->  (
x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  m
) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  m )
) `  x )
)  /  ( ( x  -  B ) ^ m ) ) )  =  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  1 ) ) `
 x )  -  ( ( ( CC  Dn T ) `
 ( N  - 
1 ) ) `  x ) )  / 
( ( x  -  B ) ^ 1 ) ) ) )
1312oveq1d 6312 . . . . . 6  |-  ( m  =  1  ->  (
( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  m
) ) `  x
) )  /  (
( x  -  B
) ^ m ) ) ) lim CC  B
)  =  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  1
) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  1 ) ) `  x ) )  /  ( ( x  -  B ) ^ 1 ) ) ) lim CC  B ) )
1413eleq2d 2490 . . . . 5  |-  ( m  =  1  ->  (
0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  m
) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  m )
) `  x )
)  /  ( ( x  -  B ) ^ m ) ) ) lim CC  B )  <->  0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  1
) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  1 ) ) `  x ) )  /  ( ( x  -  B ) ^ 1 ) ) ) lim CC  B ) ) )
1514imbi2d 317 . . . 4  |-  ( m  =  1  ->  (
( ph  ->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  m
) ) `  x
) )  /  (
( x  -  B
) ^ m ) ) ) lim CC  B
) )  <->  ( ph  ->  0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  1
) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  1 ) ) `  x ) )  /  ( ( x  -  B ) ^ 1 ) ) ) lim CC  B ) ) ) )
16 oveq2 6305 . . . . . . . . . . . . 13  |-  ( m  =  n  ->  ( N  -  m )  =  ( N  -  n ) )
1716fveq2d 5877 . . . . . . . . . . . 12  |-  ( m  =  n  ->  (
( S  Dn
F ) `  ( N  -  m )
)  =  ( ( S  Dn F ) `  ( N  -  n ) ) )
1817fveq1d 5875 . . . . . . . . . . 11  |-  ( m  =  n  ->  (
( ( S  Dn F ) `  ( N  -  m
) ) `  x
)  =  ( ( ( S  Dn
F ) `  ( N  -  n )
) `  x )
)
1916fveq2d 5877 . . . . . . . . . . . 12  |-  ( m  =  n  ->  (
( CC  Dn
T ) `  ( N  -  m )
)  =  ( ( CC  Dn T ) `  ( N  -  n ) ) )
2019fveq1d 5875 . . . . . . . . . . 11  |-  ( m  =  n  ->  (
( ( CC  Dn T ) `  ( N  -  m
) ) `  x
)  =  ( ( ( CC  Dn
T ) `  ( N  -  n )
) `  x )
)
2118, 20oveq12d 6315 . . . . . . . . . 10  |-  ( m  =  n  ->  (
( ( ( S  Dn F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  m
) ) `  x
) )  =  ( ( ( ( S  Dn F ) `
 ( N  -  n ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  n
) ) `  x
) ) )
22 oveq2 6305 . . . . . . . . . 10  |-  ( m  =  n  ->  (
( x  -  B
) ^ m )  =  ( ( x  -  B ) ^
n ) )
2321, 22oveq12d 6315 . . . . . . . . 9  |-  ( m  =  n  ->  (
( ( ( ( S  Dn F ) `  ( N  -  m ) ) `
 x )  -  ( ( ( CC  Dn T ) `
 ( N  -  m ) ) `  x ) )  / 
( ( x  -  B ) ^ m
) )  =  ( ( ( ( ( S  Dn F ) `  ( N  -  n ) ) `
 x )  -  ( ( ( CC  Dn T ) `
 ( N  -  n ) ) `  x ) )  / 
( ( x  -  B ) ^ n
) ) )
2423mpteq2dv 4505 . . . . . . . 8  |-  ( m  =  n  ->  (
x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  m
) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  m )
) `  x )
)  /  ( ( x  -  B ) ^ m ) ) )  =  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  n ) ) `
 x )  -  ( ( ( CC  Dn T ) `
 ( N  -  n ) ) `  x ) )  / 
( ( x  -  B ) ^ n
) ) ) )
25 fveq2 5873 . . . . . . . . . . 11  |-  ( x  =  y  ->  (
( ( S  Dn F ) `  ( N  -  n
) ) `  x
)  =  ( ( ( S  Dn
F ) `  ( N  -  n )
) `  y )
)
26 fveq2 5873 . . . . . . . . . . 11  |-  ( x  =  y  ->  (
( ( CC  Dn T ) `  ( N  -  n
) ) `  x
)  =  ( ( ( CC  Dn
T ) `  ( N  -  n )
) `  y )
)
2725, 26oveq12d 6315 . . . . . . . . . 10  |-  ( x  =  y  ->  (
( ( ( S  Dn F ) `
 ( N  -  n ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  n
) ) `  x
) )  =  ( ( ( ( S  Dn F ) `
 ( N  -  n ) ) `  y )  -  (
( ( CC  Dn T ) `  ( N  -  n
) ) `  y
) ) )
28 oveq1 6304 . . . . . . . . . . 11  |-  ( x  =  y  ->  (
x  -  B )  =  ( y  -  B ) )
2928oveq1d 6312 . . . . . . . . . 10  |-  ( x  =  y  ->  (
( x  -  B
) ^ n )  =  ( ( y  -  B ) ^
n ) )
3027, 29oveq12d 6315 . . . . . . . . 9  |-  ( x  =  y  ->  (
( ( ( ( S  Dn F ) `  ( N  -  n ) ) `
 x )  -  ( ( ( CC  Dn T ) `
 ( N  -  n ) ) `  x ) )  / 
( ( x  -  B ) ^ n
) )  =  ( ( ( ( ( S  Dn F ) `  ( N  -  n ) ) `
 y )  -  ( ( ( CC  Dn T ) `
 ( N  -  n ) ) `  y ) )  / 
( ( y  -  B ) ^ n
) ) )
3130cbvmptv 4510 . . . . . . . 8  |-  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  n ) ) `
 x )  -  ( ( ( CC  Dn T ) `
 ( N  -  n ) ) `  x ) )  / 
( ( x  -  B ) ^ n
) ) )  =  ( y  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  -  n ) ) `  y )  -  (
( ( CC  Dn T ) `  ( N  -  n
) ) `  y
) )  /  (
( y  -  B
) ^ n ) ) )
3224, 31syl6eq 2477 . . . . . . 7  |-  ( m  =  n  ->  (
x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  m
) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  m )
) `  x )
)  /  ( ( x  -  B ) ^ m ) ) )  =  ( y  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  n ) ) `
 y )  -  ( ( ( CC  Dn T ) `
 ( N  -  n ) ) `  y ) )  / 
( ( y  -  B ) ^ n
) ) ) )
3332oveq1d 6312 . . . . . 6  |-  ( m  =  n  ->  (
( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  m
) ) `  x
) )  /  (
( x  -  B
) ^ m ) ) ) lim CC  B
)  =  ( ( y  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  n
) ) `  y
)  -  ( ( ( CC  Dn
T ) `  ( N  -  n )
) `  y )
)  /  ( ( y  -  B ) ^ n ) ) ) lim CC  B ) )
3433eleq2d 2490 . . . . 5  |-  ( m  =  n  ->  (
0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  m
) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  m )
) `  x )
)  /  ( ( x  -  B ) ^ m ) ) ) lim CC  B )  <->  0  e.  ( ( y  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  n
) ) `  y
)  -  ( ( ( CC  Dn
T ) `  ( N  -  n )
) `  y )
)  /  ( ( y  -  B ) ^ n ) ) ) lim CC  B ) ) )
3534imbi2d 317 . . . 4  |-  ( m  =  n  ->  (
( ph  ->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  m
) ) `  x
) )  /  (
( x  -  B
) ^ m ) ) ) lim CC  B
) )  <->  ( ph  ->  0  e.  ( ( y  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  n
) ) `  y
)  -  ( ( ( CC  Dn
T ) `  ( N  -  n )
) `  y )
)  /  ( ( y  -  B ) ^ n ) ) ) lim CC  B ) ) ) )
36 oveq2 6305 . . . . . . . . . . . 12  |-  ( m  =  ( n  + 
1 )  ->  ( N  -  m )  =  ( N  -  ( n  +  1
) ) )
3736fveq2d 5877 . . . . . . . . . . 11  |-  ( m  =  ( n  + 
1 )  ->  (
( S  Dn
F ) `  ( N  -  m )
)  =  ( ( S  Dn F ) `  ( N  -  ( n  + 
1 ) ) ) )
3837fveq1d 5875 . . . . . . . . . 10  |-  ( m  =  ( n  + 
1 )  ->  (
( ( S  Dn F ) `  ( N  -  m
) ) `  x
)  =  ( ( ( S  Dn
F ) `  ( N  -  ( n  +  1 ) ) ) `  x ) )
3936fveq2d 5877 . . . . . . . . . . 11  |-  ( m  =  ( n  + 
1 )  ->  (
( CC  Dn
T ) `  ( N  -  m )
)  =  ( ( CC  Dn T ) `  ( N  -  ( n  + 
1 ) ) ) )
4039fveq1d 5875 . . . . . . . . . 10  |-  ( m  =  ( n  + 
1 )  ->  (
( ( CC  Dn T ) `  ( N  -  m
) ) `  x
)  =  ( ( ( CC  Dn
T ) `  ( N  -  ( n  +  1 ) ) ) `  x ) )
4138, 40oveq12d 6315 . . . . . . . . 9  |-  ( m  =  ( n  + 
1 )  ->  (
( ( ( S  Dn F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  m
) ) `  x
) )  =  ( ( ( ( S  Dn F ) `
 ( N  -  ( n  +  1
) ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  (
n  +  1 ) ) ) `  x
) ) )
42 oveq2 6305 . . . . . . . . 9  |-  ( m  =  ( n  + 
1 )  ->  (
( x  -  B
) ^ m )  =  ( ( x  -  B ) ^
( n  +  1 ) ) )
4341, 42oveq12d 6315 . . . . . . . 8  |-  ( m  =  ( n  + 
1 )  ->  (
( ( ( ( S  Dn F ) `  ( N  -  m ) ) `
 x )  -  ( ( ( CC  Dn T ) `
 ( N  -  m ) ) `  x ) )  / 
( ( x  -  B ) ^ m
) )  =  ( ( ( ( ( S  Dn F ) `  ( N  -  ( n  + 
1 ) ) ) `
 x )  -  ( ( ( CC  Dn T ) `
 ( N  -  ( n  +  1
) ) ) `  x ) )  / 
( ( x  -  B ) ^ (
n  +  1 ) ) ) )
4443mpteq2dv 4505 . . . . . . 7  |-  ( m  =  ( n  + 
1 )  ->  (
x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  m
) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  m )
) `  x )
)  /  ( ( x  -  B ) ^ m ) ) )  =  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  ( n  + 
1 ) ) ) `
 x )  -  ( ( ( CC  Dn T ) `
 ( N  -  ( n  +  1
) ) ) `  x ) )  / 
( ( x  -  B ) ^ (
n  +  1 ) ) ) ) )
4544oveq1d 6312 . . . . . 6  |-  ( m  =  ( n  + 
1 )  ->  (
( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  m
) ) `  x
) )  /  (
( x  -  B
) ^ m ) ) ) lim CC  B
)  =  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  (
n  +  1 ) ) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  ( n  +  1 ) ) ) `  x ) )  /  ( ( x  -  B ) ^ ( n  + 
1 ) ) ) ) lim CC  B ) )
4645eleq2d 2490 . . . . 5  |-  ( m  =  ( n  + 
1 )  ->  (
0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  m
) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  m )
) `  x )
)  /  ( ( x  -  B ) ^ m ) ) ) lim CC  B )  <->  0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  (
n  +  1 ) ) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  ( n  +  1 ) ) ) `  x ) )  /  ( ( x  -  B ) ^ ( n  + 
1 ) ) ) ) lim CC  B ) ) )
4746imbi2d 317 . . . 4  |-  ( m  =  ( n  + 
1 )  ->  (
( ph  ->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  m
) ) `  x
) )  /  (
( x  -  B
) ^ m ) ) ) lim CC  B
) )  <->  ( ph  ->  0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  (
n  +  1 ) ) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  ( n  +  1 ) ) ) `  x ) )  /  ( ( x  -  B ) ^ ( n  + 
1 ) ) ) ) lim CC  B ) ) ) )
48 oveq2 6305 . . . . . . . . . . . 12  |-  ( m  =  N  ->  ( N  -  m )  =  ( N  -  N ) )
4948fveq2d 5877 . . . . . . . . . . 11  |-  ( m  =  N  ->  (
( S  Dn
F ) `  ( N  -  m )
)  =  ( ( S  Dn F ) `  ( N  -  N ) ) )
5049fveq1d 5875 . . . . . . . . . 10  |-  ( m  =  N  ->  (
( ( S  Dn F ) `  ( N  -  m
) ) `  x
)  =  ( ( ( S  Dn
F ) `  ( N  -  N )
) `  x )
)
5148fveq2d 5877 . . . . . . . . . . 11  |-  ( m  =  N  ->  (
( CC  Dn
T ) `  ( N  -  m )
)  =  ( ( CC  Dn T ) `  ( N  -  N ) ) )
5251fveq1d 5875 . . . . . . . . . 10  |-  ( m  =  N  ->  (
( ( CC  Dn T ) `  ( N  -  m
) ) `  x
)  =  ( ( ( CC  Dn
T ) `  ( N  -  N )
) `  x )
)
5350, 52oveq12d 6315 . . . . . . . . 9  |-  ( m  =  N  ->  (
( ( ( S  Dn F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  m
) ) `  x
) )  =  ( ( ( ( S  Dn F ) `
 ( N  -  N ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  N
) ) `  x
) ) )
54 oveq2 6305 . . . . . . . . 9  |-  ( m  =  N  ->  (
( x  -  B
) ^ m )  =  ( ( x  -  B ) ^ N ) )
5553, 54oveq12d 6315 . . . . . . . 8  |-  ( m  =  N  ->  (
( ( ( ( S  Dn F ) `  ( N  -  m ) ) `
 x )  -  ( ( ( CC  Dn T ) `
 ( N  -  m ) ) `  x ) )  / 
( ( x  -  B ) ^ m
) )  =  ( ( ( ( ( S  Dn F ) `  ( N  -  N ) ) `
 x )  -  ( ( ( CC  Dn T ) `
 ( N  -  N ) ) `  x ) )  / 
( ( x  -  B ) ^ N
) ) )
5655mpteq2dv 4505 . . . . . . 7  |-  ( m  =  N  ->  (
x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  m
) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  m )
) `  x )
)  /  ( ( x  -  B ) ^ m ) ) )  =  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  N ) ) `
 x )  -  ( ( ( CC  Dn T ) `
 ( N  -  N ) ) `  x ) )  / 
( ( x  -  B ) ^ N
) ) ) )
5756oveq1d 6312 . . . . . 6  |-  ( m  =  N  ->  (
( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  m
) ) `  x
) )  /  (
( x  -  B
) ^ m ) ) ) lim CC  B
)  =  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  N
) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  N )
) `  x )
)  /  ( ( x  -  B ) ^ N ) ) ) lim CC  B ) )
5857eleq2d 2490 . . . . 5  |-  ( m  =  N  ->  (
0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  m
) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  m )
) `  x )
)  /  ( ( x  -  B ) ^ m ) ) ) lim CC  B )  <->  0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  N
) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  N )
) `  x )
)  /  ( ( x  -  B ) ^ N ) ) ) lim CC  B ) ) )
5958imbi2d 317 . . . 4  |-  ( m  =  N  ->  (
( ph  ->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  m
) ) `  x
) )  /  (
( x  -  B
) ^ m ) ) ) lim CC  B
) )  <->  ( ph  ->  0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  N
) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  N )
) `  x )
)  /  ( ( x  -  B ) ^ N ) ) ) lim CC  B ) ) ) )
60 taylthlem1.b . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  A )
61 fveq2 5873 . . . . . . . . . . . . . 14  |-  ( y  =  B  ->  (
( ( S  Dn F ) `  N ) `  y
)  =  ( ( ( S  Dn
F ) `  N
) `  B )
)
62 fveq2 5873 . . . . . . . . . . . . . 14  |-  ( y  =  B  ->  (
( ( CC  Dn T ) `  N ) `  y
)  =  ( ( ( CC  Dn
T ) `  N
) `  B )
)
6361, 62oveq12d 6315 . . . . . . . . . . . . 13  |-  ( y  =  B  ->  (
( ( ( S  Dn F ) `
 N ) `  y )  -  (
( ( CC  Dn T ) `  N ) `  y
) )  =  ( ( ( ( S  Dn F ) `
 N ) `  B )  -  (
( ( CC  Dn T ) `  N ) `  B
) ) )
64 eqid 2420 . . . . . . . . . . . . 13  |-  ( y  e.  A  |->  ( ( ( ( S  Dn F ) `  N ) `  y
)  -  ( ( ( CC  Dn
T ) `  N
) `  y )
) )  =  ( y  e.  A  |->  ( ( ( ( S  Dn F ) `
 N ) `  y )  -  (
( ( CC  Dn T ) `  N ) `  y
) ) )
65 ovex 6325 . . . . . . . . . . . . 13  |-  ( ( ( ( S  Dn F ) `  N ) `  B
)  -  ( ( ( CC  Dn
T ) `  N
) `  B )
)  e.  _V
6663, 64, 65fvmpt 5956 . . . . . . . . . . . 12  |-  ( B  e.  A  ->  (
( y  e.  A  |->  ( ( ( ( S  Dn F ) `  N ) `
 y )  -  ( ( ( CC  Dn T ) `
 N ) `  y ) ) ) `
 B )  =  ( ( ( ( S  Dn F ) `  N ) `
 B )  -  ( ( ( CC  Dn T ) `
 N ) `  B ) ) )
6760, 66syl 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 )
711nnnn0d 10921 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  NN0 )
72 nn0uz 11189 . . . . . . . . . . . . . . 15  |-  NN0  =  ( ZZ>= `  0 )
7371, 72syl6eleq 2518 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  ( ZZ>= ` 
0 ) )
74 eluzfz2b 11802 . . . . . . . . . . . . . 14  |-  ( N  e.  ( ZZ>= `  0
)  <->  N  e.  (
0 ... N ) )
7573, 74sylib 199 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  ( 0 ... N ) )
76 taylthlem1.d . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( ( S  Dn F ) `
 N )  =  A )
7760, 76eleqtrrd 2511 . . . . . . . . . . . . 13  |-  ( ph  ->  B  e.  dom  (
( S  Dn
F ) `  N
) )
78 taylthlem1.t . . . . . . . . . . . . 13  |-  T  =  ( N ( S Tayl 
F ) B )
7968, 69, 70, 75, 77, 78dvntaylp0 23304 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( CC  Dn T ) `
 N ) `  B )  =  ( ( ( S  Dn F ) `  N ) `  B
) )
8079oveq2d 6313 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( S  Dn F ) `  N ) `
 B )  -  ( ( ( CC  Dn T ) `
 N ) `  B ) )  =  ( ( ( ( S  Dn F ) `  N ) `
 B )  -  ( ( ( S  Dn F ) `
 N ) `  B ) ) )
81 cnex 9616 . . . . . . . . . . . . . . . 16  |-  CC  e.  _V
8281a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  CC  e.  _V )
83 elpm2r 7489 . . . . . . . . . . . . . . 15  |-  ( ( ( CC  e.  _V  /\  S  e.  { RR ,  CC } )  /\  ( F : A --> CC  /\  A  C_  S ) )  ->  F  e.  ( CC  ^pm  S )
)
8482, 68, 69, 70, 83syl22anc 1265 . . . . . . . . . . . . . 14  |-  ( ph  ->  F  e.  ( CC 
^pm  S ) )
85 dvnf 22858 . . . . . . . . . . . . . 14  |-  ( ( S  e.  { RR ,  CC }  /\  F  e.  ( CC  ^pm  S
)  /\  N  e.  NN0 )  ->  ( ( S  Dn F ) `
 N ) : dom  ( ( S  Dn F ) `
 N ) --> CC )
8668, 84, 71, 85syl3anc 1264 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( S  Dn F ) `  N ) : dom  ( ( S  Dn F ) `  N ) --> CC )
8786, 77ffvelrnd 6030 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( S  Dn F ) `
 N ) `  B )  e.  CC )
8887subidd 9970 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( S  Dn F ) `  N ) `
 B )  -  ( ( ( S  Dn F ) `
 N ) `  B ) )  =  0 )
8967, 80, 883eqtrd 2465 . . . . . . . . . 10  |-  ( ph  ->  ( ( y  e.  A  |->  ( ( ( ( S  Dn
F ) `  N
) `  y )  -  ( ( ( CC  Dn T ) `  N ) `
 y ) ) ) `  B )  =  0 )
90 funmpt 5629 . . . . . . . . . . 11  |-  Fun  (
y  e.  A  |->  ( ( ( ( S  Dn F ) `
 N ) `  y )  -  (
( ( CC  Dn T ) `  N ) `  y
) ) )
91 ovex 6325 . . . . . . . . . . . . 13  |-  ( ( ( ( S  Dn F ) `  N ) `  y
)  -  ( ( ( CC  Dn
T ) `  N
) `  y )
)  e.  _V
9291, 64dmmpti 5717 . . . . . . . . . . . 12  |-  dom  (
y  e.  A  |->  ( ( ( ( S  Dn F ) `
 N ) `  y )  -  (
( ( CC  Dn T ) `  N ) `  y
) ) )  =  A
9360, 92syl6eleqr 2519 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  dom  (
y  e.  A  |->  ( ( ( ( S  Dn F ) `
 N ) `  y )  -  (
( ( CC  Dn T ) `  N ) `  y
) ) ) )
94 funbrfvb 5915 . . . . . . . . . . 11  |-  ( ( Fun  ( y  e.  A  |->  ( ( ( ( S  Dn
F ) `  N
) `  y )  -  ( ( ( CC  Dn T ) `  N ) `
 y ) ) )  /\  B  e. 
dom  ( y  e.  A  |->  ( ( ( ( S  Dn
F ) `  N
) `  y )  -  ( ( ( CC  Dn T ) `  N ) `
 y ) ) ) )  ->  (
( ( y  e.  A  |->  ( ( ( ( S  Dn
F ) `  N
) `  y )  -  ( ( ( CC  Dn T ) `  N ) `
 y ) ) ) `  B )  =  0  <->  B (
y  e.  A  |->  ( ( ( ( S  Dn F ) `
 N ) `  y )  -  (
( ( CC  Dn T ) `  N ) `  y
) ) ) 0 ) )
9590, 93, 94sylancr 667 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( y  e.  A  |->  ( ( ( ( S  Dn F ) `  N ) `  y
)  -  ( ( ( CC  Dn
T ) `  N
) `  y )
) ) `  B
)  =  0  <->  B
( y  e.  A  |->  ( ( ( ( S  Dn F ) `  N ) `
 y )  -  ( ( ( CC  Dn T ) `
 N ) `  y ) ) ) 0 ) )
9689, 95mpbid 213 . . . . . . . . 9  |-  ( ph  ->  B ( y  e.  A  |->  ( ( ( ( S  Dn
F ) `  N
) `  y )  -  ( ( ( CC  Dn T ) `  N ) `
 y ) ) ) 0 )
97 nnm1nn0 10907 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN  ->  ( N  -  1 )  e.  NN0 )
981, 97syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( N  -  1 )  e.  NN0 )
99 dvnf 22858 . . . . . . . . . . . . . 14  |-  ( ( S  e.  { RR ,  CC }  /\  F  e.  ( CC  ^pm  S
)  /\  ( N  -  1 )  e. 
NN0 )  ->  (
( S  Dn
F ) `  ( N  -  1 ) ) : dom  (
( S  Dn
F ) `  ( N  -  1 ) ) --> CC )
10068, 84, 98, 99syl3anc 1264 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( S  Dn F ) `  ( N  -  1
) ) : dom  ( ( S  Dn F ) `  ( N  -  1
) ) --> CC )
101 dvnbss 22859 . . . . . . . . . . . . . . . . 17  |-  ( ( S  e.  { RR ,  CC }  /\  F  e.  ( CC  ^pm  S
)  /\  ( N  -  1 )  e. 
NN0 )  ->  dom  ( ( S  Dn F ) `  ( N  -  1
) )  C_  dom  F )
10268, 84, 98, 101syl3anc 1264 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  ( ( S  Dn F ) `
 ( N  - 
1 ) )  C_  dom  F )
103 fdm 5742 . . . . . . . . . . . . . . . . 17  |-  ( F : A --> CC  ->  dom 
F  =  A )
10469, 103syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  F  =  A )
105102, 104sseqtrd 3497 . . . . . . . . . . . . . . 15  |-  ( ph  ->  dom  ( ( S  Dn F ) `
 ( N  - 
1 ) )  C_  A )
106 fzo0end 11996 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  NN  ->  ( N  -  1 )  e.  ( 0..^ N ) )
107 elfzofz 11929 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  -  1 )  e.  ( 0..^ N )  ->  ( N  -  1 )  e.  ( 0 ... N
) )
1081, 106, 1073syl 18 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( N  -  1 )  e.  ( 0 ... N ) )
109 dvn2bss 22861 . . . . . . . . . . . . . . . . 17  |-  ( ( S  e.  { RR ,  CC }  /\  F  e.  ( CC  ^pm  S
)  /\  ( N  -  1 )  e.  ( 0 ... N
) )  ->  dom  ( ( S  Dn F ) `  N )  C_  dom  ( ( S  Dn F ) `  ( N  -  1
) ) )
11068, 84, 108, 109syl3anc 1264 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  ( ( S  Dn F ) `
 N )  C_  dom  ( ( S  Dn F ) `  ( N  -  1
) ) )
11176, 110eqsstr3d 3496 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  C_  dom  ( ( S  Dn F ) `  ( N  -  1 ) ) )
112105, 111eqssd 3478 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( ( S  Dn F ) `
 ( N  - 
1 ) )  =  A )
113112feq2d 5725 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( S  Dn F ) `
 ( N  - 
1 ) ) : dom  ( ( S  Dn F ) `
 ( N  - 
1 ) ) --> CC  <->  ( ( S  Dn
F ) `  ( N  -  1 ) ) : A --> CC ) )
114100, 113mpbid 213 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( S  Dn F ) `  ( N  -  1
) ) : A --> CC )
115114ffvelrnda 6029 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( S  Dn F ) `  ( N  -  1
) ) `  y
)  e.  CC )
11676feq2d 5725 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( S  Dn F ) `
 N ) : dom  ( ( S  Dn F ) `
 N ) --> CC  <->  ( ( S  Dn
F ) `  N
) : A --> CC ) )
11786, 116mpbid 213 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( S  Dn F ) `  N ) : A --> CC )
118117ffvelrnda 6029 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( S  Dn F ) `  N ) `  y
)  e.  CC )
1191nncnd 10621 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  CC )
120 1cnd 9655 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  CC )
121119, 120npcand 9986 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
122121fveq2d 5877 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( S  Dn F ) `  ( ( N  - 
1 )  +  1 ) )  =  ( ( S  Dn
F ) `  N
) )
123 recnprss 22836 . . . . . . . . . . . . . . 15  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )
12468, 123syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  S  C_  CC )
125 dvnp1 22856 . . . . . . . . . . . . . 14  |-  ( ( S  C_  CC  /\  F  e.  ( CC  ^pm  S
)  /\  ( N  -  1 )  e. 
NN0 )  ->  (
( S  Dn
F ) `  (
( N  -  1 )  +  1 ) )  =  ( S  _D  ( ( S  Dn F ) `
 ( N  - 
1 ) ) ) )
126124, 84, 98, 125syl3anc 1264 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( S  Dn F ) `  ( ( N  - 
1 )  +  1 ) )  =  ( S  _D  ( ( S  Dn F ) `  ( N  -  1 ) ) ) )
127122, 126eqtr3d 2463 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( S  Dn F ) `  N )  =  ( S  _D  ( ( S  Dn F ) `  ( N  -  1 ) ) ) )
128117feqmptd 5926 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( S  Dn F ) `  N )  =  ( y  e.  A  |->  ( ( ( S  Dn F ) `  N ) `  y
) ) )
129114feqmptd 5926 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( S  Dn F ) `  ( N  -  1
) )  =  ( y  e.  A  |->  ( ( ( S  Dn F ) `  ( N  -  1
) ) `  y
) ) )
130129oveq2d 6313 . . . . . . . . . . . 12  |-  ( ph  ->  ( S  _D  (
( S  Dn
F ) `  ( N  -  1 ) ) )  =  ( S  _D  ( y  e.  A  |->  ( ( ( S  Dn
F ) `  ( N  -  1 ) ) `  y ) ) ) )
131127, 128, 1303eqtr3rd 2470 . . . . . . . . . . 11  |-  ( ph  ->  ( S  _D  (
y  e.  A  |->  ( ( ( S  Dn F ) `  ( N  -  1
) ) `  y
) ) )  =  ( y  e.  A  |->  ( ( ( S  Dn F ) `
 N ) `  y ) ) )
13270, 124sstrd 3471 . . . . . . . . . . . . 13  |-  ( ph  ->  A  C_  CC )
133132sselda 3461 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  A )  ->  y  e.  CC )
134 1nn0 10881 . . . . . . . . . . . . . . . 16  |-  1  e.  NN0
135134a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  NN0 )
136 elpm2r 7489 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( CC  e.  _V  /\  S  e.  { RR ,  CC } )  /\  ( ( ( S  Dn F ) `
 ( N  - 
1 ) ) : A --> CC  /\  A  C_  S ) )  -> 
( ( S  Dn F ) `  ( N  -  1
) )  e.  ( CC  ^pm  S )
)
13782, 68, 114, 70, 136syl22anc 1265 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( S  Dn F ) `  ( N  -  1
) )  e.  ( CC  ^pm  S )
)
138 dvn1 22857 . . . . . . . . . . . . . . . . . . 19  |-  ( ( S  C_  CC  /\  (
( S  Dn
F ) `  ( N  -  1 ) )  e.  ( CC 
^pm  S ) )  ->  ( ( S  Dn ( ( S  Dn F ) `  ( N  -  1 ) ) ) `  1 )  =  ( S  _D  ( ( S  Dn F ) `  ( N  -  1
) ) ) )
139124, 137, 138syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( S  Dn ( ( S  Dn F ) `
 ( N  - 
1 ) ) ) `
 1 )  =  ( S  _D  (
( S  Dn
F ) `  ( N  -  1 ) ) ) )
140126, 122eqtr3d 2463 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( S  _D  (
( S  Dn
F ) `  ( N  -  1 ) ) )  =  ( ( S  Dn
F ) `  N
) )
141139, 140eqtrd 2461 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( S  Dn ( ( S  Dn F ) `
 ( N  - 
1 ) ) ) `
 1 )  =  ( ( S  Dn F ) `  N ) )
142141dmeqd 5049 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  ( ( S  Dn ( ( S  Dn F ) `  ( N  -  1 ) ) ) `  1 )  =  dom  ( ( S  Dn F ) `  N ) )
14377, 142eleqtrrd 2511 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  e.  dom  (
( S  Dn
( ( S  Dn F ) `  ( N  -  1
) ) ) ` 
1 ) )
144 eqid 2420 . . . . . . . . . . . . . . 15  |-  ( 1 ( S Tayl  ( ( S  Dn F ) `  ( N  -  1 ) ) ) B )  =  ( 1 ( S Tayl  ( ( S  Dn F ) `  ( N  -  1
) ) ) B )
14568, 114, 70, 135, 143, 144taylpf 23298 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1 ( S Tayl  ( ( S  Dn F ) `  ( N  -  1
) ) ) B ) : CC --> CC )
146120, 119pncan3d 9985 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1  +  ( N  -  1 ) )  =  N )
147146oveq1d 6312 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( 1  +  ( N  -  1 ) ) ( S Tayl 
F ) B )  =  ( N ( S Tayl  F ) B ) )
148147, 78syl6reqr 2480 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  T  =  ( ( 1  +  ( N  -  1 ) ) ( S Tayl  F ) B ) )
149148oveq2d 6313 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( CC  Dn
T )  =  ( CC  Dn ( ( 1  +  ( N  -  1 ) ) ( S Tayl  F
) B ) ) )
150149fveq1d 5875 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( CC  Dn T ) `  ( N  -  1
) )  =  ( ( CC  Dn
( ( 1  +  ( N  -  1 ) ) ( S Tayl 
F ) B ) ) `  ( N  -  1 ) ) )
151146fveq2d 5877 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( S  Dn F ) `  ( 1  +  ( N  -  1 ) ) )  =  ( ( S  Dn
F ) `  N
) )
152151dmeqd 5049 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  dom  ( ( S  Dn F ) `
 ( 1  +  ( N  -  1 ) ) )  =  dom  ( ( S  Dn F ) `
 N ) )
15377, 152eleqtrrd 2511 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  B  e.  dom  (
( S  Dn
F ) `  (
1  +  ( N  -  1 ) ) ) )
15468, 69, 70, 98, 135, 153dvntaylp 23303 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( CC  Dn ( ( 1  +  ( N  - 
1 ) ) ( S Tayl  F ) B ) ) `  ( N  -  1 ) )  =  ( 1 ( S Tayl  ( ( S  Dn F ) `  ( N  -  1 ) ) ) B ) )
155150, 154eqtrd 2461 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( CC  Dn T ) `  ( N  -  1
) )  =  ( 1 ( S Tayl  (
( S  Dn
F ) `  ( N  -  1 ) ) ) B ) )
156155feq1d 5724 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( CC  Dn T ) `
 ( N  - 
1 ) ) : CC --> CC  <->  ( 1 ( S Tayl  ( ( S  Dn F ) `  ( N  -  1 ) ) ) B ) : CC --> CC ) )
157145, 156mpbird 235 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( CC  Dn T ) `  ( N  -  1
) ) : CC --> CC )
158157ffvelrnda 6029 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( ( CC  Dn
T ) `  ( N  -  1 ) ) `  y )  e.  CC )
159133, 158syldan 472 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( CC  Dn T ) `  ( N  -  1
) ) `  y
)  e.  CC )
160 0nn0 10880 . . . . . . . . . . . . . . . 16  |-  0  e.  NN0
161160a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  e.  NN0 )
162 elpm2r 7489 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( CC  e.  _V  /\  S  e.  { RR ,  CC } )  /\  ( ( ( S  Dn F ) `
 N ) : A --> CC  /\  A  C_  S ) )  -> 
( ( S  Dn F ) `  N )  e.  ( CC  ^pm  S )
)
16382, 68, 117, 70, 162syl22anc 1265 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( S  Dn F ) `  N )  e.  ( CC  ^pm  S )
)
164 dvn0 22855 . . . . . . . . . . . . . . . . . 18  |-  ( ( S  C_  CC  /\  (
( S  Dn
F ) `  N
)  e.  ( CC 
^pm  S ) )  ->  ( ( S  Dn ( ( S  Dn F ) `  N ) ) `  0 )  =  ( ( S  Dn F ) `
 N ) )
165124, 163, 164syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( S  Dn ( ( S  Dn F ) `
 N ) ) `
 0 )  =  ( ( S  Dn F ) `  N ) )
166165dmeqd 5049 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  ( ( S  Dn ( ( S  Dn F ) `  N ) ) `  0 )  =  dom  ( ( S  Dn F ) `  N ) )
16777, 166eleqtrrd 2511 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  e.  dom  (
( S  Dn
( ( S  Dn F ) `  N ) ) ` 
0 ) )
168 eqid 2420 . . . . . . . . . . . . . . 15  |-  ( 0 ( S Tayl  ( ( S  Dn F ) `  N ) ) B )  =  ( 0 ( S Tayl  ( ( S  Dn F ) `  N ) ) B )
16968, 117, 70, 161, 167, 168taylpf 23298 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0 ( S Tayl  ( ( S  Dn F ) `  N ) ) B ) : CC --> CC )
170119addid2d 9830 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 0  +  N
)  =  N )
171170oveq1d 6312 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( 0  +  N ) ( S Tayl 
F ) B )  =  ( N ( S Tayl  F ) B ) )
172171, 78syl6eqr 2479 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( 0  +  N ) ( S Tayl 
F ) B )  =  T )
173172oveq2d 6313 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( CC  Dn
( ( 0  +  N ) ( S Tayl 
F ) B ) )  =  ( CC  Dn T ) )
174173fveq1d 5875 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( CC  Dn ( ( 0  +  N ) ( S Tayl  F ) B ) ) `  N
)  =  ( ( CC  Dn T ) `  N ) )
175170fveq2d 5877 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( S  Dn F ) `  ( 0  +  N
) )  =  ( ( S  Dn
F ) `  N
) )
176175dmeqd 5049 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  dom  ( ( S  Dn F ) `
 ( 0  +  N ) )  =  dom  ( ( S  Dn F ) `
 N ) )
17777, 176eleqtrrd 2511 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  B  e.  dom  (
( S  Dn
F ) `  (
0  +  N ) ) )
17868, 69, 70, 71, 161, 177dvntaylp 23303 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( CC  Dn ( ( 0  +  N ) ( S Tayl  F ) B ) ) `  N
)  =  ( 0 ( S Tayl  ( ( S  Dn F ) `  N ) ) B ) )
179174, 178eqtr3d 2463 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( CC  Dn T ) `  N )  =  ( 0 ( S Tayl  (
( S  Dn
F ) `  N
) ) B ) )
180179feq1d 5724 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( CC  Dn T ) `
 N ) : CC --> CC  <->  ( 0 ( S Tayl  ( ( S  Dn F ) `  N ) ) B ) : CC --> CC ) )
181169, 180mpbird 235 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( CC  Dn T ) `  N ) : CC --> CC )
182181ffvelrnda 6029 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( ( CC  Dn
T ) `  N
) `  y )  e.  CC )
183133, 182syldan 472 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( CC  Dn T ) `  N ) `  y
)  e.  CC )
184124sselda 3461 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  S )  ->  y  e.  CC )
185184, 158syldan 472 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  S )  ->  (
( ( CC  Dn T ) `  ( N  -  1
) ) `  y
)  e.  CC )
186184, 182syldan 472 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  S )  ->  (
( ( CC  Dn T ) `  N ) `  y
)  e.  CC )
187 eqid 2420 . . . . . . . . . . . . 13  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
188187cnfldtopon 21780 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
189 toponmax 19920 . . . . . . . . . . . . . 14  |-  ( (
TopOpen ` fld )  e.  (TopOn `  CC )  ->  CC  e.  ( TopOpen ` fld ) )
190188, 189mp1i 13 . . . . . . . . . . . . 13  |-  ( ph  ->  CC  e.  ( TopOpen ` fld )
)
191 df-ss 3447 . . . . . . . . . . . . . 14  |-  ( S 
C_  CC  <->  ( S  i^i  CC )  =  S )
192124, 191sylib 199 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S  i^i  CC )  =  S )
193 ssid 3480 . . . . . . . . . . . . . . . . 17  |-  CC  C_  CC
194193a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  CC  C_  CC )
195 mapsspm 7505 . . . . . . . . . . . . . . . . 17  |-  ( CC 
^m  CC )  C_  ( CC  ^pm  CC )
19668, 69, 70, 71, 77, 78taylpf 23298 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  T : CC --> CC )
19781, 81elmap 7500 . . . . . . . . . . . . . . . . . 18  |-  ( T  e.  ( CC  ^m  CC )  <->  T : CC --> CC )
198196, 197sylibr 215 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  T  e.  ( CC 
^m  CC ) )
199195, 198sseldi 3459 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  T  e.  ( CC 
^pm  CC ) )
200 dvnp1 22856 . . . . . . . . . . . . . . . 16  |-  ( ( CC  C_  CC  /\  T  e.  ( CC  ^pm  CC )  /\  ( N  - 
1 )  e.  NN0 )  ->  ( ( CC  Dn T ) `
 ( ( N  -  1 )  +  1 ) )  =  ( CC  _D  (
( CC  Dn
T ) `  ( N  -  1 ) ) ) )
201194, 199, 98, 200syl3anc 1264 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( CC  Dn T ) `  ( ( N  - 
1 )  +  1 ) )  =  ( CC  _D  ( ( CC  Dn T ) `  ( N  -  1 ) ) ) )
202121fveq2d 5877 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( CC  Dn T ) `  ( ( N  - 
1 )  +  1 ) )  =  ( ( CC  Dn
T ) `  N
) )
203201, 202eqtr3d 2463 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( CC  _D  (
( CC  Dn
T ) `  ( N  -  1 ) ) )  =  ( ( CC  Dn
T ) `  N
) )
204157feqmptd 5926 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( CC  Dn T ) `  ( N  -  1
) )  =  ( y  e.  CC  |->  ( ( ( CC  Dn T ) `  ( N  -  1
) ) `  y
) ) )
205204oveq2d 6313 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( CC  _D  (
( CC  Dn
T ) `  ( N  -  1 ) ) )  =  ( CC  _D  ( y  e.  CC  |->  ( ( ( CC  Dn
T ) `  ( N  -  1 ) ) `  y ) ) ) )
206181feqmptd 5926 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( CC  Dn T ) `  N )  =  ( y  e.  CC  |->  ( ( ( CC  Dn T ) `  N ) `  y
) ) )
207203, 205, 2063eqtr3d 2469 . . . . . . . . . . . . 13  |-  ( ph  ->  ( CC  _D  (
y  e.  CC  |->  ( ( ( CC  Dn T ) `  ( N  -  1
) ) `  y
) ) )  =  ( y  e.  CC  |->  ( ( ( CC  Dn T ) `
 N ) `  y ) ) )
208187, 68, 190, 192, 158, 182, 207dvmptres3 22887 . . . . . . . . . . . 12  |-  ( ph  ->  ( S  _D  (
y  e.  S  |->  ( ( ( CC  Dn T ) `  ( N  -  1
) ) `  y
) ) )  =  ( y  e.  S  |->  ( ( ( CC  Dn T ) `
 N ) `  y ) ) )
209 eqid 2420 . . . . . . . . . . . 12  |-  ( (
TopOpen ` fld )t  S )  =  ( ( TopOpen ` fld )t  S )
210 resttopon 20154 . . . . . . . . . . . . . . . 16  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  S  C_  CC )  ->  (
( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
211188, 124, 210sylancr 667 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
212 topontop 19918 . . . . . . . . . . . . . . 15  |-  ( ( ( TopOpen ` fld )t  S )  e.  (TopOn `  S )  ->  (
( TopOpen ` fld )t  S )  e.  Top )
213211, 212syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( TopOpen ` fld )t  S )  e.  Top )
214 toponuni 19919 . . . . . . . . . . . . . . . 16  |-  ( ( ( TopOpen ` fld )t  S )  e.  (TopOn `  S )  ->  S  =  U. ( ( TopOpen ` fld )t  S
) )
215211, 214syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  S  =  U. (
( TopOpen ` fld )t  S ) )
21670, 215sseqtrd 3497 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  C_  U. (
( TopOpen ` fld )t  S ) )
217 eqid 2420 . . . . . . . . . . . . . . 15  |-  U. (
( TopOpen ` fld )t  S )  =  U. ( ( TopOpen ` fld )t  S )
218217ntrss2 20049 . . . . . . . . . . . . . 14  |-  ( ( ( ( TopOpen ` fld )t  S )  e.  Top  /\  A  C_  U. (
( TopOpen ` fld )t  S ) )  -> 
( ( int `  (
( TopOpen ` fld )t  S ) ) `  A )  C_  A
)
219213, 216, 218syl2anc 665 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  A )  C_  A
)
220140dmeqd 5049 . . . . . . . . . . . . . . 15  |-  ( ph  ->  dom  ( S  _D  ( ( S  Dn F ) `  ( N  -  1
) ) )  =  dom  ( ( S  Dn F ) `
 N ) )
221220, 76eqtrd 2461 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( S  _D  ( ( S  Dn F ) `  ( N  -  1
) ) )  =  A )
222124, 114, 70, 209, 187dvbssntr 22832 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( S  _D  ( ( S  Dn F ) `  ( N  -  1
) ) )  C_  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  A ) )
223221, 222eqsstr3d 3496 . . . . . . . . . . . . 13  |-  ( ph  ->  A  C_  ( ( int `  ( ( TopOpen ` fld )t  S
) ) `  A
) )
224219, 223eqssd 3478 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  A )  =  A )
22568, 185, 186, 208, 70, 209, 187, 224dvmptres2 22893 . . . . . . . . . . 11  |-  ( ph  ->  ( S  _D  (
y  e.  A  |->  ( ( ( CC  Dn T ) `  ( N  -  1
) ) `  y
) ) )  =  ( y  e.  A  |->  ( ( ( CC  Dn T ) `
 N ) `  y ) ) )
22668, 115, 118, 131, 159, 183, 225dvmptsub 22898 . . . . . . . . . 10  |-  ( ph  ->  ( S  _D  (
y  e.  A  |->  ( ( ( ( S  Dn F ) `
 ( N  - 
1 ) ) `  y )  -  (
( ( CC  Dn T ) `  ( N  -  1
) ) `  y
) ) ) )  =  ( y  e.  A  |->  ( ( ( ( S  Dn
F ) `  N
) `  y )  -  ( ( ( CC  Dn T ) `  N ) `
 y ) ) ) )
227226breqd 4428 . . . . . . . . 9  |-  ( ph  ->  ( B ( S  _D  ( y  e.  A  |->  ( ( ( ( S  Dn
F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  Dn T ) `  ( N  -  1 ) ) `
 y ) ) ) ) 0  <->  B
( y  e.  A  |->  ( ( ( ( S  Dn F ) `  N ) `
 y )  -  ( ( ( CC  Dn T ) `
 N ) `  y ) ) ) 0 ) )
22896, 227mpbird 235 . . . . . . . 8  |-  ( ph  ->  B ( S  _D  ( y  e.  A  |->  ( ( ( ( S  Dn F ) `  ( N  -  1 ) ) `
 y )  -  ( ( ( CC  Dn T ) `
 ( N  - 
1 ) ) `  y ) ) ) ) 0 )
229 eqid 2420 . . . . . . . . 9  |-  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( y  e.  A  |->  ( ( ( ( S  Dn F ) `  ( N  -  1
) ) `  y
)  -  ( ( ( CC  Dn
T ) `  ( N  -  1 ) ) `  y ) ) ) `  x
)  -  ( ( y  e.  A  |->  ( ( ( ( S  Dn F ) `
 ( N  - 
1 ) ) `  y )  -  (
( ( CC  Dn T ) `  ( N  -  1
) ) `  y
) ) ) `  B ) )  / 
( x  -  B
) ) )  =  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( y  e.  A  |->  ( ( ( ( S  Dn
F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  Dn T ) `  ( N  -  1 ) ) `
 y ) ) ) `  x )  -  ( ( y  e.  A  |->  ( ( ( ( S  Dn F ) `  ( N  -  1
) ) `  y
)  -  ( ( ( CC  Dn
T ) `  ( N  -  1 ) ) `  y ) ) ) `  B
) )  /  (
x  -  B ) ) )
230115, 159subcld 9982 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( ( S  Dn F ) `
 ( N  - 
1 ) ) `  y )  -  (
( ( CC  Dn T ) `  ( N  -  1
) ) `  y
) )  e.  CC )
231 eqid 2420 . . . . . . . . . 10  |-  ( y  e.  A  |->  ( ( ( ( S  Dn F ) `  ( N  -  1
) ) `  y
)  -  ( ( ( CC  Dn
T ) `  ( N  -  1 ) ) `  y ) ) )  =  ( y  e.  A  |->  ( ( ( ( S  Dn F ) `
 ( N  - 
1 ) ) `  y )  -  (
( ( CC  Dn T ) `  ( N  -  1
) ) `  y
) ) )
232230, 231fmptd 6053 . . . . . . . . 9  |-  ( ph  ->  ( y  e.  A  |->  ( ( ( ( S  Dn F ) `  ( N  -  1 ) ) `
 y )  -  ( ( ( CC  Dn T ) `
 ( N  - 
1 ) ) `  y ) ) ) : A --> CC )
233209, 187, 229, 124, 232, 70eldv 22830 . . . . . . . 8  |-  ( ph  ->  ( B ( S  _D  ( y  e.  A  |->  ( ( ( ( S  Dn
F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  Dn T ) `  ( N  -  1 ) ) `
 y ) ) ) ) 0  <->  ( B  e.  ( ( int `  ( ( TopOpen ` fld )t  S
) ) `  A
)  /\  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( y  e.  A  |->  ( ( ( ( S  Dn
F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  Dn T ) `  ( N  -  1 ) ) `
 y ) ) ) `  x )  -  ( ( y  e.  A  |->  ( ( ( ( S  Dn F ) `  ( N  -  1
) ) `  y
)  -  ( ( ( CC  Dn
T ) `  ( N  -  1 ) ) `  y ) ) ) `  B
) )  /  (
x  -  B ) ) ) lim CC  B
) ) ) )
234228, 233mpbid 213 . . . . . . 7  |-  ( ph  ->  ( B  e.  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  A )  /\  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( y  e.  A  |->  ( ( ( ( S  Dn
F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  Dn T ) `  ( N  -  1 ) ) `
 y ) ) ) `  x )  -  ( ( y  e.  A  |->  ( ( ( ( S  Dn F ) `  ( N  -  1
) ) `  y
)  -  ( ( ( CC  Dn
T ) `  ( N  -  1 ) ) `  y ) ) ) `  B
) )  /  (
x  -  B ) ) ) lim CC  B
) ) )
235234simprd 464 . . . . . 6  |-  ( ph  ->  0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( y  e.  A  |->  ( ( ( ( S  Dn F ) `  ( N  -  1 ) ) `
 y )  -  ( ( ( CC  Dn T ) `
 ( N  - 
1 ) ) `  y ) ) ) `
 x )  -  ( ( y  e.  A  |->  ( ( ( ( S  Dn
F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  Dn T ) `  ( N  -  1 ) ) `
 y ) ) ) `  B ) )  /  ( x  -  B ) ) ) lim CC  B ) )
236 eldifi 3584 . . . . . . . . . 10  |-  ( x  e.  ( A  \  { B } )  ->  x  e.  A )
237 fveq2 5873 . . . . . . . . . . . . . 14  |-  ( y  =  x  ->  (
( ( S  Dn F ) `  ( N  -  1
) ) `  y
)  =  ( ( ( S  Dn
F ) `  ( N  -  1 ) ) `  x ) )
238 fveq2 5873 . . . . . . . . . . . . . 14  |-  ( y  =  x  ->  (
( ( CC  Dn T ) `  ( N  -  1
) ) `  y
)  =  ( ( ( CC  Dn
T ) `  ( N  -  1 ) ) `  x ) )
239237, 238oveq12d 6315 . . . . . . . . . . . . 13  |-  ( y  =  x  ->  (
( ( ( S  Dn F ) `
 ( N  - 
1 ) ) `  y )  -  (
( ( CC  Dn T ) `  ( N  -  1
) ) `  y
) )  =  ( ( ( ( S  Dn F ) `
 ( N  - 
1 ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  1
) ) `  x
) ) )
240 ovex 6325 . . . . . . . . . . . . 13  |-  ( ( ( ( S  Dn F ) `  ( N  -  1
) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  1 ) ) `  x ) )  e.  _V
241239, 231, 240fvmpt 5956 . . . . . . . . . . . 12  |-  ( x  e.  A  ->  (
( y  e.  A  |->  ( ( ( ( S  Dn F ) `  ( N  -  1 ) ) `
 y )  -  ( ( ( CC  Dn T ) `
 ( N  - 
1 ) ) `  y ) ) ) `
 x )  =  ( ( ( ( S  Dn F ) `  ( N  -  1 ) ) `
 x )  -  ( ( ( CC  Dn T ) `
 ( N  - 
1 ) ) `  x ) ) )
242 fveq2 5873 . . . . . . . . . . . . . . . 16  |-  ( y  =  B  ->  (
( ( S  Dn F ) `  ( N  -  1
) ) `  y
)  =  ( ( ( S  Dn
F ) `  ( N  -  1 ) ) `  B ) )
243 fveq2 5873 . . . . . . . . . . . . . . . 16  |-  ( y  =  B  ->  (
( ( CC  Dn T ) `  ( N  -  1
) ) `  y
)  =  ( ( ( CC  Dn
T ) `  ( N  -  1 ) ) `  B ) )
244242, 243oveq12d 6315 . . . . . . . . . . . . . . 15  |-  ( y  =  B  ->  (
( ( ( S  Dn F ) `
 ( N  - 
1 ) ) `  y )  -  (
( ( CC  Dn T ) `  ( N  -  1
) ) `  y
) )  =  ( ( ( ( S  Dn F ) `
 ( N  - 
1 ) ) `  B )  -  (
( ( CC  Dn T ) `  ( N  -  1
) ) `  B
) ) )
245 ovex 6325 . . . . . . . . . . . . . . 15  |-  ( ( ( ( S  Dn F ) `  ( N  -  1
) ) `  B
)  -  ( ( ( CC  Dn
T ) `  ( N  -  1 ) ) `  B ) )  e.  _V
246244, 231, 245fvmpt 5956 . . . . . . . . . . . . . 14  |-  ( B  e.  A  ->  (
( y  e.  A  |->  ( ( ( ( S  Dn F ) `  ( N  -  1 ) ) `
 y )  -  ( ( ( CC  Dn T ) `
 ( N  - 
1 ) ) `  y ) ) ) `
 B )  =  ( ( ( ( S  Dn F ) `  ( N  -  1 ) ) `
 B )  -  ( ( ( CC  Dn T ) `
 ( N  - 
1 ) ) `  B ) ) )
24760, 246syl 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 ) ) )
24868, 69, 70, 108, 77, 78dvntaylp0 23304 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( CC  Dn T ) `
 ( N  - 
1 ) ) `  B )  =  ( ( ( S  Dn F ) `  ( N  -  1
) ) `  B
) )
249248oveq2d 6313 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( S  Dn F ) `  ( N  -  1 ) ) `
 B )  -  ( ( ( CC  Dn T ) `
 ( N  - 
1 ) ) `  B ) )  =  ( ( ( ( S  Dn F ) `  ( N  -  1 ) ) `
 B )  -  ( ( ( S  Dn F ) `
 ( N  - 
1 ) ) `  B ) ) )
250114, 60ffvelrnd 6030 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( S  Dn F ) `
 ( N  - 
1 ) ) `  B )  e.  CC )
251250subidd 9970 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( S  Dn F ) `  ( N  -  1 ) ) `
 B )  -  ( ( ( S  Dn F ) `
 ( N  - 
1 ) ) `  B ) )  =  0 )
252247, 249, 2513eqtrd 2465 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( y  e.  A  |->  ( ( ( ( S  Dn
F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  Dn T ) `  ( N  -  1 ) ) `
 y ) ) ) `  B )  =  0 )
253241, 252oveqan12rd 6317 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( y  e.  A  |->  ( ( ( ( S  Dn
F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  Dn T ) `  ( N  -  1 ) ) `
 y ) ) ) `  x )  -  ( ( y  e.  A  |->  ( ( ( ( S  Dn F ) `  ( N  -  1
) ) `  y
)  -  ( ( ( CC  Dn
T ) `  ( N  -  1 ) ) `  y ) ) ) `  B
) )  =  ( ( ( ( ( S  Dn F ) `  ( N  -  1 ) ) `
 x )  -  ( ( ( CC  Dn T ) `
 ( N  - 
1 ) ) `  x ) )  - 
0 ) )
254114ffvelrnda 6029 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( S  Dn F ) `  ( N  -  1
) ) `  x
)  e.  CC )
255132sselda 3461 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  CC )
256157ffvelrnda 6029 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  CC )  ->  ( ( ( CC  Dn
T ) `  ( N  -  1 ) ) `  x )  e.  CC )
257255, 256syldan 472 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( CC  Dn T ) `  ( N  -  1
) ) `  x
)  e.  CC )
258254, 257subcld 9982 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( ( S  Dn F ) `
 ( N  - 
1 ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  1
) ) `  x
) )  e.  CC )
259258subid1d 9971 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( ( ( S  Dn F ) `  ( N  -  1 ) ) `
 x )  -  ( ( ( CC  Dn T ) `
 ( N  - 
1 ) ) `  x ) )  - 
0 )  =  ( ( ( ( S  Dn F ) `
 ( N  - 
1 ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  1
) ) `  x
) ) )
260253, 259eqtr2d 2462 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( ( S  Dn F ) `
 ( N  - 
1 ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  1
) ) `  x
) )  =  ( ( ( y  e.  A  |->  ( ( ( ( S  Dn
F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  Dn T ) `  ( N  -  1 ) ) `
 y ) ) ) `  x )  -  ( ( y  e.  A  |->  ( ( ( ( S  Dn F ) `  ( N  -  1
) ) `  y
)  -  ( ( ( CC  Dn
T ) `  ( N  -  1 ) ) `  y ) ) ) `  B
) ) )
261236, 260sylan2 476 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( ( ( S  Dn F ) `  ( N  -  1 ) ) `
 x )  -  ( ( ( CC  Dn T ) `
 ( N  - 
1 ) ) `  x ) )  =  ( ( ( y  e.  A  |->  ( ( ( ( S  Dn F ) `  ( N  -  1
) ) `  y
)  -  ( ( ( CC  Dn
T ) `  ( N  -  1 ) ) `  y ) ) ) `  x
)  -  ( ( y  e.  A  |->  ( ( ( ( S  Dn F ) `
 ( N  - 
1 ) ) `  y )  -  (
( ( CC  Dn T ) `  ( N  -  1
) ) `  y
) ) ) `  B ) ) )
262132ssdifssd 3600 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  \  { B } )  C_  CC )
263262sselda 3461 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  x  e.  CC )
264132, 60sseldd 3462 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  CC )
265264adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  B  e.  CC )
266263, 265subcld 9982 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( x  -  B
)  e.  CC )
267266exp1d 12404 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( x  -  B ) ^ 1 )  =  ( x  -  B ) )
268261, 267oveq12d 6315 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( ( ( ( S  Dn
F ) `  ( N  -  1 ) ) `  x )  -  ( ( ( CC  Dn T ) `  ( N  -  1 ) ) `
 x ) )  /  ( ( x  -  B ) ^
1 ) )  =  ( ( ( ( y  e.  A  |->  ( ( ( ( S  Dn F ) `
 ( N  - 
1 ) ) `  y )  -  (
( ( CC  Dn T ) `  ( N  -  1
) ) `  y
) ) ) `  x )  -  (
( y  e.  A  |->  ( ( ( ( S  Dn F ) `  ( N  -  1 ) ) `
 y )  -  ( ( ( CC  Dn T ) `
 ( N  - 
1 ) ) `  y ) ) ) `
 B ) )  /  ( x  -  B ) ) )
269268mpteq2dva 4504 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  - 
1 ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  1
) ) `  x
) )  /  (
( x  -  B
) ^ 1 ) ) )  =  ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( y  e.  A  |->  ( ( ( ( S  Dn F ) `  ( N  -  1 ) ) `
 y )  -  ( ( ( CC  Dn T ) `
 ( N  - 
1 ) ) `  y ) ) ) `
 x )  -  ( ( y  e.  A  |->  ( ( ( ( S  Dn
F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  Dn T ) `  ( N  -  1 ) ) `
 y ) ) ) `  B ) )  /  ( x  -  B ) ) ) )
270269oveq1d 6312 . . . . . 6  |-  ( ph  ->  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  - 
1 ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  1
) ) `  x
) )  /  (
( x  -  B
) ^ 1 ) ) ) lim CC  B
)  =  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( y  e.  A  |->  ( ( ( ( S  Dn F ) `  ( N  -  1 ) ) `
 y )  -  ( ( ( CC  Dn T ) `
 ( N  - 
1 ) ) `  y ) ) ) `
 x )  -  ( ( y  e.  A  |->  ( ( ( ( S  Dn
F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  Dn T ) `  ( N  -  1 ) ) `
 y ) ) ) `  B ) )  /  ( x  -  B ) ) ) lim CC  B ) )
271235, 270eleqtrrd 2511 . . . . 5  |-  ( ph  ->  0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  1
) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  1 ) ) `  x ) )  /  ( ( x  -  B ) ^ 1 ) ) ) lim CC  B ) )
272271a1i 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 ) )
274273expr 618 . . . . . 6  |-  ( (
ph  /\  n  e.  ( 1..^ N ) )  ->  ( 0  e.  ( ( y  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  -  n ) ) `  y )  -  (
( ( CC  Dn T ) `  ( N  -  n
) ) `  y
) )  /  (
( y  -  B
) ^ n ) ) ) lim CC  B
)  ->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  -  ( n  +  1
) ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  (
n  +  1 ) ) ) `  x
) )  /  (
( x  -  B
) ^ ( n  +  1 ) ) ) ) lim CC  B
) ) )
275274expcom 436 . . . . 5  |-  ( n  e.  ( 1..^ N )  ->  ( ph  ->  ( 0  e.  ( ( y  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  -  n ) ) `  y )  -  (
( ( CC  Dn T ) `  ( N  -  n
) ) `  y
) )  /  (
( y  -  B
) ^ n ) ) ) lim CC  B
)  ->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  -  ( n  +  1
) ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  (
n  +  1 ) ) ) `  x
) )  /  (
( x  -  B
) ^ ( n  +  1 ) ) ) ) lim CC  B
) ) ) )
276275a2d 29 . . . 4  |-  ( n  e.  ( 1..^ N )  ->  ( ( ph  ->  0  e.  ( ( y  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  -  n ) ) `  y )  -  (
( ( CC  Dn T ) `  ( N  -  n
) ) `  y
) )  /  (
( y  -  B
) ^ n ) ) ) lim CC  B
) )  ->  ( ph  ->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  -  ( n  +  1
) ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  (
n  +  1 ) ) ) `  x
) )  /  (
( x  -  B
) ^ ( n  +  1 ) ) ) ) lim CC  B
) ) ) )
27715, 35, 47, 59, 272, 276fzind2 12016 . . 3  |-  ( N  e.  ( 1 ... N )  ->  ( ph  ->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  -  N ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  N
) ) `  x
) )  /  (
( x  -  B
) ^ N ) ) ) lim CC  B
) ) )
2783, 277mpcom 37 . 2  |-  ( ph  ->  0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  Dn F ) `  ( N  -  N
) ) `  x
)  -  ( ( ( CC  Dn
T ) `  ( N  -  N )
) `  x )
)  /  ( ( x  -  B ) ^ N ) ) ) lim CC  B ) )
279119subidd 9970 . . . . . . . . . 10  |-  ( ph  ->  ( N  -  N
)  =  0 )
280279fveq2d 5877 . . . . . . . . 9  |-  ( ph  ->  ( ( S  Dn F ) `  ( N  -  N
) )  =  ( ( S  Dn
F ) `  0
) )
281 dvn0 22855 . . . . . . . . . 10  |-  ( ( S  C_  CC  /\  F  e.  ( CC  ^pm  S
) )  ->  (
( S  Dn
F ) `  0
)  =  F )
282124, 84, 281syl2anc 665 . . . . . . . . 9  |-  ( ph  ->  ( ( S  Dn F ) ` 
0 )  =  F )
283280, 282eqtrd 2461 . . . . . . . 8  |-  ( ph  ->  ( ( S  Dn F ) `  ( N  -  N
) )  =  F )
284283fveq1d 5875 . . . . . . 7  |-  ( ph  ->  ( ( ( S  Dn F ) `
 ( N  -  N ) ) `  x )  =  ( F `  x ) )
285279fveq2d 5877 . . . . . . . . 9  |-  ( ph  ->  ( ( CC  Dn T ) `  ( N  -  N
) )  =  ( ( CC  Dn
T ) `  0
) )
286 dvn0 22855 . . . . . . . . . 10  |-  ( ( CC  C_  CC  /\  T  e.  ( CC  ^pm  CC ) )  ->  (
( CC  Dn
T ) `  0
)  =  T )
287193, 199, 286sylancr 667 . . . . . . . . 9  |-  ( ph  ->  ( ( CC  Dn T ) ` 
0 )  =  T )
288285, 287eqtrd 2461 . . . . . . . 8  |-  ( ph  ->  ( ( CC  Dn T ) `  ( N  -  N
) )  =  T )
289288fveq1d 5875 . . . . . . 7  |-  ( ph  ->  ( ( ( CC  Dn T ) `
 ( N  -  N ) ) `  x )  =  ( T `  x ) )
290284, 289oveq12d 6315 . . . . . 6  |-  ( ph  ->  ( ( ( ( S  Dn F ) `  ( N  -  N ) ) `
 x )  -  ( ( ( CC  Dn T ) `
 ( N  -  N ) ) `  x ) )  =  ( ( F `  x )  -  ( T `  x )
) )
291290oveq1d 6312 . . . . 5  |-  ( ph  ->  ( ( ( ( ( S  Dn
F ) `  ( N  -  N )
) `  x )  -  ( ( ( CC  Dn T ) `  ( N  -  N ) ) `
 x ) )  /  ( ( x  -  B ) ^ N ) )  =  ( ( ( F `
 x )  -  ( T `  x ) )  /  ( ( x  -  B ) ^ N ) ) )
292291mpteq2dv 4505 . . . 4  |-  ( ph  ->  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  -  N ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  N
) ) `  x
) )  /  (
( x  -  B
) ^ N ) ) )  =  ( x  e.  ( A 
\  { B }
)  |->  ( ( ( F `  x )  -  ( T `  x ) )  / 
( ( x  -  B ) ^ N
) ) ) )
293 taylthlem1.r . . . 4  |-  R  =  ( x  e.  ( A  \  { B } )  |->  ( ( ( F `  x
)  -  ( T `
 x ) )  /  ( ( x  -  B ) ^ N ) ) )
294292, 293syl6eqr 2479 . . 3  |-  ( ph  ->  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  -  N ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  N
) ) `  x
) )  /  (
( x  -  B
) ^ N ) ) )  =  R )
295294oveq1d 6312 . 2  |-  ( ph  ->  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  Dn F ) `
 ( N  -  N ) ) `  x )  -  (
( ( CC  Dn T ) `  ( N  -  N
) ) `  x
) )  /  (
( x  -  B
) ^ N ) ) ) lim CC  B
)  =  ( R lim
CC  B ) )
296278, 295eleqtrd 2510 1  |-  ( ph  ->  0  e.  ( R lim
CC  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1867   _Vcvv 3078    \ cdif 3430    i^i cin 3432    C_ wss 3433   {csn 3993   {cpr 3995   U.cuni 4213   class class class wbr 4417    |-> cmpt 4476   dom cdm 4846   Fun wfun 5587   -->wf 5589   ` cfv 5593  (class class class)co 6297    ^m cmap 7472    ^pm cpm 7473   CCcc 9533   RRcr 9534   0cc0 9535   1c1 9536    + caddc 9538    - cmin 9856    / cdiv 10265   NNcn 10605   NN0cn0 10865   ZZ>=cuz 11155   ...cfz 11778  ..^cfzo 11909   ^cexp 12265   ↾t crest 15297   TopOpenctopn 15298  ℂfldccnfld 18948   Topctop 19894  TopOnctopon 19895   intcnt 20009   lim CC climc 22794    _D cdv 22795    Dncdvn 22796   Tayl ctayl 23285
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-rep 4530  ax-sep 4540  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6589  ax-inf2 8144  ax-cnex 9591  ax-resscn 9592  ax-1cn 9593  ax-icn 9594  ax-addcl 9595  ax-addrcl 9596  ax-mulcl 9597  ax-mulrcl 9598  ax-mulcom 9599  ax-addass 9600  ax-mulass 9601  ax-distr 9602  ax-i2m1 9603  ax-1ne0 9604  ax-1rid 9605  ax-rnegex 9606  ax-rrecex 9607  ax-cnre 9608  ax-pre-lttri 9609  ax-pre-lttrn 9610  ax-pre-ltadd 9611  ax-pre-mulgt0 9612  ax-pre-sup 9613  ax-addf 9614  ax-mulf 9615
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-reu 2780  df-rmo 2781  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-pss 3449  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4214  df-int 4250  df-iun 4295  df-iin 4296  df-br 4418  df-opab 4477  df-mpt 4478  df-tr 4513  df-eprel 4757  df-id 4761  df-po 4767  df-so 4768  df-fr 4805  df-se 4806  df-we 4807  df-xp 4852  df-rel 4853  df-cnv 4854  df-co 4855  df-dm 4856  df-rn 4857  df-res 4858  df-ima 4859  df-pred 5391  df-ord 5437  df-on 5438  df-lim 5439  df-suc 5440  df-iota 5557  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-isom 5602  df-riota 6259  df-ov 6300  df-oprab 6301  df-mpt2 6302  df-of 6537  df-om 6699  df-1st 6799  df-2nd 6800  df-supp 6918  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-2o 7183  df-oadd 7186  df-er 7363  df-map 7474  df-pm 7475  df-ixp 7523  df-en 7570  df-dom 7571  df-sdom 7572  df-fin 7573  df-fsupp 7882  df-fi 7923  df-sup 7954  df-inf 7955  df-oi 8023  df-card 8370  df-cda 8594  df-pnf 9673  df-mnf 9674  df-xr 9675  df-ltxr 9676  df-le 9677  df-sub 9858  df-neg 9859  df-div 10266  df-nn 10606  df-2 10664  df-3 10665  df-4 10666  df-5 10667  df-6 10668  df-7 10669  df-8 10670  df-9 10671  df-10 10672  df-n0 10866  df-z 10934  df-dec 11048  df-uz 11156  df-q 11261  df-rp 11299  df-xneg 11405  df-xadd 11406  df-xmul 11407  df-icc 11638  df-fz 11779  df-fzo 11910  df-seq 12207  df-exp 12266  df-fac 12453  df-hash 12509  df-cj 13141  df-re 13142  df-im 13143  df-sqrt 13277  df-abs 13278  df-clim 13530  df-sum 13731  df-struct 15101  df-ndx 15102  df-slot 15103  df-base 15104  df-sets 15105  df-ress 15106  df-plusg 15181  df-mulr 15182  df-starv 15183  df-sca 15184  df-vsca 15185  df-ip 15186  df-tset 15187  df-ple 15188  df-ds 15190  df-unif 15191  df-hom 15192  df-cco 15193  df-rest 15299  df-topn 15300  df-0g 15318  df-gsum 15319  df-topgen 15320  df-pt 15321  df-prds 15324  df-xrs 15378  df-qtop 15384  df-imas 15385  df-xps 15388  df-mre 15470  df-mrc 15471  df-acs 15473  df-mgm 16466  df-sgrp 16505  df-mnd 16515  df-submnd 16561  df-grp 16651  df-minusg 16652  df-mulg 16654  df-cntz 16949  df-cmn 17410  df-abl 17411  df-mgp 17702  df-ur 17714  df-ring 17760  df-cring 17761  df-psmet 18940  df-xmet 18941  df-met 18942  df-bl 18943  df-mopn 18944  df-fbas 18945  df-fg 18946  df-cnfld 18949  df-top 19898  df-bases 19899  df-topon 19900  df-topsp 19901  df-cld 20011  df-ntr 20012  df-cls 20013  df-nei 20091  df-lp 20129  df-perf 20130  df-cn 20220  df-cnp 20221  df-haus 20308  df-tx 20554  df-hmeo 20747  df-fil 20838  df-fm 20930  df-flim 20931  df-flf 20932  df-tsms 21118  df-xms 21312  df-ms 21313  df-tms 21314  df-cncf 21887  df-limc 22798  df-dv 22799  df-dvn 22800  df-tayl 23287
This theorem is referenced by:  taylth  23307
  Copyright terms: Public domain W3C validator