Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvnmul Structured version   Unicode version

Theorem dvnmul 37121
Description: Function-builder for the  N-th derivative, product rule. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
dvnmul.s  |-  ( ph  ->  S  e.  { RR ,  CC } )
dvnmul.x  |-  ( ph  ->  X  e.  ( (
TopOpen ` fld )t  S ) )
dvnmul.a  |-  ( (
ph  /\  x  e.  X )  ->  A  e.  CC )
dvnmul.cc  |-  ( (
ph  /\  x  e.  X )  ->  B  e.  CC )
dvnmul.n  |-  ( ph  ->  N  e.  NN0 )
dvnmulf  |-  F  =  ( x  e.  X  |->  A )
dvnmul.f  |-  G  =  ( x  e.  X  |->  B )
dvnmul.dvnf  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
( S  Dn
F ) `  k
) : X --> CC )
dvnmul.dvng  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
( S  Dn
G ) `  k
) : X --> CC )
dvnmul.c  |-  C  =  ( k  e.  ( 0 ... N ) 
|->  ( ( S  Dn F ) `  k ) )
dvnmul.d  |-  D  =  ( k  e.  ( 0 ... N ) 
|->  ( ( S  Dn G ) `  k ) )
Assertion
Ref Expression
dvnmul  |-  ( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `
 N )  =  ( x  e.  X  |-> 
sum_ k  e.  ( 0 ... N ) ( ( N  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( N  -  k ) ) `
 x ) ) ) ) )
Distinct variable groups:    A, k    B, k    x, C    x, D    k, F    k, G    k, N, x    S, k, x    k, X, x    ph, k, x
Allowed substitution hints:    A( x)    B( x)    C( k)    D( k)    F( x)    G( x)

Proof of Theorem dvnmul
Dummy variables  i  m  n  h  j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 id 23 . 2  |-  ( ph  ->  ph )
2 dvnmul.n . . 3  |-  ( ph  ->  N  e.  NN0 )
3 nn0uz 11163 . . . . 5  |-  NN0  =  ( ZZ>= `  0 )
42, 3syl6eleq 2502 . . . 4  |-  ( ph  ->  N  e.  ( ZZ>= ` 
0 ) )
5 eluzfz2 11750 . . . 4  |-  ( N  e.  ( ZZ>= `  0
)  ->  N  e.  ( 0 ... N
) )
64, 5syl 17 . . 3  |-  ( ph  ->  N  e.  ( 0 ... N ) )
7 eleq1 2476 . . . . 5  |-  ( n  =  N  ->  (
n  e.  ( 0 ... N )  <->  N  e.  ( 0 ... N
) ) )
8 fveq2 5851 . . . . . . 7  |-  ( n  =  N  ->  (
( S  Dn
( x  e.  X  |->  ( A  x.  B
) ) ) `  n )  =  ( ( S  Dn
( x  e.  X  |->  ( A  x.  B
) ) ) `  N ) )
9 oveq2 6288 . . . . . . . . . 10  |-  ( n  =  N  ->  (
0 ... n )  =  ( 0 ... N
) )
109sumeq1d 13674 . . . . . . . . 9  |-  ( n  =  N  ->  sum_ k  e.  ( 0 ... n
) ( ( n  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
n  -  k ) ) `  x ) ) )  =  sum_ k  e.  ( 0 ... N ) ( ( n  _C  k
)  x.  ( ( ( C `  k
) `  x )  x.  ( ( D `  ( n  -  k
) ) `  x
) ) ) )
11 oveq1 6287 . . . . . . . . . . 11  |-  ( n  =  N  ->  (
n  _C  k )  =  ( N  _C  k ) )
12 oveq1 6287 . . . . . . . . . . . . . 14  |-  ( n  =  N  ->  (
n  -  k )  =  ( N  -  k ) )
1312fveq2d 5855 . . . . . . . . . . . . 13  |-  ( n  =  N  ->  ( D `  ( n  -  k ) )  =  ( D `  ( N  -  k
) ) )
1413fveq1d 5853 . . . . . . . . . . . 12  |-  ( n  =  N  ->  (
( D `  (
n  -  k ) ) `  x )  =  ( ( D `
 ( N  -  k ) ) `  x ) )
1514oveq2d 6296 . . . . . . . . . . 11  |-  ( n  =  N  ->  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( n  -  k ) ) `
 x ) )  =  ( ( ( C `  k ) `
 x )  x.  ( ( D `  ( N  -  k
) ) `  x
) ) )
1611, 15oveq12d 6298 . . . . . . . . . 10  |-  ( n  =  N  ->  (
( n  _C  k
)  x.  ( ( ( C `  k
) `  x )  x.  ( ( D `  ( n  -  k
) ) `  x
) ) )  =  ( ( N  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( N  -  k ) ) `
 x ) ) ) )
1716sumeq2ad 36947 . . . . . . . . 9  |-  ( n  =  N  ->  sum_ k  e.  ( 0 ... N
) ( ( n  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
n  -  k ) ) `  x ) ) )  =  sum_ k  e.  ( 0 ... N ) ( ( N  _C  k
)  x.  ( ( ( C `  k
) `  x )  x.  ( ( D `  ( N  -  k
) ) `  x
) ) ) )
1810, 17eqtrd 2445 . . . . . . . 8  |-  ( n  =  N  ->  sum_ k  e.  ( 0 ... n
) ( ( n  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
n  -  k ) ) `  x ) ) )  =  sum_ k  e.  ( 0 ... N ) ( ( N  _C  k
)  x.  ( ( ( C `  k
) `  x )  x.  ( ( D `  ( N  -  k
) ) `  x
) ) ) )
1918mpteq2dv 4484 . . . . . . 7  |-  ( n  =  N  ->  (
x  e.  X  |->  sum_ k  e.  ( 0 ... n ) ( ( n  _C  k
)  x.  ( ( ( C `  k
) `  x )  x.  ( ( D `  ( n  -  k
) ) `  x
) ) ) )  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... N ) ( ( N  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( N  -  k ) ) `
 x ) ) ) ) )
208, 19eqeq12d 2426 . . . . . 6  |-  ( n  =  N  ->  (
( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `
 n )  =  ( x  e.  X  |-> 
sum_ k  e.  ( 0 ... n ) ( ( n  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( n  -  k ) ) `
 x ) ) ) )  <->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  N )  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... N ) ( ( N  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( N  -  k ) ) `
 x ) ) ) ) ) )
2120imbi2d 316 . . . . 5  |-  ( n  =  N  ->  (
( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  n
)  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... n
) ( ( n  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
n  -  k ) ) `  x ) ) ) ) )  <-> 
( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  N
)  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... N
) ( ( N  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  ( N  -  k )
) `  x )
) ) ) ) ) )
227, 21imbi12d 320 . . . 4  |-  ( n  =  N  ->  (
( n  e.  ( 0 ... N )  ->  ( ph  ->  ( ( S  Dn
( x  e.  X  |->  ( A  x.  B
) ) ) `  n )  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... n ) ( ( n  _C  k
)  x.  ( ( ( C `  k
) `  x )  x.  ( ( D `  ( n  -  k
) ) `  x
) ) ) ) ) )  <->  ( N  e.  ( 0 ... N
)  ->  ( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `
 N )  =  ( x  e.  X  |-> 
sum_ k  e.  ( 0 ... N ) ( ( N  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( N  -  k ) ) `
 x ) ) ) ) ) ) ) )
23 fveq2 5851 . . . . . . 7  |-  ( m  =  0  ->  (
( S  Dn
( x  e.  X  |->  ( A  x.  B
) ) ) `  m )  =  ( ( S  Dn
( x  e.  X  |->  ( A  x.  B
) ) ) ` 
0 ) )
24 simpl 457 . . . . . . . . . 10  |-  ( ( m  =  0  /\  x  e.  X )  ->  m  =  0 )
2524oveq2d 6296 . . . . . . . . 9  |-  ( ( m  =  0  /\  x  e.  X )  ->  ( 0 ... m )  =  ( 0 ... 0 ) )
26 simpll 754 . . . . . . . . . . 11  |-  ( ( ( m  =  0  /\  x  e.  X
)  /\  k  e.  ( 0 ... 0
) )  ->  m  =  0 )
2726oveq1d 6295 . . . . . . . . . 10  |-  ( ( ( m  =  0  /\  x  e.  X
)  /\  k  e.  ( 0 ... 0
) )  ->  (
m  _C  k )  =  ( 0  _C  k ) )
2826oveq1d 6295 . . . . . . . . . . . . 13  |-  ( ( ( m  =  0  /\  x  e.  X
)  /\  k  e.  ( 0 ... 0
) )  ->  (
m  -  k )  =  ( 0  -  k ) )
2928fveq2d 5855 . . . . . . . . . . . 12  |-  ( ( ( m  =  0  /\  x  e.  X
)  /\  k  e.  ( 0 ... 0
) )  ->  ( D `  ( m  -  k ) )  =  ( D `  ( 0  -  k
) ) )
3029fveq1d 5853 . . . . . . . . . . 11  |-  ( ( ( m  =  0  /\  x  e.  X
)  /\  k  e.  ( 0 ... 0
) )  ->  (
( D `  (
m  -  k ) ) `  x )  =  ( ( D `
 ( 0  -  k ) ) `  x ) )
3130oveq2d 6296 . . . . . . . . . 10  |-  ( ( ( m  =  0  /\  x  e.  X
)  /\  k  e.  ( 0 ... 0
) )  ->  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( m  -  k ) ) `
 x ) )  =  ( ( ( C `  k ) `
 x )  x.  ( ( D `  ( 0  -  k
) ) `  x
) ) )
3227, 31oveq12d 6298 . . . . . . . . 9  |-  ( ( ( m  =  0  /\  x  e.  X
)  /\  k  e.  ( 0 ... 0
) )  ->  (
( m  _C  k
)  x.  ( ( ( C `  k
) `  x )  x.  ( ( D `  ( m  -  k
) ) `  x
) ) )  =  ( ( 0  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( 0  -  k ) ) `
 x ) ) ) )
