# 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 ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
etransclem37.x ${⊢}{\phi }\to {X}\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)$
etransclem37.p ${⊢}{\phi }\to {P}\in ℕ$
etransclem37.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
etransclem37.f ${⊢}{F}=\left({x}\in {X}⟼{{x}}^{{P}-1}\prod _{{j}=1}^{{M}}{\left({x}-{j}\right)}^{{P}}\right)$
etransclem37.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
etransclem37.h ${⊢}{H}=\left({j}\in \left(0\dots {M}\right)⟼\left({x}\in {X}⟼{\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)\right)$
etransclem37.c ${⊢}{C}=\left({n}\in {ℕ}_{0}⟼\left\{{c}\in \left({\left(0\dots {n}\right)}^{\left(0\dots {M}\right)}\right)|\sum _{{j}=0}^{{M}}{c}\left({j}\right)={n}\right\}\right)$
etransclem37.9 ${⊢}{\phi }\to {J}\in \left(0\dots {M}\right)$
etransclem37.j ${⊢}{\phi }\to {J}\in {X}$
Assertion etransclem37 ${⊢}{\phi }\to \left({P}-1\right)!\parallel \left({S}{D}^{n}{F}\right)\left({N}\right)\left({J}\right)$

### Proof

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