Metamath Proof Explorer


Theorem fourierdlem58

Description: The derivative of K is continuous on the given interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem58.k
|- K = ( s e. A |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
fourierdlem58.ass
|- ( ph -> A C_ ( -u _pi [,] _pi ) )
fourierdlem58.0nA
|- ( ph -> -. 0 e. A )
fourierdlem58.4
|- ( ph -> A e. ( topGen ` ran (,) ) )
Assertion fourierdlem58
|- ( ph -> ( RR _D K ) e. ( A -cn-> RR ) )

Proof

Step Hyp Ref Expression
1 fourierdlem58.k
 |-  K = ( s e. A |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
2 fourierdlem58.ass
 |-  ( ph -> A C_ ( -u _pi [,] _pi ) )
3 fourierdlem58.0nA
 |-  ( ph -> -. 0 e. A )
4 fourierdlem58.4
 |-  ( ph -> A e. ( topGen ` ran (,) ) )
5 pire
 |-  _pi e. RR
6 5 a1i
 |-  ( ( ph /\ s e. A ) -> _pi e. RR )
7 6 renegcld
 |-  ( ( ph /\ s e. A ) -> -u _pi e. RR )
8 7 6 iccssred
 |-  ( ( ph /\ s e. A ) -> ( -u _pi [,] _pi ) C_ RR )
9 2 sselda
 |-  ( ( ph /\ s e. A ) -> s e. ( -u _pi [,] _pi ) )
10 8 9 sseldd
 |-  ( ( ph /\ s e. A ) -> s e. RR )
11 2re
 |-  2 e. RR
12 11 a1i
 |-  ( ( ph /\ s e. A ) -> 2 e. RR )
13 10 rehalfcld
 |-  ( ( ph /\ s e. A ) -> ( s / 2 ) e. RR )
14 13 resincld
 |-  ( ( ph /\ s e. A ) -> ( sin ` ( s / 2 ) ) e. RR )
15 12 14 remulcld
 |-  ( ( ph /\ s e. A ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. RR )
16 2cnd
 |-  ( ( ph /\ s e. A ) -> 2 e. CC )
17 10 recnd
 |-  ( ( ph /\ s e. A ) -> s e. CC )
18 17 halfcld
 |-  ( ( ph /\ s e. A ) -> ( s / 2 ) e. CC )
19 18 sincld
 |-  ( ( ph /\ s e. A ) -> ( sin ` ( s / 2 ) ) e. CC )
20 2ne0
 |-  2 =/= 0
21 20 a1i
 |-  ( ( ph /\ s e. A ) -> 2 =/= 0 )
22 eqcom
 |-  ( s = 0 <-> 0 = s )
23 22 biimpi
 |-  ( s = 0 -> 0 = s )
24 23 adantl
 |-  ( ( s e. A /\ s = 0 ) -> 0 = s )
25 simpl
 |-  ( ( s e. A /\ s = 0 ) -> s e. A )
26 24 25 eqeltrd
 |-  ( ( s e. A /\ s = 0 ) -> 0 e. A )
27 26 adantll
 |-  ( ( ( ph /\ s e. A ) /\ s = 0 ) -> 0 e. A )
28 3 ad2antrr
 |-  ( ( ( ph /\ s e. A ) /\ s = 0 ) -> -. 0 e. A )
29 27 28 pm2.65da
 |-  ( ( ph /\ s e. A ) -> -. s = 0 )
30 29 neqned
 |-  ( ( ph /\ s e. A ) -> s =/= 0 )
31 fourierdlem44
 |-  ( ( s e. ( -u _pi [,] _pi ) /\ s =/= 0 ) -> ( sin ` ( s / 2 ) ) =/= 0 )
32 9 30 31 syl2anc
 |-  ( ( ph /\ s e. A ) -> ( sin ` ( s / 2 ) ) =/= 0 )
33 16 19 21 32 mulne0d
 |-  ( ( ph /\ s e. A ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 )
34 10 15 33 redivcld
 |-  ( ( ph /\ s e. A ) -> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. RR )
35 34 1 fmptd
 |-  ( ph -> K : A --> RR )
36 5 a1i
 |-  ( ph -> _pi e. RR )
37 36 renegcld
 |-  ( ph -> -u _pi e. RR )
38 37 36 iccssred
 |-  ( ph -> ( -u _pi [,] _pi ) C_ RR )
39 2 38 sstrd
 |-  ( ph -> A C_ RR )
40 dvfre
 |-  ( ( K : A --> RR /\ A C_ RR ) -> ( RR _D K ) : dom ( RR _D K ) --> RR )
41 35 39 40 syl2anc
 |-  ( ph -> ( RR _D K ) : dom ( RR _D K ) --> RR )
42 eqidd
 |-  ( ph -> ( s e. A |-> s ) = ( s e. A |-> s ) )
43 eqidd
 |-  ( ph -> ( s e. A |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( s e. A |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
44 4 10 15 42 43 offval2
 |-  ( ph -> ( ( s e. A |-> s ) oF / ( s e. A |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s e. A |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
45 1 44 eqtr4id
 |-  ( ph -> K = ( ( s e. A |-> s ) oF / ( s e. A |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
46 45 oveq2d
 |-  ( ph -> ( RR _D K ) = ( RR _D ( ( s e. A |-> s ) oF / ( s e. A |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) )
47 reelprrecn
 |-  RR e. { RR , CC }
48 47 a1i
 |-  ( ph -> RR e. { RR , CC } )
49 eqid
 |-  ( s e. A |-> s ) = ( s e. A |-> s )
50 17 49 fmptd
 |-  ( ph -> ( s e. A |-> s ) : A --> CC )
51 16 19 mulcld
 |-  ( ( ph /\ s e. A ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC )
52 33 neneqd
 |-  ( ( ph /\ s e. A ) -> -. ( 2 x. ( sin ` ( s / 2 ) ) ) = 0 )
53 elsng
 |-  ( ( 2 x. ( sin ` ( s / 2 ) ) ) e. RR -> ( ( 2 x. ( sin ` ( s / 2 ) ) ) e. { 0 } <-> ( 2 x. ( sin ` ( s / 2 ) ) ) = 0 ) )
54 15 53 syl
 |-  ( ( ph /\ s e. A ) -> ( ( 2 x. ( sin ` ( s / 2 ) ) ) e. { 0 } <-> ( 2 x. ( sin ` ( s / 2 ) ) ) = 0 ) )
55 52 54 mtbird
 |-  ( ( ph /\ s e. A ) -> -. ( 2 x. ( sin ` ( s / 2 ) ) ) e. { 0 } )
56 51 55 eldifd
 |-  ( ( ph /\ s e. A ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. ( CC \ { 0 } ) )
57 eqid
 |-  ( s e. A |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( s e. A |-> ( 2 x. ( sin ` ( s / 2 ) ) ) )
58 56 57 fmptd
 |-  ( ph -> ( s e. A |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) : A --> ( CC \ { 0 } ) )
59 eqid
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
60 59 tgioo2
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
61 4 60 eleqtrdi
 |-  ( ph -> A e. ( ( TopOpen ` CCfld ) |`t RR ) )
62 48 61 dvmptidg
 |-  ( ph -> ( RR _D ( s e. A |-> s ) ) = ( s e. A |-> 1 ) )
63 ax-resscn
 |-  RR C_ CC
64 63 a1i
 |-  ( ph -> RR C_ CC )
65 39 64 sstrd
 |-  ( ph -> A C_ CC )
66 1cnd
 |-  ( ph -> 1 e. CC )
67 ssid
 |-  CC C_ CC
68 67 a1i
 |-  ( ph -> CC C_ CC )
69 65 66 68 constcncfg
 |-  ( ph -> ( s e. A |-> 1 ) e. ( A -cn-> CC ) )
70 62 69 eqeltrd
 |-  ( ph -> ( RR _D ( s e. A |-> s ) ) e. ( A -cn-> CC ) )
71 39 resmptd
 |-  ( ph -> ( ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) |` A ) = ( s e. A |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
72 71 eqcomd
 |-  ( ph -> ( s e. A |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) |` A ) )
73 72 oveq2d
 |-  ( ph -> ( RR _D ( s e. A |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( RR _D ( ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) |` A ) ) )
74 eqid
 |-  ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) )
75 2cnd
 |-  ( s e. RR -> 2 e. CC )
76 recn
 |-  ( s e. RR -> s e. CC )
77 76 halfcld
 |-  ( s e. RR -> ( s / 2 ) e. CC )
78 77 sincld
 |-  ( s e. RR -> ( sin ` ( s / 2 ) ) e. CC )
79 75 78 mulcld
 |-  ( s e. RR -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC )
80 74 79 fmpti
 |-  ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) : RR --> CC
81 80 a1i
 |-  ( ph -> ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) : RR --> CC )
82 ssid
 |-  RR C_ RR
83 82 a1i
 |-  ( ph -> RR C_ RR )
84 59 60 dvres
 |-  ( ( ( RR C_ CC /\ ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) : RR --> CC ) /\ ( RR C_ RR /\ A C_ RR ) ) -> ( RR _D ( ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) |` A ) ) = ( ( RR _D ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` A ) ) )
85 64 81 83 39 84 syl22anc
 |-  ( ph -> ( RR _D ( ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) |` A ) ) = ( ( RR _D ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` A ) ) )
86 retop
 |-  ( topGen ` ran (,) ) e. Top
87 86 a1i
 |-  ( ph -> ( topGen ` ran (,) ) e. Top )
88 uniretop
 |-  RR = U. ( topGen ` ran (,) )
89 88 isopn3
 |-  ( ( ( topGen ` ran (,) ) e. Top /\ A C_ RR ) -> ( A e. ( topGen ` ran (,) ) <-> ( ( int ` ( topGen ` ran (,) ) ) ` A ) = A ) )
90 87 39 89 syl2anc
 |-  ( ph -> ( A e. ( topGen ` ran (,) ) <-> ( ( int ` ( topGen ` ran (,) ) ) ` A ) = A ) )
91 4 90 mpbid
 |-  ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` A ) = A )
92 91 reseq2d
 |-  ( ph -> ( ( RR _D ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` A ) ) = ( ( RR _D ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |` A ) )
93 resmpt
 |-  ( RR C_ CC -> ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) = ( s e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) )
94 63 93 ax-mp
 |-  ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) = ( s e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) )
95 id
 |-  ( s e. CC -> s e. CC )
96 2cnd
 |-  ( s e. CC -> 2 e. CC )
97 20 a1i
 |-  ( s e. CC -> 2 =/= 0 )
98 95 96 97 divrec2d
 |-  ( s e. CC -> ( s / 2 ) = ( ( 1 / 2 ) x. s ) )
99 98 eqcomd
 |-  ( s e. CC -> ( ( 1 / 2 ) x. s ) = ( s / 2 ) )
100 76 99 syl
 |-  ( s e. RR -> ( ( 1 / 2 ) x. s ) = ( s / 2 ) )
101 100 fveq2d
 |-  ( s e. RR -> ( sin ` ( ( 1 / 2 ) x. s ) ) = ( sin ` ( s / 2 ) ) )
102 101 oveq2d
 |-  ( s e. RR -> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) = ( 2 x. ( sin ` ( s / 2 ) ) ) )
103 102 mpteq2ia
 |-  ( s e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) = ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) )
104 94 103 eqtr2i
 |-  ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR )
105 104 oveq2i
 |-  ( RR _D ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( RR _D ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) )
106 eqid
 |-  ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) = ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) )
107 halfcn
 |-  ( 1 / 2 ) e. CC
108 107 a1i
 |-  ( s e. CC -> ( 1 / 2 ) e. CC )
109 108 95 mulcld
 |-  ( s e. CC -> ( ( 1 / 2 ) x. s ) e. CC )
110 109 sincld
 |-  ( s e. CC -> ( sin ` ( ( 1 / 2 ) x. s ) ) e. CC )
111 96 110 mulcld
 |-  ( s e. CC -> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) e. CC )
112 106 111 fmpti
 |-  ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) : CC --> CC
113 2cn
 |-  2 e. CC
114 dvasinbx
 |-  ( ( 2 e. CC /\ ( 1 / 2 ) e. CC ) -> ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) = ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) )
115 113 107 114 mp2an
 |-  ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) = ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) )
116 113 20 recidi
 |-  ( 2 x. ( 1 / 2 ) ) = 1
117 116 a1i
 |-  ( s e. CC -> ( 2 x. ( 1 / 2 ) ) = 1 )
118 99 fveq2d
 |-  ( s e. CC -> ( cos ` ( ( 1 / 2 ) x. s ) ) = ( cos ` ( s / 2 ) ) )
119 117 118 oveq12d
 |-  ( s e. CC -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) = ( 1 x. ( cos ` ( s / 2 ) ) ) )
