Metamath Proof Explorer

Theorem etransclem22

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

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

Proof

Step Hyp Ref Expression
1 etransclem22.s ⊢ φ → S ∈ ℝ ℂ
2 etransclem22.x ⊢ φ → X ∈ TopOpen ⁡ ℂ fld ↾ 𝑡 S
3 etransclem22.p ⊢ φ → P ∈ ℕ
4 etransclem22.h ⊢ H = j ∈ 0 … M ⟼ x ∈ X ⟼ x − j if j = 0 P − 1 P
5 etransclem22.J ⊢ φ → J ∈ 0 … M
6 etransclem22.n ⊢ φ → N ∈ ℕ 0
7 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
8 simpr ⊢ φ ∧ if J = 0 P − 1 P < N → if J = 0 P − 1 P < N
9 8 iftrued ⊢ φ ∧ 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 = 0
10 9 mpteq2dv ⊢ φ ∧ 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 = x ∈ X ⟼ 0
11 1 2 dvdmsscn ⊢ φ → X ⊆ ℂ
12 0cnd ⊢ φ → 0 ∈ ℂ
13 ssid ⊢ ℂ ⊆ ℂ
14 13 a1i ⊢ φ → ℂ ⊆ ℂ
15 11 12 14 constcncfg ⊢ φ → x ∈ X ⟼ 0 : X ⟶cn ℂ
16 15 adantr ⊢ φ ∧ if J = 0 P − 1 P < N → x ∈ X ⟼ 0 : X ⟶cn ℂ
17 10 16 eqeltrd ⊢ φ ∧ 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 : X ⟶cn ℂ
18 simpr ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → ¬ if J = 0 P − 1 P < N
19 18 iffalsed ⊢ φ ∧ ¬ 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 = if J = 0 P − 1 P ! if J = 0 P − 1 P − N ! ⁢ x − J if J = 0 P − 1 P − N
20 19 mpteq2dv ⊢ φ ∧ ¬ 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 = x ∈ X ⟼ if J = 0 P − 1 P ! if J = 0 P − 1 P − N ! ⁢ x − J if J = 0 P − 1 P − N
21 nfv ⊢ Ⅎ x φ ∧ ¬ if J = 0 P − 1 P < N
22 11 14 idcncfg ⊢ φ → x ∈ X ⟼ x : X ⟶cn ℂ
23 5 elfzelzd ⊢ φ → J ∈ ℤ
24 23 zcnd ⊢ φ → J ∈ ℂ
25 11 24 14 constcncfg ⊢ φ → x ∈ X ⟼ J : X ⟶cn ℂ
26 22 25 subcncf ⊢ φ → x ∈ X ⟼ x − J : X ⟶cn ℂ
27 26 adantr ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → x ∈ X ⟼ x − J : X ⟶cn ℂ
28 13 a1i ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → ℂ ⊆ ℂ
29 nnm1nn0 ⊢ P ∈ ℕ → P − 1 ∈ ℕ 0
30 3 29 syl ⊢ φ → P − 1 ∈ ℕ 0
31 3 nnnn0d ⊢ φ → P ∈ ℕ 0
32 30 31 ifcld ⊢ φ → if J = 0 P − 1 P ∈ ℕ 0
33 32 faccld ⊢ φ → if J = 0 P − 1 P ! ∈ ℕ
34 33 nncnd ⊢ φ → if J = 0 P − 1 P ! ∈ ℂ
35 34 adantr ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → if J = 0 P − 1 P ! ∈ ℂ
36 32 nn0zd ⊢ φ → if J = 0 P − 1 P ∈ ℤ
37 6 nn0zd ⊢ φ → N ∈ ℤ
38 36 37 zsubcld ⊢ φ → if J = 0 P − 1 P − N ∈ ℤ
39 38 adantr ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → if J = 0 P − 1 P − N ∈ ℤ
40 6 nn0red ⊢ φ → N ∈ ℝ
41 40 adantr ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → N ∈ ℝ
42 32 nn0red ⊢ φ → if J = 0 P − 1 P ∈ ℝ
43 42 adantr ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → if J = 0 P − 1 P ∈ ℝ
44 41 43 18 nltled ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → N ≤ if J = 0 P − 1 P
45 43 41 subge0d ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → 0 ≤ if J = 0 P − 1 P − N ↔ N ≤ if J = 0 P − 1 P
46 44 45 mpbird ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → 0 ≤ if J = 0 P − 1 P − N
47 elnn0z ⊢ if J = 0 P − 1 P − N ∈ ℕ 0 ↔ if J = 0 P − 1 P − N ∈ ℤ ∧ 0 ≤ if J = 0 P − 1 P − N
48 39 46 47 sylanbrc ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → if J = 0 P − 1 P − N ∈ ℕ 0
49 48 faccld ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → if J = 0 P − 1 P − N ! ∈ ℕ
50 49 nncnd ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → if J = 0 P − 1 P − N ! ∈ ℂ
51 49 nnne0d ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → if J = 0 P − 1 P − N ! ≠ 0
52 35 50 51 divcld ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → if J = 0 P − 1 P ! if J = 0 P − 1 P − N ! ∈ ℂ
53 28 52 28 constcncfg ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → y ∈ ℂ ⟼ if J = 0 P − 1 P ! if J = 0 P − 1 P − N ! : ℂ ⟶cn ℂ
54 expcncf ⊢ if J = 0 P − 1 P − N ∈ ℕ 0 → y ∈ ℂ ⟼ y if J = 0 P − 1 P − N : ℂ ⟶cn ℂ
55 48 54 syl ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → y ∈ ℂ ⟼ y if J = 0 P − 1 P − N : ℂ ⟶cn ℂ
56 53 55 mulcncf ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → y ∈ ℂ ⟼ if J = 0 P − 1 P ! if J = 0 P − 1 P − N ! ⁢ y if J = 0 P − 1 P − N : ℂ ⟶cn ℂ
57 oveq1 ⊢ y = x − J → y if J = 0 P − 1 P − N = x − J if J = 0 P − 1 P − N
58 57 oveq2d ⊢ y = x − J → if J = 0 P − 1 P ! if J = 0 P − 1 P − N ! ⁢ y 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
59 21 27 56 28 58 cncfcompt2 ⊢ φ ∧ ¬ if J = 0 P − 1 P < N → x ∈ X ⟼ if J = 0 P − 1 P ! if J = 0 P − 1 P − N ! ⁢ x − J if J = 0 P − 1 P − N : X ⟶cn ℂ
60 20 59 eqeltrd ⊢ φ ∧ ¬ 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 : X ⟶cn ℂ
61 17 60 pm2.61dan ⊢ φ → 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 ⟶cn ℂ
62 7 61 eqeltrd ⊢ φ → S D n H ⁡ J ⁡ N : X ⟶cn ℂ