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

Theorem etransclem35 32218
Description:  P does not divide the P-1 -th derivative of  F applied to  0. This is case 2 of the proof in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
etransclem35.p  |-  ( ph  ->  P  e.  NN )
etransclem35.m  |-  ( ph  ->  M  e.  NN0 )
etransclem35.f  |-  F  =  ( x  e.  RR  |->  ( ( x ^
( P  -  1 ) )  x.  prod_ j  e.  ( 1 ... M ) ( ( x  -  j ) ^ P ) ) )
etransclem35.c  |-  C  =  ( n  e.  NN0  |->  { c  e.  ( ( 0 ... n
)  ^m  ( 0 ... M ) )  |  sum_ j  e.  ( 0 ... M ) ( c `  j
)  =  n }
)
etransclem35.d  |-  D  =  ( j  e.  ( 0 ... M ) 
|->  if ( j  =  0 ,  ( P  -  1 ) ,  0 ) )
Assertion
Ref Expression
etransclem35  |-  ( ph  ->  ( ( ( RR  Dn F ) `
 ( P  - 
1 ) ) ` 
0 )  =  ( ( ! `  ( P  -  1 ) )  x.  ( prod_
j  e.  ( 1 ... M ) -u j ^ P ) ) )
Distinct variable groups:    C, c,
j, x    D, c,
j    M, c, j, n, x    P, c, j, n, x    ph, c, j, n, x
Allowed substitution hints:    C( n)    D( x, n)    F( x, j, n, c)

Proof of Theorem etransclem35
Dummy variables  A  k  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reelprrecn 9495 . . . 4  |-  RR  e.  { RR ,  CC }
21a1i 11 . . 3  |-  ( ph  ->  RR  e.  { RR ,  CC } )
3 reopn 31643 . . . . 5  |-  RR  e.  ( topGen `  ran  (,) )
4 eqid 2382 . . . . . 6  |-  ( TopOpen ` fld )  =  ( TopOpen ` fld )
54tgioo2 21393 . . . . 5  |-  ( topGen ` 
ran  (,) )  =  ( ( TopOpen ` fld )t  RR )
63, 5eleqtri 2468 . . . 4  |-  RR  e.  ( ( TopOpen ` fld )t  RR )
76a1i 11 . . 3  |-  ( ph  ->  RR  e.  ( (
TopOpen ` fld )t  RR ) )
8 etransclem35.p . . 3  |-  ( ph  ->  P  e.  NN )
9 etransclem35.m . . 3  |-  ( ph  ->  M  e.  NN0 )
10 etransclem35.f . . 3  |-  F  =  ( x  e.  RR  |->  ( ( x ^
( P  -  1 ) )  x.  prod_ j  e.  ( 1 ... M ) ( ( x  -  j ) ^ P ) ) )
11 nnm1nn0 10754 . . . 4  |-  ( P  e.  NN  ->  ( P  -  1 )  e.  NN0 )
128, 11syl 16 . . 3  |-  ( ph  ->  ( P  -  1 )  e.  NN0 )
13 etransclem5 32188 . . 3  |-  ( k  e.  ( 0 ... M )  |->  ( y  e.  RR  |->  ( ( y  -  k ) ^ if ( k  =  0 ,  ( P  -  1 ) ,  P ) ) ) )  =  ( j  e.  ( 0 ... M )  |->  ( x  e.  RR  |->  ( ( x  -  j
) ^ if ( j  =  0 ,  ( P  -  1 ) ,  P ) ) ) )
14 etransclem35.c . . 3  |-  C  =  ( n  e.  NN0  |->  { c  e.  ( ( 0 ... n
)  ^m  ( 0 ... M ) )  |  sum_ j  e.  ( 0 ... M ) ( c `  j
)  =  n }
)
15 0red 9508 . . 3  |-  ( ph  ->  0  e.  RR )
162, 7, 8, 9, 10, 12, 13, 14, 15etransclem31 32214 . 2  |-  ( ph  ->  ( ( ( RR  Dn F ) `
 ( P  - 
1 ) ) ` 
0 )  =  sum_ c  e.  ( C `  ( P  -  1 ) ) ( ( ( ! `  ( P  -  1 ) )  /  prod_ j  e.  ( 0 ... M
) ( ! `  ( c `  j
) ) )  x.  ( if ( ( P  -  1 )  <  ( c ` 
0 ) ,  0 ,  ( ( ( ! `  ( P  -  1 ) )  /  ( ! `  ( ( P  - 
1 )  -  (
c `  0 )
) ) )  x.  ( 0 ^ (
( P  -  1 )  -  ( c `
 0 ) ) ) ) )  x. 
prod_ j  e.  (
1 ... M ) if ( P  <  (
c `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( c `  j ) ) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( c `  j
) ) ) ) ) ) ) )
17 nfv 1715 . . 3  |-  F/ c
ph
18 nfcv 2544 . . 3  |-  F/_ c
( ( ( ! `
 ( P  - 
1 ) )  /  prod_ j  e.  ( 0 ... M ) ( ! `  ( D `
 j ) ) )  x.  ( if ( ( P  - 
1 )  <  ( D `  0 ) ,  0 ,  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( D ` 
0 ) ) ) )  x.  ( 0 ^ ( ( P  -  1 )  -  ( D `  0 ) ) ) ) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )
1914, 12etransclem16 32199 . . 3  |-  ( ph  ->  ( C `  ( P  -  1 ) )  e.  Fin )
20 simpr 459 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  c  e.  ( C `  ( P  -  1 ) ) )
2114, 12etransclem12 32195 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( C `  ( P  -  1 ) )  =  { c  e.  ( ( 0 ... ( P  - 
1 ) )  ^m  ( 0 ... M
) )  |  sum_ j  e.  ( 0 ... M ) ( c `  j )  =  ( P  - 
1 ) } )
2221adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  ( C `  ( P  -  1 ) )  =  {
c  e.  ( ( 0 ... ( P  -  1 ) )  ^m  ( 0 ... M ) )  | 
sum_ j  e.  ( 0 ... M ) ( c `  j
)  =  ( P  -  1 ) } )
2320, 22eleqtrd 2472 . . . . . . . . . . . 12  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  c  e.  { c  e.  ( ( 0 ... ( P  -  1 ) )  ^m  ( 0 ... M ) )  | 
sum_ j  e.  ( 0 ... M ) ( c `  j
)  =  ( P  -  1 ) } )
24 rabid 2959 . . . . . . . . . . . 12  |-  ( c  e.  { c  e.  ( ( 0 ... ( P  -  1 ) )  ^m  (
0 ... M ) )  |  sum_ j  e.  ( 0 ... M ) ( c `  j
)  =  ( P  -  1 ) }  <-> 
( c  e.  ( ( 0 ... ( P  -  1 ) )  ^m  ( 0 ... M ) )  /\  sum_ j  e.  ( 0 ... M ) ( c `  j
)  =  ( P  -  1 ) ) )
2523, 24sylib 196 . . . . . . . . . . 11  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  ( c  e.  ( ( 0 ... ( P  -  1 ) )  ^m  (
0 ... M ) )  /\  sum_ j  e.  ( 0 ... M ) ( c `  j
)  =  ( P  -  1 ) ) )
2625simprd 461 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  sum_ j  e.  ( 0 ... M
) ( c `  j )  =  ( P  -  1 ) )
2726eqcomd 2390 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  ( P  -  1 )  = 
sum_ j  e.  ( 0 ... M ) ( c `  j
) )
2827fveq2d 5778 . . . . . . . 8  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  ( ! `  ( P  -  1 ) )  =  ( ! `  sum_ j  e.  ( 0 ... M
) ( c `  j ) ) )
2928oveq1d 6211 . . . . . . 7  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  ( ( ! `  ( P  -  1 ) )  /  prod_ j  e.  ( 0 ... M ) ( ! `  (
c `  j )
) )  =  ( ( ! `  sum_ j  e.  ( 0 ... M ) ( c `  j ) )  /  prod_ j  e.  ( 0 ... M
) ( ! `  ( c `  j
) ) ) )
30 nfcv 2544 . . . . . . . 8  |-  F/_ j
c
31 fzfid 11986 . . . . . . . 8  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  ( 0 ... M )  e. 
Fin )
32 nn0ex 10718 . . . . . . . . . 10  |-  NN0  e.  _V
33 fzssnn0 31688 . . . . . . . . . 10  |-  ( 0 ... ( P  - 
1 ) )  C_  NN0
34 mapss 7380 . . . . . . . . . 10  |-  ( ( NN0  e.  _V  /\  ( 0 ... ( P  -  1 ) )  C_  NN0 )  -> 
( ( 0 ... ( P  -  1 ) )  ^m  (
0 ... M ) ) 
C_  ( NN0  ^m  ( 0 ... M
) ) )
3532, 33, 34mp2an 670 . . . . . . . . 9  |-  ( ( 0 ... ( P  -  1 ) )  ^m  ( 0 ... M ) )  C_  ( NN0  ^m  ( 0 ... M ) )
3625simpld 457 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  c  e.  ( ( 0 ... ( P  -  1 ) )  ^m  (
0 ... M ) ) )
3735, 36sseldi 3415 . . . . . . . 8  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  c  e.  ( NN0  ^m  ( 0 ... M ) ) )
3830, 31, 37mccl 31772 . . . . . . 7  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  ( ( ! `  sum_ j  e.  ( 0 ... M
) ( c `  j ) )  /  prod_ j  e.  ( 0 ... M ) ( ! `  ( c `
 j ) ) )  e.  NN )