120 halfcl
 |-  ( s e. CC -> ( s / 2 ) e. CC )
121 120 coscld
 |-  ( s e. CC -> ( cos ` ( s / 2 ) ) e. CC )
122 121 mulid2d
 |-  ( s e. CC -> ( 1 x. ( cos ` ( s / 2 ) ) ) = ( cos ` ( s / 2 ) ) )
123 119 122 eqtrd
 |-  ( s e. CC -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) = ( cos ` ( s / 2 ) ) )
124 123 mpteq2ia
 |-  ( s e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. s ) ) ) ) = ( s e. CC |-> ( cos ` ( s / 2 ) ) )
125 115 124 eqtri
 |-  ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) = ( s e. CC |-> ( cos ` ( s / 2 ) ) )
126 125 dmeqi
 |-  dom ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) = dom ( s e. CC |-> ( cos ` ( s / 2 ) ) )
127 dmmptg
 |-  ( A. s e. CC ( cos ` ( s / 2 ) ) e. CC -> dom ( s e. CC |-> ( cos ` ( s / 2 ) ) ) = CC )
128 127 121 mprg
 |-  dom ( s e. CC |-> ( cos ` ( s / 2 ) ) ) = CC
129 126 128 eqtri
 |-  dom ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) = CC
130 63 129 sseqtrri
 |-  RR C_ dom ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) )
