Theorem fourierdlem62

Description: The function K is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypothesis	fourierdlem62.k	|- K = ( y e. ( -u _pi [,] _pi ) |-> if ( y = 0 , 1 , ( y / ( 2 x. ( sin ` ( y / 2 ) ) ) ) ) )
Assertion	fourierdlem62	|- K e. ( ( -u _pi [,] _pi ) -cn-> RR )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem62.k	|- K = ( y e. ( -u _pi [,] _pi ) |-> if ( y = 0 , 1 , ( y / ( 2 x. ( sin ` ( y / 2 ) ) ) ) ) )
2		eqeq1	|- ( y = s -> ( y = 0 <-> s = 0 ) )
3		id	|- ( y = s -> y = s )
4		oveq1	|- ( y = s -> ( y / 2 ) = ( s / 2 ) )
5	4	fveq2d	|- ( y = s -> ( sin ` ( y / 2 ) ) = ( sin ` ( s / 2 ) ) )
6	5	oveq2d	|- ( y = s -> ( 2 x. ( sin ` ( y / 2 ) ) ) = ( 2 x. ( sin ` ( s / 2 ) ) ) )
7	3 6	oveq12d	|- ( y = s -> ( y / ( 2 x. ( sin ` ( y / 2 ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
8	2 7	ifbieq2d	|- ( y = s -> if ( y = 0 , 1 , ( y / ( 2 x. ( sin ` ( y / 2 ) ) ) ) ) = if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
9	8	cbvmptv	|- ( y e. ( -u _pi [,] _pi ) |-> if ( y = 0 , 1 , ( y / ( 2 x. ( sin ` ( y / 2 ) ) ) ) ) ) = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
10	1 9	eqtri	|- K = ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
11	10	fourierdlem43	|- K : ( -u _pi [,] _pi ) --> RR
12		ax-resscn	|- RR C_ CC
13		fss	|- ( ( K : ( -u _pi [,] _pi ) --> RR /\ RR C_ CC ) -> K : ( -u _pi [,] _pi ) --> CC )
14	11 12 13	mp2an	|- K : ( -u _pi [,] _pi ) --> CC
15	14	a1i	|- ( s = 0 -> K : ( -u _pi [,] _pi ) --> CC )
16		difss	|- ( ( -u _pi (,) _pi ) \ { 0 } ) C_ ( -u _pi (,) _pi )
17		elioore	|- ( s e. ( -u _pi (,) _pi ) -> s e. RR )
18	17	ssriv	|- ( -u _pi (,) _pi ) C_ RR
19	16 18	sstri	|- ( ( -u _pi (,) _pi ) \ { 0 } ) C_ RR
20	19	a1i	|- ( T. -> ( ( -u _pi (,) _pi ) \ { 0 } ) C_ RR )
21		eqid	|- ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x )
22	19	sseli	|- ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> x e. RR )
23	21 22	fmpti	|- ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) : ( ( -u _pi (,) _pi ) \ { 0 } ) --> RR
24	23	a1i	|- ( T. -> ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) : ( ( -u _pi (,) _pi ) \ { 0 } ) --> RR )
25		eqid	|- ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) )
26		2re	|- 2 e. RR
27	26	a1i	|- ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> 2 e. RR )
28	22	rehalfcld	|- ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( x / 2 ) e. RR )
29	28	resincld	|- ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( sin ` ( x / 2 ) ) e. RR )
30	27 29	remulcld	|- ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( x / 2 ) ) ) e. RR )
31	25 30	fmpti	|- ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) : ( ( -u _pi (,) _pi ) \ { 0 } ) --> RR
32	31	a1i	|- ( T. -> ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) : ( ( -u _pi (,) _pi ) \ { 0 } ) --> RR )
33		iooretop	|- ( -u _pi (,) _pi ) e. ( topGen ` ran (,) )
34	33	a1i	|- ( T. -> ( -u _pi (,) _pi ) e. ( topGen ` ran (,) ) )
35		0re	|- 0 e. RR
36		negpilt0	|- -u _pi < 0
37		pipos	|- 0 < _pi
38		pire	|- _pi e. RR
39	38	renegcli	|- -u _pi e. RR
40	39	rexri	|- -u _pi e. RR*
41	38	rexri	|- _pi e. RR*
42		elioo2	|- ( ( -u _pi e. RR* /\ _pi e. RR* ) -> ( 0 e. ( -u _pi (,) _pi ) <-> ( 0 e. RR /\ -u _pi < 0 /\ 0 < _pi ) ) )
43	40 41 42	mp2an	|- ( 0 e. ( -u _pi (,) _pi ) <-> ( 0 e. RR /\ -u _pi < 0 /\ 0 < _pi ) )
44	35 36 37 43	mpbir3an	|- 0 e. ( -u _pi (,) _pi )
45	44	a1i	|- ( T. -> 0 e. ( -u _pi (,) _pi ) )
46		eqid	|- ( ( -u _pi (,) _pi ) \ { 0 } ) = ( ( -u _pi (,) _pi ) \ { 0 } )
47		1ex	|- 1 e. _V
48		eqid	|- ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 )
49	47 48	dmmpti	|- dom ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 ) = ( ( -u _pi (,) _pi ) \ { 0 } )
50		reelprrecn	|- RR e. { RR , CC }
51	50	a1i	|- ( T. -> RR e. { RR , CC } )
52	12	sseli	|- ( x e. RR -> x e. CC )
53	52	adantl	|- ( ( T. /\ x e. RR ) -> x e. CC )
54		1red	|- ( ( T. /\ x e. RR ) -> 1 e. RR )
55	51	dvmptid	|- ( T. -> ( RR _D ( x e. RR |-> x ) ) = ( x e. RR |-> 1 ) )
56		eqid	|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
57	56	tgioo2	|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
58		sncldre	|- ( 0 e. RR -> { 0 } e. ( Clsd ` ( topGen ` ran (,) ) ) )
59	35 58	ax-mp	|- { 0 } e. ( Clsd ` ( topGen ` ran (,) ) )
60		retopon	|- ( topGen ` ran (,) ) e. ( TopOn ` RR )
61	60	toponunii	|- RR = U. ( topGen ` ran (,) )
62	61	difopn	|- ( ( ( -u _pi (,) _pi ) e. ( topGen ` ran (,) ) /\ { 0 } e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( ( -u _pi (,) _pi ) \ { 0 } ) e. ( topGen ` ran (,) ) )
63	33 59 62	mp2an	|- ( ( -u _pi (,) _pi ) \ { 0 } ) e. ( topGen ` ran (,) )
64	63	a1i	|- ( T. -> ( ( -u _pi (,) _pi ) \ { 0 } ) e. ( topGen ` ran (,) ) )
65	51 53 54 55 20 57 56 64	dvmptres	|- ( T. -> ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 ) )
66	65	mptru	|- ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 )
67	66	eqcomi	|- ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 ) = ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) )
68	67	dmeqi	|- dom ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 ) = dom ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) )
69	49 68	eqtr3i	|- ( ( -u _pi (,) _pi ) \ { 0 } ) = dom ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) )
70	69	eqimssi	|- ( ( -u _pi (,) _pi ) \ { 0 } ) C_ dom ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) )
71	70	a1i	|- ( T. -> ( ( -u _pi (,) _pi ) \ { 0 } ) C_ dom ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ) )
72		fvex	|- ( cos ` ( x / 2 ) ) e. _V
73		eqid	|- ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) )
74	72 73	dmmpti	|- dom ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) = ( ( -u _pi (,) _pi ) \ { 0 } )
75		2cnd	|- ( ( T. /\ x e. RR ) -> 2 e. CC )
76	53	halfcld	|- ( ( T. /\ x e. RR ) -> ( x / 2 ) e. CC )
77	76	sincld	|- ( ( T. /\ x e. RR ) -> ( sin ` ( x / 2 ) ) e. CC )
78	75 77	mulcld	|- ( ( T. /\ x e. RR ) -> ( 2 x. ( sin ` ( x / 2 ) ) ) e. CC )
79	76	coscld	|- ( ( T. /\ x e. RR ) -> ( cos ` ( x / 2 ) ) e. CC )
80		2cnd	|- ( x e. RR -> 2 e. CC )
81		2ne0	|- 2 =/= 0
82	81	a1i	|- ( x e. RR -> 2 =/= 0 )
83	52 80 82	divrec2d	|- ( x e. RR -> ( x / 2 ) = ( ( 1 / 2 ) x. x ) )
84	83	fveq2d	|- ( x e. RR -> ( sin ` ( x / 2 ) ) = ( sin ` ( ( 1 / 2 ) x. x ) ) )
85	84	oveq2d	|- ( x e. RR -> ( 2 x. ( sin ` ( x / 2 ) ) ) = ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) )
86	85	mpteq2ia	|- ( x e. RR |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) = ( x e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) )
87	86	oveq2i	|- ( RR _D ( x e. RR |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) = ( RR _D ( x e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) )
88		resmpt	|- ( RR C_ CC -> ( ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) |` RR ) = ( x e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) )
89	12 88	ax-mp	|- ( ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) |` RR ) = ( x e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) )
90	89	eqcomi	|- ( x e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) = ( ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) |` RR )
91	90	oveq2i	|- ( RR _D ( x e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) = ( RR _D ( ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) |` RR ) )
92		eqid	|- ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) = ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) )
93		2cnd	|- ( x e. CC -> 2 e. CC )
94		halfcn	|- ( 1 / 2 ) e. CC
95	94	a1i	|- ( x e. CC -> ( 1 / 2 ) e. CC )
96		id	|- ( x e. CC -> x e. CC )
97	95 96	mulcld	|- ( x e. CC -> ( ( 1 / 2 ) x. x ) e. CC )
98	97	sincld	|- ( x e. CC -> ( sin ` ( ( 1 / 2 ) x. x ) ) e. CC )
99	93 98	mulcld	|- ( x e. CC -> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) e. CC )
100	92 99	fmpti	|- ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) : CC --> CC
101		eqid	|- ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) = ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) )
102		2cn	|- 2 e. CC
103	102 94	mulcli	|- ( 2 x. ( 1 / 2 ) ) e. CC
104	103	a1i	|- ( x e. CC -> ( 2 x. ( 1 / 2 ) ) e. CC )
105	97	coscld	|- ( x e. CC -> ( cos ` ( ( 1 / 2 ) x. x ) ) e. CC )
106	104 105	mulcld	|- ( x e. CC -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) e. CC )
107	106	adantl	|- ( ( T. /\ x e. CC ) -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) e. CC )
108	101 107	dmmptd	|- ( T. -> dom ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) = CC )
109	108	mptru	|- dom ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) = CC
110	12 109	sseqtrri	|- RR C_ dom ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) )
111		dvasinbx	|- ( ( 2 e. CC /\ ( 1 / 2 ) e. CC ) -> ( CC _D ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) = ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) )
112	102 94 111	mp2an	|- ( CC _D ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) = ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) )
113	112	dmeqi	|- dom ( CC _D ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) = dom ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) )
114	110 113	sseqtrri	|- RR C_ dom ( CC _D ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) )
115		dvcnre	|- ( ( ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) : CC --> CC /\ RR C_ dom ( CC _D ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) ) -> ( RR _D ( ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) |` RR ) ) = ( ( CC _D ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) |` RR ) )
116	100 114 115	mp2an	|- ( RR _D ( ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) |` RR ) ) = ( ( CC _D ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) |` RR )
117	112	reseq1i	|- ( ( CC _D ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) |` RR ) = ( ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) |` RR )
118		resmpt	|- ( RR C_ CC -> ( ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) |` RR ) = ( x e. RR |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) )
119	12 118	ax-mp	|- ( ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) |` RR ) = ( x e. RR |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) )
120	102 81	recidi	|- ( 2 x. ( 1 / 2 ) ) = 1
121	120	a1i	|- ( x e. RR -> ( 2 x. ( 1 / 2 ) ) = 1 )
122	83	eqcomd	|- ( x e. RR -> ( ( 1 / 2 ) x. x ) = ( x / 2 ) )
123	122	fveq2d	|- ( x e. RR -> ( cos ` ( ( 1 / 2 ) x. x ) ) = ( cos ` ( x / 2 ) ) )
124	121 123	oveq12d	|- ( x e. RR -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) = ( 1 x. ( cos ` ( x / 2 ) ) ) )
125	52	halfcld	|- ( x e. RR -> ( x / 2 ) e. CC )
126	125	coscld	|- ( x e. RR -> ( cos ` ( x / 2 ) ) e. CC )
127	126	mulid2d	|- ( x e. RR -> ( 1 x. ( cos ` ( x / 2 ) ) ) = ( cos ` ( x / 2 ) ) )
128	124 127	eqtrd	|- ( x e. RR -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) = ( cos ` ( x / 2 ) ) )
129	128	mpteq2ia	|- ( x e. RR |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) = ( x e. RR |-> ( cos ` ( x / 2 ) ) )
130	117 119 129	3eqtri	|- ( ( CC _D ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) |` RR ) = ( x e. RR |-> ( cos ` ( x / 2 ) ) )
131	91 116 130	3eqtri	|- ( RR _D ( x e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) = ( x e. RR |-> ( cos ` ( x / 2 ) ) )
132	87 131	eqtri	|- ( RR _D ( x e. RR |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) = ( x e. RR |-> ( cos ` ( x / 2 ) ) )
133	132	a1i	|- ( T. -> ( RR _D ( x e. RR |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) = ( x e. RR |-> ( cos ` ( x / 2 ) ) ) )
134	51 78 79 133 20 57 56 64	dvmptres	|- ( T. -> ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) )
135	134	mptru	|- ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) )
136	135	eqcomi	|- ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) = ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) )
137	136	dmeqi	|- dom ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) = dom ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) )
138	74 137	eqtr3i	|- ( ( -u _pi (,) _pi ) \ { 0 } ) = dom ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) )
139	138	eqimssi	|- ( ( -u _pi (,) _pi ) \ { 0 } ) C_ dom ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) )
140	139	a1i	|- ( T. -> ( ( -u _pi (,) _pi ) \ { 0 } ) C_ dom ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) )
141	17	recnd	|- ( s e. ( -u _pi (,) _pi ) -> s e. CC )
142	141	ssriv	|- ( -u _pi (,) _pi ) C_ CC
143	142	a1i	|- ( T. -> ( -u _pi (,) _pi ) C_ CC )
144		ssid	|- CC C_ CC
145	144	a1i	|- ( T. -> CC C_ CC )
146	143 145	idcncfg	|- ( T. -> ( x e. ( -u _pi (,) _pi ) |-> x ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) )
147	146	mptru	|- ( x e. ( -u _pi (,) _pi ) |-> x ) e. ( ( -u _pi (,) _pi ) -cn-> CC )
148		cnlimc	|- ( ( -u _pi (,) _pi ) C_ CC -> ( ( x e. ( -u _pi (,) _pi ) |-> x ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) <-> ( ( x e. ( -u _pi (,) _pi ) |-> x ) : ( -u _pi (,) _pi ) --> CC /\ A. y e. ( -u _pi (,) _pi ) ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC y ) ) ) )
149	142 148	ax-mp	|- ( ( x e. ( -u _pi (,) _pi ) |-> x ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) <-> ( ( x e. ( -u _pi (,) _pi ) |-> x ) : ( -u _pi (,) _pi ) --> CC /\ A. y e. ( -u _pi (,) _pi ) ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC y ) ) )
150	147 149	mpbi	|- ( ( x e. ( -u _pi (,) _pi ) |-> x ) : ( -u _pi (,) _pi ) --> CC /\ A. y e. ( -u _pi (,) _pi ) ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC y ) )
151	150	simpri	|- A. y e. ( -u _pi (,) _pi ) ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC y )
152		fveq2	|- ( y = 0 -> ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` y ) = ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` 0 ) )
153		oveq2	|- ( y = 0 -> ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC y ) = ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC 0 ) )
154	152 153	eleq12d	|- ( y = 0 -> ( ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC y ) <-> ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` 0 ) e. ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC 0 ) ) )
155	154	rspccva	|- ( ( A. y e. ( -u _pi (,) _pi ) ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC y ) /\ 0 e. ( -u _pi (,) _pi ) ) -> ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` 0 ) e. ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC 0 ) )
156	151 44 155	mp2an	|- ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` 0 ) e. ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC 0 )
157		id	|- ( x = 0 -> x = 0 )
158		eqid	|- ( x e. ( -u _pi (,) _pi ) |-> x ) = ( x e. ( -u _pi (,) _pi ) |-> x )
159		c0ex	|- 0 e. _V
160	157 158 159	fvmpt	|- ( 0 e. ( -u _pi (,) _pi ) -> ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` 0 ) = 0 )
161	44 160	ax-mp	|- ( ( x e. ( -u _pi (,) _pi ) |-> x ) ` 0 ) = 0
162		elioore	|- ( x e. ( -u _pi (,) _pi ) -> x e. RR )
163	162	recnd	|- ( x e. ( -u _pi (,) _pi ) -> x e. CC )
164	158 163	fmpti	|- ( x e. ( -u _pi (,) _pi ) |-> x ) : ( -u _pi (,) _pi ) --> CC
165	164	a1i	|- ( T. -> ( x e. ( -u _pi (,) _pi ) |-> x ) : ( -u _pi (,) _pi ) --> CC )
166	165	limcdif	|- ( T. -> ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC 0 ) = ( ( ( x e. ( -u _pi (,) _pi ) |-> x ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 ) )
167	166	mptru	|- ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC 0 ) = ( ( ( x e. ( -u _pi (,) _pi ) |-> x ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 )
168		resmpt	|- ( ( ( -u _pi (,) _pi ) \ { 0 } ) C_ ( -u _pi (,) _pi ) -> ( ( x e. ( -u _pi (,) _pi ) |-> x ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) )
169	16 168	ax-mp	|- ( ( x e. ( -u _pi (,) _pi ) |-> x ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x )
170	169	oveq1i	|- ( ( ( x e. ( -u _pi (,) _pi ) |-> x ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 ) = ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) limCC 0 )
171	167 170	eqtri	|- ( ( x e. ( -u _pi (,) _pi ) |-> x ) limCC 0 ) = ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) limCC 0 )
172	156 161 171	3eltr3i	|- 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) limCC 0 )
173	172	a1i	|- ( T. -> 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) limCC 0 ) )
174		eqid	|- ( x e. CC |-> 2 ) = ( x e. CC |-> 2 )
175	144	a1i	|- ( 2 e. CC -> CC C_ CC )
176		2cnd	|- ( 2 e. CC -> 2 e. CC )
177	175 176 175	constcncfg	|- ( 2 e. CC -> ( x e. CC |-> 2 ) e. ( CC -cn-> CC ) )
178	102 177	mp1i	|- ( T. -> ( x e. CC |-> 2 ) e. ( CC -cn-> CC ) )
179		2cnd	|- ( ( T. /\ x e. ( -u _pi (,) _pi ) ) -> 2 e. CC )
180	174 178 143 145 179	cncfmptssg	|- ( T. -> ( x e. ( -u _pi (,) _pi ) |-> 2 ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) )
181		sincn	|- sin e. ( CC -cn-> CC )
182	181	a1i	|- ( T. -> sin e. ( CC -cn-> CC ) )
183		eqid	|- ( x e. CC |-> ( x / 2 ) ) = ( x e. CC |-> ( x / 2 ) )
184	183	divccncf	|- ( ( 2 e. CC /\ 2 =/= 0 ) -> ( x e. CC |-> ( x / 2 ) ) e. ( CC -cn-> CC ) )
185	102 81 184	mp2an	|- ( x e. CC |-> ( x / 2 ) ) e. ( CC -cn-> CC )
186	185	a1i	|- ( T. -> ( x e. CC |-> ( x / 2 ) ) e. ( CC -cn-> CC ) )
187	163	adantl	|- ( ( T. /\ x e. ( -u _pi (,) _pi ) ) -> x e. CC )
188	187	halfcld	|- ( ( T. /\ x e. ( -u _pi (,) _pi ) ) -> ( x / 2 ) e. CC )
189	183 186 143 145 188	cncfmptssg	|- ( T. -> ( x e. ( -u _pi (,) _pi ) |-> ( x / 2 ) ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) )
190	182 189	cncfmpt1f	|- ( T. -> ( x e. ( -u _pi (,) _pi ) |-> ( sin ` ( x / 2 ) ) ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) )
191	180 190	mulcncf	|- ( T. -> ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) )
192	191	mptru	|- ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) e. ( ( -u _pi (,) _pi ) -cn-> CC )
193		cnlimc	|- ( ( -u _pi (,) _pi ) C_ CC -> ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) <-> ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) : ( -u _pi (,) _pi ) --> CC /\ A. y e. ( -u _pi (,) _pi ) ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC y ) ) ) )
194	142 193	ax-mp	|- ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) <-> ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) : ( -u _pi (,) _pi ) --> CC /\ A. y e. ( -u _pi (,) _pi ) ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC y ) ) )
195	192 194	mpbi	|- ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) : ( -u _pi (,) _pi ) --> CC /\ A. y e. ( -u _pi (,) _pi ) ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC y ) )
196	195	simpri	|- A. y e. ( -u _pi (,) _pi ) ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC y )
197		fveq2	|- ( y = 0 -> ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) = ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` 0 ) )
198		oveq2	|- ( y = 0 -> ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC y ) = ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 ) )
199	197 198	eleq12d	|- ( y = 0 -> ( ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC y ) <-> ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` 0 ) e. ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 ) ) )
200	199	rspccva	|- ( ( A. y e. ( -u _pi (,) _pi ) ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) e. ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC y ) /\ 0 e. ( -u _pi (,) _pi ) ) -> ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` 0 ) e. ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 ) )
201	196 44 200	mp2an	|- ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` 0 ) e. ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 )
202		oveq1	|- ( x = 0 -> ( x / 2 ) = ( 0 / 2 ) )
203	102 81	div0i	|- ( 0 / 2 ) = 0
204	202 203	eqtrdi	|- ( x = 0 -> ( x / 2 ) = 0 )
205	204	fveq2d	|- ( x = 0 -> ( sin ` ( x / 2 ) ) = ( sin ` 0 ) )
206		sin0	|- ( sin ` 0 ) = 0
207	205 206	eqtrdi	|- ( x = 0 -> ( sin ` ( x / 2 ) ) = 0 )
208	207	oveq2d	|- ( x = 0 -> ( 2 x. ( sin ` ( x / 2 ) ) ) = ( 2 x. 0 ) )
209		2t0e0	|- ( 2 x. 0 ) = 0
210	208 209	eqtrdi	|- ( x = 0 -> ( 2 x. ( sin ` ( x / 2 ) ) ) = 0 )
211		eqid	|- ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) = ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) )
212	210 211 159	fvmpt	|- ( 0 e. ( -u _pi (,) _pi ) -> ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` 0 ) = 0 )
213	44 212	ax-mp	|- ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` 0 ) = 0
214		2cnd	|- ( x e. ( -u _pi (,) _pi ) -> 2 e. CC )
215	163	halfcld	|- ( x e. ( -u _pi (,) _pi ) -> ( x / 2 ) e. CC )
216	215	sincld	|- ( x e. ( -u _pi (,) _pi ) -> ( sin ` ( x / 2 ) ) e. CC )
217	214 216	mulcld	|- ( x e. ( -u _pi (,) _pi ) -> ( 2 x. ( sin ` ( x / 2 ) ) ) e. CC )
218	211 217	fmpti	|- ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) : ( -u _pi (,) _pi ) --> CC
219	218	a1i	|- ( T. -> ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) : ( -u _pi (,) _pi ) --> CC )
220	219	limcdif	|- ( T. -> ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 ) = ( ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 ) )
221	220	mptru	|- ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 ) = ( ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 )
222		resmpt	|- ( ( ( -u _pi (,) _pi ) \ { 0 } ) C_ ( -u _pi (,) _pi ) -> ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) )
223	16 222	ax-mp	|- ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) )
224	223	oveq1i	|- ( ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 ) = ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 )
225	221 224	eqtri	|- ( ( x e. ( -u _pi (,) _pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 ) = ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 )
226	201 213 225	3eltr3i	|- 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 )
227	226	a1i	|- ( T. -> 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) limCC 0 ) )
228		eqidd	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) )
229		oveq1	|- ( x = y -> ( x / 2 ) = ( y / 2 ) )
230	229	fveq2d	|- ( x = y -> ( sin ` ( x / 2 ) ) = ( sin ` ( y / 2 ) ) )
231	230	oveq2d	|- ( x = y -> ( 2 x. ( sin ` ( x / 2 ) ) ) = ( 2 x. ( sin ` ( y / 2 ) ) ) )
232	231	adantl	|- ( ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) /\ x = y ) -> ( 2 x. ( sin ` ( x / 2 ) ) ) = ( 2 x. ( sin ` ( y / 2 ) ) ) )
233		id	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> y e. ( ( -u _pi (,) _pi ) \ { 0 } ) )
234	26	a1i	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> 2 e. RR )
235	19	sseli	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> y e. RR )
236	235	rehalfcld	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( y / 2 ) e. RR )
237	236	resincld	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( sin ` ( y / 2 ) ) e. RR )
238	234 237	remulcld	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( y / 2 ) ) ) e. RR )
239	228 232 233 238	fvmptd	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) = ( 2 x. ( sin ` ( y / 2 ) ) ) )
240		2cnd	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> 2 e. CC )
241	237	recnd	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( sin ` ( y / 2 ) ) e. CC )
242	81	a1i	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> 2 =/= 0 )
243		ioossicc	|- ( -u _pi (,) _pi ) C_ ( -u _pi [,] _pi )
244		eldifi	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> y e. ( -u _pi (,) _pi ) )
245	243 244	sseldi	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> y e. ( -u _pi [,] _pi ) )
246		eldifsni	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> y =/= 0 )
247		fourierdlem44	|- ( ( y e. ( -u _pi [,] _pi ) /\ y =/= 0 ) -> ( sin ` ( y / 2 ) ) =/= 0 )
248	245 246 247	syl2anc	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( sin ` ( y / 2 ) ) =/= 0 )
249	240 241 242 248	mulne0d	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( y / 2 ) ) ) =/= 0 )
250	239 249	eqnetrd	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) =/= 0 )
251	250	neneqd	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) = 0 )
252	251	nrex	|- -. E. y e. ( ( -u _pi (,) _pi ) \ { 0 } ) ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) = 0
253	25	fnmpt	|- ( A. x e. ( ( -u _pi (,) _pi ) \ { 0 } ) ( 2 x. ( sin ` ( x / 2 ) ) ) e. RR -> ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) Fn ( ( -u _pi (,) _pi ) \ { 0 } ) )
254	253 30	mprg	|- ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) Fn ( ( -u _pi (,) _pi ) \ { 0 } )
255		ssid	|- ( ( -u _pi (,) _pi ) \ { 0 } ) C_ ( ( -u _pi (,) _pi ) \ { 0 } )
256		fvelimab	|- ( ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) Fn ( ( -u _pi (,) _pi ) \ { 0 } ) /\ ( ( -u _pi (,) _pi ) \ { 0 } ) C_ ( ( -u _pi (,) _pi ) \ { 0 } ) ) -> ( 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) ) <-> E. y e. ( ( -u _pi (,) _pi ) \ { 0 } ) ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) = 0 ) )
257	254 255 256	mp2an	|- ( 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) ) <-> E. y e. ( ( -u _pi (,) _pi ) \ { 0 } ) ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) = 0 )
258	252 257	mtbir	|- -. 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) )
259	258	a1i	|- ( T. -> -. 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) ) )
260		eqidd	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) )
261	229	fveq2d	|- ( x = y -> ( cos ` ( x / 2 ) ) = ( cos ` ( y / 2 ) ) )
262	261	adantl	|- ( ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) /\ x = y ) -> ( cos ` ( x / 2 ) ) = ( cos ` ( y / 2 ) ) )
263	235	recnd	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> y e. CC )
264	263	halfcld	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( y / 2 ) e. CC )
265	264	coscld	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( cos ` ( y / 2 ) ) e. CC )
266	260 262 233 265	fvmptd	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) ` y ) = ( cos ` ( y / 2 ) ) )
267	236	rered	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( Re ` ( y / 2 ) ) = ( y / 2 ) )
268		halfpire	|- ( _pi / 2 ) e. RR
269	268	renegcli	|- -u ( _pi / 2 ) e. RR
270	269	a1i	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u ( _pi / 2 ) e. RR )
271	270	rexrd	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u ( _pi / 2 ) e. RR* )
272	268	a1i	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( _pi / 2 ) e. RR )
273	272	rexrd	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( _pi / 2 ) e. RR* )
274		picn	|- _pi e. CC
275		divneg	|- ( ( _pi e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> -u ( _pi / 2 ) = ( -u _pi / 2 ) )
276	274 102 81 275	mp3an	|- -u ( _pi / 2 ) = ( -u _pi / 2 )
277	39	a1i	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u _pi e. RR )
278		2rp	|- 2 e. RR+
279	278	a1i	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> 2 e. RR+ )
280	40	a1i	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u _pi e. RR* )
281	41	a1i	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> _pi e. RR* )
282		ioogtlb	|- ( ( -u _pi e. RR* /\ _pi e. RR* /\ y e. ( -u _pi (,) _pi ) ) -> -u _pi < y )
283	280 281 244 282	syl3anc	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u _pi < y )
284	277 235 279 283	ltdiv1dd	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( -u _pi / 2 ) < ( y / 2 ) )
285	276 284	eqbrtrid	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u ( _pi / 2 ) < ( y / 2 ) )
286	38	a1i	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> _pi e. RR )
287		iooltub	|- ( ( -u _pi e. RR* /\ _pi e. RR* /\ y e. ( -u _pi (,) _pi ) ) -> y < _pi )
288	280 281 244 287	syl3anc	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> y < _pi )
289	235 286 279 288	ltdiv1dd	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( y / 2 ) < ( _pi / 2 ) )
290	271 273 236 285 289	eliood	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( y / 2 ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
291	267 290	eqeltrd	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( Re ` ( y / 2 ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
292		cosne0	|- ( ( ( y / 2 ) e. CC /\ ( Re ` ( y / 2 ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( cos ` ( y / 2 ) ) =/= 0 )
293	264 291 292	syl2anc	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( cos ` ( y / 2 ) ) =/= 0 )
294	266 293	eqnetrd	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) ` y ) =/= 0 )
295	294	neneqd	|- ( y e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) ` y ) = 0 )
296	295	nrex	|- -. E. y e. ( ( -u _pi (,) _pi ) \ { 0 } ) ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) ` y ) = 0
297	72 73	fnmpti	|- ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) Fn ( ( -u _pi (,) _pi ) \ { 0 } )
298		fvelimab	|- ( ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) Fn ( ( -u _pi (,) _pi ) \ { 0 } ) /\ ( ( -u _pi (,) _pi ) \ { 0 } ) C_ ( ( -u _pi (,) _pi ) \ { 0 } ) ) -> ( 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) ) <-> E. y e. ( ( -u _pi (,) _pi ) \ { 0 } ) ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) ` y ) = 0 ) )
299	297 255 298	mp2an	|- ( 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) ) <-> E. y e. ( ( -u _pi (,) _pi ) \ { 0 } ) ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) ` y ) = 0 )
300	296 299	mtbir	|- -. 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) )
301	135	imaeq1i	|- ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) ) = ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) )
302	301	eleq2i	|- ( 0 e. ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) ) <-> 0 e. ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) ) )
303	300 302	mtbir	|- -. 0 e. ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) )
304	303	a1i	|- ( T. -> -. 0 e. ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) " ( ( -u _pi (,) _pi ) \ { 0 } ) ) )
305		eqid	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( s / 2 ) ) ) = ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( s / 2 ) ) )
306		eqid	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 1 / ( cos ` ( s / 2 ) ) ) ) = ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 1 / ( cos ` ( s / 2 ) ) ) )
307	19	sseli	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> s e. RR )
308	307	recnd	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> s e. CC )
309	308	halfcld	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( s / 2 ) e. CC )
310	309	coscld	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( cos ` ( s / 2 ) ) e. CC )
311	307	rehalfcld	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( s / 2 ) e. RR )
312	311	rered	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( Re ` ( s / 2 ) ) = ( s / 2 ) )
313	269	a1i	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u ( _pi / 2 ) e. RR )
314	313	rexrd	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u ( _pi / 2 ) e. RR* )
315	268	a1i	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( _pi / 2 ) e. RR )
316	315	rexrd	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( _pi / 2 ) e. RR* )
317	38	a1i	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> _pi e. RR )
318	317	renegcld	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u _pi e. RR )
319	278	a1i	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> 2 e. RR+ )
320	40	a1i	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u _pi e. RR* )
321	41	a1i	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> _pi e. RR* )
322		eldifi	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> s e. ( -u _pi (,) _pi ) )
323		ioogtlb	|- ( ( -u _pi e. RR* /\ _pi e. RR* /\ s e. ( -u _pi (,) _pi ) ) -> -u _pi < s )
324	320 321 322 323	syl3anc	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u _pi < s )
325	318 307 319 324	ltdiv1dd	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( -u _pi / 2 ) < ( s / 2 ) )
326	276 325	eqbrtrid	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -u ( _pi / 2 ) < ( s / 2 ) )
327		iooltub	|- ( ( -u _pi e. RR* /\ _pi e. RR* /\ s e. ( -u _pi (,) _pi ) ) -> s < _pi )
328	320 321 322 327	syl3anc	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> s < _pi )
329	307 317 319 328	ltdiv1dd	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( s / 2 ) < ( _pi / 2 ) )
330	314 316 311 326 329	eliood	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( s / 2 ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
331	312 330	eqeltrd	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( Re ` ( s / 2 ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
332		cosne0	|- ( ( ( s / 2 ) e. CC /\ ( Re ` ( s / 2 ) ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( cos ` ( s / 2 ) ) =/= 0 )
333	309 331 332	syl2anc	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( cos ` ( s / 2 ) ) =/= 0 )
334	333	neneqd	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -. ( cos ` ( s / 2 ) ) = 0 )
335	311	recoscld	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( cos ` ( s / 2 ) ) e. RR )
336		elsng	|- ( ( cos ` ( s / 2 ) ) e. RR -> ( ( cos ` ( s / 2 ) ) e. { 0 } <-> ( cos ` ( s / 2 ) ) = 0 ) )
337	335 336	syl	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( ( cos ` ( s / 2 ) ) e. { 0 } <-> ( cos ` ( s / 2 ) ) = 0 ) )
338	334 337	mtbird	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -. ( cos ` ( s / 2 ) ) e. { 0 } )
339	310 338	eldifd	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( cos ` ( s / 2 ) ) e. ( CC \ { 0 } ) )
340	339	adantl	|- ( ( T. /\ s e. ( ( -u _pi (,) _pi ) \ { 0 } ) ) -> ( cos ` ( s / 2 ) ) e. ( CC \ { 0 } ) )
341	309	ad2antrl	|- ( ( T. /\ ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) /\ ( s / 2 ) =/= 0 ) ) -> ( s / 2 ) e. CC )
342		cosf	|- cos : CC --> CC
343	342	a1i	|- ( T. -> cos : CC --> CC )
344	343	ffvelrnda	|- ( ( T. /\ x e. CC ) -> ( cos ` x ) e. CC )
345		eqid	|- ( s e. CC |-> ( s / 2 ) ) = ( s e. CC |-> ( s / 2 ) )
346	345	divccncf	|- ( ( 2 e. CC /\ 2 =/= 0 ) -> ( s e. CC |-> ( s / 2 ) ) e. ( CC -cn-> CC ) )
347	102 81 346	mp2an	|- ( s e. CC |-> ( s / 2 ) ) e. ( CC -cn-> CC )
348	347	a1i	|- ( T. -> ( s e. CC |-> ( s / 2 ) ) e. ( CC -cn-> CC ) )
349	141	adantl	|- ( ( T. /\ s e. ( -u _pi (,) _pi ) ) -> s e. CC )
350	349	halfcld	|- ( ( T. /\ s e. ( -u _pi (,) _pi ) ) -> ( s / 2 ) e. CC )
351	345 348 143 145 350	cncfmptssg	|- ( T. -> ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) e. ( ( -u _pi (,) _pi ) -cn-> CC ) )
352		oveq1	|- ( s = 0 -> ( s / 2 ) = ( 0 / 2 ) )
353	352 203	eqtrdi	|- ( s = 0 -> ( s / 2 ) = 0 )
354	351 45 353	cnmptlimc	|- ( T. -> 0 e. ( ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) limCC 0 ) )
355		eqid	|- ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) = ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) )
356	141	halfcld	|- ( s e. ( -u _pi (,) _pi ) -> ( s / 2 ) e. CC )
357	355 356	fmpti	|- ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) : ( -u _pi (,) _pi ) --> CC
358	357	a1i	|- ( T. -> ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) : ( -u _pi (,) _pi ) --> CC )
359	358	limcdif	|- ( T. -> ( ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) limCC 0 ) = ( ( ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 ) )
360	359	mptru	|- ( ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) limCC 0 ) = ( ( ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 )
361		resmpt	|- ( ( ( -u _pi (,) _pi ) \ { 0 } ) C_ ( -u _pi (,) _pi ) -> ( ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) = ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / 2 ) ) )
362	16 361	ax-mp	|- ( ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) = ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / 2 ) )
363	362	oveq1i	|- ( ( ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 ) = ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / 2 ) ) limCC 0 )
364	360 363	eqtri	|- ( ( s e. ( -u _pi (,) _pi ) |-> ( s / 2 ) ) limCC 0 ) = ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / 2 ) ) limCC 0 )
365	354 364	eleqtrdi	|- ( T. -> 0 e. ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / 2 ) ) limCC 0 ) )
366		ffn	|- ( cos : CC --> CC -> cos Fn CC )
367	342 366	ax-mp	|- cos Fn CC
368		dffn5	|- ( cos Fn CC <-> cos = ( x e. CC |-> ( cos ` x ) ) )
369	367 368	mpbi	|- cos = ( x e. CC |-> ( cos ` x ) )
370		coscn	|- cos e. ( CC -cn-> CC )
371	369 370	eqeltrri	|- ( x e. CC |-> ( cos ` x ) ) e. ( CC -cn-> CC )
372	371	a1i	|- ( T. -> ( x e. CC |-> ( cos ` x ) ) e. ( CC -cn-> CC ) )
373		0cnd	|- ( T. -> 0 e. CC )
374		fveq2	|- ( x = 0 -> ( cos ` x ) = ( cos ` 0 ) )
375		cos0	|- ( cos ` 0 ) = 1
376	374 375	eqtrdi	|- ( x = 0 -> ( cos ` x ) = 1 )
377	372 373 376	cnmptlimc	|- ( T. -> 1 e. ( ( x e. CC |-> ( cos ` x ) ) limCC 0 ) )
378		fveq2	|- ( x = ( s / 2 ) -> ( cos ` x ) = ( cos ` ( s / 2 ) ) )
379		fveq2	|- ( ( s / 2 ) = 0 -> ( cos ` ( s / 2 ) ) = ( cos ` 0 ) )
380	379 375	eqtrdi	|- ( ( s / 2 ) = 0 -> ( cos ` ( s / 2 ) ) = 1 )
381	380	ad2antll	|- ( ( T. /\ ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) /\ ( s / 2 ) = 0 ) ) -> ( cos ` ( s / 2 ) ) = 1 )
382	341 344 365 377 378 381	limcco	|- ( T. -> 1 e. ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( s / 2 ) ) ) limCC 0 ) )
383		ax-1ne0	|- 1 =/= 0
384	383	a1i	|- ( T. -> 1 =/= 0 )
385	305 306 340 382 384	reclimc	|- ( T. -> ( 1 / 1 ) e. ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 1 / ( cos ` ( s / 2 ) ) ) ) limCC 0 ) )
386		1div1e1	|- ( 1 / 1 ) = 1
387	66	fveq1i	|- ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ) ` s ) = ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 ) ` s )
388		eqidd	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 ) )
389		eqidd	|- ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) /\ x = s ) -> 1 = 1 )
390		id	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> s e. ( ( -u _pi (,) _pi ) \ { 0 } ) )
391		1red	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> 1 e. RR )
392	388 389 390 391	fvmptd	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> 1 ) ` s ) = 1 )
393	387 392	eqtr2id	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> 1 = ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ) ` s ) )
394	135	a1i	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) )
395		oveq1	|- ( x = s -> ( x / 2 ) = ( s / 2 ) )
396	395	fveq2d	|- ( x = s -> ( cos ` ( x / 2 ) ) = ( cos ` ( s / 2 ) ) )
397	396	adantl	|- ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) /\ x = s ) -> ( cos ` ( x / 2 ) ) = ( cos ` ( s / 2 ) ) )
398	394 397 390 335	fvmptd	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) ` s ) = ( cos ` ( s / 2 ) ) )
399	398	eqcomd	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( cos ` ( s / 2 ) ) = ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) ` s ) )
400	393 399	oveq12d	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( 1 / ( cos ` ( s / 2 ) ) ) = ( ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ) ` s ) / ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) ` s ) ) )
401	400	mpteq2ia	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 1 / ( cos ` ( s / 2 ) ) ) ) = ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ) ` s ) / ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) ` s ) ) )
402	401	oveq1i	|- ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 1 / ( cos ` ( s / 2 ) ) ) ) limCC 0 ) = ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ) ` s ) / ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) ` s ) ) ) limCC 0 )
403	385 386 402	3eltr3g	|- ( T. -> 1 e. ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ) ` s ) / ( ( RR _D ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) ` s ) ) ) limCC 0 ) )
404	20 24 32 34 45 46 71 140 173 227 259 304 403	lhop	|- ( T. -> 1 e. ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ` s ) / ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` s ) ) ) limCC 0 ) )
405	404	mptru	|- 1 e. ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ` s ) / ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` s ) ) ) limCC 0 )
406		eqidd	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) )
407		simpr	|- ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) /\ x = s ) -> x = s )
408	406 407 390 307	fvmptd	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ` s ) = s )
409		eqidd	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) = ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) )
410	407	oveq1d	|- ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) /\ x = s ) -> ( x / 2 ) = ( s / 2 ) )
411	410	fveq2d	|- ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) /\ x = s ) -> ( sin ` ( x / 2 ) ) = ( sin ` ( s / 2 ) ) )
412	411	oveq2d	|- ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) /\ x = s ) -> ( 2 x. ( sin ` ( x / 2 ) ) ) = ( 2 x. ( sin ` ( s / 2 ) ) ) )
413	26	a1i	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> 2 e. RR )
414	311	resincld	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( sin ` ( s / 2 ) ) e. RR )
415	413 414	remulcld	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. RR )
416	409 412 390 415	fvmptd	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` s ) = ( 2 x. ( sin ` ( s / 2 ) ) ) )
417	408 416	oveq12d	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> ( ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ` s ) / ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` s ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
418	417	mpteq2ia	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ` s ) / ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` s ) ) ) = ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
419	418	oveq1i	|- ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> x ) ` s ) / ( ( x e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` s ) ) ) limCC 0 ) = ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) limCC 0 )
420	405 419	eleqtri	|- 1 e. ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) limCC 0 )
421	10	oveq1i	|- ( K limCC 0 ) = ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) limCC 0 )
422	10	feq1i	|- ( K : ( -u _pi [,] _pi ) --> CC <-> ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) : ( -u _pi [,] _pi ) --> CC )
423	14 422	mpbi	|- ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) : ( -u _pi [,] _pi ) --> CC
424	423	a1i	|- ( T. -> ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) : ( -u _pi [,] _pi ) --> CC )
425	243	a1i	|- ( T. -> ( -u _pi (,) _pi ) C_ ( -u _pi [,] _pi ) )
426		iccssre	|- ( ( -u _pi e. RR /\ _pi e. RR ) -> ( -u _pi [,] _pi ) C_ RR )
427	39 38 426	mp2an	|- ( -u _pi [,] _pi ) C_ RR
428	427	a1i	|- ( T. -> ( -u _pi [,] _pi ) C_ RR )
429	428 12	sstrdi	|- ( T. -> ( -u _pi [,] _pi ) C_ CC )
430		eqid	|- ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) u. { 0 } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) u. { 0 } ) )
431	39 35 36	ltleii	|- -u _pi <_ 0
432	35 38 37	ltleii	|- 0 <_ _pi
433	39 38	elicc2i	|- ( 0 e. ( -u _pi [,] _pi ) <-> ( 0 e. RR /\ -u _pi <_ 0 /\ 0 <_ _pi ) )
434	35 431 432 433	mpbir3an	|- 0 e. ( -u _pi [,] _pi )
435	159	snss	|- ( 0 e. ( -u _pi [,] _pi ) <-> { 0 } C_ ( -u _pi [,] _pi ) )
436	434 435	mpbi	|- { 0 } C_ ( -u _pi [,] _pi )
437		ssequn2	|- ( { 0 } C_ ( -u _pi [,] _pi ) <-> ( ( -u _pi [,] _pi ) u. { 0 } ) = ( -u _pi [,] _pi ) )
438	436 437	mpbi	|- ( ( -u _pi [,] _pi ) u. { 0 } ) = ( -u _pi [,] _pi )
439	438	oveq2i	|- ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) u. { 0 } ) ) = ( ( TopOpen ` CCfld ) |`t ( -u _pi [,] _pi ) )
440		eqid	|- ( topGen ` ran (,) ) = ( topGen ` ran (,) )
441	56 440	rerest	|- ( ( -u _pi [,] _pi ) C_ RR -> ( ( TopOpen ` CCfld ) |`t ( -u _pi [,] _pi ) ) = ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) )
442	427 441	ax-mp	|- ( ( TopOpen ` CCfld ) |`t ( -u _pi [,] _pi ) ) = ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) )
443	439 442	eqtri	|- ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) u. { 0 } ) ) = ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) )
444	443	fveq2i	|- ( int ` ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) u. { 0 } ) ) ) = ( int ` ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) )
445	159	snss	|- ( 0 e. ( -u _pi (,) _pi ) <-> { 0 } C_ ( -u _pi (,) _pi ) )
446	44 445	mpbi	|- { 0 } C_ ( -u _pi (,) _pi )
447		ssequn2	|- ( { 0 } C_ ( -u _pi (,) _pi ) <-> ( ( -u _pi (,) _pi ) u. { 0 } ) = ( -u _pi (,) _pi ) )
448	446 447	mpbi	|- ( ( -u _pi (,) _pi ) u. { 0 } ) = ( -u _pi (,) _pi )
449	444 448	fveq12i	|- ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) u. { 0 } ) ) ) ` ( ( -u _pi (,) _pi ) u. { 0 } ) ) = ( ( int ` ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) ) ` ( -u _pi (,) _pi ) )
450		resttopon	|- ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ ( -u _pi [,] _pi ) C_ RR ) -> ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) e. ( TopOn ` ( -u _pi [,] _pi ) ) )
451	60 427 450	mp2an	|- ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) e. ( TopOn ` ( -u _pi [,] _pi ) )
452	451	topontopi	|- ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) e. Top
453		retop	|- ( topGen ` ran (,) ) e. Top
454		ovex	|- ( -u _pi [,] _pi ) e. _V
455	453 454	pm3.2i	|- ( ( topGen ` ran (,) ) e. Top /\ ( -u _pi [,] _pi ) e. _V )
456		ssid	|- ( -u _pi (,) _pi ) C_ ( -u _pi (,) _pi )
457	33 243 456	3pm3.2i	|- ( ( -u _pi (,) _pi ) e. ( topGen ` ran (,) ) /\ ( -u _pi (,) _pi ) C_ ( -u _pi [,] _pi ) /\ ( -u _pi (,) _pi ) C_ ( -u _pi (,) _pi ) )
458		restopnb	|- ( ( ( ( topGen ` ran (,) ) e. Top /\ ( -u _pi [,] _pi ) e. _V ) /\ ( ( -u _pi (,) _pi ) e. ( topGen ` ran (,) ) /\ ( -u _pi (,) _pi ) C_ ( -u _pi [,] _pi ) /\ ( -u _pi (,) _pi ) C_ ( -u _pi (,) _pi ) ) ) -> ( ( -u _pi (,) _pi ) e. ( topGen ` ran (,) ) <-> ( -u _pi (,) _pi ) e. ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) ) )
459	455 457 458	mp2an	|- ( ( -u _pi (,) _pi ) e. ( topGen ` ran (,) ) <-> ( -u _pi (,) _pi ) e. ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) )
460	33 459	mpbi	|- ( -u _pi (,) _pi ) e. ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) )
461		isopn3i	|- ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) e. Top /\ ( -u _pi (,) _pi ) e. ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) ) -> ( ( int ` ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) ) ` ( -u _pi (,) _pi ) ) = ( -u _pi (,) _pi ) )
462	452 460 461	mp2an	|- ( ( int ` ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) ) ` ( -u _pi (,) _pi ) ) = ( -u _pi (,) _pi )
463		eqid	|- ( -u _pi (,) _pi ) = ( -u _pi (,) _pi )
464	449 462 463	3eqtrri	|- ( -u _pi (,) _pi ) = ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) u. { 0 } ) ) ) ` ( ( -u _pi (,) _pi ) u. { 0 } ) )
465	44 464	eleqtri	|- 0 e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) u. { 0 } ) ) ) ` ( ( -u _pi (,) _pi ) u. { 0 } ) )
466	465	a1i	|- ( T. -> 0 e. ( ( int ` ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) u. { 0 } ) ) ) ` ( ( -u _pi (,) _pi ) u. { 0 } ) ) )
467	424 425 429 56 430 466	limcres	|- ( T. -> ( ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( -u _pi (,) _pi ) ) limCC 0 ) = ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) limCC 0 ) )
468	467	mptru	|- ( ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( -u _pi (,) _pi ) ) limCC 0 ) = ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) limCC 0 )
469	468	eqcomi	|- ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) limCC 0 ) = ( ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( -u _pi (,) _pi ) ) limCC 0 )
470		resmpt	|- ( ( -u _pi (,) _pi ) C_ ( -u _pi [,] _pi ) -> ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( -u _pi (,) _pi ) ) = ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) )
471	243 470	ax-mp	|- ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( -u _pi (,) _pi ) ) = ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
472	471	oveq1i	|- ( ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( -u _pi (,) _pi ) ) limCC 0 ) = ( ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) limCC 0 )
473	421 469 472	3eqtri	|- ( K limCC 0 ) = ( ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) limCC 0 )
474		eqid	|- ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) = ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
475		iftrue	|- ( s = 0 -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = 1 )
476		1cnd	|- ( s = 0 -> 1 e. CC )
477	475 476	eqeltrd	|- ( s = 0 -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. CC )
478	477	adantl	|- ( ( s e. ( -u _pi (,) _pi ) /\ s = 0 ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. CC )
479		iffalse	|- ( -. s = 0 -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
480	479	adantl	|- ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
481	141	adantr	|- ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> s e. CC )
482		2cnd	|- ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> 2 e. CC )
483	481	halfcld	|- ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> ( s / 2 ) e. CC )
484	483	sincld	|- ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> ( sin ` ( s / 2 ) ) e. CC )
485	482 484	mulcld	|- ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC )
486	81	a1i	|- ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> 2 =/= 0 )
487	243	sseli	|- ( s e. ( -u _pi (,) _pi ) -> s e. ( -u _pi [,] _pi ) )
488		neqne	|- ( -. s = 0 -> s =/= 0 )
489		fourierdlem44	|- ( ( s e. ( -u _pi [,] _pi ) /\ s =/= 0 ) -> ( sin ` ( s / 2 ) ) =/= 0 )
490	487 488 489	syl2an	|- ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> ( sin ` ( s / 2 ) ) =/= 0 )
491	482 484 486 490	mulne0d	|- ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 )
492	481 485 491	divcld	|- ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. CC )
493	480 492	eqeltrd	|- ( ( s e. ( -u _pi (,) _pi ) /\ -. s = 0 ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. CC )
494	478 493	pm2.61dan	|- ( s e. ( -u _pi (,) _pi ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. CC )
495	474 494	fmpti	|- ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) : ( -u _pi (,) _pi ) --> CC
496	495	a1i	|- ( T. -> ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) : ( -u _pi (,) _pi ) --> CC )
497	496	limcdif	|- ( T. -> ( ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) limCC 0 ) = ( ( ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 ) )
498	497	mptru	|- ( ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) limCC 0 ) = ( ( ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 )
499		resmpt	|- ( ( ( -u _pi (,) _pi ) \ { 0 } ) C_ ( -u _pi (,) _pi ) -> ( ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) = ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) )
500	16 499	ax-mp	|- ( ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) = ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
501		eldifn	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -. s e. { 0 } )
502		velsn	|- ( s e. { 0 } <-> s = 0 )
503	501 502	sylnib	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> -. s = 0 )
504	503 479	syl	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
505	504	mpteq2ia	|- ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) = ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
506	500 505	eqtri	|- ( ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) = ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
507	506	oveq1i	|- ( ( ( s e. ( -u _pi (,) _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( -u _pi (,) _pi ) \ { 0 } ) ) limCC 0 ) = ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) limCC 0 )
508	473 498 507	3eqtrri	|- ( ( s e. ( ( -u _pi (,) _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) limCC 0 ) = ( K limCC 0 )
509	420 508	eleqtri	|- 1 e. ( K limCC 0 )
510	509	a1i	|- ( s = 0 -> 1 e. ( K limCC 0 ) )
511		fveq2	|- ( s = 0 -> ( K ` s ) = ( K ` 0 ) )
512	475 10 47	fvmpt	|- ( 0 e. ( -u _pi [,] _pi ) -> ( K ` 0 ) = 1 )
513	434 512	ax-mp	|- ( K ` 0 ) = 1
514	511 513	eqtrdi	|- ( s = 0 -> ( K ` s ) = 1 )
515		oveq2	|- ( s = 0 -> ( K limCC s ) = ( K limCC 0 ) )
516	510 514 515	3eltr4d	|- ( s = 0 -> ( K ` s ) e. ( K limCC s ) )
517	427 12	sstri	|- ( -u _pi [,] _pi ) C_ CC
518	517	a1i	|- ( s = 0 -> ( -u _pi [,] _pi ) C_ CC )
519	38	a1i	|- ( s = 0 -> _pi e. RR )
520	519	renegcld	|- ( s = 0 -> -u _pi e. RR )
521		id	|- ( s = 0 -> s = 0 )
522	35	a1i	|- ( s = 0 -> 0 e. RR )
523	521 522	eqeltrd	|- ( s = 0 -> s e. RR )
524	431 521	breqtrrid	|- ( s = 0 -> -u _pi <_ s )
525	521 432	eqbrtrdi	|- ( s = 0 -> s <_ _pi )
526	520 519 523 524 525	eliccd	|- ( s = 0 -> s e. ( -u _pi [,] _pi ) )
527	57	oveq1i	|- ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) = ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( -u _pi [,] _pi ) )
528	56	cnfldtop	|- ( TopOpen ` CCfld ) e. Top
529		reex	|- RR e. _V
530		restabs	|- ( ( ( TopOpen ` CCfld ) e. Top /\ ( -u _pi [,] _pi ) C_ RR /\ RR e. _V ) -> ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( -u _pi [,] _pi ) ) = ( ( TopOpen ` CCfld ) |`t ( -u _pi [,] _pi ) ) )
531	528 427 529 530	mp3an	|- ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( -u _pi [,] _pi ) ) = ( ( TopOpen ` CCfld ) |`t ( -u _pi [,] _pi ) )
532	527 531	eqtri	|- ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) = ( ( TopOpen ` CCfld ) |`t ( -u _pi [,] _pi ) )
533	56 532	cnplimc	|- ( ( ( -u _pi [,] _pi ) C_ CC /\ s e. ( -u _pi [,] _pi ) ) -> ( K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s ) <-> ( K : ( -u _pi [,] _pi ) --> CC /\ ( K ` s ) e. ( K limCC s ) ) ) )
534	518 526 533	syl2anc	|- ( s = 0 -> ( K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s ) <-> ( K : ( -u _pi [,] _pi ) --> CC /\ ( K ` s ) e. ( K limCC s ) ) ) )
535	15 516 534	mpbir2and	|- ( s = 0 -> K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s ) )
536	535	adantl	|- ( ( s e. ( -u _pi [,] _pi ) /\ s = 0 ) -> K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s ) )
537		simpl	|- ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> s e. ( -u _pi [,] _pi ) )
538	502	notbii	|- ( -. s e. { 0 } <-> -. s = 0 )
539	538	biimpri	|- ( -. s = 0 -> -. s e. { 0 } )
540	539	adantl	|- ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> -. s e. { 0 } )
541	537 540	eldifd	|- ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> s e. ( ( -u _pi [,] _pi ) \ { 0 } ) )
542		fveq2	|- ( x = s -> ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` x ) = ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) )
543	542	eleq2d	|- ( x = s -> ( ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` x ) <-> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) ) )
544	429	ssdifssd	|- ( T. -> ( ( -u _pi [,] _pi ) \ { 0 } ) C_ CC )
545	544 145	idcncfg	|- ( T. -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> s ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) )
546		eqid	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) = ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) )
547		2cnd	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> 2 e. CC )
548		eldifi	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> s e. ( -u _pi [,] _pi ) )
549	517 548	sseldi	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> s e. CC )
550	549	halfcld	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( s / 2 ) e. CC )
551	550	sincld	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( sin ` ( s / 2 ) ) e. CC )
552	547 551	mulcld	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC )
553	81	a1i	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> 2 =/= 0 )
554		eldifsni	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> s =/= 0 )
555	548 554 489	syl2anc	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( sin ` ( s / 2 ) ) =/= 0 )
556	547 551 553 555	mulne0d	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) =/= 0 )
557	556	neneqd	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> -. ( 2 x. ( sin ` ( s / 2 ) ) ) = 0 )
558		elsng	|- ( ( 2 x. ( sin ` ( s / 2 ) ) ) e. CC -> ( ( 2 x. ( sin ` ( s / 2 ) ) ) e. { 0 } <-> ( 2 x. ( sin ` ( s / 2 ) ) ) = 0 ) )
559	552 558	syl	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( ( 2 x. ( sin ` ( s / 2 ) ) ) e. { 0 } <-> ( 2 x. ( sin ` ( s / 2 ) ) ) = 0 ) )
560	557 559	mtbird	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> -. ( 2 x. ( sin ` ( s / 2 ) ) ) e. { 0 } )
561	552 560	eldifd	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. ( CC \ { 0 } ) )
562	546 561	fmpti	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) : ( ( -u _pi [,] _pi ) \ { 0 } ) --> ( CC \ { 0 } )
563		difss	|- ( CC \ { 0 } ) C_ CC
564		eqid	|- ( s e. CC |-> 2 ) = ( s e. CC |-> 2 )
565	175 176 175	constcncfg	|- ( 2 e. CC -> ( s e. CC |-> 2 ) e. ( CC -cn-> CC ) )
566	102 565	mp1i	|- ( T. -> ( s e. CC |-> 2 ) e. ( CC -cn-> CC ) )
567		2cnd	|- ( ( T. /\ s e. ( ( -u _pi [,] _pi ) \ { 0 } ) ) -> 2 e. CC )
568	564 566 544 145 567	cncfmptssg	|- ( T. -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> 2 ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) )
569	549 547 553	divrecd	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( s / 2 ) = ( s x. ( 1 / 2 ) ) )
570	569	mpteq2ia	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / 2 ) ) = ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s x. ( 1 / 2 ) ) )
571		eqid	|- ( s e. CC |-> ( 1 / 2 ) ) = ( s e. CC |-> ( 1 / 2 ) )
572	144	a1i	|- ( ( 1 / 2 ) e. CC -> CC C_ CC )
573		id	|- ( ( 1 / 2 ) e. CC -> ( 1 / 2 ) e. CC )
574	572 573 572	constcncfg	|- ( ( 1 / 2 ) e. CC -> ( s e. CC |-> ( 1 / 2 ) ) e. ( CC -cn-> CC ) )
575	94 574	mp1i	|- ( T. -> ( s e. CC |-> ( 1 / 2 ) ) e. ( CC -cn-> CC ) )
576	94	a1i	|- ( ( T. /\ s e. ( ( -u _pi [,] _pi ) \ { 0 } ) ) -> ( 1 / 2 ) e. CC )
577	571 575 544 145 576	cncfmptssg	|- ( T. -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 1 / 2 ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) )
578	545 577	mulcncf	|- ( T. -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s x. ( 1 / 2 ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) )
579	570 578	eqeltrid	|- ( T. -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / 2 ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) )
580	182 579	cncfmpt1f	|- ( T. -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( sin ` ( s / 2 ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) )
581	568 580	mulcncf	|- ( T. -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) )
582	581	mptru	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC )
583		cncffvrn	|- ( ( ( CC \ { 0 } ) C_ CC /\ ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) ) -> ( ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> ( CC \ { 0 } ) ) <-> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) : ( ( -u _pi [,] _pi ) \ { 0 } ) --> ( CC \ { 0 } ) ) )
584	563 582 583	mp2an	|- ( ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> ( CC \ { 0 } ) ) <-> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) : ( ( -u _pi [,] _pi ) \ { 0 } ) --> ( CC \ { 0 } ) )
585	562 584	mpbir	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> ( CC \ { 0 } ) )
586	585	a1i	|- ( T. -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( s / 2 ) ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> ( CC \ { 0 } ) ) )
587	545 586	divcncf	|- ( T. -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) )
588	587	mptru	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC )
589	428	ssdifssd	|- ( T. -> ( ( -u _pi [,] _pi ) \ { 0 } ) C_ RR )
590	589	mptru	|- ( ( -u _pi [,] _pi ) \ { 0 } ) C_ RR
591	590 12	sstri	|- ( ( -u _pi [,] _pi ) \ { 0 } ) C_ CC
592	57	oveq1i	|- ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) )
593		restabs	|- ( ( ( TopOpen ` CCfld ) e. Top /\ ( ( -u _pi [,] _pi ) \ { 0 } ) C_ RR /\ RR e. _V ) -> ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) )
594	528 590 529 593	mp3an	|- ( ( ( TopOpen ` CCfld ) |`t RR ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) )
595	592 594	eqtri	|- ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) )
596		unicntop	|- CC = U. ( TopOpen ` CCfld )
597	596	restid	|- ( ( TopOpen ` CCfld ) e. Top -> ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld ) )
598	528 597	ax-mp	|- ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld )
599	598	eqcomi	|- ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
600	56 595 599	cncfcn	|- ( ( ( ( -u _pi [,] _pi ) \ { 0 } ) C_ CC /\ CC C_ CC ) -> ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) = ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) Cn ( TopOpen ` CCfld ) ) )
601	591 144 600	mp2an	|- ( ( ( -u _pi [,] _pi ) \ { 0 } ) -cn-> CC ) = ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) Cn ( TopOpen ` CCfld ) )
602	588 601	eleqtri	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) Cn ( TopOpen ` CCfld ) )
603		resttopon	|- ( ( ( topGen ` ran (,) ) e. ( TopOn ` RR ) /\ ( ( -u _pi [,] _pi ) \ { 0 } ) C_ RR ) -> ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) e. ( TopOn ` ( ( -u _pi [,] _pi ) \ { 0 } ) ) )
604	60 590 603	mp2an	|- ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) e. ( TopOn ` ( ( -u _pi [,] _pi ) \ { 0 } ) )
605	56	cnfldtopon	|- ( TopOpen ` CCfld ) e. ( TopOn ` CC )
606		cncnp	|- ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) e. ( TopOn ` ( ( -u _pi [,] _pi ) \ { 0 } ) ) /\ ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) -> ( ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) Cn ( TopOpen ` CCfld ) ) <-> ( ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) : ( ( -u _pi [,] _pi ) \ { 0 } ) --> CC /\ A. x e. ( ( -u _pi [,] _pi ) \ { 0 } ) ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` x ) ) ) )
607	604 605 606	mp2an	|- ( ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) Cn ( TopOpen ` CCfld ) ) <-> ( ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) : ( ( -u _pi [,] _pi ) \ { 0 } ) --> CC /\ A. x e. ( ( -u _pi [,] _pi ) \ { 0 } ) ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` x ) ) )
608	602 607	mpbi	|- ( ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) : ( ( -u _pi [,] _pi ) \ { 0 } ) --> CC /\ A. x e. ( ( -u _pi [,] _pi ) \ { 0 } ) ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` x ) )
609	608	simpri	|- A. x e. ( ( -u _pi [,] _pi ) \ { 0 } ) ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` x )
610	543 609	vtoclri	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) )
611	541 610	syl	|- ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) e. ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) )
612	10	reseq1i	|- ( K |` ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( -u _pi [,] _pi ) \ { 0 } ) )
613		difss	|- ( ( -u _pi [,] _pi ) \ { 0 } ) C_ ( -u _pi [,] _pi )
614		resmpt	|- ( ( ( -u _pi [,] _pi ) \ { 0 } ) C_ ( -u _pi [,] _pi ) -> ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) )
615	613 614	ax-mp	|- ( ( s e. ( -u _pi [,] _pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) |` ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
616		eldifn	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> -. s e. { 0 } )
617	616 502	sylnib	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> -. s = 0 )
618	617 479	syl	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
619	618	mpteq2ia	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) = ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
620	612 615 619	3eqtri	|- ( K |` ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
621		restabs	|- ( ( ( topGen ` ran (,) ) e. Top /\ ( ( -u _pi [,] _pi ) \ { 0 } ) C_ ( -u _pi [,] _pi ) /\ ( -u _pi [,] _pi ) e. _V ) -> ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) )
622	453 613 454 621	mp3an	|- ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) )
623	622	oveq1i	|- ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) = ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) )
624	623	fveq1i	|- ( ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) = ( ( ( ( topGen ` ran (,) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` s )
625	611 620 624	3eltr4g	|- ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> ( K |` ( ( -u _pi [,] _pi ) \ { 0 } ) ) e. ( ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) )
626	452 613	pm3.2i	|- ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) e. Top /\ ( ( -u _pi [,] _pi ) \ { 0 } ) C_ ( -u _pi [,] _pi ) )
627	626	a1i	|- ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) e. Top /\ ( ( -u _pi [,] _pi ) \ { 0 } ) C_ ( -u _pi [,] _pi ) ) )
628		ssdif	|- ( ( -u _pi [,] _pi ) C_ RR -> ( ( -u _pi [,] _pi ) \ { 0 } ) C_ ( RR \ { 0 } ) )
629	427 628	ax-mp	|- ( ( -u _pi [,] _pi ) \ { 0 } ) C_ ( RR \ { 0 } )
630	629 541	sseldi	|- ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> s e. ( RR \ { 0 } ) )
631		sscon	|- ( { 0 } C_ ( -u _pi [,] _pi ) -> ( RR \ ( -u _pi [,] _pi ) ) C_ ( RR \ { 0 } ) )
632	436 631	ax-mp	|- ( RR \ ( -u _pi [,] _pi ) ) C_ ( RR \ { 0 } )
633	629 632	unssi	|- ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) C_ ( RR \ { 0 } )
634		simpr	|- ( ( s e. ( RR \ { 0 } ) /\ s e. ( -u _pi [,] _pi ) ) -> s e. ( -u _pi [,] _pi ) )
635		eldifn	|- ( s e. ( RR \ { 0 } ) -> -. s e. { 0 } )
636	635	adantr	|- ( ( s e. ( RR \ { 0 } ) /\ s e. ( -u _pi [,] _pi ) ) -> -. s e. { 0 } )
637	634 636	eldifd	|- ( ( s e. ( RR \ { 0 } ) /\ s e. ( -u _pi [,] _pi ) ) -> s e. ( ( -u _pi [,] _pi ) \ { 0 } ) )
638		elun1	|- ( s e. ( ( -u _pi [,] _pi ) \ { 0 } ) -> s e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) )
639	637 638	syl	|- ( ( s e. ( RR \ { 0 } ) /\ s e. ( -u _pi [,] _pi ) ) -> s e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) )
640		eldifi	|- ( s e. ( RR \ { 0 } ) -> s e. RR )
641	640	adantr	|- ( ( s e. ( RR \ { 0 } ) /\ -. s e. ( -u _pi [,] _pi ) ) -> s e. RR )
642		simpr	|- ( ( s e. ( RR \ { 0 } ) /\ -. s e. ( -u _pi [,] _pi ) ) -> -. s e. ( -u _pi [,] _pi ) )
643	641 642	eldifd	|- ( ( s e. ( RR \ { 0 } ) /\ -. s e. ( -u _pi [,] _pi ) ) -> s e. ( RR \ ( -u _pi [,] _pi ) ) )
644		elun2	|- ( s e. ( RR \ ( -u _pi [,] _pi ) ) -> s e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) )
645	643 644	syl	|- ( ( s e. ( RR \ { 0 } ) /\ -. s e. ( -u _pi [,] _pi ) ) -> s e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) )
646	639 645	pm2.61dan	|- ( s e. ( RR \ { 0 } ) -> s e. ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) )
647	646	ssriv	|- ( RR \ { 0 } ) C_ ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) )
648	633 647	eqssi	|- ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) = ( RR \ { 0 } )
649	648	fveq2i	|- ( ( int ` ( topGen ` ran (,) ) ) ` ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) ) = ( ( int ` ( topGen ` ran (,) ) ) ` ( RR \ { 0 } ) )
650	61	cldopn	|- ( { 0 } e. ( Clsd ` ( topGen ` ran (,) ) ) -> ( RR \ { 0 } ) e. ( topGen ` ran (,) ) )
651	59 650	ax-mp	|- ( RR \ { 0 } ) e. ( topGen ` ran (,) )
652		isopn3i	|- ( ( ( topGen ` ran (,) ) e. Top /\ ( RR \ { 0 } ) e. ( topGen ` ran (,) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( RR \ { 0 } ) ) = ( RR \ { 0 } ) )
653	453 651 652	mp2an	|- ( ( int ` ( topGen ` ran (,) ) ) ` ( RR \ { 0 } ) ) = ( RR \ { 0 } )
654	649 653	eqtri	|- ( ( int ` ( topGen ` ran (,) ) ) ` ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) ) = ( RR \ { 0 } )
655	630 654	eleqtrrdi	|- ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> s e. ( ( int ` ( topGen ` ran (,) ) ) ` ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) ) )
656	655 537	elind	|- ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> s e. ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) ) i^i ( -u _pi [,] _pi ) ) )
657		eqid	|- ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) = ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) )
658	61 657	restntr	|- ( ( ( topGen ` ran (,) ) e. Top /\ ( -u _pi [,] _pi ) C_ RR /\ ( ( -u _pi [,] _pi ) \ { 0 } ) C_ ( -u _pi [,] _pi ) ) -> ( ( int ` ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) ) ` ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) ) i^i ( -u _pi [,] _pi ) ) )
659	453 427 613 658	mp3an	|- ( ( int ` ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) ) ` ( ( -u _pi [,] _pi ) \ { 0 } ) ) = ( ( ( int ` ( topGen ` ran (,) ) ) ` ( ( ( -u _pi [,] _pi ) \ { 0 } ) u. ( RR \ ( -u _pi [,] _pi ) ) ) ) i^i ( -u _pi [,] _pi ) )
660	656 659	eleqtrrdi	|- ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> s e. ( ( int ` ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) ) ` ( ( -u _pi [,] _pi ) \ { 0 } ) ) )
661	14	a1i	|- ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> K : ( -u _pi [,] _pi ) --> CC )
662	451	toponunii	|- ( -u _pi [,] _pi ) = U. ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) )
663	662 596	cnprest	|- ( ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) e. Top /\ ( ( -u _pi [,] _pi ) \ { 0 } ) C_ ( -u _pi [,] _pi ) ) /\ ( s e. ( ( int ` ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) ) ` ( ( -u _pi [,] _pi ) \ { 0 } ) ) /\ K : ( -u _pi [,] _pi ) --> CC ) ) -> ( K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s ) <-> ( K |` ( ( -u _pi [,] _pi ) \ { 0 } ) ) e. ( ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) ) )
664	627 660 661 663	syl12anc	|- ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> ( K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s ) <-> ( K |` ( ( -u _pi [,] _pi ) \ { 0 } ) ) e. ( ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) |`t ( ( -u _pi [,] _pi ) \ { 0 } ) ) CnP ( TopOpen ` CCfld ) ) ` s ) ) )
665	625 664	mpbird	|- ( ( s e. ( -u _pi [,] _pi ) /\ -. s = 0 ) -> K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s ) )
666	536 665	pm2.61dan	|- ( s e. ( -u _pi [,] _pi ) -> K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s ) )
667	666	rgen	|- A. s e. ( -u _pi [,] _pi ) K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s )
668		cncnp	|- ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) e. ( TopOn ` ( -u _pi [,] _pi ) ) /\ ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) -> ( K e. ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) Cn ( TopOpen ` CCfld ) ) <-> ( K : ( -u _pi [,] _pi ) --> CC /\ A. s e. ( -u _pi [,] _pi ) K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s ) ) ) )
669	451 605 668	mp2an	|- ( K e. ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) Cn ( TopOpen ` CCfld ) ) <-> ( K : ( -u _pi [,] _pi ) --> CC /\ A. s e. ( -u _pi [,] _pi ) K e. ( ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) CnP ( TopOpen ` CCfld ) ) ` s ) ) )
670	14 667 669	mpbir2an	|- K e. ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) Cn ( TopOpen ` CCfld ) )
671	56 532 599	cncfcn	|- ( ( ( -u _pi [,] _pi ) C_ CC /\ CC C_ CC ) -> ( ( -u _pi [,] _pi ) -cn-> CC ) = ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) Cn ( TopOpen ` CCfld ) ) )
672	517 144 671	mp2an	|- ( ( -u _pi [,] _pi ) -cn-> CC ) = ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) Cn ( TopOpen ` CCfld ) )
673	672	eqcomi	|- ( ( ( topGen ` ran (,) ) |`t ( -u _pi [,] _pi ) ) Cn ( TopOpen ` CCfld ) ) = ( ( -u _pi [,] _pi ) -cn-> CC )
674	670 673	eleqtri	|- K e. ( ( -u _pi [,] _pi ) -cn-> CC )
675		cncffvrn	|- ( ( RR C_ CC /\ K e. ( ( -u _pi [,] _pi ) -cn-> CC ) ) -> ( K e. ( ( -u _pi [,] _pi ) -cn-> RR ) <-> K : ( -u _pi [,] _pi ) --> RR ) )
676	12 674 675	mp2an	|- ( K e. ( ( -u _pi [,] _pi ) -cn-> RR ) <-> K : ( -u _pi [,] _pi ) --> RR )
677	11 676	mpbir	|- K e. ( ( -u _pi [,] _pi ) -cn-> RR )