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

Theorem etransclem24 37390
Description:  P divides the I -th derivative of  F applied to  J. when  J  =  0 and  I is not equal to  P  -  1. This is the second part of case 2 proven in [Juillerat] p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
etransclem24.p  |-  ( ph  ->  P  e.  NN )
etransclem24.m  |-  ( ph  ->  M  e.  NN0 )
etransclem24.i  |-  ( ph  ->  I  e.  NN0 )
etransclem24.ip  |-  ( ph  ->  I  =/=  ( P  -  1 ) )
etransclem24.j  |-  ( ph  ->  J  =  0 )
etransclem24.c  |-  C  =  ( n  e.  NN0  |->  { c  e.  ( ( 0 ... n
)  ^m  ( 0 ... M ) )  |  sum_ j  e.  ( 0 ... M ) ( c `  j
)  =  n }
)
etransclem24.d  |-  ( ph  ->  D  e.  ( C `
 I ) )
Assertion
Ref Expression
etransclem24  |-  ( ph  ->  P  ||  ( ( ( ( ! `  I )  /  prod_ j  e.  ( 0 ... M ) ( ! `
 ( D `  j ) ) )  x.  ( if ( ( P  -  1 )  <  ( D `
 0 ) ,  0 ,  ( ( ( ! `  ( P  -  1 ) )  /  ( ! `
 ( ( P  -  1 )  -  ( D `  0 ) ) ) )  x.  ( J ^ (
( P  -  1 )  -  ( D `
 0 ) ) ) ) )  x. 
prod_ j  e.  (
1 ... M ) if ( P  <  ( D `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )  /  ( ! `  ( P  -  1 ) ) ) )
Distinct variable groups:    D, c,
j    I, c, n    j, J    M, c, j, n    P, j    ph, j, n
Allowed substitution hints:    ph( c)    C( j, n, c)    D( n)    P( n, c)    I( j)    J( n, c)

Proof of Theorem etransclem24
Dummy variables  A  k are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 etransclem24.d . . . . . . . 8  |-  ( ph  ->  D  e.  ( C `
 I ) )
2 etransclem24.c . . . . . . . . 9  |-  C  =  ( n  e.  NN0  |->  { c  e.  ( ( 0 ... n
)  ^m  ( 0 ... M ) )  |  sum_ j  e.  ( 0 ... M ) ( c `  j
)  =  n }
)
3 etransclem24.i . . . . . . . . 9  |-  ( ph  ->  I  e.  NN0 )
42, 3etransclem12 37378 . . . . . . . 8  |-  ( ph  ->  ( C `  I
)  =  { c  e.  ( ( 0 ... I )  ^m  ( 0 ... M
) )  |  sum_ j  e.  ( 0 ... M ) ( c `  j )  =  I } )
51, 4eleqtrd 2492 . . . . . . 7  |-  ( ph  ->  D  e.  { c  e.  ( ( 0 ... I )  ^m  ( 0 ... M
) )  |  sum_ j  e.  ( 0 ... M ) ( c `  j )  =  I } )
6 fveq1 5847 . . . . . . . . . 10  |-  ( c  =  D  ->  (
c `  j )  =  ( D `  j ) )
76sumeq2ad 36915 . . . . . . . . 9  |-  ( c  =  D  ->  sum_ j  e.  ( 0 ... M
) ( c `  j )  =  sum_ j  e.  ( 0 ... M ) ( D `  j ) )
87eqeq1d 2404 . . . . . . . 8  |-  ( c  =  D  ->  ( sum_ j  e.  ( 0 ... M ) ( c `  j )  =  I  <->  sum_ j  e.  ( 0 ... M
) ( D `  j )  =  I ) )
98elrab 3206 . . . . . . 7  |-  ( D  e.  { c  e.  ( ( 0 ... I )  ^m  (
0 ... M ) )  |  sum_ j  e.  ( 0 ... M ) ( c `  j
)  =  I }  <->  ( D  e.  ( ( 0 ... I )  ^m  ( 0 ... M ) )  /\  sum_ j  e.  ( 0 ... M ) ( D `  j )  =  I ) )
105, 9sylib 196 . . . . . 6  |-  ( ph  ->  ( D  e.  ( ( 0 ... I
)  ^m  ( 0 ... M ) )  /\  sum_ j  e.  ( 0 ... M ) ( D `  j
)  =  I ) )
1110simprd 461 . . . . 5  |-  ( ph  -> 
sum_ j  e.  ( 0 ... M ) ( D `  j
)  =  I )
1211ad2antrr 724 . . . 4  |-  ( ( ( ph  /\  ( D `  0 )  =  ( P  - 
1 ) )  /\  -.  E. k  e.  ( 1 ... M ) ( D `  k
)  e.  NN )  ->  sum_ j  e.  ( 0 ... M ) ( D `  j
)  =  I )
13 ralnex 2849 . . . . 5  |-  ( A. k  e.  ( 1 ... M )  -.  ( D `  k
)  e.  NN  <->  -.  E. k  e.  ( 1 ... M
) ( D `  k )  e.  NN )
14 etransclem24.m . . . . . . . . . . 11  |-  ( ph  ->  M  e.  NN0 )
15 nn0uz 11160 . . . . . . . . . . 11  |-  NN0  =  ( ZZ>= `  0 )
1614, 15syl6eleq 2500 . . . . . . . . . 10  |-  ( ph  ->  M  e.  ( ZZ>= ` 
0 ) )
1716ad2antrr 724 . . . . . . . . 9  |-  ( ( ( ph  /\  ( D `  0 )  =  ( P  - 
1 ) )  /\  A. k  e.  ( 1 ... M )  -.  ( D `  k
)  e.  NN )  ->  M  e.  (
ZZ>= `  0 ) )
18 fzsscn 36863 . . . . . . . . . . 11  |-  ( 0 ... I )  C_  CC
19 ssrab2 3523 . . . . . . . . . . . . . . 15  |-  { c  e.  ( ( 0 ... I )  ^m  ( 0 ... M
) )  |  sum_ j  e.  ( 0 ... M ) ( c `  j )  =  I }  C_  ( ( 0 ... I )  ^m  (
0 ... M ) )
204, 19syl6eqss 3491 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( C `  I
)  C_  ( (
0 ... I )  ^m  ( 0 ... M
) ) )
2120, 1sseldd 3442 . . . . . . . . . . . . 13  |-  ( ph  ->  D  e.  ( ( 0 ... I )  ^m  ( 0 ... M ) ) )
22 elmapi 7477 . . . . . . . . . . . . 13  |-  ( D  e.  ( ( 0 ... I )  ^m  ( 0 ... M
) )  ->  D : ( 0 ... M ) --> ( 0 ... I ) )
2321, 22syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  D : ( 0 ... M ) --> ( 0 ... I ) )
2423ffvelrnda 6008 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( D `  j )  e.  ( 0 ... I
) )
2518, 24sseldi 3439 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( D `  j )  e.  CC )
2625adant423 36782 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( D `  0 )  =  ( P  - 
1 ) )  /\  A. k  e.  ( 1 ... M )  -.  ( D `  k
)  e.  NN )  /\  j  e.  ( 0 ... M ) )  ->  ( D `  j )  e.  CC )
27 fveq2 5848 . . . . . . . . 9  |-  ( j  =  0  ->  ( D `  j )  =  ( D ` 
0 ) )
2817, 26, 27fsum1p 13717 . . . . . . . 8  |-  ( ( ( ph  /\  ( D `  0 )  =  ( P  - 
1 ) )  /\  A. k  e.  ( 1 ... M )  -.  ( D `  k
)  e.  NN )  ->  sum_ j  e.  ( 0 ... M ) ( D `  j
)  =  ( ( D `  0 )  +  sum_ j  e.  ( ( 0  +  1 ) ... M ) ( D `  j
) ) )
29 simplr 754 . . . . . . . . 9  |-  ( ( ( ph  /\  ( D `  0 )  =  ( P  - 
1 ) )  /\  A. k  e.  ( 1 ... M )  -.  ( D `  k
)  e.  NN )  ->  ( D ` 
0 )  =  ( P  -  1 ) )
30 0p1e1 10687 . . . . . . . . . . . . . 14  |-  ( 0  +  1 )  =  1
3130oveq1i 6287 . . . . . . . . . . . . 13  |-  ( ( 0  +  1 ) ... M )  =  ( 1 ... M
)
3231sumeq1i 13667 . . . . . . . . . . . 12  |-  sum_ j  e.  ( ( 0  +  1 ) ... M
) ( D `  j )  =  sum_ j  e.  ( 1 ... M ) ( D `  j )
3332a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  A. k  e.  ( 1 ... M
)  -.  ( D `
 k )  e.  NN )  ->  sum_ j  e.  ( ( 0  +  1 ) ... M
) ( D `  j )  =  sum_ j  e.  ( 1 ... M ) ( D `  j ) )
34 fveq2 5848 . . . . . . . . . . . . . . . . 17  |-  ( k  =  j  ->  ( D `  k )  =  ( D `  j ) )
3534eleq1d 2471 . . . . . . . . . . . . . . . 16  |-  ( k  =  j  ->  (
( D `  k
)  e.  NN  <->  ( D `  j )  e.  NN ) )
3635notbid 292 . . . . . . . . . . . . . . 15  |-  ( k  =  j  ->  ( -.  ( D `  k
)  e.  NN  <->  -.  ( D `  j )  e.  NN ) )
3736rspccva 3158 . . . . . . . . . . . . . 14  |-  ( ( A. k  e.  ( 1 ... M )  -.  ( D `  k )  e.  NN  /\  j  e.  ( 1 ... M ) )  ->  -.  ( D `  j )  e.  NN )
3837adantll 712 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  A. k  e.  ( 1 ... M )  -.  ( D `  k
)  e.  NN )  /\  j  e.  ( 1 ... M ) )  ->  -.  ( D `  j )  e.  NN )
39 fzssnn0 36871 . . . . . . . . . . . . . . . 16  |-  ( 0 ... I )  C_  NN0
40 fz1ssfz0 36859 . . . . . . . . . . . . . . . . . 18  |-  ( 1 ... M )  C_  ( 0 ... M
)
4140sseli 3437 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 1 ... M )  ->  j  e.  ( 0 ... M
) )
4241, 24sylan2 472 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( D `  j )  e.  ( 0 ... I
) )
4339, 42sseldi 3439 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  ( D `  j )  e.  NN0 )
44 elnn0 10837 . . . . . . . . . . . . . . 15  |-  ( ( D `  j )  e.  NN0  <->  ( ( D `
 j )  e.  NN  \/  ( D `
 j )  =  0 ) )
