Metamath Proof Explorer

Theorem etransclem17

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

Ref Expression
Hypotheses etransclem17.s ⊢ φ → S ∈ ℝ ℂ
etransclem17.x ⊢ φ → X ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 S
etransclem17.p ⊢ φ → P ∈ ℕ
etransclem17.1 ⊢ H = j ∈ 0 … M ⟼ x ∈ X ⟼ x − j if j = 0 P − 1 P
etransclem17.J ⊢ φ → J ∈ 0 … M
etransclem17.n ⊢ φ → N ∈ ℕ 0
Assertion etransclem17 ⊢ φ → S D n H ⁡ J ⁡ N = x ∈ X ⟼ if if J = 0 P − 1 P < N 0 if J = 0 P − 1 P ! if J = 0 P − 1 P − N ! ⁢ x − J if J = 0 P − 1 P − N

Proof

Step Hyp Ref Expression
1 etransclem17.s ⊢ φ → S ∈ ℝ ℂ
2 etransclem17.x ⊢ φ → X ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 S
3 etransclem17.p ⊢ φ → P ∈ ℕ
4 etransclem17.1 ⊢ H = j ∈ 0 … M ⟼ x ∈ X ⟼ x − j if j = 0 P − 1 P
5 etransclem17.J ⊢ φ → J ∈ 0 … M
6 etransclem17.n ⊢ φ → N ∈ ℕ 0
7 1 2 dvdmsscn ⊢ φ → X ⊆ ℂ
8 7 sselda ⊢ φ ∧ x ∈ X → x ∈ ℂ
9 8 adantlr ⊢ φ ∧ j ∈ 0 … M ∧ x ∈ X → x ∈ ℂ
10 elfzelz ⊢ j ∈ 0 … M → j ∈ ℤ
11 10 zcnd ⊢ j ∈ 0 … M → j ∈ ℂ
12 11 ad2antlr ⊢ φ ∧ j ∈ 0 … M ∧ x ∈ X → j ∈ ℂ
13 9 12 negsubd ⊢ φ ∧ j ∈ 0 … M ∧ x ∈ X → x + − j = x − j
14 13 eqcomd ⊢ φ ∧ j ∈ 0 … M ∧ x ∈ X → x − j = x + − j
15 14 oveq1d ⊢ φ ∧ j ∈ 0 … M ∧ x ∈ X → x − j if j = 0 P − 1 P = x + − j if j = 0 P − 1 P
16 15 mpteq2dva ⊢ φ ∧ j ∈ 0 … M → x ∈ X ⟼ x − j if j = 0 P − 1 P = x ∈ X ⟼ x + − j if j = 0 P − 1 P
17 16 mpteq2dva ⊢ φ → j ∈ 0 … M ⟼ x ∈ X ⟼ x − j if j = 0 P − 1 P = j ∈ 0 … M ⟼ x ∈ X ⟼ x + − j if j = 0 P − 1 P
18 4 17 syl5eq ⊢ φ → H = j ∈ 0 … M ⟼ x ∈ X ⟼ x + − j if j = 0 P − 1 P
19 negeq ⊢ j = J → − j = − J
20 19 oveq2d ⊢ j = J → x + − j = x + -J
21 eqeq1 ⊢ j = J → j = 0 ↔ J = 0
22 21 ifbid ⊢ j = J → if j = 0 P − 1 P = if J = 0 P − 1 P
23 20 22 oveq12d ⊢ j = J → x + − j if j = 0 P − 1 P = x + -J if J = 0 P − 1 P
24 23 mpteq2dv ⊢ j = J → x ∈ X ⟼ x + − j if j = 0 P − 1 P = x ∈ X ⟼ x + -J if J = 0 P − 1 P
25 24 adantl ⊢ φ ∧ j = J → x ∈ X ⟼ x + − j if j = 0 P − 1 P = x ∈ X ⟼ x + -J if J = 0 P − 1 P
26 mptexg ⊢ X ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 S → x ∈ X ⟼ x + -J if J = 0 P − 1 P ∈ V
27 2 26 syl ⊢ φ → x ∈ X ⟼ x + -J if J = 0 P − 1 P ∈ V
28 18 25 5 27 fvmptd ⊢ φ → H ⁡ J = x ∈ X ⟼ x + -J if J = 0 P − 1 P
29 28 oveq2d ⊢ φ → S D n H ⁡ J = S D n x ∈ X ⟼ x + -J if J = 0 P − 1 P
30 29 fveq1d ⊢ φ → S D n H ⁡ J ⁡ N = S D n x ∈ X ⟼ x + -J if J = 0 P − 1 P ⁡ N
31 elfzelz ⊢ J ∈ 0 … M → J ∈ ℤ
32 31 zcnd ⊢ J ∈ 0 … M → J ∈ ℂ
33 5 32 syl ⊢ φ → J ∈ ℂ
34 33 negcld ⊢ φ → − J ∈ ℂ
35 nnm1nn0 ⊢ P ∈ ℕ → P − 1 ∈ ℕ 0
36 3 35 syl ⊢ φ → P − 1 ∈ ℕ 0
37 3 nnnn0d ⊢ φ → P ∈ ℕ 0
38 36 37 ifcld ⊢ φ → if J = 0 P − 1 P ∈ ℕ 0
39 eqid ⊢ x ∈ X ⟼ x + -J if J = 0 P − 1 P = x ∈ X ⟼ x + -J if J = 0 P − 1 P
40 1 2 34 38 39 dvnxpaek ⊢ φ ∧ N ∈ ℕ 0 → S D n x ∈ X ⟼ x + -J if J = 0 P − 1 P ⁡ N = x ∈ X ⟼ if if J = 0 P − 1 P < N 0 if J = 0 P − 1 P ! if J = 0 P − 1 P − N ! ⁢ x + -J if J = 0 P − 1 P − N
41 6 40 mpdan ⊢ φ → S D n x ∈ X ⟼ x + -J if J = 0 P − 1 P ⁡ N = x ∈ X ⟼ if if J = 0 P − 1 P < N 0 if J = 0 P − 1 P ! if J = 0 P − 1 P − N ! ⁢ x + -J if J = 0 P − 1 P − N
42 33 adantr ⊢ φ ∧ x ∈ X → J ∈ ℂ
43 8 42 negsubd ⊢ φ ∧ x ∈ X → x + -J = x − J
44 43 oveq1d ⊢ φ ∧ x ∈ X → x + -J if J = 0 P − 1 P − N = x − J if J = 0 P − 1 P − N
45 44 oveq2d ⊢ φ ∧ x ∈ X → if J = 0 P − 1 P ! if J = 0 P − 1 P − N ! ⁢ x + -J if J = 0 P − 1 P − N = if J = 0 P − 1 P ! if J = 0 P − 1 P − N ! ⁢ x − J if J = 0 P − 1 P − N
46 45 ifeq2d ⊢ φ ∧ x ∈ X → if if J = 0 P − 1 P < N 0 if J = 0 P − 1 P ! if J = 0 P − 1 P − N ! ⁢ x + -J if J = 0 P − 1 P − N = if if J = 0 P − 1 P < N 0 if J = 0 P − 1 P ! if J = 0 P − 1 P − N ! ⁢ x − J if J = 0 P − 1 P − N
47 46 mpteq2dva ⊢ φ → x ∈ X ⟼ if if J = 0 P − 1 P < N 0 if J = 0 P − 1 P ! if J = 0 P − 1 P − N ! ⁢ x + -J if J = 0 P − 1 P − N = x ∈ X ⟼ if if J = 0 P − 1 P < N 0 if J = 0 P − 1 P ! if J = 0 P − 1 P − N ! ⁢ x − J if J = 0 P − 1 P − N
48 30 41 47 3eqtrd ⊢ φ → S D n H ⁡ J ⁡ N = x ∈ X ⟼ if if J = 0 P − 1 P < N 0 if J = 0 P − 1 P ! if J = 0 P − 1 P − N ! ⁢ x − J if J = 0 P − 1 P − N