131 dvres3
 |-  ( ( ( RR e. { RR , CC } /\ ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) : CC --> CC ) /\ ( CC C_ CC /\ RR C_ dom ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) ) ) -> ( RR _D ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) ) = ( ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) |` RR ) )
132 47 112 67 130 131 mp4an
 |-  ( RR _D ( ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) |` RR ) ) = ( ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) |` RR )
133 125 reseq1i
 |-  ( ( CC _D ( s e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. s ) ) ) ) ) |` RR ) = ( ( s e. CC |-> ( cos ` ( s / 2 ) ) ) |` RR )
134 105 132 133 3eqtri
 |-  ( RR _D ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( ( s e. CC |-> ( cos ` ( s / 2 ) ) ) |` RR )
135 134 reseq1i
 |-  ( ( RR _D ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |` A ) = ( ( ( s e. CC |-> ( cos ` ( s / 2 ) ) ) |` RR ) |` A )
136 135 a1i
 |-  ( ph -> ( ( RR _D ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |` A ) = ( ( ( s e. CC |-> ( cos ` ( s / 2 ) ) ) |` RR ) |` A ) )
137 39 resabs1d
 |-  ( ph -> ( ( ( s e. CC |-> ( cos ` ( s / 2 ) ) ) |` RR ) |` A ) = ( ( s e. CC |-> ( cos ` ( s / 2 ) ) ) |` A ) )
138 65 resmptd
 |-  ( ph -> ( ( s e. CC |-> ( cos ` ( s / 2 ) ) ) |` A ) = ( s e. A |-> ( cos ` ( s / 2 ) ) ) )