3929, 38eqeltrd 2470 . . . . . 6  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  ( ( ! `  ( P  -  1 ) )  /  prod_ j  e.  ( 0 ... M ) ( ! `  (
c `  j )
) )  e.  NN )
4039nnzd 10883 . . . . 5  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  ( ( ! `  ( P  -  1 ) )  /  prod_ j  e.  ( 0 ... M ) ( ! `  (
c `  j )
) )  e.  ZZ )
418adantr 463 . . . . . . 7  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  P  e.  NN )
429adantr 463 . . . . . . 7  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  M  e.  NN0 )
43 elmapi 7359 . . . . . . . 8  |-  ( c  e.  ( ( 0 ... ( P  - 
1 ) )  ^m  ( 0 ... M
) )  ->  c : ( 0 ... M ) --> ( 0 ... ( P  - 
1 ) ) )
4436, 43syl 16 . . . . . . 7  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  c :
( 0 ... M
) --> ( 0 ... ( P  -  1 ) ) )
45 0zd 10793 . . . . . . 7  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  0  e.  ZZ )
4641, 42, 44, 45etransclem10 32193 . . . . . 6  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  if (
( P  -  1 )  <  ( c `
 0 ) ,  0 ,  ( ( ( ! `  ( P  -  1 ) )  /  ( ! `
 ( ( P  -  1 )  -  ( c `  0
) ) ) )  x.  ( 0 ^ ( ( P  - 
1 )  -  (
c `  0 )
) ) ) )  e.  ZZ )
47 fzfid 11986 . . . . . . 7  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  ( 1 ... M )  e. 
Fin )
488ad2antrr 723 . . . . . . . 8  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  j  e.  ( 1 ... M
) )  ->  P  e.  NN )
4944adantr 463 . . . . . . . 8  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  j  e.  ( 1 ... M
) )  ->  c : ( 0 ... M ) --> ( 0 ... ( P  - 
1 ) ) )
50 fz1ssfz0 31676 . . . . . . . . . 10  |-  ( 1 ... M )  C_  ( 0 ... M
)
5150sseli 3413 . . . . . . . . 9  |-  ( j  e.  ( 1 ... M )  ->  j  e.  ( 0 ... M
) )
5251adantl 464 . . . . . . . 8  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  j  e.  ( 1 ... M
) )  ->  j  e.  ( 0 ... M
) )
53 0zd 10793 . . . . . . . 8  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  j  e.  ( 1 ... M
) )  ->  0  e.  ZZ )
5448, 49, 52, 53etransclem3 32186 . . . . . . 7  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  j  e.  ( 1 ... M
) )  ->  if ( P  <  ( c `
 j ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( c `  j
) ) ) )  x.  ( ( 0  -  j ) ^
( P  -  (
c `  j )
) ) ) )  e.  ZZ )
5547, 54fprodzcl 13763 . . . . . 6  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  prod_ j  e.  ( 1 ... M
) if ( P  <  ( c `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  (
c `  j )
) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( c `  j ) ) ) ) )  e.  ZZ )
5646, 55zmulcld 10890 . . . . 5  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  ( if ( ( P  - 
1 )  <  (
c `  0 ) ,  0 ,  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( c ` 
0 ) ) ) )  x.  ( 0 ^ ( ( P  -  1 )  -  ( c `  0
) ) ) ) )  x.  prod_ j  e.  ( 1 ... M
) if ( P  <  ( c `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  (
c `  j )
) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( c `  j ) ) ) ) ) )  e.  ZZ )
5740, 56zmulcld 10890 . . . 4  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  ( (
( ! `  ( P  -  1 ) )  /  prod_ j  e.  ( 0 ... M
) ( ! `  ( c `  j
) ) )  x.  ( if ( ( P  -  1 )  <  ( c ` 
0 ) ,  0 ,  ( ( ( ! `  ( P  -  1 ) )  /  ( ! `  ( ( P  - 
1 )  -  (
c `  0 )
) ) )  x.  ( 0 ^ (
( P  -  1 )  -  ( c `
 0 ) ) ) ) )  x. 
prod_ j  e.  (
1 ... M ) if ( P  <  (
c `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( c `  j ) ) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( c `  j
) ) ) ) ) ) )  e.  ZZ )
5857zcnd 10885 . . 3  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  ( (
( ! `  ( P  -  1 ) )  /  prod_ j  e.  ( 0 ... M
) ( ! `  ( c `  j
) ) )  x.  ( if ( ( P  -  1 )  <  ( c ` 
0 ) ,  0 ,  ( ( ( ! `  ( P  -  1 ) )  /  ( ! `  ( ( P  - 
1 )  -  (
c `  0 )
) ) )  x.  ( 0 ^ (
( P  -  1 )  -  ( c `
 0 ) ) ) ) )  x. 
prod_ j  e.  (
1 ... M ) if ( P  <  (
c `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( c `  j ) ) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( c `  j
) ) ) ) ) ) )  e.  CC )
59 nn0uz 11035 . . . . . . . . . . 11  |-  NN0  =  ( ZZ>= `  0 )
6012, 59syl6eleq 2480 . . . . . . . . . 10  |-  ( ph  ->  ( P  -  1 )  e.  ( ZZ>= ` 
0 ) )
61 eluzfz2 11615 . . . . . . . . . 10  |-  ( ( P  -  1 )  e.  ( ZZ>= `  0
)  ->  ( P  -  1 )  e.  ( 0 ... ( P  -  1 ) ) )
6260, 61syl 16 . . . . . . . . 9  |-  ( ph  ->  ( P  -  1 )  e.  ( 0 ... ( P  - 
1 ) ) )
63 eluzfz1 11614 . . . . . . . . . 10  |-  ( ( P  -  1 )  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... ( P  -  1 ) ) )
6460, 63syl 16 . . . . . . . . 9  |-  ( ph  ->  0  e.  ( 0 ... ( P  - 
1 ) ) )
6562, 64ifcld 3900 . . . . . . . 8  |-  ( ph  ->  if ( j  =  0 ,  ( P  -  1 ) ,  0 )  e.  ( 0 ... ( P  -  1 ) ) )
6665adantr 463 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  if ( j  =  0 ,  ( P  - 
1 ) ,  0 )  e.  ( 0 ... ( P  - 
1 ) ) )
67 etransclem35.d . . . . . . 7  |-  D  =  ( j  e.  ( 0 ... M ) 
|->  if ( j  =  0 ,  ( P  -  1 ) ,  0 ) )
6866, 67fmptd 5957 . . . . . 6  |-  ( ph  ->  D : ( 0 ... M ) --> ( 0 ... ( P  -  1 ) ) )
69 ovex 6224 . . . . . . 7  |-  ( 0 ... ( P  - 
1 ) )  e. 
_V
70 ovex 6224 . . . . . . 7  |-  ( 0 ... M )  e. 
_V
7169, 70elmap 7366 . . . . . 6  |-  ( D  e.  ( ( 0 ... ( P  - 
1 ) )  ^m  ( 0 ... M
) )  <->  D :
( 0 ... M
) --> ( 0 ... ( P  -  1 ) ) )
7268, 71sylibr 212 . . . . 5  |-  ( ph  ->  D  e.  ( ( 0 ... ( P  -  1 ) )  ^m  ( 0 ... M ) ) )
739, 59syl6eleq 2480 . . . . . . 7  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
74 fzsscn 31680 . . . . . . . 8  |-  ( 0 ... ( P  - 
1 ) )  C_  CC
7568ffvelrnda 5933 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( D `  j )  e.  ( 0 ... ( P  -  1 ) ) )
7674, 75sseldi 3415 . . . . . . 7  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( D `  j )  e.  CC )
77 fveq2 5774 . . . . . . 7  |-  ( j  =  0  ->  ( D `  j )  =  ( D ` 
0 ) )
7873, 76, 77fsum1p 13570 . . . . . 6  |-  ( ph  -> 
sum_ j  e.  ( 0 ... M ) ( D `  j
)  =  ( ( D `  0 )  +  sum_ j  e.  ( ( 0  +  1 ) ... M ) ( D `  j
) ) )
7967a1i 11 . . . . . . . 8  |-  ( ph  ->  D  =  ( j  e.  ( 0 ... M )  |->  if ( j  =  0 ,  ( P  -  1 ) ,  0 ) ) )
80 simpr 459 . . . . . . . . 9  |-  ( (
ph  /\  j  = 
0 )  ->  j  =  0 )
8180iftrued 3865 . . . . . . . 8  |-  ( (
ph  /\  j  = 
0 )  ->  if ( j  =  0 ,  ( P  - 
1 ) ,  0 )  =  ( P  -  1 ) )
82 eluzfz1 11614 . . . . . . . . 9  |-  ( M  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... M
) )
8373, 82syl 16 . . . . . . . 8  |-  ( ph  ->  0  e.  ( 0 ... M ) )
8479, 81, 83, 12fvmptd 5862 . . . . . . 7  |-  ( ph  ->  ( D `  0
)  =  ( P  -  1 ) )
85 0p1e1 10564 . . . . . . . . . . 11  |-  ( 0  +  1 )  =  1
8685oveq1i 6206 . . . . . . . . . 10  |-  ( ( 0  +  1 ) ... M )  =  ( 1 ... M
)
8786sumeq1i 13522 . . . . . . . . 9  |-  sum_ j  e.  ( ( 0  +  1 ) ... M
) ( D `  j )  =  sum_ j  e.  ( 1 ... M ) ( D `  j )
8887a1i 11 . . . . . . . 8  |-  ( ph  -> 
sum_ j  e.  ( ( 0  +  1 ) ... M ) ( D `  j
)  =  sum_ j  e.  ( 1 ... M
) ( D `  j ) )
8967fvmpt2 5865 . . . . . . . . . . 11  |-  ( ( j  e.  ( 0 ... M )  /\  if ( j  =  0 ,  ( P  - 
1 ) ,  0 )  e.  ( 0 ... ( P  - 
1 ) ) )  ->  ( D `  j )  =  if ( j  =  0 ,  ( P  - 
1 ) ,  0 ) )
9051, 65, 89syl2anr 476 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( D `  j )  =  if ( j  =  0 ,  ( P  -  1 ) ,  0 ) )
91 0red 9508 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... M )  ->  0  e.  RR )
92 1red 9522 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 1 ... M )  ->  1  e.  RR )
93 elfzelz 11609 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 1 ... M )  ->  j  e.  ZZ )
9493zred 10884 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 1 ... M )  ->  j  e.  RR )
95 0lt1 9992 . . . . . . . . . . . . . . . 16  |-  0  <  1
9695a1i 11 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 1 ... M )  ->  0  <  1 )
97 elfzle1 11610 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( 1 ... M )  ->  1  <_  j )
9891, 92, 94, 96, 97ltletrd 9653 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... M )  ->  0  <  j )
9991, 98gtned 9631 . . . . . . . . . . . . 13  |-  ( j  e.  ( 1 ... M )  ->  j  =/=  0 )
10099neneqd 2584 . . . . . . . . . . . 12  |-  ( j  e.  ( 1 ... M )  ->  -.  j  =  0 )
101100iffalsed 3868 . . . . . . . . . . 11  |-  ( j  e.  ( 1 ... M )  ->  if ( j  =  0 ,  ( P  - 
1 ) ,  0 )  =  0 )
102101adantl 464 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  if ( j  =  0 ,  ( P  - 
1 ) ,  0 )  =  0 )
10390, 102eqtrd 2423 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( D `  j )  =  0 )
104103sumeq2dv 13527 . . . . . . . 8  |-  ( ph  -> 
sum_ j  e.  ( 1 ... M ) ( D `  j
)  =  sum_ j  e.  ( 1 ... M
) 0 )
105 fzfi 11985 . . . . . . . . . 10  |-  ( 1 ... M )  e. 
Fin
106105olci 389 . . . . . . . . 9  |-  ( ( 1 ... M ) 
C_  ( ZZ>= `  A
)  \/  ( 1 ... M )  e. 
Fin )
107 sumz 13546 . . . . . . . . 9  |-  ( ( ( 1 ... M
)  C_  ( ZZ>= `  A )  \/  (
1 ... M )  e. 
Fin )  ->  sum_ j  e.  ( 1 ... M
) 0  =  0 )
108106, 107mp1i 12 . . . . . . . 8  |-  ( ph  -> 
sum_ j  e.  ( 1 ... M ) 0  =  0 )
10988, 104, 1083eqtrd 2427 . . . . . . 7  |-  ( ph  -> 
sum_ j  e.  ( ( 0  +  1 ) ... M ) ( D `  j
)  =  0 )
11084, 109oveq12d 6214 . . . . . 6  |-  ( ph  ->  ( ( D ` 
0 )  +  sum_ j  e.  ( (
0  +  1 ) ... M ) ( D `  j ) )  =  ( ( P  -  1 )  +  0 ) )
1118nncnd 10468 . . . . . . . 8  |-  ( ph  ->  P  e.  CC )
112 1cnd 9523 . . . . . . . 8  |-  ( ph  ->  1  e.  CC )
113111, 112subcld 9844 . . . . . . 7  |-  ( ph  ->  ( P  -  1 )  e.  CC )
114113addid1d 9691 . . . . . 6  |-  ( ph  ->  ( ( P  - 
1 )  +  0 )  =  ( P  -  1 ) )
11578, 110, 1143eqtrd 2427 . . . . 5  |-  ( ph  -> 
sum_ j  e.  ( 0 ... M ) ( D `  j
)  =  ( P  -  1 ) )
116 fveq1 5773 . . . . . . . 8  |-  ( c  =  D  ->  (
c `  j )  =  ( D `  j ) )
117116sumeq2ad 31732 . . . . . . 7  |-  ( c  =  D  ->  sum_ j  e.  ( 0 ... M
) ( c `  j )  =  sum_ j  e.  ( 0 ... M ) ( D `  j ) )
118117eqeq1d 2384 . . . . . 6  |-  ( c  =  D  ->  ( sum_ j  e.  ( 0 ... M ) ( c `  j )  =  ( P  - 
1 )  <->  sum_ j  e.  ( 0 ... M
) ( D `  j )  =  ( P  -  1 ) ) )
119118elrab 3182 . . . . 5  |-  ( D  e.  { c  e.  ( ( 0 ... ( P  -  1 ) )  ^m  (
0 ... M ) )  |  sum_ j  e.  ( 0 ... M ) ( c `  j
)  =  ( P  -  1 ) }  <-> 
( D  e.  ( ( 0 ... ( P  -  1 ) )  ^m  ( 0 ... M ) )  /\  sum_ j  e.  ( 0 ... M ) ( D `  j
)  =  ( P  -  1 ) ) )
12072, 115, 119sylanbrc 662 . . . 4  |-  ( ph  ->  D  e.  { c  e.  ( ( 0 ... ( P  - 
1 ) )  ^m  ( 0 ... M
) )  |  sum_ j  e.  ( 0 ... M ) ( c `  j )  =  ( P  - 
1 ) } )
121120, 21eleqtrrd 2473 . . 3  |-  ( ph  ->  D  e.  ( C `
 ( P  - 
1 ) ) )
122116fveq2d 5778 . . . . . 6  |-  ( c  =  D  ->  ( ! `  ( c `  j ) )  =  ( ! `  ( D `  j )
) )
123122prodeq2ad 31756 . . . . 5  |-  ( c  =  D  ->  prod_ j  e.  ( 0 ... M ) ( ! `
 ( c `  j ) )  = 
