Metamath Proof Explorer


Theorem etransclem34

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

Ref Expression
Hypotheses etransclem34.s φ S
etransclem34.a φ X TopOpen fld 𝑡 S
etransclem34.p φ P
etransclem34.m φ M 0
etransclem34.f F = x X x P 1 k = 1 M x k P
etransclem34.n φ N 0
etransclem34.h H = k 0 M x X x k if k = 0 P 1 P
etransclem34.c C = n 0 c 0 n 0 M | k = 0 M c k = n
Assertion etransclem34 φ S D n F N : X cn

Proof

Step Hyp Ref Expression
1 etransclem34.s φ S
2 etransclem34.a φ X TopOpen fld 𝑡 S
3 etransclem34.p φ P
4 etransclem34.m φ M 0
5 etransclem34.f F = x X x P 1 k = 1 M x k P
6 etransclem34.n φ N 0
7 etransclem34.h H = k 0 M x X x k if k = 0 P 1 P
8 etransclem34.c C = n 0 c 0 n 0 M | k = 0 M c k = n
9 1 2 3 4 5 6 7 8 etransclem30 φ S D n F N = x X c C N N ! k = 0 M c k ! k = 0 M S D n H k c k x
10 1 2 dvdmsscn φ X
11 8 6 etransclem16 φ C N Fin
12 10 adantr φ c C N X
13 6 faccld φ N !
14 13 nncnd φ N !
15 14 adantr φ c C N N !
16 fzfid φ c C N 0 M Fin
17 fzssnn0 0 N 0
18 ssrab2 c 0 N 0 M | k = 0 M c k = N 0 N 0 M
19 simpr φ c C N c C N
20 8 6 etransclem12 φ C N = c 0 N 0 M | k = 0 M c k = N
21 20 adantr φ c C N C N = c 0 N 0 M | k = 0 M c k = N
22 19 21 eleqtrd φ c C N c c 0 N 0 M | k = 0 M c k = N
23 18 22 sseldi φ c C N c 0 N 0 M
24 elmapi c 0 N 0 M c : 0 M 0 N
25 23 24 syl φ c C N c : 0 M 0 N
26 25 ffvelrnda φ c C N k 0 M c k 0 N
27 17 26 sseldi φ c C N k 0 M c k 0
28 27 faccld φ c C N k 0 M c k !
29 28 nncnd φ c C N k 0 M c k !
30 16 29 fprodcl φ c C N k = 0 M c k !
31 28 nnne0d φ c C N k 0 M c k ! 0
32 16 29 31 fprodn0 φ c C N k = 0 M c k ! 0
33 15 30 32 divcld φ c C N N ! k = 0 M c k !
34 ssid
35 34 a1i φ c C N
36 12 33 35 constcncfg φ c C N x X N ! k = 0 M c k ! : X cn
37 1 ad2antrr φ c C N k 0 M S
38 2 ad2antrr φ c C N k 0 M X TopOpen fld 𝑡 S
39 3 ad2antrr φ c C N k 0 M P
40 etransclem5 k 0 M x X x k if k = 0 P 1 P = j 0 M y X y j if j = 0 P 1 P
41 7 40 eqtri H = j 0 M y X y j if j = 0 P 1 P
42 simpr φ c C N k 0 M k 0 M
43 37 38 39 41 42 27 etransclem20 φ c C N k 0 M S D n H k c k : X
44 43 3adant2 φ c C N x X k 0 M S D n H k c k : X
45 simp2 φ c C N x X k 0 M x X
46 44 45 ffvelrnd φ c C N x X k 0 M S D n H k c k x
47 43 feqmptd φ c C N k 0 M S D n H k c k = x X S D n H k c k x
48 37 38 39 41 42 27 etransclem22 φ c C N k 0 M S D n H k c k : X cn
49 47 48 eqeltrrd φ c C N k 0 M x X S D n H k c k x : X cn
50 12 16 46 49 fprodcncf φ c C N x X k = 0 M S D n H k c k x : X cn
51 36 50 mulcncf φ c C N x X N ! k = 0 M c k ! k = 0 M S D n H k c k x : X cn
52 10 11 51 fsumcncf φ x X c C N N ! k = 0 M c k ! k = 0 M S D n H k c k x : X cn
53 9 52 eqeltrd φ S D n F N : X cn