Metamath Proof Explorer

Theorem etransclem25

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

Ref Expression
Hypotheses etransclem25.p 
|- ( ph -> P e. NN )
etransclem25.m 
|- ( ph -> M e. NN0 )
etransclem25.n 
|- ( ph -> N e. NN0 )
etransclem25.c 
|- ( ph -> C : ( 0 ... M ) --> ( 0 ... N ) )
etransclem25.sumc 
|- ( ph -> sum_ j e. ( 0 ... M ) ( C ` j ) = N )
etransclem25.t 
|- T = ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) x. ( if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) ) )
etransclem25.j 
|- ( ph -> J e. ( 1 ... M ) )
Assertion etransclem25 
|- ( ph -> ( ! ` P ) || T )

Proof

Step Hyp Ref Expression
1 etransclem25.p 
 |-  ( ph -> P e. NN )
2 etransclem25.m 
 |-  ( ph -> M e. NN0 )
3 etransclem25.n 
 |-  ( ph -> N e. NN0 )
4 etransclem25.c 
 |-  ( ph -> C : ( 0 ... M ) --> ( 0 ... N ) )
5 etransclem25.sumc 
 |-  ( ph -> sum_ j e. ( 0 ... M ) ( C ` j ) = N )
6 etransclem25.t 
 |-  T = ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) x. ( if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) ) )
7 etransclem25.j 
 |-  ( ph -> J e. ( 1 ... M ) )
8 1 nnnn0d 
 |-  ( ph -> P e. NN0 )
9 8 faccld 
 |-  ( ph -> ( ! ` P ) e. NN )
10 9 nnzd 
 |-  ( ph -> ( ! ` P ) e. ZZ )
11 5 eqcomd 
 |-  ( ph -> N = sum_ j e. ( 0 ... M ) ( C ` j ) )
12 11 fveq2d 
 |-  ( ph -> ( ! ` N ) = ( ! ` sum_ j e. ( 0 ... M ) ( C ` j ) ) )
13 12 oveq1d 
 |-  ( ph -> ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) = ( ( ! ` sum_ j e. ( 0 ... M ) ( C ` j ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) )
14 nfcv 
 |-  F/_ j C
15 fzfid 
 |-  ( ph -> ( 0 ... M ) e. Fin )
16 nn0ex 
 |-  NN0 e. _V
17 fzssnn0 
 |-  ( 0 ... N ) C_ NN0
18 mapss 
 |-  ( ( NN0 e. _V /\ ( 0 ... N ) C_ NN0 ) -> ( ( 0 ... N ) ^m ( 0 ... M ) ) C_ ( NN0 ^m ( 0 ... M ) ) )
19 16 17 18 mp2an 
 |-  ( ( 0 ... N ) ^m ( 0 ... M ) ) C_ ( NN0 ^m ( 0 ... M ) )
20 ovex 
 |-  ( 0 ... N ) e. _V
21 ovexd 
 |-  ( C : ( 0 ... M ) --> ( 0 ... N ) -> ( 0 ... M ) e. _V )
22 elmapg 
 |-  ( ( ( 0 ... N ) e. _V /\ ( 0 ... M ) e. _V ) -> ( C e. ( ( 0 ... N ) ^m ( 0 ... M ) ) <-> C : ( 0 ... M ) --> ( 0 ... N ) ) )
23 20 21 22 sylancr 
 |-  ( C : ( 0 ... M ) --> ( 0 ... N ) -> ( C e. ( ( 0 ... N ) ^m ( 0 ... M ) ) <-> C : ( 0 ... M ) --> ( 0 ... N ) ) )
24 23 ibir 
 |-  ( C : ( 0 ... M ) --> ( 0 ... N ) -> C e. ( ( 0 ... N ) ^m ( 0 ... M ) ) )
25 19 24 sseldi 
 |-  ( C : ( 0 ... M ) --> ( 0 ... N ) -> C e. ( NN0 ^m ( 0 ... M ) ) )
26 4 25 syl 
 |-  ( ph -> C e. ( NN0 ^m ( 0 ... M ) ) )
27 14 15 26 mccl 
 |-  ( ph -> ( ( ! ` sum_ j e. ( 0 ... M ) ( C ` j ) ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) e. NN )
28 13 27 eqeltrd 
 |-  ( ph -> ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) e. NN )
29 28 nnzd 
 |-  ( ph -> ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) e. ZZ )
30 7 elfzelzd 
 |-  ( ph -> J e. ZZ )
31 1 2 4 30 etransclem10 
 |-  ( ph -> if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) e. ZZ )
32 29 31 zmulcld 
 |-  ( ph -> ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) x. if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) ) e. ZZ )
33 fzfid 
 |-  ( ph -> ( 1 ... M ) e. Fin )
34 1 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> P e. NN )
35 4 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> C : ( 0 ... M ) --> ( 0 ... N ) )
36 0z 
 |-  0 e. ZZ
37 fzp1ss 
 |-  ( 0 e. ZZ -> ( ( 0 + 1 ) ... M ) C_ ( 0 ... M ) )
38 36 37 ax-mp 
 |-  ( ( 0 + 1 ) ... M ) C_ ( 0 ... M )
39 id 
 |-  ( j e. ( 1 ... M ) -> j e. ( 1 ... M ) )
40 1e0p1 
 |-  1 = ( 0 + 1 )
41 40 oveq1i 
 |-  ( 1 ... M ) = ( ( 0 + 1 ) ... M )
42 39 41 eleqtrdi 
 |-  ( j e. ( 1 ... M ) -> j e. ( ( 0 + 1 ) ... M ) )
43 38 42 sseldi 
 |-  ( j e. ( 1 ... M ) -> j e. ( 0 ... M ) )
44 43 adantl 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> j e. ( 0 ... M ) )
45 30 adantr 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> J e. ZZ )
46 34 35 44 45 etransclem3 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) e. ZZ )
47 33 46 fprodzcl 
 |-  ( ph -> prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) e. ZZ )
48 10 32 47 3jca 
 |-  ( ph -> ( ( ! ` P ) e. ZZ /\ ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) x. if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) ) e. ZZ /\ prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) e. ZZ ) )
