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

Theorem taylthlem1 20242
Description: Lemma for taylth 20244. 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 20244 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  D n 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  D n F ) `
 ( N  -  n ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  n )
) `  y )
)  /  ( ( y  -  B ) ^ n ) ) ) lim CC  B ) ) )  ->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  ( n  +  1
) ) ) `  x )  -  (
( ( CC  D n 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 11037 . . . 4  |-  ( N  e.  NN  <->  N  e.  ( 1 ... N
) )
31, 2sylib 189 . . 3  |-  ( ph  ->  N  e.  ( 1 ... N ) )
4 oveq2 6048 . . . . . . . . . . . 12  |-  ( m  =  1  ->  ( N  -  m )  =  ( N  - 
1 ) )
54fveq2d 5691 . . . . . . . . . . 11  |-  ( m  =  1  ->  (
( S  D n F ) `  ( N  -  m )
)  =  ( ( S  D n F ) `  ( N  -  1 ) ) )
65fveq1d 5689 . . . . . . . . . 10  |-  ( m  =  1  ->  (
( ( S  D n F ) `  ( N  -  m )
) `  x )  =  ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 x ) )
74fveq2d 5691 . . . . . . . . . . 11  |-  ( m  =  1  ->  (
( CC  D n T ) `  ( N  -  m )
)  =  ( ( CC  D n T ) `  ( N  -  1 ) ) )
87fveq1d 5689 . . . . . . . . . 10  |-  ( m  =  1  ->  (
( ( CC  D n T ) `  ( N  -  m )
) `  x )  =  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 x ) )
96, 8oveq12d 6058 . . . . . . . . 9  |-  ( m  =  1  ->  (
( ( ( S  D n F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  m )
) `  x )
)  =  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 x ) ) )
10 oveq2 6048 . . . . . . . . 9  |-  ( m  =  1  ->  (
( x  -  B
) ^ m )  =  ( ( x  -  B ) ^
1 ) )
119, 10oveq12d 6058 . . . . . . . 8  |-  ( m  =  1  ->  (
( ( ( ( S  D n F ) `  ( N  -  m ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  m ) ) `  x ) )  / 
( ( x  -  B ) ^ m
) )  =  ( ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  - 
1 ) ) `  x ) )  / 
( ( x  -  B ) ^ 1 ) ) )
1211mpteq2dv 4256 . . . . . . 7  |-  ( m  =  1  ->  (
x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  D n F ) `  ( N  -  m )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  m ) ) `
 x ) )  /  ( ( x  -  B ) ^
m ) ) )  =  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  - 
1 ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  x ) )  /  ( ( x  -  B ) ^ 1 ) ) ) )
1312oveq1d 6055 . . . . . 6  |-  ( m  =  1  ->  (
( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  m )
) `  x )
)  /  ( ( x  -  B ) ^ m ) ) ) lim CC  B )  =  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  - 
1 ) ) `  x ) )  / 
( ( x  -  B ) ^ 1 ) ) ) lim CC  B ) )
1413eleq2d 2471 . . . . 5  |-  ( m  =  1  ->  (
0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  D n F ) `  ( N  -  m )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  m ) ) `
 x ) )  /  ( ( x  -  B ) ^
m ) ) ) lim
CC  B )  <->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  - 
1 ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  x ) )  /  ( ( x  -  B ) ^ 1 ) ) ) lim CC  B ) ) )
1514imbi2d 308 . . . 4  |-  ( m  =  1  ->  (
( ph  ->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  m )
) `  x )
)  /  ( ( x  -  B ) ^ m ) ) ) lim CC  B ) )  <->  ( ph  ->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  - 
1 ) ) `  x ) )  / 
( ( x  -  B ) ^ 1 ) ) ) lim CC  B ) ) ) )
16 oveq2 6048 . . . . . . . . . . . . 13  |-  ( m  =  n  ->  ( N  -  m )  =  ( N  -  n ) )
1716fveq2d 5691 . . . . . . . . . . . 12  |-  ( m  =  n  ->  (
( S  D n F ) `  ( N  -  m )
)  =  ( ( S  D n F ) `  ( N  -  n ) ) )
1817fveq1d 5689 . . . . . . . . . . 11  |-  ( m  =  n  ->  (
( ( S  D n F ) `  ( N  -  m )
) `  x )  =  ( ( ( S  D n F ) `  ( N  -  n ) ) `
 x ) )
1916fveq2d 5691 . . . . . . . . . . . 12  |-  ( m  =  n  ->  (
( CC  D n T ) `  ( N  -  m )
)  =  ( ( CC  D n T ) `  ( N  -  n ) ) )
2019fveq1d 5689 . . . . . . . . . . 11  |-  ( m  =  n  ->  (
( ( CC  D n T ) `  ( N  -  m )
) `  x )  =  ( ( ( CC  D n T ) `  ( N  -  n ) ) `
 x ) )
2118, 20oveq12d 6058 . . . . . . . . . 10  |-  ( m  =  n  ->  (
( ( ( S  D n F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  m )
) `  x )
)  =  ( ( ( ( S  D n F ) `  ( N  -  n )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  n ) ) `
 x ) ) )