4543, 44sylib 196 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  (
( D `  j
)  e.  NN  \/  ( D `  j )  =  0 ) )
4645adantlr 713 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  A. k  e.  ( 1 ... M )  -.  ( D `  k
)  e.  NN )  /\  j  e.  ( 1 ... M ) )  ->  ( ( D `  j )  e.  NN  \/  ( D `
 j )  =  0 ) )
47 orel1 380 . . . . . . . . . . . . 13  |-  ( -.  ( D `  j
)  e.  NN  ->  ( ( ( D `  j )  e.  NN  \/  ( D `  j
)  =  0 )  ->  ( D `  j )  =  0 ) )
4838, 46, 47sylc 59 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  A. k  e.  ( 1 ... M )  -.  ( D `  k
)  e.  NN )  /\  j  e.  ( 1 ... M ) )  ->  ( D `  j )  =  0 )
4948sumeq2dv 13672 . . . . . . . . . . 11  |-  ( (
ph  /\  A. k  e.  ( 1 ... M
)  -.  ( D `
 k )  e.  NN )  ->  sum_ j  e.  ( 1 ... M
) ( D `  j )  =  sum_ j  e.  ( 1 ... M ) 0 )
50 fzfi 12121 . . . . . . . . . . . . 13  |-  ( 1 ... M )  e. 
Fin
5150olci 389 . . . . . . . . . . . 12  |-  ( ( 1 ... M ) 
C_  ( ZZ>= `  A
)  \/  ( 1 ... M )  e. 
Fin )
52 sumz 13691 . . . . . . . . . . . 12  |-  ( ( ( 1 ... M
)  C_  ( ZZ>= `  A )  \/  (
1 ... M )  e. 
Fin )  ->  sum_ j  e.  ( 1 ... M
) 0  =  0 )
5351, 52mp1i 13 . . . . . . . . . . 11  |-  ( (
ph  /\  A. k  e.  ( 1 ... M
)  -.  ( D `
 k )  e.  NN )  ->  sum_ j  e.  ( 1 ... M
) 0  =  0 )
5433, 49, 533eqtrd 2447 . . . . . . . . . 10  |-  ( (
ph  /\  A. k  e.  ( 1 ... M
)  -.  ( D `
 k )  e.  NN )  ->  sum_ j  e.  ( ( 0  +  1 ) ... M
) ( D `  j )  =  0 )
5554adantlr 713 . . . . . . . . 9  |-  ( ( ( ph  /\  ( D `  0 )  =  ( P  - 
1 ) )  /\  A. k  e.  ( 1 ... M )  -.  ( D `  k
)  e.  NN )  ->  sum_ j  e.  ( ( 0  +  1 ) ... M ) ( D `  j
)  =  0 )
5629, 55oveq12d 6295 . . . . . . . 8  |-  ( ( ( ph  /\  ( D `  0 )  =  ( P  - 
1 ) )  /\  A. k  e.  ( 1 ... M )  -.  ( D `  k
)  e.  NN )  ->  ( ( D `
 0 )  + 
sum_ j  e.  ( ( 0  +  1 ) ... M ) ( D `  j
) )  =  ( ( P  -  1 )  +  0 ) )
57 etransclem24.p . . . . . . . . . . . . 13  |-  ( ph  ->  P  e.  NN )
58 nnm1nn0 10877 . . . . . . . . . . . . 13  |-  ( P  e.  NN  ->  ( P  -  1 )  e.  NN0 )
5957, 58syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( P  -  1 )  e.  NN0 )
6059nn0red 10893 . . . . . . . . . . 11  |-  ( ph  ->  ( P  -  1 )  e.  RR )
6160recnd 9651 . . . . . . . . . 10  |-  ( ph  ->  ( P  -  1 )  e.  CC )
6261addid1d 9813 . . . . . . . . 9  |-  ( ph  ->  ( ( P  - 
1 )  +  0 )  =  ( P  -  1 ) )
6362ad2antrr 724 . . . . . . . 8  |-  ( ( ( ph  /\  ( D `  0 )  =  ( P  - 
1 ) )  /\  A. k  e.  ( 1 ... M )  -.  ( D `  k
)  e.  NN )  ->  ( ( P  -  1 )  +  0 )  =  ( P  -  1 ) )
6428, 56, 633eqtrd 2447 . . . . . . 7  |-  ( ( ( ph  /\  ( D `  0 )  =  ( P  - 
1 ) )  /\  A. k  e.  ( 1 ... M )  -.  ( D `  k
)  e.  NN )  ->  sum_ j  e.  ( 0 ... M ) ( D `  j
)  =  ( P  -  1 ) )
65 etransclem24.ip . . . . . . . . 9  |-  ( ph  ->  I  =/=  ( P  -  1 ) )
6665necomd 2674 . . . . . . . 8  |-  ( ph  ->  ( P  -  1 )  =/=  I )
6766ad2antrr 724 . . . . . . 7  |-  ( ( ( ph  /\  ( D `  0 )  =  ( P  - 
1 ) )  /\  A. k  e.  ( 1 ... M )  -.  ( D `  k
)  e.  NN )  ->  ( P  - 
1 )  =/=  I
)
6864, 67eqnetrd 2696 . . . . . 6  |-  ( ( ( ph  /\  ( D `  0 )  =  ( P  - 
1 ) )  /\  A. k  e.  ( 1 ... M )  -.  ( D `  k
)  e.  NN )  ->  sum_ j  e.  ( 0 ... M ) ( D `  j
)  =/=  I )
6968neneqd 2605 . . . . 5  |-  ( ( ( ph  /\  ( D `  0 )  =  ( P  - 
1 ) )  /\  A. k  e.  ( 1 ... M )  -.  ( D `  k
)  e.  NN )  ->  -.  sum_ j  e.  ( 0 ... M
) ( D `  j )  =  I )
7013, 69sylan2br 474 . . . 4  |-  ( ( ( ph  /\  ( D `  0 )  =  ( P  - 
1 ) )  /\  -.  E. k  e.  ( 1 ... M ) ( D `  k
)  e.  NN )  ->  -.  sum_ j  e.  ( 0 ... M
) ( D `  j )  =  I )
7112, 70condan 795 . . 3  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  E. k  e.  ( 1 ... M
) ( D `  k )  e.  NN )
7257nnzd 11006 . . . . . . . . 9  |-  ( ph  ->  P  e.  ZZ )
7311eqcomd 2410 . . . . . . . . . . . . 13  |-  ( ph  ->  I  =  sum_ j  e.  ( 0 ... M
) ( D `  j ) )
7473fveq2d 5852 . . . . . . . . . . . 12  |-  ( ph  ->  ( ! `  I
)  =  ( ! `
 sum_ j  e.  ( 0 ... M ) ( D `  j
) ) )
7574oveq1d 6292 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ! `  I )  /  prod_ j  e.  ( 0 ... M ) ( ! `
 ( D `  j ) ) )  =  ( ( ! `
 sum_ j  e.  ( 0 ... M ) ( D `  j
) )  /  prod_ j  e.  ( 0 ... M ) ( ! `
 ( D `  j ) ) ) )
76 nfcv 2564 . . . . . . . . . . . 12  |-  F/_ j D
77 fzfid 12122 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0 ... M
)  e.  Fin )
78 nn0ex 10841 . . . . . . . . . . . . . 14  |-  NN0  e.  _V
79 mapss 7498 . . . . . . . . . . . . . 14  |-  ( ( NN0  e.  _V  /\  ( 0 ... I
)  C_  NN0 )  -> 
( ( 0 ... I )  ^m  (
0 ... M ) ) 
C_  ( NN0  ^m  ( 0 ... M
) ) )
8078, 39, 79mp2an 670 . . . . . . . . . . . . 13  |-  ( ( 0 ... I )  ^m  ( 0 ... M ) )  C_  ( NN0  ^m  ( 0 ... M ) )
8180, 21sseldi 3439 . . . . . . . . . . . 12  |-  ( ph  ->  D  e.  ( NN0 
^m  ( 0 ... M ) ) )
8276, 77, 81mccl 36955 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ! `  sum_ j  e.  ( 0 ... M ) ( D `  j ) )  /  prod_ j  e.  ( 0 ... M
) ( ! `  ( D `  j ) ) )  e.  NN )
8375, 82eqeltrd 2490 . . . . . . . . . 10  |-  ( ph  ->  ( ( ! `  I )  /  prod_ j  e.  ( 0 ... M ) ( ! `
 ( D `  j ) ) )  e.  NN )
8483nnzd 11006 . . . . . . . . 9  |-  ( ph  ->  ( ( ! `  I )  /  prod_ j  e.  ( 0 ... M ) ( ! `
 ( D `  j ) ) )  e.  ZZ )
85 fzfid 12122 . . . . . . . . . 10  |-  ( ph  ->  ( 1 ... M
)  e.  Fin )
8657adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  P  e.  NN )
8723adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  D : ( 0 ... M ) --> ( 0 ... I ) )
8841adantl 464 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  j  e.  ( 0 ... M
) )
89 etransclem24.j . . . . . . . . . . . . 13  |-  ( ph  ->  J  =  0 )
90 0zd 10916 . . . . . . . . . . . . 13  |-  ( ph  ->  0  e.  ZZ )
9189, 90eqeltrd 2490 . . . . . . . . . . . 12  |-  ( ph  ->  J  e.  ZZ )
9291adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  J  e.  ZZ )
9386, 87, 88, 92etransclem3 37369 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  if ( P  <  ( D `
 j ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )  e.  ZZ )
9485, 93fprodzcl 13911 . . . . . . . . 9  |-  ( ph  ->  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )  e.  ZZ )
9572, 84, 943jca 1177 . . . . . . . 8  |-  ( ph  ->  ( P  e.  ZZ  /\  ( ( ! `  I )  /  prod_ j  e.  ( 0 ... M ) ( ! `
 ( D `  j ) ) )  e.  ZZ  /\  prod_ j  e.  ( 1 ... M ) if ( P  <  ( D `
 j ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )  e.  ZZ ) )
96953ad2ant1 1018 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  ->  ( P  e.  ZZ  /\  ( ( ! `  I )  /  prod_ j  e.  ( 0 ... M ) ( ! `  ( D `  j )
) )  e.  ZZ  /\ 
prod_ j  e.  (
1 ... M ) if ( P  <  ( D `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )  e.  ZZ ) )
9772adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  P  e.  ZZ )
9857adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  P  e.  NN )
9923adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  D : ( 0 ... M ) --> ( 0 ... I ) )
10040sseli 3437 . . . . . . . . . . . . 13  |-  ( k  e.  ( 1 ... M )  ->  k  e.  ( 0 ... M
) )
101100adantl 464 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  k  e.  ( 0 ... M
) )
10291adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  J  e.  ZZ )
10398, 99, 101, 102etransclem3 37369 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  if ( P  <  ( D `
 k ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  k ) ) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) )  e.  ZZ )
104 difss 3569 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... M ) 
\  { k } )  C_  ( 1 ... M )
105 ssfi 7774 . . . . . . . . . . . . . . 15  |-  ( ( ( 1 ... M
)  e.  Fin  /\  ( ( 1 ... M )  \  {
k } )  C_  ( 1 ... M
) )  ->  (
( 1 ... M
)  \  { k } )  e.  Fin )
10650, 104, 105mp2an 670 . . . . . . . . . . . . . 14  |-  ( ( 1 ... M ) 
\  { k } )  e.  Fin
107106a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 1 ... M )  \  {
k } )  e. 
Fin )
10857adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( ( 1 ... M )  \  {
k } ) )  ->  P  e.  NN )
10923adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( ( 1 ... M )  \  {
k } ) )  ->  D : ( 0 ... M ) --> ( 0 ... I
) )
110104, 40sstri 3450 . . . . . . . . . . . . . . . 16  |-  ( ( 1 ... M ) 
\  { k } )  C_  ( 0 ... M )
111110sseli 3437 . . . . . . . . . . . . . . 15  |-  ( j  e.  ( ( 1 ... M )  \  { k } )  ->  j  e.  ( 0 ... M ) )
112111adantl 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( ( 1 ... M )  \  {
k } ) )  ->  j  e.  ( 0 ... M ) )
11391adantr 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( ( 1 ... M )  \  {
k } ) )  ->  J  e.  ZZ )
114108, 109, 112, 113etransclem3 37369 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( ( 1 ... M )  \  {
k } ) )  ->  if ( P  <  ( D `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  j )
) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )  e.  ZZ )
115107, 114fprodzcl 13911 . . . . . . . . . . . 12  |-  ( ph  ->  prod_ j  e.  ( ( 1 ... M
)  \  { k } ) if ( P  <  ( D `
 j ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )  e.  ZZ )
116115adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  prod_ j  e.  ( ( 1 ... M )  \  { k } ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )  e.  ZZ )
11797, 103, 1163jca 1177 . . . . . . . . . 10  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  ( P  e.  ZZ  /\  if ( P  <  ( D `
 k ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  k ) ) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) )  e.  ZZ  /\ 
