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		tgioo4	\|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) \|`t RR )
57		eqid	\|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
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 56 57 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	mullidd	\|- ( 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 56 57 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	sselid	\|- ( 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	ffvelcdmda	\|- ( ( 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	57 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 57 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	56	oveq1i	\|- ( ( topGen ` ran (,) ) \|`t ( -u _pi [,] _pi ) ) = ( ( ( TopOpen ` CCfld ) \|`t RR ) \|`t ( -u _pi [,] _pi ) )
528	57	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	57 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	sselid	\|- ( 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		cncfcdm	\|- ( ( ( 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	56	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	57 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	57	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	sselid	\|- ( ( 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	57 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		cncfcdm	\|- ( ( 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 )

Metamath Proof Explorer

Theorem fourierdlem62

Proof