prod_ j  e.  (
0 ... M ) ( ! `  ( D `
 j ) ) )
124123oveq2d 6212 . . . 4  |-  ( c  =  D  ->  (
( ! `  ( P  -  1 ) )  /  prod_ j  e.  ( 0 ... M
) ( ! `  ( c `  j
) ) )  =  ( ( ! `  ( P  -  1
) )  /  prod_ j  e.  ( 0 ... M ) ( ! `
 ( D `  j ) ) ) )
125 fveq1 5773 . . . . . . 7  |-  ( c  =  D  ->  (
c `  0 )  =  ( D ` 
0 ) )
126125breq2d 4379 . . . . . 6  |-  ( c  =  D  ->  (
( P  -  1 )  <  ( c `
 0 )  <->  ( P  -  1 )  < 
( D `  0
) ) )
127125oveq2d 6212 . . . . . . . . 9  |-  ( c  =  D  ->  (
( P  -  1 )  -  ( c `
 0 ) )  =  ( ( P  -  1 )  -  ( D `  0 ) ) )
128127fveq2d 5778 . . . . . . . 8  |-  ( c  =  D  ->  ( ! `  ( ( P  -  1 )  -  ( c ` 
0 ) ) )  =  ( ! `  ( ( P  - 
1 )  -  ( D `  0 )
) ) )
129128oveq2d 6212 . . . . . . 7  |-  ( c  =  D  ->  (
( ! `  ( P  -  1 ) )  /  ( ! `
 ( ( P  -  1 )  -  ( c `  0
) ) ) )  =  ( ( ! `
 ( P  - 
1 ) )  / 
( ! `  (
( P  -  1 )  -  ( D `
 0 ) ) ) ) )
130127oveq2d 6212 . . . . . . 7  |-  ( c  =  D  ->  (
0 ^ ( ( P  -  1 )  -  ( c ` 
0 ) ) )  =  ( 0 ^ ( ( P  - 
1 )  -  ( D `  0 )
) ) )
131129, 130oveq12d 6214 . . . . . 6  |-  ( c  =  D  ->  (
( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( c ` 
0 ) ) ) )  x.  ( 0 ^ ( ( P  -  1 )  -  ( c `  0
) ) ) )  =  ( ( ( ! `  ( P  -  1 ) )  /  ( ! `  ( ( P  - 
1 )  -  ( D `  0 )
) ) )  x.  ( 0 ^ (
( P  -  1 )  -  ( D `
 0 ) ) ) ) )
