Metamath Proof Explorer


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