49 30 zcnd 
 |-  ( ph -> J e. CC )
50 49 subidd 
 |-  ( ph -> ( J - J ) = 0 )
51 50 eqcomd 
 |-  ( ph -> 0 = ( J - J ) )
52 51 oveq1d 
 |-  ( ph -> ( 0 ^ ( P - ( C ` J ) ) ) = ( ( J - J ) ^ ( P - ( C ` J ) ) ) )
53 52 oveq2d 
 |-  ( ph -> ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) = ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( ( J - J ) ^ ( P - ( C ` J ) ) ) ) )
54 53 ifeq2d 
 |-  ( ph -> if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) ) = if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( ( J - J ) ^ ( P - ( C ` J ) ) ) ) ) )
55 id 
 |-  ( J e. ( 1 ... M ) -> J e. ( 1 ... M ) )
56 55 41 eleqtrdi 
 |-  ( J e. ( 1 ... M ) -> J e. ( ( 0 + 1 ) ... M ) )
57 38 56 sseldi 
 |-  ( J e. ( 1 ... M ) -> J e. ( 0 ... M ) )
58 7 57 syl 
 |-  ( ph -> J e. ( 0 ... M ) )
59 1 4 58 30 etransclem3 
 |-  ( ph -> if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( ( J - J ) ^ ( P - ( C ` J ) ) ) ) ) e. ZZ )
60 54 59 eqeltrd 
 |-  ( ph -> if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) ) e. ZZ )
61 fzfi 
 |-  ( 1 ... M ) e. Fin
62 diffi 
 |-  ( ( 1 ... M ) e. Fin -> ( ( 1 ... M ) \ { J } ) e. Fin )
63 61 62 mp1i 
 |-  ( ph -> ( ( 1 ... M ) \ { J } ) e. Fin )
64 1 adantr 
 |-  ( ( ph /\ j e. ( ( 1 ... M ) \ { J } ) ) -> P e. NN )
65 4 adantr 
 |-  ( ( ph /\ j e. ( ( 1 ... M ) \ { J } ) ) -> C : ( 0 ... M ) --> ( 0 ... N ) )
66 eldifi 
 |-  ( j e. ( ( 1 ... M ) \ { J } ) -> j e. ( 1 ... M ) )
67 66 43 syl 
 |-  ( j e. ( ( 1 ... M ) \ { J } ) -> j e. ( 0 ... M ) )
68 67 adantl 
 |-  ( ( ph /\ j e. ( ( 1 ... M ) \ { J } ) ) -> j e. ( 0 ... M ) )
69 30 adantr 
 |-  ( ( ph /\ j e. ( ( 1 ... M ) \ { J } ) ) -> J e. ZZ )
70 64 65 68 69 etransclem3 
 |-  ( ( ph /\ j e. ( ( 1 ... M ) \ { J } ) ) -> if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) e. ZZ )
71 63 70 fprodzcl 
 |-  ( ph -> prod_ j e. ( ( 1 ... M ) \ { J } ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) e. ZZ )
72 dvds0 
 |-  ( ( ! ` P ) e. ZZ -> ( ! ` P ) || 0 )
73 10 72 syl 
 |-  ( ph -> ( ! ` P ) || 0 )
74 73 adantr 
 |-  ( ( ph /\ P < ( C ` J ) ) -> ( ! ` P ) || 0 )
75 iftrue 
 |-  ( P < ( C ` J ) -> if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) ) = 0 )
76 75 eqcomd 
 |-  ( P < ( C ` J ) -> 0 = if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) ) )
77 76 adantl 
 |-  ( ( ph /\ P < ( C ` J ) ) -> 0 = if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) ) )
78 74 77 breqtrd 
 |-  ( ( ph /\ P < ( C ` J ) ) -> ( ! ` P ) || if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) ) )
79 iddvds 
 |-  ( ( ! ` P ) e. ZZ -> ( ! ` P ) || ( ! ` P ) )
80 10 79 syl 
 |-  ( ph -> ( ! ` P ) || ( ! ` P ) )
81 80 ad2antrr 
 |-  ( ( ( ph /\ -. P < ( C ` J ) ) /\ P = ( C ` J ) ) -> ( ! ` P ) || ( ! ` P ) )
82 iffalse 
 |-  ( -. P < ( C ` J ) -> if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) ) = ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) )
83 82 ad2antlr 
 |-  ( ( ( ph /\ -. P < ( C ` J ) ) /\ P = ( C ` J ) ) -> if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) ) = ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) )
84 oveq1 
 |-  ( P = ( C ` J ) -> ( P - ( C ` J ) ) = ( ( C ` J ) - ( C ` J ) ) )
85 84 adantl 
 |-  ( ( ph /\ P = ( C ` J ) ) -> ( P - ( C ` J ) ) = ( ( C ` J ) - ( C ` J ) ) )
86 4 58 ffvelrnd 
 |-  ( ph -> ( C ` J ) e. ( 0 ... N ) )
87 86 elfzelzd 
 |-  ( ph -> ( C ` J ) e. ZZ )
88 87 zcnd 
 |-  ( ph -> ( C ` J ) e. CC )
89 88 adantr 
 |-  ( ( ph /\ P = ( C ` J ) ) -> ( C ` J ) e. CC )
90 89 subidd 
 |-  ( ( ph /\ P = ( C ` J ) ) -> ( ( C ` J ) - ( C ` J ) ) = 0 )
91 85 90 eqtrd 
 |-  ( ( ph /\ P = ( C ` J ) ) -> ( P - ( C ` J ) ) = 0 )
92 91 fveq2d 
 |-  ( ( ph /\ P = ( C ` J ) ) -> ( ! ` ( P - ( C ` J ) ) ) = ( ! ` 0 ) )
93 fac0 
 |-  ( ! ` 0 ) = 1
94 92 93 eqtrdi 
 |-  ( ( ph /\ P = ( C ` J ) ) -> ( ! ` ( P - ( C ` J ) ) ) = 1 )
95 94 oveq2d 
 |-  ( ( ph /\ P = ( C ` J ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) = ( ( ! ` P ) / 1 ) )
96 9 nncnd 
 |-  ( ph -> ( ! ` P ) e. CC )
97 96 div1d 
 |-  ( ph -> ( ( ! ` P ) / 1 ) = ( ! ` P ) )
98 97 adantr 
 |-  ( ( ph /\ P = ( C ` J ) ) -> ( ( ! ` P ) / 1 ) = ( ! ` P ) )
99 95 98 eqtrd 
 |-  ( ( ph /\ P = ( C ` J ) ) -> ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) = ( ! ` P ) )
100 91 oveq2d 
 |-  ( ( ph /\ P = ( C ` J ) ) -> ( 0 ^ ( P - ( C ` J ) ) ) = ( 0 ^ 0 ) )
101 0cnd 
 |-  ( ( ph /\ P = ( C ` J ) ) -> 0 e. CC )
102 101 exp0d 
 |-  ( ( ph /\ P = ( C ` J ) ) -> ( 0 ^ 0 ) = 1 )
103 100 102 eqtrd 
 |-  ( ( ph /\ P = ( C ` J ) ) -> ( 0 ^ ( P - ( C ` J ) ) ) = 1 )
104 99 103 oveq12d 
 |-  ( ( ph /\ P = ( C ` J ) ) -> ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) = ( ( ! ` P ) x. 1 ) )
105 96 mulid1d 
 |-  ( ph -> ( ( ! ` P ) x. 1 ) = ( ! ` P ) )
106 105 adantr 
 |-  ( ( ph /\ P = ( C ` J ) ) -> ( ( ! ` P ) x. 1 ) = ( ! ` P ) )
107 104 106 eqtrd 
 |-  ( ( ph /\ P = ( C ` J ) ) -> ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) = ( ! ` P ) )
108 107 adantlr 
 |-  ( ( ( ph /\ -. P < ( C ` J ) ) /\ P = ( C ` J ) ) -> ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) = ( ! ` P ) )
109 83 108 eqtr2d 
 |-  ( ( ( ph /\ -. P < ( C ` J ) ) /\ P = ( C ` J ) ) -> ( ! ` P ) = if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) ) )
110 81 109 breqtrd 
 |-  ( ( ( ph /\ -. P < ( C ` J ) ) /\ P = ( C ` J ) ) -> ( ! ` P ) || if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) ) )
111 73 ad2antrr 
 |-  ( ( ( ph /\ -. P < ( C ` J ) ) /\ -. P = ( C ` J ) ) -> ( ! ` P ) || 0 )
112 simpr 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> -. P < ( C ` J ) )
113 112 adantr 
 |-  ( ( ( ph /\ -. P < ( C ` J ) ) /\ -. P = ( C ` J ) ) -> -. P < ( C ` J ) )
114 113 iffalsed 
 |-  ( ( ( ph /\ -. P < ( C ` J ) ) /\ -. P = ( C ` J ) ) -> if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) ) = ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) )