22 oveq2 6048 . . . . . . . . . 10  |-  ( m  =  n  ->  (
( x  -  B
) ^ m )  =  ( ( x  -  B ) ^
n ) )
2321, 22oveq12d 6058 . . . . . . . . 9  |-  ( m  =  n  ->  (
( ( ( ( S  D n F ) `  ( N  -  m ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  m ) ) `  x ) )  / 
( ( x  -  B ) ^ m
) )  =  ( ( ( ( ( S  D n F ) `  ( N  -  n ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  n ) ) `  x ) )  / 
( ( x  -  B ) ^ n
) ) )
2423mpteq2dv 4256 . . . . . . . 8  |-  ( m  =  n  ->  (
x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  D n F ) `  ( N  -  m )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  m ) ) `
 x ) )  /  ( ( x  -  B ) ^
m ) ) )  =  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  n ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  n )
) `  x )
)  /  ( ( x  -  B ) ^ n ) ) ) )
25 fveq2 5687 . . . . . . . . . . 11  |-  ( x  =  y  ->  (
( ( S  D n F ) `  ( N  -  n )
) `  x )  =  ( ( ( S  D n F ) `  ( N  -  n ) ) `
 y ) )
26 fveq2 5687 . . . . . . . . . . 11  |-  ( x  =  y  ->  (
( ( CC  D n T ) `  ( N  -  n )
) `  x )  =  ( ( ( CC  D n T ) `  ( N  -  n ) ) `
 y ) )
2725, 26oveq12d 6058 . . . . . . . . . 10  |-  ( x  =  y  ->  (
( ( ( S  D n F ) `
 ( N  -  n ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  n )
) `  x )
)  =  ( ( ( ( S  D n F ) `  ( N  -  n )
) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  n ) ) `
 y ) ) )
28 oveq1 6047 . . . . . . . . . . 11  |-  ( x  =  y  ->  (
x  -  B )  =  ( y  -  B ) )
2928oveq1d 6055 . . . . . . . . . 10  |-  ( x  =  y  ->  (
( x  -  B
) ^ n )  =  ( ( y  -  B ) ^
n ) )
3027, 29oveq12d 6058 . . . . . . . . 9  |-  ( x  =  y  ->  (
( ( ( ( S  D n F ) `  ( N  -  n ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  n ) ) `  x ) )  / 
( ( x  -  B ) ^ n
) )  =  ( ( ( ( ( S  D n F ) `  ( N  -  n ) ) `
 y )  -  ( ( ( CC  D n T ) `
 ( N  -  n ) ) `  y ) )  / 
( ( y  -  B ) ^ n
) ) )
3130cbvmptv 4260 . . . . . . . 8  |-  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `  ( N  -  n ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  n ) ) `  x ) )  / 
( ( x  -  B ) ^ n
) ) )  =  ( y  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  n ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  n )
) `  y )
)  /  ( ( y  -  B ) ^ n ) ) )
3224, 31syl6eq 2452 . . . . . . 7  |-  ( m  =  n  ->  (
x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  D n F ) `  ( N  -  m )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  m ) ) `
 x ) )  /  ( ( x  -  B ) ^
m ) ) )  =  ( y  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  n ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  n )
) `  y )
)  /  ( ( y  -  B ) ^ n ) ) ) )
3332oveq1d 6055 . . . . . 6  |-  ( m  =  n  ->  (
( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  m )
) `  x )
)  /  ( ( x  -  B ) ^ m ) ) ) lim CC  B )  =  ( ( y  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `  ( N  -  n ) ) `
 y )  -  ( ( ( CC  D n T ) `
 ( N  -  n ) ) `  y ) )  / 
( ( y  -  B ) ^ n
) ) ) lim CC  B ) )
3433eleq2d 2471 . . . . 5  |-  ( m  =  n  ->  (
0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  D n F ) `  ( N  -  m )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  m ) ) `
 x ) )  /  ( ( x  -  B ) ^
m ) ) ) lim
CC  B )  <->  0  e.  ( ( y  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  n ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  n )
) `  y )
)  /  ( ( y  -  B ) ^ n ) ) ) lim CC  B ) ) )
3534imbi2d 308 . . . 4  |-  ( m  =  n  ->  (
( ph  ->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  m )
) `  x )
)  /  ( ( x  -  B ) ^ m ) ) ) lim CC  B ) )  <->  ( ph  ->  0  e.  ( ( y  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `  ( N  -  n ) ) `
 y )  -  ( ( ( CC  D n T ) `
 ( N  -  n ) ) `  y ) )  / 
( ( y  -  B ) ^ n
) ) ) lim CC  B ) ) ) )
36 oveq2 6048 . . . . . . . . . . . 12  |-  ( m  =  ( n  + 
1 )  ->  ( N  -  m )  =  ( N  -  ( n  +  1
) ) )
3736fveq2d 5691 . . . . . . . . . . 11  |-  ( m  =  ( n  + 
1 )  ->  (
( S  D n F ) `  ( N  -  m )
)  =  ( ( S  D n F ) `  ( N  -  ( n  + 
1 ) ) ) )
3837fveq1d 5689 . . . . . . . . . 10  |-  ( m  =  ( n  + 
1 )  ->  (
( ( S  D n F ) `  ( N  -  m )
) `  x )  =  ( ( ( S  D n F ) `  ( N  -  ( n  + 
1 ) ) ) `
 x ) )
3936fveq2d 5691 . . . . . . . . . . 11  |-  ( m  =  ( n  + 
1 )  ->  (
( CC  D n T ) `  ( N  -  m )
)  =  ( ( CC  D n T ) `  ( N  -  ( n  + 
1 ) ) ) )
4039fveq1d 5689 . . . . . . . . . 10  |-  ( m  =  ( n  + 
1 )  ->  (
( ( CC  D n T ) `  ( N  -  m )
) `  x )  =  ( ( ( CC  D n T ) `  ( N  -  ( n  + 
1 ) ) ) `
 x ) )
4138, 40oveq12d 6058 . . . . . . . . 9  |-  ( m  =  ( n  + 
1 )  ->  (
( ( ( S  D n F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  m )
) `  x )
)  =  ( ( ( ( S  D n F ) `  ( N  -  ( n  +  1 ) ) ) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  ( n  + 
1 ) ) ) `
 x ) ) )
42 oveq2 6048 . . . . . . . . 9  |-  ( m  =  ( n  + 
1 )  ->  (
( x  -  B
) ^ m )  =  ( ( x  -  B ) ^
( n  +  1 ) ) )
4341, 42oveq12d 6058 . . . . . . . 8  |-  ( m  =  ( n  + 
1 )  ->  (
( ( ( ( S  D n F ) `  ( N  -  m ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  m ) ) `  x ) )  / 
( ( x  -  B ) ^ m
) )  =  ( ( ( ( ( S  D n F ) `  ( N  -  ( n  + 
1 ) ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  ( n  +  1
) ) ) `  x ) )  / 
( ( x  -  B ) ^ (
n  +  1 ) ) ) )
4443mpteq2dv 4256 . . . . . . 7  |-  ( m  =  ( n  + 
1 )  ->  (
x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  D n F ) `  ( N  -  m )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  m ) ) `
 x ) )  /  ( ( x  -  B ) ^
m ) ) )  =  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  ( n  +  1
) ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  ( n  +  1 ) ) ) `  x ) )  /  ( ( x  -  B ) ^ ( n  + 
1 ) ) ) ) )
4544oveq1d 6055 . . . . . 6  |-  ( m  =  ( n  + 
1 )  ->  (
( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  m )
) `  x )
)  /  ( ( x  -  B ) ^ m ) ) ) lim CC  B )  =  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `  ( N  -  ( n  + 
1 ) ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  ( n  +  1
) ) ) `  x ) )  / 
( ( x  -  B ) ^ (
n  +  1 ) ) ) ) lim CC  B ) )
4645eleq2d 2471 . . . . 5  |-  ( m  =  ( n  + 
1 )  ->  (
0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  D n F ) `  ( N  -  m )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  m ) ) `
 x ) )  /  ( ( x  -  B ) ^
m ) ) ) lim
CC  B )  <->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  ( n  +  1
) ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  ( n  +  1 ) ) ) `  x ) )  /  ( ( x  -  B ) ^ ( n  + 
1 ) ) ) ) lim CC  B ) ) )
4746imbi2d 308 . . . 4  |-  ( m  =  ( n  + 
1 )  ->  (
( ph  ->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  m )
) `  x )
)  /  ( ( x  -  B ) ^ m ) ) ) lim CC  B ) )  <->  ( ph  ->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `  ( N  -  ( n  + 
1 ) ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  ( n  +  1
) ) ) `  x ) )  / 
( ( x  -  B ) ^ (
n  +  1 ) ) ) ) lim CC  B ) ) ) )
48 oveq2 6048 . . . . . . . . . . . 12  |-  ( m  =  N  ->  ( N  -  m )  =  ( N  -  N ) )
4948fveq2d 5691 . . . . . . . . . . 11  |-  ( m  =  N  ->  (
( S  D n F ) `  ( N  -  m )
)  =  ( ( S  D n F ) `  ( N  -  N ) ) )
5049fveq1d 5689 . . . . . . . . . 10  |-  ( m  =  N  ->  (
( ( S  D n F ) `  ( N  -  m )
) `  x )  =  ( ( ( S  D n F ) `  ( N  -  N ) ) `
 x ) )
5148fveq2d 5691 . . . . . . . . . . 11  |-  ( m  =  N  ->  (
( CC  D n T ) `  ( N  -  m )
)  =  ( ( CC  D n T ) `  ( N  -  N ) ) )
5251fveq1d 5689 . . . . . . . . . 10  |-  ( m  =  N  ->  (
( ( CC  D n T ) `  ( N  -  m )
) `  x )  =  ( ( ( CC  D n T ) `  ( N  -  N ) ) `
 x ) )
5350, 52oveq12d 6058 . . . . . . . . 9  |-  ( m  =  N  ->  (
( ( ( S  D n F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  m )
) `  x )
)  =  ( ( ( ( S  D n F ) `  ( N  -  N )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  N ) ) `
 x ) ) )
