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

Theorem taylthlem1 20291
Description: Lemma for taylth 20293. 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 20293 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 11083 . . . 4  |-  ( N  e.  NN  <->  N  e.  ( 1 ... N
) )
31, 2sylib 190 . . 3  |-  ( ph  ->  N  e.  ( 1 ... N ) )
4 oveq2 6091 . . . . . . . . . . . 12  |-  ( m  =  1  ->  ( N  -  m )  =  ( N  - 
1 ) )
54fveq2d 5734 . . . . . . . . . . 11  |-  ( m  =  1  ->  (
( S  D n F ) `  ( N  -  m )
)  =  ( ( S  D n F ) `  ( N  -  1 ) ) )
65fveq1d 5732 . . . . . . . . . 10  |-  ( m  =  1  ->  (
( ( S  D n F ) `  ( N  -  m )
) `  x )  =  ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 x ) )
74fveq2d 5734 . . . . . . . . . . 11  |-  ( m  =  1  ->  (
( CC  D n T ) `  ( N  -  m )
)  =  ( ( CC  D n T ) `  ( N  -  1 ) ) )
87fveq1d 5732 . . . . . . . . . 10  |-  ( m  =  1  ->  (
( ( CC  D n T ) `  ( N  -  m )
) `  x )  =  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 x ) )
96, 8oveq12d 6101 . . . . . . . . 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 6091 . . . . . . . . 9  |-  ( m  =  1  ->  (
( x  -  B
) ^ m )  =  ( ( x  -  B ) ^
1 ) )
119, 10oveq12d 6101 . . . . . . . 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 4298 . . . . . . 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 6098 . . . . . 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 2505 . . . . 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 309 . . . 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 6091 . . . . . . . . . . . . 13  |-  ( m  =  n  ->  ( N  -  m )  =  ( N  -  n ) )
1716fveq2d 5734 . . . . . . . . . . . 12  |-  ( m  =  n  ->  (
( S  D n F ) `  ( N  -  m )
)  =  ( ( S  D n F ) `  ( N  -  n ) ) )
1817fveq1d 5732 . . . . . . . . . . 11  |-  ( m  =  n  ->  (
( ( S  D n F ) `  ( N  -  m )
) `  x )  =  ( ( ( S  D n F ) `  ( N  -  n ) ) `
 x ) )
1916fveq2d 5734 . . . . . . . . . . . 12  |-  ( m  =  n  ->  (
( CC  D n T ) `  ( N  -  m )
)  =  ( ( CC  D n T ) `  ( N  -  n ) ) )
2019fveq1d 5732 . . . . . . . . . . 11  |-  ( m  =  n  ->  (
( ( CC  D n T ) `  ( N  -  m )
) `  x )  =  ( ( ( CC  D n T ) `  ( N  -  n ) ) `
 x ) )
2118, 20oveq12d 6101 . . . . . . . . . 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 6091 . . . . . . . . . 10  |-  ( m  =  n  ->  (
( x  -  B
) ^ m )  =  ( ( x  -  B ) ^
n ) )
2321, 22oveq12d 6101 . . . . . . . . 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 4298 . . . . . . . 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 5730 . . . . . . . . . . 11  |-  ( x  =  y  ->  (
( ( S  D n F ) `  ( N  -  n )
) `  x )  =  ( ( ( S  D n F ) `  ( N  -  n ) ) `
 y ) )
26 fveq2 5730 . . . . . . . . . . 11  |-  ( x  =  y  ->  (
( ( CC  D n T ) `  ( N  -  n )
) `  x )  =  ( ( ( CC  D n T ) `  ( N  -  n ) ) `
 y ) )
2725, 26oveq12d 6101 . . . . . . . . . 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 6090 . . . . . . . . . . 11  |-  ( x  =  y  ->  (
x  -  B )  =  ( y  -  B ) )
2928oveq1d 6098 . . . . . . . . . 10  |-  ( x  =  y  ->  (
( x  -  B
) ^ n )  =  ( ( y  -  B ) ^
n ) )
3027, 29oveq12d 6101 . . . . . . . . 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 4302 . . . . . . . 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 2486 . . . . . . 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 6098 . . . . . 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 2505 . . . . 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 309 . . . 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 6091 . . . . . . . . . . . 12  |-  ( m  =  ( n  + 
1 )  ->  ( N  -  m )  =  ( N  -  ( n  +  1
) ) )
3736fveq2d 5734 . . . . . . . . . . 11  |-  ( m  =  ( n  + 
1 )  ->  (
( S  D n F ) `  ( N  -  m )
)  =  ( ( S  D n F ) `  ( N  -  ( n  + 
1 ) ) ) )
3837fveq1d 5732 . . . . . . . . . 10  |-  ( m  =  ( n  + 
1 )  ->  (
( ( S  D n F ) `  ( N  -  m )
) `  x )  =  ( ( ( S  D n F ) `  ( N  -  ( n  + 
1 ) ) ) `
 x ) )
3936fveq2d 5734 . . . . . . . . . . 11  |-  ( m  =  ( n  + 
1 )  ->  (
( CC  D n T ) `  ( N  -  m )
)  =  ( ( CC  D n T ) `  ( N  -  ( n  + 
1 ) ) ) )
4039fveq1d 5732 . . . . . . . . . 10  |-  ( m  =  ( n  + 
1 )  ->  (
( ( CC  D n T ) `  ( N  -  m )
) `  x )  =  ( ( ( CC  D n T ) `  ( N  -  ( n  + 
1 ) ) ) `
 x ) )
4138, 40oveq12d 6101 . . . . . . . . 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 6091 . . . . . . . . 9  |-  ( m  =  ( n  + 
1 )  ->  (
( x  -  B
) ^ m )  =  ( ( x  -  B ) ^
( n  +  1 ) ) )
4341, 42oveq12d 6101 . . . . . . . 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 4298 . . . . . . 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 6098 . . . . . 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 2505 . . . . 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 309 . . . 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 6091 . . . . . . . . . . . 12  |-  ( m  =  N  ->  ( N  -  m )  =  ( N  -  N ) )
4948fveq2d 5734 . . . . . . . . . . 11  |-  ( m  =  N  ->  (
( S  D n F ) `  ( N  -  m )
)  =  ( ( S  D n F ) `  ( N  -  N ) ) )
5049fveq1d 5732 . . . . . . . . . 10  |-  ( m  =  N  ->  (
( ( S  D n F ) `  ( N  -  m )
) `  x )  =  ( ( ( S  D n F ) `  ( N  -  N ) ) `
 x ) )
5148fveq2d 5734 . . . . . . . . . . 11  |-  ( m  =  N  ->  (
( CC  D n T ) `  ( N  -  m )
)  =  ( ( CC  D n T ) `  ( N  -  N ) ) )
5251fveq1d 5732 . . . . . . . . . 10  |-  ( m  =  N  ->  (
( ( CC  D n T ) `  ( N  -  m )
) `  x )  =  ( ( ( CC  D n T ) `  ( N  -  N ) ) `
 x ) )
5350, 52oveq12d 6101 . . . . . . . . 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 6091 . . . . . . . . 9  |-  ( m  =  N  ->  (
( x  -  B
) ^ m )  =  ( ( x  -  B ) ^ N ) )
5553, 54oveq12d 6101 . . . . . . . 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 4298 . . . . . . 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 6098 . . . . . 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 2505 . . . . 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 309 . . . 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 5730 . . . . . . . . . . . . . 14  |-  ( y  =  B  ->  (
( ( S  D n F ) `  N
) `  y )  =  ( ( ( S  D n F ) `  N ) `
 B ) )
62 fveq2 5730 . . . . . . . . . . . . . 14  |-  ( y  =  B  ->  (
( ( CC  D n T ) `  N
) `  y )  =  ( ( ( CC  D n T ) `  N ) `
 B ) )
6361, 62oveq12d 6101 . . . . . . . . . . . . 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 2438 . . . . . . . . . . . . 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 6108 . . . . . . . . . . . . 13  |-  ( ( ( ( S  D n F ) `  N
) `  B )  -  ( ( ( CC  D n T ) `  N ) `
 B ) )  e.  _V
6663, 64, 65fvmpt 5808 . . . . . . . . . . . 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 10276 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  NN0 )
72 nn0uz 10522 . . . . . . . . . . . . . . 15  |-  NN0  =  ( ZZ>= `  0 )
7371, 72syl6eleq 2528 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  ( ZZ>= ` 
0 ) )
74 eluzfz2b 11068 . . . . . . . . . . . . . 14  |-  ( N  e.  ( ZZ>= `  0
)  <->  N  e.  (
0 ... N ) )
7573, 74sylib 190 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  ( 0 ... N ) )
76 taylthlem1.d . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( ( S  D n F ) `
 N )  =  A )
7760, 76eleqtrrd 2515 . . . . . . . . . . . . 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 20290 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( CC  D n T ) `
 N ) `  B )  =  ( ( ( S  D n F ) `  N
) `  B )
)
8079oveq2d 6099 . . . . . . . . . . 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 9073 . . . . . . . . . . . . . . . 16  |-  CC  e.  _V
8281a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  CC  e.  _V )
83 elpm2r 7036 . . . . . . . . . . . . . . 15  |-  ( ( ( CC  e.  _V  /\  S  e.  { RR ,  CC } )  /\  ( F : A --> CC  /\  A  C_  S ) )  ->  F  e.  ( CC  ^pm  S )
)
8482, 68, 69, 70, 83syl22anc 1186 . . . . . . . . . . . . . 14  |-  ( ph  ->  F  e.  ( CC 
^pm  S ) )
85 dvnf 19815 . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( S  D n F ) `  N
) : dom  (
( S  D n F ) `  N
) --> CC )
8786, 77ffvelrnd 5873 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( S  D n F ) `
 N ) `  B )  e.  CC )
8887subidd 9401 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( S  D n F ) `  N ) `
 B )  -  ( ( ( S  D n F ) `
 N ) `  B ) )  =  0 )
8967, 80, 883eqtrd 2474 . . . . . . . . . 10  |-  ( ph  ->  ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  N
) `  y )  -  ( ( ( CC  D n T ) `  N ) `
 y ) ) ) `  B )  =  0 )
90 funmpt 5491 . . . . . . . . . . 11  |-  Fun  (
y  e.  A  |->  ( ( ( ( S  D n F ) `
 N ) `  y )  -  (
( ( CC  D n T ) `  N
) `  y )
) )
91 ovex 6108 . . . . . . . . . . . . 13  |-  ( ( ( ( S  D n F ) `  N
) `  y )  -  ( ( ( CC  D n T ) `  N ) `
 y ) )  e.  _V
9291, 64dmmpti 5576 . . . . . . . . . . . 12  |-  dom  (
y  e.  A  |->  ( ( ( ( S  D n F ) `
 N ) `  y )  -  (
( ( CC  D n T ) `  N
) `  y )
) )  =  A
9360, 92syl6eleqr 2529 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  dom  (
y  e.  A  |->  ( ( ( ( S  D n F ) `
 N ) `  y )  -  (
( ( CC  D n T ) `  N
) `  y )
) ) )
94 funbrfvb 5771 . . . . . . . . . . 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 646 . . . . . . . . . 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 203 . . . . . . . . 9  |-  ( ph  ->  B ( y  e.  A  |->  ( ( ( ( S  D n F ) `  N
) `  y )  -  ( ( ( CC  D n T ) `  N ) `
 y ) ) ) 0 )
97 nnm1nn0 10263 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN  ->  ( N  -  1 )  e.  NN0 )
981, 97syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( N  -  1 )  e.  NN0 )
99 dvnf 19815 . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( S  D n F ) `  ( N  -  1 ) ) : dom  (
( S  D n F ) `  ( N  -  1 ) ) --> CC )
101 dvnbss 19816 . . . . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  ( ( S  D n F ) `
 ( N  - 
1 ) )  C_  dom  F )
103 fdm 5597 . . . . . . . . . . . . . . . . 17  |-  ( F : A --> CC  ->  dom 
F  =  A )
10469, 103syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  F  =  A )
105102, 104sseqtrd 3386 . . . . . . . . . . . . . . 15  |-  ( ph  ->  dom  ( ( S  D n F ) `
 ( N  - 
1 ) )  C_  A )
106 fzo0end 11190 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  NN  ->  ( N  -  1 )  e.  ( 0..^ N ) )
107 elfzofz 11156 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  -  1 )  e.  ( 0..^ N )  ->  ( N  -  1 )  e.  ( 0 ... N
) )
1081, 106, 1073syl 19 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( N  -  1 )  e.  ( 0 ... N ) )
109 dvn2bss 19818 . . . . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  ( ( S  D n F ) `
 N )  C_  dom  ( ( S  D n F ) `  ( N  -  1 ) ) )
11176, 110eqsstr3d 3385 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  C_  dom  ( ( S  D n F ) `  ( N  -  1 ) ) )
112105, 111eqssd 3367 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( ( S  D n F ) `
 ( N  - 
1 ) )  =  A )
113112feq2d 5583 . . . . . . . . . . . . 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 203 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( S  D n F ) `  ( N  -  1 ) ) : A --> CC )
115114ffvelrnda 5872 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( S  D n F ) `  ( N  -  1 ) ) `  y )  e.  CC )
11676feq2d 5583 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( S  D n F ) `
 N ) : dom  ( ( S  D n F ) `
 N ) --> CC  <->  ( ( S  D n F ) `  N
) : A --> CC ) )
11786, 116mpbid 203 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( S  D n F ) `  N
) : A --> CC )
118117ffvelrnda 5872 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( S  D n F ) `  N
) `  y )  e.  CC )
1191nncnd 10018 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  CC )
120 ax-1cn 9050 . . . . . . . . . . . . . . . 16  |-  1  e.  CC
121120a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  CC )
122119, 121npcand 9417 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
123122fveq2d 5734 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( S  D n F ) `  (
( N  -  1 )  +  1 ) )  =  ( ( S  D n F ) `  N ) )
124 recnprss 19793 . . . . . . . . . . . . . . 15  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )
12568, 124syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  S  C_  CC )
126 dvnp1 19813 . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( S  D n F ) `  (
( N  -  1 )  +  1 ) )  =  ( S  _D  ( ( S  D n F ) `
 ( N  - 
1 ) ) ) )
128123, 127eqtr3d 2472 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( S  D n F ) `  N
)  =  ( S  _D  ( ( S  D n F ) `
 ( N  - 
1 ) ) ) )
129117feqmptd 5781 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( S  D n F ) `  N
)  =  ( y  e.  A  |->  ( ( ( S  D n F ) `  N
) `  y )
) )
130114feqmptd 5781 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( S  D n F ) `  ( N  -  1 ) )  =  ( y  e.  A  |->  ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y ) ) )
131130oveq2d 6099 . . . . . . . . . . . 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 2479 . . . . . . . . . . 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 3360 . . . . . . . . . . . . 13  |-  ( ph  ->  A  C_  CC )
134133sselda 3350 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  A )  ->  y  e.  CC )
135 1nn0 10239 . . . . . . . . . . . . . . . 16  |-  1  e.  NN0
136135a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  NN0 )
137 elpm2r 7036 . . . . . . . . . . . . . . . . . . . 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 1186 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( S  D n F ) `  ( N  -  1 ) )  e.  ( CC 
^pm  S ) )
139 dvn1 19814 . . . . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( S  D n ( ( S  D n F ) `
 ( N  - 
1 ) ) ) `
 1 )  =  ( S  _D  (
( S  D n F ) `  ( N  -  1 ) ) ) )
141127, 123eqtr3d 2472 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( S  _D  (
( S  D n F ) `  ( N  -  1 ) ) )  =  ( ( S  D n F ) `  N
) )
142140, 141eqtrd 2470 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( S  D n ( ( S  D n F ) `
 ( N  - 
1 ) ) ) `
 1 )  =  ( ( S  D n F ) `  N
) )
143142dmeqd 5074 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  ( ( S  D n ( ( S  D n F ) `  ( N  -  1 ) ) ) `  1 )  =  dom  ( ( S  D n F ) `  N ) )
14477, 143eleqtrrd 2515 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  e.  dom  (
( S  D n
( ( S  D n F ) `  ( N  -  1 ) ) ) `  1
) )
145 eqid 2438 . . . . . . . . . . . . . . 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 20284 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1 ( S Tayl  ( ( S  D n F ) `  ( N  -  1 ) ) ) B ) : CC --> CC )
147121, 119pncan3d 9416 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1  +  ( N  -  1 ) )  =  N )
148147oveq1d 6098 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( 1  +  ( N  -  1 ) ) ( S Tayl 
F ) B )  =  ( N ( S Tayl  F ) B ) )
149148, 78syl6reqr 2489 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  T  =  ( ( 1  +  ( N  -  1 ) ) ( S Tayl  F ) B ) )
150149oveq2d 6099 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( CC  D n T )  =  ( CC  D n ( ( 1  +  ( N  -  1 ) ) ( S Tayl  F
) B ) ) )
151150fveq1d 5732 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  1 ) )  =  ( ( CC  D n ( ( 1  +  ( N  -  1 ) ) ( S Tayl  F
) B ) ) `
 ( N  - 
1 ) ) )
152147fveq2d 5734 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( S  D n F ) `  (
1  +  ( N  -  1 ) ) )  =  ( ( S  D n F ) `  N ) )
153152dmeqd 5074 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  dom  ( ( S  D n F ) `
 ( 1  +  ( N  -  1 ) ) )  =  dom  ( ( S  D n F ) `
 N ) )
15477, 153eleqtrrd 2515 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  B  e.  dom  (
( S  D n F ) `  (
1  +  ( N  -  1 ) ) ) )
15568, 69, 70, 98, 136, 154dvntaylp 20289 . . . . . . . . . . . . . . . 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 2470 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  1 ) )  =  ( 1 ( S Tayl  ( ( S  D n F ) `  ( N  -  1 ) ) ) B ) )
157156feq1d 5582 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( CC  D n T ) `
 ( N  - 
1 ) ) : CC --> CC  <->  ( 1 ( S Tayl  ( ( S  D n F ) `  ( N  -  1 ) ) ) B ) : CC --> CC ) )
158146, 157mpbird 225 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  1 ) ) : CC --> CC )
159158ffvelrnda 5872 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `  y )  e.  CC )
160134, 159syldan 458 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  y )  e.  CC )
161 0nn0 10238 . . . . . . . . . . . . . . . 16  |-  0  e.  NN0
162161a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  e.  NN0 )
163 elpm2r 7036 . . . . . . . . . . . . . . . . . . 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 1186 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( S  D n F ) `  N
)  e.  ( CC 
^pm  S ) )
165 dvn0 19812 . . . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( S  D n ( ( S  D n F ) `
 N ) ) `
 0 )  =  ( ( S  D n F ) `  N
) )
167166dmeqd 5074 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  dom  ( ( S  D n ( ( S  D n F ) `  N ) ) `  0 )  =  dom  ( ( S  D n F ) `  N ) )
16877, 167eleqtrrd 2515 . . . . . . . . . . . . . . 15  |-  ( ph  ->  B  e.  dom  (
( S  D n
( ( S  D n F ) `  N
) ) `  0
) )
169 eqid 2438 . . . . . . . . . . . . . . 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 20284 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 0 ( S Tayl  ( ( S  D n F ) `  N
) ) B ) : CC --> CC )
171119addid2d 9269 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 0  +  N
)  =  N )
172171oveq1d 6098 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( 0  +  N ) ( S Tayl 
F ) B )  =  ( N ( S Tayl  F ) B ) )
173172, 78syl6eqr 2488 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( 0  +  N ) ( S Tayl 
F ) B )  =  T )
174173oveq2d 6099 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( CC  D n
( ( 0  +  N ) ( S Tayl 
F ) B ) )  =  ( CC  D n T ) )
175174fveq1d 5732 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( CC  D n ( ( 0  +  N ) ( S Tayl  F ) B ) ) `  N
)  =  ( ( CC  D n T ) `  N ) )
176171fveq2d 5734 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( S  D n F ) `  (
0  +  N ) )  =  ( ( S  D n F ) `  N ) )
177176dmeqd 5074 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  dom  ( ( S  D n F ) `
 ( 0  +  N ) )  =  dom  ( ( S  D n F ) `
 N ) )
