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 ) )