132126, 131ifbieq2d 3882 . . . . 5  |-  ( c  =  D  ->  if ( ( P  - 
1 )  <  (
c `  0 ) ,  0 ,  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( c ` 
0 ) ) ) )  x.  ( 0 ^ ( ( P  -  1 )  -  ( c `  0
) ) ) ) )  =  if ( ( P  -  1 )  <  ( D `
 0 ) ,  0 ,  ( ( ( ! `  ( P  -  1 ) )  /  ( ! `
 ( ( P  -  1 )  -  ( D `  0 ) ) ) )  x.  ( 0 ^ (
( P  -  1 )  -  ( D `
 0 ) ) ) ) ) )
133116breq2d 4379 . . . . . . 7  |-  ( c  =  D  ->  ( P  <  ( c `  j )  <->  P  <  ( D `  j ) ) )
134116oveq2d 6212 . . . . . . . . . 10  |-  ( c  =  D  ->  ( P  -  ( c `  j ) )  =  ( P  -  ( D `  j )
) )
135134fveq2d 5778 . . . . . . . . 9  |-  ( c  =  D  ->  ( ! `  ( P  -  ( c `  j ) ) )  =  ( ! `  ( P  -  ( D `  j )
) ) )
136135oveq2d 6212 . . . . . . . 8  |-  ( c  =  D  ->  (
( ! `  P
)  /  ( ! `
 ( P  -  ( c `  j
) ) ) )  =  ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) ) )
137134oveq2d 6212 . . . . . . . 8  |-  ( c  =  D  ->  (
( 0  -  j
) ^ ( P  -  ( c `  j ) ) )  =  ( ( 0  -  j ) ^
( P  -  ( D `  j )
) ) )
138136, 137oveq12d 6214 . . . . . . 7  |-  ( c  =  D  ->  (
( ( ! `  P )  /  ( ! `  ( P  -  ( c `  j ) ) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( c `  j
) ) ) )  =  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  j )
) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )
139133, 138ifbieq2d 3882 . . . . . 6  |-  ( c  =  D  ->  if ( P  <  ( c `
 j ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( c `  j
) ) ) )  x.  ( ( 0  -  j ) ^
( P  -  (
c `  j )
) ) ) )  =  if ( P  <  ( D `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  j )
) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) )
140139prodeq2ad 31756 . . . . 5  |-  ( c  =  D  ->  prod_ j  e.  ( 1 ... M ) if ( P  <  ( c `
 j ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( c `  j
) ) ) )  x.  ( ( 0  -  j ) ^
( P  -  (
c `  j )
) ) ) )  =  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) )
141132, 140oveq12d 6214 . . . 4  |-  ( c  =  D  ->  ( if ( ( P  - 
1 )  <  (
c `  0 ) ,  0 ,  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( c ` 
0 ) ) ) )  x.  ( 0 ^ ( ( P  -  1 )  -  ( c `  0
) ) ) ) )  x.  prod_ j  e.  ( 1 ... M
) if ( P  <  ( c `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  (
c `  j )
) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( c `  j ) ) ) ) ) )  =  ( if ( ( P  -  1 )  <  ( D ` 
0 ) ,  0 ,  ( ( ( ! `  ( P  -  1 ) )  /  ( ! `  ( ( P  - 
1 )  -  ( D `  0 )
) ) )  x.  ( 0 ^ (
( P  -  1 )  -  ( D `
 0 ) ) ) ) )  x. 
prod_ j  e.  (
1 ... M ) if ( P  <  ( D `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )
142124, 141oveq12d 6214 . . 3  |-  ( c  =  D  ->  (
( ( ! `  ( P  -  1
) )  /  prod_ j  e.  ( 0 ... M ) ( ! `
 ( c `  j ) ) )  x.  ( if ( ( P  -  1 )  <  ( c `
 0 ) ,  0 ,  ( ( ( ! `  ( P  -  1 ) )  /  ( ! `
 ( ( P  -  1 )  -  ( c `  0
) ) ) )  x.  ( 0 ^ ( ( P  - 
1 )  -  (
c `  0 )
) ) ) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  < 
( c `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( c `  j ) ) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( c `  j
) ) ) ) ) ) )  =  ( ( ( ! `
 ( P  - 
1 ) )  /  prod_ j  e.  ( 0 ... M ) ( ! `  ( D `
 j ) ) )  x.  ( if ( ( P  - 
1 )  <  ( D `  0 ) ,  0 ,  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( D ` 
0 ) ) ) )  x.  ( 0 ^ ( ( P  -  1 )  -  ( D `  0 ) ) ) ) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) ) )
14317, 18, 19, 58, 121, 142fsumsplit1 31739 . 2  |-  ( ph  -> 
sum_ c  e.  ( C `  ( P  -  1 ) ) ( ( ( ! `
 ( P  - 
1 ) )  /  prod_ j  e.  ( 0 ... M ) ( ! `  ( c `
 j ) ) )  x.  ( if ( ( P  - 
1 )  <  (
c `  0 ) ,  0 ,  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( c ` 
0 ) ) ) )  x.  ( 0 ^ ( ( P  -  1 )  -  ( c `  0
) ) ) ) )  x.  prod_ j  e.  ( 1 ... M
) if ( P  <  ( c `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  (
c `  j )
) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( c `  j ) ) ) ) ) ) )  =  ( ( ( ( ! `  ( P  -  1 ) )  /  prod_ j  e.  ( 0 ... M
) ( ! `  ( D `  j ) ) )  x.  ( if ( ( P  - 
1 )  <  ( D `  0 ) ,  0 ,  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( D ` 
0 ) ) ) )  x.  ( 0 ^ ( ( P  -  1 )  -  ( D `  0 ) ) ) ) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )  +  sum_ c  e.  ( ( C `  ( P  -  1 ) ) 
\  { D }
) ( ( ( ! `  ( P  -  1 ) )  /  prod_ j  e.  ( 0 ... M ) ( ! `  (
c `  j )
) )  x.  ( if ( ( P  - 
1 )  <  (
c `  0 ) ,  0 ,  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( c ` 
0 ) ) ) )  x.  ( 0 ^ ( ( P  -  1 )  -  ( c `  0
) ) ) ) )  x.  prod_ j  e.  ( 1 ... M
) if ( P  <  ( c `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  (
c `  j )
) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( c `  j ) ) ) ) ) ) ) ) )
14433, 75sseldi 3415 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( D `  j )  e.  NN0 )
145144faccld 31682 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( ! `  ( D `  j ) )  e.  NN )
146145nncnd 10468 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( ! `  ( D `  j ) )  e.  CC )
14777fveq2d 5778 . . . . . . . . . 10  |-  ( j  =  0  ->  ( ! `  ( D `  j ) )  =  ( ! `  ( D `  0 )
) )
14873, 146, 147fprod1p 13774 . . . . . . . . 9  |-  ( ph  ->  prod_ j  e.  ( 0 ... M ) ( ! `  ( D `  j )
)  =  ( ( ! `  ( D `
 0 ) )  x.  prod_ j  e.  ( ( 0  +  1 ) ... M ) ( ! `  ( D `  j )
) ) )
14984fveq2d 5778 . . . . . . . . . 10  |-  ( ph  ->  ( ! `  ( D `  0 )
)  =  ( ! `
 ( P  - 
1 ) ) )
15086prodeq1i 13727 . . . . . . . . . . . 12  |-  prod_ j  e.  ( ( 0  +  1 ) ... M
) ( ! `  ( D `  j ) )  =  prod_ j  e.  ( 1 ... M
) ( ! `  ( D `  j ) )
151150a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  prod_ j  e.  ( ( 0  +  1 ) ... M ) ( ! `  ( D `  j )
)  =  prod_ j  e.  ( 1 ... M
) ( ! `  ( D `  j ) ) )
152103fveq2d 5778 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( ! `  ( D `  j ) )  =  ( ! `  0
) )
153 fac0 12258 . . . . . . . . . . . . 13  |-  ( ! `
 0 )  =  1
154152, 153syl6eq 2439 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( ! `  ( D `  j ) )  =  1 )
155154prodeq2dv 13732 . . . . . . . . . . 11  |-  ( ph  ->  prod_ j  e.  ( 1 ... M ) ( ! `  ( D `  j )
)  =  prod_ j  e.  ( 1 ... M
) 1 )
156 prod1 13753 . . . . . . . . . . . 12  |-  ( ( ( 1 ... M
)  C_  ( ZZ>= `  A )  \/  (
1 ... M )  e. 
Fin )  ->  prod_ j  e.  ( 1 ... M ) 1  =  1 )
157106, 156mp1i 12 . . . . . . . . . . 11  |-  ( ph  ->  prod_ j  e.  ( 1 ... M ) 1  =  1 )
158151, 155, 1573eqtrd 2427 . . . . . . . . . 10  |-  ( ph  ->  prod_ j  e.  ( ( 0  +  1 ) ... M ) ( ! `  ( D `  j )
)  =  1 )
159149, 158oveq12d 6214 . . . . . . . . 9  |-  ( ph  ->  ( ( ! `  ( D `  0 ) )  x.  prod_ j  e.  ( ( 0  +  1 ) ... M
) ( ! `  ( D `  j ) ) )  =  ( ( ! `  ( P  -  1 ) )  x.  1 ) )
16012faccld 31682 . . . . . . . . . . 11  |-  ( ph  ->  ( ! `  ( P  -  1 ) )  e.  NN )
161160nncnd 10468 . . . . . . . . . 10  |-  ( ph  ->  ( ! `  ( P  -  1 ) )  e.  CC )
162161mulid1d 9524 . . . . . . . . 9  |-  ( ph  ->  ( ( ! `  ( P  -  1
) )  x.  1 )  =  ( ! `
 ( P  - 
1 ) ) )
163148, 159, 1623eqtrd 2427 . . . . . . . 8  |-  ( ph  ->  prod_ j  e.  ( 0 ... M ) ( ! `  ( D `  j )
)  =  ( ! `
 ( P  - 
1 ) ) )
164163oveq2d 6212 . . . . . . 7  |-  ( ph  ->  ( ( ! `  ( P  -  1
) )  /  prod_ j  e.  ( 0 ... M ) ( ! `
 ( D `  j ) ) )  =  ( ( ! `
 ( P  - 
1 ) )  / 
( ! `  ( P  -  1 ) ) ) )
165160nnne0d 10497 . . . . . . . 8  |-  ( ph  ->  ( ! `  ( P  -  1 ) )  =/=  0 )
166161, 165dividd 10235 . . . . . . 7  |-  ( ph  ->  ( ( ! `  ( P  -  1
) )  /  ( ! `  ( P  -  1 ) ) )  =  1 )
167164, 166eqtrd 2423 . . . . . 6  |-  ( ph  ->  ( ( ! `  ( P  -  1
) )  /  prod_ j  e.  ( 0 ... M ) ( ! `
 ( D `  j ) ) )  =  1 )
16812nn0red 10770 . . . . . . . . . . . . 13  |-  ( ph  ->  ( P  -  1 )  e.  RR )
16984, 168eqeltrd 2470 . . . . . . . . . . . 12  |-  ( ph  ->  ( D `  0
)  e.  RR )
170169, 168lttri3d 9636 . . . . . . . . . . 11  |-  ( ph  ->  ( ( D ` 
0 )  =  ( P  -  1 )  <-> 
( -.  ( D `
 0 )  < 
( P  -  1 )  /\  -.  ( P  -  1 )  <  ( D ` 
0 ) ) ) )
17184, 170mpbid 210 . . . . . . . . . 10  |-  ( ph  ->  ( -.  ( D `
 0 )  < 
( P  -  1 )  /\  -.  ( P  -  1 )  <  ( D ` 
0 ) ) )
172171simprd 461 . . . . . . . . 9  |-  ( ph  ->  -.  ( P  - 
1 )  <  ( D `  0 )
)
173172iffalsed 3868 . . . . . . . 8  |-  ( ph  ->  if ( ( P  -  1 )  < 
( D `  0
) ,  0 ,  ( ( ( ! `
 ( P  - 
1 ) )  / 
( ! `  (
( P  -  1 )  -  ( D `
 0 ) ) ) )  x.  (
0 ^ ( ( P  -  1 )  -  ( D ` 
0 ) ) ) ) )  =  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( D ` 
0 ) ) ) )  x.  ( 0 ^ ( ( P  -  1 )  -  ( D `  0 ) ) ) ) )
17484eqcomd 2390 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( P  -  1 )  =  ( D `
 0 ) )
175113, 174subeq0bd 9903 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( P  - 
1 )  -  ( D `  0 )
)  =  0 )
176175fveq2d 5778 . . . . . . . . . . . 12  |-  ( ph  ->  ( ! `  (
( P  -  1 )  -  ( D `
 0 ) ) )  =  ( ! `
 0 ) )
177176, 153syl6eq 2439 . . . . . . . . . . 11  |-  ( ph  ->  ( ! `  (
( P  -  1 )  -  ( D `
 0 ) ) )  =  1 )
178177oveq2d 6212 . . . . . . . . . 10  |-  ( ph  ->  ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( D ` 
0 ) ) ) )  =  ( ( ! `  ( P  -  1 ) )  /  1 ) )
179161div1d 10229 . . . . . . . . . 10  |-  ( ph  ->  ( ( ! `  ( P  -  1
) )  /  1
)  =  ( ! `
 ( P  - 
1 ) ) )
180178, 179eqtrd 2423 . . . . . . . . 9  |-  ( ph  ->  ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( D ` 
0 ) ) ) )  =  ( ! `
 ( P  - 
1 ) ) )
181175oveq2d 6212 . . . . . . . . . 10  |-  ( ph  ->  ( 0 ^ (
( P  -  1 )  -  ( D `
 0 ) ) )  =  ( 0 ^ 0 ) )
182 0cnd 9500 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  CC )
183182exp0d 12206 . . . . . . . . . 10  |-  ( ph  ->  ( 0 ^ 0 )  =  1 )
184181, 183eqtrd 2423 . . . . . . . . 9  |-  ( ph  ->  ( 0 ^ (
( P  -  1 )  -  ( D `
 0 ) ) )  =  1 )
185180, 184oveq12d 6214 . . . . . . . 8  |-  ( ph  ->  ( ( ( ! `
 ( P  - 
1 ) )  / 
( ! `  (
( P  -  1 )  -  ( D `
 0 ) ) ) )  x.  (
0 ^ ( ( P  -  1 )  -  ( D ` 
0 ) ) ) )  =  ( ( ! `  ( P  -  1 ) )  x.  1 ) )
186173, 185, 1623eqtrd 2427 . . . . . . 7  |-  ( ph  ->  if ( ( P  -  1 )  < 
( D `  0
) ,  0 ,  ( ( ( ! `
 ( P  - 
1 ) )  / 
( ! `  (
( P  -  1 )  -  ( D `
 0 ) ) ) )  x.  (
0 ^ ( ( P  -  1 )  -  ( D ` 
0 ) ) ) ) )  =  ( ! `  ( P  -  1 ) ) )
187 fzssre 31684 . . . . . . . . . . . 12  |-  ( 0 ... ( P  - 
1 ) )  C_  RR
18868adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  D : ( 0 ... M ) --> ( 0 ... ( P  - 
1 ) ) )
18951adantl 464 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  j  e.  ( 0 ... M
) )
190188, 189ffvelrnd 5934 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( D `  j )  e.  ( 0 ... ( P  -  1 ) ) )
191187, 190sseldi 3415 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( D `  j )  e.  RR )
1928nnred 10467 . . . . . . . . . . . 12  |-  ( ph  ->  P  e.  RR )
193192adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  P  e.  RR )
1948nngt0d 10496 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <  P )
19515, 192, 194ltled 9644 . . . . . . . . . . . . 13  |-  ( ph  ->  0  <_  P )
196195adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  0  <_  P )
197103, 196eqbrtrd 4387 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( D `  j )  <_  P )
198191, 193, 197leimnltd 31639 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  -.  P  <  ( D `  j ) )
199198iffalsed 3868 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  if ( P  <  ( D `
 j ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  j ) ) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )  =  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )
200103oveq2d 6212 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( P  -  ( D `  j ) )  =  ( P  -  0 ) )
201111adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  P  e.  CC )
202201subid1d 9833 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( P  -  0 )  =  P )
203200, 202eqtrd 2423 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( P  -  ( D `  j ) )  =  P )
204203fveq2d 5778 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( ! `  ( P  -  ( D `  j ) ) )  =  ( ! `  P ) )
205204oveq2d 6212 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  (
( ! `  P
)  /  ( ! `
 ( P  -  ( D `  j ) ) ) )  =  ( ( ! `  P )  /  ( ! `  P )
) )
2068nnnn0d 10769 . . . . . . . . . . . . . . 15  |-  ( ph  ->  P  e.  NN0 )
207206faccld 31682 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ! `  P
)  e.  NN )
208207nncnd 10468 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ! `  P
)  e.  CC )
209207nnne0d 10497 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ! `  P
)  =/=  0 )
210208, 209dividd 10235 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ! `  P )  /  ( ! `  P )
)  =  1 )
211210adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  (
( ! `  P
)  /  ( ! `
 P ) )  =  1 )
212205, 211eqtrd 2423 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  (
( ! `  P
)  /  ( ! `
 ( P  -  ( D `  j ) ) ) )  =  1 )