17877, 177eleqtrrd 2515 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  B  e.  dom  (
( S  D n F ) `  (
0  +  N ) ) )
17968, 69, 70, 71, 162, 178dvntaylp 20289 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( CC  D n ( ( 0  +  N ) ( S Tayl  F ) B ) ) `  N
)  =  ( 0 ( S Tayl  ( ( S  D n F ) `  N ) ) B ) )
180175, 179eqtr3d 2472 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( CC  D n T ) `  N
)  =  ( 0 ( S Tayl  ( ( S  D n F ) `  N ) ) B ) )
181180feq1d 5582 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( CC  D n T ) `
 N ) : CC --> CC  <->  ( 0 ( S Tayl  ( ( S  D n F ) `  N ) ) B ) : CC --> CC ) )
182170, 181mpbird 225 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( CC  D n T ) `  N
) : CC --> CC )
183182ffvelrnda 5872 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  CC )  ->  ( ( ( CC  D n T ) `  N
) `  y )  e.  CC )
184134, 183syldan 458 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( CC  D n T ) `  N
) `  y )  e.  CC )
185125sselda 3350 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  S )  ->  y  e.  CC )
186185, 159syldan 458 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  S )  ->  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  y )  e.  CC )
187185, 183syldan 458 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  S )  ->  (
( ( CC  D n T ) `  N
) `  y )  e.  CC )
188 eqid 2438 . . . . . . . . . . . . 13  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
189188cnfldtopon 18819 . . . . . . . . . . . . . 14  |-  ( TopOpen ` fld )  e.  (TopOn `  CC )
190 toponmax 16995 . . . . . . . . . . . . . 14  |-  ( (
TopOpen ` fld )  e.  (TopOn `  CC )  ->  CC  e.  ( TopOpen ` fld ) )
191189, 190mp1i 12 . . . . . . . . . . . . 13  |-  ( ph  ->  CC  e.  ( TopOpen ` fld )
)
192 df-ss 3336 . . . . . . . . . . . . . 14  |-  ( S 
C_  CC  <->  ( S  i^i  CC )  =  S )
193125, 192sylib 190 . . . . . . . . . . . . 13  |-  ( ph  ->  ( S  i^i  CC )  =  S )
194 ssid 3369 . . . . . . . . . . . . . . . . 17  |-  CC  C_  CC
195194a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  CC  C_  CC )
196 mapsspm 7049 . . . . . . . . . . . . . . . . 17  |-  ( CC 
^m  CC )  C_  ( CC  ^pm  CC )
19768, 69, 70, 71, 77, 78taylpf 20284 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  T : CC --> CC )
19881, 81elmap 7044 . . . . . . . . . . . . . . . . . 18  |-  ( T  e.  ( CC  ^m  CC )  <->  T : CC --> CC )
199197, 198sylibr 205 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  T  e.  ( CC 
^m  CC ) )
200196, 199sseldi 3348 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  T  e.  ( CC 
^pm  CC ) )
201 dvnp1 19813 . . . . . . . . . . . . . . . 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 1185 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( CC  D n T ) `  (
( N  -  1 )  +  1 ) )  =  ( CC 
_D  ( ( CC  D n T ) `
 ( N  - 
1 ) ) ) )
203122fveq2d 5734 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( CC  D n T ) `  (
( N  -  1 )  +  1 ) )  =  ( ( CC  D n T ) `  N ) )
204202, 203eqtr3d 2472 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( CC  _D  (
( CC  D n T ) `  ( N  -  1 ) ) )  =  ( ( CC  D n T ) `  N
) )
205158feqmptd 5781 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  1 ) )  =  ( y  e.  CC  |->  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `  y ) ) )
206205oveq2d 6099 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( CC  _D  (
( CC  D n T ) `  ( N  -  1 ) ) )  =  ( CC  _D  ( y  e.  CC  |->  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `  y ) ) ) )
207182feqmptd 5781 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( CC  D n T ) `  N
)  =  ( y  e.  CC  |->  ( ( ( CC  D n T ) `  N
) `  y )
) )
208204, 206, 2073eqtr3d 2478 . . . . . . . . . . . . 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 19844 . . . . . . . . . . . 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 2438 . . . . . . . . . . . 12  |-  ( (
TopOpen ` fld )t  S )  =  ( ( TopOpen ` fld )t  S )
211 resttopon 17227 . . . . . . . . . . . . . . . 16  |-  ( ( ( TopOpen ` fld )  e.  (TopOn `  CC )  /\  S  C_  CC )  ->  (
( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
212189, 125, 211sylancr 646 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( TopOpen ` fld )t  S )  e.  (TopOn `  S ) )
213 topontop 16993 . . . . . . . . . . . . . . 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 16994 . . . . . . . . . . . . . . . 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 3386 . . . . . . . . . . . . . 14  |-  ( ph  ->  A  C_  U. (
( TopOpen ` fld )t  S ) )
218 eqid 2438 . . . . . . . . . . . . . . 15  |-  U. (
( TopOpen ` fld )t  S )  =  U. ( ( TopOpen ` fld )t  S )
219218ntrss2 17123 . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  A )  C_  A
)
221141dmeqd 5074 . . . . . . . . . . . . . . 15  |-  ( ph  ->  dom  ( S  _D  ( ( S  D n F ) `  ( N  -  1 ) ) )  =  dom  ( ( S  D n F ) `  N
) )
222221, 76eqtrd 2470 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( S  _D  ( ( S  D n F ) `  ( N  -  1 ) ) )  =  A )
223125, 114, 70, 210, 188dvbssntr 19789 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  ( S  _D  ( ( S  D n F ) `  ( N  -  1 ) ) )  C_  (
( int `  (
( TopOpen ` fld )t  S ) ) `  A ) )
224222, 223eqsstr3d 3385 . . . . . . . . . . . . 13  |-  ( ph  ->  A  C_  ( ( int `  ( ( TopOpen ` fld )t  S
) ) `  A
) )
225220, 224eqssd 3367 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( int `  (
( TopOpen ` fld )t  S ) ) `  A )  =  A )
22668, 186, 187, 209, 70, 210, 188, 225dvmptres2 19850 . . . . . . . . . . 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 19855 . . . . . . . . . 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 4225 . . . . . . . . 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 225 . . . . . . . 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 2438 . . . . . . . . 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 9413 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  A )  ->  (
( ( ( S  D n F ) `
 ( N  - 
1 ) ) `  y )  -  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  y ) )  e.  CC )
232 eqid 2438 . . . . . . . . . 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 5895 . . . . . . . . 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 19787 . . . . . . . 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 203 . . . . . . 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 451 . . . . . 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 3471 . . . . . . . . . 10  |-  ( x  e.  ( A  \  { B } )  ->  x  e.  A )
238 fveq2 5730 . . . . . . . . . . . . . 14  |-  ( y  =  x  ->  (
( ( S  D n F ) `  ( N  -  1 ) ) `  y )  =  ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 x ) )
239 fveq2 5730 . . . . . . . . . . . . . 14  |-  ( y  =  x  ->  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  y )  =  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 x ) )
240238, 239oveq12d 6101 . . . . . . . . . . . . 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 6108 . . . . . . . . . . . . 13  |-  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  x )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 x ) )  e.  _V
242240, 232, 241fvmpt 5808 . . . . . . . . . . . 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 5730 . . . . . . . . . . . . . . . 16  |-  ( y  =  B  ->  (
( ( S  D n F ) `  ( N  -  1 ) ) `  y )  =  ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 B ) )
244 fveq2 5730 . . . . . . . . . . . . . . . 16  |-  ( y  =  B  ->  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  y )  =  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 B ) )
245243, 244oveq12d 6101 . . . . . . . . . . . . . . 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 6108 . . . . . . . . . . . . . . 15  |-  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  B )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 B ) )  e.  _V
247245, 232, 246fvmpt 5808 . . . . . . . . . . . . . 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 20290 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( CC  D n T ) `
 ( N  - 
1 ) ) `  B )  =  ( ( ( S  D n F ) `  ( N  -  1 ) ) `  B ) )
250249oveq2d 6099 . . . . . . . . . . . . 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 5873 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( S  D n F ) `
 ( N  - 
1 ) ) `  B )  e.  CC )
252251subidd 9401 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `
 B )  -  ( ( ( S  D n F ) `
 ( N  - 
1 ) ) `  B ) )  =  0 )
253248, 250, 2523eqtrd 2474 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( y  e.  A  |->  ( ( ( ( S  D n F ) `  ( N  -  1 ) ) `  y )  -  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `
 y ) ) ) `  B )  =  0 )
254242, 253oveqan12rd 6103 . . . . . . . . . . 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 5872 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( S  D n F ) `  ( N  -  1 ) ) `  x )  e.  CC )
256133sselda 3350 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  A )  ->  x  e.  CC )
257158ffvelrnda 5872 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  x  e.  CC )  ->  ( ( ( CC  D n T ) `  ( N  -  1 ) ) `  x )  e.  CC )
258256, 257syldan 458 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  x )  e.  CC )
259255, 258subcld 9413 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  A )  ->  (
( ( ( S  D n F ) `
 ( N  - 
1 ) ) `  x )  -  (
( ( CC  D n T ) `  ( N  -  1 ) ) `  x ) )  e.  CC )
260259subid1d 9402 . . . . . . . . . . 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 2471 . . . . . . . . . 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 462 . . . . . . . . 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 3487 . . . . . . . . . . . 12  |-  ( ph  ->  ( A  \  { B } )  C_  CC )
264263sselda 3350 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  x  e.  CC )
265133, 60sseldd 3351 . . . . . . . . . . . 12  |-  ( ph  ->  B  e.  CC )
266265adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  ->  B  e.  CC )
267264, 266subcld 9413 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( x  -  B
)  e.  CC )
268267exp1d 11520 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( A  \  { B } ) )  -> 
( ( x  -  B ) ^ 1 )  =  ( x  -  B ) )
269262, 268oveq12d 6101 . . . . . . . 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 4297 . . . . . . 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 6098 . . . . . 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 2515 . . . . 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 600 . . . . . 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 426 . . . . 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 25 . . . 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 11200 . . 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 35 . 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 9401 . . . . . . . . . 10  |-  ( ph  ->  ( N  -  N
)  =  0 )
281280fveq2d 5734 . . . . . . . . 9  |-  ( ph  ->  ( ( S  D n F ) `  ( N  -  N )
)  =  ( ( S  D n F ) `  0 ) )
282 dvn0 19812 . . . . . . . . . 10  |-  ( ( S  C_  CC  /\  F  e.  ( CC  ^pm  S
) )  ->  (
( S  D n F ) `  0
)  =  F )
283125, 84, 282syl2anc 644 . . . . . . . . 9  |-  ( ph  ->  ( ( S  D n F ) `  0
)  =  F )
284281, 283eqtrd 2470 . . . . . . . 8  |-  ( ph  ->  ( ( S  D n F ) `  ( N  -  N )
)  =  F )
285284fveq1d 5732 . . . . . . 7  |-  ( ph  ->  ( ( ( S  D n F ) `
 ( N  -  N ) ) `  x )  =  ( F `  x ) )
286280fveq2d 5734 . . . . . . . . 9  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  N )
)  =  ( ( CC  D n T ) `  0 ) )
287 dvn0 19812 . . . . . . . . . 10  |-  ( ( CC  C_  CC  /\  T  e.  ( CC  ^pm  CC ) )  ->  (
( CC  D n T ) `  0
)  =  T )
288194, 200, 287sylancr 646 . . . . . . . . 9  |-  ( ph  ->  ( ( CC  D n T ) `  0
)  =  T )
289286, 288eqtrd 2470 . . . . . . . 8  |-  ( ph  ->  ( ( CC  D n T ) `  ( N  -  N )
)  =  T )
290289fveq1d 5732 . . . . . . 7  |-  ( ph  ->  ( ( ( CC  D n T ) `
 ( N  -  N ) ) `  x )  =  ( T `  x ) )
