Metamath Proof Explorer


Theorem etransclem20

Description: H is smooth. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem20.s φS
etransclem20.x φXTopOpenfld𝑡S
etransclem20.p φP
etransclem20.h H=j0MxXxjifj=0P1P
etransclem20.J φJ0M
etransclem20.n φN0
Assertion etransclem20 φSDnHJN:X

Proof

Step Hyp Ref Expression
1 etransclem20.s φS
2 etransclem20.x φXTopOpenfld𝑡S
3 etransclem20.p φP
4 etransclem20.h H=j0MxXxjifj=0P1P
5 etransclem20.J φJ0M
6 etransclem20.n φN0
7 iftrue ifJ=0P1P<NififJ=0P1P<N0ifJ=0P1P!ifJ=0P1PN!xJifJ=0P1PN=0
8 0cnd ifJ=0P1P<N0
9 7 8 eqeltrd ifJ=0P1P<NififJ=0P1P<N0ifJ=0P1P!ifJ=0P1PN!xJifJ=0P1PN
10 9 adantl φxXifJ=0P1P<NififJ=0P1P<N0ifJ=0P1P!ifJ=0P1PN!xJifJ=0P1PN
11 simpr φxX¬ifJ=0P1P<N¬ifJ=0P1P<N
12 11 iffalsed φxX¬ifJ=0P1P<NififJ=0P1P<N0ifJ=0P1P!ifJ=0P1PN!xJifJ=0P1PN=ifJ=0P1P!ifJ=0P1PN!xJifJ=0P1PN
13 nnm1nn0 PP10
14 3 13 syl φP10
15 3 nnnn0d φP0
16 14 15 ifcld φifJ=0P1P0
17 16 faccld φifJ=0P1P!
18 17 nncnd φifJ=0P1P!
19 18 adantr φ¬ifJ=0P1P<NifJ=0P1P!
20 16 nn0zd φifJ=0P1P
21 6 nn0zd φN
22 20 21 zsubcld φifJ=0P1PN
23 22 adantr φ¬ifJ=0P1P<NifJ=0P1PN
24 6 nn0red φN
25 24 adantr φ¬ifJ=0P1P<NN
26 16 nn0red φifJ=0P1P
27 26 adantr φ¬ifJ=0P1P<NifJ=0P1P
28 simpr φ¬ifJ=0P1P<N¬ifJ=0P1P<N
29 25 27 28 nltled φ¬ifJ=0P1P<NNifJ=0P1P
30 27 25 subge0d φ¬ifJ=0P1P<N0ifJ=0P1PNNifJ=0P1P
31 29 30 mpbird φ¬ifJ=0P1P<N0ifJ=0P1PN
32 elnn0z ifJ=0P1PN0ifJ=0P1PN0ifJ=0P1PN
33 23 31 32 sylanbrc φ¬ifJ=0P1P<NifJ=0P1PN0
34 33 faccld φ¬ifJ=0P1P<NifJ=0P1PN!
35 34 nncnd φ¬ifJ=0P1P<NifJ=0P1PN!
36 34 nnne0d φ¬ifJ=0P1P<NifJ=0P1PN!0
37 19 35 36 divcld φ¬ifJ=0P1P<NifJ=0P1P!ifJ=0P1PN!
38 37 adantlr φxX¬ifJ=0P1P<NifJ=0P1P!ifJ=0P1PN!
39 1 2 dvdmsscn φX
40 39 sselda φxXx
41 elfzelz J0MJ
42 41 zcnd J0MJ
43 5 42 syl φJ
44 43 adantr φxXJ
45 40 44 subcld φxXxJ
46 45 adantr φxX¬ifJ=0P1P<NxJ
47 33 adantlr φxX¬ifJ=0P1P<NifJ=0P1PN0
48 46 47 expcld φxX¬ifJ=0P1P<NxJifJ=0P1PN
49 38 48 mulcld φxX¬ifJ=0P1P<NifJ=0P1P!ifJ=0P1PN!xJifJ=0P1PN
50 12 49 eqeltrd φxX¬ifJ=0P1P<NififJ=0P1P<N0ifJ=0P1P!ifJ=0P1PN!xJifJ=0P1PN
51 10 50 pm2.61dan φxXififJ=0P1P<N0ifJ=0P1P!ifJ=0P1PN!xJifJ=0P1PN
52 eqid xXififJ=0P1P<N0ifJ=0P1P!ifJ=0P1PN!xJifJ=0P1PN=xXififJ=0P1P<N0ifJ=0P1P!ifJ=0P1PN!xJifJ=0P1PN
53 51 52 fmptd φxXififJ=0P1P<N0ifJ=0P1P!ifJ=0P1PN!xJifJ=0P1PN:X
54 1 2 3 4 5 6 etransclem17 φSDnHJN=xXififJ=0P1P<N0ifJ=0P1P!ifJ=0P1PN!xJifJ=0P1PN
55 54 feq1d φSDnHJN:XxXififJ=0P1P<N0ifJ=0P1P!ifJ=0P1PN!xJifJ=0P1PN:X
56 53 55 mpbird φSDnHJN:X