3325, 32sumeq12rdv 13680 . . . . . . . 8  |-  ( ( m  =  0  /\  x  e.  X )  ->  sum_ k  e.  ( 0 ... m ) ( ( m  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( m  -  k ) ) `
 x ) ) )  =  sum_ k  e.  ( 0 ... 0
) ( ( 0  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
0  -  k ) ) `  x ) ) ) )
3433mpteq2dva 4483 . . . . . . 7  |-  ( m  =  0  ->  (
x  e.  X  |->  sum_ k  e.  ( 0 ... m ) ( ( m  _C  k
)  x.  ( ( ( C `  k
) `  x )  x.  ( ( D `  ( m  -  k
) ) `  x
) ) ) )  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... 0 ) ( ( 0  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( 0  -  k ) ) `
 x ) ) ) ) )
3523, 34eqeq12d 2426 . . . . . 6  |-  ( m  =  0  ->  (
( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `
 m )  =  ( x  e.  X  |-> 
sum_ k  e.  ( 0 ... m ) ( ( m  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( m  -  k ) ) `
 x ) ) ) )  <->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  0 )  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... 0 ) ( ( 0  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( 0  -  k ) ) `
 x ) ) ) ) ) )
3635imbi2d 316 . . . . 5  |-  ( m  =  0  ->  (
( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  m
)  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... m
) ( ( m  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
m  -  k ) ) `  x ) ) ) ) )  <-> 
( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  0
)  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... 0
) ( ( 0  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
0  -  k ) ) `  x ) ) ) ) ) ) )
37 fveq2 5851 . . . . . . 7  |-  ( m  =  i  ->  (
( S  Dn
( x  e.  X  |->  ( A  x.  B
) ) ) `  m )  =  ( ( S  Dn
( x  e.  X  |->  ( A  x.  B
) ) ) `  i ) )
38 simpl 457 . . . . . . . . . 10  |-  ( ( m  =  i  /\  x  e.  X )  ->  m  =  i )
3938oveq2d 6296 . . . . . . . . 9  |-  ( ( m  =  i  /\  x  e.  X )  ->  ( 0 ... m
)  =  ( 0 ... i ) )
40 simpll 754 . . . . . . . . . . 11  |-  ( ( ( m  =  i  /\  x  e.  X
)  /\  k  e.  ( 0 ... i
) )  ->  m  =  i )
4140oveq1d 6295 . . . . . . . . . 10  |-  ( ( ( m  =  i  /\  x  e.  X
)  /\  k  e.  ( 0 ... i
) )  ->  (
m  _C  k )  =  ( i  _C  k ) )
4240oveq1d 6295 . . . . . . . . . . . . 13  |-  ( ( ( m  =  i  /\  x  e.  X
)  /\  k  e.  ( 0 ... i
) )  ->  (
m  -  k )  =  ( i  -  k ) )
4342fveq2d 5855 . . . . . . . . . . . 12  |-  ( ( ( m  =  i  /\  x  e.  X
)  /\  k  e.  ( 0 ... i
) )  ->  ( D `  ( m  -  k ) )  =  ( D `  ( i  -  k
) ) )
4443fveq1d 5853 . . . . . . . . . . 11  |-  ( ( ( m  =  i  /\  x  e.  X
)  /\  k  e.  ( 0 ... i
) )  ->  (
( D `  (
m  -  k ) ) `  x )  =  ( ( D `
 ( i  -  k ) ) `  x ) )
4544oveq2d 6296 . . . . . . . . . 10  |-  ( ( ( m  =  i  /\  x  e.  X
)  /\  k  e.  ( 0 ... i
) )  ->  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( m  -  k ) ) `
 x ) )  =  ( ( ( C `  k ) `
 x )  x.  ( ( D `  ( i  -  k
) ) `  x
) ) )
4641, 45oveq12d 6298 . . . . . . . . 9  |-  ( ( ( m  =  i  /\  x  e.  X
)  /\  k  e.  ( 0 ... i
) )  ->  (
( m  _C  k
)  x.  ( ( ( C `  k
) `  x )  x.  ( ( D `  ( m  -  k
) ) `  x
) ) )  =  ( ( i  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( i  -  k ) ) `
 x ) ) ) )
4739, 46sumeq12rdv 13680 . . . . . . . 8  |-  ( ( m  =  i  /\  x  e.  X )  -> 
sum_ k  e.  ( 0 ... m ) ( ( m  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( m  -  k ) ) `
 x ) ) )  =  sum_ k  e.  ( 0 ... i
) ( ( i  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
i  -  k ) ) `  x ) ) ) )
4847mpteq2dva 4483 . . . . . . 7  |-  ( m  =  i  ->  (
x  e.  X  |->  sum_ k  e.  ( 0 ... m ) ( ( m  _C  k
)  x.  ( ( ( C `  k
) `  x )  x.  ( ( D `  ( m  -  k
) ) `  x
) ) ) )  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... i ) ( ( i  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( i  -  k ) ) `
 x ) ) ) ) )
4937, 48eqeq12d 2426 . . . . . 6  |-  ( m  =  i  ->  (
( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `
 m )  =  ( x  e.  X  |-> 
sum_ k  e.  ( 0 ... m ) ( ( m  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( m  -  k ) ) `
 x ) ) ) )  <->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  i )  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... i ) ( ( i  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( i  -  k ) ) `
 x ) ) ) ) ) )
5049imbi2d 316 . . . . 5  |-  ( m  =  i  ->  (
( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  m
)  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... m
) ( ( m  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
m  -  k ) ) `  x ) ) ) ) )  <-> 
( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  i
)  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... i
) ( ( i  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
i  -  k ) ) `  x ) ) ) ) ) ) )
51 fveq2 5851 . . . . . . 7  |-  ( m  =  ( i  +  1 )  ->  (
( S  Dn
( x  e.  X  |->  ( A  x.  B
) ) ) `  m )  =  ( ( S  Dn
( x  e.  X  |->  ( A  x.  B
) ) ) `  ( i  +  1 ) ) )
52 simpl 457 . . . . . . . . . 10  |-  ( ( m  =  ( i  +  1 )  /\  x  e.  X )  ->  m  =  ( i  +  1 ) )
5352oveq2d 6296 . . . . . . . . 9  |-  ( ( m  =  ( i  +  1 )  /\  x  e.  X )  ->  ( 0 ... m
)  =  ( 0 ... ( i  +  1 ) ) )
54 simpll 754 . . . . . . . . . . 11  |-  ( ( ( m  =  ( i  +  1 )  /\  x  e.  X
)  /\  k  e.  ( 0 ... (
i  +  1 ) ) )  ->  m  =  ( i  +  1 ) )
5554oveq1d 6295 . . . . . . . . . 10  |-  ( ( ( m  =  ( i  +  1 )  /\  x  e.  X
)  /\  k  e.  ( 0 ... (
i  +  1 ) ) )  ->  (
m  _C  k )  =  ( ( i  +  1 )  _C  k ) )
5654oveq1d 6295 . . . . . . . . . . . . 13  |-  ( ( ( m  =  ( i  +  1 )  /\  x  e.  X
)  /\  k  e.  ( 0 ... (
i  +  1 ) ) )  ->  (
m  -  k )  =  ( ( i  +  1 )  -  k ) )
5756fveq2d 5855 . . . . . . . . . . . 12  |-  ( ( ( m  =  ( i  +  1 )  /\  x  e.  X
)  /\  k  e.  ( 0 ... (
i  +  1 ) ) )  ->  ( D `  ( m  -  k ) )  =  ( D `  ( ( i  +  1 )  -  k
) ) )
5857fveq1d 5853 . . . . . . . . . . 11  |-  ( ( ( m  =  ( i  +  1 )  /\  x  e.  X
)  /\  k  e.  ( 0 ... (
i  +  1 ) ) )  ->  (
( D `  (
m  -  k ) ) `  x )  =  ( ( D `
 ( ( i  +  1 )  -  k ) ) `  x ) )
5958oveq2d 6296 . . . . . . . . . 10  |-  ( ( ( m  =  ( i  +  1 )  /\  x  e.  X
)  /\  k  e.  ( 0 ... (
i  +  1 ) ) )  ->  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( m  -  k ) ) `
 x ) )  =  ( ( ( C `  k ) `
 x )  x.  ( ( D `  ( ( i  +  1 )  -  k
) ) `  x
) ) )
6055, 59oveq12d 6298 . . . . . . . . 9  |-  ( ( ( m  =  ( i  +  1 )  /\  x  e.  X
)  /\  k  e.  ( 0 ... (
i  +  1 ) ) )  ->  (
( m  _C  k
)  x.  ( ( ( C `  k
) `  x )  x.  ( ( D `  ( m  -  k
) ) `  x
) ) )  =  ( ( ( i  +  1 )  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( ( i  +  1 )  -  k ) ) `
 x ) ) ) )
