Description: H is smooth. (Contributed by Glauco Siliprandi, 5-Apr-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | etransclem20.s | |
|
etransclem20.x | |
||
etransclem20.p | |
||
etransclem20.h | |
||
etransclem20.J | |
||
etransclem20.n | |
||
Assertion | etransclem20 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | etransclem20.s | |
|
2 | etransclem20.x | |
|
3 | etransclem20.p | |
|
4 | etransclem20.h | |
|
5 | etransclem20.J | |
|
6 | etransclem20.n | |
|
7 | iftrue | |
|
8 | 0cnd | |
|
9 | 7 8 | eqeltrd | |
10 | 9 | adantl | |
11 | simpr | |
|
12 | 11 | iffalsed | |
13 | nnm1nn0 | |
|
14 | 3 13 | syl | |
15 | 3 | nnnn0d | |
16 | 14 15 | ifcld | |
17 | 16 | faccld | |
18 | 17 | nncnd | |
19 | 18 | adantr | |
20 | 16 | nn0zd | |
21 | 6 | nn0zd | |
22 | 20 21 | zsubcld | |
23 | 22 | adantr | |
24 | 6 | nn0red | |
25 | 24 | adantr | |
26 | 16 | nn0red | |
27 | 26 | adantr | |
28 | simpr | |
|
29 | 25 27 28 | nltled | |
30 | 27 25 | subge0d | |
31 | 29 30 | mpbird | |
32 | elnn0z | |
|
33 | 23 31 32 | sylanbrc | |
34 | 33 | faccld | |
35 | 34 | nncnd | |
36 | 34 | nnne0d | |
37 | 19 35 36 | divcld | |
38 | 37 | adantlr | |
39 | 1 2 | dvdmsscn | |
40 | 39 | sselda | |
41 | elfzelz | |
|
42 | 41 | zcnd | |
43 | 5 42 | syl | |
44 | 43 | adantr | |
45 | 40 44 | subcld | |
46 | 45 | adantr | |
47 | 33 | adantlr | |
48 | 46 47 | expcld | |
49 | 38 48 | mulcld | |
50 | 12 49 | eqeltrd | |
51 | 10 50 | pm2.61dan | |
52 | eqid | |
|
53 | 51 52 | fmptd | |
54 | 1 2 3 4 5 6 | etransclem17 | |
55 | 54 | feq1d | |
56 | 53 55 | mpbird | |