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 φ P
etransclem28.m φ M 0
etransclem28.n φ N 0
etransclem28.c C = n 0 c 0 n 0 M | j = 0 M c j = n
etransclem28.d φ D C N
etransclem28.j φ J 0 M
etransclem28.t T = N ! 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
Assertion etransclem28 φ P 1 ! T

Proof

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