# Metamath Proof Explorer

## Theorem etransclem17

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

Ref Expression
Hypotheses etransclem17.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
etransclem17.x ${⊢}{\phi }\to {X}\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)$
etransclem17.p ${⊢}{\phi }\to {P}\in ℕ$
etransclem17.1 ${⊢}{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)$
etransclem17.J ${⊢}{\phi }\to {J}\in \left(0\dots {M}\right)$
etransclem17.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
Assertion etransclem17 ${⊢}{\phi }\to \left({S}{D}^{n}{H}\left({J}\right)\right)\left({N}\right)=\left({x}\in {X}⟼if\left(if\left({J}=0,{P}-1,{P}\right)<{N},0,\left(\frac{if\left({J}=0,{P}-1,{P}\right)!}{\left(if\left({J}=0,{P}-1,{P}\right)-{N}\right)!}\right){\left({x}-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)-{N}}\right)\right)$

### Proof

Step Hyp Ref Expression
1 etransclem17.s ${⊢}{\phi }\to {S}\in \left\{ℝ,ℂ\right\}$
2 etransclem17.x ${⊢}{\phi }\to {X}\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)$
3 etransclem17.p ${⊢}{\phi }\to {P}\in ℕ$
4 etransclem17.1 ${⊢}{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)$
5 etransclem17.J ${⊢}{\phi }\to {J}\in \left(0\dots {M}\right)$
6 etransclem17.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
7 1 2 dvdmsscn ${⊢}{\phi }\to {X}\subseteq ℂ$
8 7 sselda ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {x}\in ℂ$
9 8 adantlr ${⊢}\left(\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\wedge {x}\in {X}\right)\to {x}\in ℂ$
10 elfzelz ${⊢}{j}\in \left(0\dots {M}\right)\to {j}\in ℤ$
11 10 zcnd ${⊢}{j}\in \left(0\dots {M}\right)\to {j}\in ℂ$
12 11 ad2antlr ${⊢}\left(\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\wedge {x}\in {X}\right)\to {j}\in ℂ$
13 9 12 negsubd ${⊢}\left(\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\wedge {x}\in {X}\right)\to {x}+\left(-{j}\right)={x}-{j}$
14 13 eqcomd ${⊢}\left(\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\wedge {x}\in {X}\right)\to {x}-{j}={x}+\left(-{j}\right)$
15 14 oveq1d ${⊢}\left(\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\wedge {x}\in {X}\right)\to {\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}={\left({x}+\left(-{j}\right)\right)}^{if\left({j}=0,{P}-1,{P}\right)}$
16 15 mpteq2dva ${⊢}\left({\phi }\wedge {j}\in \left(0\dots {M}\right)\right)\to \left({x}\in {X}⟼{\left({x}-{j}\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)=\left({x}\in {X}⟼{\left({x}+\left(-{j}\right)\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)$
17 16 mpteq2dva ${⊢}{\phi }\to \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)=\left({j}\in \left(0\dots {M}\right)⟼\left({x}\in {X}⟼{\left({x}+\left(-{j}\right)\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)\right)$
18 4 17 syl5eq ${⊢}{\phi }\to {H}=\left({j}\in \left(0\dots {M}\right)⟼\left({x}\in {X}⟼{\left({x}+\left(-{j}\right)\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)\right)$
19 negeq ${⊢}{j}={J}\to -{j}=-{J}$
20 19 oveq2d ${⊢}{j}={J}\to {x}+\left(-{j}\right)={x}+-{J}$
21 eqeq1 ${⊢}{j}={J}\to \left({j}=0↔{J}=0\right)$
22 21 ifbid ${⊢}{j}={J}\to if\left({j}=0,{P}-1,{P}\right)=if\left({J}=0,{P}-1,{P}\right)$
23 20 22 oveq12d ${⊢}{j}={J}\to {\left({x}+\left(-{j}\right)\right)}^{if\left({j}=0,{P}-1,{P}\right)}={\left({x}+-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)}$
24 23 mpteq2dv ${⊢}{j}={J}\to \left({x}\in {X}⟼{\left({x}+\left(-{j}\right)\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)=\left({x}\in {X}⟼{\left({x}+-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)}\right)$
25 24 adantl ${⊢}\left({\phi }\wedge {j}={J}\right)\to \left({x}\in {X}⟼{\left({x}+\left(-{j}\right)\right)}^{if\left({j}=0,{P}-1,{P}\right)}\right)=\left({x}\in {X}⟼{\left({x}+-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)}\right)$
26 mptexg ${⊢}{X}\in \left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}{S}\right)\to \left({x}\in {X}⟼{\left({x}+-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)}\right)\in \mathrm{V}$
27 2 26 syl ${⊢}{\phi }\to \left({x}\in {X}⟼{\left({x}+-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)}\right)\in \mathrm{V}$
28 18 25 5 27 fvmptd ${⊢}{\phi }\to {H}\left({J}\right)=\left({x}\in {X}⟼{\left({x}+-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)}\right)$
29 28 oveq2d ${⊢}{\phi }\to {S}{D}^{n}{H}\left({J}\right)={S}{D}^{n}\left({x}\in {X}⟼{\left({x}+-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)}\right)$
30 29 fveq1d ${⊢}{\phi }\to \left({S}{D}^{n}{H}\left({J}\right)\right)\left({N}\right)=\left({S}{D}^{n}\left({x}\in {X}⟼{\left({x}+-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)}\right)\right)\left({N}\right)$
31 elfzelz ${⊢}{J}\in \left(0\dots {M}\right)\to {J}\in ℤ$
32 31 zcnd ${⊢}{J}\in \left(0\dots {M}\right)\to {J}\in ℂ$
33 5 32 syl ${⊢}{\phi }\to {J}\in ℂ$
34 33 negcld ${⊢}{\phi }\to -{J}\in ℂ$
35 nnm1nn0 ${⊢}{P}\in ℕ\to {P}-1\in {ℕ}_{0}$
36 3 35 syl ${⊢}{\phi }\to {P}-1\in {ℕ}_{0}$
37 3 nnnn0d ${⊢}{\phi }\to {P}\in {ℕ}_{0}$
38 36 37 ifcld ${⊢}{\phi }\to if\left({J}=0,{P}-1,{P}\right)\in {ℕ}_{0}$
39 eqid ${⊢}\left({x}\in {X}⟼{\left({x}+-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)}\right)=\left({x}\in {X}⟼{\left({x}+-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)}\right)$
40 1 2 34 38 39 dvnxpaek ${⊢}\left({\phi }\wedge {N}\in {ℕ}_{0}\right)\to \left({S}{D}^{n}\left({x}\in {X}⟼{\left({x}+-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)}\right)\right)\left({N}\right)=\left({x}\in {X}⟼if\left(if\left({J}=0,{P}-1,{P}\right)<{N},0,\left(\frac{if\left({J}=0,{P}-1,{P}\right)!}{\left(if\left({J}=0,{P}-1,{P}\right)-{N}\right)!}\right){\left({x}+-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)-{N}}\right)\right)$
41 6 40 mpdan ${⊢}{\phi }\to \left({S}{D}^{n}\left({x}\in {X}⟼{\left({x}+-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)}\right)\right)\left({N}\right)=\left({x}\in {X}⟼if\left(if\left({J}=0,{P}-1,{P}\right)<{N},0,\left(\frac{if\left({J}=0,{P}-1,{P}\right)!}{\left(if\left({J}=0,{P}-1,{P}\right)-{N}\right)!}\right){\left({x}+-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)-{N}}\right)\right)$
42 33 adantr ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {J}\in ℂ$
43 8 42 negsubd ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {x}+-{J}={x}-{J}$
44 43 oveq1d ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to {\left({x}+-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)-{N}}={\left({x}-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)-{N}}$
45 44 oveq2d ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to \left(\frac{if\left({J}=0,{P}-1,{P}\right)!}{\left(if\left({J}=0,{P}-1,{P}\right)-{N}\right)!}\right){\left({x}+-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)-{N}}=\left(\frac{if\left({J}=0,{P}-1,{P}\right)!}{\left(if\left({J}=0,{P}-1,{P}\right)-{N}\right)!}\right){\left({x}-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)-{N}}$
46 45 ifeq2d ${⊢}\left({\phi }\wedge {x}\in {X}\right)\to if\left(if\left({J}=0,{P}-1,{P}\right)<{N},0,\left(\frac{if\left({J}=0,{P}-1,{P}\right)!}{\left(if\left({J}=0,{P}-1,{P}\right)-{N}\right)!}\right){\left({x}+-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)-{N}}\right)=if\left(if\left({J}=0,{P}-1,{P}\right)<{N},0,\left(\frac{if\left({J}=0,{P}-1,{P}\right)!}{\left(if\left({J}=0,{P}-1,{P}\right)-{N}\right)!}\right){\left({x}-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)-{N}}\right)$
47 46 mpteq2dva ${⊢}{\phi }\to \left({x}\in {X}⟼if\left(if\left({J}=0,{P}-1,{P}\right)<{N},0,\left(\frac{if\left({J}=0,{P}-1,{P}\right)!}{\left(if\left({J}=0,{P}-1,{P}\right)-{N}\right)!}\right){\left({x}+-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)-{N}}\right)\right)=\left({x}\in {X}⟼if\left(if\left({J}=0,{P}-1,{P}\right)<{N},0,\left(\frac{if\left({J}=0,{P}-1,{P}\right)!}{\left(if\left({J}=0,{P}-1,{P}\right)-{N}\right)!}\right){\left({x}-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)-{N}}\right)\right)$
48 30 41 47 3eqtrd ${⊢}{\phi }\to \left({S}{D}^{n}{H}\left({J}\right)\right)\left({N}\right)=\left({x}\in {X}⟼if\left(if\left({J}=0,{P}-1,{P}\right)<{N},0,\left(\frac{if\left({J}=0,{P}-1,{P}\right)!}{\left(if\left({J}=0,{P}-1,{P}\right)-{N}\right)!}\right){\left({x}-{J}\right)}^{if\left({J}=0,{P}-1,{P}\right)-{N}}\right)\right)$