prod_ j  e.  (
( 1 ... M
)  \  { k } ) if ( P  <  ( D `
 j ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )  e.  ZZ ) )
1181173adant3 1017 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  ->  ( P  e.  ZZ  /\  if ( P  <  ( D `
 k ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  k ) ) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) )  e.  ZZ  /\ 
prod_ j  e.  (
( 1 ... M
)  \  { k } ) if ( P  <  ( D `
 j ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )  e.  ZZ ) )
119 dvds0 14206 . . . . . . . . . . . . . 14  |-  ( P  e.  ZZ  ->  P  ||  0 )
12072, 119syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  P  ||  0 )
121120adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  P  <  ( D `  k ) )  ->  P  ||  0
)
1221213ad2antl1 1159 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  P  <  ( D `  k )
)  ->  P  ||  0
)
123 iftrue 3890 . . . . . . . . . . . . 13  |-  ( P  <  ( D `  k )  ->  if ( P  <  ( D `
 k ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  k ) ) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) )  =  0 )
124123eqcomd 2410 . . . . . . . . . . . 12  |-  ( P  <  ( D `  k )  ->  0  =  if ( P  < 
( D `  k
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  k ) ) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) ) )
125124adantl 464 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  P  <  ( D `  k )
)  ->  0  =  if ( P  <  ( D `  k ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  k ) ) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) ) )
126122, 125breqtrd 4418 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  P  <  ( D `  k )
)  ->  P  ||  if ( P  <  ( D `
 k ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  k ) ) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) ) )
12797adantr 463 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  ->  P  e.  ZZ )
128 0zd 10916 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  0  e.  ZZ )
12999, 101ffvelrnd 6009 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  ( D `  k )  e.  ( 0 ... I
) )
130129elfzelzd 36868 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  ( D `  k )  e.  ZZ )
13197, 130zsubcld 11012 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  ( P  -  ( D `  k ) )  e.  ZZ )
132128, 97, 1313jca 1177 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  (
0  e.  ZZ  /\  P  e.  ZZ  /\  ( P  -  ( D `  k ) )  e.  ZZ ) )
133132adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
( 0  e.  ZZ  /\  P  e.  ZZ  /\  ( P  -  ( D `  k )
)  e.  ZZ ) )
134 fzssre 36867 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0 ... I )  C_  RR
135134, 129sseldi 3439 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  ( D `  k )  e.  RR )
136135adantr 463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
( D `  k
)  e.  RR )
137127zred 11007 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  ->  P  e.  RR )
138 simpr 459 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  ->  -.  P  <  ( D `
 k ) )
139136, 137, 138nltled 9766 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
( D `  k
)  <_  P )
140137, 136subge0d 10181 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
( 0  <_  ( P  -  ( D `  k ) )  <->  ( D `  k )  <_  P
) )
141139, 140mpbird 232 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
0  <_  ( P  -  ( D `  k ) ) )
142 elfzle1 11741 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( D `  k )  e.  ( 0 ... I )  ->  0  <_  ( D `  k
) )
143129, 142syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  0  <_  ( D `  k
) )
144143adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
0  <_  ( D `  k ) )
145137, 136subge02d 10183 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
( 0  <_  ( D `  k )  <->  ( P  -  ( D `
 k ) )  <_  P ) )
146144, 145mpbid 210 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
( P  -  ( D `  k )
)  <_  P )
147133, 141, 146jca32 533 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
( ( 0  e.  ZZ  /\  P  e.  ZZ  /\  ( P  -  ( D `  k ) )  e.  ZZ )  /\  (
0  <_  ( P  -  ( D `  k ) )  /\  ( P  -  ( D `  k )
)  <_  P )
) )
148 elfz2 11731 . . . . . . . . . . . . . . . . 17  |-  ( ( P  -  ( D `
 k ) )  e.  ( 0 ... P )  <->  ( (
0  e.  ZZ  /\  P  e.  ZZ  /\  ( P  -  ( D `  k ) )  e.  ZZ )  /\  (
0  <_  ( P  -  ( D `  k ) )  /\  ( P  -  ( D `  k )
)  <_  P )
) )
149147, 148sylibr 212 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
( P  -  ( D `  k )
)  e.  ( 0 ... P ) )
150 permnn 12446 . . . . . . . . . . . . . . . 16  |-  ( ( P  -  ( D `
 k ) )  e.  ( 0 ... P )  ->  (
( ! `  P
)  /  ( ! `
 ( P  -  ( D `  k ) ) ) )  e.  NN )
151149, 150syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
( ( ! `  P )  /  ( ! `  ( P  -  ( D `  k ) ) ) )  e.  NN )
152151nnzd 11006 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
( ( ! `  P )  /  ( ! `  ( P  -  ( D `  k ) ) ) )  e.  ZZ )
153101elfzelzd 36868 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  k  e.  ZZ )
154102, 153zsubcld 11012 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  ( J  -  k )  e.  ZZ )
155154adantr 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
( J  -  k
)  e.  ZZ )
156131adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
( P  -  ( D `  k )
)  e.  ZZ )
157 elnn0z 10917 . . . . . . . . . . . . . . . 16  |-  ( ( P  -  ( D `
 k ) )  e.  NN0  <->  ( ( P  -  ( D `  k ) )  e.  ZZ  /\  0  <_ 
( P  -  ( D `  k )
) ) )
158156, 141, 157sylanbrc 662 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
( P  -  ( D `  k )
)  e.  NN0 )
159 zexpcl 12223 . . . . . . . . . . . . . . 15  |-  ( ( ( J  -  k
)  e.  ZZ  /\  ( P  -  ( D `  k )
)  e.  NN0 )  ->  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) )  e.  ZZ )
160155, 158, 159syl2anc 659 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
( ( J  -  k ) ^ ( P  -  ( D `  k ) ) )  e.  ZZ )
161127, 152, 1603jca 1177 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
( P  e.  ZZ  /\  ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  k ) ) ) )  e.  ZZ  /\  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) )  e.  ZZ ) )
1621613adantl3 1155 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  -.  P  < 
( D `  k
) )  ->  ( P  e.  ZZ  /\  (
( ! `  P
)  /  ( ! `
 ( P  -  ( D `  k ) ) ) )  e.  ZZ  /\  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) )  e.  ZZ ) )
1631273adantl3 1155 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  -.  P  < 
( D `  k
) )  ->  P  e.  ZZ )
16459nn0zd 11005 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( P  -  1 )  e.  ZZ )
165164adantr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  ( P  -  1 )  e.  ZZ )
166128, 165, 1313jca 1177 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  k  e.  ( 1 ... M
) )  ->  (
0  e.  ZZ  /\  ( P  -  1
)  e.  ZZ  /\  ( P  -  ( D `  k )
)  e.  ZZ ) )
1671663adant3 1017 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  ->  ( 0  e.  ZZ  /\  ( P  -  1 )  e.  ZZ  /\  ( P  -  ( D `  k ) )  e.  ZZ ) )
168167adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  -.  P  < 
( D `  k
) )  ->  (
0  e.  ZZ  /\  ( P  -  1
)  e.  ZZ  /\  ( P  -  ( D `  k )
)  e.  ZZ ) )
1691413adantl3 1155 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  -.  P  < 
( D `  k
) )  ->  0  <_  ( P  -  ( D `  k )
) )
170 1red 9640 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( D `  k )  e.  NN )  ->  1  e.  RR )
171 nnre 10582 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( D `  k )  e.  NN  ->  ( D `  k )  e.  RR )
172171adantl 464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( D `  k )  e.  NN )  ->  ( D `  k )  e.  RR )
17357nnred 10590 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  P  e.  RR )
174173adantr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( D `  k )  e.  NN )  ->  P  e.  RR )
175 nnge1 10601 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( D `  k )  e.  NN  ->  1  <_  ( D `  k
) )
176175adantl 464 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( D `  k )  e.  NN )  ->  1  <_  ( D `  k )
)
177170, 172, 174, 176lesub2dd 10208 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( D `  k )  e.  NN )  ->  ( P  -  ( D `  k ) )  <_  ( P  -  1 ) )
1781773adant2 1016 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  ->  ( P  -  ( D `  k ) )  <_  ( P  -  1 ) )
179178adantr 463 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  -.  P  < 
( D `  k
) )  ->  ( P  -  ( D `  k ) )  <_ 
( P  -  1 ) )
180168, 169, 179jca32 533 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  -.  P  < 
( D `  k
) )  ->  (
( 0  e.  ZZ  /\  ( P  -  1 )  e.  ZZ  /\  ( P  -  ( D `  k )
)  e.  ZZ )  /\  ( 0  <_ 
( P  -  ( D `  k )
)  /\  ( P  -  ( D `  k ) )  <_ 
( P  -  1 ) ) ) )
181 elfz2 11731 . . . . . . . . . . . . . . . . 17  |-  ( ( P  -  ( D `
 k ) )  e.  ( 0 ... ( P  -  1 ) )  <->  ( (
0  e.  ZZ  /\  ( P  -  1
)  e.  ZZ  /\  ( P  -  ( D `  k )
)  e.  ZZ )  /\  ( 0  <_ 
( P  -  ( D `  k )
)  /\  ( P  -  ( D `  k ) )  <_ 
( P  -  1 ) ) ) )
182180, 181sylibr 212 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  -.  P  < 
( D `  k
) )  ->  ( P  -  ( D `  k ) )  e.  ( 0 ... ( P  -  1 ) ) )
183 permnn 12446 . . . . . . . . . . . . . . . 16  |-  ( ( P  -  ( D `
 k ) )  e.  ( 0 ... ( P  -  1 ) )  ->  (
( ! `  ( P  -  1 ) )  /  ( ! `
 ( P  -  ( D `  k ) ) ) )  e.  NN )
184182, 183syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  -.  P  < 
( D `  k
) )  ->  (
( ! `  ( P  -  1 ) )  /  ( ! `
 ( P  -  ( D `  k ) ) ) )  e.  NN )
185184nnzd 11006 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  -.  P  < 
( D `  k
) )  ->  (
( ! `  ( P  -  1 ) )  /  ( ! `
 ( P  -  ( D `  k ) ) ) )  e.  ZZ )
186 dvdsmul1 14212 . . . . . . . . . . . . . 14  |-  ( ( P  e.  ZZ  /\  ( ( ! `  ( P  -  1
) )  /  ( ! `  ( P  -  ( D `  k ) ) ) )  e.  ZZ )  ->  P  ||  ( P  x.  ( ( ! `  ( P  -  1 ) )  /  ( ! `  ( P  -  ( D `  k )
) ) ) ) )
187163, 185, 186syl2anc 659 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  -.  P  < 
( D `  k
) )  ->  P  ||  ( P  x.  (
( ! `  ( P  -  1 ) )  /  ( ! `
 ( P  -  ( D `  k ) ) ) ) ) )
18857nncnd 10591 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  P  e.  CC )
189 1cnd 9641 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  1  e.  CC )
190188, 189npcand 9970 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( P  - 
1 )  +  1 )  =  P )
191190eqcomd 2410 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  P  =  ( ( P  -  1 )  +  1 ) )
192191fveq2d 5852 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ! `  P
)  =  ( ! `
 ( ( P  -  1 )  +  1 ) ) )
193 facp1 12400 . . . . . . . . . . . . . . . . . . 19  |-  ( ( P  -  1 )  e.  NN0  ->  ( ! `
 ( ( P  -  1 )  +  1 ) )  =  ( ( ! `  ( P  -  1
) )  x.  (
( P  -  1 )  +  1 ) ) )
19459, 193syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ! `  (
( P  -  1 )  +  1 ) )  =  ( ( ! `  ( P  -  1 ) )  x.  ( ( P  -  1 )  +  1 ) ) )
195190oveq2d 6293 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ! `  ( P  -  1
) )  x.  (
( P  -  1 )  +  1 ) )  =  ( ( ! `  ( P  -  1 ) )  x.  P ) )
19659faccld 36865 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ! `  ( P  -  1 ) )  e.  NN )
197196nncnd 10591 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ! `  ( P  -  1 ) )  e.  CC )
198197, 188mulcomd 9646 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ! `  ( P  -  1
) )  x.  P
)  =  ( P  x.  ( ! `  ( P  -  1
) ) ) )
199195, 198eqtrd 2443 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ! `  ( P  -  1
) )  x.  (
( P  -  1 )  +  1 ) )  =  ( P  x.  ( ! `  ( P  -  1
) ) ) )
200192, 194, 1993eqtrd 2447 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ! `  P
)  =  ( P  x.  ( ! `  ( P  -  1
) ) ) )
201200oveq1d 6292 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  k ) ) ) )  =  ( ( P  x.  ( ! `
 ( P  - 
1 ) ) )  /  ( ! `  ( P  -  ( D `  k )
) ) ) )
202201adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  -.  P  <  ( D `  k
) )  ->  (
( ! `  P
)  /  ( ! `
 ( P  -  ( D `  k ) ) ) )  =  ( ( P  x.  ( ! `  ( P  -  1 ) ) )  /  ( ! `
 ( P  -  ( D `  k ) ) ) ) )
2032023ad2antl1 1159 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  -.  P  < 
( D `  k
) )  ->  (
( ! `  P
)  /  ( ! `
 ( P  -  ( D `  k ) ) ) )  =  ( ( P  x.  ( ! `  ( P  -  1 ) ) )  /  ( ! `
 ( P  -  ( D `  k ) ) ) ) )
204188ad2antrr 724 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  ->  P  e.  CC )
205197ad2antrr 724 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
( ! `  ( P  -  1 ) )  e.  CC )
206158faccld 36865 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
( ! `  ( P  -  ( D `  k ) ) )  e.  NN )
207206nncnd 10591 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
( ! `  ( P  -  ( D `  k ) ) )  e.  CC )
208206nnne0d 10620 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
( ! `  ( P  -  ( D `  k ) ) )  =/=  0 )
209204, 205, 207, 208divassd 10395 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
) )  /\  -.  P  <  ( D `  k ) )  -> 
( ( P  x.  ( ! `  ( P  -  1 ) ) )  /  ( ! `
 ( P  -  ( D `  k ) ) ) )  =  ( P  x.  (
( ! `  ( P  -  1 ) )  /  ( ! `
 ( P  -  ( D `  k ) ) ) ) ) )
2102093adantl3 1155 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  -.  P  < 
( D `  k
) )  ->  (
( P  x.  ( ! `  ( P  -  1 ) ) )  /  ( ! `
 ( P  -  ( D `  k ) ) ) )  =  ( P  x.  (
( ! `  ( P  -  1 ) )  /  ( ! `
 ( P  -  ( D `  k ) ) ) ) ) )
211203, 210eqtr2d 2444 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  -.  P  < 
( D `  k
) )  ->  ( P  x.  ( ( ! `  ( P  -  1 ) )  /  ( ! `  ( P  -  ( D `  k )
) ) ) )  =  ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  k ) ) ) ) )
212187, 211breqtrd 4418 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  -.  P  < 
( D `  k
) )  ->  P  ||  ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  k ) ) ) ) )
213 dvdsmultr1 14226 . . . . . . . . . . . 12  |-  ( ( P  e.  ZZ  /\  ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  k ) ) ) )  e.  ZZ  /\  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) )  e.  ZZ )  -> 
( P  ||  (
( ! `  P
)  /  ( ! `
 ( P  -  ( D `  k ) ) ) )  ->  P  ||  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  k )
) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) ) )
214162, 212, 213sylc 59 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  -.  P  < 
( D `  k
) )  ->  P  ||  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  k ) ) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) )
215 iffalse 3893 . . . . . . . . . . . 12  |-  ( -.  P  <  ( D `
 k )  ->  if ( P  <  ( D `  k ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  k ) ) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) )  =  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  k )
) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) )
216215adantl 464 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  -.  P  < 
( D `  k
) )  ->  if ( P  <  ( D `
 k ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  k ) ) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) )  =  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  k ) ) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) )