6153, 60sumeq12rdv 13680 . . . . . . . 8  |-  ( ( m  =  ( i  +  1 )  /\  x  e.  X )  -> 
sum_ k  e.  ( 0 ... m ) ( ( m  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( m  -  k ) ) `
 x ) ) )  =  sum_ k  e.  ( 0 ... (
i  +  1 ) ) ( ( ( i  +  1 )  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
( i  +  1 )  -  k ) ) `  x ) ) ) )
6261mpteq2dva 4483 . . . . . . 7  |-  ( m  =  ( i  +  1 )  ->  (
x  e.  X  |->  sum_ k  e.  ( 0 ... m ) ( ( m  _C  k
)  x.  ( ( ( C `  k
) `  x )  x.  ( ( D `  ( m  -  k
) ) `  x
) ) ) )  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... ( i  +  1 ) ) ( ( ( i  +  1 )  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( ( i  +  1 )  -  k ) ) `
 x ) ) ) ) )
6351, 62eqeq12d 2426 . . . . . 6  |-  ( m  =  ( i  +  1 )  ->  (
( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `
 m )  =  ( x  e.  X  |-> 
sum_ k  e.  ( 0 ... m ) ( ( m  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( m  -  k ) ) `
 x ) ) ) )  <->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  ( i  +  1 ) )  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... ( i  +  1 ) ) ( ( ( i  +  1 )  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( ( i  +  1 )  -  k ) ) `
 x ) ) ) ) ) )
6463imbi2d 316 . . . . 5  |-  ( m  =  ( i  +  1 )  ->  (
( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  m
)  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... m
) ( ( m  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
m  -  k ) ) `  x ) ) ) ) )  <-> 
( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  (
i  +  1 ) )  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... (
i  +  1 ) ) ( ( ( i  +  1 )  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
( i  +  1 )  -  k ) ) `  x ) ) ) ) ) ) )
65 fveq2 5851 . . . . . . 7  |-  ( m  =  n  ->  (
( S  Dn
( x  e.  X  |->  ( A  x.  B
) ) ) `  m )  =  ( ( S  Dn
( x  e.  X  |->  ( A  x.  B
) ) ) `  n ) )
66 simpl 457 . . . . . . . . . 10  |-  ( ( m  =  n  /\  x  e.  X )  ->  m  =  n )
6766oveq2d 6296 . . . . . . . . 9  |-  ( ( m  =  n  /\  x  e.  X )  ->  ( 0 ... m
)  =  ( 0 ... n ) )
68 simpll 754 . . . . . . . . . . 11  |-  ( ( ( m  =  n  /\  x  e.  X
)  /\  k  e.  ( 0 ... n
) )  ->  m  =  n )
6968oveq1d 6295 . . . . . . . . . 10  |-  ( ( ( m  =  n  /\  x  e.  X
)  /\  k  e.  ( 0 ... n
) )  ->  (
m  _C  k )  =  ( n  _C  k ) )
7068oveq1d 6295 . . . . . . . . . . . . 13  |-  ( ( ( m  =  n  /\  x  e.  X
)  /\  k  e.  ( 0 ... n
) )  ->  (
m  -  k )  =  ( n  -  k ) )
7170fveq2d 5855 . . . . . . . . . . . 12  |-  ( ( ( m  =  n  /\  x  e.  X
)  /\  k  e.  ( 0 ... n
) )  ->  ( D `  ( m  -  k ) )  =  ( D `  ( n  -  k
) ) )
7271fveq1d 5853 . . . . . . . . . . 11  |-  ( ( ( m  =  n  /\  x  e.  X
)  /\  k  e.  ( 0 ... n
) )  ->  (
( D `  (
m  -  k ) ) `  x )  =  ( ( D `
 ( n  -  k ) ) `  x ) )
7372oveq2d 6296 . . . . . . . . . 10  |-  ( ( ( m  =  n  /\  x  e.  X
)  /\  k  e.  ( 0 ... n
) )  ->  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( m  -  k ) ) `
 x ) )  =  ( ( ( C `  k ) `
 x )  x.  ( ( D `  ( n  -  k
) ) `  x
) ) )
7469, 73oveq12d 6298 . . . . . . . . 9  |-  ( ( ( m  =  n  /\  x  e.  X
)  /\  k  e.  ( 0 ... n
) )  ->  (
( m  _C  k
)  x.  ( ( ( C `  k
) `  x )  x.  ( ( D `  ( m  -  k
) ) `  x
) ) )  =  ( ( n  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( n  -  k ) ) `
 x ) ) ) )
7567, 74sumeq12rdv 13680 . . . . . . . 8  |-  ( ( m  =  n  /\  x  e.  X )  -> 
sum_ k  e.  ( 0 ... m ) ( ( m  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( m  -  k ) ) `
 x ) ) )  =  sum_ k  e.  ( 0 ... n
) ( ( n  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
n  -  k ) ) `  x ) ) ) )
7675mpteq2dva 4483 . . . . . . 7  |-  ( m  =  n  ->  (
x  e.  X  |->  sum_ k  e.  ( 0 ... m ) ( ( m  _C  k
)  x.  ( ( ( C `  k
) `  x )  x.  ( ( D `  ( m  -  k
) ) `  x
) ) ) )  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... n ) ( ( n  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( n  -  k ) ) `
 x ) ) ) ) )
7765, 76eqeq12d 2426 . . . . . 6  |-  ( m  =  n  ->  (
( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `
 m )  =  ( x  e.  X  |-> 
sum_ k  e.  ( 0 ... m ) ( ( m  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( m  -  k ) ) `
 x ) ) ) )  <->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  n )  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... n ) ( ( n  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( n  -  k ) ) `
 x ) ) ) ) ) )