291285, 290oveq12d 6101 . . . . . 6  |-  ( ph  ->  ( ( ( ( S  D n F ) `  ( N  -  N ) ) `
 x )  -  ( ( ( CC  D n T ) `
 ( N  -  N ) ) `  x ) )  =  ( ( F `  x )  -  ( T `  x )
) )
292291oveq1d 6098 . . . . 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 4298 . . . 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 2488 . . 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 6098 . 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 2514 1  |-  ( ph  ->  0  e.  ( R lim
CC  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1726   _Vcvv 2958    \ cdif 3319    i^i cin 3321    C_ wss 3322   {csn 3816   {cpr 3817   U.cuni 4017   class class class wbr 4214    e. cmpt 4268   dom cdm 4880   Fun wfun 5450   -->wf 5452   ` cfv 5456  (class class class)co 6083    ^m cmap 7020    ^pm cpm 7021   CCcc 8990   RRcr 8991   0cc0 8992   1c1 8993    + caddc 8995    - cmin 9293    / cdiv 9679   NNcn 10002   NN0cn0 10223   ZZ>=cuz 10490   ...cfz 11045  ..^cfzo 11137   ^cexp 11384   ↾t crest 13650   TopOpenctopn 13651  ℂfldccnfld 16705   Topctop 16960  TopOnctopon 16961   intcnt 17083   lim CC climc 19751    _D cdv 19752    D ncdvn 19753   Tayl ctayl 20271
This theorem is referenced by:  taylth  20293
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-rep 4322  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703  ax-inf2 7598  ax-cnex 9048  ax-resscn 9049  ax-1cn 9050  ax-icn 9051  ax-addcl 9052  ax-addrcl 9053  ax-mulcl 9054  ax-mulrcl 9055  ax-mulcom 9056  ax-addass 9057  ax-mulass 9058  ax-distr 9059  ax-i2m1 9060  ax-1ne0 9061  ax-1rid 9062  ax-rnegex 9063  ax-rrecex 9064  ax-cnre 9065  ax-pre-lttri 9066  ax-pre-lttrn 9067  ax-pre-ltadd 9068  ax-pre-mulgt0 9069  ax-pre-sup 9070  ax-addf 9071  ax-mulf 9072
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-reu 2714  df-rmo 2715  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-int 4053  df-iun 4097  df-iin 4098  df-br 4215  df-opab 4269  df-mpt 4270  df-tr 4305  df-eprel 4496  df-id 4500  df-po 4505  df-so 4506  df-fr 4543  df-se 4544  df-we 4545  df-ord 4586  df-on 4587  df-lim 4588  df-suc 4589  df-om 4848  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-fv 5464  df-isom 5465  df-ov 6086  df-oprab 6087  df-mpt2 6088  df-of 6307  df-1st 6351  df-2nd 6352  df-riota 6551  df-recs 6635  df-rdg 6670  df-1o 6726  df-2o 6727  df-oadd 6730  df-er 6907  df-map 7022  df-pm 7023  df-ixp 7066  df-en 7112  df-dom 7113  df-sdom 7114  df-fin 7115  df-fi 7418  df-sup 7448  df-oi 7481  df-card 7828  df-cda 8050  df-pnf 9124  df-mnf 9125  df-xr 9126  df-ltxr 9127  df-le 9128  df-sub 9295  df-neg 9296  df-div 9680  df-nn 10003  df-2 10060  df-3 10061  df-4 10062  df-5 10063  df-6 10064  df-7 10065  df-8 10066  df-9 10067  df-10 10068  df-n0 10224  df-z 10285  df-dec 10385  df-uz 10491  df-q 10577  df-rp 10615  df-xneg 10712  df-xadd 10713  df-xmul 10714  df-icc 10925  df-fz 11046  df-fzo 11138  df-seq 11326  df-exp 11385  df-fac 11569  df-hash 11621  df-cj 11906  df-re 11907  df-im 11908  df-sqr 12042  df-abs 12043  df-clim 12284  df-sum 12482  df-struct 13473  df-ndx 13474  df-slot 13475  df-base 13476  df-sets 13477  df-ress 13478  df-plusg 13544  df-mulr 13545  df-starv 13546  df-sca 13547  df-vsca 13548  df-tset 13550  df-ple 13551  df-ds 13553  df-unif 13554  df-hom 13555  df-cco 13556  df-rest 13652  df-topn 13653  df-topgen 13669  df-pt 13670  df-prds 13673  df-xrs 13728  df-0g 13729  df-gsum 13730  df-qtop 13735  df-imas 13736  df-xps 13738  df-mre 13813  df-mrc 13814  df-acs 13816  df-mnd 14692  df-submnd 14741  df-grp 14814  df-minusg 14815  df-mulg 14817  df-cntz 15118  df-cmn 15416  df-abl 15417  df-mgp 15651  df-rng 15665  df-cring 15666  df-ur 15667  df-psmet 16696  df-xmet 16697  df-met 16698  df-bl 16699  df-mopn 16700  df-fbas 16701  df-fg 16702  df-cnfld 16706  df-top 16965  df-bases 16967  df-topon 16968  df-topsp 16969  df-cld 17085  df-ntr 17086  df-cls 17087  df-nei 17164  df-lp 17202  df-perf 17203  df-cn 17293  df-cnp 17294  df-haus 17381  df-tx 17596  df-hmeo 17789  df-fil 17880  df-fm 17972  df-flim 17973  df-flf 17974  df-tsms 18158  df-xms 18352  df-ms 18353  df-tms 18354  df-cncf 18910  df-limc 19755  df-dv 19756  df-dvn 19757  df-tayl 20273
  Copyright terms: Public domain W3C validator