54 oveq2 6048 . . . . . . . . 9  |-  ( m  =  N  ->  (
( x  -  B
) ^ m )  =  ( ( x  -  B ) ^ N ) )
5553, 54oveq12d 6058 . . . . . . . 8  |-  ( m  =  N  ->  (
( ( ( ( S  D n F ) `  ( N  -  m ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  m ) ) `  x ) )  / 
( ( x  -  B ) ^ m
) )  =  ( ( ( ( ( S  D n F ) `  ( N  -  N ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  N ) ) `  x ) )  / 
( ( x  -  B ) ^ N
) ) )
5655mpteq2dv 4256 . . . . . . 7  |-  ( m  =  N  ->  (
x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  D n F ) `  ( N  -  m )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  m ) ) `
 x ) )  /  ( ( x  -  B ) ^
m ) ) )  =  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  N ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  N )
) `  x )
)  /  ( ( x  -  B ) ^ N ) ) ) )
5756oveq1d 6055 . . . . . 6  |-  ( m  =  N  ->  (
( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  m )
) `  x )
)  /  ( ( x  -  B ) ^ m ) ) ) lim CC  B )  =  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `  ( N  -  N ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  N ) ) `  x ) )  / 
( ( x  -  B ) ^ N
) ) ) lim CC  B ) )
5857eleq2d 2471 . . . . 5  |-  ( m  =  N  ->  (
0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  D n F ) `  ( N  -  m )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  m ) ) `
 x ) )  /  ( ( x  -  B ) ^
m ) ) ) lim
CC  B )  <->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  N ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  N )
) `  x )
)  /  ( ( x  -  B ) ^ N ) ) ) lim CC  B ) ) )
5958imbi2d 308 . . . 4  |-  ( m  =  N  ->  (
( ph  ->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  m ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  m )
) `  x )
)  /  ( ( x  -  B ) ^ m ) ) ) lim CC  B ) )  <->  ( ph  ->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `  ( N  -  N ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  N ) ) `  x ) )  / 
( ( x  -  B ) ^ N
) ) ) lim CC  B ) ) ) )
60 taylthlem1.b . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  A )
61 fveq2 5687 . . . . . . . . . . . . . 14  |-  ( y  =  B  ->  (
( ( S  D n F ) `  N
) `  y )  =  ( ( ( S  D n F ) `  N ) `
 B ) )
62 fveq2 5687 . . . . . . . . . . . . . 14  |-  ( y  =  B  ->  (
( ( CC  D n T ) `  N
) `  y )  =  ( ( ( CC  D n T ) `  N ) `
 B ) )
6361, 62oveq12d 6058 . . . . . . . . . . . . 13  |-  ( y  =  B  ->  (
( ( ( S  D n F ) `
 N ) `  y )  -  (
( ( CC  D n T ) `  N
) `  y )
)  =  ( ( ( ( S  D n F ) `  N
) `  B )  -  ( ( ( CC  D n T ) `  N ) `
 B ) ) )
64 eqid 2404 . . . . . . . . . . . . 13  |-  ( y  e.  A  |->  ( ( ( ( S  D n F ) `  N
) `  y )  -  ( ( ( CC  D n T ) `  N ) `
 y ) ) )  =  ( y  e.  A  |->  ( ( ( ( S  D n F ) `  N
) `  y )  -  ( ( ( CC  D n T ) `  N ) `
 y ) ) )
65 ovex 6065 . . . . . . . . . . . . 13  |-  ( ( ( ( S  D n F ) `  N
) `  B )  -  ( ( ( CC  D n T ) `  N ) `
 B ) )  e.  _V
6663, 64, 65fvmpt 5765 . . . . . . . . . . . 12  |-  ( B  e.  A  ->  (
( y  e.  A  |->  ( ( ( ( S  D n F ) `  N ) `
 y )  -  ( ( ( CC  D n T ) `
 N ) `  y ) ) ) `
 B )  =  ( ( ( ( S  D n F ) `  N ) `
 B )  -  ( ( ( CC  D n T ) `
 N ) `  B ) ) )
6760, 66syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  N
) `  y )  -  ( ( ( CC  D n T ) `  N ) `
 y ) ) ) `  B )  =  ( ( ( ( S  D n F ) `  N
) `  B )  -  ( ( ( CC  D n 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 10230 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  NN0 )
72 nn0uz 10476 . . . . . . . . . . . . . . 15  |-  NN0  =  ( ZZ>= `  0 )
7371, 72syl6eleq 2494 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  ( ZZ>= ` 
0 ) )
74 eluzfz2b 11022 . . . . . . . . . . . . . 14  |-  ( N  e.  ( ZZ>= `  0
)  <->  N  e.  (
0 ... N ) )
7573, 74sylib 189 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  ( 0 ... N ) )
76 taylthlem1.d . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( ( S  D n F ) `
 N )  =  A )
7760, 76eleqtrrd 2481 . . . . . . . . . . . . 13  |-  ( ph  ->  B  e.  dom  (
( S  D n F ) `  N
) )
78 taylthlem1.t . . . . . . . . . . . . 13  |-  T  =  ( N ( S Tayl 
F ) B )
7968, 69, 70, 75, 77, 78dvntaylp0 20241 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( CC  D n T ) `
 N ) `  B )  =  ( ( ( S  D n F ) `  N
) `  B )
)
8079oveq2d 6056 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( S  D n F ) `  N ) `
 B )  -  ( ( ( CC  D n T ) `
 N ) `  B ) )  =  ( ( ( ( S  D n F ) `  N ) `
 B )  -  ( ( ( S  D n F ) `
 N ) `  B ) ) )
81 cnex 9027 . . . . . . . . . . . . . . . 16  |-  CC  e.  _V
8281a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  CC  e.  _V )
83 elpm2r 6993 . . . . . . . . . . . . . . 15  |-  ( ( ( CC  e.  _V  /\  S  e.  { RR ,  CC } )  /\  ( F : A --> CC  /\  A  C_  S ) )  ->  F  e.  ( CC  ^pm  S )
)
8482, 68, 69, 70, 83syl22anc 1185 . . . . . . . . . . . . . 14  |-  ( ph  ->  F  e.  ( CC 
^pm  S ) )
85 dvnf 19766 . . . . . . . . . . . . . 14  |-  ( ( S  e.  { RR ,  CC }  /\  F  e.  ( CC  ^pm  S
)  /\  N  e.  NN0 )  ->  ( ( S  D n F ) `
 N ) : dom  ( ( S  D n F ) `
 N ) --> CC )
8668, 84, 71, 85syl3anc 1184 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( S  D n F ) `  N
) : dom  (
( S  D n F ) `  N
) --> CC )
8786, 77ffvelrnd 5830 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( S  D n F ) `
 N ) `  B )  e.  CC )
8887subidd 9355 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( S  D n F ) `  N ) `
 B )  -  ( ( ( S  D n F ) `
 N ) `  B ) )  =  0 )
8967, 80, 883eqtrd 2440 . . . . . . . . . 10  |-  ( ph  ->  ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  N
) `  y )  -  ( ( ( CC  D n T ) `  N ) `
 y ) ) ) `  B )  =  0 )
