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