217214, 216breqtrrd 4420 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  -.  P  < 
( D `  k
) )  ->  P  ||  if ( P  < 
( D `  k
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  k ) ) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) ) )
218126, 217pm2.61dan 792 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  ->  P  ||  if ( P  <  ( D `
 k ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  k ) ) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) ) )
219 dvdsmultr1 14226 . . . . . . . . 9  |-  ( ( P  e.  ZZ  /\  if ( P  <  ( D `  k ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  k ) ) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) )  e.  ZZ  /\  prod_ j  e.  ( ( 1 ... M )  \  { k } ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )  e.  ZZ )  -> 
( P  ||  if ( P  <  ( D `
 k ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  k ) ) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) )  ->  P  ||  ( if ( P  <  ( D `  k ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  k )
) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) )  x.  prod_ j  e.  ( ( 1 ... M )  \  { k } ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) ) )
220118, 218, 219sylc 59 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  ->  P  ||  ( if ( P  <  ( D `  k ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  k ) ) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) )  x.  prod_ j  e.  ( ( 1 ... M
)  \  { k } ) if ( P  <  ( D `
 j ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )
221 fzfid 12122 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  ->  ( 1 ... M )  e.  Fin )
22293zcnd 11008 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 1 ... M
) )  ->  if ( P  <  ( D `
 j ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )  e.  CC )
2232223ad2antl1 1159 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  j  e.  ( 1 ... M ) )  ->  if ( P  <  ( D `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  j )
) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )  e.  CC )
224 simp2 998 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  ->  k  e.  ( 1 ... M ) )
225 fveq2 5848 . . . . . . . . . . . 12  |-  ( j  =  k  ->  ( D `  j )  =  ( D `  k ) )
226225breq2d 4406 . . . . . . . . . . 11  |-  ( j  =  k  ->  ( P  <  ( D `  j )  <->  P  <  ( D `  k ) ) )
227225oveq2d 6293 . . . . . . . . . . . . . 14  |-  ( j  =  k  ->  ( P  -  ( D `  j ) )  =  ( P  -  ( D `  k )
) )
228227fveq2d 5852 . . . . . . . . . . . . 13  |-  ( j  =  k  ->  ( ! `  ( P  -  ( D `  j ) ) )  =  ( ! `  ( P  -  ( D `  k )
) ) )
229228oveq2d 6293 . . . . . . . . . . . 12  |-  ( j  =  k  ->  (
( ! `  P
)  /  ( ! `
 ( P  -  ( D `  j ) ) ) )  =  ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  k ) ) ) ) )
230 oveq2 6285 . . . . . . . . . . . . 13  |-  ( j  =  k  ->  ( J  -  j )  =  ( J  -  k ) )
231230, 227oveq12d 6295 . . . . . . . . . . . 12  |-  ( j  =  k  ->  (
( J  -  j
) ^ ( P  -  ( D `  j ) ) )  =  ( ( J  -  k ) ^
( P  -  ( D `  k )
) ) )
232229, 231oveq12d 6295 . . . . . . . . . . 11  |-  ( j  =  k  ->  (
( ( ! `  P )  /  ( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) )  =  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  k ) ) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) )
233226, 232ifbieq2d 3909 . . . . . . . . . 10  |-  ( j  =  k  ->  if ( P  <  ( D `
 j ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )  =  if ( P  <  ( D `  k ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  k ) ) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) ) )
