Metamath Proof Explorer

Theorem etransclem28

Description: ( P - 1 ) factorial divides the N -th derivative of F applied to J . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem28.p 
|- ( ph -> P e. NN )
etransclem28.m 
|- ( ph -> M e. NN0 )
etransclem28.n 
|- ( ph -> N e. NN0 )
etransclem28.c 
|- C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } )
etransclem28.d 
|- ( ph -> D e. ( C ` N ) )
etransclem28.j 
|- ( ph -> J e. ( 0 ... M ) )
etransclem28.t 
|- T = ( ( ( ! ` N ) / 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 ) ) ) ) ) ) )
Assertion etransclem28 
|- ( ph -> ( ! ` ( P - 1 ) ) || T )

Proof

Step Hyp Ref Expression
1 etransclem28.p 
 |-  ( ph -> P e. NN )
2 etransclem28.m 
 |-  ( ph -> M e. NN0 )
3 etransclem28.n 
 |-  ( ph -> N e. NN0 )
4 etransclem28.c 
 |-  C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } )
5 etransclem28.d 
 |-  ( ph -> D e. ( C ` N ) )
6 etransclem28.j 
 |-  ( ph -> J e. ( 0 ... M ) )
7 etransclem28.t 
 |-  T = ( ( ( ! ` N ) / 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 ) ) ) ) ) ) )
8 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
9 1 8 syl 
 |-  ( ph -> ( P - 1 ) e. NN0 )
10 9 faccld 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. NN )
11 10 nnzd 
 |-  ( ph -> ( ! ` ( P - 1 ) ) e. ZZ )
12 11 adantr 
 |-  ( ( ph /\ J = 0 ) -> ( ! ` ( P - 1 ) ) e. ZZ )
13 4 3 etransclem12 
 |-  ( ph -> ( C ` N ) = { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } )
14 5 13 eleqtrd 
 |-  ( ph -> D e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } )
15 fveq1 
 |-  ( c = D -> ( c ` j ) = ( D ` j ) )
16 15 sumeq2sdv 
 |-  ( c = D -> sum_ j e. ( 0 ... M ) ( c ` j ) = sum_ j e. ( 0 ... M ) ( D ` j ) )
17 16 eqeq1d 
 |-  ( c = D -> ( sum_ j e. ( 0 ... M ) ( c ` j ) = N <-> sum_ j e. ( 0 ... M ) ( D ` j ) = N ) )
18 17 elrab 
 |-  ( D e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } <-> ( D e. ( ( 0 ... N ) ^m ( 0 ... M ) ) /\ sum_ j e. ( 0 ... M ) ( D ` j ) = N ) )
19 18 simprbi 
 |-  ( D e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } -> sum_ j e. ( 0 ... M ) ( D ` j ) = N )
20 14 19 syl 
 |-  ( ph -> sum_ j e. ( 0 ... M ) ( D ` j ) = N )
21 20 eqcomd 
 |-  ( ph -> N = sum_ j e. ( 0 ... M ) ( D ` j ) )
22 21 fveq2d 
 |-  ( ph -> ( ! ` N ) = ( ! ` sum_ j e. ( 0 ... M ) ( D ` j ) ) )
23 22 oveq1d 
 |-  ( ph -> ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) = ( ( ! ` sum_ j e. ( 0 ... M ) ( D ` j ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) )
24 nfcv 
 |-  F/_ j D
25 fzfid 
 |-  ( ph -> ( 0 ... M ) e. Fin )
26 nn0ex 
 |-  NN0 e. _V
27 fzssnn0 
 |-  ( 0 ... N ) C_ NN0
28 27 a1i 
 |-  ( D e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } -> ( 0 ... N ) C_ NN0 )
29 mapss 
 |-  ( ( NN0 e. _V /\ ( 0 ... N ) C_ NN0 ) -> ( ( 0 ... N ) ^m ( 0 ... M ) ) C_ ( NN0 ^m ( 0 ... M ) ) )
30 26 28 29 sylancr 
 |-  ( D e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } -> ( ( 0 ... N ) ^m ( 0 ... M ) ) C_ ( NN0 ^m ( 0 ... M ) ) )
31 elrabi 
 |-  ( D e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } -> D e. ( ( 0 ... N ) ^m ( 0 ... M ) ) )
32 30 31 sseldd 
 |-  ( D e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } -> D e. ( NN0 ^m ( 0 ... M ) ) )
33 14 32 syl 
 |-  ( ph -> D e. ( NN0 ^m ( 0 ... M ) ) )
34 24 25 33 mccl 
 |-  ( ph -> ( ( ! ` sum_ j e. ( 0 ... M ) ( D ` j ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. NN )
35 23 34 eqeltrd 
 |-  ( ph -> ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. NN )
36 35 nnzd 
 |-  ( ph -> ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. ZZ )
37 36 adantr 
 |-  ( ( ph /\ J = 0 ) -> ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. ZZ )
38 df-neg 
 |-  -u j = ( 0 - j )
39 oveq1 
 |-  ( J = 0 -> ( J - j ) = ( 0 - j ) )
40 38 39 eqtr4id 
 |-  ( J = 0 -> -u j = ( J - j ) )
41 40 oveq1d 
 |-  ( J = 0 -> ( -u j ^ ( P - ( D ` j ) ) ) = ( ( J - j ) ^ ( P - ( D ` j ) ) ) )
42 41 oveq2d 
 |-  ( J = 0 -> ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( -u j ^ ( P - ( D ` j ) ) ) ) = ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) )
