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

Theorem etransclem24 38235
 Description: divides the I -th derivative of applied to . when and is not equal to . 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
etransclem24.m
etransclem24.i
etransclem24.ip
etransclem24.j
etransclem24.c
etransclem24.d
Assertion
Ref Expression
etransclem24
Distinct variable groups:   ,,   ,,   ,   ,,,   ,   ,,
Allowed substitution hints:   ()   (,,)   ()   (,)   ()   (,)

Proof of Theorem etransclem24
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 etransclem24.d . . . . . . . 8
2 etransclem24.c . . . . . . . . 9
3 etransclem24.i . . . . . . . . 9
42, 3etransclem12 38223 . . . . . . . 8
51, 4eleqtrd 2551 . . . . . . 7
6 fveq1 5878 . . . . . . . . . 10
76sumeq2ad 37740 . . . . . . . . 9
87eqeq1d 2473 . . . . . . . 8
98elrab 3184 . . . . . . 7
105, 9sylib 201 . . . . . 6
1110simprd 470 . . . . 5
1211ad2antrr 740 . . . 4
13 ralnex 2834 . . . . 5
14 etransclem24.m . . . . . . . . . . 11
15 nn0uz 11217 . . . . . . . . . . 11
1614, 15syl6eleq 2559 . . . . . . . . . 10
1716ad2antrr 740 . . . . . . . . 9
18 fzsscn 37619 . . . . . . . . . . 11
19 ssrab2 3500 . . . . . . . . . . . . . . 15
204, 19syl6eqss 3468 . . . . . . . . . . . . . 14
2120, 1sseldd 3419 . . . . . . . . . . . . 13
22 elmapi 7511 . . . . . . . . . . . . 13
2321, 22syl 17 . . . . . . . . . . . 12
2423ffvelrnda 6037 . . . . . . . . . . 11
2518, 24sseldi 3416 . . . . . . . . . 10
2625adant423 37430 . . . . . . . . 9
27 fveq2 5879 . . . . . . . . 9
2817, 26, 27fsum1p 13891 . . . . . . . 8
29 simplr 770 . . . . . . . . 9
30 0p1e1 10743 . . . . . . . . . . . . . 14
3130oveq1i 6318 . . . . . . . . . . . . 13
3231sumeq1i 13841 . . . . . . . . . . . 12
3332a1i 11 . . . . . . . . . . 11
34 fveq2 5879 . . . . . . . . . . . . . . . . 17
3534eleq1d 2533 . . . . . . . . . . . . . . . 16
3635notbid 301 . . . . . . . . . . . . . . 15
3736rspccva 3135 . . . . . . . . . . . . . 14
3837adantll 728 . . . . . . . . . . . . 13
39 fzssnn0 37627 . . . . . . . . . . . . . . . 16
40 fz1ssfz0 37616 . . . . . . . . . . . . . . . . . 18
4140sseli 3414 . . . . . . . . . . . . . . . . 17
4241, 24sylan2 482 . . . . . . . . . . . . . . . 16
4339, 42sseldi 3416 . . . . . . . . . . . . . . 15
44 elnn0 10895 . . . . . . . . . . . . . . 15
4543, 44sylib 201 . . . . . . . . . . . . . 14
4645adantlr 729 . . . . . . . . . . . . 13
47 orel1 389 . . . . . . . . . . . . 13
4838, 46, 47sylc 61 . . . . . . . . . . . 12
4948sumeq2dv 13846 . . . . . . . . . . 11
50 fzfi 12223 . . . . . . . . . . . . 13
5150olci 398 . . . . . . . . . . . 12
52 sumz 13865 . . . . . . . . . . . 12
5351, 52mp1i 13 . . . . . . . . . . 11
5433, 49, 533eqtrd 2509 . . . . . . . . . 10
5554adantlr 729 . . . . . . . . 9
5629, 55oveq12d 6326 . . . . . . . 8
57 etransclem24.p . . . . . . . . . . . . 13
58 nnm1nn0 10935 . . . . . . . . . . . . 13
5957, 58syl 17 . . . . . . . . . . . 12
6059nn0red 10950 . . . . . . . . . . 11
6160recnd 9687 . . . . . . . . . 10
6261addid1d 9851 . . . . . . . . 9
6362ad2antrr 740 . . . . . . . 8
6428, 56, 633eqtrd 2509 . . . . . . 7
65 etransclem24.ip . . . . . . . . 9
6665necomd 2698 . . . . . . . 8
6766ad2antrr 740 . . . . . . 7
6864, 67eqnetrd 2710 . . . . . 6
6968neneqd 2648 . . . . 5
7013, 69sylan2br 484 . . . 4
7112, 70condan 811 . . 3
7257nnzd 11062 . . . . . . . . 9
7311eqcomd 2477 . . . . . . . . . . . . 13
7473fveq2d 5883 . . . . . . . . . . . 12
7574oveq1d 6323 . . . . . . . . . . 11
76 nfcv 2612 . . . . . . . . . . . 12
77 fzfid 12224 . . . . . . . . . . . 12
78 nn0ex 10899 . . . . . . . . . . . . . 14
79 mapss 7532 . . . . . . . . . . . . . 14
8078, 39, 79mp2an 686 . . . . . . . . . . . . 13
8180, 21sseldi 3416 . . . . . . . . . . . 12
8276, 77, 81mccl 37775 . . . . . . . . . . 11
8375, 82eqeltrd 2549 . . . . . . . . . 10
8483nnzd 11062 . . . . . . . . 9
85 fzfid 12224 . . . . . . . . . 10
8657adantr 472 . . . . . . . . . . 11
8723adantr 472 . . . . . . . . . . 11
8841adantl 473 . . . . . . . . . . 11
89 etransclem24.j . . . . . . . . . . . . 13
90 0zd 10973 . . . . . . . . . . . . 13
9189, 90eqeltrd 2549 . . . . . . . . . . . 12
9291adantr 472 . . . . . . . . . . 11
9386, 87, 88, 92etransclem3 38214 . . . . . . . . . 10
9485, 93fprodzcl 14085 . . . . . . . . 9
9572, 84, 943jca 1210 . . . . . . . 8
96953ad2ant1 1051 . . . . . . 7
9772adantr 472 . . . . . . . . . . 11
9857adantr 472 . . . . . . . . . . . 12
9923adantr 472 . . . . . . . . . . . 12
10040sseli 3414 . . . . . . . . . . . . 13
101100adantl 473 . . . . . . . . . . . 12
10291adantr 472 . . . . . . . . . . . 12
10398, 99, 101, 102etransclem3 38214 . . . . . . . . . . 11
104 difss 3549 . . . . . . . . . . . . . . 15
105 ssfi 7810 . . . . . . . . . . . . . . 15
10650, 104, 105mp2an 686 . . . . . . . . . . . . . 14
107106a1i 11 . . . . . . . . . . . . 13
10857adantr 472 . . . . . . . . . . . . . 14
10923adantr 472 . . . . . . . . . . . . . 14
110104, 40sstri 3427 . . . . . . . . . . . . . . . 16
111110sseli 3414 . . . . . . . . . . . . . . 15
112111adantl 473 . . . . . . . . . . . . . 14
11391adantr 472 . . . . . . . . . . . . . 14
114108, 109, 112, 113etransclem3 38214 . . . . . . . . . . . . 13
115107, 114fprodzcl 14085 . . . . . . . . . . . 12
116115adantr 472 . . . . . . . . . . 11
11797, 103, 1163jca 1210 . . . . . . . . . 10
1181173adant3 1050 . . . . . . . . 9
119 dvds0 14395 . . . . . . . . . . . . . 14
12072, 119syl 17 . . . . . . . . . . . . 13
121120adantr 472 . . . . . . . . . . . 12
1221213ad2antl1 1192 . . . . . . . . . . 11
123 iftrue 3878 . . . . . . . . . . . . 13
124123eqcomd 2477 . . . . . . . . . . . 12
125124adantl 473 . . . . . . . . . . 11
126122, 125breqtrd 4420 . . . . . . . . . 10
12797adantr 472 . . . . . . . . . . . . . 14
128 0zd 10973 . . . . . . . . . . . . . . . . . . . 20
12999, 101ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . 22
130129elfzelzd 37624 . . . . . . . . . . . . . . . . . . . . 21
13197, 130zsubcld 11068 . . . . . . . . . . . . . . . . . . . 20
132128, 97, 1313jca 1210 . . . . . . . . . . . . . . . . . . 19
133132adantr 472 . . . . . . . . . . . . . . . . . 18
134 fzssre 37623 . . . . . . . . . . . . . . . . . . . . . 22
135134, 129sseldi 3416 . . . . . . . . . . . . . . . . . . . . 21
136135adantr 472 . . . . . . . . . . . . . . . . . . . 20
137127zred 11063 . . . . . . . . . . . . . . . . . . . 20
138 simpr 468 . . . . . . . . . . . . . . . . . . . 20
139136, 137, 138nltled 9802 . . . . . . . . . . . . . . . . . . 19
140137, 136subge0d 10224 . . . . . . . . . . . . . . . . . . 19
141139, 140mpbird 240 . . . . . . . . . . . . . . . . . 18
142 elfzle1 11828 . . . . . . . . . . . . . . . . . . . . 21
143129, 142syl 17 . . . . . . . . . . . . . . . . . . . 20
144143adantr 472 . . . . . . . . . . . . . . . . . . 19
145137, 136subge02d 10226 . . . . . . . . . . . . . . . . . . 19
146144, 145mpbid 215 . . . . . . . . . . . . . . . . . 18
147133, 141, 146jca32 544 . . . . . . . . . . . . . . . . 17
148 elfz2 11817 . . . . . . . . . . . . . . . . 17
149147, 148sylibr 217 . . . . . . . . . . . . . . . 16
150 permnn 12549 . . . . . . . . . . . . . . . 16
151149, 150syl 17 . . . . . . . . . . . . . . 15
152151nnzd 11062 . . . . . . . . . . . . . 14
153101elfzelzd 37624 . . . . . . . . . . . . . . . . 17
154102, 153zsubcld 11068 . . . . . . . . . . . . . . . 16
155154adantr 472 . . . . . . . . . . . . . . 15
156131adantr 472 . . . . . . . . . . . . . . . 16
157 elnn0z 10974 . . . . . . . . . . . . . . . 16
158156, 141, 157sylanbrc 677 . . . . . . . . . . . . . . 15
159 zexpcl 12325 . . . . . . . . . . . . . . 15
160155, 158, 159syl2anc 673 . . . . . . . . . . . . . 14
161127, 152, 1603jca 1210 . . . . . . . . . . . . 13
1621613adantl3 1188 . . . . . . . . . . . 12
1631273adantl3 1188 . . . . . . . . . . . . . 14
16459nn0zd 11061 . . . . . . . . . . . . . . . . . . . . . 22
165164adantr 472 . . . . . . . . . . . . . . . . . . . . 21
166128, 165, 1313jca 1210 . . . . . . . . . . . . . . . . . . . 20
1671663adant3 1050 . . . . . . . . . . . . . . . . . . 19
168167adantr 472 . . . . . . . . . . . . . . . . . 18
1691413adantl3 1188 . . . . . . . . . . . . . . . . . 18
170 1red 9676 . . . . . . . . . . . . . . . . . . . . 21
171 nnre 10638 . . . . . . . . . . . . . . . . . . . . . 22
172171adantl 473 . . . . . . . . . . . . . . . . . . . . 21
17357nnred 10646 . . . . . . . . . . . . . . . . . . . . . 22
174173adantr 472 . . . . . . . . . . . . . . . . . . . . 21
175 nnge1 10657 . . . . . . . . . . . . . . . . . . . . . 22
176175adantl 473 . . . . . . . . . . . . . . . . . . . . 21
177170, 172, 174, 176lesub2dd 10251 . . . . . . . . . . . . . . . . . . . 20
1781773adant2 1049 . . . . . . . . . . . . . . . . . . 19
179178adantr 472 . . . . . . . . . . . . . . . . . 18
180168, 169, 179jca32 544 . . . . . . . . . . . . . . . . 17
181 elfz2 11817 . . . . . . . . . . . . . . . . 17
182180, 181sylibr 217 . . . . . . . . . . . . . . . 16
183 permnn 12549 . . . . . . . . . . . . . . . 16
184182, 183syl 17 . . . . . . . . . . . . . . 15
185184nnzd 11062 . . . . . . . . . . . . . 14
186 dvdsmul1 14401 . . . . . . . . . . . . . 14
187163, 185, 186syl2anc 673 . . . . . . . . . . . . 13
18857nncnd 10647 . . . . . . . . . . . . . . . . . . . . 21
189 1cnd 9677 . . . . . . . . . . . . . . . . . . . . 21
190188, 189npcand 10009 . . . . . . . . . . . . . . . . . . . 20
191190eqcomd 2477 . . . . . . . . . . . . . . . . . . 19
192191fveq2d 5883 . . . . . . . . . . . . . . . . . 18
193 facp1 12502 . . . . . . . . . . . . . . . . . . 19
19459, 193syl 17 . . . . . . . . . . . . . . . . . 18
195190oveq2d 6324 . . . . . . . . . . . . . . . . . . 19
19659faccld 37621 . . . . . . . . . . . . . . . . . . . . 21
197196nncnd 10647 . . . . . . . . . . . . . . . . . . . 20
198197, 188mulcomd 9682 . . . . . . . . . . . . . . . . . . 19
199195, 198eqtrd 2505 . . . . . . . . . . . . . . . . . 18
200192, 194, 1993eqtrd 2509 . . . . . . . . . . . . . . . . 17
201200oveq1d 6323 . . . . . . . . . . . . . . . 16
202201adantr 472 . . . . . . . . . . . . . . 15
2032023ad2antl1 1192 . . . . . . . . . . . . . 14
204188ad2antrr 740 . . . . . . . . . . . . . . . 16
205197ad2antrr 740 . . . . . . . . . . . . . . . 16
206158faccld 37621 . . . . . . . . . . . . . . . . 17
207206nncnd 10647 . . . . . . . . . . . . . . . 16
208206nnne0d 10676 . . . . . . . . . . . . . . . 16
209204, 205, 207, 208divassd 10440 . . . . . . . . . . . . . . 15
2102093adantl3 1188 . . . . . . . . . . . . . 14
211203, 210eqtr2d 2506 . . . . . . . . . . . . 13
212187, 211breqtrd 4420 . . . . . . . . . . . 12
213 dvdsmultr1 14415 . . . . . . . . . . . 12
214162, 212, 213sylc 61 . . . . . . . . . . 11
215 iffalse 3881 . . . . . . . . . . . 12
216215adantl 473 . . . . . . . . . . 11
217214, 216breqtrrd 4422 . . . . . . . . . 10
218126, 217pm2.61dan 808 . . . . . . . . 9
219 dvdsmultr1 14415 . . . . . . . . 9
220118, 218, 219sylc 61 . . . . . . . 8
221 fzfid 12224 . . . . . . . . 9
22293zcnd 11064 . . . . . . . . . 10
2232223ad2antl1 1192 . . . . . . . . 9
224 simp2 1031 . . . . . . . . 9
225 fveq2 5879 . . . . . . . . . . . 12
226225breq2d 4407 . . . . . . . . . . 11
227225oveq2d 6324 . . . . . . . . . . . . . 14
228227fveq2d 5883 . . . . . . . . . . . . 13
229228oveq2d 6324 . . . . . . . . . . . 12
230 oveq2 6316 . . . . . . . . . . . . 13
231230, 227oveq12d 6326 . . . . . . . . . . . 12
232229, 231oveq12d 6326 . . . . . . . . . . 11
233226, 232ifbieq2d 3897 . . . . . . . . . 10
234233adantl 473 . . . . . . . . 9
235221, 223, 224, 234fprodsplit1 37770 . . . . . . . 8
236220, 235breqtrrd 4422 . . . . . . 7
237 dvdsmultr2 14417 . . . . . . 7
23896, 236, 237sylc 61 . . . . . 6
2392383adant1r 1285 . . . . 5
240 simpr 468 . . . . . . . . . . . . . 14
241 eluzfz1 11832 . . . . . . . . . . . . . . . . . . 19
24216, 241syl 17 . . . . . . . . . . . . . . . . . 18
24323, 242ffvelrnd 6038 . . . . . . . . . . . . . . . . 17
244134, 243sseldi 3416 . . . . . . . . . . . . . . . 16
245244adantr 472 . . . . . . . . . . . . . . 15
24660adantr 472 . . . . . . . . . . . . . . 15
247245, 246lttri3d 9792 . . . . . . . . . . . . . 14
248240, 247mpbid 215 . . . . . . . . . . . . 13
249248simprd 470 . . . . . . . . . . . 12
250249iffalsed 3883 . . . . . . . . . . 11
251 oveq2 6316 . . . . . . . . . . . . . . . . 17
25261subidd 9993 . . . . . . . . . . . . . . . . 17
253251, 252sylan9eqr 2527 . . . . . . . . . . . . . . . 16
254253fveq2d 5883 . . . . . . . . . . . . . . 15
255 fac0 12500 . . . . . . . . . . . . . . 15
256254, 255syl6eq 2521 . . . . . . . . . . . . . 14
257256oveq2d 6324 . . . . . . . . . . . . 13
258197div1d 10397 . . . . . . . . . . . . . 14
259258adantr 472 . . . . . . . . . . . . 13
260257, 259eqtrd 2505 . . . . . . . . . . . 12
261253oveq2d 6324 . . . . . . . . . . . . 13
26291zcnd 11064 . . . . . . . . . . . . . . 15
263262exp0d 12448 . . . . . . . . . . . . . 14
264263adantr 472 . . . . . . . . . . . . 13
265261, 264eqtrd 2505 . . . . . . . . . . . 12
266260, 265oveq12d 6326 . . . . . . . . . . 11
267197mulid1d 9678 . . . . . . . . . . . 12
268267adantr 472 . . . . . . . . . . 11
269250, 266, 2683eqtrd 2509 . . . . . . . . . 10
270269oveq1d 6323 . . . . . . . . 9
271270oveq2d 6324 . . . . . . . 8
272271oveq1d 6323 . . . . . . 7
27383nncnd 10647 . . . . . . . . 9
27494zcnd 11064 . . . . . . . . . 10
275197, 274mulcld 9681 . . . . . . . . 9
276196nnne0d 10676 . . . . . . . . 9
277273, 275, 197, 276divassd 10440 . . . . . . . 8
278277adantr 472 . . . . . . 7
279274, 197, 276divcan3d 10410 . . . . . . . . 9
280279oveq2d 6324 . . . . . . . 8
281280adantr 472 . . . . . . 7
282272, 278, 2813eqtrd 2509 . . . . . 6
2832823ad2ant1 1051 . . . . 5
284239, 283breqtrrd 4422 . . . 4
285284rexlimdv3a 2873 . . 3
28671, 285mpd 15 . 2
288 simpr 468 . . . . . . . . . . 11
289288iftrued 3880 . . . . . . . . . 10
290 simpr 468 . . . . . . . . . . . 12
291290iffalsed 3883 . . . . . . . . . . 11
292 simpll 768 . . . . . . . . . . . 12
293244ad2antrr 740 . . . . . . . . . . . . 13
29460ad2antrr 740 . . . . . . . . . . . . 13
295293, 294, 290nltled 9802 . . . . . . . . . . . . 13
296 id 22 . . . . . . . . . . . . . . 15
297296necomd 2698 . . . . . . . . . . . . . 14
298297ad2antlr 741 . . . . . . . . . . . . 13
299293, 294, 295, 298leneltd 9806 . . . . . . . . . . . 12
30089oveq1d 6323 . . . . . . . . . . . . . . . 16
301300adantr 472 . . . . . . . . . . . . . . 15
302243elfzelzd 37624 . . . . . . . . . . . . . . . . . . 19
303164, 302zsubcld 11068 . . . . . . . . . . . . . . . . . 18
304303adantr 472 . . . . . . . . . . . . . . . . 17
305 simpr 468 . . . . . . . . . . . . . . . . . 18
306244adantr 472 . . . . . . . . . . . . . . . . . . 19
30760adantr 472 . . . . . . . . . . . . . . . . . . 19
308306, 307posdifd 10221 . . . . . . . . . . . . . . . . . 18
309305, 308mpbid 215 . . . . . . . . . . . . . . . . 17
310 elnnz 10971 . . . . . . . . . . . . . . . . 17
311304, 309, 310sylanbrc 677 . . . . . . . . . . . . . . . 16
3123110expd 12470 . . . . . . . . . . . . . . 15