7877imbi2d 316 . . . . 5  |-  ( m  =  n  ->  (
( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  m
)  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... m
) ( ( m  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
m  -  k ) ) `  x ) ) ) ) )  <-> 
( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  n
)  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... n
) ( ( n  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
n  -  k ) ) `  x ) ) ) ) ) ) )
79 dvnmul.s . . . . . . . . 9  |-  ( ph  ->  S  e.  { RR ,  CC } )
80 recnprss 22602 . . . . . . . . 9  |-  ( S  e.  { RR ,  CC }  ->  S  C_  CC )
8179, 80syl 17 . . . . . . . 8  |-  ( ph  ->  S  C_  CC )
82 dvnmul.a . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  X )  ->  A  e.  CC )
83 dvnmul.cc . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  X )  ->  B  e.  CC )
8482, 83mulcld 9648 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  X )  ->  ( A  x.  B )  e.  CC )
85 restsspw 15048 . . . . . . . . . . 11  |-  ( (
TopOpen ` fld )t  S )  C_  ~P S
86 dvnmul.x . . . . . . . . . . 11  |-  ( ph  ->  X  e.  ( (
TopOpen ` fld )t  S ) )
8785, 86sseldi 3442 . . . . . . . . . 10  |-  ( ph  ->  X  e.  ~P S
)
88 elpwi 3966 . . . . . . . . . 10  |-  ( X  e.  ~P S  ->  X  C_  S )
8987, 88syl 17 . . . . . . . . 9  |-  ( ph  ->  X  C_  S )
90 cnex 9605 . . . . . . . . . 10  |-  CC  e.  _V
9190a1i 11 . . . . . . . . 9  |-  ( ph  ->  CC  e.  _V )
9284, 89, 91, 79mptelpm 36841 . . . . . . . 8  |-  ( ph  ->  ( x  e.  X  |->  ( A  x.  B
) )  e.  ( CC  ^pm  S )
)
93 dvn0 22621 . . . . . . . 8  |-  ( ( S  C_  CC  /\  (
x  e.  X  |->  ( A  x.  B ) )  e.  ( CC 
^pm  S ) )  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  0 )  =  ( x  e.  X  |->  ( A  x.  B ) ) )
9481, 92, 93syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `
 0 )  =  ( x  e.  X  |->  ( A  x.  B
) ) )
95 0z 10918 . . . . . . . . . . . 12  |-  0  e.  ZZ
96 fzsn 11782 . . . . . . . . . . . 12  |-  ( 0  e.  ZZ  ->  (
0 ... 0 )  =  { 0 } )
9795, 96ax-mp 5 . . . . . . . . . . 11  |-  ( 0 ... 0 )  =  { 0 }
9897sumeq1i 13671 . . . . . . . . . 10  |-  sum_ k  e.  ( 0 ... 0
) ( ( 0  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
0  -  k ) ) `  x ) ) )  =  sum_ k  e.  { 0 }  ( ( 0  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
0  -  k ) ) `  x ) ) )
9998a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  X )  ->  sum_ k  e.  ( 0 ... 0
) ( ( 0  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
0  -  k ) ) `  x ) ) )  =  sum_ k  e.  { 0 }  ( ( 0  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
0  -  k ) ) `  x ) ) ) )
100 nfcvd 2567 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  X )  ->  F/_ k
( A  x.  B
) )
101 nfv 1730 . . . . . . . . . 10  |-  F/ k ( ph  /\  x  e.  X )
102 oveq2 6288 . . . . . . . . . . . . . 14  |-  ( k  =  0  ->  (
0  _C  k )  =  ( 0  _C  0 ) )
103 0nn0 10853 . . . . . . . . . . . . . . . 16  |-  0  e.  NN0
104 bcn0 12434 . . . . . . . . . . . . . . . 16  |-  ( 0  e.  NN0  ->  ( 0  _C  0 )  =  1 )
105103, 104ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( 0  _C  0 )  =  1
106105a1i 11 . . . . . . . . . . . . . 14  |-  ( k  =  0  ->  (
0  _C  0 )  =  1 )
107102, 106eqtrd 2445 . . . . . . . . . . . . 13  |-  ( k  =  0  ->  (
0  _C  k )  =  1 )
108107adantl 466 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  X )  /\  k  =  0 )  -> 
( 0  _C  k
)  =  1 )
109 fveq2 5851 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  0  ->  ( C `  k )  =  ( C ` 
0 ) )
110109adantl 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  = 
0 )  ->  ( C `  k )  =  ( C ` 
0 ) )
111 dvnmul.c . . . . . . . . . . . . . . . . . . . . . 22  |-  C  =  ( k  e.  ( 0 ... N ) 
|->  ( ( S  Dn F ) `  k ) )
112 fveq2 5851 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  n  ->  (
( S  Dn
F ) `  k
)  =  ( ( S  Dn F ) `  n ) )
113112cbvmptv 4489 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  e.  ( 0 ... N )  |->  ( ( S  Dn F ) `  k ) )  =  ( n  e.  ( 0 ... N )  |->  ( ( S  Dn F ) `  n ) )
114111, 113eqtri 2433 . . . . . . . . . . . . . . . . . . . . 21  |-  C  =  ( n  e.  ( 0 ... N ) 
|->  ( ( S  Dn F ) `  n ) )
115114a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  C  =  ( n  e.  ( 0 ... N )  |->  ( ( S  Dn F ) `  n ) ) )
116 fveq2 5851 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  0  ->  (
( S  Dn
F ) `  n
)  =  ( ( S  Dn F ) `  0 ) )
117116adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  n  = 
0 )  ->  (
( S  Dn
F ) `  n
)  =  ( ( S  Dn F ) `  0 ) )
118 eluzfz1 11749 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... N
) )
1194, 118syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  0  e.  ( 0 ... N ) )
120 fvex 5861 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( S  Dn F ) `  0 )  e.  _V
121120a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( S  Dn F ) ` 
0 )  e.  _V )
122115, 117, 119, 121fvmptd 5940 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( C `  0
)  =  ( ( S  Dn F ) `  0 ) )
123122adantr 465 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  = 
0 )  ->  ( C `  0 )  =  ( ( S  Dn F ) `
 0 ) )
124110, 123eqtrd 2445 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  = 
0 )  ->  ( C `  k )  =  ( ( S  Dn F ) `
 0 ) )
125 dvnmulf . . . . . . . . . . . . . . . . . . . 20  |-  F  =  ( x  e.  X  |->  A )
12682, 89, 91, 79mptelpm 36841 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( x  e.  X  |->  A )  e.  ( CC  ^pm  S )
)
127125, 126syl5eqel 2496 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  F  e.  ( CC 
^pm  S ) )
128 dvn0 22621 . . . . . . . . . . . . . . . . . . 19  |-  ( ( S  C_  CC  /\  F  e.  ( CC  ^pm  S
) )  ->  (
( S  Dn
F ) `  0
)  =  F )
12981, 127, 128syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( S  Dn F ) ` 
0 )  =  F )
130129adantr 465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  = 
0 )  ->  (
( S  Dn
F ) `  0
)  =  F )
131124, 130eqtrd 2445 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  = 
0 )  ->  ( C `  k )  =  F )
132131fveq1d 5853 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  = 
0 )  ->  (
( C `  k
) `  x )  =  ( F `  x ) )
133132adantlr 715 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  X )  /\  k  =  0 )  -> 
( ( C `  k ) `  x
)  =  ( F `
 x ) )
134 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  x  e.  X )  ->  x  e.  X )
135125fvmpt2 5943 . . . . . . . . . . . . . . . 16  |-  ( ( x  e.  X  /\  A  e.  CC )  ->  ( F `  x
)  =  A )
136134, 82, 135syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  X )  ->  ( F `  x )  =  A )
137136adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  X )  /\  k  =  0 )  -> 
( F `  x
)  =  A )
138133, 137eqtrd 2445 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  X )  /\  k  =  0 )  -> 
( ( C `  k ) `  x
)  =  A )
139 oveq2 6288 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  0  ->  (
0  -  k )  =  ( 0  -  0 ) )
140 0m0e0 10688 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  -  0 )  =  0
141140a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  0  ->  (
0  -  0 )  =  0 )
142139, 141eqtrd 2445 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  0  ->  (
0  -  k )  =  0 )
143142fveq2d 5855 . . . . . . . . . . . . . . . . 17  |-  ( k  =  0  ->  ( D `  ( 0  -  k ) )  =  ( D ` 
0 ) )
144143fveq1d 5853 . . . . . . . . . . . . . . . 16  |-  ( k  =  0  ->  (
( D `  (
0  -  k ) ) `  x )  =  ( ( D `
 0 ) `  x ) )
145144adantl 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  k  = 
0 )  ->  (
( D `  (
0  -  k ) ) `  x )  =  ( ( D `
 0 ) `  x ) )
146145adantlr 715 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  X )  /\  k  =  0 )  -> 
( ( D `  ( 0  -  k
) ) `  x
)  =  ( ( D `  0 ) `
 x ) )
147 dvnmul.d . . . . . . . . . . . . . . . . . . . 20  |-  D  =  ( k  e.  ( 0 ... N ) 
|->  ( ( S  Dn G ) `  k ) )
148 fveq2 5851 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  n  ->  (
( S  Dn
G ) `  k
)  =  ( ( S  Dn G ) `  n ) )
149148cbvmptv 4489 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  ( 0 ... N )  |->  ( ( S  Dn G ) `  k ) )  =  ( n  e.  ( 0 ... N )  |->  ( ( S  Dn G ) `  n ) )
150147, 149eqtri 2433 . . . . . . . . . . . . . . . . . . 19  |-  D  =  ( n  e.  ( 0 ... N ) 
|->  ( ( S  Dn G ) `  n ) )
151150fveq1i 5852 . . . . . . . . . . . . . . . . . 18  |-  ( D `
 0 )  =  ( ( n  e.  ( 0 ... N
)  |->  ( ( S  Dn G ) `
 n ) ) `
 0 )
152151a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D `  0
)  =  ( ( n  e.  ( 0 ... N )  |->  ( ( S  Dn
G ) `  n
) ) `  0
) )
153 eqidd 2405 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( n  e.  ( 0 ... N ) 
|->  ( ( S  Dn G ) `  n ) )  =  ( n  e.  ( 0 ... N ) 
|->  ( ( S  Dn G ) `  n ) ) )
154 fveq2 5851 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  0  ->  (
( S  Dn
G ) `  n
)  =  ( ( S  Dn G ) `  0 ) )
155154adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  = 
0 )  ->  (
( S  Dn
G ) `  n
)  =  ( ( S  Dn G ) `  0 ) )
156 dvnmul.f . . . . . . . . . . . . . . . . . . . . . 22  |-  G  =  ( x  e.  X  |->  B )
15783, 89, 91, 79mptelpm 36841 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( x  e.  X  |->  B )  e.  ( CC  ^pm  S )
)
158156, 157syl5eqel 2496 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  G  e.  ( CC 
^pm  S ) )
159 dvn0 22621 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( S  C_  CC  /\  G  e.  ( CC  ^pm  S
) )  ->  (
( S  Dn
G ) `  0
)  =  G )
16081, 158, 159syl2anc 661 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( S  Dn G ) ` 
0 )  =  G )
161160adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  = 
0 )  ->  (
( S  Dn
G ) `  0
)  =  G )
162155, 161eqtrd 2445 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  = 
0 )  ->  (
( S  Dn
G ) `  n
)  =  G )
163156a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  G  =  ( x  e.  X  |->  B ) )
164 mptexg 6125 . . . . . . . . . . . . . . . . . . . 20  |-  ( X  e.  ~P S  -> 
( x  e.  X  |->  B )  e.  _V )
16587, 164syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( x  e.  X  |->  B )  e.  _V )
166163, 165eqeltrd 2492 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  G  e.  _V )
167153, 162, 119, 166fvmptd 5940 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( n  e.  ( 0 ... N
)  |->  ( ( S  Dn G ) `
 n ) ) `
 0 )  =  G )
168152, 167eqtrd 2445 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D `  0
)  =  G )
169168fveq1d 5853 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( D ` 
0 ) `  x
)  =  ( G `
 x ) )
170169ad2antrr 726 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  X )  /\  k  =  0 )  -> 
( ( D ` 
0 ) `  x
)  =  ( G `
 x ) )
