Metamath Proof Explorer


Theorem etransclem29

Description: The N -th derivative of F . (Contributed by Glauco Siliprandi, 5-Apr-2020)

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

Proof

Step Hyp Ref Expression
1 etranslemdvnf2lemlem.s φ S
2 etransclem29.a φ X TopOpen fld 𝑡 S
3 etransclem29.p φ P
4 etransclem29.m φ M 0
5 etransclem29.f F = x X x P 1 j = 1 M x j P
6 etransclem29.n φ N 0
7 etransclem29.h H = j 0 M x X x j if j = 0 P 1 P
8 etransclem29.c C = n 0 c 0 n 0 M | j = 0 M c j = n
9 etransclem29.e E = x X j = 0 M H j x
10 1 2 dvdmsscn φ X
11 10 3 4 5 7 9 etransclem4 φ F = E
12 11 oveq2d φ S D n F = S D n E
13 12 fveq1d φ S D n F N = S D n E N
14 fzfid φ 0 M Fin
15 10 adantr φ j 0 M X
16 3 adantr φ j 0 M P
17 simpr φ j 0 M j 0 M
18 15 16 7 17 etransclem1 φ j 0 M H j : X
19 1 3ad2ant1 φ j 0 M i 0 N S
20 2 3ad2ant1 φ j 0 M i 0 N X TopOpen fld 𝑡 S
21 3 3ad2ant1 φ j 0 M i 0 N P
22 etransclem5 j 0 M x X x j if j = 0 P 1 P = k 0 M y X y k if k = 0 P 1 P
23 7 22 eqtri H = k 0 M y X y k if k = 0 P 1 P
24 simp2 φ j 0 M i 0 N j 0 M
25 elfznn0 i 0 N i 0
26 25 3ad2ant3 φ j 0 M i 0 N i 0
27 19 20 21 23 24 26 etransclem20 φ j 0 M i 0 N S D n H j i : X
28 1 2 14 18 6 27 9 8 dvnprod φ S D n E N = x X c C N N ! j = 0 M c j ! j = 0 M S D n H j c j x
29 13 28 eqtrd φ S D n F N = x X c C N N ! j = 0 M c j ! j = 0 M S D n H j c j x