213 df-neg 9721 . . . . . . . . . . . . 13  |-  -u j  =  ( 0  -  j )
214213eqcomi 2395 . . . . . . . . . . . 12  |-  ( 0  -  j )  = 
-u j
215214a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  (
0  -  j )  =  -u j )
216215, 203oveq12d 6214 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  (
( 0  -  j
) ^ ( P  -  ( D `  j ) ) )  =  ( -u j ^ P ) )
217212, 216oveq12d 6214 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  (
( ( ! `  P )  /  ( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( D `  j ) ) ) )  =  ( 1  x.  ( -u j ^ P ) ) )
21893znegcld 10886 . . . . . . . . . . . . 13  |-  ( j  e.  ( 1 ... M )  ->  -u j  e.  ZZ )
219218zcnd 10885 . . . . . . . . . . . 12  |-  ( j  e.  ( 1 ... M )  ->  -u j  e.  CC )
220219adantl 464 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  -u j  e.  CC )
221206adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  P  e.  NN0 )
222220, 221expcld 12212 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( -u j ^ P )  e.  CC )
223222mulid2d 9525 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  (
1  x.  ( -u j ^ P ) )  =  ( -u j ^ P ) )
224199, 217, 2233eqtrd 2427 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  if ( P  <  ( D `
 j ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  j ) ) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )  =  (
-u j ^ P
) )
225224prodeq2dv 13732 . . . . . . 7  |-  ( ph  ->  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )  =  prod_ j  e.  ( 1 ... M ) ( -u j ^ P ) )
226186, 225oveq12d 6214 . . . . . 6  |-  ( ph  ->  ( if ( ( P  -  1 )  <  ( D ` 
0 ) ,  0 ,  ( ( ( ! `  ( P  -  1 ) )  /  ( ! `  ( ( P  - 
1 )  -  ( D `  0 )
) ) )  x.  ( 0 ^ (
( P  -  1 )  -  ( D `
 0 ) ) ) ) )  x. 
prod_ j  e.  (
1 ... M ) if ( P  <  ( D `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) )  =  ( ( ! `  ( P  -  1 ) )  x.  prod_ j  e.  ( 1 ... M ) ( -u j ^ P ) ) )
227167, 226oveq12d 6214 . . . . 5  |-  ( ph  ->  ( ( ( ! `
 ( P  - 
1 ) )  /  prod_ j  e.  ( 0 ... M ) ( ! `  ( D `
 j ) ) )  x.  ( if ( ( P  - 
1 )  <  ( D `  0 ) ,  0 ,  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( D ` 
0 ) ) ) )  x.  ( 0 ^ ( ( P  -  1 )  -  ( D `  0 ) ) ) ) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )  =  ( 1  x.  ( ( ! `  ( P  -  1 ) )  x.  prod_ j  e.  ( 1 ... M ) ( -u j ^ P ) ) ) )
228 fzfid 11986 . . . . . . . . 9  |-  ( ph  ->  ( 1 ... M
)  e.  Fin )
229 zexpcl 12084 . . . . . . . . . 10  |-  ( (
-u j  e.  ZZ  /\  P  e.  NN0 )  ->  ( -u j ^ P )  e.  ZZ )
230218, 206, 229syl2anr 476 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( -u j ^ P )  e.  ZZ )
231228, 230fprodzcl 13763 . . . . . . . 8  |-  ( ph  ->  prod_ j  e.  ( 1 ... M ) ( -u j ^ P )  e.  ZZ )
232231zcnd 10885 . . . . . . 7  |-  ( ph  ->  prod_ j  e.  ( 1 ... M ) ( -u j ^ P )  e.  CC )
233161, 232mulcld 9527 . . . . . 6  |-  ( ph  ->  ( ( ! `  ( P  -  1
) )  x.  prod_ j  e.  ( 1 ... M ) ( -u j ^ P ) )  e.  CC )
234233mulid2d 9525 . . . . 5  |-  ( ph  ->  ( 1  x.  (
( ! `  ( P  -  1 ) )  x.  prod_ j  e.  ( 1 ... M
) ( -u j ^ P ) ) )  =  ( ( ! `
 ( P  - 
1 ) )  x. 
prod_ j  e.  (
1 ... M ) (
-u j ^ P
) ) )
235227, 234eqtrd 2423 . . . 4  |-  ( ph  ->  ( ( ( ! `
 ( P  - 
1 ) )  /  prod_ j  e.  ( 0 ... M ) ( ! `  ( D `
 j ) ) )  x.  ( if ( ( P  - 
1 )  <  ( D `  0 ) ,  0 ,  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( D ` 
0 ) ) ) )  x.  ( 0 ^ ( ( P  -  1 )  -  ( D `  0 ) ) ) ) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( 0  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )  =  ( ( ! `  ( P  -  1 ) )  x.  prod_ j  e.  ( 1 ... M
) ( -u j ^ P ) ) )
236 eldifi 3540 . . . . . . . . . . . . . . 15  |-  ( c  e.  ( ( C `
 ( P  - 
1 ) )  \  { D } )  -> 
c  e.  ( C `
 ( P  - 
1 ) ) )
23783adantr 463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  0  e.  ( 0 ... M
) )
23844, 237ffvelrnd 5934 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  ( c `  0 )  e.  ( 0 ... ( P  -  1 ) ) )
239236, 238sylan2 472 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  c  e.  ( ( C `  ( P  -  1
) )  \  { D } ) )  -> 
( c `  0
)  e.  ( 0 ... ( P  - 
1 ) ) )
240187, 239sseldi 3415 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c  e.  ( ( C `  ( P  -  1
) )  \  { D } ) )  -> 
( c `  0
)  e.  RR )
241168adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c  e.  ( ( C `  ( P  -  1
) )  \  { D } ) )  -> 
( P  -  1 )  e.  RR )
242 elfzle2 11611 . . . . . . . . . . . . . 14  |-  ( ( c `  0 )  e.  ( 0 ... ( P  -  1 ) )  ->  (
c `  0 )  <_  ( P  -  1 ) )
243239, 242syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c  e.  ( ( C `  ( P  -  1
) )  \  { D } ) )  -> 
( c `  0
)  <_  ( P  -  1 ) )
244240, 241, 243leimnltd 31639 . . . . . . . . . . . 12  |-  ( (
ph  /\  c  e.  ( ( C `  ( P  -  1
) )  \  { D } ) )  ->  -.  ( P  -  1 )  <  ( c `
 0 ) )
245244iffalsed 3868 . . . . . . . . . . 11  |-  ( (
ph  /\  c  e.  ( ( C `  ( P  -  1
) )  \  { D } ) )  ->  if ( ( P  - 
1 )  <  (
c `  0 ) ,  0 ,  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( c ` 
0 ) ) ) )  x.  ( 0 ^ ( ( P  -  1 )  -  ( c `  0
) ) ) ) )  =  ( ( ( ! `  ( P  -  1 ) )  /  ( ! `
 ( ( P  -  1 )  -  ( c `  0
) ) ) )  x.  ( 0 ^ ( ( P  - 
1 )  -  (
c `  0 )
) ) ) )
24612nn0zd 10882 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( P  -  1 )  e.  ZZ )
247246adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  c  e.  ( ( C `  ( P  -  1
) )  \  { D } ) )  -> 
( P  -  1 )  e.  ZZ )
248239elfzelzd 31685 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  c  e.  ( ( C `  ( P  -  1
) )  \  { D } ) )  -> 
( c `  0
)  e.  ZZ )
249247, 248zsubcld 10889 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  c  e.  ( ( C `  ( P  -  1
) )  \  { D } ) )  -> 
( ( P  - 
1 )  -  (
c `  0 )
)  e.  ZZ )
250 ffn 5639 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( c : ( 0 ... M ) --> ( 0 ... ( P  - 
1 ) )  -> 
c  Fn  ( 0 ... M ) )
25144, 250syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  c  Fn  ( 0 ... M
) )
252251adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  ( P  -  1 )  =  ( c ` 
0 ) )  -> 
c  Fn  ( 0 ... M ) )
253 ffn 5639 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( D : ( 0 ... M ) --> ( 0 ... ( P  - 
1 ) )  ->  D  Fn  ( 0 ... M ) )
25468, 253syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  D  Fn  ( 0 ... M ) )
255254ad2antrr 723 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  ( P  -  1 )  =  ( c ` 
0 ) )  ->  D  Fn  ( 0 ... M ) )
256 fveq2 5774 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  =  0  ->  (
c `  j )  =  ( c ` 
0 ) )
257256adantl 464 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  ( P  -  1 )  =  ( c ` 
0 ) )  /\  j  =  0 )  ->  ( c `  j )  =  ( c `  0 ) )
258 id 22 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( P  -  1 )  =  ( c ` 
0 )  ->  ( P  -  1 )  =  ( c ` 
0 ) )
259258eqcomd 2390 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( P  -  1 )  =  ( c ` 
0 )  ->  (
c `  0 )  =  ( P  - 
1 ) )
260259ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  ( P  -  1 )  =  ( c ` 
0 ) )  /\  j  =  0 )  ->  ( c ` 
0 )  =  ( P  -  1 ) )
26177adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  = 
0 )  ->  ( D `  j )  =  ( D ` 
0 ) )
26284adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  = 
0 )  ->  ( D `  0 )  =  ( P  - 
1 ) )
263261, 262eqtr2d 2424 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  = 
0 )  ->  ( P  -  1 )  =  ( D `  j ) )
264263adantlr 712 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  ( P  -  1 )  =  ( c ` 
0 ) )  /\  j  =  0 )  ->  ( P  - 
1 )  =  ( D `  j ) )
265257, 260, 2643eqtrd 2427 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  ( P  -  1 )  =  ( c ` 
0 ) )  /\  j  =  0 )  ->  ( c `  j )  =  ( D `  j ) )
266265adantllr 716 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  ( P  -  1
)  =  ( c `
 0 ) )  /\  j  =  0 )  ->  ( c `  j )  =  ( D `  j ) )