139 137 138 eqtrd
 |-  ( ph -> ( ( ( s e. CC |-> ( cos ` ( s / 2 ) ) ) |` RR ) |` A ) = ( s e. A |-> ( cos ` ( s / 2 ) ) ) )
140 92 136 139 3eqtrd
 |-  ( ph -> ( ( RR _D ( s e. RR |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` A ) ) = ( s e. A |-> ( cos ` ( s / 2 ) ) ) )
141 73 85 140 3eqtrd
 |-  ( ph -> ( RR _D ( s e. A |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s e. A |-> ( cos ` ( s / 2 ) ) ) )
142 coscn
 |-  cos e. ( CC -cn-> CC )
143 142 a1i
 |-  ( ph -> cos e. ( CC -cn-> CC ) )
144 65 68 idcncfg
 |-  ( ph -> ( s e. A |-> s ) e. ( A -cn-> CC ) )
145 2cnd
 |-  ( ph -> 2 e. CC )
146 20 a1i
 |-  ( ph -> 2 =/= 0 )
147 eldifsn
 |-  ( 2 e. ( CC \ { 0 } ) <-> ( 2 e. CC /\ 2 =/= 0 ) )
148 145 146 147 sylanbrc
 |-  ( ph -> 2 e. ( CC \ { 0 } ) )
149 difssd
 |-  ( ph -> ( CC \ { 0 } ) C_ CC )
150 65 148 149 constcncfg
 |-  ( ph -> ( s e. A |-> 2 ) e. ( A -cn-> ( CC \ { 0 } ) ) )
151 144 150 divcncf
 |-  ( ph -> ( s e. A |-> ( s / 2 ) ) e. ( A -cn-> CC ) )
152 143 151 cncfmpt1f
 |-  ( ph -> ( s e. A |-> ( cos ` ( s / 2 ) ) ) e. ( A -cn-> CC ) )
153 141 152 eqeltrd
 |-  ( ph -> ( RR _D ( s e. A |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( A -cn-> CC ) )
154 48 50 58 70 153 dvdivcncf
 |-  ( ph -> ( RR _D ( ( s e. A |-> s ) oF / ( s e. A |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) e. ( A -cn-> CC ) )
155 46 154 eqeltrd
 |-  ( ph -> ( RR _D K ) e. ( A -cn-> CC ) )
156 cncff
 |-  ( ( RR _D K ) e. ( A -cn-> CC ) -> ( RR _D K ) : A --> CC )
157 fdm
 |-  ( ( RR _D K ) : A --> CC -> dom ( RR _D K ) = A )
158 155 156 157 3syl
 |-  ( ph -> dom ( RR _D K ) = A )
159 158 feq2d
 |-  ( ph -> ( ( RR _D K ) : dom ( RR _D K ) --> RR <-> ( RR _D K ) : A --> RR ) )
160 41 159 mpbid
 |-  ( ph -> ( RR _D K ) : A --> RR )
161 cncffvrn
 |-  ( ( RR C_ CC /\ ( RR _D K ) e. ( A -cn-> CC ) ) -> ( ( RR _D K ) e. ( A -cn-> RR ) <-> ( RR _D K ) : A --> RR ) )
162 64 155 161 syl2anc
 |-  ( ph -> ( ( RR _D K ) e. ( A -cn-> RR ) <-> ( RR _D K ) : A --> RR ) )
163 160 162 mpbird
 |-  ( ph -> ( RR _D K ) e. ( A -cn-> RR ) )