234233adantl 464 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  /\  j  =  k )  ->  if ( P  <  ( D `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  j )
) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )  =  if ( P  <  ( D `  k ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  k ) ) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) ) )
235221, 223, 224, 234fprodsplit1 36948 . . . . . . . 8  |-  ( (
ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  ->  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )  =  ( if ( P  <  ( D `
 k ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  k ) ) ) )  x.  ( ( J  -  k ) ^ ( P  -  ( D `  k ) ) ) ) )  x.  prod_ j  e.  ( ( 1 ... M )  \  { k } ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )
236220, 235breqtrrd 4420 . . . . . . 7  |-  ( (
ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  ->  P  ||  prod_ j  e.  ( 1 ... M ) if ( P  <  ( D `
 j ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) )
237 dvdsmultr2 14228 . . . . . . 7  |-  ( ( P  e.  ZZ  /\  ( ( ! `  I )  /  prod_ j  e.  ( 0 ... M ) ( ! `
 ( D `  j ) ) )  e.  ZZ  /\  prod_ j  e.  ( 1 ... M ) if ( P  <  ( D `
 j ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )  e.  ZZ )  ->  ( P  ||  prod_ j  e.  ( 1 ... M ) if ( P  <  ( D `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )  ->  P  ||  (
( ( ! `  I )  /  prod_ j  e.  ( 0 ... M ) ( ! `
 ( D `  j ) ) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) ) )
23896, 236, 237sylc 59 . . . . . 6  |-  ( (
ph  /\  k  e.  ( 1 ... M
)  /\  ( D `  k )  e.  NN )  ->  P  ||  (
( ( ! `  I )  /  prod_ j  e.  ( 0 ... M ) ( ! `
 ( D `  j ) ) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )
2392383adant1r 1223 . . . . 5  |-  ( ( ( ph  /\  ( D `  0 )  =  ( P  - 
1 ) )  /\  k  e.  ( 1 ... M )  /\  ( D `  k )  e.  NN )  ->  P  ||  ( ( ( ! `  I )  /  prod_ j  e.  ( 0 ... M ) ( ! `  ( D `  j )
) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  <  ( D `
 j ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )
240 simpr 459 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  ( D `  0 )  =  ( P  - 
1 ) )
241 eluzfz1 11745 . . . . . . . . . . . . . . . . . . 19  |-  ( M  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... M
) )
24216, 241syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  0  e.  ( 0 ... M ) )
24323, 242ffvelrnd 6009 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D `  0
)  e.  ( 0 ... I ) )
244134, 243sseldi 3439 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( D `  0
)  e.  RR )
245244adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  ( D `  0 )  e.  RR )
24660adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  ( P  -  1 )  e.  RR )
247245, 246lttri3d 9756 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  (
( D `  0
)  =  ( P  -  1 )  <->  ( -.  ( D `  0 )  <  ( P  - 
1 )  /\  -.  ( P  -  1
)  <  ( D `  0 ) ) ) )
248240, 247mpbid 210 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  ( -.  ( D `  0
)  <  ( P  -  1 )  /\  -.  ( P  -  1 )  <  ( D `
 0 ) ) )