171163, 83fvmpt2d 5945 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  x  e.  X )  ->  ( G `  x )  =  B )
172171adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  x  e.  X )  /\  k  =  0 )  -> 
( G `  x
)  =  B )
173146, 170, 1723eqtrd 2449 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  x  e.  X )  /\  k  =  0 )  -> 
( ( D `  ( 0  -  k
) ) `  x
)  =  B )
174138, 173oveq12d 6298 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  x  e.  X )  /\  k  =  0 )  -> 
( ( ( C `
 k ) `  x )  x.  (
( D `  (
0  -  k ) ) `  x ) )  =  ( A  x.  B ) )
175108, 174oveq12d 6298 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  X )  /\  k  =  0 )  -> 
( ( 0  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( 0  -  k ) ) `
 x ) ) )  =  ( 1  x.  ( A  x.  B ) ) )
17684mulid2d 9646 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  X )  ->  (
1  x.  ( A  x.  B ) )  =  ( A  x.  B ) )
177176adantr 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  x  e.  X )  /\  k  =  0 )  -> 
( 1  x.  ( A  x.  B )
)  =  ( A  x.  B ) )
178175, 177eqtrd 2445 . . . . . . . . . 10  |-  ( ( ( ph  /\  x  e.  X )  /\  k  =  0 )  -> 
( ( 0  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( 0  -  k ) ) `
 x ) ) )  =  ( A  x.  B ) )
179 0re 9628 . . . . . . . . . . 11  |-  0  e.  RR
180179a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  X )  ->  0  e.  RR )
181100, 101, 178, 180, 84sumsnd 36794 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  X )  ->  sum_ k  e.  { 0 }  (
( 0  _C  k
)  x.  ( ( ( C `  k
) `  x )  x.  ( ( D `  ( 0  -  k
) ) `  x
) ) )  =  ( A  x.  B
) )
18299, 181eqtr2d 2446 . . . . . . . 8  |-  ( (
ph  /\  x  e.  X )  ->  ( A  x.  B )  =  sum_ k  e.  ( 0 ... 0 ) ( ( 0  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( 0  -  k ) ) `
 x ) ) ) )
183182mpteq2dva 4483 . . . . . . 7  |-  ( ph  ->  ( x  e.  X  |->  ( A  x.  B
) )  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... 0 ) ( ( 0  _C  k
)  x.  ( ( ( C `  k
) `  x )  x.  ( ( D `  ( 0  -  k
) ) `  x
) ) ) ) )
18494, 183eqtrd 2445 . . . . . 6  |-  ( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `
 0 )  =  ( x  e.  X  |-> 
sum_ k  e.  ( 0 ... 0 ) ( ( 0  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( 0  -  k ) ) `
 x ) ) ) ) )
185184a1i 11 . . . . 5  |-  ( N  e.  ( ZZ>= `  0
)  ->  ( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `
 0 )  =  ( x  e.  X  |-> 
sum_ k  e.  ( 0 ... 0 ) ( ( 0  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( 0  -  k ) ) `
 x ) ) ) ) ) )
186 simp3 1001 . . . . . . 7  |-  ( ( i  e.  ( 0..^ N )  /\  ( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  i )  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... i ) ( ( i  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( i  -  k ) ) `
 x ) ) ) ) )  /\  ph )  ->  ph )
187 simp1 999 . . . . . . 7  |-  ( ( i  e.  ( 0..^ N )  /\  ( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  i )  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... i ) ( ( i  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( i  -  k ) ) `
 x ) ) ) ) )  /\  ph )  ->  i  e.  ( 0..^ N ) )
188 simp2 1000 . . . . . . . 8  |-  ( ( i  e.  ( 0..^ N )  /\  ( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  i )  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... i ) ( ( i  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( i  -  k ) ) `
 x ) ) ) ) )  /\  ph )  ->  ( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `
 i )  =  ( x  e.  X  |-> 
sum_ k  e.  ( 0 ... i ) ( ( i  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( i  -  k ) ) `
 x ) ) ) ) ) )
189 pm3.35 587 . . . . . . . 8  |-  ( (
ph  /\  ( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `
 i )  =  ( x  e.  X  |-> 
sum_ k  e.  ( 0 ... i ) ( ( i  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( i  -  k ) ) `
 x ) ) ) ) ) )  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  i )  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... i ) ( ( i  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( i  -  k ) ) `
 x ) ) ) ) )
190186, 188, 189syl2anc 661 . . . . . . 7  |-  ( ( i  e.  ( 0..^ N )  /\  ( ph  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  i )  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... i ) ( ( i  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( i  -  k ) ) `
 x ) ) ) ) )  /\  ph )  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  i )  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... i ) ( ( i  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( i  -  k ) ) `
 x ) ) ) ) )
19181adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  S  C_  CC )
19292adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( x  e.  X  |->  ( A  x.  B ) )  e.  ( CC  ^pm  S
) )
193 elfzonn0 11901 . . . . . . . . . . 11  |-  ( i  e.  ( 0..^ N )  ->  i  e.  NN0 )
194193adantl 466 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  i  e.  NN0 )
195 dvnp1 22622 . . . . . . . . . 10  |-  ( ( S  C_  CC  /\  (
x  e.  X  |->  ( A  x.  B ) )  e.  ( CC 
^pm  S )  /\  i  e.  NN0 )  -> 
( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `
 ( i  +  1 ) )  =  ( S  _D  (
( S  Dn
( x  e.  X  |->  ( A  x.  B
) ) ) `  i ) ) )
196191, 192, 194, 195syl3anc 1232 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  ( i  +  1 ) )  =  ( S  _D  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `
 i ) ) )
197196adantr 465 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  i
)  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... i
) ( ( i  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
i  -  k ) ) `  x ) ) ) ) )  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  ( i  +  1 ) )  =  ( S  _D  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `
 i ) ) )
198 simpr 461 . . . . . . . . 9  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  i
)  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... i
) ( ( i  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
i  -  k ) ) `  x ) ) ) ) )  ->  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  i )  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... i ) ( ( i  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( i  -  k ) ) `
 x ) ) ) ) )
199198oveq2d 6296 . . . . . . . 8  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `  i
)  =  ( x  e.  X  |->  sum_ k  e.  ( 0 ... i
) ( ( i  _C  k )  x.  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
i  -  k ) ) `  x ) ) ) ) )  ->  ( S  _D  ( ( S  Dn ( x  e.  X  |->  ( A  x.  B ) ) ) `
 i ) )  =  ( S  _D  ( x  e.  X  |-> 
sum_ k  e.  ( 0 ... i ) ( ( i  _C  k )  x.  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( i  -  k ) ) `
 x ) ) ) ) ) )
200 eqid 2404 . . . . . . . . . . 11  |-  ( (
TopOpen ` fld )t  S )  =  ( ( TopOpen ` fld )t  S )
201 eqid 2404 . . . . . . . . . . 11  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
20279adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  S  e.  { RR ,  CC } )
20386adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  X  e.  ( ( TopOpen ` fld )t  S ) )
204 fzfid 12126 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0..^ N ) )  ->  ( 0 ... i )  e.  Fin )
205193adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  i  e.  NN0 )
206 elfzelz 11744 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ( 0 ... i )  ->  k  e.  ZZ )
207206adantl 466 . . . . . . . . . . . . . . . 16  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  k  e.  ZZ )
208205, 207bccld 36902 . . . . . . . . . . . . . . 15  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
i  _C  k )  e.  NN0 )
209208nn0cnd 10897 . . . . . . . . . . . . . 14  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
i  _C  k )  e.  CC )
210209adantll 714 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
) )  ->  (
i  _C  k )  e.  CC )
2112103adant3 1019 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
)  /\  x  e.  X )  ->  (
i  _C  k )  e.  CC )
212 simpll 754 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
) )  ->  ph )
213 0zd 10919 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  0  e.  ZZ )
214 elfzoel2 11860 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( 0..^ N )  ->  N  e.  ZZ )
215214adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  N  e.  ZZ )
216213, 215, 2073jca 1179 . . . . . . . . . . . . . . . . . . 19  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
0  e.  ZZ  /\  N  e.  ZZ  /\  k  e.  ZZ ) )
217 elfzle1 11745 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  ( 0 ... i )  ->  0  <_  k )
218217adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  0  <_  k )
219207zred 11010 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  k  e.  RR )
220214zred 11010 . . . . . . . . . . . . . . . . . . . . 21  |-  ( i  e.  ( 0..^ N )  ->  N  e.  RR )
221220adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  N  e.  RR )
222193nn0red 10896 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  e.  ( 0..^ N )  ->  i  e.  RR )
223222adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  i  e.  RR )
224 elfzle2 11746 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  e.  ( 0 ... i )  ->  k  <_  i )
225224adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  k  <_  i )
226 elfzolt2 11870 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  e.  ( 0..^ N )  ->  i  <  N )
227226adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  i  <  N )
228219, 223, 221, 225, 227lelttrd 9776 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  k  <  N )
229219, 221, 228ltled 9767 . . . . . . . . . . . . . . . . . . 19  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  k  <_  N )
230216, 218, 229jca32 535 . . . . . . . . . . . . . . . . . 18  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
( 0  e.  ZZ  /\  N  e.  ZZ  /\  k  e.  ZZ )  /\  ( 0  <_  k  /\  k  <_  N ) ) )
231 elfz2 11735 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( 0 ... N )  <->  ( (
0  e.  ZZ  /\  N  e.  ZZ  /\  k  e.  ZZ )  /\  (
0  <_  k  /\  k  <_  N ) ) )
232230, 231sylibr 214 . . . . . . . . . . . . . . . . 17  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  k  e.  ( 0 ... N
) )
233232adantll 714 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
) )  ->  k  e.  ( 0 ... N
) )
234 dvnmul.dvnf . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
( S  Dn
F ) `  k
) : X --> CC )
235111a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  C  =  ( k  e.  ( 0 ... N )  |->  ( ( S  Dn F ) `  k ) ) )
236 fvex 5861 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( S  Dn F ) `  k )  e.  _V
237236a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
( S  Dn
F ) `  k
)  e.  _V )
238235, 237fvmpt2d 5945 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  ( C `  k )  =  ( ( S  Dn F ) `
 k ) )
