Metamath Proof Explorer


Theorem etransclem24

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)

Ref Expression
Hypotheses etransclem24.p φ P
etransclem24.m φ M 0
etransclem24.i φ I 0
etransclem24.ip φ I P 1
etransclem24.j φ J = 0
etransclem24.c C = n 0 c 0 n 0 M | j = 0 M c j = n
etransclem24.d φ D C I
Assertion etransclem24 φ P I ! j = 0 M D j ! if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! J j P D j P 1 !

Proof

Step Hyp Ref Expression
1 etransclem24.p φ P
2 etransclem24.m φ M 0
3 etransclem24.i φ I 0
4 etransclem24.ip φ I P 1
5 etransclem24.j φ J = 0
6 etransclem24.c C = n 0 c 0 n 0 M | j = 0 M c j = n
7 etransclem24.d φ D C I
8 6 3 etransclem12 φ C I = c 0 I 0 M | j = 0 M c j = I
9 7 8 eleqtrd φ D c 0 I 0 M | j = 0 M c j = I
10 fveq1 c = D c j = D j
11 10 sumeq2sdv c = D j = 0 M c j = j = 0 M D j
12 11 eqeq1d c = D j = 0 M c j = I j = 0 M D j = I
13 12 elrab D c 0 I 0 M | j = 0 M c j = I D 0 I 0 M j = 0 M D j = I
14 9 13 sylib φ D 0 I 0 M j = 0 M D j = I
15 14 simprd φ j = 0 M D j = I
16 15 ad2antrr φ D 0 = P 1 ¬ k 1 M D k j = 0 M D j = I
17 ralnex k 1 M ¬ D k ¬ k 1 M D k
18 nn0uz 0 = 0
19 2 18 eleqtrdi φ M 0
20 19 ad2antrr φ D 0 = P 1 k 1 M ¬ D k M 0
21 fzsscn 0 I
22 ssrab2 c 0 I 0 M | j = 0 M c j = I 0 I 0 M
23 8 22 eqsstrdi φ C I 0 I 0 M
24 23 7 sseldd φ D 0 I 0 M
25 elmapi D 0 I 0 M D : 0 M 0 I
26 24 25 syl φ D : 0 M 0 I
27 26 ffvelrnda φ j 0 M D j 0 I
28 21 27 sseldi φ j 0 M D j
29 28 ad4ant14 φ D 0 = P 1 k 1 M ¬ D k j 0 M D j
30 fveq2 j = 0 D j = D 0
31 20 29 30 fsum1p φ D 0 = P 1 k 1 M ¬ D k j = 0 M D j = D 0 + j = 0 + 1 M D j
32 simplr φ D 0 = P 1 k 1 M ¬ D k D 0 = P 1
33 0p1e1 0 + 1 = 1
34 33 oveq1i 0 + 1 M = 1 M
35 34 sumeq1i j = 0 + 1 M D j = j = 1 M D j
36 35 a1i φ k 1 M ¬ D k j = 0 + 1 M D j = j = 1 M D j
37 fveq2 k = j D k = D j
38 37 eleq1d k = j D k D j
39 38 notbid k = j ¬ D k ¬ D j
40 39 rspccva k 1 M ¬ D k j 1 M ¬ D j
41 40 adantll φ k 1 M ¬ D k j 1 M ¬ D j
42 fzssnn0 0 I 0
43 fz1ssfz0 1 M 0 M
44 43 sseli j 1 M j 0 M
45 44 27 sylan2 φ j 1 M D j 0 I
46 42 45 sseldi φ j 1 M D j 0
47 elnn0 D j 0 D j D j = 0
48 46 47 sylib φ j 1 M D j D j = 0
49 48 adantlr φ k 1 M ¬ D k j 1 M D j D j = 0
50 orel1 ¬ D j D j D j = 0 D j = 0
51 41 49 50 sylc φ k 1 M ¬ D k j 1 M D j = 0
52 51 sumeq2dv φ k 1 M ¬ D k j = 1 M D j = j = 1 M 0
53 fzfi 1 M Fin
54 53 olci 1 M A 1 M Fin
55 sumz 1 M A 1 M Fin j = 1 M 0 = 0
56 54 55 mp1i φ k 1 M ¬ D k j = 1 M 0 = 0
57 36 52 56 3eqtrd φ k 1 M ¬ D k j = 0 + 1 M D j = 0
58 57 adantlr φ D 0 = P 1 k 1 M ¬ D k j = 0 + 1 M D j = 0
59 32 58 oveq12d φ D 0 = P 1 k 1 M ¬ D k D 0 + j = 0 + 1 M D j = P - 1 + 0
60 nnm1nn0 P P 1 0
61 1 60 syl φ P 1 0
62 61 nn0red φ P 1
63 62 recnd φ P 1
64 63 addid1d φ P - 1 + 0 = P 1
65 64 ad2antrr φ D 0 = P 1 k 1 M ¬ D k P - 1 + 0 = P 1
66 31 59 65 3eqtrd φ D 0 = P 1 k 1 M ¬ D k j = 0 M D j = P 1
67 4 necomd φ P 1 I
68 67 ad2antrr φ D 0 = P 1 k 1 M ¬ D k P 1 I
69 66 68 eqnetrd φ D 0 = P 1 k 1 M ¬ D k j = 0 M D j I
70 69 neneqd φ D 0 = P 1 k 1 M ¬ D k ¬ j = 0 M D j = I
71 17 70 sylan2br φ D 0 = P 1 ¬ k 1 M D k ¬ j = 0 M D j = I
72 16 71 condan φ D 0 = P 1 k 1 M D k
73 1 nnzd φ P
74 15 eqcomd φ I = j = 0 M D j
75 74 fveq2d φ I ! = j = 0 M D j !
76 75 oveq1d φ I ! j = 0 M D j ! = j = 0 M D j ! j = 0 M D j !
77 nfcv _ j D
78 fzfid φ 0 M Fin
79 nn0ex 0 V
80 mapss 0 V 0 I 0 0 I 0 M 0 0 M
81 79 42 80 mp2an 0 I 0 M 0 0 M
82 81 24 sseldi φ D 0 0 M
83 77 78 82 mccl φ j = 0 M D j ! j = 0 M D j !
84 76 83 eqeltrd φ I ! j = 0 M D j !
85 84 nnzd φ I ! j = 0 M D j !
86 fzfid φ 1 M Fin
87 1 adantr φ j 1 M P
88 26 adantr φ j 1 M D : 0 M 0 I
89 44 adantl φ j 1 M j 0 M
90 0zd φ 0
91 5 90 eqeltrd φ J
92 91 adantr φ j 1 M J
93 87 88 89 92 etransclem3 φ j 1 M if P < D j 0 P ! P D j ! J j P D j
94 86 93 fprodzcl φ j = 1 M if P < D j 0 P ! P D j ! J j P D j
95 73 85 94 3jca φ P I ! j = 0 M D j ! j = 1 M if P < D j 0 P ! P D j ! J j P D j
96 95 3ad2ant1 φ k 1 M D k P I ! j = 0 M D j ! j = 1 M if P < D j 0 P ! P D j ! J j P D j
97 73 adantr φ k 1 M P
98 1 adantr φ k 1 M P
99 26 adantr φ k 1 M D : 0 M 0 I
100 43 sseli k 1 M k 0 M
101 100 adantl φ k 1 M k 0 M
102 91 adantr φ k 1 M J
103 98 99 101 102 etransclem3 φ k 1 M if P < D k 0 P ! P D k ! J k P D k
104 difss 1 M k 1 M
105 ssfi 1 M Fin 1 M k 1 M 1 M k Fin
106 53 104 105 mp2an 1 M k Fin
107 106 a1i φ 1 M k Fin
108 1 adantr φ j 1 M k P
109 26 adantr φ j 1 M k D : 0 M 0 I
110 104 43 sstri 1 M k 0 M
111 110 sseli j 1 M k j 0 M
112 111 adantl φ j 1 M k j 0 M
113 91 adantr φ j 1 M k J
114 108 109 112 113 etransclem3 φ j 1 M k if P < D j 0 P ! P D j ! J j P D j
115 107 114 fprodzcl φ j 1 M k if P < D j 0 P ! P D j ! J j P D j
116 115 adantr φ k 1 M j 1 M k if P < D j 0 P ! P D j ! J j P D j
117 97 103 116 3jca φ k 1 M P if P < D k 0 P ! P D k ! J k P D k j 1 M k if P < D j 0 P ! P D j ! J j P D j
118 117 3adant3 φ k 1 M D k P if P < D k 0 P ! P D k ! J k P D k j 1 M k if P < D j 0 P ! P D j ! J j P D j
119 dvds0 P P 0
120 73 119 syl φ P 0
121 120 adantr φ P < D k P 0
122 121 3ad2antl1 φ k 1 M D k P < D k P 0
123 iftrue P < D k if P < D k 0 P ! P D k ! J k P D k = 0
124 123 eqcomd P < D k 0 = if P < D k 0 P ! P D k ! J k P D k
125 124 adantl φ k 1 M D k P < D k 0 = if P < D k 0 P ! P D k ! J k P D k
126 122 125 breqtrd φ k 1 M D k P < D k P if P < D k 0 P ! P D k ! J k P D k
127 97 adantr φ k 1 M ¬ P < D k P
128 0zd φ k 1 M 0
129 99 101 ffvelrnd φ k 1 M D k 0 I
130 129 elfzelzd φ k 1 M D k
131 97 130 zsubcld φ k 1 M P D k
132 128 97 131 3jca φ k 1 M 0 P P D k
133 132 adantr φ k 1 M ¬ P < D k 0 P P D k
134 fzssre 0 I
135 134 129 sseldi φ k 1 M D k
136 135 adantr φ k 1 M ¬ P < D k D k
137 127 zred φ k 1 M ¬ P < D k P
138 simpr φ k 1 M ¬ P < D k ¬ P < D k
139 136 137 138 nltled φ k 1 M ¬ P < D k D k P
140 137 136 subge0d φ k 1 M ¬ P < D k 0 P D k D k P
141 139 140 mpbird φ k 1 M ¬ P < D k 0 P D k
142 elfzle1 D k 0 I 0 D k
143 129 142 syl φ k 1 M 0 D k
144 143 adantr φ k 1 M ¬ P < D k 0 D k
145 137 136 subge02d φ k 1 M ¬ P < D k 0 D k P D k P
146 144 145 mpbid φ k 1 M ¬ P < D k P D k P
147 133 141 146 jca32 φ k 1 M ¬ P < D k 0 P P D k 0 P D k P D k P
148 elfz2 P D k 0 P 0 P P D k 0 P D k P D k P
149 147 148 sylibr φ k 1 M ¬ P < D k P D k 0 P
150 permnn P D k 0 P P ! P D k !
151 149 150 syl φ k 1 M ¬ P < D k P ! P D k !
152 151 nnzd φ k 1 M ¬ P < D k P ! P D k !
153 101 elfzelzd φ k 1 M k
154 102 153 zsubcld φ k 1 M J k
155 154 adantr φ k 1 M ¬ P < D k J k
156 131 adantr φ k 1 M ¬ P < D k P D k
157 elnn0z P D k 0 P D k 0 P D k
158 156 141 157 sylanbrc φ k 1 M ¬ P < D k P D k 0
159 zexpcl J k P D k 0 J k P D k
160 155 158 159 syl2anc φ k 1 M ¬ P < D k J k P D k
161 127 152 160 3jca φ k 1 M ¬ P < D k P P ! P D k ! J k P D k
162 161 3adantl3 φ k 1 M D k ¬ P < D k P P ! P D k ! J k P D k
163 127 3adantl3 φ k 1 M D k ¬ P < D k P
164 61 nn0zd φ P 1
165 164 adantr φ k 1 M P 1
166 128 165 131 3jca φ k 1 M 0 P 1 P D k
167 166 3adant3 φ k 1 M D k 0 P 1 P D k
168 167 adantr φ k 1 M D k ¬ P < D k 0 P 1 P D k
169 141 3adantl3 φ k 1 M D k ¬ P < D k 0 P D k
170 1red φ D k 1
171 nnre D k D k
172 171 adantl φ D k D k
173 1 nnred φ P
174 173 adantr φ D k P
175 nnge1 D k 1 D k
176 175 adantl φ D k 1 D k
177 170 172 174 176 lesub2dd φ D k P D k P 1
178 177 3adant2 φ k 1 M D k P D k P 1
179 178 adantr φ k 1 M D k ¬ P < D k P D k P 1
180 168 169 179 jca32 φ k 1 M D k ¬ P < D k 0 P 1 P D k 0 P D k P D k P 1
181 elfz2 P D k 0 P 1 0 P 1 P D k 0 P D k P D k P 1
182 180 181 sylibr φ k 1 M D k ¬ P < D k P D k 0 P 1
183 permnn P D k 0 P 1 P 1 ! P D k !
184 182 183 syl φ k 1 M D k ¬ P < D k P 1 ! P D k !
185 184 nnzd φ k 1 M D k ¬ P < D k P 1 ! P D k !
186 dvdsmul1 P P 1 ! P D k ! P P P 1 ! P D k !
187 163 185 186 syl2anc φ k 1 M D k ¬ P < D k P P P 1 ! P D k !
188 1 nncnd φ P
189 1cnd φ 1
190 188 189 npcand φ P - 1 + 1 = P
191 190 eqcomd φ P = P - 1 + 1
192 191 fveq2d φ P ! = P - 1 + 1 !
193 facp1 P 1 0 P - 1 + 1 ! = P 1 ! P - 1 + 1
194 61 193 syl φ P - 1 + 1 ! = P 1 ! P - 1 + 1
195 190 oveq2d φ P 1 ! P - 1 + 1 = P 1 ! P
196 61 faccld φ P 1 !
197 196 nncnd φ P 1 !
198 197 188 mulcomd φ P 1 ! P = P P 1 !
199 195 198 eqtrd φ P 1 ! P - 1 + 1 = P P 1 !
200 192 194 199 3eqtrd φ P ! = P P 1 !
201 200 oveq1d φ P ! P D k ! = P P 1 ! P D k !
202 201 adantr φ ¬ P < D k P ! P D k ! = P P 1 ! P D k !
203 202 3ad2antl1 φ k 1 M D k ¬ P < D k P ! P D k ! = P P 1 ! P D k !
204 188 ad2antrr φ k 1 M ¬ P < D k P
205 197 ad2antrr φ k 1 M ¬ P < D k P 1 !
206 158 faccld φ k 1 M ¬ P < D k P D k !
207 206 nncnd φ k 1 M ¬ P < D k P D k !
208 206 nnne0d φ k 1 M ¬ P < D k P D k ! 0
209 204 205 207 208 divassd φ k 1 M ¬ P < D k P P 1 ! P D k ! = P P 1 ! P D k !
210 209 3adantl3 φ k 1 M D k ¬ P < D k P P 1 ! P D k ! = P P 1 ! P D k !
211 203 210 eqtr2d φ k 1 M D k ¬ P < D k P P 1 ! P D k ! = P ! P D k !
212 187 211 breqtrd φ k 1 M D k ¬ P < D k P P ! P D k !
213 dvdsmultr1 P P ! P D k ! J k P D k P P ! P D k ! P P ! P D k ! J k P D k
214 162 212 213 sylc φ k 1 M D k ¬ P < D k P P ! P D k ! J k P D k
215 iffalse ¬ P < D k if P < D k 0 P ! P D k ! J k P D k = P ! P D k ! J k P D k
216 215 adantl φ k 1 M D k ¬ P < D k if P < D k 0 P ! P D k ! J k P D k = P ! P D k ! J k P D k
217 214 216 breqtrrd φ k 1 M D k ¬ P < D k P if P < D k 0 P ! P D k ! J k P D k
218 126 217 pm2.61dan φ k 1 M D k P if P < D k 0 P ! P D k ! J k P D k
219 dvdsmultr1 P if P < D k 0 P ! P D k ! J k P D k j 1 M k if P < D j 0 P ! P D j ! J j P D j P if P < D k 0 P ! P D k ! J k P D k P if P < D k 0 P ! P D k ! J k P D k j 1 M k if P < D j 0 P ! P D j ! J j P D j
220 118 218 219 sylc φ k 1 M D k P if P < D k 0 P ! P D k ! J k P D k j 1 M k if P < D j 0 P ! P D j ! J j P D j
221 fzfid φ k 1 M D k 1 M Fin
222 93 zcnd φ j 1 M if P < D j 0 P ! P D j ! J j P D j
223 222 3ad2antl1 φ k 1 M D k j 1 M if P < D j 0 P ! P D j ! J j P D j
224 simp2 φ k 1 M D k k 1 M
225 fveq2 j = k D j = D k
226 225 breq2d j = k P < D j P < D k
227 225 oveq2d j = k P D j = P D k
228 227 fveq2d j = k P D j ! = P D k !
229 228 oveq2d j = k P ! P D j ! = P ! P D k !
230 oveq2 j = k J j = J k
231 230 227 oveq12d j = k J j P D j = J k P D k
232 229 231 oveq12d j = k P ! P D j ! J j P D j = P ! P D k ! J k P D k
233 226 232 ifbieq2d j = k if P < D j 0 P ! P D j ! J j P D j = if P < D k 0 P ! P D k ! J k P D k
234 233 adantl φ k 1 M D k j = k if P < D j 0 P ! P D j ! J j P D j = if P < D k 0 P ! P D k ! J k P D k
235 221 223 224 234 fprodsplit1 φ k 1 M D k j = 1 M if P < D j 0 P ! P D j ! J j P D j = if P < D k 0 P ! P D k ! J k P D k j 1 M k if P < D j 0 P ! P D j ! J j P D j
236 220 235 breqtrrd φ k 1 M D k P j = 1 M if P < D j 0 P ! P D j ! J j P D j
237 dvdsmultr2 P I ! j = 0 M D j ! j = 1 M if P < D j 0 P ! P D j ! J j P D j P j = 1 M if P < D j 0 P ! P D j ! J j P D j P I ! j = 0 M D j ! j = 1 M if P < D j 0 P ! P D j ! J j P D j
238 96 236 237 sylc φ k 1 M D k P I ! j = 0 M D j ! j = 1 M if P < D j 0 P ! P D j ! J j P D j
239 238 3adant1r φ D 0 = P 1 k 1 M D k P I ! j = 0 M D j ! j = 1 M if P < D j 0 P ! P D j ! J j P D j
240 simpr φ D 0 = P 1 D 0 = P 1
241 eluzfz1 M 0 0 0 M
242 19 241 syl φ 0 0 M
243 26 242 ffvelrnd φ D 0 0 I
244 134 243 sseldi φ D 0
245 244 adantr φ D 0 = P 1 D 0
246 62 adantr φ D 0 = P 1 P 1
247 245 246 lttri3d φ D 0 = P 1 D 0 = P 1 ¬ D 0 < P 1 ¬ P 1 < D 0
248 240 247 mpbid φ D 0 = P 1 ¬ D 0 < P 1 ¬ P 1 < D 0
249 248 simprd φ D 0 = P 1 ¬ P 1 < D 0
250 249 iffalsed φ D 0 = P 1 if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 = P 1 ! P - 1 - D 0 ! J P - 1 - D 0
251 oveq2 D 0 = P 1 P - 1 - D 0 = P - 1 - P 1
252 63 subidd φ P - 1 - P 1 = 0
253 251 252 sylan9eqr φ D 0 = P 1 P - 1 - D 0 = 0
254 253 fveq2d φ D 0 = P 1 P - 1 - D 0 ! = 0 !
255 fac0 0 ! = 1
256 254 255 eqtrdi φ D 0 = P 1 P - 1 - D 0 ! = 1
257 256 oveq2d φ D 0 = P 1 P 1 ! P - 1 - D 0 ! = P 1 ! 1
258 197 div1d φ P 1 ! 1 = P 1 !
259 258 adantr φ D 0 = P 1 P 1 ! 1 = P 1 !
260 257 259 eqtrd φ D 0 = P 1 P 1 ! P - 1 - D 0 ! = P 1 !
261 253 oveq2d φ D 0 = P 1 J P - 1 - D 0 = J 0
262 91 zcnd φ J
263 262 exp0d φ J 0 = 1
264 263 adantr φ D 0 = P 1 J 0 = 1
265 261 264 eqtrd φ D 0 = P 1 J P - 1 - D 0 = 1
266 260 265 oveq12d φ D 0 = P 1 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 = P 1 ! 1
267 197 mulid1d φ P 1 ! 1 = P 1 !
268 267 adantr φ D 0 = P 1 P 1 ! 1 = P 1 !
269 250 266 268 3eqtrd φ D 0 = P 1 if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 = P 1 !
270 269 oveq1d φ D 0 = P 1 if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! J j P D j = P 1 ! j = 1 M if P < D j 0 P ! P D j ! J j P D j
271 270 oveq2d φ D 0 = P 1 I ! j = 0 M D j ! if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! J j P D j = I ! j = 0 M D j ! P 1 ! j = 1 M if P < D j 0 P ! P D j ! J j P D j
272 271 oveq1d φ D 0 = P 1 I ! j = 0 M D j ! if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! J j P D j P 1 ! = I ! j = 0 M D j ! P 1 ! j = 1 M if P < D j 0 P ! P D j ! J j P D j P 1 !
273 84 nncnd φ I ! j = 0 M D j !
274 94 zcnd φ j = 1 M if P < D j 0 P ! P D j ! J j P D j
275 197 274 mulcld φ P 1 ! j = 1 M if P < D j 0 P ! P D j ! J j P D j
276 196 nnne0d φ P 1 ! 0
277 273 275 197 276 divassd φ I ! j = 0 M D j ! P 1 ! j = 1 M if P < D j 0 P ! P D j ! J j P D j P 1 ! = I ! j = 0 M D j ! P 1 ! j = 1 M if P < D j 0 P ! P D j ! J j P D j P 1 !
278 277 adantr φ D 0 = P 1 I ! j = 0 M D j ! P 1 ! j = 1 M if P < D j 0 P ! P D j ! J j P D j P 1 ! = I ! j = 0 M D j ! P 1 ! j = 1 M if P < D j 0 P ! P D j ! J j P D j P 1 !
279 274 197 276 divcan3d φ P 1 ! j = 1 M if P < D j 0 P ! P D j ! J j P D j P 1 ! = j = 1 M if P < D j 0 P ! P D j ! J j P D j
280 279 oveq2d φ I ! j = 0 M D j ! P 1 ! j = 1 M if P < D j 0 P ! P D j ! J j P D j P 1 ! = I ! j = 0 M D j ! j = 1 M if P < D j 0 P ! P D j ! J j P D j
281 280 adantr φ D 0 = P 1 I ! j = 0 M D j ! P 1 ! j = 1 M if P < D j 0 P ! P D j ! J j P D j P 1 ! = I ! j = 0 M D j ! j = 1 M if P < D j 0 P ! P D j ! J j P D j
282 272 278 281 3eqtrd φ D 0 = P 1 I ! j = 0 M D j ! if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! J j P D j P 1 ! = I ! j = 0 M D j ! j = 1 M if P < D j 0 P ! P D j ! J j P D j
283 282 3ad2ant1 φ D 0 = P 1 k 1 M D k I ! j = 0 M D j ! if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! J j P D j P 1 ! = I ! j = 0 M D j ! j = 1 M if P < D j 0 P ! P D j ! J j P D j
284 239 283 breqtrrd φ D 0 = P 1 k 1 M D k P I ! j = 0 M D j ! if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! J j P D j P 1 !
285 284 rexlimdv3a φ D 0 = P 1 k 1 M D k P I ! j = 0 M D j ! if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! J j P D j P 1 !
286 72 285 mpd φ D 0 = P 1 P I ! j = 0 M D j ! if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! J j P D j P 1 !
287 120 adantr φ D 0 P 1 P 0
288 simpr φ D 0 P 1 P 1 < D 0 P 1 < D 0
289 288 iftrued φ D 0 P 1 P 1 < D 0 if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 = 0
290 simpr φ D 0 P 1 ¬ P 1 < D 0 ¬ P 1 < D 0
291 290 iffalsed φ D 0 P 1 ¬ P 1 < D 0 if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 = P 1 ! P - 1 - D 0 ! J P - 1 - D 0
292 simpll φ D 0 P 1 ¬ P 1 < D 0 φ
293 244 ad2antrr φ D 0 P 1 ¬ P 1 < D 0 D 0
294 62 ad2antrr φ D 0 P 1 ¬ P 1 < D 0 P 1
295 293 294 290 nltled φ D 0 P 1 ¬ P 1 < D 0 D 0 P 1
296 id D 0 P 1 D 0 P 1
297 296 necomd D 0 P 1 P 1 D 0
298 297 ad2antlr φ D 0 P 1 ¬ P 1 < D 0 P 1 D 0
299 293 294 295 298 leneltd φ D 0 P 1 ¬ P 1 < D 0 D 0 < P 1
300 5 oveq1d φ J P - 1 - D 0 = 0 P - 1 - D 0
301 300 adantr φ D 0 < P 1 J P - 1 - D 0 = 0 P - 1 - D 0
302 243 elfzelzd φ D 0
303 164 302 zsubcld φ P - 1 - D 0
304 303 adantr φ D 0 < P 1 P - 1 - D 0
305 simpr φ D 0 < P 1 D 0 < P 1
306 244 adantr φ D 0 < P 1 D 0
307 62 adantr φ D 0 < P 1 P 1
308 306 307 posdifd φ D 0 < P 1 D 0 < P 1 0 < P - 1 - D 0
309 305 308 mpbid φ D 0 < P 1 0 < P - 1 - D 0
310 elnnz P - 1 - D 0 P - 1 - D 0 0 < P - 1 - D 0
311 304 309 310 sylanbrc φ D 0 < P 1 P - 1 - D 0
312 311 0expd φ D 0 < P 1 0 P - 1 - D 0 = 0
313 301 312 eqtrd φ D 0 < P 1 J P - 1 - D 0 = 0
314 313 oveq2d φ D 0 < P 1 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 = P 1 ! P - 1 - D 0 ! 0
315 197 adantr φ D 0 < P 1 P 1 !
316 311 nnnn0d φ D 0 < P 1 P - 1 - D 0 0
317 316 faccld φ D 0 < P 1 P - 1 - D 0 !
318 317 nncnd φ D 0 < P 1 P - 1 - D 0 !
319 317 nnne0d φ D 0 < P 1 P - 1 - D 0 ! 0
320 315 318 319 divcld φ D 0 < P 1 P 1 ! P - 1 - D 0 !
321 320 mul01d φ D 0 < P 1 P 1 ! P - 1 - D 0 ! 0 = 0
322 314 321 eqtrd φ D 0 < P 1 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 = 0
323 292 299 322 syl2anc φ D 0 P 1 ¬ P 1 < D 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 = 0
324 291 323 eqtrd φ D 0 P 1 ¬ P 1 < D 0 if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 = 0
325 289 324 pm2.61dan φ D 0 P 1 if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 = 0
326 325 oveq1d φ D 0 P 1 if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! J j P D j = 0 j = 1 M if P < D j 0 P ! P D j ! J j P D j
327 274 mul02d φ 0 j = 1 M if P < D j 0 P ! P D j ! J j P D j = 0
328 327 adantr φ D 0 P 1 0 j = 1 M if P < D j 0 P ! P D j ! J j P D j = 0
329 326 328 eqtrd φ D 0 P 1 if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! J j P D j = 0
330 329 oveq2d φ D 0 P 1 I ! j = 0 M D j ! if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! J j P D j = I ! j = 0 M D j ! 0
331 273 mul01d φ I ! j = 0 M D j ! 0 = 0
332 331 adantr φ D 0 P 1 I ! j = 0 M D j ! 0 = 0
333 330 332 eqtrd φ D 0 P 1 I ! j = 0 M D j ! if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! J j P D j = 0
334 333 oveq1d φ D 0 P 1 I ! j = 0 M D j ! if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! J j P D j P 1 ! = 0 P 1 !
335 197 276 div0d φ 0 P 1 ! = 0
336 335 adantr φ D 0 P 1 0 P 1 ! = 0
337 334 336 eqtrd φ D 0 P 1 I ! j = 0 M D j ! if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! J j P D j P 1 ! = 0
338 287 337 breqtrrd φ D 0 P 1 P I ! j = 0 M D j ! if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! J j P D j P 1 !
339 286 338 pm2.61dane φ P I ! j = 0 M D j ! if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! J P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! J j P D j P 1 !