This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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