249248simprd 461 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  -.  ( P  -  1
)  <  ( D `  0 ) )
250249iffalsed 3895 . . . . . . . . . . 11  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  if ( ( P  - 
1 )  <  ( D `  0 ) ,  0 ,  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( D ` 
0 ) ) ) )  x.  ( J ^ ( ( P  -  1 )  -  ( D `  0 ) ) ) ) )  =  ( ( ( ! `  ( P  -  1 ) )  /  ( ! `  ( ( P  - 
1 )  -  ( D `  0 )
) ) )  x.  ( J ^ (
( P  -  1 )  -  ( D `
 0 ) ) ) ) )
251 oveq2 6285 . . . . . . . . . . . . . . . . 17  |-  ( ( D `  0 )  =  ( P  - 
1 )  ->  (
( P  -  1 )  -  ( D `
 0 ) )  =  ( ( P  -  1 )  -  ( P  -  1
) ) )
25261subidd 9954 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( P  - 
1 )  -  ( P  -  1 ) )  =  0 )
253251, 252sylan9eqr 2465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  (
( P  -  1 )  -  ( D `
 0 ) )  =  0 )
254253fveq2d 5852 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  ( ! `  ( ( P  -  1 )  -  ( D ` 
0 ) ) )  =  ( ! ` 
0 ) )
255 fac0 12398 . . . . . . . . . . . . . . 15  |-  ( ! `
 0 )  =  1
256254, 255syl6eq 2459 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  ( ! `  ( ( P  -  1 )  -  ( D ` 
0 ) ) )  =  1 )
257256oveq2d 6293 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  (
( ! `  ( P  -  1 ) )  /  ( ! `
 ( ( P  -  1 )  -  ( D `  0 ) ) ) )  =  ( ( ! `  ( P  -  1
) )  /  1
) )
258197div1d 10352 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ! `  ( P  -  1
) )  /  1
)  =  ( ! `
 ( P  - 
1 ) ) )
259258adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  (
( ! `  ( P  -  1 ) )  /  1 )  =  ( ! `  ( P  -  1
) ) )
260257, 259eqtrd 2443 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  (
( ! `  ( P  -  1 ) )  /  ( ! `
 ( ( P  -  1 )  -  ( D `  0 ) ) ) )  =  ( ! `  ( P  -  1 ) ) )
261253oveq2d 6293 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  ( J ^ ( ( P  -  1 )  -  ( D `  0 ) ) )  =  ( J ^ 0 ) )
26291zcnd 11008 . . . . . . . . . . . . . . 15  |-  ( ph  ->  J  e.  CC )
263262exp0d 12346 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( J ^ 0 )  =  1 )
264263adantr 463 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  ( J ^ 0 )  =  1 )
265261, 264eqtrd 2443 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  ( J ^ ( ( P  -  1 )  -  ( D `  0 ) ) )  =  1 )
266260, 265oveq12d 6295 . . . . . . . . . . 11  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  (
( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( D ` 
0 ) ) ) )  x.  ( J ^ ( ( P  -  1 )  -  ( D `  0 ) ) ) )  =  ( ( ! `  ( P  -  1
) )  x.  1 ) )
267197mulid1d 9642 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ! `  ( P  -  1
) )  x.  1 )  =  ( ! `
 ( P  - 
1 ) ) )
268267adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  (
( ! `  ( P  -  1 ) )  x.  1 )  =  ( ! `  ( P  -  1
) ) )
269250, 266, 2683eqtrd 2447 . . . . . . . . . 10  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  if ( ( P  - 
1 )  <  ( D `  0 ) ,  0 ,  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( D ` 
0 ) ) ) )  x.  ( J ^ ( ( P  -  1 )  -  ( D `  0 ) ) ) ) )  =  ( ! `  ( P  -  1
) ) )
270269oveq1d 6292 . . . . . . . . 9  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  ( if ( ( P  - 
1 )  <  ( D `  0 ) ,  0 ,  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( D ` 
0 ) ) ) )  x.  ( J ^ ( ( P  -  1 )  -  ( D `  0 ) ) ) ) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) )  =  ( ( ! `  ( P  -  1 ) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )
271270oveq2d 6293 . . . . . . . 8  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  (
( ( ! `  I )  /  prod_ j  e.  ( 0 ... M ) ( ! `
 ( D `  j ) ) )  x.  ( if ( ( P  -  1 )  <  ( D `
 0 ) ,  0 ,  ( ( ( ! `  ( P  -  1 ) )  /  ( ! `
 ( ( P  -  1 )  -  ( D `  0 ) ) ) )  x.  ( J ^ (
( P  -  1 )  -  ( D `
 0 ) ) ) ) )  x. 
prod_ j  e.  (
1 ... M ) if ( P  <  ( D `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )  =  ( ( ( ! `  I )  /  prod_ j  e.  ( 0 ... M ) ( ! `
 ( D `  j ) ) )  x.  ( ( ! `
 ( P  - 
1 ) )  x. 
prod_ j  e.  (
1 ... M ) if ( P  <  ( D `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) ) )
272271oveq1d 6292 . . . . . . 7  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  (
( ( ( ! `
 I )  /  prod_ j  e.  ( 0 ... M ) ( ! `  ( D `
 j ) ) )  x.  ( if ( ( P  - 
1 )  <  ( D `  0 ) ,  0 ,  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( D ` 
0 ) ) ) )  x.  ( J ^ ( ( P  -  1 )  -  ( D `  0 ) ) ) ) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )  /  ( ! `  ( P  -  1 ) ) )  =  ( ( ( ( ! `  I )  /  prod_ j  e.  ( 0 ... M ) ( ! `
 ( D `  j ) ) )  x.  ( ( ! `
 ( P  - 
1 ) )  x. 
prod_ j  e.  (
1 ... M ) if ( P  <  ( D `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )  /  ( ! `  ( P  -  1 ) ) ) )
27383nncnd 10591 . . . . . . . . 9  |-  ( ph  ->  ( ( ! `  I )  /  prod_ j  e.  ( 0 ... M ) ( ! `
 ( D `  j ) ) )  e.  CC )
