Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
e is transcendental
etransclem40
Next ⟩
etransclem41
Metamath Proof Explorer
Ascii
Unicode
Theorem
etransclem40
Description:
The
N
-th derivative of
F
is continuous.
(Contributed by
Glauco Siliprandi
, 5-Apr-2020)
Ref
Expression
Hypotheses
etransclem40.s
⊢
φ
→
S
∈
ℝ
ℂ
etransclem40.a
⊢
φ
→
X
∈
TopOpen
⁡
ℂ
fld
↾
𝑡
S
etransclem40.p
⊢
φ
→
P
∈
ℕ
etransclem40.m
⊢
φ
→
M
∈
ℕ
0
etransclem40.f
⊢
F
=
x
∈
X
⟼
x
P
−
1
⁢
∏
k
=
1
M
x
−
k
P
etransclem40.6
⊢
φ
→
N
∈
ℕ
0
Assertion
etransclem40
⊢
φ
→
S
D
n
F
⁡
N
:
X
⟶
cn
ℂ
Proof
Step
Hyp
Ref
Expression
1
etransclem40.s
⊢
φ
→
S
∈
ℝ
ℂ
2
etransclem40.a
⊢
φ
→
X
∈
TopOpen
⁡
ℂ
fld
↾
𝑡
S
3
etransclem40.p
⊢
φ
→
P
∈
ℕ
4
etransclem40.m
⊢
φ
→
M
∈
ℕ
0
5
etransclem40.f
⊢
F
=
x
∈
X
⟼
x
P
−
1
⁢
∏
k
=
1
M
x
−
k
P
6
etransclem40.6
⊢
φ
→
N
∈
ℕ
0
7
etransclem5
⊢
j
∈
0
…
M
⟼
y
∈
X
⟼
y
−
j
if
j
=
0
P
−
1
P
=
k
∈
0
…
M
⟼
x
∈
X
⟼
x
−
k
if
k
=
0
P
−
1
P
8
etransclem11
⊢
m
∈
ℕ
0
⟼
d
∈
0
…
m
0
…
M
|
∑
j
=
0
M
d
⁡
j
=
m
=
n
∈
ℕ
0
⟼
c
∈
0
…
n
0
…
M
|
∑
k
=
0
M
c
⁡
k
=
n
9
1
2
3
4
5
6
7
8
etransclem34
⊢
φ
→
S
D
n
F
⁡
N
:
X
⟶
cn
ℂ