43 42 ifeq2d 
 |-  ( J = 0 -> if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( -u j ^ ( P - ( D ` j ) ) ) ) ) = if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) )
44 43 prodeq2ad 
 |-  ( J = 0 -> prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( -u j ^ ( P - ( D ` j ) ) ) ) ) = prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) )
45 44 adantl 
 |-  ( ( ph /\ J = 0 ) -> prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( -u j ^ ( P - ( D ` j ) ) ) ) ) = prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) )
46 14 31 syl 
 |-  ( ph -> D e. ( ( 0 ... N ) ^m ( 0 ... M ) ) )
47 elmapi 
 |-  ( D e. ( ( 0 ... N ) ^m ( 0 ... M ) ) -> D : ( 0 ... M ) --> ( 0 ... N ) )
48 46 47 syl 
 |-  ( ph -> D : ( 0 ... M ) --> ( 0 ... N ) )
49 1 48 6 etransclem7 
 |-  ( ph -> prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ )
50 49 adantr 
 |-  ( ( ph /\ J = 0 ) -> prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( D ` j ) ) ) ) ) e. ZZ )
51 45 50 eqeltrd 
 |-  ( ( ph /\ J = 0 ) -> prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( -u j ^ ( P - ( D ` j ) ) ) ) ) e. ZZ )
52 12 51 zmulcld 
 |-  ( ( ph /\ J = 0 ) -> ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( -u j ^ ( P - ( D ` j ) ) ) ) ) ) e. ZZ )
53 12 37 52 3jca 
 |-  ( ( ph /\ J = 0 ) -> ( ( ! ` ( P - 1 ) ) e. ZZ /\ ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. ZZ /\ ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( -u j ^ ( P - ( D ` j ) ) ) ) ) ) e. ZZ ) )
54 dvdsmul1 
 |-  ( ( ( ! ` ( P - 1 ) ) e. ZZ /\ prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( -u j ^ ( P - ( D ` j ) ) ) ) ) e. ZZ ) -> ( ! ` ( P - 1 ) ) || ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( -u j ^ ( P - ( D ` j ) ) ) ) ) ) )
55 12 51 54 syl2anc 
 |-  ( ( ph /\ J = 0 ) -> ( ! ` ( P - 1 ) ) || ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( -u j ^ ( P - ( D ` j ) ) ) ) ) ) )
56 dvdsmultr2 
 |-  ( ( ( ! ` ( P - 1 ) ) e. ZZ /\ ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( D ` j ) ) ) e. ZZ /\ ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( -u j ^ ( P - ( D ` j ) ) ) ) ) ) e. ZZ ) -> ( ( ! ` ( P - 1 ) ) || ( ( ! ` ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( D ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( D ` j ) ) ) ) x. ( -u j ^ ( P - ( D ` j ) ) ) ) ) ) -> ( ! ` ( P - 1 ) ) || ( ( ( ! ` N ) / 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. ( -u j ^ ( P - ( D ` j ) ) ) ) ) ) ) ) )
57 53 55 56 sylc 
 |-  ( ( ph /\ J = 0 ) -> ( ! ` ( P - 1 ) ) || ( ( ( ! ` N ) / 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. ( -u j ^ ( P - ( D ` j ) ) ) ) ) ) ) )
58 57 adantr 
 |-  ( ( ( ph /\ J = 0 ) /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ! ` ( P - 1 ) ) || ( ( ( ! ` N ) / 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. ( -u j ^ ( P - ( D ` j ) ) ) ) ) ) ) )
59 1 ad2antrr 
 |-  ( ( ( ph /\ J = 0 ) /\ ( D ` 0 ) = ( P - 1 ) ) -> P e. NN )
60 2 ad2antrr 
 |-  ( ( ( ph /\ J = 0 ) /\ ( D ` 0 ) = ( P - 1 ) ) -> M e. NN0 )