27494zcnd 11008 . . . . . . . . . 10  |-  ( ph  ->  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) )  e.  CC )
275197, 274mulcld 9645 . . . . . . . . 9  |-  ( ph  ->  ( ( ! `  ( P  -  1
) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  <  ( D `
 j ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) )  e.  CC )
276196nnne0d 10620 . . . . . . . . 9  |-  ( ph  ->  ( ! `  ( P  -  1 ) )  =/=  0 )
277273, 275, 197, 276divassd 10395 . . . . . . . 8  |-  ( ph  ->  ( ( ( ( ! `  I )  /  prod_ j  e.  ( 0 ... M ) ( ! `  ( D `  j )
) )  x.  (
( ! `  ( P  -  1 ) )  x.  prod_ j  e.  ( 1 ... M
) if ( P  <  ( D `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  j )
) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )  /  ( ! `  ( P  -  1
) ) )  =  ( ( ( ! `
 I )  /  prod_ j  e.  ( 0 ... M ) ( ! `  ( D `
 j ) ) )  x.  ( ( ( ! `  ( P  -  1 ) )  x.  prod_ j  e.  ( 1 ... M
) if ( P  <  ( D `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  j )
) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) )  / 
( ! `  ( P  -  1 ) ) ) ) )
278277adantr 463 . . . . . . 7  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  (
( ( ( ! `
 I )  /  prod_ j  e.  ( 0 ... M ) ( ! `  ( D `
 j ) ) )  x.  ( ( ! `  ( P  -  1 ) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )  /  ( ! `  ( P  -  1 ) ) )  =  ( ( ( ! `  I
)  /  prod_ j  e.  ( 0 ... M
) ( ! `  ( D `  j ) ) )  x.  (
( ( ! `  ( P  -  1
) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  <  ( D `
 j ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) )  / 
( ! `  ( P  -  1 ) ) ) ) )
279274, 197, 276divcan3d 10365 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ! `
 ( P  - 
1 ) )  x. 
prod_ j  e.  (
1 ... M ) if ( P  <  ( D `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) )  /  ( ! `
 ( P  - 
1 ) ) )  =  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) )
280279oveq2d 6293 . . . . . . . 8  |-  ( ph  ->  ( ( ( ! `
 I )  /  prod_ j  e.  ( 0 ... M ) ( ! `  ( D `
 j ) ) )  x.  ( ( ( ! `  ( P  -  1 ) )  x.  prod_ j  e.  ( 1 ... M
) if ( P  <  ( D `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  j )
) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) )  / 
( ! `  ( P  -  1 ) ) ) )  =  ( ( ( ! `
 I )  /  prod_ j  e.  ( 0 ... M ) ( ! `  ( D `
 j ) ) )  x.  prod_ j  e.  ( 1 ... M
) if ( P  <  ( D `  j ) ,  0 ,  ( ( ( ! `  P )  /  ( ! `  ( P  -  ( D `  j )
) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )
281280adantr 463 . . . . . . 7  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  (
( ( ! `  I )  /  prod_ j  e.  ( 0 ... M ) ( ! `
 ( D `  j ) ) )  x.  ( ( ( ! `  ( P  -  1 ) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) )  /  ( ! `
 ( P  - 
1 ) ) ) )  =  ( ( ( ! `  I
)  /  prod_ j  e.  ( 0 ... M
) ( ! `  ( D `  j ) ) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  <  ( D `
 j ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )
282272, 278, 2813eqtrd 2447 . . . . . 6  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  (
( ( ( ! `
 I )  /  prod_ j  e.  ( 0 ... M ) ( ! `  ( D `
 j ) ) )  x.  ( if ( ( P  - 
1 )  <  ( D `  0 ) ,  0 ,  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( D ` 
0 ) ) ) )  x.  ( J ^ ( ( P  -  1 )  -  ( D `  0 ) ) ) ) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )  /  ( ! `  ( P  -  1 ) ) )  =  ( ( ( ! `  I
)  /  prod_ j  e.  ( 0 ... M
) ( ! `  ( D `  j ) ) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  <  ( D `
 j ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )
2832823ad2ant1 1018 . . . . 5  |-  ( ( ( ph  /\  ( D `  0 )  =  ( P  - 
1 ) )  /\  k  e.  ( 1 ... M )  /\  ( D `  k )  e.  NN )  -> 
( ( ( ( ! `  I )  /  prod_ j  e.  ( 0 ... M ) ( ! `  ( D `  j )
) )  x.  ( if ( ( P  - 
1 )  <  ( D `  0 ) ,  0 ,  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( D ` 
0 ) ) ) )  x.  ( J ^ ( ( P  -  1 )  -  ( D `  0 ) ) ) ) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )  /  ( ! `  ( P  -  1 ) ) )  =  ( ( ( ! `  I
)  /  prod_ j  e.  ( 0 ... M
) ( ! `  ( D `  j ) ) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  <  ( D `
 j ) ,  0 ,  ( ( ( ! `  P
)  /  ( ! `
 ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )
284239, 283breqtrrd 4420 . . . 4  |-  ( ( ( ph  /\  ( D `  0 )  =  ( P  - 
1 ) )  /\  k  e.  ( 1 ... M )  /\  ( D `  k )  e.  NN )  ->  P  ||  ( ( ( ( ! `  I
)  /  prod_ j  e.  ( 0 ... M
) ( ! `  ( D `  j ) ) )  x.  ( if ( ( P  - 
1 )  <  ( D `  0 ) ,  0 ,  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( D ` 
0 ) ) ) )  x.  ( J ^ ( ( P  -  1 )  -  ( D `  0 ) ) ) ) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )  /  ( ! `  ( P  -  1 ) ) ) )
285284rexlimdv3a 2897 . . 3  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  ( E. k  e.  (
1 ... M ) ( D `  k )  e.  NN  ->  P  ||  ( ( ( ( ! `  I )  /  prod_ j  e.  ( 0 ... M ) ( ! `  ( D `  j )
) )  x.  ( if ( ( P  - 
1 )  <  ( D `  0 ) ,  0 ,  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( D ` 
0 ) ) ) )  x.  ( J ^ ( ( P  -  1 )  -  ( D `  0 ) ) ) ) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )  /  ( ! `  ( P  -  1 ) ) ) ) )
28671, 285mpd 15 . 2  |-  ( (
ph  /\  ( D `  0 )  =  ( P  -  1 ) )  ->  P  ||  ( ( ( ( ! `  I )  /  prod_ j  e.  ( 0 ... M ) ( ! `  ( D `  j )
) )  x.  ( if ( ( P  - 
1 )  <  ( D `  0 ) ,  0 ,  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( D ` 
0 ) ) ) )  x.  ( J ^ ( ( P  -  1 )  -  ( D `  0 ) ) ) ) )  x.  prod_ j  e.  ( 1 ... M ) if ( P  < 
( D `  j
) ,  0 ,  ( ( ( ! `
 P )  / 
( ! `  ( P  -  ( D `  j ) ) ) )  x.  ( ( J  -  j ) ^ ( P  -  ( D `  j ) ) ) ) ) ) )  /  ( ! `  ( P  -  1 ) ) ) )
287120adantr 463 . . 3  |-  ( (
ph  /\  ( D `  0 )  =/=  ( P  -  1 ) )  ->  P  ||  0 )
288 simpr 459 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( D `  0 )  =/=  ( P  -  1 ) )  /\  ( P  -  1 )  <  ( D ` 
0 ) )  -> 
( P  -  1 )  <  ( D `
 0 ) )
289288iftrued 3892 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( D `  0 )  =/=  ( P  -  1 ) )  /\  ( P  -  1 )  <  ( D ` 
0 ) )  ->  if ( ( P  - 
1 )  <  ( D `  0 ) ,  0 ,  ( ( ( ! `  ( P  -  1
) )  /  ( ! `  ( ( P  -  1 )  -  ( D ` 
0 ) ) ) )  x.  ( J ^ ( ( P  -  1 )  -  ( D `  0 ) ) ) ) )  =  0 )
290 simpr 459 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( D `  0 )  =/=  ( P  -  1 ) )  /\  -.  ( P  -  1
)  <  ( D `  0 ) )  ->  -.  ( P  -  1 )  < 
( D `  0
) )
291290iffalsed 3895 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( D `  0 )  =/=  ( P  -  1 ) )  /\  -.  ( P  -  1
)  <  ( D `  0 ) )  ->  if ( ( P  -  1 )  <  ( D ` 
0 ) ,  0 ,  ( ( ( ! `  ( P  -  1 ) )  /  ( ! `  ( ( P  - 
1 )  -  ( D `  0 )
) ) )  x.  ( J ^ (
( P  -  1 )  -  ( D `
 0 ) ) ) ) )  =  ( ( ( ! `
 ( P  - 
1 ) )  / 
( ! `  (
( P  -  1 )  -  ( D `
 0 ) ) ) )  x.  ( J ^ ( ( P  -  1 )  -  ( D `  0 ) ) ) ) )