239238feq1d 5702 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
( C `  k
) : X --> CC  <->  ( ( S  Dn F ) `
 k ) : X --> CC ) )
240234, 239mpbird 234 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  ( C `  k ) : X --> CC )
241212, 233, 240syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
) )  ->  ( C `  k ) : X --> CC )
2422413adant3 1019 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
)  /\  x  e.  X )  ->  ( C `  k ) : X --> CC )
243 simp3 1001 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
)  /\  x  e.  X )  ->  x  e.  X )
244242, 243ffvelrnd 6012 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
)  /\  x  e.  X )  ->  (
( C `  k
) `  x )  e.  CC )
245193nn0zd 11008 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  e.  ( 0..^ N )  ->  i  e.  ZZ )
246245adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  i  e.  ZZ )
247246, 207zsubcld 11015 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
i  -  k )  e.  ZZ )
248213, 215, 2473jca 1179 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
0  e.  ZZ  /\  N  e.  ZZ  /\  (
i  -  k )  e.  ZZ ) )
249 elfzel2 11742 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  e.  ( 0 ... i )  ->  i  e.  ZZ )
250249zred 11010 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  ( 0 ... i )  ->  i  e.  RR )
251206zred 11010 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  ( 0 ... i )  ->  k  e.  RR )
252250, 251subge0d 10184 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  e.  ( 0 ... i )  ->  (
0  <_  ( i  -  k )  <->  k  <_  i ) )
253224, 252mpbird 234 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  ( 0 ... i )  ->  0  <_  ( i  -  k
) )
254253adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  0  <_  ( i  -  k
) )
255223, 219resubcld 10030 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
i  -  k )  e.  RR )
256221, 219resubcld 10030 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  ( N  -  k )  e.  RR )
257179a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  0  e.  RR )
258221, 257jca 532 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  ( N  e.  RR  /\  0  e.  RR ) )
259 resubcl 9921 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  e.  RR  /\  0  e.  RR )  ->  ( N  -  0 )  e.  RR )
260258, 259syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  ( N  -  0 )  e.  RR )
261223, 221, 219, 227ltsub1dd 10206 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
i  -  k )  <  ( N  -  k ) )
262257, 219, 221, 218lesub2dd 10211 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  ( N  -  k )  <_  ( N  -  0 ) )
263255, 256, 260, 261, 262ltletrd 9778 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
i  -  k )  <  ( N  - 
0 ) )
264220recnd 9654 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  e.  ( 0..^ N )  ->  N  e.  CC )
265264subid1d 9958 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  e.  ( 0..^ N )  ->  ( N  -  0 )  =  N )
266265adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  ( N  -  0 )  =  N )
267263, 266breqtrd 4421 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
i  -  k )  <  N )
268255, 221, 267ltled 9767 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
i  -  k )  <_  N )
269248, 254, 268jca32 535 . . . . . . . . . . . . . . . . . . 19  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
( 0  e.  ZZ  /\  N  e.  ZZ  /\  ( i  -  k
)  e.  ZZ )  /\  ( 0  <_ 
( i  -  k
)  /\  ( i  -  k )  <_  N ) ) )
270 elfz2 11735 . . . . . . . . . . . . . . . . . . 19  |-  ( ( i  -  k )  e.  ( 0 ... N )  <->  ( (
0  e.  ZZ  /\  N  e.  ZZ  /\  (
i  -  k )  e.  ZZ )  /\  ( 0  <_  (
i  -  k )  /\  ( i  -  k )  <_  N
) ) )
271269, 270sylibr 214 . . . . . . . . . . . . . . . . . 18  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
i  -  k )  e.  ( 0 ... N ) )
272271adantll 714 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
) )  ->  (
i  -  k )  e.  ( 0 ... N ) )
273 ovex 6308 . . . . . . . . . . . . . . . . . 18  |-  ( i  -  k )  e. 
_V
274 eleq1 2476 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  ( i  -  k )  ->  (
j  e.  ( 0 ... N )  <->  ( i  -  k )  e.  ( 0 ... N
) ) )
275274anbi2d 704 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  ( i  -  k )  ->  (
( ph  /\  j  e.  ( 0 ... N
) )  <->  ( ph  /\  ( i  -  k
)  e.  ( 0 ... N ) ) ) )
276 fveq2 5851 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  ( i  -  k )  ->  (
( S  Dn
G ) `  j
)  =  ( ( S  Dn G ) `  ( i  -  k ) ) )
277276feq1d 5702 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  ( i  -  k )  ->  (
( ( S  Dn G ) `  j ) : X --> CC 
<->  ( ( S  Dn G ) `  ( i  -  k
) ) : X --> CC ) )
278275, 277imbi12d 320 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  ( i  -  k )  ->  (
( ( ph  /\  j  e.  ( 0 ... N ) )  ->  ( ( S  Dn G ) `
 j ) : X --> CC )  <->  ( ( ph  /\  ( i  -  k )  e.  ( 0 ... N ) )  ->  ( ( S  Dn G ) `
 ( i  -  k ) ) : X --> CC ) ) )
279 nfv 1730 . . . . . . . . . . . . . . . . . . 19  |-  F/ k ( ( ph  /\  j  e.  ( 0 ... N ) )  ->  ( ( S  Dn G ) `
 j ) : X --> CC )
280 eleq1 2476 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  j  ->  (
k  e.  ( 0 ... N )  <->  j  e.  ( 0 ... N
) ) )
281280anbi2d 704 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  j  ->  (
( ph  /\  k  e.  ( 0 ... N
) )  <->  ( ph  /\  j  e.  ( 0 ... N ) ) ) )
282 fveq2 5851 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  j  ->  (
( S  Dn
G ) `  k
)  =  ( ( S  Dn G ) `  j ) )
283282feq1d 5702 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  j  ->  (
( ( S  Dn G ) `  k ) : X --> CC 
<->  ( ( S  Dn G ) `  j ) : X --> CC ) )
284281, 283imbi12d 320 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  j  ->  (
( ( ph  /\  k  e.  ( 0 ... N ) )  ->  ( ( S  Dn G ) `
 k ) : X --> CC )  <->  ( ( ph  /\  j  e.  ( 0 ... N ) )  ->  ( ( S  Dn G ) `
 j ) : X --> CC ) ) )