90 funmpt 5448 . . . . . . . . . . 11  |-  Fun  (
y  e.  A  |->  ( ( ( ( S  D n F ) `
 N ) `  y )  -  (
( ( CC  D n T ) `  N
) `  y )
) )
91 ovex 6065 . . . . . . . . . . . . 13  |-  ( ( ( ( S  D n F ) `  N
) `  y )  -  ( ( ( CC  D n T ) `  N ) `
 y ) )  e.  _V
9291, 64dmmpti 5533 . . . . . . . . . . . 12  |-  dom  (
y  e.  A  |->  ( ( ( ( S  D n F ) `
 N ) `  y )  -  (
( ( CC  D n T ) `  N
) `  y )
) )  =  A
9360, 92syl6eleqr 2495 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  dom  (
y  e.  A  |->  ( ( ( ( S  D n F ) `
 N ) `  y )  -  (
( ( CC  D n T ) `  N
) `  y )
) ) )
94 funbrfvb 5728 . . . . . . . . . . 11  |-  ( ( Fun  ( y  e.  A  |->  ( ( ( ( S  D n F ) `  N
) `  y )  -  ( ( ( CC  D n T ) `  N ) `
 y ) ) )  /\  B  e. 
dom  ( y  e.  A  |->  ( ( ( ( S  D n F ) `  N
) `  y )  -  ( ( ( CC  D n T ) `  N ) `
 y ) ) ) )  ->  (
( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  N
) `  y )  -  ( ( ( CC  D n T ) `  N ) `
 y ) ) ) `  B )  =  0  <->  B (
y  e.  A  |->  ( ( ( ( S  D n F ) `
 N ) `  y )  -  (
( ( CC  D n T ) `  N
) `  y )
) ) 0 ) )
9590, 93, 94sylancr 645 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  N
) `  y )  -  ( ( ( CC  D n T ) `  N ) `
 y ) ) ) `  B )  =  0  <->  B (
y  e.  A  |->  ( ( ( ( S  D n F ) `
 N ) `  y )  -  (
( ( CC  D n T ) `  N
) `  y )
) ) 0 ) )
9689, 95mpbid 202 . . . . . . . . 9  |-  ( ph  ->  B ( y  e.  A  |->  ( ( ( ( S  D n F ) `  N
) `  y )  -  ( ( ( CC  D n T ) `  N ) `
 y ) ) ) 0 )
97 nnm1nn0 10217 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN  ->  ( N  -  1 )  e.  NN0 )
981, 97syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( N  -  1 )  e.  NN0 )
99 dvnf 19766 . . . . . . . . . . . . . 14  |-  ( ( S  e.  { RR ,  CC }  /\  F  e.  ( CC  ^pm  S
)  /\  ( N  -  1 )  e. 
NN0 )  ->  (
( S  D n F ) `  ( N  -  1 ) ) : dom  (
( S  D n F ) `  ( N  -  1 ) ) --> CC )
10068, 84, 98, 99syl3anc 1184 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( S  D n F ) `  ( N  -  1 ) ) : dom  (
( S  D n F ) `  ( N  -  1 ) ) --> CC )
101 dvnbss 19767 . . . . . . . . . . . . . . . . 17  |-  ( ( S  e.  { RR ,  CC }  /\  F  e.  ( CC  ^pm  S
)  /\  ( N  -  1 )  e. 
NN0 )  ->  dom  ( ( S  D n F ) `  ( N  -  1 ) )  C_  dom  F )
10268, 84, 98, 101syl3anc 1184 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  ( ( S  D n F ) `
 ( N  - 
1 ) )  C_  dom  F )
103 fdm 5554 . . . . . . . . . . . . . . . . 17  |-  ( F : A --> CC  ->  dom 
F  =  A )
10469, 103syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  F  =  A )
105102, 104sseqtrd 3344 . . . . . . . . . . . . . . 15  |-  ( ph  ->  dom  ( ( S  D n F ) `
 ( N  - 
1 ) )  C_  A )
106 fzo0end 11143 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  NN  ->  ( N  -  1 )  e.  ( 0..^ N ) )
107 elfzofz 11109 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  -  1 )  e.  ( 0..^ N )  ->  ( N  -  1 )  e.  ( 0 ... N
) )
1081, 106, 1073syl 19 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( N  -  1 )  e.  ( 0 ... N ) )
109 dvn2bss 19769 . . . . . . . . . . . . . . . . 17  |-  ( ( S  e.  { RR ,  CC }  /\  F  e.  ( CC  ^pm  S
)  /\  ( N  -  1 )  e.  ( 0 ... N
) )  ->  dom  ( ( S  D n F ) `  N
)  C_  dom  ( ( S  D n F ) `  ( N  -  1 ) ) )
11068, 84, 108, 109syl3anc 1184 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  ( ( S  D n F ) `
 N )  C_  dom  ( ( S  D n F ) `  ( N  -  1 ) ) )
11176, 110eqsstr3d 3343 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  C_  dom  ( ( S  D n F ) `  ( N  -  1 ) ) )
112105, 111eqssd 3325 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( ( S  D n F ) `
 ( N  - 
1 ) )  =  A )
113112feq2d 5540 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( S  D n F ) `
 ( N  - 
1 ) ) : dom  ( ( S  D n F ) `
 ( N  - 
1 ) ) --> CC  <->  ( ( S  D n F ) `  ( N  -  1 ) ) : A --> CC ) )
114100, 113mpbid 202 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( S  D n F ) `  ( N  -  1 ) ) : A --> CC )
115114ffvelrnda 5829 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( S  D n F ) `  ( N  -  1 ) ) `  y )  e.  CC )
11676feq2d 5540 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( S  D n F ) `
 N ) : dom  ( ( S  D n F ) `
 N ) --> CC  <->  ( ( S  D n F ) `  N
) : A --> CC ) )
11786, 116mpbid 202 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( S  D n F ) `  N
) : A --> CC )
118117ffvelrnda 5829 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( S  D n F ) `  N
) `  y )  e.  CC )
1191nncnd 9972 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  CC )
120 ax-1cn 9004 . . . . . . . . . . . . . . . 16  |-  1  e.  CC
121120a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  CC )
122119, 121npcand 9371 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
123122fveq2d 5691 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( S  D n F ) `  (
( N  -  1 )  +  1 ) )  =  ( ( S  D n F ) `  N ) )
124 recnprss 19744 . . . . . . . . . . . . . . 15  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )
12568, 124syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  S  C_  CC )
126 dvnp1 19764 . . . . . . . . . . . . . 14  |-  ( ( S  C_  CC  /\  F  e.  ( CC  ^pm  S
)  /\  ( N  -  1 )  e. 
NN0 )  ->  (
( S  D n F ) `  (
( N  -  1 )  +  1 ) )  =  ( S  _D  ( ( S  D n F ) `
 ( N  - 
1 ) ) ) )
127125, 84, 98, 126syl3anc 1184 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( S  D n F ) `  (
( N  -  1 )  +  1 ) )  =  ( S  _D  ( ( S  D n F ) `
 ( N  - 
1 ) ) ) )
128123, 127eqtr3d 2438 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( S  D n F ) `  N
)  =  ( S  _D  ( ( S  D n F ) `
 ( N  - 
1 ) ) ) )
129117feqmptd 5738 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( S  D n F ) `  N
)  =  ( y  e.  A  |->  ( ( ( S  D n F ) `  N
) `  y )
) )
130114feqmptd 5738 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( S  D n F ) `  ( N  -  1 ) )  =  ( y  e.  A  |->  ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y ) ) )
131130oveq2d 6056 . . . . . . . . . . . 12  |-  ( ph  ->  ( S  _D  (
( S  D n F ) `  ( N  -  1 ) ) )  =  ( S  _D  ( y  e.  A  |->  ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y ) ) ) )
132128, 129, 1313eqtr3rd 2445 . . . . . . . . . . 11  |-  ( ph  ->  ( S  _D  (
y  e.  A  |->  ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y ) ) )  =  ( y  e.  A  |->  ( ( ( S  D n F ) `  N
) `  y )
) )
13370, 125sstrd 3318 . . . . . . . . . . . . 13  |-  ( ph  ->  A  C_  CC )
134133sselda 3308 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  A )  ->  y  e.  CC )
135 1nn0 10193 . . . . . . . . . . . . . . . 16  |-  1  e.  NN0
136135a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  NN0 )
137 elpm2r 6993 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( CC  e.  _V  /\  S  e.  { RR ,  CC } )  /\  ( ( ( S  D n F ) `
 ( N  - 
1 ) ) : A --> CC  /\  A  C_  S ) )  -> 
( ( S  D n F ) `  ( N  -  1 ) )  e.  ( CC 
^pm  S ) )
13882, 68, 114, 70, 137syl22anc 1185 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( S  D n F ) `  ( N  -  1 ) )  e.  ( CC 
^pm  S ) )
139 dvn1 19765 . . . . . . . . . . . . . . . . . . 19  |-  ( ( S  C_  CC  /\  (
( S  D n F ) `  ( N  -  1 ) )  e.  ( CC 
^pm  S ) )  ->  ( ( S  D n ( ( S  D n F ) `  ( N  -  1 ) ) ) `  1 )  =  ( S  _D  ( ( S  D n F ) `  ( N  -  1 ) ) ) )
140125, 138, 139syl2anc 643 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( S  D n ( ( S  D n F ) `
 ( N  - 
1 ) ) ) `
 1 )  =  ( S  _D  (
( S  D n F ) `  ( N  -  1 ) ) ) )
141127, 123eqtr3d 2438 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( S  _D  (
( S  D n F ) `  ( N  -  1 ) ) )  =  ( ( S  D n F ) `  N
) )
142140, 141eqtrd 2436 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( S  D n ( ( S  D n F ) `
 ( N  - 
1 ) ) ) `
 1 )  =  ( ( S  D n F ) `  N
) )
143142dmeqd 5031 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  ( ( S  D n ( ( S  D n F ) `  ( N  -  1 ) ) ) `  1 )  =  dom  ( ( S  D n F ) `  N ) )
14477, 143eleqtrrd 2481 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  e.  dom  (
( S  D n
( ( S  D n F ) `  ( N  -  1 ) ) ) `  1
) )
145 eqid 2404 . . . . . . . . . . . . . . 15  |-  ( 1 ( S Tayl  ( ( S  D n F ) `  ( N  -  1 ) ) ) B )  =  ( 1 ( S Tayl  ( ( S  D n F ) `  ( N  -  1 ) ) ) B )
14668, 114, 70, 136, 144, 145taylpf 20235 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1 ( S Tayl  ( ( S  D n F ) `  ( N  -  1 ) ) ) B ) : CC --> CC )
147121, 119pncan3d 9370 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1  +  ( N  -  1 ) )  =  N )
148147oveq1d 6055 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( 1  +  ( N  -  1 ) ) ( S Tayl 
F ) B )  =  ( N ( S Tayl  F ) B ) )
149148, 78syl6reqr 2455 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  T  =  ( ( 1  +  ( N  -  1 ) ) ( S Tayl  F ) B ) )
150149oveq2d 6056 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( CC  D n T )  =  ( CC  D n ( ( 1  +  ( N  -  1 ) ) ( S Tayl  F
) B ) ) )
151150fveq1d 5689 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  1 ) )  =  ( ( CC  D n ( ( 1  +  ( N  -  1 ) ) ( S Tayl  F
) B ) ) `
 ( N  - 
1 ) ) )
152147fveq2d 5691 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( S  D n F ) `  (
1  +  ( N  -  1 ) ) )  =  ( ( S  D n F ) `  N ) )
153152dmeqd 5031 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  dom  ( ( S  D n F ) `
 ( 1  +  ( N  -  1 ) ) )  =  dom  ( ( S  D n F ) `
 N ) )