292 simpll 752 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( D `  0 )  =/=  ( P  -  1 ) )  /\  -.  ( P  -  1
)  <  ( D `  0 ) )  ->  ph )
293244ad2antrr 724 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( D `  0 )  =/=  ( P  -  1 ) )  /\  -.  ( P  -  1
)  <  ( D `  0 ) )  ->  ( D ` 
0 )  e.  RR )
29460ad2antrr 724 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( D `  0 )  =/=  ( P  -  1 ) )  /\  -.  ( P  -  1
)  <  ( D `  0 ) )  ->  ( P  - 
1 )  e.  RR )
295293, 294, 290nltled 9766 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( D `  0 )  =/=  ( P  -  1 ) )  /\  -.  ( P  -  1
)  <  ( D `  0 ) )  ->  ( D ` 
0 )  <_  ( P  -  1 ) )
296 id 22 . . . . . . . . . . . . . . 15  |-  ( ( D `  0 )  =/=  ( P  - 
1 )  ->  ( D `  0 )  =/=  ( P  -  1 ) )
297296necomd 2674 . . . . . . . . . . . . . 14  |-  ( ( D `  0 )  =/=  ( P  - 
1 )  ->  ( P  -  1 )  =/=  ( D ` 
0 ) )
298297ad2antlr 725 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( D `  0 )  =/=  ( P  -  1 ) )  /\  -.  ( P  -  1
)  <  ( D `  0 ) )  ->  ( P  - 
1 )  =/=  ( D `  0 )
)
299293, 294, 295, 298leneltd 36844 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( D `  0 )  =/=  ( P  -  1 ) )  /\  -.  ( P  -  1
)  <  ( D `  0 ) )  ->  ( D ` 
0 )  <  ( P  -  1 ) )
30089oveq1d 6292 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( J ^ (
( P  -  1 )  -  ( D `
 0 ) ) )  =  ( 0 ^ ( ( P  -  1 )  -  ( D `  0 ) ) ) )
301300adantr 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( D `  0 )  < 
( P  -  1 ) )  ->  ( J ^ ( ( P  -  1 )  -  ( D `  0 ) ) )  =  ( 0 ^ ( ( P  -  1 )  -  ( D ` 
0 ) ) ) )
302243elfzelzd 36868 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( D `  0
)  e.  ZZ )
303164, 302zsubcld 11012 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( P  - 
1 )  -  ( D `  0 )
)  e.  ZZ )
304303adantr 463 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( D `  0 )  < 
( P  -  1 ) )  ->  (
( P  -  1 )  -  ( D `
 0 ) )  e.  ZZ )
305 simpr 459 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( D `  0 )  < 
( P  -  1 ) )  ->  ( D `  0 )  <  ( P  -  1 ) )
306244adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( D `  0 )  < 
( P  -  1 ) )  ->  ( D `  0 )  e.  RR )
30760adantr 463 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( D `  0 )  < 
( P  -  1 ) )  ->  ( P  -  1 )  e.  RR )
308306, 307posdifd 10178 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( D `  0 )  < 
( P  -  1 ) )  ->  (
( D `  0
)  <  ( P  -  1 )  <->  0  <  ( ( P  -  1 )  -  ( D `
 0 ) ) ) )
309305, 308mpbid 210 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( D `  0 )  < 
( P  -  1 ) )  ->  0  <  ( ( P  - 
1 )  -  ( D `  0 )
) )
310 elnnz 10914 . . . . . . . . . . . . . . . . 17  |-  ( ( ( P  -  1 )  -  ( D `
 0 ) )  e.  NN  <->  ( (
( P  -  1 )  -  ( D `
 0 ) )  e.  ZZ  /\  0  <  ( ( P  - 
1 )  -  ( D `  0 )
) ) )
311304, 309, 310sylanbrc 662 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( D `  0 )  < 
( P  -  1 ) )  ->  (
( P  -  1 )  -  ( D `
 0 ) )  e.  NN )
3123110expd 12368 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( D