285 dvnmul.dvng . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  ( 0 ... N
) )  ->  (
( S  Dn
G ) `  k
) : X --> CC )
286279, 284, 285chvar 2042 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( S  Dn
G ) `  j
) : X --> CC )
287273, 278, 286vtocl 3113 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( i  -  k )  e.  ( 0 ... N
) )  ->  (
( S  Dn
G ) `  (
i  -  k ) ) : X --> CC )
288212, 272, 287syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
) )  ->  (
( S  Dn
G ) `  (
i  -  k ) ) : X --> CC )
289150a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  D  =  ( n  e.  ( 0 ... N
)  |->  ( ( S  Dn G ) `
 n ) ) )
290 fveq2 5851 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  ( i  -  k )  ->  (
( S  Dn
G ) `  n
)  =  ( ( S  Dn G ) `  ( i  -  k ) ) )
291290adantl 466 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i ) )  /\  n  =  ( i  -  k ) )  ->  ( ( S  Dn G ) `
 n )  =  ( ( S  Dn G ) `  ( i  -  k
) ) )
292 fvex 5861 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( S  Dn G ) `  ( i  -  k ) )  e.  _V
293292a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
( S  Dn
G ) `  (
i  -  k ) )  e.  _V )
294289, 291, 271, 293fvmptd 5940 . . . . . . . . . . . . . . . . . 18  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  ( D `  ( i  -  k ) )  =  ( ( S  Dn G ) `
 ( i  -  k ) ) )
295294adantll 714 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
) )  ->  ( D `  ( i  -  k ) )  =  ( ( S  Dn G ) `
 ( i  -  k ) ) )
296295feq1d 5702 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
) )  ->  (
( D `  (
i  -  k ) ) : X --> CC  <->  ( ( S  Dn G ) `
 ( i  -  k ) ) : X --> CC ) )
297288, 296mpbird 234 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
) )  ->  ( D `  ( i  -  k ) ) : X --> CC )
2982973adant3 1019 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
)  /\  x  e.  X )  ->  ( D `  ( i  -  k ) ) : X --> CC )
299298, 243ffvelrnd 6012 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
)  /\  x  e.  X )  ->  (
( D `  (
i  -  k ) ) `  x )  e.  CC )
300244, 299mulcld 9648 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
)  /\  x  e.  X )  ->  (
( ( C `  k ) `  x
)  x.  ( ( D `  ( i  -  k ) ) `
 x ) )  e.  CC )
301211, 300mulcld 9648 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
)  /\  x  e.  X )  ->  (
( i  _C  k
)  x.  ( ( ( C `  k
) `  x )  x.  ( ( D `  ( i  -  k
) ) `  x
) ) )  e.  CC )
3022113expa 1199 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i ) )  /\  x  e.  X
)  ->  ( i  _C  k )  e.  CC )
303246peano2zd 11013 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
i  +  1 )  e.  ZZ )
304303, 207zsubcld 11015 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
( i  +  1 )  -  k )  e.  ZZ )
305213, 215, 3043jca 1179 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
0  e.  ZZ  /\  N  e.  ZZ  /\  (
( i  +  1 )  -  k )  e.  ZZ ) )
306 peano2re 9789 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  e.  RR  ->  (
i  +  1 )  e.  RR )
307250, 306syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  e.  ( 0 ... i )  ->  (
i  +  1 )  e.  RR )
308 peano2re 9789 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  e.  RR  ->  (
k  +  1 )  e.  RR )
309251, 308syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  e.  ( 0 ... i )  ->  (
k  +  1 )  e.  RR )
310251ltp1d 10518 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  e.  ( 0 ... i )  ->  k  <  ( k  +  1 ) )
311 1red 9643 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( k  e.  ( 0 ... i )  ->  1  e.  RR )
312251, 250, 311, 224leadd1dd 10208 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  e.  ( 0 ... i )  ->  (
k  +  1 )  <_  ( i  +  1 ) )
313251, 309, 307, 310, 312ltletrd 9778 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  e.  ( 0 ... i )  ->  k  <  ( i  +  1 ) )
314251, 307, 313ltled 9767 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  e.  ( 0 ... i )  ->  k  <_  ( i  +  1 ) )
315314adantl 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  k  <_  ( i  +  1 ) )
316223, 306syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
i  +  1 )  e.  RR )
317316, 219subge0d 10184 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
0  <_  ( (
i  +  1 )  -  k )  <->  k  <_  ( i  +  1 ) ) )
318315, 317mpbird 234 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  0  <_  ( ( i  +  1 )  -  k
) )
319316, 219resubcld 10030 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
( i  +  1 )  -  k )  e.  RR )
320 elfzop1le2 36863 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  e.  ( 0..^ N )  ->  ( i  +  1 )  <_  N )
321320adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
i  +  1 )  <_  N )
322316, 221, 219, 321lesub1dd 10210 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
( i  +  1 )  -  k )  <_  ( N  -  k ) )
323262, 266breqtrd 4421 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  ( N  -  k )  <_  N )
324319, 256, 221, 322, 323letrd 9775 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
( i  +  1 )  -  k )  <_  N )
325305, 318, 324jca32 535 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
( 0  e.  ZZ  /\  N  e.  ZZ  /\  ( ( i  +  1 )  -  k
)  e.  ZZ )  /\  ( 0  <_ 
( ( i  +  1 )  -  k
)  /\  ( (
i  +  1 )  -  k )  <_  N ) ) )
326 elfz2 11735 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( i  +  1 )  -  k )  e.  ( 0 ... N )  <->  ( (
0  e.  ZZ  /\  N  e.  ZZ  /\  (
( i  +  1 )  -  k )  e.  ZZ )  /\  ( 0  <_  (
( i  +  1 )  -  k )  /\  ( ( i  +  1 )  -  k )  <_  N
) ) )
327325, 326sylibr 214 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
( i  +  1 )  -  k )  e.  ( 0 ... N ) )
328327adantll 714 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
) )  ->  (
( i  +  1 )  -  k )  e.  ( 0 ... N ) )
329 ovex 6308 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  +  1 )  -  k )  e. 
_V
330 eleq1 2476 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  ( ( i  +  1 )  -  k )  ->  (
j  e.  ( 0 ... N )  <->  ( (
i  +  1 )  -  k )  e.  ( 0 ... N
) ) )
331330anbi2d 704 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  ( ( i  +  1 )  -  k )  ->  (
( ph  /\  j  e.  ( 0 ... N
) )  <->  ( ph  /\  ( ( i  +  1 )  -  k
)  e.  ( 0 ... N ) ) ) )
332 fveq2 5851 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  ( ( i  +  1 )  -  k )  ->  (
( S  Dn
G ) `  j
)  =  ( ( S  Dn G ) `  ( ( i  +  1 )  -  k ) ) )
333332feq1d 5702 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  ( ( i  +  1 )  -  k )  ->  (
( ( S  Dn G ) `  j ) : X --> CC 
<->  ( ( S  Dn G ) `  ( ( i  +  1 )  -  k
) ) : X --> CC ) )
334331, 333imbi12d 320 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  ( ( i  +  1 )  -  k )  ->  (
( ( ph  /\  j  e.  ( 0 ... N ) )  ->  ( ( S  Dn G ) `
 j ) : X --> CC )  <->  ( ( ph  /\  ( ( i  +  1 )  -  k )  e.  ( 0 ... N ) )  ->  ( ( S  Dn G ) `
 ( ( i  +  1 )  -  k ) ) : X --> CC ) ) )
335329, 334, 286vtocl 3113 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( (
i  +  1 )  -  k )  e.  ( 0 ... N
) )  ->  (
( S  Dn
G ) `  (
( i  +  1 )  -  k ) ) : X --> CC )
336212, 328, 335syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
) )  ->  (
( S  Dn
G ) `  (
( i  +  1 )  -  k ) ) : X --> CC )
337150a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
) )  ->  D  =  ( n  e.  ( 0 ... N
)  |->  ( ( S  Dn G ) `
 n ) ) )
338 simpr 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i ) )  /\  n  =  ( ( i  +  1 )  -  k ) )  ->  n  =  ( ( i  +  1 )  -  k
) )
339338fveq2d 5855 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i ) )  /\  n  =  ( ( i  +  1 )  -  k ) )  ->  ( ( S  Dn G ) `
 n )  =  ( ( S  Dn G ) `  ( ( i  +  1 )  -  k
) ) )
340 fvex 5861 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( S  Dn G ) `  ( ( i  +  1 )  -  k ) )  e.  _V
341340a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
) )  ->  (
( S  Dn
G ) `  (
( i  +  1 )  -  k ) )  e.  _V )
342337, 339, 328, 341fvmptd 5940 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
) )  ->  ( D `  ( (
i  +  1 )  -  k ) )  =  ( ( S  Dn G ) `
 ( ( i  +  1 )  -  k ) ) )