15477, 153eleqtrrd 2481 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  B  e.  dom  (
( S  D n F ) `  (
1  +  ( N  -  1 ) ) ) )
15568, 69, 70, 98, 136, 154dvntaylp 20240 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( CC  D n ( ( 1  +  ( N  - 
1 ) ) ( S Tayl  F ) B ) ) `  ( N  -  1 ) )  =  ( 1 ( S Tayl  ( ( S  D n F ) `  ( N  -  1 ) ) ) B ) )
156151, 155eqtrd 2436 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  1 ) )  =  ( 1 ( S Tayl  ( ( S  D n F ) `  ( N  -  1 ) ) ) B ) )
157156feq1d 5539 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( CC  D n T ) `
 ( N  - 
1 ) ) : CC --> CC  <->  ( 1 ( S Tayl  ( ( S  D n F ) `  ( N  -  1 ) ) ) B ) : CC --> CC ) )
158146, 157mpbird 224 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  1 ) ) : CC --> CC )
159158ffvelrnda 5829 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `  y )  e.  CC )
160134, 159syldan 457 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  y )  e.  CC )
161 0nn0 10192 . . . . . . . . . . . . . . . 16  |-  0  e.  NN0
162161a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  e.  NN0 )
163 elpm2r 6993 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( CC  e.  _V  /\  S  e.  { RR ,  CC } )  /\  ( ( ( S  D n F ) `
 N ) : A --> CC  /\  A  C_  S ) )  -> 
( ( S  D n F ) `  N
)  e.  ( CC 
^pm  S ) )
16482, 68, 117, 70, 163syl22anc 1185 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( S  D n F ) `  N
)  e.  ( CC 
^pm  S ) )
165 dvn0 19763 . . . . . . . . . . . . . . . . . 18  |-  ( ( S  C_  CC  /\  (
( S  D n F ) `  N
)  e.  ( CC 
^pm  S ) )  ->  ( ( S  D n ( ( S  D n F ) `  N ) ) `  0 )  =  ( ( S  D n F ) `
 N ) )
166125, 164, 165syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( S  D n ( ( S  D n F ) `
 N ) ) `
 0 )  =  ( ( S  D n F ) `  N
) )
167166dmeqd 5031 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  ( ( S  D n ( ( S  D n F ) `  N ) ) `  0 )  =  dom  ( ( S  D n F ) `  N ) )
16877, 167eleqtrrd 2481 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  e.  dom  (
( S  D n
( ( S  D n F ) `  N
) ) `  0
) )
169 eqid 2404 . . . . . . . . . . . . . . 15  |-  ( 0 ( S Tayl  ( ( S  D n F ) `  N ) ) B )  =  ( 0 ( S Tayl  ( ( S  D n F ) `  N
) ) B )
17068, 117, 70, 162, 168, 169taylpf 20235 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0 ( S Tayl  ( ( S  D n F ) `  N
) ) B ) : CC --> CC )
171119addid2d 9223 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 0  +  N
)  =  N )
172171oveq1d 6055 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( 0  +  N ) ( S Tayl 
F ) B )  =  ( N ( S Tayl  F ) B ) )
173172, 78syl6eqr 2454 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( 0  +  N ) ( S Tayl 
F ) B )  =  T )
174173oveq2d 6056 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( CC  D n
( ( 0  +  N ) ( S Tayl 
F ) B ) )  =  ( CC  D n T ) )
175174fveq1d 5689 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( CC  D n ( ( 0  +  N ) ( S Tayl  F ) B ) ) `  N
)  =  ( ( CC  D n T ) `  N ) )
176171fveq2d 5691 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( S  D n F ) `  (
0  +  N ) )  =  ( ( S  D n F ) `  N ) )
177176dmeqd 5031 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  dom  ( ( S  D n F ) `
 ( 0  +  N ) )  =  dom  ( ( S  D n F ) `
 N ) )
17877, 177eleqtrrd 2481 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  B  e.  dom  (
( S  D n F ) `  (
0  +  N ) ) )
17968, 69, 70, 71, 162, 178dvntaylp 20240 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( CC  D n ( ( 0  +  N ) ( S Tayl  F ) B ) ) `  N
)  =  ( 0 ( S Tayl  ( ( S  D n F ) `  N ) ) B ) )
180175, 179eqtr3d 2438 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( CC  D n T ) `  N
)  =  ( 0 ( S Tayl  ( ( S  D n F ) `  N ) ) B ) )
181180feq1d 5539 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( CC  D n T ) `
 N ) : CC --> CC  <->  ( 0 ( S Tayl  ( ( S  D n F ) `  N ) ) B ) : CC --> CC ) )