267266adantlr 712 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) )  /\  ( P  - 
1 )  =  ( c `  0 ) )  /\  j  e.  ( 0 ... M
) )  /\  j  =  0 )  -> 
( c `  j
)  =  ( D `
 j ) )
26826ad4antr 729 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  ( P  -  1 )  =  ( c `  0
) )  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  /\  -.  ( c `
 j )  =  0 )  ->  sum_ j  e.  ( 0 ... M
) ( c `  j )  =  ( P  -  1 ) )
269168ad5antr 731 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  ( P  -  1 )  =  ( c `  0
) )  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  /\  -.  ( c `
 j )  =  0 )  ->  ( P  -  1 )  e.  RR )
270168ad4antr 729 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) )  /\  j  e.  ( 0 ... M ) )  /\  -.  j  =  0 )  /\  -.  ( c `  j
)  =  0 )  ->  ( P  - 
1 )  e.  RR )
27144adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  k  e.  ( 1 ... M
) )  ->  c : ( 0 ... M ) --> ( 0 ... ( P  - 
1 ) ) )
27250sseli 3413 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( k  e.  ( 1 ... M )  ->  k  e.  ( 0 ... M
) )
273272adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  k  e.  ( 1 ... M
) )  ->  k  e.  ( 0 ... M
) )
274271, 273ffvelrnd 5934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  k  e.  ( 1 ... M
) )  ->  (
c `  k )  e.  ( 0 ... ( P  -  1 ) ) )
27533, 274sseldi 3415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  k  e.  ( 1 ... M
) )  ->  (
c `  k )  e.  NN0 )
27647, 275fsumnn0cl 13560 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  sum_ k  e.  ( 1 ... M
) ( c `  k )  e.  NN0 )
277276nn0red 10770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  sum_ k  e.  ( 1 ... M
) ( c `  k )  e.  RR )
278277ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) )  /\  j  e.  ( 0 ... M ) )  /\  -.  j  =  0 )  /\  -.  ( c `  j
)  =  0 )  ->  sum_ k  e.  ( 1 ... M ) ( c `  k
)  e.  RR )
279 0red 9508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) )  /\  j  e.  ( 0 ... M ) )  /\  -.  j  =  0 )  /\  -.  ( c `  j
)  =  0 )  ->  0  e.  RR )
28044ffvelrnda 5933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  j  e.  ( 0 ... M
) )  ->  (
c `  j )  e.  ( 0 ... ( P  -  1 ) ) )
281187, 280sseldi 3415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  j  e.  ( 0 ... M
) )  ->  (
c `  j )  e.  RR )
282281ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) )  /\  j  e.  ( 0 ... M ) )  /\  -.  j  =  0 )  /\  -.  ( c `  j
)  =  0 )  ->  ( c `  j )  e.  RR )
283 nfv 1715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  F/ k ( ( ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  /\  -.  ( c `
 j )  =  0 )
284 nfcv 2544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  F/_ k
( c `  j
)
285 fzfid 11986 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) )  /\  j  e.  ( 0 ... M ) )  /\  -.  j  =  0 )  /\  -.  ( c `  j
)  =  0 )  ->  ( 1 ... M )  e.  Fin )
286 simp-4l 765 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  /\  -.  ( c `
 j )  =  0 )  /\  k  e.  ( 1 ... M
) )  ->  ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) ) )
28774, 274sseldi 3415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  k  e.  ( 1 ... M
) )  ->  (
c `  k )  e.  CC )
288286, 287sylancom 665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  /\  -.  ( c `
 j )  =  0 )  /\  k  e.  ( 1 ... M
) )  ->  (
c `  k )  e.  CC )
289 1zzd 10812 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( j  e.  ( 0 ... M )  /\  -.  j  =  0
)  ->  1  e.  ZZ )
290 elfzel2 11607 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( j  e.  ( 0 ... M )  ->  M  e.  ZZ )
291290adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( j  e.  ( 0 ... M )  /\  -.  j  =  0
)  ->  M  e.  ZZ )
292 elfzelz 11609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( j  e.  ( 0 ... M )  ->  j  e.  ZZ )
293292adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( j  e.  ( 0 ... M )  /\  -.  j  =  0
)  ->  j  e.  ZZ )
294289, 291, 2933jca 1174 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( j  e.  ( 0 ... M )  /\  -.  j  =  0
)  ->  ( 1  e.  ZZ  /\  M  e.  ZZ  /\  j  e.  ZZ ) )
295 elfznn0 11693 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( j  e.  ( 0 ... M )  ->  j  e.  NN0 )
296295adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( j  e.  ( 0 ... M )  /\  -.  j  =  0
)  ->  j  e.  NN0 )
297 neqne 31601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( -.  j  =  0  -> 
j  =/=  0 )
298297adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( j  e.  ( 0 ... M )  /\  -.  j  =  0
)  ->  j  =/=  0 )
299 elnnne0 10726 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( j  e.  NN  <->  ( j  e.  NN0  /\  j  =/=  0 ) )
300296, 298, 299sylanbrc 662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( j  e.  ( 0 ... M )  /\  -.  j  =  0
)  ->  j  e.  NN )
301300nnge1d 10495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( j  e.  ( 0 ... M )  /\  -.  j  =  0
)  ->  1  <_  j )
302 elfzle2 11611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( j  e.  ( 0 ... M )  ->  j  <_  M )
303302adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( j  e.  ( 0 ... M )  /\  -.  j  =  0
)  ->  j  <_  M )
304294, 301, 303jca32 533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( j  e.  ( 0 ... M )  /\  -.  j  =  0
)  ->  ( (
1  e.  ZZ  /\  M  e.  ZZ  /\  j  e.  ZZ )  /\  (
1  <_  j  /\  j  <_  M ) ) )
305 elfz2 11600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( j  e.  ( 1 ... M )  <->  ( (
1  e.  ZZ  /\  M  e.  ZZ  /\  j  e.  ZZ )  /\  (
1  <_  j  /\  j  <_  M ) ) )
306304, 305sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( j  e.  ( 0 ... M )  /\  -.  j  =  0
)  ->  j  e.  ( 1 ... M
) )
307306adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( j  e.  ( 0 ... M )  /\  -.  j  =  0 )  /\  -.  ( c `  j
)  =  0 )  ->  j  e.  ( 1 ... M ) )
308307adantlll 715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ( ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) )  /\  j  e.  ( 0 ... M ) )  /\  -.  j  =  0 )  /\  -.  ( c `  j
)  =  0 )  ->  j  e.  ( 1 ... M ) )
309 fveq2 5774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( k  =  j  ->  (
c `  k )  =  ( c `  j ) )
310283, 284, 285, 288, 308, 309fsumsplit1 31739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) )  /\  j  e.  ( 0 ... M ) )  /\  -.  j  =  0 )  /\  -.  ( c `  j
)  =  0 )  ->  sum_ k  e.  ( 1 ... M ) ( c `  k
)  =  ( ( c `  j )  +  sum_ k  e.  ( ( 1 ... M
)  \  { j } ) ( c `
 k ) ) )
311310eqcomd 2390 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) )  /\  j  e.  ( 0 ... M ) )  /\  -.  j  =  0 )  /\  -.  ( c `  j
)  =  0 )  ->  ( ( c `
 j )  + 
sum_ k  e.  ( ( 1 ... M
)  \  { j } ) ( c `
 k ) )  =  sum_ k  e.  ( 1 ... M ) ( c `  k
) )
312311, 278eqeltrd 2470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) )  /\  j  e.  ( 0 ... M ) )  /\  -.  j  =  0 )  /\  -.  ( c `  j
)  =  0 )  ->  ( ( c `
 j )  + 
sum_ k  e.  ( ( 1 ... M
)  \  { j } ) ( c `
 k ) )  e.  RR )