115 simpll 
 |-  ( ( ( ph /\ -. P < ( C ` J ) ) /\ -. P = ( C ` J ) ) -> ph )
116 87 zred 
 |-  ( ph -> ( C ` J ) e. RR )
117 116 ad2antrr 
 |-  ( ( ( ph /\ -. P < ( C ` J ) ) /\ -. P = ( C ` J ) ) -> ( C ` J ) e. RR )
118 1 nnred 
 |-  ( ph -> P e. RR )
119 118 ad2antrr 
 |-  ( ( ( ph /\ -. P < ( C ` J ) ) /\ -. P = ( C ` J ) ) -> P e. RR )
120 116 adantr 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( C ` J ) e. RR )
121 118 adantr 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> P e. RR )
122 120 121 112 nltled 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( C ` J ) <_ P )
123 122 adantr 
 |-  ( ( ( ph /\ -. P < ( C ` J ) ) /\ -. P = ( C ` J ) ) -> ( C ` J ) <_ P )
124 neqne 
 |-  ( -. P = ( C ` J ) -> P =/= ( C ` J ) )
125 124 adantl 
 |-  ( ( ( ph /\ -. P < ( C ` J ) ) /\ -. P = ( C ` J ) ) -> P =/= ( C ` J ) )
126 117 119 123 125 leneltd 
 |-  ( ( ( ph /\ -. P < ( C ` J ) ) /\ -. P = ( C ` J ) ) -> ( C ` J ) < P )
127 1 nnzd 
 |-  ( ph -> P e. ZZ )
128 127 adantr 
 |-  ( ( ph /\ ( C ` J ) < P ) -> P e. ZZ )