182170, 181mpbird 224 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( CC  D n T ) `  N
) : CC --> CC )
183182ffvelrnda 5829 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( ( CC  D n T ) `  N
) `  y )  e.  CC )
184134, 183syldan 457 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( CC  D n T ) `  N
) `  y )  e.  CC )
185125sselda 3308 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  S )  ->  y  e.  CC )
186185, 159syldan 457 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  S )  ->  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  y )  e.  CC )
187185, 183syldan 457 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  S )  ->  (
( ( CC  D n T ) `  N
) `  y )  e.  CC )
188 eqid 2404 . . . . . . . . . . . . 13  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
189188cnfldtopon 18770 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
190 toponmax 16948 . . . . . . . . . . . . . 14  |-  ( (
TopOpen ` fld )  e.  (TopOn `  CC )  ->  CC  e.  ( TopOpen ` fld ) )
191189, 190mp1i 12 . . . . . . . . . . . . 13  |-  ( ph  ->  CC  e.  ( TopOpen ` fld )
)
192 df-ss 3294 . . . . . . . . . . . . . 14  |-  ( S 
C_  CC  <->  ( S  i^i  CC )  =  S )
193125, 192sylib 189 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S  i^i  CC )  =  S )
194 ssid 3327 . . . . . . . . . . . . . . . . 17  |-  CC  C_  CC
195194a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  CC  C_  CC )
196 mapsspm 7006 . . . . . . . . . . . . . . . . 17  |-  ( CC 
^m  CC )  C_  ( CC  ^pm  CC )
19768, 69, 70, 71, 77, 78taylpf 20235 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  T : CC --> CC )
19881, 81elmap 7001 . . . . . . . . . . . . . . . . . 18  |-  ( T  e.  ( CC  ^m  CC )  <->  T : CC --> CC )
199197, 198sylibr 204 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  T  e.  ( CC 
^m  CC ) )
200196, 199sseldi 3306 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  T  e.  ( CC 
^pm  CC ) )
201 dvnp1 19764 . . . . . . . . . . . . . . . 16  |-  ( ( CC  C_  CC  /\  T  e.  ( CC  ^pm  CC )  /\  ( N  - 
1 )  e.  NN0 )  ->  ( ( CC  D n T ) `
 ( ( N  -  1 )  +  1 ) )  =  ( CC  _D  (
( CC  D n T ) `  ( N  -  1 ) ) ) )
202195, 200, 98, 201syl3anc 1184 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( CC  D n T ) `  (
( N  -  1 )  +  1 ) )  =  ( CC 
_D  ( ( CC  D n T ) `
 ( N  - 
1 ) ) ) )
203122fveq2d 5691 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( CC  D n T ) `  (
( N  -  1 )  +  1 ) )  =  ( ( CC  D n T ) `  N ) )
204202, 203eqtr3d 2438 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( CC  _D  (
( CC  D n T ) `  ( N  -  1 ) ) )  =  ( ( CC  D n T ) `  N
) )
205158feqmptd 5738 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  1 ) )  =  ( y  e.  CC  |->  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `  y ) ) )
206205oveq2d 6056 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( CC  _D  (
( CC  D n T ) `  ( N  -  1 ) ) )  =  ( CC  _D  ( y  e.  CC  |->  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `  y ) ) ) )
207182feqmptd 5738 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( CC  D n T ) `  N
)  =  ( y  e.  CC  |->  ( ( ( CC  D n T ) `  N
) `  y )
) )
208204, 206, 2073eqtr3d 2444 . . . . . . . . . . . . 13  |-  ( ph  ->  ( CC  _D  (
y  e.  CC  |->  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `  y ) ) )  =  ( y  e.  CC  |->  ( ( ( CC  D n T ) `  N
) `  y )
) )
209188, 68, 191, 193, 159, 183, 208dvmptres3 19795 . . . . . . . . . . . 12  |-  ( ph  ->  ( S  _D  (
y  e.  S  |->  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `  y ) ) )  =  ( y  e.  S  |->  ( ( ( CC  D n T ) `  N
) `  y )
) )
210 eqid 2404 . . . . . . . . . . . 12  |-  ( (
TopOpen ` fld )t  S )  =  ( ( TopOpen ` fld )t  S )
211 resttopon 17179 . . . . . . . . . . . . . . . 16  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  S  C_  CC )  ->  (
( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
212189, 125, 211sylancr 645 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
213 topontop 16946 . . . . . . . . . . . . . . 15  |-  ( ( ( TopOpen ` fld )t  S )  e.  (TopOn `  S )  ->  (
( TopOpen ` fld )t  S )  e.  Top )
214212, 213syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( TopOpen ` fld )t  S )  e.  Top )
215 toponuni 16947 . . . . . . . . . . . . . . . 16  |-  ( ( ( TopOpen ` fld )t  S )  e.  (TopOn `  S )  ->  S  =  U. ( ( TopOpen ` fld )t  S
) )
216212, 215syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  S  =  U. (
( TopOpen ` fld )t  S ) )
21770, 216sseqtrd 3344 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  C_  U. (
( TopOpen ` fld )t  S ) )
218 eqid 2404 . . . . . . . . . . . . . . 15  |-  U. (
( TopOpen ` fld )t  S )  =  U. ( ( TopOpen ` fld )t  S )
219218ntrss2 17076 . . . . . . . . . . . . . 14  |-  ( ( ( ( TopOpen ` fld )t  S )  e.  Top  /\  A  C_  U. (
( TopOpen ` fld )t  S ) )  -> 
( ( int `  (
( TopOpen ` fld )t  S ) ) `  A )  C_  A
)
220214, 217, 219syl2anc 643 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  A )  C_  A
)
221141dmeqd 5031 . . . . . . . . . . . . . . 15  |-  ( ph  ->  dom  ( S  _D  ( ( S  D n F ) `  ( N  -  1 ) ) )  =  dom  ( ( S  D n F ) `  N
) )
222221, 76eqtrd 2436 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( S  _D  ( ( S  D n F ) `  ( N  -  1 ) ) )  =  A )
223125, 114, 70, 210, 188dvbssntr 19740 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( S  _D  ( ( S  D n F ) `  ( N  -  1 ) ) )  C_  (
( int `  (
( TopOpen ` fld )t  S ) ) `  A ) )
224222, 223eqsstr3d 3343 . . . . . . . . . . . . 13  |-  ( ph  ->  A  C_  ( ( int `  ( ( TopOpen ` fld )t  S
) ) `  A
) )
225220, 224eqssd 3325 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  A )  =  A )
22668, 186, 187, 209, 70, 210, 188, 225dvmptres2 19801 . . . . . . . . . . 11  |-  ( ph  ->  ( S  _D  (
y  e.  A  |->  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `  y ) ) )  =  ( y  e.  A  |->  ( ( ( CC  D n T ) `  N
) `  y )
) )
22768, 115, 118, 132, 160, 184, 226dvmptsub 19806 . . . . . . . . . 10  |-  ( ph  ->  ( S  _D  (
y  e.  A  |->  ( ( ( ( S  D n F ) `
 ( N  - 
1 ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  y ) ) ) )  =  ( y  e.  A  |->  ( ( ( ( S  D n F ) `  N ) `
 y )  -  ( ( ( CC  D n T ) `
 N ) `  y ) ) ) )
228227breqd 4183 . . . . . . . . 9  |-  ( ph  ->  ( B ( S  _D  ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) ) 0  <->  B
( y  e.  A  |->  ( ( ( ( S  D n F ) `  N ) `
 y )  -  ( ( ( CC  D n T ) `
 N ) `  y ) ) ) 0 ) )
22996, 228mpbird 224 . . . . . . . 8  |-  ( ph  ->  B ( S  _D  ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 y )  -  ( ( ( CC  D n T ) `
 ( N  - 
1 ) ) `  y ) ) ) ) 0 )
230 eqid 2404 . . . . . . . . 9  |-  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) `  x )  -  ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) `  B ) )  /  ( x  -  B ) ) )  =  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) `  x )  -  ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) `  B ) )  /  ( x  -  B ) ) )
231115, 160subcld 9367 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( ( S  D n F ) `
 ( N  - 
1 ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  y ) )  e.  CC )
232 eqid 2404 . . . . . . . . . 10  |-  ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) )  =  ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) )
233231, 232fmptd 5852 . . . . . . . . 9  |-  ( ph  ->  ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 y )  -  ( ( ( CC  D n T ) `
 ( N  - 
1 ) ) `  y ) ) ) : A --> CC )
234210, 188, 230, 125, 233, 70eldv 19738 . . . . . . . 8  |-  ( ph  ->  ( B ( S  _D  ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) ) 0  <->  ( B  e.  ( ( int `  ( ( TopOpen ` fld )t  S
) ) `  A
)  /\  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) `  x )  -  ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) `  B ) )  /  ( x  -  B ) ) ) lim CC  B ) ) ) )
235229, 234mpbid 202 . . . . . . 7  |-  ( ph  ->  ( B  e.  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  A )  /\  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) `  x )  -  ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) `  B ) )  /  ( x  -  B ) ) ) lim CC  B ) ) )
236235simprd 450 . . . . . 6  |-  ( ph  ->  0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 y )  -  ( ( ( CC  D n T ) `
 ( N  - 
1 ) ) `  y ) ) ) `
 x )  -  ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) `  B ) )  /  ( x  -  B ) ) ) lim CC  B ) )
237 eldifi 3429 . . . . . . . . . 10  |-  ( x  e.  ( A  \  { B } )  ->  x  e.  A )
238 fveq2 5687 . . . . . . . . . . . . . 14  |-  ( y  =  x  ->  (
( ( S  D n F ) `  ( N  -  1 ) ) `  y )  =  ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 x ) )
239 fveq2 5687 . . . . . . . . . . . . . 14  |-  ( y  =  x  ->  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  y )  =  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 x ) )
240238, 239oveq12d 6058 . . . . . . . . . . . . 13  |-  ( y  =  x  ->  (
( ( ( S  D n F ) `
 ( N  - 
1 ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  y ) )  =  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 x ) ) )
241 ovex 6065 . . . . . . . . . . . . 13  |-  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 x ) )  e.  _V
242240, 232, 241fvmpt 5765 . . . . . . . . . . . 12  |-  ( x  e.  A  ->  (
( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 y )  -  ( ( ( CC  D n T ) `
 ( N  - 
1 ) ) `  y ) ) ) `
 x )  =  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  - 
1 ) ) `  x ) ) )
243 fveq2 5687 . . . . . . . . . . . . . . . 16  |-  ( y  =  B  ->  (
( ( S  D n F ) `  ( N  -  1 ) ) `  y )  =  ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 B ) )
244 fveq2 5687 . . . . . . . . . . . . . . . 16  |-  ( y  =  B  ->  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  y )  =  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 B ) )
245243, 244oveq12d 6058 . . . . . . . . . . . . . . 15  |-  ( y  =  B  ->  (
( ( ( S  D n F ) `
 ( N  - 
1 ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  y ) )  =  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  B )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 B ) ) )
246 ovex 6065 . . . . . . . . . . . . . . 15  |-  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  B )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 B ) )  e.  _V
247245, 232, 246fvmpt 5765 . . . . . . . . . . . . . 14  |-  ( B  e.  A  ->  (
( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 y )  -  ( ( ( CC  D n T ) `
 ( N  - 
1 ) ) `  y ) ) ) `
 B )  =  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 B )  -  ( ( ( CC  D n T ) `
 ( N  - 
1 ) ) `  B ) ) )
24860, 247syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) `  B )  =  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  B )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 B ) ) )
24968, 69, 70, 108, 77, 78dvntaylp0 20241 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( CC  D n T ) `
 ( N  - 
1 ) ) `  B )  =  ( ( ( S  D n F ) `  ( N  -  1 ) ) `  B ) )
250249oveq2d 6056 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 B )  -  ( ( ( CC  D n T ) `
 ( N  - 
1 ) ) `  B ) )  =  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 B )  -  ( ( ( S  D n F ) `
 ( N  - 
1 ) ) `  B ) ) )
251114, 60ffvelrnd 5830 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( S  D n F ) `
 ( N  - 
1 ) ) `  B )  e.  CC )
252251subidd 9355 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 B )  -  ( ( ( S  D n F ) `
 ( N  - 
1 ) ) `  B ) )  =  0 )
253248, 250, 2523eqtrd 2440 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) `  B )  =  0 )
254242, 253oveqan12rd 6060 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) `  x )  -  ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) `  B ) )  =  ( ( ( ( ( S  D n F ) `
 ( N  - 
1 ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  x ) )  -  0 ) )
255114ffvelrnda 5829 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( S  D n F ) `  ( N  -  1 ) ) `  x )  e.  CC )
256133sselda 3308 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  CC )
257158ffvelrnda 5829 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  CC )  ->  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `  x )  e.  CC )
258256, 257syldan 457 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  x )  e.  CC )
259255, 258subcld 9367 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( ( S  D n F ) `
 ( N  - 
1 ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  x ) )  e.  CC )
260259subid1d 9356 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  - 
1 ) ) `  x ) )  - 
0 )  =  ( ( ( ( S  D n F ) `
 ( N  - 
1 ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  x ) ) )
261254, 260eqtr2d 2437 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( ( S  D n F ) `
 ( N  - 
1 ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  x ) )  =  ( ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 y )  -  ( ( ( CC  D n T ) `
 ( N  - 
1 ) ) `  y ) ) ) `
 x )  -  ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) `  B ) ) )