313 elfzle1 11610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( c `  j )  e.  ( 0 ... ( P  -  1 ) )  ->  0  <_  ( c `  j
) )
314280, 313syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  j  e.  ( 0 ... M
) )  ->  0  <_  ( c `  j
) )
315314ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) )  /\  j  e.  ( 0 ... M ) )  /\  -.  j  =  0 )  /\  -.  ( c `  j
)  =  0 )  ->  0  <_  (
c `  j )
)
316 neqne 31601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( -.  ( c `  j
)  =  0  -> 
( c `  j
)  =/=  0 )
317316adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) )  /\  j  e.  ( 0 ... M ) )  /\  -.  j  =  0 )  /\  -.  ( c `  j
)  =  0 )  ->  ( c `  j )  =/=  0
)
318279, 282, 315, 317leneltd 31660 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) )  /\  j  e.  ( 0 ... M ) )  /\  -.  j  =  0 )  /\  -.  ( c `  j
)  =  0 )  ->  0  <  (
c `  j )
)
319 diffi 7667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( 1 ... M )  e.  Fin  ->  (
( 1 ... M
)  \  { j } )  e.  Fin )
320105, 319mp1i 12 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  ( (
1 ... M )  \  { j } )  e.  Fin )
321 eldifi 3540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( k  e.  ( ( 1 ... M )  \  { j } )  ->  k  e.  ( 1 ... M ) )
322321adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  k  e.  ( ( 1 ... M )  \  {
j } ) )  ->  k  e.  ( 1 ... M ) )
32350, 322sseldi 3415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  k  e.  ( ( 1 ... M )  \  {
j } ) )  ->  k  e.  ( 0 ... M ) )
32444ffvelrnda 5933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  k  e.  ( 0 ... M
) )  ->  (
c `  k )  e.  ( 0 ... ( P  -  1 ) ) )
325187, 324sseldi 3415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  k  e.  ( 0 ... M
) )  ->  (
c `  k )  e.  RR )
326323, 325syldan 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  k  e.  ( ( 1 ... M )  \  {
j } ) )  ->  ( c `  k )  e.  RR )
327 elfzle1 11610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( c `  k )  e.  ( 0 ... ( P  -  1 ) )  ->  0  <_  ( c `  k
) )
328324, 327syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  k  e.  ( 0 ... M
) )  ->  0  <_  ( c `  k
) )
329323, 328syldan 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  k  e.  ( ( 1 ... M )  \  {
j } ) )  ->  0  <_  (
c `  k )
)
330320, 326, 329fsumge0 13611 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  0  <_  sum_ k  e.  ( ( 1 ... M ) 
\  { j } ) ( c `  k ) )
331330adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  j  e.  ( 0 ... M
) )  ->  0  <_ 
sum_ k  e.  ( ( 1 ... M
)  \  { j } ) ( c `
 k ) )
332320, 326fsumrecl 13558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  ->  sum_ k  e.  ( ( 1 ... M )  \  {
j } ) ( c `  k )  e.  RR )
333332adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  j  e.  ( 0 ... M
) )  ->  sum_ k  e.  ( ( 1 ... M )  \  {
j } ) ( c `  k )  e.  RR )
334281, 333addge01d 10057 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  j  e.  ( 0 ... M
) )  ->  (
0  <_  sum_ k  e.  ( ( 1 ... M )  \  {
j } ) ( c `  k )  <-> 
( c `  j
)  <_  ( (
c `  j )  +  sum_ k  e.  ( ( 1 ... M
)  \  { j } ) ( c `
 k ) ) ) )