129 87 adantr 
 |-  ( ( ph /\ ( C ` J ) < P ) -> ( C ` J ) e. ZZ )
130 128 129 zsubcld 
 |-  ( ( ph /\ ( C ` J ) < P ) -> ( P - ( C ` J ) ) e. ZZ )
131 simpr 
 |-  ( ( ph /\ ( C ` J ) < P ) -> ( C ` J ) < P )
132 116 adantr 
 |-  ( ( ph /\ ( C ` J ) < P ) -> ( C ` J ) e. RR )
133 118 adantr 
 |-  ( ( ph /\ ( C ` J ) < P ) -> P e. RR )
134 132 133 posdifd 
 |-  ( ( ph /\ ( C ` J ) < P ) -> ( ( C ` J ) < P <-> 0 < ( P - ( C ` J ) ) ) )
135 131 134 mpbid 
 |-  ( ( ph /\ ( C ` J ) < P ) -> 0 < ( P - ( C ` J ) ) )
136 elnnz 
 |-  ( ( P - ( C ` J ) ) e. NN <-> ( ( P - ( C ` J ) ) e. ZZ /\ 0 < ( P - ( C ` J ) ) ) )
137 130 135 136 sylanbrc 
 |-  ( ( ph /\ ( C ` J ) < P ) -> ( P - ( C ` J ) ) e. NN )
138 137 0expd 
 |-  ( ( ph /\ ( C ` J ) < P ) -> ( 0 ^ ( P - ( C ` J ) ) ) = 0 )
139 138 oveq2d 
 |-  ( ( ph /\ ( C ` J ) < P ) -> ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) = ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. 0 ) )
140 96 adantr 
 |-  ( ( ph /\ ( C ` J ) < P ) -> ( ! ` P ) e. CC )
141 137 nnnn0d 
 |-  ( ( ph /\ ( C ` J ) < P ) -> ( P - ( C ` J ) ) e. NN0 )
142 141 faccld 
 |-  ( ( ph /\ ( C ` J ) < P ) -> ( ! ` ( P - ( C ` J ) ) ) e. NN )
143 142 nncnd 
 |-  ( ( ph /\ ( C ` J ) < P ) -> ( ! ` ( P - ( C ` J ) ) ) e. CC )
144 142 nnne0d 
 |-  ( ( ph /\ ( C ` J ) < P ) -> ( ! ` ( P - ( C ` J ) ) ) =/= 0 )
145 140 143 144 divcld 
 |-  ( ( ph /\ ( C ` J ) < P ) -> ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) e. CC )
146 145 mul01d 
 |-  ( ( ph /\ ( C ` J ) < P ) -> ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. 0 ) = 0 )
147 139 146 eqtrd 
 |-  ( ( ph /\ ( C ` J ) < P ) -> ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) = 0 )
148 115 126 147 syl2anc 
 |-  ( ( ( ph /\ -. P < ( C ` J ) ) /\ -. P = ( C ` J ) ) -> ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) = 0 )
149 114 148 eqtr2d 
 |-  ( ( ( ph /\ -. P < ( C ` J ) ) /\ -. P = ( C ` J ) ) -> 0 = if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) ) )
150 111 149 breqtrd 
 |-  ( ( ( ph /\ -. P < ( C ` J ) ) /\ -. P = ( C ` J ) ) -> ( ! ` P ) || if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) ) )
151 110 150 pm2.61dan 
 |-  ( ( ph /\ -. P < ( C ` J ) ) -> ( ! ` P ) || if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) ) )
152 78 151 pm2.61dan 
 |-  ( ph -> ( ! ` P ) || if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) ) )