262237, 261sylan2 461 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  - 
1 ) ) `  x ) )  =  ( ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) `  x )  -  ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) `  B ) ) )
263133ssdifssd 3445 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  \  { B } )  C_  CC )
264263sselda 3308 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  x  e.  CC )
265133, 60sseldd 3309 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  CC )
266265adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  B  e.  CC )
267264, 266subcld 9367 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( x  -  B
)  e.  CC )
268267exp1d 11473 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( x  -  B ) ^ 1 )  =  ( x  -  B ) )
269262, 268oveq12d 6058 . . . . . . . 8  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 x ) )  /  ( ( x  -  B ) ^
1 ) )  =  ( ( ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `
 ( N  - 
1 ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  y ) ) ) `  x
)  -  ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `
 ( N  - 
1 ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  y ) ) ) `  B
) )  /  (
x  -  B ) ) )
270269mpteq2dva 4255 . . . . . . 7  |-  ( ph  ->  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  - 
1 ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  x ) )  /  ( ( x  -  B ) ^ 1 ) ) )  =  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) `  x )  -  ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) `  B ) )  /  ( x  -  B ) ) ) )
271270oveq1d 6055 . . . . . 6  |-  ( ph  ->  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  - 
1 ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  x ) )  /  ( ( x  -  B ) ^ 1 ) ) ) lim CC  B )  =  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) `  x )  -  ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) `  B ) )  /  ( x  -  B ) ) ) lim CC  B ) )
272236, 271eleqtrrd 2481 . . . . 5  |-  ( ph  ->  0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 x ) )  /  ( ( x  -  B ) ^
1 ) ) ) lim
CC  B ) )
273272a1i 11 . . . 4  |-  ( N  e.  ( ZZ>= `  1
)  ->  ( ph  ->  0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 x ) )  /  ( ( x  -  B ) ^
1 ) ) ) lim
CC  B ) ) )
274 taylthlem1.i . . . . . . 7  |-  ( (
ph  /\  ( n  e.  ( 1..^ N )  /\  0  e.  ( ( y  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  n ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  n )
) `  y )
)  /  ( ( y  -  B ) ^ n ) ) ) lim CC  B ) ) )  ->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  ( n  +  1
) ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  ( n  +  1 ) ) ) `  x ) )  /  ( ( x  -  B ) ^ ( n  + 
1 ) ) ) ) lim CC  B ) )
275274expr 599 . . . . . 6  |-  ( (
ph  /\  n  e.  ( 1..^ N ) )  ->  ( 0  e.  ( ( y  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  n ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  n )
) `  y )
)  /  ( ( y  -  B ) ^ n ) ) ) lim CC  B )  ->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  ( n  +  1
) ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  ( n  +  1 ) ) ) `  x ) )  /  ( ( x  -  B ) ^ ( n  + 
1 ) ) ) ) lim CC  B ) ) )
276275expcom 425 . . . . 5  |-  ( n  e.  ( 1..^ N )  ->  ( ph  ->  ( 0  e.  ( ( y  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  n ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  n )
) `  y )
)  /  ( ( y  -  B ) ^ n ) ) ) lim CC  B )  ->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  ( n  +  1
) ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  ( n  +  1 ) ) ) `  x ) )  /  ( ( x  -  B ) ^ ( n  + 
1 ) ) ) ) lim CC  B ) ) ) )
277276a2d 24 . . . 4  |-  ( n  e.  ( 1..^ N )  ->  ( ( ph  ->  0  e.  ( ( y  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  n ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  n )
) `  y )
)  /  ( ( y  -  B ) ^ n ) ) ) lim CC  B ) )  ->  ( ph  ->  0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  D n F ) `  ( N  -  ( n  +  1 ) ) ) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  ( n  + 
1 ) ) ) `
 x ) )  /  ( ( x  -  B ) ^
( n  +  1 ) ) ) ) lim
CC  B ) ) ) )
27815, 35, 47, 59, 273, 277fzind2 11153 . . 3  |-  ( N  e.  ( 1 ... N )  ->  ( ph  ->  0  e.  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  N ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  N )
) `  x )
)  /  ( ( x  -  B ) ^ N ) ) ) lim CC  B ) ) )
2793, 278mpcom 34 . 2  |-  ( ph  ->  0  e.  ( ( x  e.  ( A 
\  { B }
)  |->  ( ( ( ( ( S  D n F ) `  ( N  -  N )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  N ) ) `
 x ) )  /  ( ( x  -  B ) ^ N ) ) ) lim
CC  B ) )
280119subidd 9355 . . . . . . . . . 10  |-  ( ph  ->  ( N  -  N
)  =  0 )
281280fveq2d 5691 . . . . . . . . 9  |-  ( ph  ->  ( ( S  D n F ) `  ( N  -  N )
)  =  ( ( S  D n F ) `  0 ) )
282 dvn0 19763 . . . . . . . . . 10  |-  ( ( S  C_  CC  /\  F  e.  ( CC  ^pm  S
) )  ->  (
( S  D n F ) `  0
)  =  F )
283125, 84, 282syl2anc 643 . . . . . . . . 9  |-  ( ph  ->  ( ( S  D n F ) `  0
)  =  F )
284281, 283eqtrd 2436 . . . . . . . 8  |-  ( ph  ->  ( ( S  D n F ) `  ( N  -  N )
)  =  F )
285284fveq1d 5689 . . . . . . 7  |-  ( ph  ->  ( ( ( S  D n F ) `
 ( N  -  N ) ) `  x )  =  ( F `  x ) )
