Metamath Proof Explorer


Theorem etransclem37

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

Ref Expression
Hypotheses etransclem37.s φ S
etransclem37.x φ X TopOpen fld 𝑡 S
etransclem37.p φ P
etransclem37.m φ M 0
etransclem37.f F = x X x P 1 j = 1 M x j P
etransclem37.n φ N 0
etransclem37.h H = j 0 M x X x j if j = 0 P 1 P
etransclem37.c C = n 0 c 0 n 0 M | j = 0 M c j = n
etransclem37.9 φ J 0 M
etransclem37.j φ J X
Assertion etransclem37 φ P 1 ! S D n F N J

Proof

Step Hyp Ref Expression
1 etransclem37.s φ S
2 etransclem37.x φ X TopOpen fld 𝑡 S
3 etransclem37.p φ P
4 etransclem37.m φ M 0
5 etransclem37.f F = x X x P 1 j = 1 M x j P
6 etransclem37.n φ N 0
7 etransclem37.h H = j 0 M x X x j if j = 0 P 1 P
8 etransclem37.c C = n 0 c 0 n 0 M | j = 0 M c j = n
9 etransclem37.9 φ J 0 M
10 etransclem37.j φ J X
11 8 6 etransclem16 φ C N Fin
12 nnm1nn0 P P 1 0
13 3 12 syl φ P 1 0
14 13 faccld φ P 1 !
15 14 nnzd φ P 1 !
16 8 6 etransclem12 φ C N = c 0 N 0 M | j = 0 M c j = N
17 16 eleq2d φ c C N c c 0 N 0 M | j = 0 M c j = N
18 17 biimpa φ c C N c c 0 N 0 M | j = 0 M c j = N
19 rabid c c 0 N 0 M | j = 0 M c j = N c 0 N 0 M j = 0 M c j = N
20 19 biimpi c c 0 N 0 M | j = 0 M c j = N c 0 N 0 M j = 0 M c j = N
21 20 simprd c c 0 N 0 M | j = 0 M c j = N j = 0 M c j = N
22 18 21 syl φ c C N j = 0 M c j = N
23 22 eqcomd φ c C N N = j = 0 M c j
24 23 fveq2d φ c C N N ! = j = 0 M c j !
25 24 oveq1d φ c C N N ! j = 0 M c j ! = j = 0 M c j ! j = 0 M c j !
26 nfcv _ j c
27 fzfid φ c C N 0 M Fin
28 nn0ex 0 V
29 28 a1i c c 0 N 0 M | j = 0 M c j = N 0 V
30 fzssnn0 0 N 0
31 mapss 0 V 0 N 0 0 N 0 M 0 0 M
32 29 30 31 sylancl c c 0 N 0 M | j = 0 M c j = N 0 N 0 M 0 0 M
33 20 simpld c c 0 N 0 M | j = 0 M c j = N c 0 N 0 M
34 32 33 sseldd c c 0 N 0 M | j = 0 M c j = N c 0 0 M
35 18 34 syl φ c C N c 0 0 M
36 26 27 35 mccl φ c C N j = 0 M c j ! j = 0 M c j !
37 25 36 eqeltrd φ c C N N ! j = 0 M c j !
38 37 nnzd φ c C N N ! j = 0 M c j !
39 3 adantr φ c C N P
40 4 adantr φ c C N M 0
41 elmapi c 0 N 0 M c : 0 M 0 N
42 18 33 41 3syl φ c C N c : 0 M 0 N
43 9 elfzelzd φ J
44 43 adantr φ c C N J
45 39 40 42 44 etransclem10 φ c C N if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! J P - 1 - c 0
46 fzfid φ c C N 1 M Fin
47 39 adantr φ c C N j 1 M P
48 42 adantr φ c C N j 1 M c : 0 M 0 N
49 0z 0
50 fzp1ss 0 0 + 1 M 0 M
51 49 50 ax-mp 0 + 1 M 0 M
52 51 sseli j 0 + 1 M j 0 M
53 1e0p1 1 = 0 + 1
54 53 oveq1i 1 M = 0 + 1 M
55 52 54 eleq2s j 1 M j 0 M
56 55 adantl φ c C N j 1 M j 0 M
57 44 adantr φ c C N j 1 M J
58 47 48 56 57 etransclem3 φ c C N j 1 M if P < c j 0 P ! P c j ! J j P c j
59 46 58 fprodzcl φ c C N j = 1 M if P < c j 0 P ! P c j ! J j P c j
60 45 59 zmulcld φ c C N if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! J P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! J j P c j
61 38 60 zmulcld φ c C N N ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! J P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! J j P c j
62 6 adantr φ c C N N 0
63 etransclem11 n 0 c 0 n 0 M | j = 0 M c j = n = m 0 d 0 m 0 M | k = 0 M d k = m
64 8 63 eqtri C = m 0 d 0 m 0 M | k = 0 M d k = m
65 simpr φ c C N c C N
66 9 adantr φ c C N J 0 M
67 fveq2 j = k c j = c k
68 67 fveq2d j = k c j ! = c k !
69 68 cbvprodv j = 0 M c j ! = k = 0 M c k !
70 69 oveq2i N ! j = 0 M c j ! = N ! k = 0 M c k !
71 67 breq2d j = k P < c j P < c k
72 67 oveq2d j = k P c j = P c k
73 72 fveq2d j = k P c j ! = P c k !
74 73 oveq2d j = k P ! P c j ! = P ! P c k !
75 oveq2 j = k J j = J k
76 75 72 oveq12d j = k J j P c j = J k P c k
77 74 76 oveq12d j = k P ! P c j ! J j P c j = P ! P c k ! J k P c k
78 71 77 ifbieq2d j = k if P < c j 0 P ! P c j ! J j P c j = if P < c k 0 P ! P c k ! J k P c k
79 78 cbvprodv j = 1 M if P < c j 0 P ! P c j ! J j P c j = k = 1 M if P < c k 0 P ! P c k ! J k P c k
80 79 oveq2i if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! J P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! J j P c j = if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! J P - 1 - c 0 k = 1 M if P < c k 0 P ! P c k ! J k P c k
81 70 80 oveq12i N ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! J P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! J j P c j = N ! k = 0 M c k ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! J P - 1 - c 0 k = 1 M if P < c k 0 P ! P c k ! J k P c k
82 39 40 62 64 65 66 81 etransclem28 φ c C N P 1 ! N ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! J P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! J j P c j
83 11 15 61 82 fsumdvds φ P 1 ! c C N N ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! J P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! J j P c j
84 1 2 3 4 5 6 7 8 10 etransclem31 φ S D n F N J = c C N N ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! J P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! J j P c j
85 83 84 breqtrrd φ P 1 ! S D n F N J