153 10 60 71 152 dvdsmultr1d 
 |-  ( ph -> ( ! ` P ) || ( if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) ) x. prod_ j e. ( ( 1 ... M ) \ { J } ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) ) )
154 46 zcnd 
 |-  ( ( ph /\ j e. ( 1 ... M ) ) -> if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) e. CC )
155 fveq2 
 |-  ( j = J -> ( C ` j ) = ( C ` J ) )
156 155 breq2d 
 |-  ( j = J -> ( P < ( C ` j ) <-> P < ( C ` J ) ) )
157 156 adantl 
 |-  ( ( ph /\ j = J ) -> ( P < ( C ` j ) <-> P < ( C ` J ) ) )
158 155 oveq2d 
 |-  ( j = J -> ( P - ( C ` j ) ) = ( P - ( C ` J ) ) )
159 158 fveq2d 
 |-  ( j = J -> ( ! ` ( P - ( C ` j ) ) ) = ( ! ` ( P - ( C ` J ) ) ) )
160 159 oveq2d 
 |-  ( j = J -> ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) = ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) )
161 160 adantl 
 |-  ( ( ph /\ j = J ) -> ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) = ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) )
162 oveq2 
 |-  ( j = J -> ( J - j ) = ( J - J ) )
163 162 50 sylan9eqr 
 |-  ( ( ph /\ j = J ) -> ( J - j ) = 0 )
164 158 adantl 
 |-  ( ( ph /\ j = J ) -> ( P - ( C ` j ) ) = ( P - ( C ` J ) ) )
165 163 164 oveq12d 
 |-  ( ( ph /\ j = J ) -> ( ( J - j ) ^ ( P - ( C ` j ) ) ) = ( 0 ^ ( P - ( C ` J ) ) ) )
166 161 165 oveq12d 
 |-  ( ( ph /\ j = J ) -> ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) = ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) )
167 157 166 ifbieq2d 
 |-  ( ( ph /\ j = J ) -> if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) = if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) ) )
168 33 154 7 167 fprodsplit1 
 |-  ( ph -> prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) = ( if ( P < ( C ` J ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` J ) ) ) ) x. ( 0 ^ ( P - ( C ` J ) ) ) ) ) x. prod_ j e. ( ( 1 ... M ) \ { J } ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) ) )