335331, 334mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  j  e.  ( 0 ... M
) )  ->  (
c `  j )  <_  ( ( c `  j )  +  sum_ k  e.  ( (
1 ... M )  \  { j } ) ( c `  k
) ) )
336335ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) )  /\  j  e.  ( 0 ... M ) )  /\  -.  j  =  0 )  /\  -.  ( c `  j
)  =  0 )  ->  ( c `  j )  <_  (
( c `  j
)  +  sum_ k  e.  ( ( 1 ... M )  \  {
j } ) ( c `  k ) ) )
337279, 282, 312, 318, 336ltletrd 9653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) )  /\  j  e.  ( 0 ... M ) )  /\  -.  j  =  0 )  /\  -.  ( c `  j
)  =  0 )  ->  0  <  (
( c `  j
)  +  sum_ k  e.  ( ( 1 ... M )  \  {
j } ) ( c `  k ) ) )
338337, 311breqtrd 4391 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) )  /\  j  e.  ( 0 ... M ) )  /\  -.  j  =  0 )  /\  -.  ( c `  j
)  =  0 )  ->  0  <  sum_ k  e.  ( 1 ... M ) ( c `  k ) )
339278, 338elrpd 11174 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) )  /\  j  e.  ( 0 ... M ) )  /\  -.  j  =  0 )  /\  -.  ( c `  j
)  =  0 )  ->  sum_ k  e.  ( 1 ... M ) ( c `  k
)  e.  RR+ )
340270, 339ltaddrpd 11206 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) )  /\  j  e.  ( 0 ... M ) )  /\  -.  j  =  0 )  /\  -.  ( c `  j
)  =  0 )  ->  ( P  - 
1 )  <  (
( P  -  1 )  +  sum_ k  e.  ( 1 ... M
) ( c `  k ) ) )
341340adantlllr 31583 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  ( P  -  1 )  =  ( c `  0
) )  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  /\  -.  ( c `
 j )  =  0 )  ->  ( P  -  1 )  <  ( ( P  -  1 )  + 
sum_ k  e.  ( 1 ... M ) ( c `  k
) ) )
342 fveq2 5774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  =  k  ->  (
c `  j )  =  ( c `  k ) )
343342cbvsumv 13520 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  sum_ j  e.  ( 0 ... M
) ( c `  j )  =  sum_ k  e.  ( 0 ... M ) ( c `  k )
344343a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  ( P  -  1 )  =  ( c `  0
) )  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  /\  -.  ( c `
 j )  =  0 )  ->  sum_ j  e.  ( 0 ... M
) ( c `  j )  =  sum_ k  e.  ( 0 ... M ) ( c `  k ) )
34573ad5antr 731 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  ( P  -  1 )  =  ( c `  0
) )  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  /\  -.  ( c `
 j )  =  0 )  ->  M  e.  ( ZZ>= `  0 )
)
346 simp-5l 767 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  ( P  -  1 )  =  ( c ` 
0 ) )  /\  j  e.  ( 0 ... M ) )  /\  -.  j  =  0 )  /\  -.  ( c `  j
)  =  0 )  /\  k  e.  ( 0 ... M ) )  ->  ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) ) )
34774, 324sseldi 3415 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  k  e.  ( 0 ... M
) )  ->  (
c `  k )  e.  CC )
348346, 347sylancom 665 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  ( P  -  1 )  =  ( c ` 
0 ) )  /\  j  e.  ( 0 ... M ) )  /\  -.  j  =  0 )  /\  -.  ( c `  j
)  =  0 )  /\  k  e.  ( 0 ... M ) )  ->  ( c `  k )  e.  CC )
349 fveq2 5774 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k  =  0  ->  (
c `  k )  =  ( c ` 
0 ) )
350345, 348, 349fsum1p 13570 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  ( P  -  1 )  =  ( c `  0
) )  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  /\  -.  ( c `
 j )  =  0 )  ->  sum_ k  e.  ( 0 ... M
) ( c `  k )  =  ( ( c `  0
)  +  sum_ k  e.  ( ( 0  +  1 ) ... M
) ( c `  k ) ) )
351259ad4antlr 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  ( P  -  1 )  =  ( c `  0
) )  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  /\  -.  ( c `
 j )  =  0 )  ->  (
c `  0 )  =  ( P  - 
1 ) )
35286sumeq1i 13522 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  sum_ k  e.  ( ( 0  +  1 ) ... M
) ( c `  k )  =  sum_ k  e.  ( 1 ... M ) ( c `  k )
353352a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  ( P  -  1 )  =  ( c `  0
) )  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  /\  -.  ( c `
 j )  =  0 )  ->  sum_ k  e.  ( ( 0  +  1 ) ... M
) ( c `  k )  =  sum_ k  e.  ( 1 ... M ) ( c `  k ) )
354351, 353oveq12d 6214 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  ( P  -  1 )  =  ( c `  0
) )  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  /\  -.  ( c `
 j )  =  0 )  ->  (
( c `  0
)  +  sum_ k  e.  ( ( 0  +  1 ) ... M
) ( c `  k ) )  =  ( ( P  - 
1 )  +  sum_ k  e.  ( 1 ... M ) ( c `  k ) ) )
355344, 350, 3543eqtrrd 2428 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  ( P  -  1 )  =  ( c `  0
) )  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  /\  -.  ( c `
 j )  =  0 )  ->  (
( P  -  1 )  +  sum_ k  e.  ( 1 ... M
) ( c `  k ) )  = 
sum_ j  e.  ( 0 ... M ) ( c `  j
) )
356341, 355breqtrd 4391 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  ( P  -  1 )  =  ( c `  0
) )  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  /\  -.  ( c `
 j )  =  0 )  ->  ( P  -  1 )  <  sum_ j  e.  ( 0 ... M ) ( c `  j
) )
357269, 356gtned 9631 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  ( P  -  1 )  =  ( c `  0
) )  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  /\  -.  ( c `
 j )  =  0 )  ->  sum_ j  e.  ( 0 ... M
) ( c `  j )  =/=  ( P  -  1 ) )
358357neneqd 2584 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( (
ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  ( P  -  1 )  =  ( c `  0
) )  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  /\  -.  ( c `
 j )  =  0 )  ->  -.  sum_ j  e.  ( 0 ... M ) ( c `  j )  =  ( P  - 
1 ) )
359268, 358condan 792 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) )  /\  ( P  - 
1 )  =  ( c `  0 ) )  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  ->  ( c `  j )  =  0 )
360 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  j  e.  ( 0 ... M
) )
36133, 66sseldi 3415 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  if ( j  =  0 ,  ( P  - 
1 ) ,  0 )  e.  NN0 )
36267fvmpt2 5865 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( j  e.  ( 0 ... M )  /\  if ( j  =  0 ,  ( P  - 
1 ) ,  0 )  e.  NN0 )  ->  ( D `  j
)  =  if ( j  =  0 ,  ( P  -  1 ) ,  0 ) )
363360, 361, 362syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( D `  j )  =  if ( j  =  0 ,  ( P  -  1 ) ,  0 ) )
364363adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  ->  ( D `  j )  =  if ( j  =  0 ,  ( P  - 
1 ) ,  0 ) )
365 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  ->  -.  j  = 
0 )
366365iffalsed 3868 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  ->  if ( j  =  0 ,  ( P  -  1 ) ,  0 )  =  0 )
367364, 366eqtr2d 2424 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  ->  0  =  ( D `  j ) )
368367adantllr 716 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  j  e.  ( 0 ... M ) )  /\  -.  j  =  0 )  ->  0  =  ( D `  j ) )
369368adantllr 716 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) )  /\  ( P  - 
1 )  =  ( c `  0 ) )  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  ->  0  =  ( D `  j ) )
370359, 369eqtrd 2423 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  c  e.  ( C `
 ( P  - 
1 ) ) )  /\  ( P  - 
1 )  =  ( c `  0 ) )  /\  j  e.  ( 0 ... M
) )  /\  -.  j  =  0 )  ->  ( c `  j )  =  ( D `  j ) )
371267, 370pm2.61dan 789 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  ( P  -  1
)  =  ( c `
 0 ) )  /\  j  e.  ( 0 ... M ) )  ->  ( c `  j )  =  ( D `  j ) )
372252, 255, 371eqfnfvd 5886 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  c  e.  ( C `  ( P  -  1 ) ) )  /\  ( P  -  1 )  =  ( c ` 
0 ) )  -> 
c  =  D )
373236, 372sylanl2 649 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( P  -  1
) )  \  { D } ) )  /\  ( P  -  1
)  =  ( c `
 0 ) )  ->  c  =  D )
374 eldifsni 4070 . . . . . . . . . . . . . . . . . . . 20  |-  ( c  e.  ( ( C `
 ( P  - 
1 ) )  \  { D } )  -> 
c  =/=  D )
375374neneqd 2584 . . . . . . . . . . . . . . . . . . 19  |-  ( c  e.  ( ( C `
 ( P  - 
1 ) )  \  { D } )  ->  -.  c  =  D
)
376375ad2antlr 724 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  c  e.  ( ( C `  ( P  -  1
)