Metamath Proof Explorer

Theorem etransclem21

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

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

Proof

Step Hyp Ref Expression
1 etransclem21.s ⊢ φ → S ∈ ℝ ℂ
2 etransclem21.x ⊢ φ → X ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 S
3 etransclem21.p ⊢ φ → P ∈ ℕ
4 etransclem21.h ⊢ H = j ∈ 0 … M ⟼ x ∈ X ⟼ x − j if j = 0 P − 1 P
5 etransclem21.j ⊢ φ → J ∈ 0 … M
6 etransclem21.n ⊢ φ → N ∈ ℕ 0
7 etransclem21.y ⊢ φ → Y ∈ X
8 1 2 3 4 5 6 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
9 oveq1 ⊢ x = Y → x − J = Y − J
10 9 oveq1d ⊢ x = Y → x − J if J = 0 P − 1 P − N = Y − J if J = 0 P − 1 P − N
11 10 oveq2d ⊢ x = Y → 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 ! ⁢ Y − J if J = 0 P − 1 P − N
12 11 ifeq2d ⊢ x = Y → 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 ! ⁢ Y − J if J = 0 P − 1 P − N
13 12 adantl ⊢ φ ∧ x = Y → 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 ! ⁢ Y − J if J = 0 P − 1 P − N
14 0cnd ⊢ φ ∧ if J = 0 P − 1 P < N → 0 ∈ ℂ
15 nnm1nn0 ⊢ P ∈ ℕ → P − 1 ∈ ℕ 0
16 3 15 syl ⊢ φ → P − 1 ∈ ℕ 0
17 3 nnnn0d ⊢ φ → P ∈ ℕ 0
18 16 17 ifcld ⊢ φ → if J = 0 P − 1 P ∈ ℕ 0
19 18 faccld ⊢ φ → if J = 0 P − 1 P ! ∈ ℕ
20 19 nncnd ⊢ φ → if J = 0 P − 1 P ! ∈ ℂ
21 20 adantr ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → if J = 0 P − 1 P ! ∈ ℂ
22 18 nn0zd ⊢ φ → if J = 0 P − 1 P ∈ ℤ
23 6 nn0zd ⊢ φ → N ∈ ℤ
24 22 23 zsubcld ⊢ φ → if J = 0 P − 1 P − N ∈ ℤ
25 24 adantr ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → if J = 0 P − 1 P − N ∈ ℤ
26 6 nn0red ⊢ φ → N ∈ ℝ
27 26 adantr ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → N ∈ ℝ
28 18 nn0red ⊢ φ → if J = 0 P − 1 P ∈ ℝ
29 28 adantr ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → if J = 0 P − 1 P ∈ ℝ
30 simpr ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → ¬ if J = 0 P − 1 P < N
31 27 29 30 nltled ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → N ≤ if J = 0 P − 1 P
32 29 27 subge0d ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → 0 ≤ if J = 0 P − 1 P − N ↔ N ≤ if J = 0 P − 1 P
33 31 32 mpbird ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → 0 ≤ if J = 0 P − 1 P − N
34 elnn0z ⊢ if J = 0 P − 1 P − N ∈ ℕ 0 ↔ if J = 0 P − 1 P − N ∈ ℤ ∧ 0 ≤ if J = 0 P − 1 P − N
35 25 33 34 sylanbrc ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → if J = 0 P − 1 P − N ∈ ℕ 0
36 35 faccld ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → if J = 0 P − 1 P − N ! ∈ ℕ
37 36 nncnd ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → if J = 0 P − 1 P − N ! ∈ ℂ
38 36 nnne0d ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → if J = 0 P − 1 P − N ! ≠ 0
39 21 37 38 divcld ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → if J = 0 P − 1 P ! if J = 0 P − 1 P − N ! ∈ ℂ
40 1 2 dvdmsscn ⊢ φ → X ⊆ ℂ
41 40 7 sseldd ⊢ φ → Y ∈ ℂ
42 5 elfzelzd ⊢ φ → J ∈ ℤ
43 42 zcnd ⊢ φ → J ∈ ℂ
44 41 43 subcld ⊢ φ → Y − J ∈ ℂ
45 44 adantr ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → Y − J ∈ ℂ
46 45 35 expcld ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → Y − J if J = 0 P − 1 P − N ∈ ℂ
47 39 46 mulcld ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → if J = 0 P − 1 P ! if J = 0 P − 1 P − N ! ⁢ Y − J if J = 0 P − 1 P − N ∈ ℂ
48 14 47 ifclda ⊢ φ → if if J = 0 P − 1 P < N 0 if J = 0 P − 1 P ! if J = 0 P − 1 P − N ! ⁢ Y − J if J = 0 P − 1 P − N ∈ ℂ
49 8 13 7 48 fvmptd ⊢ φ → S D n H ⁡ J ⁡ N ⁡ Y = if if J = 0 P − 1 P < N 0 if J = 0 P − 1 P ! if J = 0 P − 1 P − N ! ⁢ Y − J if J = 0 P − 1 P − N