169 153 168 breqtrrd 
 |-  ( ph -> ( ! ` P ) || prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) )
170 dvdsmultr2 
 |-  ( ( ( ! ` P ) e. ZZ /\ ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) x. if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) ) e. ZZ /\ prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) e. ZZ ) -> ( ( ! ` P ) || prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) -> ( ! ` P ) || ( ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) x. if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) ) ) )
171 48 169 170 sylc 
 |-  ( ph -> ( ! ` P ) || ( ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) x. if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) ) )
172 3 faccld 
 |-  ( ph -> ( ! ` N ) e. NN )
173 172 nncnd 
 |-  ( ph -> ( ! ` N ) e. CC )
174 4 ffvelrnda 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( C ` j ) e. ( 0 ... N ) )
175 17 174 sseldi 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( C ` j ) e. NN0 )
176 175 faccld 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ! ` ( C ` j ) ) e. NN )
177 176 nncnd 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ! ` ( C ` j ) ) e. CC )
178 15 177 fprodcl 
 |-  ( ph -> prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) e. CC )
179 176 nnne0d 
 |-  ( ( ph /\ j e. ( 0 ... M ) ) -> ( ! ` ( C ` j ) ) =/= 0 )
180 15 177 179 fprodn0 
 |-  ( ph -> prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) =/= 0 )
181 173 178 180 divcld 
 |-  ( ph -> ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) e. CC )
182 31 zcnd 
 |-  ( ph -> if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) e. CC )
183 33 154 fprodcl 
 |-  ( ph -> prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) e. CC )
184 181 182 183 mulassd 
 |-  ( ph -> ( ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) x. if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) ) = ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) x. ( if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) ) ) )
185 184 6 eqtr4di 
 |-  ( ph -> ( ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( C ` j ) ) ) x. if ( ( P - 1 ) < ( C ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( C ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( C ` 0 ) ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( C ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( C ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( C ` j ) ) ) ) ) ) = T )
186 171 185 breqtrd 
 |-  ( ph -> ( ! ` P ) || T )