286280fveq2d 5691 . . . . . . . . 9  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  N )
)  =  ( ( CC  D n T ) `  0 ) )
287 dvn0 19763 . . . . . . . . . 10  |-  ( ( CC  C_  CC  /\  T  e.  ( CC  ^pm  CC ) )  ->  (
( CC  D n T ) `  0
)  =  T )
288194, 200, 287sylancr 645 . . . . . . . . 9  |-  ( ph  ->  ( ( CC  D n T ) `  0
)  =  T )
289286, 288eqtrd 2436 . . . . . . . 8  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  N )
)  =  T )
290289fveq1d 5689 . . . . . . 7  |-  ( ph  ->  ( ( ( CC  D n T ) `
 ( N  -  N ) ) `  x )  =  ( T `  x ) )
291285, 290oveq12d 6058 . . . . . 6  |-  ( ph  ->  ( ( ( ( S  D n F ) `  ( N  -  N ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  N ) ) `  x ) )  =  ( ( F `  x )  -  ( T `  x )
) )
292291oveq1d 6055 . . . . 5  |-  ( ph  ->  ( ( ( ( ( S  D n F ) `  ( N  -  N )
) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  N ) ) `
 x ) )  /  ( ( x  -  B ) ^ N ) )  =  ( ( ( F `
 x )  -  ( T `  x ) )  /  ( ( x  -  B ) ^ N ) ) )
293292mpteq2dv 4256 . . . 4  |-  ( ph  ->  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  N ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  N )
) `  x )
)  /  ( ( x  -  B ) ^ N ) ) )  =  ( x  e.  ( A  \  { B } )  |->  ( ( ( F `  x )  -  ( T `  x )
)  /  ( ( x  -  B ) ^ N ) ) ) )
294 taylthlem1.r . . . 4  |-  R  =  ( x  e.  ( A  \  { B } )  |->  ( ( ( F `  x
)  -  ( T `
 x ) )  /  ( ( x  -  B ) ^ N ) ) )
295293, 294syl6eqr 2454 . . 3  |-  ( ph  ->  ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  N ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  N )
) `  x )
)  /  ( ( x  -  B ) ^ N ) ) )  =  R )
296295oveq1d 6055 . 2  |-  ( ph  ->  ( ( x  e.  ( A  \  { B } )  |->  ( ( ( ( ( S  D n F ) `
 ( N  -  N ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  N )
) `  x )
)  /  ( ( x  -  B ) ^ N ) ) ) lim CC  B )  =  ( R lim CC  B ) )
297279, 296eleqtrd 2480 1  |-  ( ph  ->  0  e.  ( R lim
CC  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1721   _Vcvv 2916    \ cdif 3277    i^i cin 3279    C_ wss 3280   {csn 3774   {cpr 3775   U.cuni 3975   class class class wbr 4172    e. cmpt 4226   dom cdm 4837   Fun wfun 5407   -->wf 5409   ` cfv 5413  (class class class)co 6040    ^m cmap 6977    ^pm cpm 6978   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947    + caddc 8949    - cmin 9247    / cdiv 9633   NNcn 9956   NN0cn0 10177   ZZ>=cuz 10444   ...cfz 10999  ..^cfzo 11090   ^cexp 11337   ↾t crest 13603   TopOpenctopn 13604  ℂfldccnfld 16658   Topctop 16913  TopOnctopon 16914   intcnt 17036   lim CC climc 19702    _D cdv 19703    D ncdvn 19704   Tayl ctayl 20222
This theorem is referenced by:  taylth  20244
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024  ax-addf 9025  ax-mulf 9026
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-iin 4056  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-of 6264  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-2o 6684  df-oadd 6687  df-er 6864  df-map 6979  df-pm 6980  df-ixp 7023  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-fi 7374  df-sup 7404  df-oi 7435  df-card 7782  df-cda 8004  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-4 10016  df-5 10017  df-6 10018  df-7 10019  df-8 10020  df-9 10021  df-10 10022  df-n0 10178  df-z 10239  df-dec 10339  df-uz 10445  df-q 10531  df-rp 10569  df-xneg 10666  df-xadd 10667  df-xmul 10668  df-icc 10879  df-fz 11000  df-fzo 11091  df-seq 11279  df-exp 11338  df-fac 11522  df-hash 11574  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-clim 12237  df-sum 12435  df-struct 13426  df-ndx 13427  df-slot 13428  df-base 13429  df-sets 13430  df-ress 13431  df-plusg 13497  df-mulr 13498  df-starv 13499  df-sca 13500  df-vsca 13501  df-tset 13503  df-ple 13504  df-ds 13506  df-unif 13507  df-hom 13508  df-cco 13509  df-rest 13605  df-topn 13606  df-topgen 13622  df-pt 13623  df-prds 13626  df-xrs 13681  df-0g 13682  df-gsum 13683  df-qtop 13688  df-imas 13689  df-xps 13691  df-mre 13766  df-mrc 13767  df-acs 13769  df-mnd 14645  df-submnd 14694  df-grp 14767  df-minusg 14768  df-mulg 14770  df-cntz 15071  df-cmn 15369  df-abl 15370  df-mgp 15604  df-rng 15618  df-cring 15619  df-ur 15620  df-psmet 16649  df-xmet 16650  df-met 16651  df-bl 16652  df-mopn 16653  df-fbas 16654  df-fg 16655  df-cnfld 16659  df-top 16918  df-bases 16920  df-topon 16921  df-topsp 16922  df-cld 17038  df-ntr 17039  df-cls 17040  df-nei 17117  df-lp 17155  df-perf 17156  df-cn 17245  df-cnp 17246  df-haus 17333  df-tx 17547  df-hmeo 17740  df-fil 17831  df-fm 17923  df-flim 17924  df-flf 17925  df-tsms 18109  df-xms 18303  df-ms 18304  df-tms 18305  df-cncf 18861  df-limc 19706  df-dv 19707  df-dvn 19708  df-tayl 20224
  Copyright terms: Public domain W3C validator