Metamath Proof Explorer


Theorem etransclem35

Description: P does not divide the P-1 -th derivative of F applied to 0 . This is case 2 of the proof in Juillerat p. 13 . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem35.p φ P
etransclem35.m φ M 0
etransclem35.f F = x x P 1 j = 1 M x j P
etransclem35.c C = n 0 c 0 n 0 M | j = 0 M c j = n
etransclem35.d D = j 0 M if j = 0 P 1 0
Assertion etransclem35 φ D n F P 1 0 = P 1 ! j = 1 M j P

Proof

Step Hyp Ref Expression
1 etransclem35.p φ P
2 etransclem35.m φ M 0
3 etransclem35.f F = x x P 1 j = 1 M x j P
4 etransclem35.c C = n 0 c 0 n 0 M | j = 0 M c j = n
5 etransclem35.d D = j 0 M if j = 0 P 1 0
6 reelprrecn
7 6 a1i φ
8 reopn topGen ran .
9 eqid TopOpen fld = TopOpen fld
10 9 tgioo2 topGen ran . = TopOpen fld 𝑡
11 8 10 eleqtri TopOpen fld 𝑡
12 11 a1i φ TopOpen fld 𝑡
13 nnm1nn0 P P 1 0
14 1 13 syl φ P 1 0
15 etransclem5 k 0 M y y k if k = 0 P 1 P = j 0 M x x j if j = 0 P 1 P
16 0red φ 0
17 7 12 1 2 3 14 15 4 16 etransclem31 φ D n F P 1 0 = c C P 1 P 1 ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! 0 j P c j
18 nfv c φ
19 nfcv _ c P 1 ! j = 0 M D j ! if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! 0 P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! 0 j P D j
20 4 14 etransclem16 φ C P 1 Fin
21 simpr φ c C P 1 c C P 1
22 4 14 etransclem12 φ C P 1 = c 0 P 1 0 M | j = 0 M c j = P 1
23 22 adantr φ c C P 1 C P 1 = c 0 P 1 0 M | j = 0 M c j = P 1
24 21 23 eleqtrd φ c C P 1 c c 0 P 1 0 M | j = 0 M c j = P 1
25 rabid c c 0 P 1 0 M | j = 0 M c j = P 1 c 0 P 1 0 M j = 0 M c j = P 1
26 24 25 sylib φ c C P 1 c 0 P 1 0 M j = 0 M c j = P 1
27 26 simprd φ c C P 1 j = 0 M c j = P 1
28 27 eqcomd φ c C P 1 P 1 = j = 0 M c j
29 28 fveq2d φ c C P 1 P 1 ! = j = 0 M c j !
30 29 oveq1d φ c C P 1 P 1 ! j = 0 M c j ! = j = 0 M c j ! j = 0 M c j !
31 nfcv _ j c
32 fzfid φ c C P 1 0 M Fin
33 nn0ex 0 V
34 fzssnn0 0 P 1 0
35 mapss 0 V 0 P 1 0 0 P 1 0 M 0 0 M
36 33 34 35 mp2an 0 P 1 0 M 0 0 M
37 26 simpld φ c C P 1 c 0 P 1 0 M
38 36 37 sseldi φ c C P 1 c 0 0 M
39 31 32 38 mccl φ c C P 1 j = 0 M c j ! j = 0 M c j !
40 30 39 eqeltrd φ c C P 1 P 1 ! j = 0 M c j !
41 40 nnzd φ c C P 1 P 1 ! j = 0 M c j !
42 1 adantr φ c C P 1 P
43 2 adantr φ c C P 1 M 0
44 elmapi c 0 P 1 0 M c : 0 M 0 P 1
45 37 44 syl φ c C P 1 c : 0 M 0 P 1
46 0zd φ c C P 1 0
47 42 43 45 46 etransclem10 φ c C P 1 if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0
48 fzfid φ c C P 1 1 M Fin
49 1 ad2antrr φ c C P 1 j 1 M P
50 45 adantr φ c C P 1 j 1 M c : 0 M 0 P 1
51 fz1ssfz0 1 M 0 M
52 51 sseli j 1 M j 0 M
53 52 adantl φ c C P 1 j 1 M j 0 M
54 0zd φ c C P 1 j 1 M 0
55 49 50 53 54 etransclem3 φ c C P 1 j 1 M if P < c j 0 P ! P c j ! 0 j P c j
56 48 55 fprodzcl φ c C P 1 j = 1 M if P < c j 0 P ! P c j ! 0 j P c j
57 47 56 zmulcld φ c C P 1 if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! 0 j P c j
58 41 57 zmulcld φ c C P 1 P 1 ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! 0 j P c j
59 58 zcnd φ c C P 1 P 1 ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! 0 j P c j
60 nn0uz 0 = 0
61 14 60 eleqtrdi φ P 1 0
62 eluzfz2 P 1 0 P 1 0 P 1
63 61 62 syl φ P 1 0 P 1
64 eluzfz1 P 1 0 0 0 P 1
65 61 64 syl φ 0 0 P 1
66 63 65 ifcld φ if j = 0 P 1 0 0 P 1
67 66 adantr φ j 0 M if j = 0 P 1 0 0 P 1
68 67 5 fmptd φ D : 0 M 0 P 1
69 ovex 0 P 1 V
70 ovex 0 M V
71 69 70 elmap D 0 P 1 0 M D : 0 M 0 P 1
72 68 71 sylibr φ D 0 P 1 0 M
73 2 60 eleqtrdi φ M 0
74 fzsscn 0 P 1
75 68 ffvelrnda φ j 0 M D j 0 P 1
76 74 75 sseldi φ j 0 M D j
77 fveq2 j = 0 D j = D 0
78 73 76 77 fsum1p φ j = 0 M D j = D 0 + j = 0 + 1 M D j
79 5 a1i φ D = j 0 M if j = 0 P 1 0
80 simpr φ j = 0 j = 0
81 80 iftrued φ j = 0 if j = 0 P 1 0 = P 1
82 eluzfz1 M 0 0 0 M
83 73 82 syl φ 0 0 M
84 79 81 83 14 fvmptd φ D 0 = P 1
85 0p1e1 0 + 1 = 1
86 85 oveq1i 0 + 1 M = 1 M
87 86 sumeq1i j = 0 + 1 M D j = j = 1 M D j
88 87 a1i φ j = 0 + 1 M D j = j = 1 M D j
89 5 fvmpt2 j 0 M if j = 0 P 1 0 0 P 1 D j = if j = 0 P 1 0
90 52 66 89 syl2anr φ j 1 M D j = if j = 0 P 1 0
91 0red j 1 M 0
92 1red j 1 M 1
93 elfzelz j 1 M j
94 93 zred j 1 M j
95 0lt1 0 < 1
96 95 a1i j 1 M 0 < 1
97 elfzle1 j 1 M 1 j
98 91 92 94 96 97 ltletrd j 1 M 0 < j
99 91 98 gtned j 1 M j 0
100 99 neneqd j 1 M ¬ j = 0
101 100 iffalsed j 1 M if j = 0 P 1 0 = 0
102 101 adantl φ j 1 M if j = 0 P 1 0 = 0
103 90 102 eqtrd φ j 1 M D j = 0
104 103 sumeq2dv φ j = 1 M D j = j = 1 M 0
105 fzfi 1 M Fin
106 105 olci 1 M A 1 M Fin
107 sumz 1 M A 1 M Fin j = 1 M 0 = 0
108 106 107 mp1i φ j = 1 M 0 = 0
109 88 104 108 3eqtrd φ j = 0 + 1 M D j = 0
110 84 109 oveq12d φ D 0 + j = 0 + 1 M D j = P - 1 + 0
111 1 nncnd φ P
112 1cnd φ 1
113 111 112 subcld φ P 1
114 113 addid1d φ P - 1 + 0 = P 1
115 78 110 114 3eqtrd φ j = 0 M D j = P 1
116 fveq1 c = D c j = D j
117 116 sumeq2sdv c = D j = 0 M c j = j = 0 M D j
118 117 eqeq1d c = D j = 0 M c j = P 1 j = 0 M D j = P 1
119 118 elrab D c 0 P 1 0 M | j = 0 M c j = P 1 D 0 P 1 0 M j = 0 M D j = P 1
120 72 115 119 sylanbrc φ D c 0 P 1 0 M | j = 0 M c j = P 1
121 120 22 eleqtrrd φ D C P 1
122 116 fveq2d c = D c j ! = D j !
123 122 prodeq2ad c = D j = 0 M c j ! = j = 0 M D j !
124 123 oveq2d c = D P 1 ! j = 0 M c j ! = P 1 ! j = 0 M D j !
125 fveq1 c = D c 0 = D 0
126 125 breq2d c = D P 1 < c 0 P 1 < D 0
127 125 oveq2d c = D P - 1 - c 0 = P - 1 - D 0
128 127 fveq2d c = D P - 1 - c 0 ! = P - 1 - D 0 !
129 128 oveq2d c = D P 1 ! P - 1 - c 0 ! = P 1 ! P - 1 - D 0 !
130 127 oveq2d c = D 0 P - 1 - c 0 = 0 P - 1 - D 0
131 129 130 oveq12d c = D P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0 = P 1 ! P - 1 - D 0 ! 0 P - 1 - D 0
132 126 131 ifbieq2d c = D if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0 = if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! 0 P - 1 - D 0
133 116 breq2d c = D P < c j P < D j
134 116 oveq2d c = D P c j = P D j
135 134 fveq2d c = D P c j ! = P D j !
136 135 oveq2d c = D P ! P c j ! = P ! P D j !
137 134 oveq2d c = D 0 j P c j = 0 j P D j
138 136 137 oveq12d c = D P ! P c j ! 0 j P c j = P ! P D j ! 0 j P D j
139 133 138 ifbieq2d c = D if P < c j 0 P ! P c j ! 0 j P c j = if P < D j 0 P ! P D j ! 0 j P D j
140 139 prodeq2ad c = D j = 1 M if P < c j 0 P ! P c j ! 0 j P c j = j = 1 M if P < D j 0 P ! P D j ! 0 j P D j
141 132 140 oveq12d c = D if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! 0 j P c j = if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! 0 P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! 0 j P D j
142 124 141 oveq12d c = D P 1 ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! 0 j P c j = P 1 ! j = 0 M D j ! if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! 0 P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! 0 j P D j
143 18 19 20 59 121 142 fsumsplit1 φ c C P 1 P 1 ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! 0 j P c j = P 1 ! j = 0 M D j ! if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! 0 P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! 0 j P D j + c C P 1 D P 1 ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! 0 j P c j
144 34 75 sseldi φ j 0 M D j 0
145 144 faccld φ j 0 M D j !
146 145 nncnd φ j 0 M D j !
147 77 fveq2d j = 0 D j ! = D 0 !
148 73 146 147 fprod1p φ j = 0 M D j ! = D 0 ! j = 0 + 1 M D j !
149 84 fveq2d φ D 0 ! = P 1 !
150 86 prodeq1i j = 0 + 1 M D j ! = j = 1 M D j !
151 150 a1i φ j = 0 + 1 M D j ! = j = 1 M D j !
152 103 fveq2d φ j 1 M D j ! = 0 !
153 fac0 0 ! = 1
154 152 153 syl6eq φ j 1 M D j ! = 1
155 154 prodeq2dv φ j = 1 M D j ! = j = 1 M 1
156 prod1 1 M A 1 M Fin j = 1 M 1 = 1
157 106 156 mp1i φ j = 1 M 1 = 1
158 151 155 157 3eqtrd φ j = 0 + 1 M D j ! = 1
159 149 158 oveq12d φ D 0 ! j = 0 + 1 M D j ! = P 1 ! 1
160 14 faccld φ P 1 !
161 160 nncnd φ P 1 !
162 161 mulid1d φ P 1 ! 1 = P 1 !
163 148 159 162 3eqtrd φ j = 0 M D j ! = P 1 !
164 163 oveq2d φ P 1 ! j = 0 M D j ! = P 1 ! P 1 !
165 160 nnne0d φ P 1 ! 0
166 161 165 dividd φ P 1 ! P 1 ! = 1
167 164 166 eqtrd φ P 1 ! j = 0 M D j ! = 1
168 14 nn0red φ P 1
169 84 168 eqeltrd φ D 0
170 169 168 lttri3d φ D 0 = P 1 ¬ D 0 < P 1 ¬ P 1 < D 0
171 84 170 mpbid φ ¬ D 0 < P 1 ¬ P 1 < D 0
172 171 simprd φ ¬ P 1 < D 0
173 172 iffalsed φ if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! 0 P - 1 - D 0 = P 1 ! P - 1 - D 0 ! 0 P - 1 - D 0
174 84 eqcomd φ P 1 = D 0
175 113 174 subeq0bd φ P - 1 - D 0 = 0
176 175 fveq2d φ P - 1 - D 0 ! = 0 !
177 176 153 syl6eq φ P - 1 - D 0 ! = 1
178 177 oveq2d φ P 1 ! P - 1 - D 0 ! = P 1 ! 1
179 161 div1d φ P 1 ! 1 = P 1 !
180 178 179 eqtrd φ P 1 ! P - 1 - D 0 ! = P 1 !
181 175 oveq2d φ 0 P - 1 - D 0 = 0 0
182 0cnd φ 0
183 182 exp0d φ 0 0 = 1
184 181 183 eqtrd φ 0 P - 1 - D 0 = 1
185 180 184 oveq12d φ P 1 ! P - 1 - D 0 ! 0 P - 1 - D 0 = P 1 ! 1
186 173 185 162 3eqtrd φ if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! 0 P - 1 - D 0 = P 1 !
187 fzssre 0 P 1
188 68 adantr φ j 1 M D : 0 M 0 P 1
189 52 adantl φ j 1 M j 0 M
190 188 189 ffvelrnd φ j 1 M D j 0 P 1
191 187 190 sseldi φ j 1 M D j
192 1 nnred φ P
193 192 adantr φ j 1 M P
194 1 nngt0d φ 0 < P
195 16 192 194 ltled φ 0 P
196 195 adantr φ j 1 M 0 P
197 103 196 eqbrtrd φ j 1 M D j P
198 191 193 197 lensymd φ j 1 M ¬ P < D j
199 198 iffalsed φ j 1 M if P < D j 0 P ! P D j ! 0 j P D j = P ! P D j ! 0 j P D j
200 103 oveq2d φ j 1 M P D j = P 0
201 111 adantr φ j 1 M P
202 201 subid1d φ j 1 M P 0 = P
203 200 202 eqtrd φ j 1 M P D j = P
204 203 fveq2d φ j 1 M P D j ! = P !
205 204 oveq2d φ j 1 M P ! P D j ! = P ! P !
206 1 nnnn0d φ P 0
207 206 faccld φ P !
208 207 nncnd φ P !
209 207 nnne0d φ P ! 0
210 208 209 dividd φ P ! P ! = 1
211 210 adantr φ j 1 M P ! P ! = 1
212 205 211 eqtrd φ j 1 M P ! P D j ! = 1
213 df-neg j = 0 j
214 213 eqcomi 0 j = j
215 214 a1i φ j 1 M 0 j = j
216 215 203 oveq12d φ j 1 M 0 j P D j = j P
217 212 216 oveq12d φ j 1 M P ! P D j ! 0 j P D j = 1 j P
218 93 znegcld j 1 M j
219 218 zcnd j 1 M j
220 219 adantl φ j 1 M j
221 206 adantr φ j 1 M P 0
222 220 221 expcld φ j 1 M j P
223 222 mulid2d φ j 1 M 1 j P = j P
224 199 217 223 3eqtrd φ j 1 M if P < D j 0 P ! P D j ! 0 j P D j = j P
225 224 prodeq2dv φ j = 1 M if P < D j 0 P ! P D j ! 0 j P D j = j = 1 M j P
226 186 225 oveq12d φ if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! 0 P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! 0 j P D j = P 1 ! j = 1 M j P
227 167 226 oveq12d φ P 1 ! j = 0 M D j ! if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! 0 P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! 0 j P D j = 1 P 1 ! j = 1 M j P
228 fzfid φ 1 M Fin
229 zexpcl j P 0 j P
230 218 206 229 syl2anr φ j 1 M j P
231 228 230 fprodzcl φ j = 1 M j P
232 231 zcnd φ j = 1 M j P
233 161 232 mulcld φ P 1 ! j = 1 M j P
234 233 mulid2d φ 1 P 1 ! j = 1 M j P = P 1 ! j = 1 M j P
235 227 234 eqtrd φ P 1 ! j = 0 M D j ! if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! 0 P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! 0 j P D j = P 1 ! j = 1 M j P
236 eldifi c C P 1 D c C P 1
237 83 adantr φ c C P 1 0 0 M
238 45 237 ffvelrnd φ c C P 1 c 0 0 P 1
239 236 238 sylan2 φ c C P 1 D c 0 0 P 1
240 187 239 sseldi φ c C P 1 D c 0
241 168 adantr φ c C P 1 D P 1
242 elfzle2 c 0 0 P 1 c 0 P 1
243 239 242 syl φ c C P 1 D c 0 P 1
244 240 241 243 lensymd φ c C P 1 D ¬ P 1 < c 0
245 244 iffalsed φ c C P 1 D if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0 = P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0
246 14 nn0zd φ P 1
247 246 adantr φ c C P 1 D P 1
248 239 elfzelzd φ c C P 1 D c 0
249 247 248 zsubcld φ c C P 1 D P - 1 - c 0
250 45 ffnd φ c C P 1 c Fn 0 M
251 250 adantr φ c C P 1 P 1 = c 0 c Fn 0 M
252 68 ffnd φ D Fn 0 M
253 252 ad2antrr φ c C P 1 P 1 = c 0 D Fn 0 M
254 fveq2 j = 0 c j = c 0
255 254 adantl φ P 1 = c 0 j = 0 c j = c 0
256 id P 1 = c 0 P 1 = c 0
257 256 eqcomd P 1 = c 0 c 0 = P 1
258 257 ad2antlr φ P 1 = c 0 j = 0 c 0 = P 1
259 77 adantl φ j = 0 D j = D 0
260 84 adantr φ j = 0 D 0 = P 1
261 259 260 eqtr2d φ j = 0 P 1 = D j
262 261 adantlr φ P 1 = c 0 j = 0 P 1 = D j
263 255 258 262 3eqtrd φ P 1 = c 0 j = 0 c j = D j
264 263 adantllr φ c C P 1 P 1 = c 0 j = 0 c j = D j
265 264 adantlr φ c C P 1 P 1 = c 0 j 0 M j = 0 c j = D j
266 27 ad4antr φ c C P 1 P 1 = c 0 j 0 M ¬ j = 0 ¬ c j = 0 j = 0 M c j = P 1
267 168 ad5antr φ c C P 1 P 1 = c 0 j 0 M ¬ j = 0 ¬ c j = 0 P 1
268 168 ad4antr φ c C P 1 j 0 M ¬ j = 0 ¬ c j = 0 P 1
269 45 adantr φ c C P 1 k 1 M c : 0 M 0 P 1
270 51 sseli k 1 M k 0 M
271 270 adantl φ c C P 1 k 1 M k 0 M
272 269 271 ffvelrnd φ c C P 1 k 1 M c k 0 P 1
273 34 272 sseldi φ c C P 1 k 1 M c k 0
274 48 273 fsumnn0cl φ c C P 1 k = 1 M c k 0
275 274 nn0red φ c C P 1 k = 1 M c k
276 275 ad3antrrr φ c C P 1 j 0 M ¬ j = 0 ¬ c j = 0 k = 1 M c k
277 0red φ c C P 1 j 0 M ¬ j = 0 ¬ c j = 0 0
278 45 ffvelrnda φ c C P 1 j 0 M c j 0 P 1
279 187 278 sseldi φ c C P 1 j 0 M c j
280 279 ad2antrr φ c C P 1 j 0 M ¬ j = 0 ¬ c j = 0 c j
281 nfv k φ c C P 1 j 0 M ¬ j = 0 ¬ c j = 0
282 nfcv _ k c j
283 fzfid φ c C P 1 j 0 M ¬ j = 0 ¬ c j = 0 1 M Fin
284 simp-4l φ c C P 1 j 0 M ¬ j = 0 ¬ c j = 0 k 1 M φ c C P 1
285 74 272 sseldi φ c C P 1 k 1 M c k
286 284 285 sylancom φ c C P 1 j 0 M ¬ j = 0 ¬ c j = 0 k 1 M c k
287 1zzd j 0 M ¬ j = 0 1
288 elfzel2 j 0 M M
289 288 adantr j 0 M ¬ j = 0 M
290 elfzelz j 0 M j
291 290 adantr j 0 M ¬ j = 0 j
292 287 289 291 3jca j 0 M ¬ j = 0 1 M j
293 elfznn0 j 0 M j 0
294 293 adantr j 0 M ¬ j = 0 j 0
295 neqne ¬ j = 0 j 0
296 295 adantl j 0 M ¬ j = 0 j 0
297 elnnne0 j j 0 j 0
298 294 296 297 sylanbrc j 0 M ¬ j = 0 j
299 298 nnge1d j 0 M ¬ j = 0 1 j
300 elfzle2 j 0 M j M
301 300 adantr j 0 M ¬ j = 0 j M
302 292 299 301 jca32 j 0 M ¬ j = 0 1 M j 1 j j M
303 elfz2 j 1 M 1 M j 1 j j M
304 302 303 sylibr j 0 M ¬ j = 0 j 1 M
305 304 adantr j 0 M ¬ j = 0 ¬ c j = 0 j 1 M
306 305 adantlll φ c C P 1 j 0 M ¬ j = 0 ¬ c j = 0 j 1 M
307 fveq2 k = j c k = c j
308 281 282 283 286 306 307 fsumsplit1 φ c C P 1 j 0 M ¬ j = 0 ¬ c j = 0 k = 1 M c k = c j + k 1 M j c k
309 308 eqcomd φ c C P 1 j 0 M ¬ j = 0 ¬ c j = 0 c j + k 1 M j c k = k = 1 M c k
310 309 276 eqeltrd φ c C P 1 j 0 M ¬ j = 0 ¬ c j = 0 c j + k 1 M j c k
311 elfzle1 c j 0 P 1 0 c j
312 278 311 syl φ c C P 1 j 0 M 0 c j
313 312 ad2antrr φ c C P 1 j 0 M ¬ j = 0 ¬ c j = 0 0 c j
314 neqne ¬ c j = 0 c j 0
315 314 adantl φ c C P 1 j 0 M ¬ j = 0 ¬ c j = 0 c j 0
316 277 280 313 315 leneltd φ c C P 1 j 0 M ¬ j = 0 ¬ c j = 0 0 < c j
317 diffi 1 M Fin 1 M j Fin
318 105 317 mp1i φ c C P 1 1 M j Fin
319 eldifi k 1 M j k 1 M
320 319 adantl φ c C P 1 k 1 M j k 1 M
321 51 320 sseldi φ c C P 1 k 1 M j k 0 M
322 45 ffvelrnda φ c C P 1 k 0 M c k 0 P 1
323 187 322 sseldi φ c C P 1 k 0 M c k
324 321 323 syldan φ c C P 1 k 1 M j c k
325 elfzle1 c k 0 P 1 0 c k
326 322 325 syl φ c C P 1 k 0 M 0 c k
327 321 326 syldan φ c C P 1 k 1 M j 0 c k
328 318 324 327 fsumge0 φ c C P 1 0 k 1 M j c k
329 328 adantr φ c C P 1 j 0 M 0 k 1 M j c k
330 318 324 fsumrecl φ c C P 1 k 1 M j c k
331 330 adantr φ c C P 1 j 0 M k 1 M j c k
332 279 331 addge01d φ c C P 1 j 0 M 0 k 1 M j c k c j c j + k 1 M j c k
333 329 332 mpbid φ c C P 1 j 0 M c j c j + k 1 M j c k
334 333 ad2antrr φ c C P 1 j 0 M ¬ j = 0 ¬ c j = 0 c j c j + k 1 M j c k
335 277 280 310 316 334 ltletrd φ c C P 1 j 0 M ¬ j = 0 ¬ c j = 0 0 < c j + k 1 M j c k
336 335 309 breqtrd φ c C P 1 j 0 M ¬ j = 0 ¬ c j = 0 0 < k = 1 M c k
337 276 336 elrpd φ c C P 1 j 0 M ¬ j = 0 ¬ c j = 0 k = 1 M c k +
338 268 337 ltaddrpd φ c C P 1 j 0 M ¬ j = 0 ¬ c j = 0 P 1 < P - 1 + k = 1 M c k
339 338 adantl3r φ c C P 1 P 1 = c 0 j 0 M ¬ j = 0 ¬ c j = 0 P 1 < P - 1 + k = 1 M c k
340 fveq2 j = k c j = c k
341 340 cbvsumv j = 0 M c j = k = 0 M c k
342 341 a1i φ c C P 1 P 1 = c 0 j 0 M ¬ j = 0 ¬ c j = 0 j = 0 M c j = k = 0 M c k
343 73 ad5antr φ c C P 1 P 1 = c 0 j 0 M ¬ j = 0 ¬ c j = 0 M 0
344 simp-5l φ c C P 1 P 1 = c 0 j 0 M ¬ j = 0 ¬ c j = 0 k 0 M φ c C P 1
345 74 322 sseldi φ c C P 1 k 0 M c k
346 344 345 sylancom φ c C P 1 P 1 = c 0 j 0 M ¬ j = 0 ¬ c j = 0 k 0 M c k
347 fveq2 k = 0 c k = c 0
348 343 346 347 fsum1p φ c C P 1 P 1 = c 0 j 0 M ¬ j = 0 ¬ c j = 0 k = 0 M c k = c 0 + k = 0 + 1 M c k
349 257 ad4antlr φ c C P 1 P 1 = c 0 j 0 M ¬ j = 0 ¬ c j = 0 c 0 = P 1
350 86 sumeq1i k = 0 + 1 M c k = k = 1 M c k
351 350 a1i φ c C P 1 P 1 = c 0 j 0 M ¬ j = 0 ¬ c j = 0 k = 0 + 1 M c k = k = 1 M c k
352 349 351 oveq12d φ c C P 1 P 1 = c 0 j 0 M ¬ j = 0 ¬ c j = 0 c 0 + k = 0 + 1 M c k = P - 1 + k = 1 M c k
353 342 348 352 3eqtrrd φ c C P 1 P 1 = c 0 j 0 M ¬ j = 0 ¬ c j = 0 P - 1 + k = 1 M c k = j = 0 M c j
354 339 353 breqtrd φ c C P 1 P 1 = c 0 j 0 M ¬ j = 0 ¬ c j = 0 P 1 < j = 0 M c j
355 267 354 gtned φ c C P 1 P 1 = c 0 j 0 M ¬ j = 0 ¬ c j = 0 j = 0 M c j P 1
356 355 neneqd φ c C P 1 P 1 = c 0 j 0 M ¬ j = 0 ¬ c j = 0 ¬ j = 0 M c j = P 1
357 266 356 condan φ c C P 1 P 1 = c 0 j 0 M ¬ j = 0 c j = 0
358 simpr φ j 0 M j 0 M
359 34 67 sseldi φ j 0 M if j = 0 P 1 0 0
360 5 fvmpt2 j 0 M if j = 0 P 1 0 0 D j = if j = 0 P 1 0
361 358 359 360 syl2anc φ j 0 M D j = if j = 0 P 1 0
362 361 adantr φ j 0 M ¬ j = 0 D j = if j = 0 P 1 0
363 simpr φ j 0 M ¬ j = 0 ¬ j = 0
364 363 iffalsed φ j 0 M ¬ j = 0 if j = 0 P 1 0 = 0
365 362 364 eqtr2d φ j 0 M ¬ j = 0 0 = D j
366 365 adantllr φ c C P 1 j 0 M ¬ j = 0 0 = D j
367 366 adantllr φ c C P 1 P 1 = c 0 j 0 M ¬ j = 0 0 = D j
368 357 367 eqtrd φ c C P 1 P 1 = c 0 j 0 M ¬ j = 0 c j = D j
369 265 368 pm2.61dan φ c C P 1 P 1 = c 0 j 0 M c j = D j
370 251 253 369 eqfnfvd φ c C P 1 P 1 = c 0 c = D
371 236 370 sylanl2 φ c C P 1 D P 1 = c 0 c = D
372 eldifsni c C P 1 D c D
373 372 neneqd c C P 1 D ¬ c = D
374 373 ad2antlr φ c C P 1 D P 1 = c 0 ¬ c = D
375 371 374 pm2.65da φ c C P 1 D ¬ P 1 = c 0
376 375 neqned φ c C P 1 D P 1 c 0
377 240 241 243 376 leneltd φ c C P 1 D c 0 < P 1
378 240 241 posdifd φ c C P 1 D c 0 < P 1 0 < P - 1 - c 0
379 377 378 mpbid φ c C P 1 D 0 < P - 1 - c 0
380 elnnz P - 1 - c 0 P - 1 - c 0 0 < P - 1 - c 0
381 249 379 380 sylanbrc φ c C P 1 D P - 1 - c 0
382 381 0expd φ c C P 1 D 0 P - 1 - c 0 = 0
383 382 oveq2d φ c C P 1 D P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0 = P 1 ! P - 1 - c 0 ! 0
384 161 adantr φ c C P 1 D P 1 !
385 381 nnnn0d φ c C P 1 D P - 1 - c 0 0
386 385 faccld φ c C P 1 D P - 1 - c 0 !
387 386 nncnd φ c C P 1 D P - 1 - c 0 !
388 386 nnne0d φ c C P 1 D P - 1 - c 0 ! 0
389 384 387 388 divcld φ c C P 1 D P 1 ! P - 1 - c 0 !
390 389 mul01d φ c C P 1 D P 1 ! P - 1 - c 0 ! 0 = 0
391 245 383 390 3eqtrd φ c C P 1 D if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0 = 0
392 391 oveq1d φ c C P 1 D if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! 0 j P c j = 0 j = 1 M if P < c j 0 P ! P c j ! 0 j P c j
393 236 56 sylan2 φ c C P 1 D j = 1 M if P < c j 0 P ! P c j ! 0 j P c j
394 393 zcnd φ c C P 1 D j = 1 M if P < c j 0 P ! P c j ! 0 j P c j
395 394 mul02d φ c C P 1 D 0 j = 1 M if P < c j 0 P ! P c j ! 0 j P c j = 0
396 392 395 eqtrd φ c C P 1 D if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! 0 j P c j = 0
397 396 oveq2d φ c C P 1 D P 1 ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! 0 j P c j = P 1 ! j = 0 M c j ! 0
398 fzfid φ c C P 1 D 0 M Fin
399 34 278 sseldi φ c C P 1 j 0 M c j 0
400 236 399 sylanl2 φ c C P 1 D j 0 M c j 0
401 400 faccld φ c C P 1 D j 0 M c j !
402 398 401 fprodnncl φ c C P 1 D j = 0 M c j !
403 402 nncnd φ c C P 1 D j = 0 M c j !
404 402 nnne0d φ c C P 1 D j = 0 M c j ! 0
405 384 403 404 divcld φ c C P 1 D P 1 ! j = 0 M c j !
406 405 mul01d φ c C P 1 D P 1 ! j = 0 M c j ! 0 = 0
407 397 406 eqtrd φ c C P 1 D P 1 ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! 0 j P c j = 0
408 407 sumeq2dv φ c C P 1 D P 1 ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! 0 j P c j = c C P 1 D 0
409 diffi C P 1 Fin C P 1 D Fin
410 20 409 syl φ C P 1 D Fin
411 410 olcd φ C P 1 D 0 C P 1 D Fin
412 sumz C P 1 D 0 C P 1 D Fin c C P 1 D 0 = 0
413 411 412 syl φ c C P 1 D 0 = 0
414 408 413 eqtrd φ c C P 1 D P 1 ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! 0 j P c j = 0
415 235 414 oveq12d φ P 1 ! j = 0 M D j ! if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! 0 P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! 0 j P D j + c C P 1 D P 1 ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! 0 j P c j = P 1 ! j = 1 M j P + 0
416 233 addid1d φ P 1 ! j = 1 M j P + 0 = P 1 ! j = 1 M j P
417 nfv j φ
418 417 206 228 220 fprodexp φ j = 1 M j P = j = 1 M j P
419 418 oveq2d φ P 1 ! j = 1 M j P = P 1 ! j = 1 M j P
420 415 416 419 3eqtrd φ P 1 ! j = 0 M D j ! if P 1 < D 0 0 P 1 ! P - 1 - D 0 ! 0 P - 1 - D 0 j = 1 M if P < D j 0 P ! P D j ! 0 j P D j + c C P 1 D P 1 ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! 0 P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! 0 j P c j = P 1 ! j = 1 M j P
421 17 143 420 3eqtrd φ D n F P 1 0 = P 1 ! j = 1 M j P