343342feq1d 5702 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
) )  ->  (
( D `  (
( i  +  1 )  -  k ) ) : X --> CC  <->  ( ( S  Dn G ) `
 ( ( i  +  1 )  -  k ) ) : X --> CC ) )
344336, 343mpbird 234 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
) )  ->  ( D `  ( (
i  +  1 )  -  k ) ) : X --> CC )
345344ffvelrnda 6011 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i ) )  /\  x  e.  X
)  ->  ( ( D `  ( (
i  +  1 )  -  k ) ) `
 x )  e.  CC )
3462443expa 1199 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i ) )  /\  x  e.  X
)  ->  ( ( C `  k ) `  x )  e.  CC )
347345, 346mulcomd 9649 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i ) )  /\  x  e.  X
)  ->  ( (
( D `  (
( i  +  1 )  -  k ) ) `  x )  x.  ( ( C `
 k ) `  x ) )  =  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
( i  +  1 )  -  k ) ) `  x ) ) )
348347oveq2d 6296 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i ) )  /\  x  e.  X
)  ->  ( (
( ( C `  ( k  +  1 ) ) `  x
)  x.  ( ( D `  ( i  -  k ) ) `
 x ) )  +  ( ( ( D `  ( ( i  +  1 )  -  k ) ) `
 x )  x.  ( ( C `  k ) `  x
) ) )  =  ( ( ( ( C `  ( k  +  1 ) ) `
 x )  x.  ( ( D `  ( i  -  k
) ) `  x
) )  +  ( ( ( C `  k ) `  x
)  x.  ( ( D `  ( ( i  +  1 )  -  k ) ) `
 x ) ) ) )
349207peano2zd 11013 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
k  +  1 )  e.  ZZ )
350213, 215, 3493jca 1179 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
0  e.  ZZ  /\  N  e.  ZZ  /\  (
k  +  1 )  e.  ZZ ) )
351179a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  ( 0 ... i )  ->  0  e.  RR )
352351, 251, 309, 217, 310lelttrd 9776 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  ( 0 ... i )  ->  0  <  ( k  +  1 ) )
353351, 309, 352ltled 9767 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  e.  ( 0 ... i )  ->  0  <_  ( k  +  1 ) )
354353adantl 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  0  <_  ( k  +  1 ) )
355219, 308syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
k  +  1 )  e.  RR )
356312adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
k  +  1 )  <_  ( i  +  1 ) )
357355, 316, 221, 356, 321letrd 9775 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
k  +  1 )  <_  N )
358350, 354, 357jca32 535 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
( 0  e.  ZZ  /\  N  e.  ZZ  /\  ( k  +  1 )  e.  ZZ )  /\  ( 0  <_ 
( k  +  1 )  /\  ( k  +  1 )  <_  N ) ) )
359 elfz2 11735 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  +  1 )  e.  ( 0 ... N )  <->  ( (
0  e.  ZZ  /\  N  e.  ZZ  /\  (
k  +  1 )  e.  ZZ )  /\  ( 0  <_  (
k  +  1 )  /\  ( k  +  1 )  <_  N
) ) )
360358, 359sylibr 214 . . . . . . . . . . . . . . . . . . 19  |-  ( ( i  e.  ( 0..^ N )  /\  k  e.  ( 0 ... i
) )  ->  (
k  +  1 )  e.  ( 0 ... N ) )
361360adantll 714 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
) )  ->  (
k  +  1 )  e.  ( 0 ... N ) )
362 ovex 6308 . . . . . . . . . . . . . . . . . . 19  |-  ( k  +  1 )  e. 
_V
363 eleq1 2476 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  ( k  +  1 )  ->  (
j  e.  ( 0 ... N )  <->  ( k  +  1 )  e.  ( 0 ... N
) ) )
364363anbi2d 704 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  ( k  +  1 )  ->  (
( ph  /\  j  e.  ( 0 ... N
) )  <->  ( ph  /\  ( k  +  1 )  e.  ( 0 ... N ) ) ) )
365 fveq2 5851 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  ( k  +  1 )  ->  ( C `  j )  =  ( C `  ( k  +  1 ) ) )
366365feq1d 5702 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  ( k  +  1 )  ->  (
( C `  j
) : X --> CC  <->  ( C `  ( k  +  1 ) ) : X --> CC ) )
367364, 366imbi12d 320 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  ( k  +  1 )  ->  (
( ( ph  /\  j  e.  ( 0 ... N ) )  ->  ( C `  j ) : X --> CC )  <->  ( ( ph  /\  ( k  +  1 )  e.  ( 0 ... N ) )  ->  ( C `  ( k  +  1 ) ) : X --> CC ) ) )
368 nfv 1730 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ k ( ph  /\  j  e.  ( 0 ... N
) )
369 nfmpt1 4486 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ k
( k  e.  ( 0 ... N ) 
|->  ( ( S  Dn F ) `  k ) )
370111, 369nfcxfr 2564 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ k C
371 nfcv 2566 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ k
j
372370, 371nffv 5858 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ k
( C `  j
)
373 nfcv 2566 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ k X
374 nfcv 2566 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ k CC
375372, 373, 374nff 5712 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ k ( C `  j
) : X --> CC
376368, 375nfim 1950 . . . . . . . . . . . . . . . . . . . 20  |-  F/ k ( ( ph  /\  j  e.  ( 0 ... N ) )  ->  ( C `  j ) : X --> CC )
377 fveq2 5851 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  j  ->  ( C `  k )  =  ( C `  j ) )
378377feq1d 5702 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  j  ->  (
( C `  k
) : X --> CC  <->  ( C `  j ) : X --> CC ) )
379281, 378imbi12d 320 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  j  ->  (
( ( ph  /\  k  e.  ( 0 ... N ) )  ->  ( C `  k ) : X --> CC )  <->  ( ( ph  /\  j  e.  ( 0 ... N ) )  ->  ( C `  j ) : X --> CC ) ) )
380376, 379, 240chvar 2042 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( C `  j ) : X --> CC )
381362, 367, 380vtocl 3113 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( k  +  1 )  e.  ( 0 ... N
) )  ->  ( C `  ( k  +  1 ) ) : X --> CC )
382212, 361, 381syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
) )  ->  ( C `  ( k  +  1 ) ) : X --> CC )
383382ffvelrnda 6011 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i ) )  /\  x  e.  X
)  ->  ( ( C `  ( k  +  1 ) ) `
 x )  e.  CC )
3842993expa 1199 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i ) )  /\  x  e.  X
)  ->  ( ( D `  ( i  -  k ) ) `
 x )  e.  CC )
385383, 384mulcld 9648 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i ) )  /\  x  e.  X
)  ->  ( (
( C `  (
k  +  1 ) ) `  x )  x.  ( ( D `
 ( i  -  k ) ) `  x ) )  e.  CC )
386345, 346mulcld 9648 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i ) )  /\  x  e.  X
)  ->  ( (
( D `  (
( i  +  1 )  -  k ) ) `  x )  x.  ( ( C `
 k ) `  x ) )  e.  CC )
387385, 386addcld 9647 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i ) )  /\  x  e.  X
)  ->  ( (
( ( C `  ( k  +  1 ) ) `  x
)  x.  ( ( D `  ( i  -  k ) ) `
 x ) )  +  ( ( ( D `  ( ( i  +  1 )  -  k ) ) `
 x )  x.  ( ( C `  k ) `  x
) ) )  e.  CC )
388348, 387eqeltrrd 2493 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i ) )  /\  x  e.  X
)  ->  ( (
( ( C `  ( k  +  1 ) ) `  x
)  x.  ( ( D `  ( i  -  k ) ) `
 x ) )  +  ( ( ( C `  k ) `
 x )  x.  ( ( D `  ( ( i  +  1 )  -  k
) ) `  x
) ) )  e.  CC )
389302, 388mulcld 9648 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i ) )  /\  x  e.  X
)  ->  ( (
i  _C  k )  x.  ( ( ( ( C `  (
k  +  1 ) ) `  x )  x.  ( ( D `
 ( i  -  k ) ) `  x ) )  +  ( ( ( C `
 k ) `  x )  x.  (
( D `  (
( i  +  1 )  -  k ) ) `  x ) ) ) )  e.  CC )
3903893impa 1194 . . . . . . . . . . 11  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
)  /\  x  e.  X )  ->  (
( i  _C  k
)  x.  ( ( ( ( C `  ( k  +  1 ) ) `  x
)  x.  ( ( D `  ( i  -  k ) ) `
 x ) )  +  ( ( ( C `  k ) `
 x )  x.  ( ( D `  ( ( i  +  1 )  -  k
) ) `  x
) ) ) )  e.  CC )
391212, 79syl 17 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  i  e.  ( 0..^ N ) )  /\  k  e.  ( 0 ... i
) )  ->  S  e.  { RR ,  CC } )
392179a1i 11 . . . . . . . . . . . . 13