61 48 ad2antrr 
 |-  ( ( ( ph /\ J = 0 ) /\ ( D ` 0 ) = ( P - 1 ) ) -> D : ( 0 ... M ) --> ( 0 ... N ) )
62 eqid 
 |-  ( ( ( ! ` N ) / 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 ) ) ) ) ) ) ) = ( ( ( ! ` N ) / 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 ) ) ) ) ) ) )
63 simplr 
 |-  ( ( ( ph /\ J = 0 ) /\ ( D ` 0 ) = ( P - 1 ) ) -> J = 0 )
64 simpr 
 |-  ( ( ( ph /\ J = 0 ) /\ ( D ` 0 ) = ( P - 1 ) ) -> ( D ` 0 ) = ( P - 1 ) )
65 59 60 61 62 63 64 etransclem14 
 |-  ( ( ( ph /\ J = 0 ) /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ( ( ! ` N ) / 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 ) ) ) ) ) ) ) = ( ( ( ! ` N ) / 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. ( -u j ^ ( P - ( D ` j ) ) ) ) ) ) ) )
66 58 65 breqtrrd 
 |-  ( ( ( ph /\ J = 0 ) /\ ( D ` 0 ) = ( P - 1 ) ) -> ( ! ` ( P - 1 ) ) || ( ( ( ! ` N ) / 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 ) ) ) ) ) ) ) )
67 dvds0 
 |-  ( ( ! ` ( P - 1 ) ) e. ZZ -> ( ! ` ( P - 1 ) ) || 0 )
68 11 67 syl 
 |-  ( ph -> ( ! ` ( P - 1 ) ) || 0 )
69 68 ad2antrr 
 |-  ( ( ( ph /\ J = 0 ) /\ -. ( D ` 0 ) = ( P - 1 ) ) -> ( ! ` ( P - 1 ) ) || 0 )
70 1 ad2antrr 
 |-  ( ( ( ph /\ J = 0 ) /\ -. ( D ` 0 ) = ( P - 1 ) ) -> P e. NN )
71 2 ad2antrr 
 |-  ( ( ( ph /\ J = 0 ) /\ -. ( D ` 0 ) = ( P - 1 ) ) -> M e. NN0 )
72 3 ad2antrr 
 |-  ( ( ( ph /\ J = 0 ) /\ -. ( D ` 0 ) = ( P - 1 ) ) -> N e. NN0 )
73 48 ad2antrr 
 |-  ( ( ( ph /\ J = 0 ) /\ -. ( D ` 0 ) = ( P - 1 ) ) -> D : ( 0 ... M ) --> ( 0 ... N ) )
74 simplr 
 |-  ( ( ( ph /\ J = 0 ) /\ -. ( D ` 0 ) = ( P - 1 ) ) -> J = 0 )
75 neqne 
 |-  ( -. ( D ` 0 ) = ( P - 1 ) -> ( D ` 0 ) =/= ( P - 1 ) )
76 75 adantl 
 |-  ( ( ( ph /\ J = 0 ) /\ -. ( D ` 0 ) = ( P - 1 ) ) -> ( D ` 0 ) =/= ( P - 1 ) )
77 70 71 72 73 62 74 76 etransclem15 
 |-  ( ( ( ph /\ J = 0 ) /\ -. ( D ` 0 ) = ( P - 1 ) ) -> ( ( ( ! ` N ) / 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 ) ) ) ) ) ) ) = 0 )
78 69 77 breqtrrd 
 |-  ( ( ( ph /\ J = 0 ) /\ -. ( D ` 0 ) = ( P - 1 ) ) -> ( ! ` ( P - 1 ) ) || ( ( ( ! ` N ) / 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 ) ) ) ) ) ) ) )
79 66 78 pm2.61dan 
 |-  ( ( ph /\ J = 0 ) -> ( ! ` ( P - 1 ) ) || ( ( ( ! ` N ) / 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 ) ) ) ) ) ) ) )
80 1 nnzd 
 |-  ( ph -> P e. ZZ )
81 elfznn0 
 |-  ( J e. ( 0 ... M ) -> J e. NN0 )
82 6 81 syl 
 |-  ( ph -> J e. NN0 )
83 82 nn0zd 
 |-  ( ph -> J e. ZZ )
84 1 2 3 83 4 5 etransclem26 
 |-  ( ph -> ( ( ( ! ` N ) / 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 ) ) ) ) ) ) ) e. ZZ )
