Theorem fourierdlem62 32154

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

Hypothesis

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

Assertion

Ref	Expression
fourierdlem62	|- K e. ( ( -u pi [,] pi ) -cn-> RR )

Proof of Theorem fourierdlem62

Dummy variables s x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem62.k	. . . 4 |- K = ( y e. ( -u pi [,] pi ) |-> if ( y = 0 , 1 , ( y / ( 2 x. ( sin ` ( y / 2 ) ) ) ) ) )
2		eqeq1 2461	. . . . . 6 |- ( y = s -> ( y = 0 <-> s = 0 ) )
3		id 22	. . . . . . 7 |- ( y = s -> y = s )
4		oveq1 6303	. . . . . . . . 9 |- ( y = s -> ( y / 2 ) = ( s / 2 ) )
5	4	fveq2d 5876	. . . . . . . 8 |- ( y = s -> ( sin ` ( y / 2 ) ) = ( sin ` ( s / 2 ) ) )
6	5	oveq2d 6312	. . . . . . 7 |- ( y = s -> ( 2 x. ( sin ` ( y / 2 ) ) ) = ( 2 x. ( sin ` ( s / 2 ) ) ) )
7	3, 6	oveq12d 6314	. . . . . 6 |- ( y = s -> ( y / ( 2 x. ( sin ` ( y / 2 ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
8	2, 7	ifbieq2d 3969	. . . . 5 |- ( 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 4548	. . . 4 |- ( 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 2486	. . 3 |- K = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
11	10	fourierdlem43 32135	. 2 |- K : ( -u pi [,] pi ) --> RR
12		ax-resscn 9566	. . 3 |- RR C_ CC
13		fss 5745	. . . . . 6 |- ( ( K : ( -u pi [,] pi ) --> RR /\ RR C_ CC ) -> K : ( -u pi [,] pi ) --> CC )
14	11, 12, 13	mp2an 672	. . . . 5 |- K : ( -u pi [,] pi ) --> CC
15	14	a1i 11	. . . . . . . . 9 |- ( s = 0 -> K : ( -u pi [,] pi ) --> CC )
16		difss 3627	. . . . . . . . . . . . . . . . 17 |- ( ( -u pi (,) pi ) \ { 0 } ) C_ ( -u pi (,) pi )
17		elioore 11584	. . . . . . . . . . . . . . . . . 18 |- ( s e. ( -u pi (,) pi ) -> s e. RR )
18	17	ssriv 3503	. . . . . . . . . . . . . . . . 17 |- ( -u pi (,) pi ) C_ RR
19	16, 18	sstri 3508	. . . . . . . . . . . . . . . 16 |- ( ( -u pi (,) pi ) \ { 0 } ) C_ RR
20	19	a1i 11	. . . . . . . . . . . . . . 15 |- ( T. -> ( ( -u pi (,) pi ) \ { 0 } ) C_ RR )
21		eqid 2457	. . . . . . . . . . . . . . . . 17 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) = ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x )
22	19	sseli 3495	. . . . . . . . . . . . . . . . 17 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) -> x e. RR )
23	21, 22	fmpti 6055	. . . . . . . . . . . . . . . 16 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) : ( ( -u pi (,) pi ) \ { 0 } ) --> RR
24	23	a1i 11	. . . . . . . . . . . . . . 15 |- ( T. -> ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) : ( ( -u pi (,) pi ) \ { 0 } ) --> RR )
25		eqid 2457	. . . . . . . . . . . . . . . . 17 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) = ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) )
26		2re 10626	. . . . . . . . . . . . . . . . . . 19 |- 2 e. RR
27	26	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) -> 2 e. RR )
28	22	rehalfcld 10806	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( x / 2 ) e. RR )
29	28	resincld 13890	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( sin ` ( x / 2 ) ) e. RR )
30	27, 29	remulcld 9641	. . . . . . . . . . . . . . . . 17 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( x / 2 ) ) ) e. RR )
31	25, 30	fmpti 6055	. . . . . . . . . . . . . . . 16 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) : ( ( -u pi (,) pi ) \ { 0 } ) --> RR
32	31	a1i 11	. . . . . . . . . . . . . . 15 |- ( T. -> ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) : ( ( -u pi (,) pi ) \ { 0 } ) --> RR )
33		iooretop 21399	. . . . . . . . . . . . . . . 16 |- ( -u pi (,) pi ) e. ( topGen ` ran (,) )
34	33	a1i 11	. . . . . . . . . . . . . . 15 |- ( T. -> ( -u pi (,) pi ) e. ( topGen ` ran (,) ) )
35		0re 9613	. . . . . . . . . . . . . . . . 17 |- 0 e. RR
36		negpilt0 31665	. . . . . . . . . . . . . . . . 17 |- -u pi < 0
37		pipos 22979	. . . . . . . . . . . . . . . . 17 |- 0 < pi
38		pire 22977	. . . . . . . . . . . . . . . . . . . 20 |- pi e. RR
39	38	renegcli 9899	. . . . . . . . . . . . . . . . . . 19 |- -u pi e. RR
40	39	rexri 9663	. . . . . . . . . . . . . . . . . 18 |- -u pi e. RR*
41	38	rexri 9663	. . . . . . . . . . . . . . . . . 18 |- pi e. RR*
42		elioo2 11595	. . . . . . . . . . . . . . . . . 18 |- ( ( -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 672	. . . . . . . . . . . . . . . . 17 |- ( 0 e. ( -u pi (,) pi ) <-> ( 0 e. RR /\ -u pi < 0 /\ 0 < pi ) )
44	35, 36, 37, 43	mpbir3an 1178	. . . . . . . . . . . . . . . 16 |- 0 e. ( -u pi (,) pi )
45	44	a1i 11	. . . . . . . . . . . . . . 15 |- ( T. -> 0 e. ( -u pi (,) pi ) )
46		eqid 2457	. . . . . . . . . . . . . . 15 |- ( ( -u pi (,) pi ) \ { 0 } ) = ( ( -u pi (,) pi ) \ { 0 } )
47		1ex 9608	. . . . . . . . . . . . . . . . . . 19 |- 1 e. _V
48		eqid 2457	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 ) = ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 )
49	47, 48	dmmpti 5716	. . . . . . . . . . . . . . . . . 18 |- dom ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 ) = ( ( -u pi (,) pi ) \ { 0 } )
50		reelprrecn 9601	. . . . . . . . . . . . . . . . . . . . . . 23 |- RR e. { RR , CC }
51	50	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( T. -> RR e. { RR , CC } )
52	12	sseli 3495	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. RR -> x e. CC )
53	52	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( T. /\ x e. RR ) -> x e. CC )
54		1red 9628	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( T. /\ x e. RR ) -> 1 e. RR )
55	51	dvmptid 22486	. . . . . . . . . . . . . . . . . . . . . 22 |- ( T. -> ( RR _D ( x e. RR |-> x ) ) = ( x e. RR |-> 1 ) )
56		eqid 2457	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
57	56	tgioo2 21434	. . . . . . . . . . . . . . . . . . . . . 22 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
58		sncldre 31636	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 0 e. RR -> { 0 } e. ( Clsd ` ( topGen ` ran (,) ) ) )
59	35, 58	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 |- { 0 } e. ( Clsd ` ( topGen ` ran (,) ) )
60		retopon 21396	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( topGen ` ran (,) ) e. (TopOn ` RR )
61	60	toponunii 19560	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- RR = U. ( topGen ` ran (,) )
62	61	difopn 19662	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( -u pi (,) pi ) e. ( topGen ` ran (,) ) /\ { 0 } e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( ( -u pi (,) pi ) \ { 0 } ) e. ( topGen ` ran (,) ) )
63	33, 59, 62	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( -u pi (,) pi ) \ { 0 } ) e. ( topGen ` ran (,) )
64	63	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( T. -> ( ( -u pi (,) pi ) \ { 0 } ) e. ( topGen ` ran (,) ) )
65	51, 53, 54, 55, 20, 57, 56, 64	dvmptres 22492	. . . . . . . . . . . . . . . . . . . . 21 |- ( T. -> ( RR _D ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) ) = ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 ) )
66	65	trud 1404	. . . . . . . . . . . . . . . . . . . 20 |- ( RR _D ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) ) = ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 )
67	66	eqcomi 2470	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 ) = ( RR _D ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) )
68	67	dmeqi 5214	. . . . . . . . . . . . . . . . . 18 |- dom ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 ) = dom ( RR _D ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) )
69	49, 68	eqtr3i 2488	. . . . . . . . . . . . . . . . 17 |- ( ( -u pi (,) pi ) \ { 0 } ) = dom ( RR _D ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) )
70	69	eqimssi 3553	. . . . . . . . . . . . . . . 16 |- ( ( -u pi (,) pi ) \ { 0 } ) C_ dom ( RR _D ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) )
71	70	a1i 11	. . . . . . . . . . . . . . 15 |- ( T. -> ( ( -u pi (,) pi ) \ { 0 } ) C_ dom ( RR _D ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) ) )
72		fvex 5882	. . . . . . . . . . . . . . . . . . 19 |- ( cos ` ( x / 2 ) ) e. _V
73		eqid 2457	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) = ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) )
74	72, 73	dmmpti 5716	. . . . . . . . . . . . . . . . . 18 |- dom ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) = ( ( -u pi (,) pi ) \ { 0 } )
75		2cnd 10629	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( T. /\ x e. RR ) -> 2 e. CC )
76	53	halfcld 10804	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( T. /\ x e. RR ) -> ( x / 2 ) e. CC )
77	76	sincld 13877	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( T. /\ x e. RR ) -> ( sin ` ( x / 2 ) ) e. CC )
78	75, 77	mulcld 9633	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( T. /\ x e. RR ) -> ( 2 x. ( sin ` ( x / 2 ) ) ) e. CC )
79	76	coscld 13878	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( T. /\ x e. RR ) -> ( cos ` ( x / 2 ) ) e. CC )
80		2cnd 10629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. RR -> 2 e. CC )
81		2ne0 10649	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- 2 =/= 0
82	81	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. RR -> 2 =/= 0 )
83	52, 80, 82	divrec2d 10345	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x e. RR -> ( x / 2 ) = ( ( 1 / 2 ) x. x ) )
84	83	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x e. RR -> ( sin ` ( x / 2 ) ) = ( sin ` ( ( 1 / 2 ) x. x ) ) )
85	84	oveq2d 6312	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x e. RR -> ( 2 x. ( sin ` ( x / 2 ) ) ) = ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) )
86	85	mpteq2ia 4539	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x e. RR |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) = ( x e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) )
87	86	oveq2i 6307	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( RR _D ( x e. RR |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) = ( RR _D ( x e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) )
88		resmpt 5333	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( 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 5	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) |` RR ) = ( x e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) )
90	89	eqcomi 2470	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) = ( ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) |` RR )
91	90	oveq2i 6307	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 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 2457	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) = ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) )
93		2cnd 10629	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x e. CC -> 2 e. CC )
94		halfcn 10776	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( 1 / 2 ) e. CC
95	94	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( x e. CC -> ( 1 / 2 ) e. CC )
96		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( x e. CC -> x e. CC )
97	95, 96	mulcld 9633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. CC -> ( ( 1 / 2 ) x. x ) e. CC )
98	97	sincld 13877	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x e. CC -> ( sin ` ( ( 1 / 2 ) x. x ) ) e. CC )
99	93, 98	mulcld 9633	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x e. CC -> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) e. CC )
100	92, 99	fmpti 6055	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) : CC --> CC
101		eqid 2457	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( 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 10627	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- 2 e. CC
103	102, 94	mulcli 9618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( 2 x. ( 1 / 2 ) ) e. CC
104	103	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( x e. CC -> ( 2 x. ( 1 / 2 ) ) e. CC )
105	97	coscld 13878	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( x e. CC -> ( cos ` ( ( 1 / 2 ) x. x ) ) e. CC )
106	104, 105	mulcld 9633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( x e. CC -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) e. CC )
107	106	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( T. /\ x e. CC ) -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) e. CC )
108	101, 107	dmmptd 5717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( T. -> dom ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) = CC )
109	108	trud 1404	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- dom ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) = CC
110	12, 109	sseqtr4i 3532	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- RR C_ dom ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) )
111		dvasinbx 31920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( 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 672	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( 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 5214	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- 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	sseqtr4i 3532	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- RR C_ dom ( CC _D ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) )
115		dvcnre 31914	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( 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 672	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 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 5279	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 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 5333	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( 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 5	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 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 10296	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( 2 x. ( 1 / 2 ) ) = 1
121	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. RR -> ( 2 x. ( 1 / 2 ) ) = 1 )
122	83	eqcomd 2465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( x e. RR -> ( ( 1 / 2 ) x. x ) = ( x / 2 ) )
123	122	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. RR -> ( cos ` ( ( 1 / 2 ) x. x ) ) = ( cos ` ( x / 2 ) ) )
124	121, 123	oveq12d 6314	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x e. RR -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) = ( 1 x. ( cos ` ( x / 2 ) ) ) )
125	52	halfcld 10804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( x e. RR -> ( x / 2 ) e. CC )
126	125	coscld 13878	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. RR -> ( cos ` ( x / 2 ) ) e. CC )
127	126	mulid2d 9631	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x e. RR -> ( 1 x. ( cos ` ( x / 2 ) ) ) = ( cos ` ( x / 2 ) ) )
128	124, 127	eqtrd 2498	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x e. RR -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) = ( cos ` ( x / 2 ) ) )
129	128	mpteq2ia 4539	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x e. RR |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) = ( x e. RR |-> ( cos ` ( x / 2 ) ) )
130	117, 119, 129	3eqtri 2490	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( CC _D ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) |` RR ) = ( x e. RR |-> ( cos ` ( x / 2 ) ) )
131	91, 116, 130	3eqtri 2490	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( RR _D ( x e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) = ( x e. RR |-> ( cos ` ( x / 2 ) ) )
132	87, 131	eqtri 2486	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( RR _D ( x e. RR |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) = ( x e. RR |-> ( cos ` ( x / 2 ) ) )
133	132	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 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 22492	. . . . . . . . . . . . . . . . . . . . 21 |- ( 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	trud 1404	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 2470	. . . . . . . . . . . . . . . . . . 19 |- ( 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 5214	. . . . . . . . . . . . . . . . . 18 |- 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 2488	. . . . . . . . . . . . . . . . 17 |- ( ( -u pi (,) pi ) \ { 0 } ) = dom ( RR _D ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) )
139	138	eqimssi 3553	. . . . . . . . . . . . . . . 16 |- ( ( -u pi (,) pi ) \ { 0 } ) C_ dom ( RR _D ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) )
140	139	a1i 11	. . . . . . . . . . . . . . 15 |- ( T. -> ( ( -u pi (,) pi ) \ { 0 } ) C_ dom ( RR _D ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) )
141	17	recnd 9639	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s e. ( -u pi (,) pi ) -> s e. CC )
142	141	ssriv 3503	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( -u pi (,) pi ) C_ CC
143	142	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( T. -> ( -u pi (,) pi ) C_ CC )
144		ssid 3518	. . . . . . . . . . . . . . . . . . . . . . 23 |- CC C_ CC
145	144	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( T. -> CC C_ CC )
146	143, 145	idcncfg 31877	. . . . . . . . . . . . . . . . . . . . 21 |- ( T. -> ( x e. ( -u pi (,) pi ) |-> x ) e. ( ( -u pi (,) pi ) -cn-> CC ) )
147	146	trud 1404	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( -u pi (,) pi ) |-> x ) e. ( ( -u pi (,) pi ) -cn-> CC )
148		cnlimc 22418	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( -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 ) lim CC y ) ) ) )
149	142, 148	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 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 ) lim CC y ) ) )
150	147, 149	mpbi 208	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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 ) lim CC y ) )
151	150	simpri 462	. . . . . . . . . . . . . . . . . 18 |- A. y e. ( -u pi (,) pi ) ( ( x e. ( -u pi (,) pi ) |-> x ) ` y ) e. ( ( x e. ( -u pi (,) pi ) |-> x ) lim CC y )
152		fveq2 5872	. . . . . . . . . . . . . . . . . . . 20 |- ( y = 0 -> ( ( x e. ( -u pi (,) pi ) |-> x ) ` y ) = ( ( x e. ( -u pi (,) pi ) |-> x ) ` 0 ) )
153		oveq2 6304	. . . . . . . . . . . . . . . . . . . 20 |- ( y = 0 -> ( ( x e. ( -u pi (,) pi ) |-> x ) lim CC y ) = ( ( x e. ( -u pi (,) pi ) |-> x ) lim CC 0 ) )
154	152, 153	eleq12d 2539	. . . . . . . . . . . . . . . . . . 19 |- ( y = 0 -> ( ( ( x e. ( -u pi (,) pi ) |-> x ) ` y ) e. ( ( x e. ( -u pi (,) pi ) |-> x ) lim CC y ) <-> ( ( x e. ( -u pi (,) pi ) |-> x ) ` 0 ) e. ( ( x e. ( -u pi (,) pi ) |-> x ) lim CC 0 ) ) )
155	154	rspccva 3209	. . . . . . . . . . . . . . . . . 18 |- ( ( A. y e. ( -u pi (,) pi ) ( ( x e. ( -u pi (,) pi ) |-> x ) ` y ) e. ( ( x e. ( -u pi (,) pi ) |-> x ) lim CC y ) /\ 0 e. ( -u pi (,) pi ) ) -> ( ( x e. ( -u pi (,) pi ) |-> x ) ` 0 ) e. ( ( x e. ( -u pi (,) pi ) |-> x ) lim CC 0 ) )
156	151, 44, 155	mp2an 672	. . . . . . . . . . . . . . . . 17 |- ( ( x e. ( -u pi (,) pi ) |-> x ) ` 0 ) e. ( ( x e. ( -u pi (,) pi ) |-> x ) lim CC 0 )
157		id 22	. . . . . . . . . . . . . . . . . . 19 |- ( x = 0 -> x = 0 )
158		eqid 2457	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( -u pi (,) pi ) |-> x ) = ( x e. ( -u pi (,) pi ) |-> x )
159		c0ex 9607	. . . . . . . . . . . . . . . . . . 19 |- 0 e. _V
160	157, 158, 159	fvmpt 5956	. . . . . . . . . . . . . . . . . 18 |- ( 0 e. ( -u pi (,) pi ) -> ( ( x e. ( -u pi (,) pi ) |-> x ) ` 0 ) = 0 )
161	44, 160	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( ( x e. ( -u pi (,) pi ) |-> x ) ` 0 ) = 0
162		elioore 11584	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. ( -u pi (,) pi ) -> x e. RR )
163	162	recnd 9639	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. ( -u pi (,) pi ) -> x e. CC )
164	158, 163	fmpti 6055	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. ( -u pi (,) pi ) |-> x ) : ( -u pi (,) pi ) --> CC
165	164	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( T. -> ( x e. ( -u pi (,) pi ) |-> x ) : ( -u pi (,) pi ) --> CC )
166	165	limcdif 22406	. . . . . . . . . . . . . . . . . . 19 |- ( T. -> ( ( x e. ( -u pi (,) pi ) |-> x ) lim CC 0 ) = ( ( ( x e. ( -u pi (,) pi ) |-> x ) |` ( ( -u pi (,) pi ) \ { 0 } ) ) lim CC 0 ) )
167	166	trud 1404	. . . . . . . . . . . . . . . . . 18 |- ( ( x e. ( -u pi (,) pi ) |-> x ) lim CC 0 ) = ( ( ( x e. ( -u pi (,) pi ) |-> x ) |` ( ( -u pi (,) pi ) \ { 0 } ) ) lim CC 0 )
168		resmpt 5333	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( -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 5	. . . . . . . . . . . . . . . . . . 19 |- ( ( x e. ( -u pi (,) pi ) |-> x ) |` ( ( -u pi (,) pi ) \ { 0 } ) ) = ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x )
170	169	oveq1i 6306	. . . . . . . . . . . . . . . . . 18 |- ( ( ( x e. ( -u pi (,) pi ) |-> x ) |` ( ( -u pi (,) pi ) \ { 0 } ) ) lim CC 0 ) = ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) lim CC 0 )
171	167, 170	eqtri 2486	. . . . . . . . . . . . . . . . 17 |- ( ( x e. ( -u pi (,) pi ) |-> x ) lim CC 0 ) = ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) lim CC 0 )
172	156, 161, 171	3eltr3i 2557	. . . . . . . . . . . . . . . 16 |- 0 e. ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) lim CC 0 )
173	172	a1i 11	. . . . . . . . . . . . . . 15 |- ( T. -> 0 e. ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) lim CC 0 ) )
174		eqid 2457	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. CC |-> 2 ) = ( x e. CC |-> 2 )
175	144	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 2 e. CC -> CC C_ CC )
176		2cnd 10629	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 2 e. CC -> 2 e. CC )
177	175, 176, 175	constcncfg 31876	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 2 e. CC -> ( x e. CC |-> 2 ) e. ( CC -cn-> CC ) )
178	102, 177	mp1i 12	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( T. -> ( x e. CC |-> 2 ) e. ( CC -cn-> CC ) )
179		2cnd 10629	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( T. /\ x e. ( -u pi (,) pi ) ) -> 2 e. CC )
180	174, 178, 143, 145, 179	cncfmptssg 31875	. . . . . . . . . . . . . . . . . . . . . 22 |- ( T. -> ( x e. ( -u pi (,) pi ) |-> 2 ) e. ( ( -u pi (,) pi ) -cn-> CC ) )
181		sincn 22965	. . . . . . . . . . . . . . . . . . . . . . . 24 |- sin e. ( CC -cn-> CC )
182	181	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( T. -> sin e. ( CC -cn-> CC ) )
183		eqid 2457	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x e. CC |-> ( x / 2 ) ) = ( x e. CC |-> ( x / 2 ) )
184	183	divccncf 21536	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 2 e. CC /\ 2 =/= 0 ) -> ( x e. CC |-> ( x / 2 ) ) e. ( CC -cn-> CC ) )
185	102, 81, 184	mp2an 672	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x e. CC |-> ( x / 2 ) ) e. ( CC -cn-> CC )
186	185	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( T. -> ( x e. CC |-> ( x / 2 ) ) e. ( CC -cn-> CC ) )
187	163	adantl 466	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( T. /\ x e. ( -u pi (,) pi ) ) -> x e. CC )
188	187	halfcld 10804	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( T. /\ x e. ( -u pi (,) pi ) ) -> ( x / 2 ) e. CC )
189	183, 186, 143, 145, 188	cncfmptssg 31875	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( T. -> ( x e. ( -u pi (,) pi ) |-> ( x / 2 ) ) e. ( ( -u pi (,) pi ) -cn-> CC ) )
190	182, 189	cncfmpt1f 21543	. . . . . . . . . . . . . . . . . . . . . 22 |- ( T. -> ( x e. ( -u pi (,) pi ) |-> ( sin ` ( x / 2 ) ) ) e. ( ( -u pi (,) pi ) -cn-> CC ) )
191	180, 190	mulcncf 21985	. . . . . . . . . . . . . . . . . . . . 21 |- ( T. -> ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) e. ( ( -u pi (,) pi ) -cn-> CC ) )
192	191	trud 1404	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) e. ( ( -u pi (,) pi ) -cn-> CC )
193		cnlimc 22418	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( -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 ) ) ) ) lim CC y ) ) ) )
194	142, 193	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 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 ) ) ) ) lim CC y ) ) )
195	192, 194	mpbi 208	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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 ) ) ) ) lim CC y ) )
196	195	simpri 462	. . . . . . . . . . . . . . . . . 18 |- 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 ) ) ) ) lim CC y )
197		fveq2 5872	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 6304	. . . . . . . . . . . . . . . . . . . 20 |- ( y = 0 -> ( ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) lim CC y ) = ( ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) lim CC 0 ) )
199	197, 198	eleq12d 2539	. . . . . . . . . . . . . . . . . . 19 |- ( y = 0 -> ( ( ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) e. ( ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) lim CC y ) <-> ( ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` 0 ) e. ( ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) lim CC 0 ) ) )
200	199	rspccva 3209	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) ) ) ) lim CC 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 ) ) ) ) lim CC 0 ) )
201	196, 44, 200	mp2an 672	. . . . . . . . . . . . . . . . 17 |- ( ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` 0 ) e. ( ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) lim CC 0 )
202		oveq1 6303	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x = 0 -> ( x / 2 ) = ( 0 / 2 ) )
203	102, 81	div0i 10299	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 0 / 2 ) = 0
204	202, 203	syl6eq 2514	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = 0 -> ( x / 2 ) = 0 )
205	204	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = 0 -> ( sin ` ( x / 2 ) ) = ( sin ` 0 ) )
206		sin0 13896	. . . . . . . . . . . . . . . . . . . . . 22 |- ( sin ` 0 ) = 0
207	205, 206	syl6eq 2514	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = 0 -> ( sin ` ( x / 2 ) ) = 0 )
208	207	oveq2d 6312	. . . . . . . . . . . . . . . . . . . 20 |- ( x = 0 -> ( 2 x. ( sin ` ( x / 2 ) ) ) = ( 2 x. 0 ) )
209		2t0e0 10712	. . . . . . . . . . . . . . . . . . . 20 |- ( 2 x. 0 ) = 0
210	208, 209	syl6eq 2514	. . . . . . . . . . . . . . . . . . 19 |- ( x = 0 -> ( 2 x. ( sin ` ( x / 2 ) ) ) = 0 )
211		eqid 2457	. . . . . . . . . . . . . . . . . . 19 |- ( 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 5956	. . . . . . . . . . . . . . . . . 18 |- ( 0 e. ( -u pi (,) pi ) -> ( ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` 0 ) = 0 )
213	44, 212	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` 0 ) = 0
214		2cnd 10629	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. ( -u pi (,) pi ) -> 2 e. CC )
215	163	halfcld 10804	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x e. ( -u pi (,) pi ) -> ( x / 2 ) e. CC )
216	215	sincld 13877	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. ( -u pi (,) pi ) -> ( sin ` ( x / 2 ) ) e. CC )
217	214, 216	mulcld 9633	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. ( -u pi (,) pi ) -> ( 2 x. ( sin ` ( x / 2 ) ) ) e. CC )
218	211, 217	fmpti 6055	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) : ( -u pi (,) pi ) --> CC
219	218	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( T. -> ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) : ( -u pi (,) pi ) --> CC )
220	219	limcdif 22406	. . . . . . . . . . . . . . . . . . 19 |- ( T. -> ( ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) lim CC 0 ) = ( ( ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) |` ( ( -u pi (,) pi ) \ { 0 } ) ) lim CC 0 ) )
221	220	trud 1404	. . . . . . . . . . . . . . . . . 18 |- ( ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) lim CC 0 ) = ( ( ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) |` ( ( -u pi (,) pi ) \ { 0 } ) ) lim CC 0 )
222		resmpt 5333	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( -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 5	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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 6306	. . . . . . . . . . . . . . . . . 18 |- ( ( ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) |` ( ( -u pi (,) pi ) \ { 0 } ) ) lim CC 0 ) = ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) lim CC 0 )
225	221, 224	eqtri 2486	. . . . . . . . . . . . . . . . 17 |- ( ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) lim CC 0 ) = ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) lim CC 0 )
226	201, 213, 225	3eltr3i 2557	. . . . . . . . . . . . . . . 16 |- 0 e. ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) lim CC 0 )
227	226	a1i 11	. . . . . . . . . . . . . . 15 |- ( T. -> 0 e. ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) lim CC 0 ) )
228		eqidd 2458	. . . . . . . . . . . . . . . . . . . . 21 |- ( 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 6303	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x = y -> ( x / 2 ) = ( y / 2 ) )
230	229	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = y -> ( sin ` ( x / 2 ) ) = ( sin ` ( y / 2 ) ) )
231	230	oveq2d 6312	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = y -> ( 2 x. ( sin ` ( x / 2 ) ) ) = ( 2 x. ( sin ` ( y / 2 ) ) ) )
232	231	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( y e. ( ( -u pi (,) pi ) \ { 0 } ) /\ x = y ) -> ( 2 x. ( sin ` ( x / 2 ) ) ) = ( 2 x. ( sin ` ( y / 2 ) ) ) )
233		id 22	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> y e. ( ( -u pi (,) pi ) \ { 0 } ) )
234	26	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> 2 e. RR )
235	19	sseli 3495	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> y e. RR )
236	235	rehalfcld 10806	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( y / 2 ) e. RR )
237	236	resincld 13890	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( sin ` ( y / 2 ) ) e. RR )
238	234, 237	remulcld 9641	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( y / 2 ) ) ) e. RR )
239	228, 232, 233, 238	fvmptd 5961	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 10629	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> 2 e. CC )
241	237	recnd 9639	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( sin ` ( y / 2 ) ) e. CC )
242	81	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> 2 =/= 0 )
243		ioossicc 11635	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( -u pi (,) pi ) C_ ( -u pi [,] pi )
244		eldifi 3622	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> y e. ( -u pi (,) pi ) )
245	243, 244	sseldi 3497	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> y e. ( -u pi [,] pi ) )
246		eldifsni 4158	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> y =/= 0 )
247		fourierdlem44 32136	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( y e. ( -u pi [,] pi ) /\ y =/= 0 ) -> ( sin ` ( y / 2 ) ) =/= 0 )
248	245, 246, 247	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( sin ` ( y / 2 ) ) =/= 0 )
249	240, 241, 242, 248	mulne0d 10222	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( y / 2 ) ) ) =/= 0 )
250	239, 249	eqnetrd 2750	. . . . . . . . . . . . . . . . . . 19 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) =/= 0 )
251	250	neneqd 2659	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> -. ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) = 0 )
252	251	nrex 2912	. . . . . . . . . . . . . . . . 17 |- -. E. y e. ( ( -u pi (,) pi ) \ { 0 } ) ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) = 0
253	25	fnmpt 5713	. . . . . . . . . . . . . . . . . . 19 |- ( 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 2820	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) Fn ( ( -u pi (,) pi ) \ { 0 } )
255		ssid 3518	. . . . . . . . . . . . . . . . . 18 |- ( ( -u pi (,) pi ) \ { 0 } ) C_ ( ( -u pi (,) pi ) \ { 0 } )
256		fvelimab 5929	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 672	. . . . . . . . . . . . . . . . 17 |- ( 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 299	. . . . . . . . . . . . . . . 16 |- -. 0 e. ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) " ( ( -u pi (,) pi ) \ { 0 } ) )
259	258	a1i 11	. . . . . . . . . . . . . . 15 |- ( T. -> -. 0 e. ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) " ( ( -u pi (,) pi ) \ { 0 } ) ) )
260		eqidd 2458	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 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 5876	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = y -> ( cos ` ( x / 2 ) ) = ( cos ` ( y / 2 ) ) )
262	261	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( y e. ( ( -u pi (,) pi ) \ { 0 } ) /\ x = y ) -> ( cos ` ( x / 2 ) ) = ( cos ` ( y / 2 ) ) )
263	235	recnd 9639	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> y e. CC )
264	263	halfcld 10804	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( y / 2 ) e. CC )
265	264	coscld 13878	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( cos ` ( y / 2 ) ) e. CC )
266	260, 262, 233, 265	fvmptd 5961	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) ` y ) = ( cos ` ( y / 2 ) ) )
267	236	rered 13069	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( Re ` ( y / 2 ) ) = ( y / 2 ) )
268		halfpire 22983	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( pi / 2 ) e. RR
269	268	renegcli 9899	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- -u ( pi / 2 ) e. RR
270	269	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> -u ( pi / 2 ) e. RR )
271	270	rexrd 9660	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> -u ( pi / 2 ) e. RR* )
272	268	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( pi / 2 ) e. RR )
273	272	rexrd 9660	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( pi / 2 ) e. RR* )
274		picn 22978	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- pi e. CC
275		divneg 10260	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( pi e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> -u ( pi / 2 ) = ( -u pi / 2 ) )
276	274, 102, 81, 275	mp3an 1324	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- -u ( pi / 2 ) = ( -u pi / 2 )
277	39	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> -u pi e. RR )
278		2rp 11250	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- 2 e. RR+
279	278	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> 2 e. RR+ )
280	40	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> -u pi e. RR* )
281	41	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> pi e. RR* )
282		ioogtlb 31731	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( -u pi e. RR* /\ pi e. RR* /\ y e. ( -u pi (,) pi ) ) -> -u pi < y )
283	280, 281, 244, 282	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> -u pi < y )
284	277, 235, 279, 283	ltdiv1dd 11334	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( -u pi / 2 ) < ( y / 2 ) )
285	276, 284	syl5eqbr 4489	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> -u ( pi / 2 ) < ( y / 2 ) )
286	38	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> pi e. RR )
287		iooltub 31751	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( -u pi e. RR* /\ pi e. RR* /\ y e. ( -u pi (,) pi ) ) -> y < pi )
288	280, 281, 244, 287	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> y < pi )
289	235, 286, 279, 288	ltdiv1dd 11334	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( y / 2 ) < ( pi / 2 ) )
290	271, 273, 236, 285, 289	eliood 31734	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( y / 2 ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) )
291	267, 290	eqeltrd 2545	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( Re ` ( y / 2 ) ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) )
292		cosne0 23043	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( y / 2 ) e. CC /\ ( Re ` ( y / 2 ) ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) ) -> ( cos ` ( y / 2 ) ) =/= 0 )
293	264, 291, 292	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( cos ` ( y / 2 ) ) =/= 0 )
294	266, 293	eqnetrd 2750	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) ` y ) =/= 0 )
295	294	neneqd 2659	. . . . . . . . . . . . . . . . . . 19 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> -. ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) ` y ) = 0 )
296	295	nrex 2912	. . . . . . . . . . . . . . . . . 18 |- -. E. y e. ( ( -u pi (,) pi ) \ { 0 } ) ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) ` y ) = 0
297	72, 73	fnmpti 5715	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) Fn ( ( -u pi (,) pi ) \ { 0 } )
298		fvelimab 5929	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 672	. . . . . . . . . . . . . . . . . 18 |- ( 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 299	. . . . . . . . . . . . . . . . 17 |- -. 0 e. ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) " ( ( -u pi (,) pi ) \ { 0 } ) )
301	135	imaeq1i 5344	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 2535	. . . . . . . . . . . . . . . . 17 |- ( 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 299	. . . . . . . . . . . . . . . 16 |- -. 0 e. ( ( RR _D ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) " ( ( -u pi (,) pi ) \ { 0 } ) )
304	303	a1i 11	. . . . . . . . . . . . . . 15 |- ( T. -> -. 0 e. ( ( RR _D ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ) " ( ( -u pi (,) pi ) \ { 0 } ) ) )
305		eqid 2457	. . . . . . . . . . . . . . . . 17 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( s / 2 ) ) ) = ( s e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( s / 2 ) ) )
306		eqid 2457	. . . . . . . . . . . . . . . . 17 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 1 / ( cos ` ( s / 2 ) ) ) ) = ( s e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 1 / ( cos ` ( s / 2 ) ) ) )
307	19	sseli 3495	. . . . . . . . . . . . . . . . . . . . . 22 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> s e. RR )
308	307	recnd 9639	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> s e. CC )
309	308	halfcld 10804	. . . . . . . . . . . . . . . . . . . 20 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( s / 2 ) e. CC )
310	309	coscld 13878	. . . . . . . . . . . . . . . . . . 19 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( cos ` ( s / 2 ) ) e. CC )
311	307	rehalfcld 10806	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( s / 2 ) e. RR )
312	311	rered 13069	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( Re ` ( s / 2 ) ) = ( s / 2 ) )
313	269	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> -u ( pi / 2 ) e. RR )
314	313	rexrd 9660	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> -u ( pi / 2 ) e. RR* )
315	268	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( pi / 2 ) e. RR )
316	315	rexrd 9660	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( pi / 2 ) e. RR* )
317	38	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> pi e. RR )
318	317	renegcld 10007	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> -u pi e. RR )
319	278	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> 2 e. RR+ )
320	40	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> -u pi e. RR* )
321	41	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> pi e. RR* )
322		eldifi 3622	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> s e. ( -u pi (,) pi ) )
323		ioogtlb 31731	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( -u pi e. RR* /\ pi e. RR* /\ s e. ( -u pi (,) pi ) ) -> -u pi < s )
324	320, 321, 322, 323	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> -u pi < s )
325	318, 307, 319, 324	ltdiv1dd 11334	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( -u pi / 2 ) < ( s / 2 ) )
326	276, 325	syl5eqbr 4489	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> -u ( pi / 2 ) < ( s / 2 ) )
327		iooltub 31751	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( -u pi e. RR* /\ pi e. RR* /\ s e. ( -u pi (,) pi ) ) -> s < pi )
328	320, 321, 322, 327	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> s < pi )
329	307, 317, 319, 328	ltdiv1dd 11334	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( s / 2 ) < ( pi / 2 ) )
330	314, 316, 311, 326, 329	eliood 31734	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( s / 2 ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) )
331	312, 330	eqeltrd 2545	. . . . . . . . . . . . . . . . . . . . . 22 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( Re ` ( s / 2 ) ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) )
332		cosne0 23043	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( s / 2 ) e. CC /\ ( Re ` ( s / 2 ) ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) ) -> ( cos ` ( s / 2 ) ) =/= 0 )
333	309, 331, 332	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( cos ` ( s / 2 ) ) =/= 0 )
334	333	neneqd 2659	. . . . . . . . . . . . . . . . . . . 20 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> -. ( cos ` ( s / 2 ) ) = 0 )
335	311	recoscld 13891	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( cos ` ( s / 2 ) ) e. RR )
336		elsncg 4055	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( cos ` ( s / 2 ) ) e. RR -> ( ( cos ` ( s / 2 ) ) e. { 0 } <-> ( cos ` ( s / 2 ) ) = 0 ) )
337	335, 336	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( ( cos ` ( s / 2 ) ) e. { 0 } <-> ( cos ` ( s / 2 ) ) = 0 ) )
338	334, 337	mtbird 301	. . . . . . . . . . . . . . . . . . 19 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> -. ( cos ` ( s / 2 ) ) e. { 0 } )
339	310, 338	eldifd 3482	. . . . . . . . . . . . . . . . . 18 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( cos ` ( s / 2 ) ) e. ( CC \ { 0 } ) )
340	339	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ s e. ( ( -u pi (,) pi ) \ { 0 } ) ) -> ( cos ` ( s / 2 ) ) e. ( CC \ { 0 } ) )
341	309	ad2antrl 727	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ ( s e. ( ( -u pi (,) pi ) \ { 0 } ) /\ ( s / 2 ) =/= 0 ) ) -> ( s / 2 ) e. CC )
342		cosf 13872	. . . . . . . . . . . . . . . . . . . 20 |- cos : CC --> CC
343	342	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( T. -> cos : CC --> CC )
344	343	ffvelrnda 6032	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ x e. CC ) -> ( cos ` x ) e. CC )
345		eqid 2457	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. CC |-> ( s / 2 ) ) = ( s e. CC |-> ( s / 2 ) )
346	345	divccncf 21536	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 2 e. CC /\ 2 =/= 0 ) -> ( s e. CC |-> ( s / 2 ) ) e. ( CC -cn-> CC ) )
347	102, 81, 346	mp2an 672	. . . . . . . . . . . . . . . . . . . . . 22 |- ( s e. CC |-> ( s / 2 ) ) e. ( CC -cn-> CC )
348	347	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( T. -> ( s e. CC |-> ( s / 2 ) ) e. ( CC -cn-> CC ) )
349	141	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( T. /\ s e. ( -u pi (,) pi ) ) -> s e. CC )
350	349	halfcld 10804	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( T. /\ s e. ( -u pi (,) pi ) ) -> ( s / 2 ) e. CC )
351	345, 348, 143, 145, 350	cncfmptssg 31875	. . . . . . . . . . . . . . . . . . . 20 |- ( T. -> ( s e. ( -u pi (,) pi ) |-> ( s / 2 ) ) e. ( ( -u pi (,) pi ) -cn-> CC ) )
352		oveq1 6303	. . . . . . . . . . . . . . . . . . . . 21 |- ( s = 0 -> ( s / 2 ) = ( 0 / 2 ) )
353	352, 203	syl6eq 2514	. . . . . . . . . . . . . . . . . . . 20 |- ( s = 0 -> ( s / 2 ) = 0 )
354	351, 45, 353	cnmptlimc 22420	. . . . . . . . . . . . . . . . . . 19 |- ( T. -> 0 e. ( ( s e. ( -u pi (,) pi ) |-> ( s / 2 ) ) lim CC 0 ) )
355		eqid 2457	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s e. ( -u pi (,) pi ) |-> ( s / 2 ) ) = ( s e. ( -u pi (,) pi ) |-> ( s / 2 ) )
356	141	halfcld 10804	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s e. ( -u pi (,) pi ) -> ( s / 2 ) e. CC )
357	355, 356	fmpti 6055	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( s e. ( -u pi (,) pi ) |-> ( s / 2 ) ) : ( -u pi (,) pi ) --> CC
358	357	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( T. -> ( s e. ( -u pi (,) pi ) |-> ( s / 2 ) ) : ( -u pi (,) pi ) --> CC )
359	358	limcdif 22406	. . . . . . . . . . . . . . . . . . . . 21 |- ( T. -> ( ( s e. ( -u pi (,) pi ) |-> ( s / 2 ) ) lim CC 0 ) = ( ( ( s e. ( -u pi (,) pi ) |-> ( s / 2 ) ) |` ( ( -u pi (,) pi ) \ { 0 } ) ) lim CC 0 ) )
360	359	trud 1404	. . . . . . . . . . . . . . . . . . . 20 |- ( ( s e. ( -u pi (,) pi ) |-> ( s / 2 ) ) lim CC 0 ) = ( ( ( s e. ( -u pi (,) pi ) |-> ( s / 2 ) ) |` ( ( -u pi (,) pi ) \ { 0 } ) ) lim CC 0 )
361		resmpt 5333	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( -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 5	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( s e. ( -u pi (,) pi ) |-> ( s / 2 ) ) |` ( ( -u pi (,) pi ) \ { 0 } ) ) = ( s e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( s / 2 ) )
363	362	oveq1i 6306	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( s e. ( -u pi (,) pi ) |-> ( s / 2 ) ) |` ( ( -u pi (,) pi ) \ { 0 } ) ) lim CC 0 ) = ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( s / 2 ) ) lim CC 0 )
364	360, 363	eqtri 2486	. . . . . . . . . . . . . . . . . . 19 |- ( ( s e. ( -u pi (,) pi ) |-> ( s / 2 ) ) lim CC 0 ) = ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( s / 2 ) ) lim CC 0 )
365	354, 364	syl6eleq 2555	. . . . . . . . . . . . . . . . . 18 |- ( T. -> 0 e. ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( s / 2 ) ) lim CC 0 ) )
366		ffn 5737	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( cos : CC --> CC -> cos Fn CC )
367	342, 366	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 |- cos Fn CC
368		dffn5 5918	. . . . . . . . . . . . . . . . . . . . . 22 |- ( cos Fn CC <-> cos = ( x e. CC |-> ( cos ` x ) ) )
369	367, 368	mpbi 208	. . . . . . . . . . . . . . . . . . . . 21 |- cos = ( x e. CC |-> ( cos ` x ) )
370		coscn 22966	. . . . . . . . . . . . . . . . . . . . 21 |- cos e. ( CC -cn-> CC )
371	369, 370	eqeltrri 2542	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. CC |-> ( cos ` x ) ) e. ( CC -cn-> CC )
372	371	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( T. -> ( x e. CC |-> ( cos ` x ) ) e. ( CC -cn-> CC ) )
373		0cnd 9606	. . . . . . . . . . . . . . . . . . 19 |- ( T. -> 0 e. CC )
374		fveq2 5872	. . . . . . . . . . . . . . . . . . . 20 |- ( x = 0 -> ( cos ` x ) = ( cos ` 0 ) )
375		cos0 13897	. . . . . . . . . . . . . . . . . . . 20 |- ( cos ` 0 ) = 1
376	374, 375	syl6eq 2514	. . . . . . . . . . . . . . . . . . 19 |- ( x = 0 -> ( cos ` x ) = 1 )
377	372, 373, 376	cnmptlimc 22420	. . . . . . . . . . . . . . . . . 18 |- ( T. -> 1 e. ( ( x e. CC |-> ( cos ` x ) ) lim CC 0 ) )
378		fveq2 5872	. . . . . . . . . . . . . . . . . 18 |- ( x = ( s / 2 ) -> ( cos ` x ) = ( cos ` ( s / 2 ) ) )
379		fveq2 5872	. . . . . . . . . . . . . . . . . . . 20 |- ( ( s / 2 ) = 0 -> ( cos ` ( s / 2 ) ) = ( cos ` 0 ) )
380	379, 375	syl6eq 2514	. . . . . . . . . . . . . . . . . . 19 |- ( ( s / 2 ) = 0 -> ( cos ` ( s / 2 ) ) = 1 )
381	380	ad2antll 728	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ ( s e. ( ( -u pi (,) pi ) \ { 0 } ) /\ ( s / 2 ) = 0 ) ) -> ( cos ` ( s / 2 ) ) = 1 )
382	341, 344, 365, 377, 378, 381	limcco 22423	. . . . . . . . . . . . . . . . 17 |- ( T. -> 1 e. ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( s / 2 ) ) ) lim CC 0 ) )
383		ax-1ne0 9578	. . . . . . . . . . . . . . . . . 18 |- 1 =/= 0
384	383	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( T. -> 1 =/= 0 )
385	305, 306, 340, 382, 384	reclimc 31862	. . . . . . . . . . . . . . . 16 |- ( T. -> ( 1 / 1 ) e. ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 1 / ( cos ` ( s / 2 ) ) ) ) lim CC 0 ) )
386		1div1e1 10258	. . . . . . . . . . . . . . . 16 |- ( 1 / 1 ) = 1
387	66	fveq1i 5873	. . . . . . . . . . . . . . . . . . . 20 |- ( ( RR _D ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) ) ` s ) = ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 ) ` s )
388		eqidd 2458	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 ) = ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 ) )
389		eqidd 2458	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) /\ x = s ) -> 1 = 1 )
390		id 22	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> s e. ( ( -u pi (,) pi ) \ { 0 } ) )
391		1red 9628	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> 1 e. RR )
392	388, 389, 390, 391	fvmptd 5961	. . . . . . . . . . . . . . . . . . . 20 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 ) ` s ) = 1 )
393	387, 392	syl5req 2511	. . . . . . . . . . . . . . . . . . 19 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> 1 = ( ( RR _D ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) ) ` s ) )
394	135	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( 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 6303	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = s -> ( x / 2 ) = ( s / 2 ) )
396	395	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = s -> ( cos ` ( x / 2 ) ) = ( cos ` ( s / 2 ) ) )
397	396	adantl 466	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) /\ x = s ) -> ( cos ` ( x / 2 ) ) = ( cos ` ( s / 2 ) ) )
398	394, 397, 390, 335	fvmptd 5961	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 2465	. . . . . . . . . . . . . . . . . . 19 |- ( 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 6314	. . . . . . . . . . . . . . . . . 18 |- ( 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 4539	. . . . . . . . . . . . . . . . 17 |- ( 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 6306	. . . . . . . . . . . . . . . 16 |- ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 1 / ( cos ` ( s / 2 ) ) ) ) lim CC 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 ) ) ) lim CC 0 )
403	385, 386, 402	3eltr3g 2561	. . . . . . . . . . . . . . 15 |- ( 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 ) ) ) lim CC 0 ) )
404	20, 24, 32, 34, 45, 46, 71, 140, 173, 227, 259, 304, 403	lhop 22543	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) lim CC 0 ) )
405	404	trud 1404	. . . . . . . . . . . . 13 |- 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 ) ) ) lim CC 0 )
406		eqidd 2458	. . . . . . . . . . . . . . . . 17 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) = ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) )
407		simpr 461	. . . . . . . . . . . . . . . . 17 |- ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) /\ x = s ) -> x = s )
408	406, 407, 390, 307	fvmptd 5961	. . . . . . . . . . . . . . . 16 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) ` s ) = s )
409		eqidd 2458	. . . . . . . . . . . . . . . . 17 |- ( 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 6311	. . . . . . . . . . . . . . . . . . 19 |- ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) /\ x = s ) -> ( x / 2 ) = ( s / 2 ) )
411	410	fveq2d 5876	. . . . . . . . . . . . . . . . . 18 |- ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) /\ x = s ) -> ( sin ` ( x / 2 ) ) = ( sin ` ( s / 2 ) ) )
412	411	oveq2d 6312	. . . . . . . . . . . . . . . . 17 |- ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) /\ x = s ) -> ( 2 x. ( sin ` ( x / 2 ) ) ) = ( 2 x. ( sin ` ( s / 2 ) ) ) )
413	26	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> 2 e. RR )
414	311	resincld 13890	. . . . . . . . . . . . . . . . . 18 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( sin ` ( s / 2 ) ) e. RR )
415	413, 414	remulcld 9641	. . . . . . . . . . . . . . . . 17 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. RR )
416	409, 412, 390, 415	fvmptd 5961	. . . . . . . . . . . . . . . 16 |- ( 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 6314	. . . . . . . . . . . . . . 15 |- ( 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 4539	. . . . . . . . . . . . . 14 |- ( 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 6306	. . . . . . . . . . . . 13 |- ( ( 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 ) ) ) lim CC 0 ) = ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) lim CC 0 )
420	405, 419	eleqtri 2543	. . . . . . . . . . . 12 |- 1 e. ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) lim CC 0 )
421	10	oveq1i 6306	. . . . . . . . . . . . . 14 |- ( K lim CC 0 ) = ( ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) ) lim CC 0 )
422	10	feq1i 5729	. . . . . . . . . . . . . . . . . . 19 |- ( 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 208	. . . . . . . . . . . . . . . . . 18 |- ( s e. ( -u pi [,] pi ) |-> if ( s =