Theorem fourierdlem62 37858

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 2427	. . . . . 6 |- ( y = s -> ( y = 0 <-> s = 0 ) )
3		id 23	. . . . . . 7 |- ( y = s -> y = s )
4		oveq1 6310	. . . . . . . . 9 |- ( y = s -> ( y / 2 ) = ( s / 2 ) )
5	4	fveq2d 5883	. . . . . . . 8 |- ( y = s -> ( sin ` ( y / 2 ) ) = ( sin ` ( s / 2 ) ) )
6	5	oveq2d 6319	. . . . . . 7 |- ( y = s -> ( 2 x. ( sin ` ( y / 2 ) ) ) = ( 2 x. ( sin ` ( s / 2 ) ) ) )
7	3, 6	oveq12d 6321	. . . . . 6 |- ( y = s -> ( y / ( 2 x. ( sin ` ( y / 2 ) ) ) ) = ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) )
8	2, 7	ifbieq2d 3935	. . . . 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 4514	. . . 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 2452	. . 3 |- K = ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 1 , ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) )
11	10	fourierdlem43 37840	. 2 |- K : ( -u pi [,] pi ) --> RR
12		ax-resscn 9598	. . 3 |- RR C_ CC
13		fss 5752	. . . . . 6 |- ( ( K : ( -u pi [,] pi ) --> RR /\ RR C_ CC ) -> K : ( -u pi [,] pi ) --> CC )
14	11, 12, 13	mp2an 677	. . . . 5 |- K : ( -u pi [,] pi ) --> CC
15	14	a1i 11	. . . . . . . . 9 |- ( s = 0 -> K : ( -u pi [,] pi ) --> CC )
16		difss 3593	. . . . . . . . . . . . . . . . 17 |- ( ( -u pi (,) pi ) \ { 0 } ) C_ ( -u pi (,) pi )
17		elioore 11668	. . . . . . . . . . . . . . . . . 18 |- ( s e. ( -u pi (,) pi ) -> s e. RR )
18	17	ssriv 3469	. . . . . . . . . . . . . . . . 17 |- ( -u pi (,) pi ) C_ RR
19	16, 18	sstri 3474	. . . . . . . . . . . . . . . 16 |- ( ( -u pi (,) pi ) \ { 0 } ) C_ RR
20	19	a1i 11	. . . . . . . . . . . . . . 15 |- ( T. -> ( ( -u pi (,) pi ) \ { 0 } ) C_ RR )
21		eqid 2423	. . . . . . . . . . . . . . . . 17 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) = ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x )
22	19	sseli 3461	. . . . . . . . . . . . . . . . 17 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) -> x e. RR )
23	21, 22	fmpti 6058	. . . . . . . . . . . . . . . 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 2423	. . . . . . . . . . . . . . . . 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 10681	. . . . . . . . . . . . . . . . . . 19 |- 2 e. RR
27	26	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) -> 2 e. RR )
28	22	rehalfcld 10861	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( x / 2 ) e. RR )
29	28	resincld 14190	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( sin ` ( x / 2 ) ) e. RR )
30	27, 29	remulcld 9673	. . . . . . . . . . . . . . . . 17 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( x / 2 ) ) ) e. RR )
31	25, 30	fmpti 6058	. . . . . . . . . . . . . . . 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 21778	. . . . . . . . . . . . . . . 16 |- ( -u pi (,) pi ) e. ( topGen ` ran (,) )
34	33	a1i 11	. . . . . . . . . . . . . . 15 |- ( T. -> ( -u pi (,) pi ) e. ( topGen ` ran (,) ) )
35		0re 9645	. . . . . . . . . . . . . . . . 17 |- 0 e. RR
36		negpilt0 37338	. . . . . . . . . . . . . . . . 17 |- -u pi < 0
37		pipos 23407	. . . . . . . . . . . . . . . . 17 |- 0 < pi
38		pire 23405	. . . . . . . . . . . . . . . . . . . 20 |- pi e. RR
39	38	renegcli 9937	. . . . . . . . . . . . . . . . . . 19 |- -u pi e. RR
40	39	rexri 9695	. . . . . . . . . . . . . . . . . 18 |- -u pi e. RR*
41	38	rexri 9695	. . . . . . . . . . . . . . . . . 18 |- pi e. RR*
42		elioo2 11679	. . . . . . . . . . . . . . . . . 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 677	. . . . . . . . . . . . . . . . 17 |- ( 0 e. ( -u pi (,) pi ) <-> ( 0 e. RR /\ -u pi < 0 /\ 0 < pi ) )
44	35, 36, 37, 43	mpbir3an 1188	. . . . . . . . . . . . . . . 16 |- 0 e. ( -u pi (,) pi )
45	44	a1i 11	. . . . . . . . . . . . . . 15 |- ( T. -> 0 e. ( -u pi (,) pi ) )
46		eqid 2423	. . . . . . . . . . . . . . 15 |- ( ( -u pi (,) pi ) \ { 0 } ) = ( ( -u pi (,) pi ) \ { 0 } )
47		1ex 9640	. . . . . . . . . . . . . . . . . . 19 |- 1 e. _V
48		eqid 2423	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 ) = ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 )
49	47, 48	dmmpti 5723	. . . . . . . . . . . . . . . . . 18 |- dom ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 ) = ( ( -u pi (,) pi ) \ { 0 } )
50		reelprrecn 9633	. . . . . . . . . . . . . . . . . . . . . . 23 |- RR e. { RR , CC }
51	50	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( T. -> RR e. { RR , CC } )
52	12	sseli 3461	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. RR -> x e. CC )
53	52	adantl 468	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( T. /\ x e. RR ) -> x e. CC )
54		1red 9660	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( T. /\ x e. RR ) -> 1 e. RR )
55	51	dvmptid 22903	. . . . . . . . . . . . . . . . . . . . . 22 |- ( T. -> ( RR _D ( x e. RR |-> x ) ) = ( x e. RR |-> 1 ) )
56		eqid 2423	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
57	56	tgioo2 21813	. . . . . . . . . . . . . . . . . . . . . 22 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
58		sncldre 37240	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 0 e. RR -> { 0 } e. ( Clsd ` ( topGen ` ran (,) ) ) )
59	35, 58	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 |- { 0 } e. ( Clsd ` ( topGen ` ran (,) ) )
60		retopon 21776	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( topGen ` ran (,) ) e. (TopOn ` RR )
61	60	toponunii 19939	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- RR = U. ( topGen ` ran (,) )
62	61	difopn 20041	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( -u pi (,) pi ) e. ( topGen ` ran (,) ) /\ { 0 } e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( ( -u pi (,) pi ) \ { 0 } ) e. ( topGen ` ran (,) ) )
63	33, 59, 62	mp2an 677	. . . . . . . . . . . . . . . . . . . . . . 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 22909	. . . . . . . . . . . . . . . . . . . . 21 |- ( T. -> ( RR _D ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) ) = ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 ) )
66	65	trud 1447	. . . . . . . . . . . . . . . . . . . 20 |- ( RR _D ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) ) = ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 )
67	66	eqcomi 2436	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 ) = ( RR _D ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) )
68	67	dmeqi 5053	. . . . . . . . . . . . . . . . . 18 |- dom ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 ) = dom ( RR _D ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) )
69	49, 68	eqtr3i 2454	. . . . . . . . . . . . . . . . 17 |- ( ( -u pi (,) pi ) \ { 0 } ) = dom ( RR _D ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) )
70	69	eqimssi 3519	. . . . . . . . . . . . . . . 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 5889	. . . . . . . . . . . . . . . . . . 19 |- ( cos ` ( x / 2 ) ) e. _V
73		eqid 2423	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) = ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) )
74	72, 73	dmmpti 5723	. . . . . . . . . . . . . . . . . 18 |- dom ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) = ( ( -u pi (,) pi ) \ { 0 } )
75		2cnd 10684	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( T. /\ x e. RR ) -> 2 e. CC )
76	53	halfcld 10859	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( T. /\ x e. RR ) -> ( x / 2 ) e. CC )
77	76	sincld 14177	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( T. /\ x e. RR ) -> ( sin ` ( x / 2 ) ) e. CC )
78	75, 77	mulcld 9665	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( T. /\ x e. RR ) -> ( 2 x. ( sin ` ( x / 2 ) ) ) e. CC )
79	76	coscld 14178	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( T. /\ x e. RR ) -> ( cos ` ( x / 2 ) ) e. CC )
80		2cnd 10684	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. RR -> 2 e. CC )
81		2ne0 10704	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- 2 =/= 0
82	81	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. RR -> 2 =/= 0 )
83	52, 80, 82	divrec2d 10389	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x e. RR -> ( x / 2 ) = ( ( 1 / 2 ) x. x ) )
84	83	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x e. RR -> ( sin ` ( x / 2 ) ) = ( sin ` ( ( 1 / 2 ) x. x ) ) )
85	84	oveq2d 6319	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x e. RR -> ( 2 x. ( sin ` ( x / 2 ) ) ) = ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) )
86	85	mpteq2ia 4504	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( x e. RR |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) = ( x e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) )
87	86	oveq2i 6314	. . . . . . . . . . . . . . . . . . . . . . . 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 5171	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2436	. . . . . . . . . . . . . . . . . . . . . . . . . 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 6314	. . . . . . . . . . . . . . . . . . . . . . . . 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 2423	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) = ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) )
93		2cnd 10684	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x e. CC -> 2 e. CC )
94		halfcn 10831	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( 1 / 2 ) e. CC
95	94	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( x e. CC -> ( 1 / 2 ) e. CC )
96		id 23	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( x e. CC -> x e. CC )
97	95, 96	mulcld 9665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. CC -> ( ( 1 / 2 ) x. x ) e. CC )
98	97	sincld 14177	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x e. CC -> ( sin ` ( ( 1 / 2 ) x. x ) ) e. CC )
99	93, 98	mulcld 9665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x e. CC -> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) e. CC )
100	92, 99	fmpti 6058	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) : CC --> CC
101		eqid 2423	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- 2 e. CC
103	102, 94	mulcli 9650	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( 2 x. ( 1 / 2 ) ) e. CC
104	103	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( x e. CC -> ( 2 x. ( 1 / 2 ) ) e. CC )
105	97	coscld 14178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( x e. CC -> ( cos ` ( ( 1 / 2 ) x. x ) ) e. CC )
106	104, 105	mulcld 9665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( x e. CC -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) e. CC )
107	106	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( T. /\ x e. CC ) -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) e. CC )
108	101, 107	dmmptd 5724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( T. -> dom ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) = CC )
109	108	trud 1447	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- dom ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) ) = CC
110	12, 109	sseqtr4i 3498	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- RR C_ dom ( x e. CC |-> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) )
111		dvasinbx 37618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 677	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5053	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 3498	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- RR C_ dom ( CC _D ( x e. CC |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) )
115		dvcnre 37612	. . . . . . . . . . . . . . . . . . . . . . . . . 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 677	. . . . . . . . . . . . . . . . . . . . . . . . 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 5118	. . . . . . . . . . . . . . . . . . . . . . . . . 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 5171	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 10340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( 2 x. ( 1 / 2 ) ) = 1
121	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. RR -> ( 2 x. ( 1 / 2 ) ) = 1 )
122	83	eqcomd 2431	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( x e. RR -> ( ( 1 / 2 ) x. x ) = ( x / 2 ) )
123	122	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. RR -> ( cos ` ( ( 1 / 2 ) x. x ) ) = ( cos ` ( x / 2 ) ) )
124	121, 123	oveq12d 6321	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x e. RR -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) = ( 1 x. ( cos ` ( x / 2 ) ) ) )
125	52	halfcld 10859	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( x e. RR -> ( x / 2 ) e. CC )
126	125	coscld 14178	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. RR -> ( cos ` ( x / 2 ) ) e. CC )
127	126	mulid2d 9663	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x e. RR -> ( 1 x. ( cos ` ( x / 2 ) ) ) = ( cos ` ( x / 2 ) ) )
128	124, 127	eqtrd 2464	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( x e. RR -> ( ( 2 x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. x ) ) ) = ( cos ` ( x / 2 ) ) )
129	128	mpteq2ia 4504	. . . . . . . . . . . . . . . . . . . . . . . . . 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 2456	. . . . . . . . . . . . . . . . . . . . . . . . 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 2456	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( RR _D ( x e. RR |-> ( 2 x. ( sin ` ( ( 1 / 2 ) x. x ) ) ) ) ) = ( x e. RR |-> ( cos ` ( x / 2 ) ) )
132	87, 131	eqtri 2452	. . . . . . . . . . . . . . . . . . . . . . 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 22909	. . . . . . . . . . . . . . . . . . . . 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 1447	. . . . . . . . . . . . . . . . . . . 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 2436	. . . . . . . . . . . . . . . . . . 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 5053	. . . . . . . . . . . . . . . . . 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 2454	. . . . . . . . . . . . . . . . 17 |- ( ( -u pi (,) pi ) \ { 0 } ) = dom ( RR _D ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) )
139	138	eqimssi 3519	. . . . . . . . . . . . . . . 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 9671	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s e. ( -u pi (,) pi ) -> s e. CC )
142	141	ssriv 3469	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( -u pi (,) pi ) C_ CC
143	142	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( T. -> ( -u pi (,) pi ) C_ CC )
144		ssid 3484	. . . . . . . . . . . . . . . . . . . . . . 23 |- CC C_ CC
145	144	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( T. -> CC C_ CC )
146	143, 145	idcncfg 37575	. . . . . . . . . . . . . . . . . . . . 21 |- ( T. -> ( x e. ( -u pi (,) pi ) |-> x ) e. ( ( -u pi (,) pi ) -cn-> CC ) )
147	146	trud 1447	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( -u pi (,) pi ) |-> x ) e. ( ( -u pi (,) pi ) -cn-> CC )
148		cnlimc 22835	. . . . . . . . . . . . . . . . . . . . 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 212	. . . . . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . . . . 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 5879	. . . . . . . . . . . . . . . . . . . 20 |- ( y = 0 -> ( ( x e. ( -u pi (,) pi ) |-> x ) ` y ) = ( ( x e. ( -u pi (,) pi ) |-> x ) ` 0 ) )
153		oveq2 6311	. . . . . . . . . . . . . . . . . . . 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 2505	. . . . . . . . . . . . . . . . . . 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 3182	. . . . . . . . . . . . . . . . . 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 677	. . . . . . . . . . . . . . . . 17 |- ( ( x e. ( -u pi (,) pi ) |-> x ) ` 0 ) e. ( ( x e. ( -u pi (,) pi ) |-> x ) lim CC 0 )
157		id 23	. . . . . . . . . . . . . . . . . . 19 |- ( x = 0 -> x = 0 )
158		eqid 2423	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( -u pi (,) pi ) |-> x ) = ( x e. ( -u pi (,) pi ) |-> x )
159		c0ex 9639	. . . . . . . . . . . . . . . . . . 19 |- 0 e. _V
160	157, 158, 159	fvmpt 5962	. . . . . . . . . . . . . . . . . 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 11668	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. ( -u pi (,) pi ) -> x e. RR )
163	162	recnd 9671	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. ( -u pi (,) pi ) -> x e. CC )
164	158, 163	fmpti 6058	. . . . . . . . . . . . . . . . . . . . 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 22823	. . . . . . . . . . . . . . . . . . 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 1447	. . . . . . . . . . . . . . . . . 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 5171	. . . . . . . . . . . . . . . . . . . 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 6313	. . . . . . . . . . . . . . . . . 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 2452	. . . . . . . . . . . . . . . . 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 2523	. . . . . . . . . . . . . . . 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 2423	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. CC |-> 2 ) = ( x e. CC |-> 2 )
175	144	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 2 e. CC -> CC C_ CC )
176		2cnd 10684	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( 2 e. CC -> 2 e. CC )
177	175, 176, 175	constcncfg 37574	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 2 e. CC -> ( x e. CC |-> 2 ) e. ( CC -cn-> CC ) )
178	102, 177	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( T. -> ( x e. CC |-> 2 ) e. ( CC -cn-> CC ) )
179		2cnd 10684	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( T. /\ x e. ( -u pi (,) pi ) ) -> 2 e. CC )
180	174, 178, 143, 145, 179	cncfmptssg 37573	. . . . . . . . . . . . . . . . . . . . . 22 |- ( T. -> ( x e. ( -u pi (,) pi ) |-> 2 ) e. ( ( -u pi (,) pi ) -cn-> CC ) )
181		sincn 23391	. . . . . . . . . . . . . . . . . . . . . . . 24 |- sin e. ( CC -cn-> CC )
182	181	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( T. -> sin e. ( CC -cn-> CC ) )
183		eqid 2423	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x e. CC |-> ( x / 2 ) ) = ( x e. CC |-> ( x / 2 ) )
184	183	divccncf 21930	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 2 e. CC /\ 2 =/= 0 ) -> ( x e. CC |-> ( x / 2 ) ) e. ( CC -cn-> CC ) )
185	102, 81, 184	mp2an 677	. . . . . . . . . . . . . . . . . . . . . . . . 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 468	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( T. /\ x e. ( -u pi (,) pi ) ) -> x e. CC )
188	187	halfcld 10859	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( T. /\ x e. ( -u pi (,) pi ) ) -> ( x / 2 ) e. CC )
189	183, 186, 143, 145, 188	cncfmptssg 37573	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( T. -> ( x e. ( -u pi (,) pi ) |-> ( x / 2 ) ) e. ( ( -u pi (,) pi ) -cn-> CC ) )
190	182, 189	cncfmpt1f 21937	. . . . . . . . . . . . . . . . . . . . . 22 |- ( T. -> ( x e. ( -u pi (,) pi ) |-> ( sin ` ( x / 2 ) ) ) e. ( ( -u pi (,) pi ) -cn-> CC ) )
191	180, 190	mulcncf 22390	. . . . . . . . . . . . . . . . . . . . 21 |- ( T. -> ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) e. ( ( -u pi (,) pi ) -cn-> CC ) )
192	191	trud 1447	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. ( -u pi (,) pi ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) e. ( ( -u pi (,) pi ) -cn-> CC )
193		cnlimc 22835	. . . . . . . . . . . . . . . . . . . . 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 212	. . . . . . . . . . . . . . . . . . 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 464	. . . . . . . . . . . . . . . . . 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 5879	. . . . . . . . . . . . . . . . . . . 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 6311	. . . . . . . . . . . . . . . . . . . 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 2505	. . . . . . . . . . . . . . . . . . 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 3182	. . . . . . . . . . . . . . . . . 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 677	. . . . . . . . . . . . . . . . 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 6310	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x = 0 -> ( x / 2 ) = ( 0 / 2 ) )
203	102, 81	div0i 10343	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 0 / 2 ) = 0
204	202, 203	syl6eq 2480	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = 0 -> ( x / 2 ) = 0 )
205	204	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = 0 -> ( sin ` ( x / 2 ) ) = ( sin ` 0 ) )
206		sin0 14196	. . . . . . . . . . . . . . . . . . . . . 22 |- ( sin ` 0 ) = 0
207	205, 206	syl6eq 2480	. . . . . . . . . . . . . . . . . . . . 21 |- ( x = 0 -> ( sin ` ( x / 2 ) ) = 0 )
208	207	oveq2d 6319	. . . . . . . . . . . . . . . . . . . 20 |- ( x = 0 -> ( 2 x. ( sin ` ( x / 2 ) ) ) = ( 2 x. 0 ) )
209		2t0e0 10767	. . . . . . . . . . . . . . . . . . . 20 |- ( 2 x. 0 ) = 0
210	208, 209	syl6eq 2480	. . . . . . . . . . . . . . . . . . 19 |- ( x = 0 -> ( 2 x. ( sin ` ( x / 2 ) ) ) = 0 )
211		eqid 2423	. . . . . . . . . . . . . . . . . . 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 5962	. . . . . . . . . . . . . . . . . 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 10684	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. ( -u pi (,) pi ) -> 2 e. CC )
215	163	halfcld 10859	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x e. ( -u pi (,) pi ) -> ( x / 2 ) e. CC )
216	215	sincld 14177	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x e. ( -u pi (,) pi ) -> ( sin ` ( x / 2 ) ) e. CC )
217	214, 216	mulcld 9665	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x e. ( -u pi (,) pi ) -> ( 2 x. ( sin ` ( x / 2 ) ) ) e. CC )
218	211, 217	fmpti 6058	. . . . . . . . . . . . . . . . . . . . 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 22823	. . . . . . . . . . . . . . . . . . 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 1447	. . . . . . . . . . . . . . . . . 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 5171	. . . . . . . . . . . . . . . . . . . 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 6313	. . . . . . . . . . . . . . . . . 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 2452	. . . . . . . . . . . . . . . . 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 2523	. . . . . . . . . . . . . . . 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 2424	. . . . . . . . . . . . . . . . . . . . 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 6310	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x = y -> ( x / 2 ) = ( y / 2 ) )
230	229	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = y -> ( sin ` ( x / 2 ) ) = ( sin ` ( y / 2 ) ) )
231	230	oveq2d 6319	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = y -> ( 2 x. ( sin ` ( x / 2 ) ) ) = ( 2 x. ( sin ` ( y / 2 ) ) ) )
232	231	adantl 468	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( y e. ( ( -u pi (,) pi ) \ { 0 } ) /\ x = y ) -> ( 2 x. ( sin ` ( x / 2 ) ) ) = ( 2 x. ( sin ` ( y / 2 ) ) ) )
233		id 23	. . . . . . . . . . . . . . . . . . . . 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 3461	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> y e. RR )
236	235	rehalfcld 10861	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( y / 2 ) e. RR )
237	236	resincld 14190	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( sin ` ( y / 2 ) ) e. RR )
238	234, 237	remulcld 9673	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( y / 2 ) ) ) e. RR )
239	228, 232, 233, 238	fvmptd 5968	. . . . . . . . . . . . . . . . . . . 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 10684	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> 2 e. CC )
241	237	recnd 9671	. . . . . . . . . . . . . . . . . . . . 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 11722	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( -u pi (,) pi ) C_ ( -u pi [,] pi )
244		eldifi 3588	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> y e. ( -u pi (,) pi ) )
245	243, 244	sseldi 3463	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> y e. ( -u pi [,] pi ) )
246		eldifsni 4124	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> y =/= 0 )
247		fourierdlem44 37841	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( y e. ( -u pi [,] pi ) /\ y =/= 0 ) -> ( sin ` ( y / 2 ) ) =/= 0 )
248	245, 246, 247	syl2anc 666	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( sin ` ( y / 2 ) ) =/= 0 )
249	240, 241, 242, 248	mulne0d 10266	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( y / 2 ) ) ) =/= 0 )
250	239, 249	eqnetrd 2718	. . . . . . . . . . . . . . . . . . 19 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) =/= 0 )
251	250	neneqd 2626	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> -. ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) = 0 )
252	251	nrex 2881	. . . . . . . . . . . . . . . . 17 |- -. E. y e. ( ( -u pi (,) pi ) \ { 0 } ) ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) ` y ) = 0
253	25	fnmpt 5720	. . . . . . . . . . . . . . . . . . 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 2789	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 2 x. ( sin ` ( x / 2 ) ) ) ) Fn ( ( -u pi (,) pi ) \ { 0 } )
255		ssid 3484	. . . . . . . . . . . . . . . . . 18 |- ( ( -u pi (,) pi ) \ { 0 } ) C_ ( ( -u pi (,) pi ) \ { 0 } )
256		fvelimab 5935	. . . . . . . . . . . . . . . . . 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 677	. . . . . . . . . . . . . . . . 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 301	. . . . . . . . . . . . . . . 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 2424	. . . . . . . . . . . . . . . . . . . . . 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 5883	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = y -> ( cos ` ( x / 2 ) ) = ( cos ` ( y / 2 ) ) )
262	261	adantl 468	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( y e. ( ( -u pi (,) pi ) \ { 0 } ) /\ x = y ) -> ( cos ` ( x / 2 ) ) = ( cos ` ( y / 2 ) ) )
263	235	recnd 9671	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> y e. CC )
264	263	halfcld 10859	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( y / 2 ) e. CC )
265	264	coscld 14178	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( cos ` ( y / 2 ) ) e. CC )
266	260, 262, 233, 265	fvmptd 5968	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) ` y ) = ( cos ` ( y / 2 ) ) )
267	236	rered 13281	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( Re ` ( y / 2 ) ) = ( y / 2 ) )
268		halfpire 23411	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( pi / 2 ) e. RR
269	268	renegcli 9937	. . . . . . . . . . . . . . . . . . . . . . . . . 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 9692	. . . . . . . . . . . . . . . . . . . . . . . 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 9692	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( pi / 2 ) e. RR* )
274		picn 23406	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- pi e. CC
275		divneg 10304	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( pi e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> -u ( pi / 2 ) = ( -u pi / 2 ) )
276	274, 102, 81, 275	mp3an 1361	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- -u ( pi / 2 ) = ( -u pi / 2 )
277	39	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> -u pi e. RR )
278		2rp 11309	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 37429	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( -u pi e. RR* /\ pi e. RR* /\ y e. ( -u pi (,) pi ) ) -> -u pi < y )
283	280, 281, 244, 282	syl3anc 1265	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> -u pi < y )
284	277, 235, 279, 283	ltdiv1dd 11397	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( -u pi / 2 ) < ( y / 2 ) )
285	276, 284	syl5eqbr 4455	. . . . . . . . . . . . . . . . . . . . . . . 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 37447	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( -u pi e. RR* /\ pi e. RR* /\ y e. ( -u pi (,) pi ) ) -> y < pi )
288	280, 281, 244, 287	syl3anc 1265	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> y < pi )
289	235, 286, 279, 288	ltdiv1dd 11397	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( y / 2 ) < ( pi / 2 ) )
290	271, 273, 236, 285, 289	eliood 37432	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( y / 2 ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) )
291	267, 290	eqeltrd 2511	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( Re ` ( y / 2 ) ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) )
292		cosne0 23471	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( y / 2 ) e. CC /\ ( Re ` ( y / 2 ) ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) ) -> ( cos ` ( y / 2 ) ) =/= 0 )
293	264, 291, 292	syl2anc 666	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( cos ` ( y / 2 ) ) =/= 0 )
294	266, 293	eqnetrd 2718	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) ` y ) =/= 0 )
295	294	neneqd 2626	. . . . . . . . . . . . . . . . . . 19 |- ( y e. ( ( -u pi (,) pi ) \ { 0 } ) -> -. ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) ` y ) = 0 )
296	295	nrex 2881	. . . . . . . . . . . . . . . . . 18 |- -. E. y e. ( ( -u pi (,) pi ) \ { 0 } ) ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) ` y ) = 0
297	72, 73	fnmpti 5722	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) Fn ( ( -u pi (,) pi ) \ { 0 } )
298		fvelimab 5935	. . . . . . . . . . . . . . . . . . 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 677	. . . . . . . . . . . . . . . . . 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 301	. . . . . . . . . . . . . . . . 17 |- -. 0 e. ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( x / 2 ) ) ) " ( ( -u pi (,) pi ) \ { 0 } ) )
301	135	imaeq1i 5182	. . . . . . . . . . . . . . . . . 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 2501	. . . . . . . . . . . . . . . . 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 301	. . . . . . . . . . . . . . . 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 2423	. . . . . . . . . . . . . . . . 17 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( s / 2 ) ) ) = ( s e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( s / 2 ) ) )
306		eqid 2423	. . . . . . . . . . . . . . . . 17 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 1 / ( cos ` ( s / 2 ) ) ) ) = ( s e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 1 / ( cos ` ( s / 2 ) ) ) )
307	19	sseli 3461	. . . . . . . . . . . . . . . . . . . . . 22 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> s e. RR )
308	307	recnd 9671	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> s e. CC )
309	308	halfcld 10859	. . . . . . . . . . . . . . . . . . . 20 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( s / 2 ) e. CC )
310	309	coscld 14178	. . . . . . . . . . . . . . . . . . 19 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( cos ` ( s / 2 ) ) e. CC )
311	307	rehalfcld 10861	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( s / 2 ) e. RR )
312	311	rered 13281	. . . . . . . . . . . . . . . . . . . . . . 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 9692	. . . . . . . . . . . . . . . . . . . . . . . 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 9692	. . . . . . . . . . . . . . . . . . . . . . . 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 10048	. . . . . . . . . . . . . . . . . . . . . . . . . 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 3588	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> s e. ( -u pi (,) pi ) )
323		ioogtlb 37429	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( -u pi e. RR* /\ pi e. RR* /\ s e. ( -u pi (,) pi ) ) -> -u pi < s )
324	320, 321, 322, 323	syl3anc 1265	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> -u pi < s )
325	318, 307, 319, 324	ltdiv1dd 11397	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( -u pi / 2 ) < ( s / 2 ) )
326	276, 325	syl5eqbr 4455	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> -u ( pi / 2 ) < ( s / 2 ) )
327		iooltub 37447	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( -u pi e. RR* /\ pi e. RR* /\ s e. ( -u pi (,) pi ) ) -> s < pi )
328	320, 321, 322, 327	syl3anc 1265	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> s < pi )
329	307, 317, 319, 328	ltdiv1dd 11397	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( s / 2 ) < ( pi / 2 ) )
330	314, 316, 311, 326, 329	eliood 37432	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( s / 2 ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) )
331	312, 330	eqeltrd 2511	. . . . . . . . . . . . . . . . . . . . . 22 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( Re ` ( s / 2 ) ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) )
332		cosne0 23471	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( s / 2 ) e. CC /\ ( Re ` ( s / 2 ) ) e. ( -u ( pi / 2 ) (,) ( pi / 2 ) ) ) -> ( cos ` ( s / 2 ) ) =/= 0 )
333	309, 331, 332	syl2anc 666	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( cos ` ( s / 2 ) ) =/= 0 )
334	333	neneqd 2626	. . . . . . . . . . . . . . . . . . . 20 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> -. ( cos ` ( s / 2 ) ) = 0 )
335	311	recoscld 14191	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( cos ` ( s / 2 ) ) e. RR )
336		elsncg 4020	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( cos ` ( s / 2 ) ) e. RR -> ( ( cos ` ( s / 2 ) ) e. { 0 } <-> ( cos ` ( s / 2 ) ) = 0 ) )
337	335, 336	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( ( cos ` ( s / 2 ) ) e. { 0 } <-> ( cos ` ( s / 2 ) ) = 0 ) )
338	334, 337	mtbird 303	. . . . . . . . . . . . . . . . . . 19 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> -. ( cos ` ( s / 2 ) ) e. { 0 } )
339	310, 338	eldifd 3448	. . . . . . . . . . . . . . . . . 18 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( cos ` ( s / 2 ) ) e. ( CC \ { 0 } ) )
340	339	adantl 468	. . . . . . . . . . . . . . . . 17 |- ( ( T. /\ s e. ( ( -u pi (,) pi ) \ { 0 } ) ) -> ( cos ` ( s / 2 ) ) e. ( CC \ { 0 } ) )
341	309	ad2antrl 733	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ ( s e. ( ( -u pi (,) pi ) \ { 0 } ) /\ ( s / 2 ) =/= 0 ) ) -> ( s / 2 ) e. CC )
342		cosf 14172	. . . . . . . . . . . . . . . . . . . 20 |- cos : CC --> CC
343	342	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( T. -> cos : CC --> CC )
344	343	ffvelrnda 6035	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ x e. CC ) -> ( cos ` x ) e. CC )
345		eqid 2423	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. CC |-> ( s / 2 ) ) = ( s e. CC |-> ( s / 2 ) )
346	345	divccncf 21930	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( 2 e. CC /\ 2 =/= 0 ) -> ( s e. CC |-> ( s / 2 ) ) e. ( CC -cn-> CC ) )
347	102, 81, 346	mp2an 677	. . . . . . . . . . . . . . . . . . . . . 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 468	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( T. /\ s e. ( -u pi (,) pi ) ) -> s e. CC )
350	349	halfcld 10859	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( T. /\ s e. ( -u pi (,) pi ) ) -> ( s / 2 ) e. CC )
351	345, 348, 143, 145, 350	cncfmptssg 37573	. . . . . . . . . . . . . . . . . . . 20 |- ( T. -> ( s e. ( -u pi (,) pi ) |-> ( s / 2 ) ) e. ( ( -u pi (,) pi ) -cn-> CC ) )
352		oveq1 6310	. . . . . . . . . . . . . . . . . . . . 21 |- ( s = 0 -> ( s / 2 ) = ( 0 / 2 ) )
353	352, 203	syl6eq 2480	. . . . . . . . . . . . . . . . . . . 20 |- ( s = 0 -> ( s / 2 ) = 0 )
354	351, 45, 353	cnmptlimc 22837	. . . . . . . . . . . . . . . . . . 19 |- ( T. -> 0 e. ( ( s e. ( -u pi (,) pi ) |-> ( s / 2 ) ) lim CC 0 ) )
355		eqid 2423	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s e. ( -u pi (,) pi ) |-> ( s / 2 ) ) = ( s e. ( -u pi (,) pi ) |-> ( s / 2 ) )
356	141	halfcld 10859	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( s e. ( -u pi (,) pi ) -> ( s / 2 ) e. CC )
357	355, 356	fmpti 6058	. . . . . . . . . . . . . . . . . . . . . . 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 22823	. . . . . . . . . . . . . . . . . . . . 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 1447	. . . . . . . . . . . . . . . . . . . 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 5171	. . . . . . . . . . . . . . . . . . . . . 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 6313	. . . . . . . . . . . . . . . . . . . 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 2452	. . . . . . . . . . . . . . . . . . 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 2521	. . . . . . . . . . . . . . . . . 18 |- ( T. -> 0 e. ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( s / 2 ) ) lim CC 0 ) )
366		ffn 5744	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( cos : CC --> CC -> cos Fn CC )
367	342, 366	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22 |- cos Fn CC
368		dffn5 5924	. . . . . . . . . . . . . . . . . . . . . 22 |- ( cos Fn CC <-> cos = ( x e. CC |-> ( cos ` x ) ) )
369	367, 368	mpbi 212	. . . . . . . . . . . . . . . . . . . . 21 |- cos = ( x e. CC |-> ( cos ` x ) )
370		coscn 23392	. . . . . . . . . . . . . . . . . . . . 21 |- cos e. ( CC -cn-> CC )
371	369, 370	eqeltrri 2508	. . . . . . . . . . . . . . . . . . . 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 9638	. . . . . . . . . . . . . . . . . . 19 |- ( T. -> 0 e. CC )
374		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20 |- ( x = 0 -> ( cos ` x ) = ( cos ` 0 ) )
375		cos0 14197	. . . . . . . . . . . . . . . . . . . 20 |- ( cos ` 0 ) = 1
376	374, 375	syl6eq 2480	. . . . . . . . . . . . . . . . . . 19 |- ( x = 0 -> ( cos ` x ) = 1 )
377	372, 373, 376	cnmptlimc 22837	. . . . . . . . . . . . . . . . . 18 |- ( T. -> 1 e. ( ( x e. CC |-> ( cos ` x ) ) lim CC 0 ) )
378		fveq2 5879	. . . . . . . . . . . . . . . . . 18 |- ( x = ( s / 2 ) -> ( cos ` x ) = ( cos ` ( s / 2 ) ) )
379		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20 |- ( ( s / 2 ) = 0 -> ( cos ` ( s / 2 ) ) = ( cos ` 0 ) )
380	379, 375	syl6eq 2480	. . . . . . . . . . . . . . . . . . 19 |- ( ( s / 2 ) = 0 -> ( cos ` ( s / 2 ) ) = 1 )
381	380	ad2antll 734	. . . . . . . . . . . . . . . . . 18 |- ( ( T. /\ ( s e. ( ( -u pi (,) pi ) \ { 0 } ) /\ ( s / 2 ) = 0 ) ) -> ( cos ` ( s / 2 ) ) = 1 )
382	341, 344, 365, 377, 378, 381	limcco 22840	. . . . . . . . . . . . . . . . 17 |- ( T. -> 1 e. ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( cos ` ( s / 2 ) ) ) lim CC 0 ) )
383		ax-1ne0 9610	. . . . . . . . . . . . . . . . . 18 |- 1 =/= 0
384	383	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( T. -> 1 =/= 0 )
385	305, 306, 340, 382, 384	reclimc 37560	. . . . . . . . . . . . . . . 16 |- ( T. -> ( 1 / 1 ) e. ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( 1 / ( cos ` ( s / 2 ) ) ) ) lim CC 0 ) )
386		1div1e1 10302	. . . . . . . . . . . . . . . 16 |- ( 1 / 1 ) = 1
387	66	fveq1i 5880	. . . . . . . . . . . . . . . . . . . 20 |- ( ( RR _D ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) ) ` s ) = ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 ) ` s )
388		eqidd 2424	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 ) = ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 ) )
389		eqidd 2424	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) /\ x = s ) -> 1 = 1 )
390		id 23	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> s e. ( ( -u pi (,) pi ) \ { 0 } ) )
391		1red 9660	. . . . . . . . . . . . . . . . . . . . 21 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> 1 e. RR )
392	388, 389, 390, 391	fvmptd 5968	. . . . . . . . . . . . . . . . . . . 20 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> 1 ) ` s ) = 1 )
393	387, 392	syl5req 2477	. . . . . . . . . . . . . . . . . . 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 6310	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( x = s -> ( x / 2 ) = ( s / 2 ) )
396	395	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . 22 |- ( x = s -> ( cos ` ( x / 2 ) ) = ( cos ` ( s / 2 ) ) )
397	396	adantl 468	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) /\ x = s ) -> ( cos ` ( x / 2 ) ) = ( cos ` ( s / 2 ) ) )
398	394, 397, 390, 335	fvmptd 5968	. . . . . . . . . . . . . . . . . . . 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 2431	. . . . . . . . . . . . . . . . . . 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 6321	. . . . . . . . . . . . . . . . . 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 4504	. . . . . . . . . . . . . . . . 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 6313	. . . . . . . . . . . . . . . 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 2527	. . . . . . . . . . . . . . 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 22960	. . . . . . . . . . . . . 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 1447	. . . . . . . . . . . . 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 2424	. . . . . . . . . . . . . . . . 17 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) = ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) )
407		simpr 463	. . . . . . . . . . . . . . . . 17 |- ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) /\ x = s ) -> x = s )
408	406, 407, 390, 307	fvmptd 5968	. . . . . . . . . . . . . . . 16 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( ( x e. ( ( -u pi (,) pi ) \ { 0 } ) |-> x ) ` s ) = s )
409		eqidd 2424	. . . . . . . . . . . . . . . . 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 6318	. . . . . . . . . . . . . . . . . . 19 |- ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) /\ x = s ) -> ( x / 2 ) = ( s / 2 ) )
411	410	fveq2d 5883	. . . . . . . . . . . . . . . . . 18 |- ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) /\ x = s ) -> ( sin ` ( x / 2 ) ) = ( sin ` ( s / 2 ) ) )
412	411	oveq2d 6319	. . . . . . . . . . . . . . . . 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 14190	. . . . . . . . . . . . . . . . . 18 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( sin ` ( s / 2 ) ) e. RR )
415	413, 414	remulcld 9673	. . . . . . . . . . . . . . . . 17 |- ( s e. ( ( -u pi (,) pi ) \ { 0 } ) -> ( 2 x. ( sin ` ( s / 2 ) ) ) e. RR )
416	409, 412, 390, 415	fvmptd 5968	. . . . . . . . . . . . . . . 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 6321	. . . . . . . . . . . . . . 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 4504	. . . . . . . . . . . . . 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 6313	. . . . . . . . . . . . 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 2509	. . . . . . . . . . . 12 |- 1 e. ( ( s e. ( ( -u pi (,) pi ) \ { 0 } ) |-> ( s / ( 2 x. ( sin ` ( s / 2 ) ) ) ) ) lim CC 0 )
421	10	oveq1i 6313	. . . . . . . . . . . . . 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 5736	. . . . . . . . . . . . . . . . . . 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 212	. . . . . . . . . . . . . . . . . 18 |- ( s e. ( -u pi [,] pi ) |-> if ( s = 0 , 1 , ( s