85 11 80 84 3jca 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) e. ZZ /\ P e. ZZ /\ ( ( ( ! ` N ) / 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 ) ) ) ) ) ) ) e. ZZ ) )
86 85 adantr 
 |-  ( ( ph /\ -. J = 0 ) -> ( ( ! ` ( P - 1 ) ) e. ZZ /\ P e. ZZ /\ ( ( ( ! ` N ) / 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 ) ) ) ) ) ) ) e. ZZ ) )
87 1 nncnd 
 |-  ( ph -> P e. CC )
88 1cnd 
 |-  ( ph -> 1 e. CC )
89 87 88 npcand 
 |-  ( ph -> ( ( P - 1 ) + 1 ) = P )
90 89 eqcomd 
 |-  ( ph -> P = ( ( P - 1 ) + 1 ) )
91 90 fveq2d 
 |-  ( ph -> ( ! ` P ) = ( ! ` ( ( P - 1 ) + 1 ) ) )
92 facp1 
 |-  ( ( P - 1 ) e. NN0 -> ( ! ` ( ( P - 1 ) + 1 ) ) = ( ( ! ` ( P - 1 ) ) x. ( ( P - 1 ) + 1 ) ) )
93 9 92 syl 
 |-  ( ph -> ( ! ` ( ( P - 1 ) + 1 ) ) = ( ( ! ` ( P - 1 ) ) x. ( ( P - 1 ) + 1 ) ) )
94 89 oveq2d 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) x. ( ( P - 1 ) + 1 ) ) = ( ( ! ` ( P - 1 ) ) x. P ) )
95 91 93 94 3eqtrrd 
 |-  ( ph -> ( ( ! ` ( P - 1 ) ) x. P ) = ( ! ` P ) )
96 95 adantr 
 |-  ( ( ph /\ -. J = 0 ) -> ( ( ! ` ( P - 1 ) ) x. P ) = ( ! ` P ) )
97 1 adantr 
 |-  ( ( ph /\ -. J = 0 ) -> P e. NN )
98 2 adantr 
 |-  ( ( ph /\ -. J = 0 ) -> M e. NN0 )
99 3 adantr 
 |-  ( ( ph /\ -. J = 0 ) -> N e. NN0 )
100 48 adantr 
 |-  ( ( ph /\ -. J = 0 ) -> D : ( 0 ... M ) --> ( 0 ... N ) )
101 20 adantr 
 |-  ( ( ph /\ -. J = 0 ) -> sum_ j e. ( 0 ... M ) ( D ` j ) = N )
102 1zzd 
 |-  ( ( ph /\ -. J = 0 ) -> 1 e. ZZ )
103 2 nn0zd 
 |-  ( ph -> M e. ZZ )
104 103 adantr 
 |-  ( ( ph /\ -. J = 0 ) -> M e. ZZ )
105 83 adantr 
 |-  ( ( ph /\ -. J = 0 ) -> J e. ZZ )
106 82 adantr 
 |-  ( ( ph /\ -. J = 0 ) -> J e. NN0 )
107 neqne 
 |-  ( -. J = 0 -> J =/= 0 )
108 107 adantl 
 |-  ( ( ph /\ -. J = 0 ) -> J =/= 0 )
109 elnnne0 
 |-  ( J e. NN <-> ( J e. NN0 /\ J =/= 0 ) )
110 106 108 109 sylanbrc 
 |-  ( ( ph /\ -. J = 0 ) -> J e. NN )
111 110 nnge1d 
 |-  ( ( ph /\ -. J = 0 ) -> 1 <_ J )
112 elfzle2 
 |-  ( J e. ( 0 ... M ) -> J <_ M )
113 6 112 syl 
 |-  ( ph -> J <_ M )
114 113 adantr 
 |-  ( ( ph /\ -. J = 0 ) -> J <_ M )
115 102 104 105 111 114 elfzd 
 |-  ( ( ph /\ -. J = 0 ) -> J e. ( 1 ... M ) )
116 97 98 99 100 101 62 115 etransclem25 
 |-  ( ( ph /\ -. J = 0 ) -> ( ! ` P ) || ( ( ( ! ` N ) / 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 ) ) ) ) ) ) ) )
117 96 116 eqbrtrd 
 |-  ( ( ph /\ -. J = 0 ) -> ( ( ! ` ( P - 1 ) ) x. P ) || ( ( ( ! ` N ) / 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 ) ) ) ) ) ) ) )
118 muldvds1 
 |-  ( ( ( ! ` ( P - 1 ) ) e. ZZ /\ P e. ZZ /\ ( ( ( ! ` N ) / 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 ) ) ) ) ) ) ) e. ZZ ) -> ( ( ( ! ` ( P - 1 ) ) x. P ) || ( ( ( ! ` N ) / 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 ) ) || ( ( ( ! ` N ) / 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 ) ) ) ) ) ) ) ) )
119 86 117 118 sylc 
 |-  ( ( ph /\ -. J = 0 ) -> ( ! ` ( P - 1 ) ) || ( ( ( ! ` N ) / 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 ) ) ) ) ) ) ) )
120 79 119 pm2.61dan 
 |-  ( ph -> ( ! ` ( P - 1 ) ) || ( ( ( ! ` N ) / 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 ) ) ) ) ) ) ) )
121 120 7 breqtrrdi 
 |-  ( ph -> ( ! ` ( P - 1 ) ) || T )