Theorem dirkercncflem2

Description: Lemma used to prove that the Dirichlet kernel is continuous at Y points that are multiples of ( 2 x. _pi ) . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	dirkercncflem2.d	|- D = ( n e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
	dirkercncflem2.f	|- F = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) )
	dirkercncflem2.g	|- G = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) )
	dirkercncflem2.yne0	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( sin ` ( y / 2 ) ) =/= 0 )
	dirkercncflem2.h	|- H = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
	dirkercncflem2.i	|- I = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( _pi x. ( cos ` ( y / 2 ) ) ) )
	dirkercncflem2.l	|- L = ( w e. ( A (,) B ) |-> ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) / ( _pi x. ( cos ` ( w / 2 ) ) ) ) )
	dirkercncflem2.n	|- ( ph -> N e. NN )
	dirkercncflem2.y	|- ( ph -> Y e. ( A (,) B ) )
	dirkercncflem2.ymod	|- ( ph -> ( Y mod ( 2 x. _pi ) ) = 0 )
	dirkercncflem2.11	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( cos ` ( y / 2 ) ) =/= 0 )
Assertion	dirkercncflem2	|- ( ph -> ( ( D ` N ) ` Y ) e. ( ( ( D ` N ) |` ( ( A (,) B ) \ { Y } ) ) limCC Y ) )

Proof

Step	Hyp	Ref	Expression
1		dirkercncflem2.d	|- D = ( n e. NN |-> ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. n ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( n + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
2		dirkercncflem2.f	|- F = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) )
3		dirkercncflem2.g	|- G = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) )
4		dirkercncflem2.yne0	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( sin ` ( y / 2 ) ) =/= 0 )
5		dirkercncflem2.h	|- H = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
6		dirkercncflem2.i	|- I = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( _pi x. ( cos ` ( y / 2 ) ) ) )
7		dirkercncflem2.l	|- L = ( w e. ( A (,) B ) |-> ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) / ( _pi x. ( cos ` ( w / 2 ) ) ) ) )
8		dirkercncflem2.n	|- ( ph -> N e. NN )
9		dirkercncflem2.y	|- ( ph -> Y e. ( A (,) B ) )
10		dirkercncflem2.ymod	|- ( ph -> ( Y mod ( 2 x. _pi ) ) = 0 )
11		dirkercncflem2.11	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( cos ` ( y / 2 ) ) =/= 0 )
12		difss	|- ( ( A (,) B ) \ { Y } ) C_ ( A (,) B )
13		ioossre	|- ( A (,) B ) C_ RR
14	12 13	sstri	|- ( ( A (,) B ) \ { Y } ) C_ RR
15	14	a1i	|- ( ph -> ( ( A (,) B ) \ { Y } ) C_ RR )
16	8	adantr	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> N e. NN )
17	16	nnred	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> N e. RR )
18		halfre	|- ( 1 / 2 ) e. RR
19	18	a1i	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( 1 / 2 ) e. RR )
20	17 19	readdcld	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( N + ( 1 / 2 ) ) e. RR )
21	15	sselda	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> y e. RR )
22	20 21	remulcld	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. y ) e. RR )
23	22	resincld	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) e. RR )
24	23 2	fmptd	|- ( ph -> F : ( ( A (,) B ) \ { Y } ) --> RR )
25		2pire	|- ( 2 x. _pi ) e. RR
26	25	a1i	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( 2 x. _pi ) e. RR )
27	21	rehalfcld	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( y / 2 ) e. RR )
28	27	resincld	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( sin ` ( y / 2 ) ) e. RR )
29	26 28	remulcld	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) e. RR )
30	29 3	fmptd	|- ( ph -> G : ( ( A (,) B ) \ { Y } ) --> RR )
31		iooretop	|- ( A (,) B ) e. ( topGen ` ran (,) )
32	31	a1i	|- ( ph -> ( A (,) B ) e. ( topGen ` ran (,) ) )
33		eqid	|- ( ( A (,) B ) \ { Y } ) = ( ( A (,) B ) \ { Y } )
34	2	a1i	|- ( ph -> F = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
35	34	oveq2d	|- ( ph -> ( RR _D F ) = ( RR _D ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
36		resmpt	|- ( ( ( A (,) B ) \ { Y } ) C_ RR -> ( ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` ( ( A (,) B ) \ { Y } ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
37	14 36	ax-mp	|- ( ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` ( ( A (,) B ) \ { Y } ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) )
38	37	eqcomi	|- ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) = ( ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` ( ( A (,) B ) \ { Y } ) )
39	38	a1i	|- ( ph -> ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) = ( ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` ( ( A (,) B ) \ { Y } ) ) )
40	39	oveq2d	|- ( ph -> ( RR _D ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = ( RR _D ( ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` ( ( A (,) B ) \ { Y } ) ) ) )
41		ax-resscn	|- RR C_ CC
42	41	a1i	|- ( ph -> RR C_ CC )
43	8	nncnd	|- ( ph -> N e. CC )
44		halfcn	|- ( 1 / 2 ) e. CC
45	44	a1i	|- ( ph -> ( 1 / 2 ) e. CC )
46	43 45	addcld	|- ( ph -> ( N + ( 1 / 2 ) ) e. CC )
47	46	adantr	|- ( ( ph /\ y e. RR ) -> ( N + ( 1 / 2 ) ) e. CC )
48	42	sselda	|- ( ( ph /\ y e. RR ) -> y e. CC )
49	47 48	mulcld	|- ( ( ph /\ y e. RR ) -> ( ( N + ( 1 / 2 ) ) x. y ) e. CC )
50	49	sincld	|- ( ( ph /\ y e. RR ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) e. CC )
51		eqid	|- ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) = ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) )
52	50 51	fmptd	|- ( ph -> ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) : RR --> CC )
53		ssid	|- RR C_ RR
54	53 14	pm3.2i	|- ( RR C_ RR /\ ( ( A (,) B ) \ { Y } ) C_ RR )
55	54	a1i	|- ( ph -> ( RR C_ RR /\ ( ( A (,) B ) \ { Y } ) C_ RR ) )
56		eqid	|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
57		tgioo4	|- ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
58	56 57	dvres	|- ( ( ( RR C_ CC /\ ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) : RR --> CC ) /\ ( RR C_ RR /\ ( ( A (,) B ) \ { Y } ) C_ RR ) ) -> ( RR _D ( ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` ( ( A (,) B ) \ { Y } ) ) ) = ( ( RR _D ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) \ { Y } ) ) ) )
59	42 52 55 58	syl21anc	|- ( ph -> ( RR _D ( ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` ( ( A (,) B ) \ { Y } ) ) ) = ( ( RR _D ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) \ { Y } ) ) ) )
60		retop	|- ( topGen ` ran (,) ) e. Top
61		rehaus	|- ( topGen ` ran (,) ) e. Haus
62	9	elioored	|- ( ph -> Y e. RR )
63		uniretop	|- RR = U. ( topGen ` ran (,) )
64	63	sncld	|- ( ( ( topGen ` ran (,) ) e. Haus /\ Y e. RR ) -> { Y } e. ( Clsd ` ( topGen ` ran (,) ) ) )
65	61 62 64	sylancr	|- ( ph -> { Y } e. ( Clsd ` ( topGen ` ran (,) ) ) )
66	63	difopn	|- ( ( ( A (,) B ) e. ( topGen ` ran (,) ) /\ { Y } e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( ( A (,) B ) \ { Y } ) e. ( topGen ` ran (,) ) )
67	31 65 66	sylancr	|- ( ph -> ( ( A (,) B ) \ { Y } ) e. ( topGen ` ran (,) ) )
68		isopn3i	|- ( ( ( topGen ` ran (,) ) e. Top /\ ( ( A (,) B ) \ { Y } ) e. ( topGen ` ran (,) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) \ { Y } ) ) = ( ( A (,) B ) \ { Y } ) )
69	60 67 68	sylancr	|- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) \ { Y } ) ) = ( ( A (,) B ) \ { Y } ) )
70	69	reseq2d	|- ( ph -> ( ( RR _D ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) \ { Y } ) ) ) = ( ( RR _D ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) |` ( ( A (,) B ) \ { Y } ) ) )
71		reelprrecn	|- RR e. { RR , CC }
72	71	a1i	|- ( ph -> RR e. { RR , CC } )
73	46	adantr	|- ( ( ph /\ y e. CC ) -> ( N + ( 1 / 2 ) ) e. CC )
74		simpr	|- ( ( ph /\ y e. CC ) -> y e. CC )
75	73 74	mulcld	|- ( ( ph /\ y e. CC ) -> ( ( N + ( 1 / 2 ) ) x. y ) e. CC )
76	75	sincld	|- ( ( ph /\ y e. CC ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) e. CC )
77		eqid	|- ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) = ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) )
78	76 77	fmptd	|- ( ph -> ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) : CC --> CC )
79		ssid	|- CC C_ CC
80	79	a1i	|- ( ph -> CC C_ CC )
81		dvsinax	|- ( ( N + ( 1 / 2 ) ) e. CC -> ( CC _D ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = ( y e. CC |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
82	46 81	syl	|- ( ph -> ( CC _D ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = ( y e. CC |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
83	82	dmeqd	|- ( ph -> dom ( CC _D ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = dom ( y e. CC |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
84		eqid	|- ( y e. CC |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = ( y e. CC |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
85	75	coscld	|- ( ( ph /\ y e. CC ) -> ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) e. CC )
86	73 85	mulcld	|- ( ( ph /\ y e. CC ) -> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) e. CC )
87	84 86	dmmptd	|- ( ph -> dom ( y e. CC |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = CC )
88	83 87	eqtrd	|- ( ph -> dom ( CC _D ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = CC )
89	41 88	sseqtrrid	|- ( ph -> RR C_ dom ( CC _D ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
90		dvres3	|- ( ( ( RR e. { RR , CC } /\ ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) : CC --> CC ) /\ ( CC C_ CC /\ RR C_ dom ( CC _D ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) ) ) -> ( RR _D ( ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` RR ) ) = ( ( CC _D ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) |` RR ) )
91	72 78 80 89 90	syl22anc	|- ( ph -> ( RR _D ( ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` RR ) ) = ( ( CC _D ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) |` RR ) )
92		resmpt	|- ( RR C_ CC -> ( ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` RR ) = ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
93	41 92	mp1i	|- ( ph -> ( ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` RR ) = ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
94	93	oveq2d	|- ( ph -> ( RR _D ( ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` RR ) ) = ( RR _D ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
95	82	reseq1d	|- ( ph -> ( ( CC _D ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) |` RR ) = ( ( y e. CC |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) |` RR ) )
96		resmpt	|- ( RR C_ CC -> ( ( y e. CC |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) |` RR ) = ( y e. RR |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
97	41 96	ax-mp	|- ( ( y e. CC |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) |` RR ) = ( y e. RR |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
98	95 97	eqtrdi	|- ( ph -> ( ( CC _D ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) |` RR ) = ( y e. RR |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
99	91 94 98	3eqtr3d	|- ( ph -> ( RR _D ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = ( y e. RR |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
100	99	reseq1d	|- ( ph -> ( ( RR _D ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) |` ( ( A (,) B ) \ { Y } ) ) = ( ( y e. RR |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) |` ( ( A (,) B ) \ { Y } ) ) )
101		resmpt	|- ( ( ( A (,) B ) \ { Y } ) C_ RR -> ( ( y e. RR |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) |` ( ( A (,) B ) \ { Y } ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
102	14 101	mp1i	|- ( ph -> ( ( y e. RR |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) |` ( ( A (,) B ) \ { Y } ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
103	70 100 102	3eqtrd	|- ( ph -> ( ( RR _D ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) \ { Y } ) ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
104	40 59 103	3eqtrd	|- ( ph -> ( RR _D ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
105	5	a1i	|- ( ph -> H = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
106	105	eqcomd	|- ( ph -> ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = H )
107	35 104 106	3eqtrd	|- ( ph -> ( RR _D F ) = H )
108	107	dmeqd	|- ( ph -> dom ( RR _D F ) = dom H )
109	21	recnd	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> y e. CC )
110	109 86	syldan	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) e. CC )
111	5 110	dmmptd	|- ( ph -> dom H = ( ( A (,) B ) \ { Y } ) )
112	108 111	eqtr2d	|- ( ph -> ( ( A (,) B ) \ { Y } ) = dom ( RR _D F ) )
113		eqimss	|- ( ( ( A (,) B ) \ { Y } ) = dom ( RR _D F ) -> ( ( A (,) B ) \ { Y } ) C_ dom ( RR _D F ) )
114	112 113	syl	|- ( ph -> ( ( A (,) B ) \ { Y } ) C_ dom ( RR _D F ) )
115	6	a1i	|- ( ph -> I = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( _pi x. ( cos ` ( y / 2 ) ) ) ) )
116		resmpt	|- ( ( ( A (,) B ) \ { Y } ) C_ RR -> ( ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) |` ( ( A (,) B ) \ { Y } ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) )
117	14 116	ax-mp	|- ( ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) |` ( ( A (,) B ) \ { Y } ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) )
118	117	eqcomi	|- ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) = ( ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) |` ( ( A (,) B ) \ { Y } ) )
119	118	oveq2i	|- ( RR _D ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) = ( RR _D ( ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) |` ( ( A (,) B ) \ { Y } ) ) )
120	119	a1i	|- ( ph -> ( RR _D ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) = ( RR _D ( ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) |` ( ( A (,) B ) \ { Y } ) ) ) )
121		2picn	|- ( 2 x. _pi ) e. CC
122	121	a1i	|- ( ( ph /\ y e. RR ) -> ( 2 x. _pi ) e. CC )
123	48	halfcld	|- ( ( ph /\ y e. RR ) -> ( y / 2 ) e. CC )
124	123	sincld	|- ( ( ph /\ y e. RR ) -> ( sin ` ( y / 2 ) ) e. CC )
125	122 124	mulcld	|- ( ( ph /\ y e. RR ) -> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) e. CC )
126		eqid	|- ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) = ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) )
127	125 126	fmptd	|- ( ph -> ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) : RR --> CC )
128	56 57	dvres	|- ( ( ( RR C_ CC /\ ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) : RR --> CC ) /\ ( RR C_ RR /\ ( ( A (,) B ) \ { Y } ) C_ RR ) ) -> ( RR _D ( ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) |` ( ( A (,) B ) \ { Y } ) ) ) = ( ( RR _D ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) \ { Y } ) ) ) )
129	42 127 55 128	syl21anc	|- ( ph -> ( RR _D ( ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) |` ( ( A (,) B ) \ { Y } ) ) ) = ( ( RR _D ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) \ { Y } ) ) ) )
130	69	reseq2d	|- ( ph -> ( ( RR _D ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) \ { Y } ) ) ) = ( ( RR _D ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) |` ( ( A (,) B ) \ { Y } ) ) )
131	41	sseli	|- ( y e. RR -> y e. CC )
132		1cnd	|- ( y e. CC -> 1 e. CC )
133		2cnd	|- ( y e. CC -> 2 e. CC )
134		id	|- ( y e. CC -> y e. CC )
135		2ne0	|- 2 =/= 0
136	135	a1i	|- ( y e. CC -> 2 =/= 0 )
137	132 133 134 136	div13d	|- ( y e. CC -> ( ( 1 / 2 ) x. y ) = ( ( y / 2 ) x. 1 ) )
138		halfcl	|- ( y e. CC -> ( y / 2 ) e. CC )
139	138	mulridd	|- ( y e. CC -> ( ( y / 2 ) x. 1 ) = ( y / 2 ) )
140	137 139	eqtrd	|- ( y e. CC -> ( ( 1 / 2 ) x. y ) = ( y / 2 ) )
141	140	fveq2d	|- ( y e. CC -> ( sin ` ( ( 1 / 2 ) x. y ) ) = ( sin ` ( y / 2 ) ) )
142	141	oveq2d	|- ( y e. CC -> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) = ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) )
143	142	eqcomd	|- ( y e. CC -> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) = ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) )
144	131 143	syl	|- ( y e. RR -> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) = ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) )
145	144	adantl	|- ( ( ph /\ y e. RR ) -> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) = ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) )
146	145	mpteq2dva	|- ( ph -> ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) = ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) )
147	146	oveq2d	|- ( ph -> ( RR _D ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) = ( RR _D ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) )
148	121	a1i	|- ( ( ph /\ y e. CC ) -> ( 2 x. _pi ) e. CC )
149	44	a1i	|- ( ( ph /\ y e. CC ) -> ( 1 / 2 ) e. CC )
150	149 74	mulcld	|- ( ( ph /\ y e. CC ) -> ( ( 1 / 2 ) x. y ) e. CC )
151	150	sincld	|- ( ( ph /\ y e. CC ) -> ( sin ` ( ( 1 / 2 ) x. y ) ) e. CC )
152	148 151	mulcld	|- ( ( ph /\ y e. CC ) -> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) e. CC )
153		eqid	|- ( y e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) = ( y e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) )
154	152 153	fmptd	|- ( ph -> ( y e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) : CC --> CC )
155		2cnd	|- ( ph -> 2 e. CC )
156		picn	|- _pi e. CC
157	156	a1i	|- ( ph -> _pi e. CC )
158	155 157	mulcld	|- ( ph -> ( 2 x. _pi ) e. CC )
159		dvasinbx	|- ( ( ( 2 x. _pi ) e. CC /\ ( 1 / 2 ) e. CC ) -> ( CC _D ( y e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) = ( y e. CC |-> ( ( ( 2 x. _pi ) x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. y ) ) ) ) )
160	158 44 159	sylancl	|- ( ph -> ( CC _D ( y e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) = ( y e. CC |-> ( ( ( 2 x. _pi ) x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. y ) ) ) ) )
161		2cnd	|- ( ( ph /\ y e. CC ) -> 2 e. CC )
162	156	a1i	|- ( ( ph /\ y e. CC ) -> _pi e. CC )
163	161 162 149	mul32d	|- ( ( ph /\ y e. CC ) -> ( ( 2 x. _pi ) x. ( 1 / 2 ) ) = ( ( 2 x. ( 1 / 2 ) ) x. _pi ) )
164	135	a1i	|- ( ( ph /\ y e. CC ) -> 2 =/= 0 )
165	161 164	recidd	|- ( ( ph /\ y e. CC ) -> ( 2 x. ( 1 / 2 ) ) = 1 )
166	165	oveq1d	|- ( ( ph /\ y e. CC ) -> ( ( 2 x. ( 1 / 2 ) ) x. _pi ) = ( 1 x. _pi ) )
167	162	mullidd	|- ( ( ph /\ y e. CC ) -> ( 1 x. _pi ) = _pi )
168	163 166 167	3eqtrd	|- ( ( ph /\ y e. CC ) -> ( ( 2 x. _pi ) x. ( 1 / 2 ) ) = _pi )
169	140	fveq2d	|- ( y e. CC -> ( cos ` ( ( 1 / 2 ) x. y ) ) = ( cos ` ( y / 2 ) ) )
170	169	adantl	|- ( ( ph /\ y e. CC ) -> ( cos ` ( ( 1 / 2 ) x. y ) ) = ( cos ` ( y / 2 ) ) )
171	168 170	oveq12d	|- ( ( ph /\ y e. CC ) -> ( ( ( 2 x. _pi ) x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. y ) ) ) = ( _pi x. ( cos ` ( y / 2 ) ) ) )
172	171	mpteq2dva	|- ( ph -> ( y e. CC |-> ( ( ( 2 x. _pi ) x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. y ) ) ) ) = ( y e. CC |-> ( _pi x. ( cos ` ( y / 2 ) ) ) ) )
173	160 172	eqtrd	|- ( ph -> ( CC _D ( y e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) = ( y e. CC |-> ( _pi x. ( cos ` ( y / 2 ) ) ) ) )
174	173	dmeqd	|- ( ph -> dom ( CC _D ( y e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) = dom ( y e. CC |-> ( _pi x. ( cos ` ( y / 2 ) ) ) ) )
175		eqid	|- ( y e. CC |-> ( _pi x. ( cos ` ( y / 2 ) ) ) ) = ( y e. CC |-> ( _pi x. ( cos ` ( y / 2 ) ) ) )
176	74	halfcld	|- ( ( ph /\ y e. CC ) -> ( y / 2 ) e. CC )
177	176	coscld	|- ( ( ph /\ y e. CC ) -> ( cos ` ( y / 2 ) ) e. CC )
178	162 177	mulcld	|- ( ( ph /\ y e. CC ) -> ( _pi x. ( cos ` ( y / 2 ) ) ) e. CC )
179	175 178	dmmptd	|- ( ph -> dom ( y e. CC |-> ( _pi x. ( cos ` ( y / 2 ) ) ) ) = CC )
180	174 179	eqtrd	|- ( ph -> dom ( CC _D ( y e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) = CC )
181	41 180	sseqtrrid	|- ( ph -> RR C_ dom ( CC _D ( y e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) )
182		dvres3	|- ( ( ( RR e. { RR , CC } /\ ( y e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) : CC --> CC ) /\ ( CC C_ CC /\ RR C_ dom ( CC _D ( y e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) ) ) -> ( RR _D ( ( y e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) |` RR ) ) = ( ( CC _D ( y e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) |` RR ) )
183	72 154 80 181 182	syl22anc	|- ( ph -> ( RR _D ( ( y e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) |` RR ) ) = ( ( CC _D ( y e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) |` RR ) )
184		resmpt	|- ( RR C_ CC -> ( ( y e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) |` RR ) = ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) )
185	41 184	mp1i	|- ( ph -> ( ( y e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) |` RR ) = ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) )
186	185	oveq2d	|- ( ph -> ( RR _D ( ( y e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) |` RR ) ) = ( RR _D ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) )
187	173	reseq1d	|- ( ph -> ( ( CC _D ( y e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) |` RR ) = ( ( y e. CC |-> ( _pi x. ( cos ` ( y / 2 ) ) ) ) |` RR ) )
188	183 186 187	3eqtr3d	|- ( ph -> ( RR _D ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) = ( ( y e. CC |-> ( _pi x. ( cos ` ( y / 2 ) ) ) ) |` RR ) )
189		resmpt	|- ( RR C_ CC -> ( ( y e. CC |-> ( _pi x. ( cos ` ( y / 2 ) ) ) ) |` RR ) = ( y e. RR |-> ( _pi x. ( cos ` ( y / 2 ) ) ) ) )
190	41 189	ax-mp	|- ( ( y e. CC |-> ( _pi x. ( cos ` ( y / 2 ) ) ) ) |` RR ) = ( y e. RR |-> ( _pi x. ( cos ` ( y / 2 ) ) ) )
191	188 190	eqtrdi	|- ( ph -> ( RR _D ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) = ( y e. RR |-> ( _pi x. ( cos ` ( y / 2 ) ) ) ) )
192	147 191	eqtrd	|- ( ph -> ( RR _D ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) = ( y e. RR |-> ( _pi x. ( cos ` ( y / 2 ) ) ) ) )
193	192	reseq1d	|- ( ph -> ( ( RR _D ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) |` ( ( A (,) B ) \ { Y } ) ) = ( ( y e. RR |-> ( _pi x. ( cos ` ( y / 2 ) ) ) ) |` ( ( A (,) B ) \ { Y } ) ) )
194	15	resmptd	|- ( ph -> ( ( y e. RR |-> ( _pi x. ( cos ` ( y / 2 ) ) ) ) |` ( ( A (,) B ) \ { Y } ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( _pi x. ( cos ` ( y / 2 ) ) ) ) )
195	130 193 194	3eqtrd	|- ( ph -> ( ( RR _D ( y e. RR |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) \ { Y } ) ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( _pi x. ( cos ` ( y / 2 ) ) ) ) )
196	120 129 195	3eqtrd	|- ( ph -> ( RR _D ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( _pi x. ( cos ` ( y / 2 ) ) ) ) )
197	196	eqcomd	|- ( ph -> ( y e. ( ( A (,) B ) \ { Y } ) |-> ( _pi x. ( cos ` ( y / 2 ) ) ) ) = ( RR _D ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) )
198	3	a1i	|- ( ph -> G = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) )
199	198	oveq2d	|- ( ph -> ( RR _D G ) = ( RR _D ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) )
200	199	eqcomd	|- ( ph -> ( RR _D ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) = ( RR _D G ) )
201	115 197 200	3eqtrrd	|- ( ph -> ( RR _D G ) = I )
202	201	dmeqd	|- ( ph -> dom ( RR _D G ) = dom I )
203	109 178	syldan	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( _pi x. ( cos ` ( y / 2 ) ) ) e. CC )
204	6 203	dmmptd	|- ( ph -> dom I = ( ( A (,) B ) \ { Y } ) )
205	202 204	eqtr2d	|- ( ph -> ( ( A (,) B ) \ { Y } ) = dom ( RR _D G ) )
206		eqimss	|- ( ( ( A (,) B ) \ { Y } ) = dom ( RR _D G ) -> ( ( A (,) B ) \ { Y } ) C_ dom ( RR _D G ) )
207	205 206	syl	|- ( ph -> ( ( A (,) B ) \ { Y } ) C_ dom ( RR _D G ) )
208	109 75	syldan	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. y ) e. CC )
209	208	ralrimiva	|- ( ph -> A. y e. ( ( A (,) B ) \ { Y } ) ( ( N + ( 1 / 2 ) ) x. y ) e. CC )
210		eqid	|- ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) )
211	210	fnmpt	|- ( A. y e. ( ( A (,) B ) \ { Y } ) ( ( N + ( 1 / 2 ) ) x. y ) e. CC -> ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) Fn ( ( A (,) B ) \ { Y } ) )
212	209 211	syl	|- ( ph -> ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) Fn ( ( A (,) B ) \ { Y } ) )
213		eqidd	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) )
214		simpr	|- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ y = w ) -> y = w )
215	214	oveq2d	|- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ y = w ) -> ( ( N + ( 1 / 2 ) ) x. y ) = ( ( N + ( 1 / 2 ) ) x. w ) )
216		simpr	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> w e. ( ( A (,) B ) \ { Y } ) )
217	43	adantr	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> N e. CC )
218		1cnd	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> 1 e. CC )
219	218	halfcld	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( 1 / 2 ) e. CC )
220	217 219	addcld	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( N + ( 1 / 2 ) ) e. CC )
221		eldifi	|- ( w e. ( ( A (,) B ) \ { Y } ) -> w e. ( A (,) B ) )
222	221	elioored	|- ( w e. ( ( A (,) B ) \ { Y } ) -> w e. RR )
223	222	recnd	|- ( w e. ( ( A (,) B ) \ { Y } ) -> w e. CC )
224	223	adantl	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> w e. CC )
225	220 224	mulcld	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. w ) e. CC )
226	213 215 216 225	fvmptd	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) = ( ( N + ( 1 / 2 ) ) x. w ) )
227		eleq1w	|- ( y = w -> ( y e. ( ( A (,) B ) \ { Y } ) <-> w e. ( ( A (,) B ) \ { Y } ) ) )
228	227	anbi2d	|- ( y = w -> ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) <-> ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) ) )
229		oveq1	|- ( y = w -> ( y mod ( 2 x. _pi ) ) = ( w mod ( 2 x. _pi ) ) )
230	229	neeq1d	|- ( y = w -> ( ( y mod ( 2 x. _pi ) ) =/= 0 <-> ( w mod ( 2 x. _pi ) ) =/= 0 ) )
231	228 230	imbi12d	|- ( y = w -> ( ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( y mod ( 2 x. _pi ) ) =/= 0 ) <-> ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( w mod ( 2 x. _pi ) ) =/= 0 ) ) )
232		eldifi	|- ( y e. ( ( A (,) B ) \ { Y } ) -> y e. ( A (,) B ) )
233		elioore	|- ( y e. ( A (,) B ) -> y e. RR )
234	232 233 131	3syl	|- ( y e. ( ( A (,) B ) \ { Y } ) -> y e. CC )
235		2cnd	|- ( y e. ( ( A (,) B ) \ { Y } ) -> 2 e. CC )
236	156	a1i	|- ( y e. ( ( A (,) B ) \ { Y } ) -> _pi e. CC )
237	135	a1i	|- ( y e. ( ( A (,) B ) \ { Y } ) -> 2 =/= 0 )
238		0re	|- 0 e. RR
239		pipos	|- 0 < _pi
240	238 239	gtneii	|- _pi =/= 0
241	240	a1i	|- ( y e. ( ( A (,) B ) \ { Y } ) -> _pi =/= 0 )
242	234 235 236 237 241	divdiv1d	|- ( y e. ( ( A (,) B ) \ { Y } ) -> ( ( y / 2 ) / _pi ) = ( y / ( 2 x. _pi ) ) )
243	242	eqcomd	|- ( y e. ( ( A (,) B ) \ { Y } ) -> ( y / ( 2 x. _pi ) ) = ( ( y / 2 ) / _pi ) )
244	243	adantl	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( y / ( 2 x. _pi ) ) = ( ( y / 2 ) / _pi ) )
245	4	neneqd	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> -. ( sin ` ( y / 2 ) ) = 0 )
246	109	halfcld	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( y / 2 ) e. CC )
247		sineq0	|- ( ( y / 2 ) e. CC -> ( ( sin ` ( y / 2 ) ) = 0 <-> ( ( y / 2 ) / _pi ) e. ZZ ) )
248	246 247	syl	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( sin ` ( y / 2 ) ) = 0 <-> ( ( y / 2 ) / _pi ) e. ZZ ) )
249	245 248	mtbid	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> -. ( ( y / 2 ) / _pi ) e. ZZ )
250	244 249	eqneltrd	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> -. ( y / ( 2 x. _pi ) ) e. ZZ )
251		2rp	|- 2 e. RR+
252		pirp	|- _pi e. RR+
253		rpmulcl	|- ( ( 2 e. RR+ /\ _pi e. RR+ ) -> ( 2 x. _pi ) e. RR+ )
254	251 252 253	mp2an	|- ( 2 x. _pi ) e. RR+
255		mod0	|- ( ( y e. RR /\ ( 2 x. _pi ) e. RR+ ) -> ( ( y mod ( 2 x. _pi ) ) = 0 <-> ( y / ( 2 x. _pi ) ) e. ZZ ) )
256	21 254 255	sylancl	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( y mod ( 2 x. _pi ) ) = 0 <-> ( y / ( 2 x. _pi ) ) e. ZZ ) )
257	250 256	mtbird	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> -. ( y mod ( 2 x. _pi ) ) = 0 )
258	257	neqned	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( y mod ( 2 x. _pi ) ) =/= 0 )
259	231 258	chvarvv	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( w mod ( 2 x. _pi ) ) =/= 0 )
260	259	neneqd	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> -. ( w mod ( 2 x. _pi ) ) = 0 )
261		simpll	|- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> ph )
262		simpr	|- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) )
263	223	ad2antlr	|- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> w e. CC )
264	62	recnd	|- ( ph -> Y e. CC )
265	264	ad2antrr	|- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> Y e. CC )
266		0red	|- ( ph -> 0 e. RR )
267	8	nnred	|- ( ph -> N e. RR )
268		1red	|- ( ph -> 1 e. RR )
269	268	rehalfcld	|- ( ph -> ( 1 / 2 ) e. RR )
270	267 269	readdcld	|- ( ph -> ( N + ( 1 / 2 ) ) e. RR )
271	8	nngt0d	|- ( ph -> 0 < N )
272	251	a1i	|- ( ph -> 2 e. RR+ )
273	272	rpreccld	|- ( ph -> ( 1 / 2 ) e. RR+ )
274	267 273	ltaddrpd	|- ( ph -> N < ( N + ( 1 / 2 ) ) )
275	266 267 270 271 274	lttrd	|- ( ph -> 0 < ( N + ( 1 / 2 ) ) )
276	275	gt0ne0d	|- ( ph -> ( N + ( 1 / 2 ) ) =/= 0 )
277	46 276	jca	|- ( ph -> ( ( N + ( 1 / 2 ) ) e. CC /\ ( N + ( 1 / 2 ) ) =/= 0 ) )
278	277	ad2antrr	|- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> ( ( N + ( 1 / 2 ) ) e. CC /\ ( N + ( 1 / 2 ) ) =/= 0 ) )
279		mulcan	|- ( ( w e. CC /\ Y e. CC /\ ( ( N + ( 1 / 2 ) ) e. CC /\ ( N + ( 1 / 2 ) ) =/= 0 ) ) -> ( ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) <-> w = Y ) )
280	263 265 278 279	syl3anc	|- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> ( ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) <-> w = Y ) )
281	262 280	mpbid	|- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> w = Y )
282		oveq1	|- ( w = Y -> ( w mod ( 2 x. _pi ) ) = ( Y mod ( 2 x. _pi ) ) )
283	282 10	sylan9eqr	|- ( ( ph /\ w = Y ) -> ( w mod ( 2 x. _pi ) ) = 0 )
284	261 281 283	syl2anc	|- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> ( w mod ( 2 x. _pi ) ) = 0 )
285	260 284	mtand	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> -. ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) )
286	46 264	mulcld	|- ( ph -> ( ( N + ( 1 / 2 ) ) x. Y ) e. CC )
287	286	adantr	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. Y ) e. CC )
288		elsn2g	|- ( ( ( N + ( 1 / 2 ) ) x. Y ) e. CC -> ( ( ( N + ( 1 / 2 ) ) x. w ) e. { ( ( N + ( 1 / 2 ) ) x. Y ) } <-> ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) )
289	287 288	syl	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( ( ( N + ( 1 / 2 ) ) x. w ) e. { ( ( N + ( 1 / 2 ) ) x. Y ) } <-> ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) )
290	285 289	mtbird	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> -. ( ( N + ( 1 / 2 ) ) x. w ) e. { ( ( N + ( 1 / 2 ) ) x. Y ) } )
291	225 290	eldifd	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. w ) e. ( CC \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) )
292	226 291	eqeltrd	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) e. ( CC \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) )
293		sinf	|- sin : CC --> CC
294	293	fdmi	|- dom sin = CC
295	294	eqcomi	|- CC = dom sin
296	295	a1i	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> CC = dom sin )
297	296	difeq1d	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( CC \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) = ( dom sin \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) )
298	292 297	eleqtrd	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) e. ( dom sin \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) )
299	298	ralrimiva	|- ( ph -> A. w e. ( ( A (,) B ) \ { Y } ) ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) e. ( dom sin \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) )
300		fnfvrnss	|- ( ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) Fn ( ( A (,) B ) \ { Y } ) /\ A. w e. ( ( A (,) B ) \ { Y } ) ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) e. ( dom sin \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) ) -> ran ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) C_ ( dom sin \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) )
301	212 299 300	syl2anc	|- ( ph -> ran ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) C_ ( dom sin \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) )
302		uncom	|- ( ( ( A (,) B ) \ { Y } ) u. { Y } ) = ( { Y } u. ( ( A (,) B ) \ { Y } ) )
303	302	a1i	|- ( ph -> ( ( ( A (,) B ) \ { Y } ) u. { Y } ) = ( { Y } u. ( ( A (,) B ) \ { Y } ) ) )
304	9	snssd	|- ( ph -> { Y } C_ ( A (,) B ) )
305		undif	|- ( { Y } C_ ( A (,) B ) <-> ( { Y } u. ( ( A (,) B ) \ { Y } ) ) = ( A (,) B ) )
306	304 305	sylib	|- ( ph -> ( { Y } u. ( ( A (,) B ) \ { Y } ) ) = ( A (,) B ) )
307	303 306	eqtrd	|- ( ph -> ( ( ( A (,) B ) \ { Y } ) u. { Y } ) = ( A (,) B ) )
308	307	mpteq1d	|- ( ph -> ( w e. ( ( ( A (,) B ) \ { Y } ) u. { Y } ) |-> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) ) = ( w e. ( A (,) B ) |-> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) ) )
309		iftrue	|- ( w = Y -> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) = ( ( N + ( 1 / 2 ) ) x. Y ) )
310		oveq2	|- ( w = Y -> ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) )
311	309 310	eqtr4d	|- ( w = Y -> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) = ( ( N + ( 1 / 2 ) ) x. w ) )
312	311	adantl	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ w = Y ) -> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) = ( ( N + ( 1 / 2 ) ) x. w ) )
313		iffalse	|- ( -. w = Y -> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) = ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) )
314	313	adantl	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) = ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) )
315		eqidd	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) )
316		oveq2	|- ( y = w -> ( ( N + ( 1 / 2 ) ) x. y ) = ( ( N + ( 1 / 2 ) ) x. w ) )
317	316	adantl	|- ( ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) /\ y = w ) -> ( ( N + ( 1 / 2 ) ) x. y ) = ( ( N + ( 1 / 2 ) ) x. w ) )
318		simpl	|- ( ( w e. ( A (,) B ) /\ -. w = Y ) -> w e. ( A (,) B ) )
319		id	|- ( -. w = Y -> -. w = Y )
320		velsn	|- ( w e. { Y } <-> w = Y )
321	319 320	sylnibr	|- ( -. w = Y -> -. w e. { Y } )
322	321	adantl	|- ( ( w e. ( A (,) B ) /\ -. w = Y ) -> -. w e. { Y } )
323	318 322	eldifd	|- ( ( w e. ( A (,) B ) /\ -. w = Y ) -> w e. ( ( A (,) B ) \ { Y } ) )
324	323	adantll	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> w e. ( ( A (,) B ) \ { Y } ) )
325	46	adantr	|- ( ( ph /\ w e. ( A (,) B ) ) -> ( N + ( 1 / 2 ) ) e. CC )
326		elioore	|- ( w e. ( A (,) B ) -> w e. RR )
327	326	recnd	|- ( w e. ( A (,) B ) -> w e. CC )
328	327	adantl	|- ( ( ph /\ w e. ( A (,) B ) ) -> w e. CC )
329	325 328	mulcld	|- ( ( ph /\ w e. ( A (,) B ) ) -> ( ( N + ( 1 / 2 ) ) x. w ) e. CC )
330	329	adantr	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( ( N + ( 1 / 2 ) ) x. w ) e. CC )
331	315 317 324 330	fvmptd	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) = ( ( N + ( 1 / 2 ) ) x. w ) )
332	314 331	eqtrd	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) = ( ( N + ( 1 / 2 ) ) x. w ) )
333	312 332	pm2.61dan	|- ( ( ph /\ w e. ( A (,) B ) ) -> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) = ( ( N + ( 1 / 2 ) ) x. w ) )
334	333	mpteq2dva	|- ( ph -> ( w e. ( A (,) B ) |-> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) ) = ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) )
335		ioosscn	|- ( A (,) B ) C_ CC
336		resmpt	|- ( ( A (,) B ) C_ CC -> ( ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) ) |` ( A (,) B ) ) = ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) )
337	335 336	ax-mp	|- ( ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) ) |` ( A (,) B ) ) = ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) )
338		eqid	|- ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) ) = ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) )
339	338	mulc1cncf	|- ( ( N + ( 1 / 2 ) ) e. CC -> ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( CC -cn-> CC ) )
340	46 339	syl	|- ( ph -> ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( CC -cn-> CC ) )
341	56	cnfldtop	|- ( TopOpen ` CCfld ) e. Top
342		unicntop	|- CC = U. ( TopOpen ` CCfld )
343	342	restid	|- ( ( TopOpen ` CCfld ) e. Top -> ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld ) )
344	341 343	ax-mp	|- ( ( TopOpen ` CCfld ) |`t CC ) = ( TopOpen ` CCfld )
345	344	eqcomi	|- ( TopOpen ` CCfld ) = ( ( TopOpen ` CCfld ) |`t CC )
346	56 345 345	cncfcn	|- ( ( CC C_ CC /\ CC C_ CC ) -> ( CC -cn-> CC ) = ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
347	79 80 346	sylancr	|- ( ph -> ( CC -cn-> CC ) = ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
348	340 347	eleqtrd	|- ( ph -> ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) )
349	13 42	sstrid	|- ( ph -> ( A (,) B ) C_ CC )
350	342	cnrest	|- ( ( ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( TopOpen ` CCfld ) Cn ( TopOpen ` CCfld ) ) /\ ( A (,) B ) C_ CC ) -> ( ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) ) |` ( A (,) B ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) )
351	348 349 350	syl2anc	|- ( ph -> ( ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) ) |` ( A (,) B ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) )
352	337 351	eqeltrrid	|- ( ph -> ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) )
353	56	cnfldtopon	|- ( TopOpen ` CCfld ) e. ( TopOn ` CC )
354		resttopon	|- ( ( ( TopOpen ` CCfld ) e. ( TopOn ` CC ) /\ ( A (,) B ) C_ CC ) -> ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) e. ( TopOn ` ( A (,) B ) ) )
355	353 349 354	sylancr	|- ( ph -> ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) e. ( TopOn ` ( A (,) B ) ) )
356		cncnp	|- ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) e. ( TopOn ` ( A (,) B ) ) /\ ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) -> ( ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) <-> ( ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) : ( A (,) B ) --> CC /\ A. y e. ( A (,) B ) ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) ) ) )
357	355 353 356	sylancl	|- ( ph -> ( ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) <-> ( ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) : ( A (,) B ) --> CC /\ A. y e. ( A (,) B ) ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) ) ) )
358	352 357	mpbid	|- ( ph -> ( ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) : ( A (,) B ) --> CC /\ A. y e. ( A (,) B ) ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) ) )
359	358	simprd	|- ( ph -> A. y e. ( A (,) B ) ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
360		fveq2	|- ( y = Y -> ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) = ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) )
361	360	eleq2d	|- ( y = Y -> ( ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) <-> ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) ) )
362	361	rspccva	|- ( ( A. y e. ( A (,) B ) ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) /\ Y e. ( A (,) B ) ) -> ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) )
363	359 9 362	syl2anc	|- ( ph -> ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) )
364	334 363	eqeltrd	|- ( ph -> ( w e. ( A (,) B ) |-> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) )
365	307	eqcomd	|- ( ph -> ( A (,) B ) = ( ( ( A (,) B ) \ { Y } ) u. { Y } ) )
366	365	oveq2d	|- ( ph -> ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) = ( ( TopOpen ` CCfld ) |`t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) )
367	366	oveq1d	|- ( ph -> ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) = ( ( ( TopOpen ` CCfld ) |`t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) CnP ( TopOpen ` CCfld ) ) )
368	367	fveq1d	|- ( ph -> ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) = ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) )
369	364 368	eleqtrd	|- ( ph -> ( w e. ( A (,) B ) |-> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) )
370	308 369	eqeltrd	|- ( ph -> ( w e. ( ( ( A (,) B ) \ { Y } ) u. { Y } ) |-> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) )
371		eqid	|- ( ( TopOpen ` CCfld ) |`t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) = ( ( TopOpen ` CCfld ) |`t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) )
372		eqid	|- ( w e. ( ( ( A (,) B ) \ { Y } ) u. { Y } ) |-> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) ) = ( w e. ( ( ( A (,) B ) \ { Y } ) u. { Y } ) |-> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) )
373	208 210	fmptd	|- ( ph -> ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) : ( ( A (,) B ) \ { Y } ) --> CC )
374	15 41	sstrdi	|- ( ph -> ( ( A (,) B ) \ { Y } ) C_ CC )
375	371 56 372 373 374 264	ellimc	|- ( ph -> ( ( ( N + ( 1 / 2 ) ) x. Y ) e. ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) limCC Y ) <-> ( w e. ( ( ( A (,) B ) \ { Y } ) u. { Y } ) |-> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) ) )
376	370 375	mpbird	|- ( ph -> ( ( N + ( 1 / 2 ) ) x. Y ) e. ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) limCC Y ) )
377	135	a1i	|- ( ph -> 2 =/= 0 )
378	240	a1i	|- ( ph -> _pi =/= 0 )
379	155 157 377 378	mulne0d	|- ( ph -> ( 2 x. _pi ) =/= 0 )
380	264 158 379	divcan1d	|- ( ph -> ( ( Y / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) = Y )
381	380	eqcomd	|- ( ph -> Y = ( ( Y / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) )
382	381	oveq2d	|- ( ph -> ( ( N + ( 1 / 2 ) ) x. Y ) = ( ( N + ( 1 / 2 ) ) x. ( ( Y / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) ) )
383	382	fveq2d	|- ( ph -> ( sin ` ( ( N + ( 1 / 2 ) ) x. Y ) ) = ( sin ` ( ( N + ( 1 / 2 ) ) x. ( ( Y / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) ) ) )
384	264 158 379	divcld	|- ( ph -> ( Y / ( 2 x. _pi ) ) e. CC )
385	46 384 158	mul12d	|- ( ph -> ( ( N + ( 1 / 2 ) ) x. ( ( Y / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) ) = ( ( Y / ( 2 x. _pi ) ) x. ( ( N + ( 1 / 2 ) ) x. ( 2 x. _pi ) ) ) )
386	46 155 157	mulassd	|- ( ph -> ( ( ( N + ( 1 / 2 ) ) x. 2 ) x. _pi ) = ( ( N + ( 1 / 2 ) ) x. ( 2 x. _pi ) ) )
387	386	eqcomd	|- ( ph -> ( ( N + ( 1 / 2 ) ) x. ( 2 x. _pi ) ) = ( ( ( N + ( 1 / 2 ) ) x. 2 ) x. _pi ) )
388	387	oveq2d	|- ( ph -> ( ( Y / ( 2 x. _pi ) ) x. ( ( N + ( 1 / 2 ) ) x. ( 2 x. _pi ) ) ) = ( ( Y / ( 2 x. _pi ) ) x. ( ( ( N + ( 1 / 2 ) ) x. 2 ) x. _pi ) ) )
389	43 45 155	adddird	|- ( ph -> ( ( N + ( 1 / 2 ) ) x. 2 ) = ( ( N x. 2 ) + ( ( 1 / 2 ) x. 2 ) ) )
390	155 377	recid2d	|- ( ph -> ( ( 1 / 2 ) x. 2 ) = 1 )
391	390	oveq2d	|- ( ph -> ( ( N x. 2 ) + ( ( 1 / 2 ) x. 2 ) ) = ( ( N x. 2 ) + 1 ) )
392	389 391	eqtrd	|- ( ph -> ( ( N + ( 1 / 2 ) ) x. 2 ) = ( ( N x. 2 ) + 1 ) )
393	392	oveq1d	|- ( ph -> ( ( ( N + ( 1 / 2 ) ) x. 2 ) x. _pi ) = ( ( ( N x. 2 ) + 1 ) x. _pi ) )
394	393	oveq2d	|- ( ph -> ( ( Y / ( 2 x. _pi ) ) x. ( ( ( N + ( 1 / 2 ) ) x. 2 ) x. _pi ) ) = ( ( Y / ( 2 x. _pi ) ) x. ( ( ( N x. 2 ) + 1 ) x. _pi ) ) )
395	385 388 394	3eqtrd	|- ( ph -> ( ( N + ( 1 / 2 ) ) x. ( ( Y / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) ) = ( ( Y / ( 2 x. _pi ) ) x. ( ( ( N x. 2 ) + 1 ) x. _pi ) ) )
396	43 155	mulcld	|- ( ph -> ( N x. 2 ) e. CC )
397		1cnd	|- ( ph -> 1 e. CC )
398	396 397	addcld	|- ( ph -> ( ( N x. 2 ) + 1 ) e. CC )
399	384 398 157	mulassd	|- ( ph -> ( ( ( Y / ( 2 x. _pi ) ) x. ( ( N x. 2 ) + 1 ) ) x. _pi ) = ( ( Y / ( 2 x. _pi ) ) x. ( ( ( N x. 2 ) + 1 ) x. _pi ) ) )
400	395 399	eqtr4d	|- ( ph -> ( ( N + ( 1 / 2 ) ) x. ( ( Y / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) ) = ( ( ( Y / ( 2 x. _pi ) ) x. ( ( N x. 2 ) + 1 ) ) x. _pi ) )
401	400	fveq2d	|- ( ph -> ( sin ` ( ( N + ( 1 / 2 ) ) x. ( ( Y / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) ) ) = ( sin ` ( ( ( Y / ( 2 x. _pi ) ) x. ( ( N x. 2 ) + 1 ) ) x. _pi ) ) )
402		mod0	|- ( ( Y e. RR /\ ( 2 x. _pi ) e. RR+ ) -> ( ( Y mod ( 2 x. _pi ) ) = 0 <-> ( Y / ( 2 x. _pi ) ) e. ZZ ) )
403	62 254 402	sylancl	|- ( ph -> ( ( Y mod ( 2 x. _pi ) ) = 0 <-> ( Y / ( 2 x. _pi ) ) e. ZZ ) )
404	10 403	mpbid	|- ( ph -> ( Y / ( 2 x. _pi ) ) e. ZZ )
405	8	nnzd	|- ( ph -> N e. ZZ )
406		2z	|- 2 e. ZZ
407	406	a1i	|- ( ph -> 2 e. ZZ )
408	405 407	zmulcld	|- ( ph -> ( N x. 2 ) e. ZZ )
409	408	peano2zd	|- ( ph -> ( ( N x. 2 ) + 1 ) e. ZZ )
410	404 409	zmulcld	|- ( ph -> ( ( Y / ( 2 x. _pi ) ) x. ( ( N x. 2 ) + 1 ) ) e. ZZ )
411		sinkpi	|- ( ( ( Y / ( 2 x. _pi ) ) x. ( ( N x. 2 ) + 1 ) ) e. ZZ -> ( sin ` ( ( ( Y / ( 2 x. _pi ) ) x. ( ( N x. 2 ) + 1 ) ) x. _pi ) ) = 0 )
412	410 411	syl	|- ( ph -> ( sin ` ( ( ( Y / ( 2 x. _pi ) ) x. ( ( N x. 2 ) + 1 ) ) x. _pi ) ) = 0 )
413	383 401 412	3eqtrd	|- ( ph -> ( sin ` ( ( N + ( 1 / 2 ) ) x. Y ) ) = 0 )
414		sincn	|- sin e. ( CC -cn-> CC )
415	414	a1i	|- ( ph -> sin e. ( CC -cn-> CC ) )
416	415 286	cnlimci	|- ( ph -> ( sin ` ( ( N + ( 1 / 2 ) ) x. Y ) ) e. ( sin limCC ( ( N + ( 1 / 2 ) ) x. Y ) ) )
417	413 416	eqeltrrd	|- ( ph -> 0 e. ( sin limCC ( ( N + ( 1 / 2 ) ) x. Y ) ) )
418	301 376 417	limccog	|- ( ph -> 0 e. ( ( sin o. ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ) limCC Y ) )
419	2	a1i	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> F = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
420	215	fveq2d	|- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ y = w ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) = ( sin ` ( ( N + ( 1 / 2 ) ) x. w ) ) )
421	225	sincld	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. w ) ) e. CC )
422	419 420 216 421	fvmptd	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( F ` w ) = ( sin ` ( ( N + ( 1 / 2 ) ) x. w ) ) )
423	226	fveq2d	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( sin ` ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) = ( sin ` ( ( N + ( 1 / 2 ) ) x. w ) ) )
424	422 423	eqtr4d	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( F ` w ) = ( sin ` ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) )
425	424	mpteq2dva	|- ( ph -> ( w e. ( ( A (,) B ) \ { Y } ) |-> ( F ` w ) ) = ( w e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) ) )
426	24	feqmptd	|- ( ph -> F = ( w e. ( ( A (,) B ) \ { Y } ) |-> ( F ` w ) ) )
427		fcompt	|- ( ( sin : CC --> CC /\ ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) : ( ( A (,) B ) \ { Y } ) --> CC ) -> ( sin o. ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ) = ( w e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) ) )
428	293 373 427	sylancr	|- ( ph -> ( sin o. ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ) = ( w e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) ) )
429	425 426 428	3eqtr4rd	|- ( ph -> ( sin o. ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ) = F )
430	429	oveq1d	|- ( ph -> ( ( sin o. ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ) limCC Y ) = ( F limCC Y ) )
431	418 430	eleqtrd	|- ( ph -> 0 e. ( F limCC Y ) )
432		simpr	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ w = Y ) -> w = Y )
433	432	iftrued	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ w = Y ) -> if ( w = Y , 0 , ( G ` w ) ) = 0 )
434	264 155 158 377 379	divdiv32d	|- ( ph -> ( ( Y / 2 ) / ( 2 x. _pi ) ) = ( ( Y / ( 2 x. _pi ) ) / 2 ) )
435	434	oveq1d	|- ( ph -> ( ( ( Y / 2 ) / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) = ( ( ( Y / ( 2 x. _pi ) ) / 2 ) x. ( 2 x. _pi ) ) )
436	264	halfcld	|- ( ph -> ( Y / 2 ) e. CC )
437	436 158 379	divcan1d	|- ( ph -> ( ( ( Y / 2 ) / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) = ( Y / 2 ) )
438	384 155 158 377	div32d	|- ( ph -> ( ( ( Y / ( 2 x. _pi ) ) / 2 ) x. ( 2 x. _pi ) ) = ( ( Y / ( 2 x. _pi ) ) x. ( ( 2 x. _pi ) / 2 ) ) )
439	157 155 377	divcan3d	|- ( ph -> ( ( 2 x. _pi ) / 2 ) = _pi )
440	439	oveq2d	|- ( ph -> ( ( Y / ( 2 x. _pi ) ) x. ( ( 2 x. _pi ) / 2 ) ) = ( ( Y / ( 2 x. _pi ) ) x. _pi ) )
441	438 440	eqtrd	|- ( ph -> ( ( ( Y / ( 2 x. _pi ) ) / 2 ) x. ( 2 x. _pi ) ) = ( ( Y / ( 2 x. _pi ) ) x. _pi ) )
442	435 437 441	3eqtr3d	|- ( ph -> ( Y / 2 ) = ( ( Y / ( 2 x. _pi ) ) x. _pi ) )
443	442	fveq2d	|- ( ph -> ( sin ` ( Y / 2 ) ) = ( sin ` ( ( Y / ( 2 x. _pi ) ) x. _pi ) ) )
444		sinkpi	|- ( ( Y / ( 2 x. _pi ) ) e. ZZ -> ( sin ` ( ( Y / ( 2 x. _pi ) ) x. _pi ) ) = 0 )
445	404 444	syl	|- ( ph -> ( sin ` ( ( Y / ( 2 x. _pi ) ) x. _pi ) ) = 0 )
446	443 445	eqtrd	|- ( ph -> ( sin ` ( Y / 2 ) ) = 0 )
447	446	oveq2d	|- ( ph -> ( ( 2 x. _pi ) x. ( sin ` ( Y / 2 ) ) ) = ( ( 2 x. _pi ) x. 0 ) )
448	158	mul01d	|- ( ph -> ( ( 2 x. _pi ) x. 0 ) = 0 )
449	447 448	eqtrd	|- ( ph -> ( ( 2 x. _pi ) x. ( sin ` ( Y / 2 ) ) ) = 0 )
450	449	eqcomd	|- ( ph -> 0 = ( ( 2 x. _pi ) x. ( sin ` ( Y / 2 ) ) ) )
451	450	ad2antrr	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ w = Y ) -> 0 = ( ( 2 x. _pi ) x. ( sin ` ( Y / 2 ) ) ) )
452		fvoveq1	|- ( w = Y -> ( sin ` ( w / 2 ) ) = ( sin ` ( Y / 2 ) ) )
453	452	oveq2d	|- ( w = Y -> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) = ( ( 2 x. _pi ) x. ( sin ` ( Y / 2 ) ) ) )
454	453	eqcomd	|- ( w = Y -> ( ( 2 x. _pi ) x. ( sin ` ( Y / 2 ) ) ) = ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) )
455	454	adantl	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ w = Y ) -> ( ( 2 x. _pi ) x. ( sin ` ( Y / 2 ) ) ) = ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) )
456	433 451 455	3eqtrd	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ w = Y ) -> if ( w = Y , 0 , ( G ` w ) ) = ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) )
457		iffalse	|- ( -. w = Y -> if ( w = Y , 0 , ( G ` w ) ) = ( G ` w ) )
458	457	adantl	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> if ( w = Y , 0 , ( G ` w ) ) = ( G ` w ) )
459		fvoveq1	|- ( y = w -> ( sin ` ( y / 2 ) ) = ( sin ` ( w / 2 ) ) )
460	459	oveq2d	|- ( y = w -> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) = ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) )
461	121	a1i	|- ( ( ph /\ w e. ( A (,) B ) ) -> ( 2 x. _pi ) e. CC )
462	328	halfcld	|- ( ( ph /\ w e. ( A (,) B ) ) -> ( w / 2 ) e. CC )
463	462	sincld	|- ( ( ph /\ w e. ( A (,) B ) ) -> ( sin ` ( w / 2 ) ) e. CC )
464	461 463	mulcld	|- ( ( ph /\ w e. ( A (,) B ) ) -> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) e. CC )
465	464	adantr	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) e. CC )
466	3 460 324 465	fvmptd3	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( G ` w ) = ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) )
467	458 466	eqtrd	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> if ( w = Y , 0 , ( G ` w ) ) = ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) )
468	456 467	pm2.61dan	|- ( ( ph /\ w e. ( A (,) B ) ) -> if ( w = Y , 0 , ( G ` w ) ) = ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) )
469	468	mpteq2dva	|- ( ph -> ( w e. ( A (,) B ) |-> if ( w = Y , 0 , ( G ` w ) ) ) = ( w e. ( A (,) B ) |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) )
470		eqid	|- ( w e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) = ( w e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) )
471	80 158 80	constcncfg	|- ( ph -> ( w e. CC |-> ( 2 x. _pi ) ) e. ( CC -cn-> CC ) )
472		id	|- ( w e. CC -> w e. CC )
473		2cnd	|- ( w e. CC -> 2 e. CC )
474	135	a1i	|- ( w e. CC -> 2 =/= 0 )
475	472 473 474	divrec2d	|- ( w e. CC -> ( w / 2 ) = ( ( 1 / 2 ) x. w ) )
476	475	mpteq2ia	|- ( w e. CC |-> ( w / 2 ) ) = ( w e. CC |-> ( ( 1 / 2 ) x. w ) )
477		eqid	|- ( w e. CC |-> ( ( 1 / 2 ) x. w ) ) = ( w e. CC |-> ( ( 1 / 2 ) x. w ) )
478	477	mulc1cncf	|- ( ( 1 / 2 ) e. CC -> ( w e. CC |-> ( ( 1 / 2 ) x. w ) ) e. ( CC -cn-> CC ) )
479	44 478	ax-mp	|- ( w e. CC |-> ( ( 1 / 2 ) x. w ) ) e. ( CC -cn-> CC )
480	476 479	eqeltri	|- ( w e. CC |-> ( w / 2 ) ) e. ( CC -cn-> CC )
481	480	a1i	|- ( ph -> ( w e. CC |-> ( w / 2 ) ) e. ( CC -cn-> CC ) )
482	415 481	cncfmpt1f	|- ( ph -> ( w e. CC |-> ( sin ` ( w / 2 ) ) ) e. ( CC -cn-> CC ) )
483	471 482	mulcncf	|- ( ph -> ( w e. CC |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) e. ( CC -cn-> CC ) )
484	470 483 349 80 464	cncfmptssg	|- ( ph -> ( w e. ( A (,) B ) |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
485		eqid	|- ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) = ( ( TopOpen ` CCfld ) |`t ( A (,) B ) )
486	56 485 345	cncfcn	|- ( ( ( A (,) B ) C_ CC /\ CC C_ CC ) -> ( ( A (,) B ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) )
487	349 79 486	sylancl	|- ( ph -> ( ( A (,) B ) -cn-> CC ) = ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) )
488	484 487	eleqtrd	|- ( ph -> ( w e. ( A (,) B ) |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) )
489		cncnp	|- ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) e. ( TopOn ` ( A (,) B ) ) /\ ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) -> ( ( w e. ( A (,) B ) |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) <-> ( ( w e. ( A (,) B ) |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) : ( A (,) B ) --> CC /\ A. y e. ( A (,) B ) ( w e. ( A (,) B ) |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) ) ) )
490	355 353 489	sylancl	|- ( ph -> ( ( w e. ( A (,) B ) |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) <-> ( ( w e. ( A (,) B ) |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) : ( A (,) B ) --> CC /\ A. y e. ( A (,) B ) ( w e. ( A (,) B ) |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) ) ) )
491	488 490	mpbid	|- ( ph -> ( ( w e. ( A (,) B ) |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) : ( A (,) B ) --> CC /\ A. y e. ( A (,) B ) ( w e. ( A (,) B ) |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) ) )
492	491	simprd	|- ( ph -> A. y e. ( A (,) B ) ( w e. ( A (,) B ) |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
493	360	eleq2d	|- ( y = Y -> ( ( w e. ( A (,) B ) |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) <-> ( w e. ( A (,) B ) |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) ) )
494	493	rspccva	|- ( ( A. y e. ( A (,) B ) ( w e. ( A (,) B ) |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) /\ Y e. ( A (,) B ) ) -> ( w e. ( A (,) B ) |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) )
495	492 9 494	syl2anc	|- ( ph -> ( w e. ( A (,) B ) |-> ( ( 2 x. _pi ) x. ( sin ` ( w / 2 ) ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) )
496	469 495	eqeltrd	|- ( ph -> ( w e. ( A (,) B ) |-> if ( w = Y , 0 , ( G ` w ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) )
497	307	mpteq1d	|- ( ph -> ( w e. ( ( ( A (,) B ) \ { Y } ) u. { Y } ) |-> if ( w = Y , 0 , ( G ` w ) ) ) = ( w e. ( A (,) B ) |-> if ( w = Y , 0 , ( G ` w ) ) ) )
498	366	eqcomd	|- ( ph -> ( ( TopOpen ` CCfld ) |`t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) = ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) )
499	498	oveq1d	|- ( ph -> ( ( ( TopOpen ` CCfld ) |`t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) CnP ( TopOpen ` CCfld ) ) = ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) )
500	499	fveq1d	|- ( ph -> ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) = ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) )
501	496 497 500	3eltr4d	|- ( ph -> ( w e. ( ( ( A (,) B ) \ { Y } ) u. { Y } ) |-> if ( w = Y , 0 , ( G ` w ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) )
502		eqid	|- ( w e. ( ( ( A (,) B ) \ { Y } ) u. { Y } ) |-> if ( w = Y , 0 , ( G ` w ) ) ) = ( w e. ( ( ( A (,) B ) \ { Y } ) u. { Y } ) |-> if ( w = Y , 0 , ( G ` w ) ) )
503	21 125	syldan	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) e. CC )
504	503 3	fmptd	|- ( ph -> G : ( ( A (,) B ) \ { Y } ) --> CC )
505	371 56 502 504 374 264	ellimc	|- ( ph -> ( 0 e. ( G limCC Y ) <-> ( w e. ( ( ( A (,) B ) \ { Y } ) u. { Y } ) |-> if ( w = Y , 0 , ( G ` w ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) ) )
506	501 505	mpbird	|- ( ph -> 0 e. ( G limCC Y ) )
507	257	nrexdv	|- ( ph -> -. E. y e. ( ( A (,) B ) \ { Y } ) ( y mod ( 2 x. _pi ) ) = 0 )
508	504	ffund	|- ( ph -> Fun G )
509		fvelima	|- ( ( Fun G /\ 0 e. ( G " ( ( A (,) B ) \ { Y } ) ) ) -> E. y e. ( ( A (,) B ) \ { Y } ) ( G ` y ) = 0 )
510	508 509	sylan	|- ( ( ph /\ 0 e. ( G " ( ( A (,) B ) \ { Y } ) ) ) -> E. y e. ( ( A (,) B ) \ { Y } ) ( G ` y ) = 0 )
511		2cnd	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> 2 e. CC )
512	156	a1i	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> _pi e. CC )
513	135	a1i	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> 2 =/= 0 )
514	240	a1i	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> _pi =/= 0 )
515	109 511 512 513 514	divdiv1d	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( y / 2 ) / _pi ) = ( y / ( 2 x. _pi ) ) )
516	515	eqcomd	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( y / ( 2 x. _pi ) ) = ( ( y / 2 ) / _pi ) )
517	516	adantr	|- ( ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) /\ ( G ` y ) = 0 ) -> ( y / ( 2 x. _pi ) ) = ( ( y / 2 ) / _pi ) )
518		2cnd	|- ( ( y e. ( ( A (,) B ) \ { Y } ) /\ ( G ` y ) = 0 ) -> 2 e. CC )
519	156	a1i	|- ( ( y e. ( ( A (,) B ) \ { Y } ) /\ ( G ` y ) = 0 ) -> _pi e. CC )
520	518 519	mulcld	|- ( ( y e. ( ( A (,) B ) \ { Y } ) /\ ( G ` y ) = 0 ) -> ( 2 x. _pi ) e. CC )
521	234	adantr	|- ( ( y e. ( ( A (,) B ) \ { Y } ) /\ ( G ` y ) = 0 ) -> y e. CC )
522	521	halfcld	|- ( ( y e. ( ( A (,) B ) \ { Y } ) /\ ( G ` y ) = 0 ) -> ( y / 2 ) e. CC )
523	522	sincld	|- ( ( y e. ( ( A (,) B ) \ { Y } ) /\ ( G ` y ) = 0 ) -> ( sin ` ( y / 2 ) ) e. CC )
524	520 523	mulcld	|- ( ( y e. ( ( A (,) B ) \ { Y } ) /\ ( G ` y ) = 0 ) -> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) e. CC )
525	3	fvmpt2	|- ( ( y e. ( ( A (,) B ) \ { Y } ) /\ ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) e. CC ) -> ( G ` y ) = ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) )
526	524 525	syldan	|- ( ( y e. ( ( A (,) B ) \ { Y } ) /\ ( G ` y ) = 0 ) -> ( G ` y ) = ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) )
527	526	eqcomd	|- ( ( y e. ( ( A (,) B ) \ { Y } ) /\ ( G ` y ) = 0 ) -> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) = ( G ` y ) )
528		simpr	|- ( ( y e. ( ( A (,) B ) \ { Y } ) /\ ( G ` y ) = 0 ) -> ( G ` y ) = 0 )
529	527 528	eqtrd	|- ( ( y e. ( ( A (,) B ) \ { Y } ) /\ ( G ` y ) = 0 ) -> ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) = 0 )
530	121	a1i	|- ( y e. ( ( A (,) B ) \ { Y } ) -> ( 2 x. _pi ) e. CC )
531	234	halfcld	|- ( y e. ( ( A (,) B ) \ { Y } ) -> ( y / 2 ) e. CC )
532	531	sincld	|- ( y e. ( ( A (,) B ) \ { Y } ) -> ( sin ` ( y / 2 ) ) e. CC )
533	530 532	mul0ord	|- ( y e. ( ( A (,) B ) \ { Y } ) -> ( ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) = 0 <-> ( ( 2 x. _pi ) = 0 \/ ( sin ` ( y / 2 ) ) = 0 ) ) )
534	533	adantr	|- ( ( y e. ( ( A (,) B ) \ { Y } ) /\ ( G ` y ) = 0 ) -> ( ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) = 0 <-> ( ( 2 x. _pi ) = 0 \/ ( sin ` ( y / 2 ) ) = 0 ) ) )
535	529 534	mpbid	|- ( ( y e. ( ( A (,) B ) \ { Y } ) /\ ( G ` y ) = 0 ) -> ( ( 2 x. _pi ) = 0 \/ ( sin ` ( y / 2 ) ) = 0 ) )
536		2cnne0	|- ( 2 e. CC /\ 2 =/= 0 )
537	156 240	pm3.2i	|- ( _pi e. CC /\ _pi =/= 0 )
538		mulne0	|- ( ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( _pi e. CC /\ _pi =/= 0 ) ) -> ( 2 x. _pi ) =/= 0 )
539	536 537 538	mp2an	|- ( 2 x. _pi ) =/= 0
540	539	neii	|- -. ( 2 x. _pi ) = 0
541		pm2.53	|- ( ( ( 2 x. _pi ) = 0 \/ ( sin ` ( y / 2 ) ) = 0 ) -> ( -. ( 2 x. _pi ) = 0 -> ( sin ` ( y / 2 ) ) = 0 ) )
542	535 540 541	mpisyl	|- ( ( y e. ( ( A (,) B ) \ { Y } ) /\ ( G ` y ) = 0 ) -> ( sin ` ( y / 2 ) ) = 0 )
543	542	adantll	|- ( ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) /\ ( G ` y ) = 0 ) -> ( sin ` ( y / 2 ) ) = 0 )
544	109	adantr	|- ( ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) /\ ( G ` y ) = 0 ) -> y e. CC )
545	544	halfcld	|- ( ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) /\ ( G ` y ) = 0 ) -> ( y / 2 ) e. CC )
546	545 247	syl	|- ( ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) /\ ( G ` y ) = 0 ) -> ( ( sin ` ( y / 2 ) ) = 0 <-> ( ( y / 2 ) / _pi ) e. ZZ ) )
547	543 546	mpbid	|- ( ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) /\ ( G ` y ) = 0 ) -> ( ( y / 2 ) / _pi ) e. ZZ )
548	517 547	eqeltrd	|- ( ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) /\ ( G ` y ) = 0 ) -> ( y / ( 2 x. _pi ) ) e. ZZ )
549	21	adantr	|- ( ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) /\ ( G ` y ) = 0 ) -> y e. RR )
550	549 254 255	sylancl	|- ( ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) /\ ( G ` y ) = 0 ) -> ( ( y mod ( 2 x. _pi ) ) = 0 <-> ( y / ( 2 x. _pi ) ) e. ZZ ) )
551	548 550	mpbird	|- ( ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) /\ ( G ` y ) = 0 ) -> ( y mod ( 2 x. _pi ) ) = 0 )
552	551	ex	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( G ` y ) = 0 -> ( y mod ( 2 x. _pi ) ) = 0 ) )
553	552	reximdva	|- ( ph -> ( E. y e. ( ( A (,) B ) \ { Y } ) ( G ` y ) = 0 -> E. y e. ( ( A (,) B ) \ { Y } ) ( y mod ( 2 x. _pi ) ) = 0 ) )
554	553	adantr	|- ( ( ph /\ 0 e. ( G " ( ( A (,) B ) \ { Y } ) ) ) -> ( E. y e. ( ( A (,) B ) \ { Y } ) ( G ` y ) = 0 -> E. y e. ( ( A (,) B ) \ { Y } ) ( y mod ( 2 x. _pi ) ) = 0 ) )
555	510 554	mpd	|- ( ( ph /\ 0 e. ( G " ( ( A (,) B ) \ { Y } ) ) ) -> E. y e. ( ( A (,) B ) \ { Y } ) ( y mod ( 2 x. _pi ) ) = 0 )
556	507 555	mtand	|- ( ph -> -. 0 e. ( G " ( ( A (,) B ) \ { Y } ) ) )
557		simpr	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> y e. ( ( A (,) B ) \ { Y } ) )
558	6	fvmpt2	|- ( ( y e. ( ( A (,) B ) \ { Y } ) /\ ( _pi x. ( cos ` ( y / 2 ) ) ) e. CC ) -> ( I ` y ) = ( _pi x. ( cos ` ( y / 2 ) ) ) )
559	557 203 558	syl2anc	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( I ` y ) = ( _pi x. ( cos ` ( y / 2 ) ) ) )
560	531	coscld	|- ( y e. ( ( A (,) B ) \ { Y } ) -> ( cos ` ( y / 2 ) ) e. CC )
561	560	adantl	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( cos ` ( y / 2 ) ) e. CC )
562	512 561 514 11	mulne0d	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( _pi x. ( cos ` ( y / 2 ) ) ) =/= 0 )
563	559 562	eqnetrd	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( I ` y ) =/= 0 )
564	563	neneqd	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> -. ( I ` y ) = 0 )
565	564	nrexdv	|- ( ph -> -. E. y e. ( ( A (,) B ) \ { Y } ) ( I ` y ) = 0 )
566	203 6	fmptd	|- ( ph -> I : ( ( A (,) B ) \ { Y } ) --> CC )
567	566	ffund	|- ( ph -> Fun I )
568		fvelima	|- ( ( Fun I /\ 0 e. ( I " ( ( A (,) B ) \ { Y } ) ) ) -> E. y e. ( ( A (,) B ) \ { Y } ) ( I ` y ) = 0 )
569	567 568	sylan	|- ( ( ph /\ 0 e. ( I " ( ( A (,) B ) \ { Y } ) ) ) -> E. y e. ( ( A (,) B ) \ { Y } ) ( I ` y ) = 0 )
570	565 569	mtand	|- ( ph -> -. 0 e. ( I " ( ( A (,) B ) \ { Y } ) ) )
571	201	imaeq1d	|- ( ph -> ( ( RR _D G ) " ( ( A (,) B ) \ { Y } ) ) = ( I " ( ( A (,) B ) \ { Y } ) ) )
572	570 571	neleqtrrd	|- ( ph -> -. 0 e. ( ( RR _D G ) " ( ( A (,) B ) \ { Y } ) ) )
573	1	dirkerval2	|- ( ( N e. NN /\ Y e. RR ) -> ( ( D ` N ) ` Y ) = if ( ( Y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. Y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( Y / 2 ) ) ) ) ) )
574	8 62 573	syl2anc	|- ( ph -> ( ( D ` N ) ` Y ) = if ( ( Y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. Y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( Y / 2 ) ) ) ) ) )
575	10	iftrued	|- ( ph -> if ( ( Y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. Y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( Y / 2 ) ) ) ) ) = ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) )
576	7	a1i	|- ( ph -> L = ( w e. ( A (,) B ) |-> ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) / ( _pi x. ( cos ` ( w / 2 ) ) ) ) ) )
577		iftrue	|- ( w = Y -> if ( w = Y , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) ` w ) ) = ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) )
578	577	adantl	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ w = Y ) -> if ( w = Y , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) ` w ) ) = ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) )
579	155 43	mulcld	|- ( ph -> ( 2 x. N ) e. CC )
580	579 397	addcld	|- ( ph -> ( ( 2 x. N ) + 1 ) e. CC )
581	580 155 157 377 378	divdiv1d	|- ( ph -> ( ( ( ( 2 x. N ) + 1 ) / 2 ) / _pi ) = ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) )
582	581	eqcomd	|- ( ph -> ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) = ( ( ( ( 2 x. N ) + 1 ) / 2 ) / _pi ) )
583	579 397 155 377	divdird	|- ( ph -> ( ( ( 2 x. N ) + 1 ) / 2 ) = ( ( ( 2 x. N ) / 2 ) + ( 1 / 2 ) ) )
584	43 155 377	divcan3d	|- ( ph -> ( ( 2 x. N ) / 2 ) = N )
585	584	oveq1d	|- ( ph -> ( ( ( 2 x. N ) / 2 ) + ( 1 / 2 ) ) = ( N + ( 1 / 2 ) ) )
586	583 585	eqtrd	|- ( ph -> ( ( ( 2 x. N ) + 1 ) / 2 ) = ( N + ( 1 / 2 ) ) )
587	586	oveq1d	|- ( ph -> ( ( ( ( 2 x. N ) + 1 ) / 2 ) / _pi ) = ( ( N + ( 1 / 2 ) ) / _pi ) )
588	582 587	eqtrd	|- ( ph -> ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) = ( ( N + ( 1 / 2 ) ) / _pi ) )
589	588	ad2antrr	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ w = Y ) -> ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) = ( ( N + ( 1 / 2 ) ) / _pi ) )
590	310	fveq2d	|- ( w = Y -> ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) = ( cos ` ( ( N + ( 1 / 2 ) ) x. Y ) ) )
591	590	oveq2d	|- ( w = Y -> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) = ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. Y ) ) ) )
592		fvoveq1	|- ( w = Y -> ( cos ` ( w / 2 ) ) = ( cos ` ( Y / 2 ) ) )
593	592	oveq2d	|- ( w = Y -> ( _pi x. ( cos ` ( w / 2 ) ) ) = ( _pi x. ( cos ` ( Y / 2 ) ) ) )
594	591 593	oveq12d	|- ( w = Y -> ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) / ( _pi x. ( cos ` ( w / 2 ) ) ) ) = ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. Y ) ) ) / ( _pi x. ( cos ` ( Y / 2 ) ) ) ) )
595	594	adantl	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ w = Y ) -> ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) / ( _pi x. ( cos ` ( w / 2 ) ) ) ) = ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. Y ) ) ) / ( _pi x. ( cos ` ( Y / 2 ) ) ) ) )
596	43 45 264	adddird	|- ( ph -> ( ( N + ( 1 / 2 ) ) x. Y ) = ( ( N x. Y ) + ( ( 1 / 2 ) x. Y ) ) )
597	397 155 264 377	div32d	|- ( ph -> ( ( 1 / 2 ) x. Y ) = ( 1 x. ( Y / 2 ) ) )
598	436	mullidd	|- ( ph -> ( 1 x. ( Y / 2 ) ) = ( Y / 2 ) )
599	597 598	eqtrd	|- ( ph -> ( ( 1 / 2 ) x. Y ) = ( Y / 2 ) )
600	599	oveq2d	|- ( ph -> ( ( N x. Y ) + ( ( 1 / 2 ) x. Y ) ) = ( ( N x. Y ) + ( Y / 2 ) ) )
601	43 264	mulcld	|- ( ph -> ( N x. Y ) e. CC )
602	601 436	addcomd	|- ( ph -> ( ( N x. Y ) + ( Y / 2 ) ) = ( ( Y / 2 ) + ( N x. Y ) ) )
603	596 600 602	3eqtrd	|- ( ph -> ( ( N + ( 1 / 2 ) ) x. Y ) = ( ( Y / 2 ) + ( N x. Y ) ) )
604	603	fveq2d	|- ( ph -> ( cos ` ( ( N + ( 1 / 2 ) ) x. Y ) ) = ( cos ` ( ( Y / 2 ) + ( N x. Y ) ) ) )
605	601 158 379	divcan1d	|- ( ph -> ( ( ( N x. Y ) / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) = ( N x. Y ) )
606	605	eqcomd	|- ( ph -> ( N x. Y ) = ( ( ( N x. Y ) / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) )
607	606	oveq2d	|- ( ph -> ( ( Y / 2 ) + ( N x. Y ) ) = ( ( Y / 2 ) + ( ( ( N x. Y ) / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) ) )
608	607	fveq2d	|- ( ph -> ( cos ` ( ( Y / 2 ) + ( N x. Y ) ) ) = ( cos ` ( ( Y / 2 ) + ( ( ( N x. Y ) / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) ) ) )
609	43 264 158 379	divassd	|- ( ph -> ( ( N x. Y ) / ( 2 x. _pi ) ) = ( N x. ( Y / ( 2 x. _pi ) ) ) )
610	405 404	zmulcld	|- ( ph -> ( N x. ( Y / ( 2 x. _pi ) ) ) e. ZZ )
611	609 610	eqeltrd	|- ( ph -> ( ( N x. Y ) / ( 2 x. _pi ) ) e. ZZ )
612		cosper	|- ( ( ( Y / 2 ) e. CC /\ ( ( N x. Y ) / ( 2 x. _pi ) ) e. ZZ ) -> ( cos ` ( ( Y / 2 ) + ( ( ( N x. Y ) / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) ) ) = ( cos ` ( Y / 2 ) ) )
613	436 611 612	syl2anc	|- ( ph -> ( cos ` ( ( Y / 2 ) + ( ( ( N x. Y ) / ( 2 x. _pi ) ) x. ( 2 x. _pi ) ) ) ) = ( cos ` ( Y / 2 ) ) )
614	604 608 613	3eqtrd	|- ( ph -> ( cos ` ( ( N + ( 1 / 2 ) ) x. Y ) ) = ( cos ` ( Y / 2 ) ) )
615	614	oveq2d	|- ( ph -> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. Y ) ) ) = ( ( N + ( 1 / 2 ) ) x. ( cos ` ( Y / 2 ) ) ) )
616	615	oveq1d	|- ( ph -> ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. Y ) ) ) / ( _pi x. ( cos ` ( Y / 2 ) ) ) ) = ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( Y / 2 ) ) ) / ( _pi x. ( cos ` ( Y / 2 ) ) ) ) )
617	436	coscld	|- ( ph -> ( cos ` ( Y / 2 ) ) e. CC )
618	264 155 157 377 378	divdiv1d	|- ( ph -> ( ( Y / 2 ) / _pi ) = ( Y / ( 2 x. _pi ) ) )
619	618 404	eqeltrd	|- ( ph -> ( ( Y / 2 ) / _pi ) e. ZZ )
620	619	zred	|- ( ph -> ( ( Y / 2 ) / _pi ) e. RR )
621	620 273	ltaddrpd	|- ( ph -> ( ( Y / 2 ) / _pi ) < ( ( ( Y / 2 ) / _pi ) + ( 1 / 2 ) ) )
622		halflt1	|- ( 1 / 2 ) < 1
623	622	a1i	|- ( ph -> ( 1 / 2 ) < 1 )
624	269 268 620 623	ltadd2dd	|- ( ph -> ( ( ( Y / 2 ) / _pi ) + ( 1 / 2 ) ) < ( ( ( Y / 2 ) / _pi ) + 1 ) )
625		btwnnz	|- ( ( ( ( Y / 2 ) / _pi ) e. ZZ /\ ( ( Y / 2 ) / _pi ) < ( ( ( Y / 2 ) / _pi ) + ( 1 / 2 ) ) /\ ( ( ( Y / 2 ) / _pi ) + ( 1 / 2 ) ) < ( ( ( Y / 2 ) / _pi ) + 1 ) ) -> -. ( ( ( Y / 2 ) / _pi ) + ( 1 / 2 ) ) e. ZZ )
626	619 621 624 625	syl3anc	|- ( ph -> -. ( ( ( Y / 2 ) / _pi ) + ( 1 / 2 ) ) e. ZZ )
627		coseq0	|- ( ( Y / 2 ) e. CC -> ( ( cos ` ( Y / 2 ) ) = 0 <-> ( ( ( Y / 2 ) / _pi ) + ( 1 / 2 ) ) e. ZZ ) )
628	436 627	syl	|- ( ph -> ( ( cos ` ( Y / 2 ) ) = 0 <-> ( ( ( Y / 2 ) / _pi ) + ( 1 / 2 ) ) e. ZZ ) )
629	626 628	mtbird	|- ( ph -> -. ( cos ` ( Y / 2 ) ) = 0 )
630	629	neqned	|- ( ph -> ( cos ` ( Y / 2 ) ) =/= 0 )
631	46 157 617 378 630	divcan5rd	|- ( ph -> ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( Y / 2 ) ) ) / ( _pi x. ( cos ` ( Y / 2 ) ) ) ) = ( ( N + ( 1 / 2 ) ) / _pi ) )
632	616 631	eqtrd	|- ( ph -> ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. Y ) ) ) / ( _pi x. ( cos ` ( Y / 2 ) ) ) ) = ( ( N + ( 1 / 2 ) ) / _pi ) )
633	632	ad2antrr	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ w = Y ) -> ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. Y ) ) ) / ( _pi x. ( cos ` ( Y / 2 ) ) ) ) = ( ( N + ( 1 / 2 ) ) / _pi ) )
634	595 633	eqtr2d	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ w = Y ) -> ( ( N + ( 1 / 2 ) ) / _pi ) = ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) / ( _pi x. ( cos ` ( w / 2 ) ) ) ) )
635	578 589 634	3eqtrrd	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ w = Y ) -> ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) / ( _pi x. ( cos ` ( w / 2 ) ) ) ) = if ( w = Y , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) ` w ) ) )
636		iffalse	|- ( -. w = Y -> if ( w = Y , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) ` w ) ) = ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) ` w ) )
637	636	adantl	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> if ( w = Y , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) ` w ) ) = ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) ` w ) )
638		eqidd	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) )
639		fveq2	|- ( y = w -> ( H ` y ) = ( H ` w ) )
640		fveq2	|- ( y = w -> ( I ` y ) = ( I ` w ) )
641	639 640	oveq12d	|- ( y = w -> ( ( H ` y ) / ( I ` y ) ) = ( ( H ` w ) / ( I ` w ) ) )
642	641	adantl	|- ( ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) /\ y = w ) -> ( ( H ` y ) / ( I ` y ) ) = ( ( H ` w ) / ( I ` w ) ) )
643	110 5	fmptd	|- ( ph -> H : ( ( A (,) B ) \ { Y } ) --> CC )
644	643	ad2antrr	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> H : ( ( A (,) B ) \ { Y } ) --> CC )
645	644 324	ffvelcdmd	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( H ` w ) e. CC )
646	566	ad2antrr	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> I : ( ( A (,) B ) \ { Y } ) --> CC )
647	646 324	ffvelcdmd	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( I ` w ) e. CC )
648	6	a1i	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> I = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( _pi x. ( cos ` ( y / 2 ) ) ) ) )
649		simpr	|- ( ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) /\ y = w ) -> y = w )
650	649	fvoveq1d	|- ( ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) /\ y = w ) -> ( cos ` ( y / 2 ) ) = ( cos ` ( w / 2 ) ) )
651	650	oveq2d	|- ( ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) /\ y = w ) -> ( _pi x. ( cos ` ( y / 2 ) ) ) = ( _pi x. ( cos ` ( w / 2 ) ) ) )
652	156	a1i	|- ( w e. ( A (,) B ) -> _pi e. CC )
653	327	halfcld	|- ( w e. ( A (,) B ) -> ( w / 2 ) e. CC )
654	653	coscld	|- ( w e. ( A (,) B ) -> ( cos ` ( w / 2 ) ) e. CC )
655	652 654	mulcld	|- ( w e. ( A (,) B ) -> ( _pi x. ( cos ` ( w / 2 ) ) ) e. CC )
656	655	ad2antlr	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( _pi x. ( cos ` ( w / 2 ) ) ) e. CC )
657	648 651 324 656	fvmptd	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( I ` w ) = ( _pi x. ( cos ` ( w / 2 ) ) ) )
658	537	a1i	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( _pi e. CC /\ _pi =/= 0 ) )
659	654	ad2antlr	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( cos ` ( w / 2 ) ) e. CC )
660		simpll	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ph )
661		fvoveq1	|- ( y = w -> ( cos ` ( y / 2 ) ) = ( cos ` ( w / 2 ) ) )
662	661	neeq1d	|- ( y = w -> ( ( cos ` ( y / 2 ) ) =/= 0 <-> ( cos ` ( w / 2 ) ) =/= 0 ) )
663	228 662	imbi12d	|- ( y = w -> ( ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( cos ` ( y / 2 ) ) =/= 0 ) <-> ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( cos ` ( w / 2 ) ) =/= 0 ) ) )
664	663 11	chvarvv	|- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( cos ` ( w / 2 ) ) =/= 0 )
665	660 324 664	syl2anc	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( cos ` ( w / 2 ) ) =/= 0 )
666		mulne0	|- ( ( ( _pi e. CC /\ _pi =/= 0 ) /\ ( ( cos ` ( w / 2 ) ) e. CC /\ ( cos ` ( w / 2 ) ) =/= 0 ) ) -> ( _pi x. ( cos ` ( w / 2 ) ) ) =/= 0 )
667	658 659 665 666	syl12anc	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( _pi x. ( cos ` ( w / 2 ) ) ) =/= 0 )
668	657 667	eqnetrd	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( I ` w ) =/= 0 )
669	645 647 668	divcld	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( ( H ` w ) / ( I ` w ) ) e. CC )
670	638 642 324 669	fvmptd	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) ` w ) = ( ( H ` w ) / ( I ` w ) ) )
671	5	a1i	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> H = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
672	317	fveq2d	|- ( ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) /\ y = w ) -> ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) = ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) )
673	672	oveq2d	|- ( ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) /\ y = w ) -> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) = ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) )
674	329	coscld	|- ( ( ph /\ w e. ( A (,) B ) ) -> ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) e. CC )
675	325 674	mulcld	|- ( ( ph /\ w e. ( A (,) B ) ) -> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) e. CC )
676	675	adantr	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) e. CC )
677	671 673 324 676	fvmptd	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( H ` w ) = ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) )
678	677 657	oveq12d	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( ( H ` w ) / ( I ` w ) ) = ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) / ( _pi x. ( cos ` ( w / 2 ) ) ) ) )
679	637 670 678	3eqtrrd	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) / ( _pi x. ( cos ` ( w / 2 ) ) ) ) = if ( w = Y , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) ` w ) ) )
680	635 679	pm2.61dan	|- ( ( ph /\ w e. ( A (,) B ) ) -> ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) / ( _pi x. ( cos ` ( w / 2 ) ) ) ) = if ( w = Y , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) ` w ) ) )
681	680	mpteq2dva	|- ( ph -> ( w e. ( A (,) B ) |-> ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) / ( _pi x. ( cos ` ( w / 2 ) ) ) ) ) = ( w e. ( A (,) B ) |-> if ( w = Y , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) ` w ) ) ) )
682	576 681	eqtr2d	|- ( ph -> ( w e. ( A (,) B ) |-> if ( w = Y , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) ` w ) ) ) = L )
683	349 46 80	constcncfg	|- ( ph -> ( w e. ( A (,) B ) |-> ( N + ( 1 / 2 ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
684		cosf	|- cos : CC --> CC
685	233 49	sylan2	|- ( ( ph /\ y e. ( A (,) B ) ) -> ( ( N + ( 1 / 2 ) ) x. y ) e. CC )
686		eqid	|- ( y e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) = ( y e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. y ) )
687	685 686	fmptd	|- ( ph -> ( y e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) : ( A (,) B ) --> CC )
688		fcompt	|- ( ( cos : CC --> CC /\ ( y e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) : ( A (,) B ) --> CC ) -> ( cos o. ( y e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ) = ( w e. ( A (,) B ) |-> ( cos ` ( ( y e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) ) )
689	684 687 688	sylancr	|- ( ph -> ( cos o. ( y e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ) = ( w e. ( A (,) B ) |-> ( cos ` ( ( y e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) ) )
690		eqidd	|- ( ( ph /\ w e. ( A (,) B ) ) -> ( y e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) = ( y e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) )
691	316	adantl	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ y = w ) -> ( ( N + ( 1 / 2 ) ) x. y ) = ( ( N + ( 1 / 2 ) ) x. w ) )
692		simpr	|- ( ( ph /\ w e. ( A (,) B ) ) -> w e. ( A (,) B ) )
693	690 691 692 329	fvmptd	|- ( ( ph /\ w e. ( A (,) B ) ) -> ( ( y e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) = ( ( N + ( 1 / 2 ) ) x. w ) )
694	693	fveq2d	|- ( ( ph /\ w e. ( A (,) B ) ) -> ( cos ` ( ( y e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) = ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) )
695	694	mpteq2dva	|- ( ph -> ( w e. ( A (,) B ) |-> ( cos ` ( ( y e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) ) = ( w e. ( A (,) B ) |-> ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) )
696	689 695	eqtr2d	|- ( ph -> ( w e. ( A (,) B ) |-> ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) = ( cos o. ( y e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
697	349 46 80	constcncfg	|- ( ph -> ( y e. ( A (,) B ) |-> ( N + ( 1 / 2 ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
698	349 80	idcncfg	|- ( ph -> ( y e. ( A (,) B ) |-> y ) e. ( ( A (,) B ) -cn-> CC ) )
699	697 698	mulcncf	|- ( ph -> ( y e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) e. ( ( A (,) B ) -cn-> CC ) )
700		coscn	|- cos e. ( CC -cn-> CC )
701	700	a1i	|- ( ph -> cos e. ( CC -cn-> CC ) )
702	699 701	cncfco	|- ( ph -> ( cos o. ( y e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
703	696 702	eqeltrd	|- ( ph -> ( w e. ( A (,) B ) |-> ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
704	683 703	mulcncf	|- ( ph -> ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
705		eqid	|- ( w e. ( A (,) B ) |-> ( _pi x. ( cos ` ( w / 2 ) ) ) ) = ( w e. ( A (,) B ) |-> ( _pi x. ( cos ` ( w / 2 ) ) ) )
706	349 157 80	constcncfg	|- ( ph -> ( w e. ( A (,) B ) |-> _pi ) e. ( ( A (,) B ) -cn-> CC ) )
707		2cnd	|- ( ( ph /\ w e. ( A (,) B ) ) -> 2 e. CC )
708	135	a1i	|- ( ( ph /\ w e. ( A (,) B ) ) -> 2 =/= 0 )
709	328 707 708	divrecd	|- ( ( ph /\ w e. ( A (,) B ) ) -> ( w / 2 ) = ( w x. ( 1 / 2 ) ) )
710	709	mpteq2dva	|- ( ph -> ( w e. ( A (,) B ) |-> ( w / 2 ) ) = ( w e. ( A (,) B ) |-> ( w x. ( 1 / 2 ) ) ) )
711		eqid	|- ( w e. CC |-> ( w x. ( 1 / 2 ) ) ) = ( w e. CC |-> ( w x. ( 1 / 2 ) ) )
712		cncfmptid	|- ( ( CC C_ CC /\ CC C_ CC ) -> ( w e. CC |-> w ) e. ( CC -cn-> CC ) )
713	79 79 712	mp2an	|- ( w e. CC |-> w ) e. ( CC -cn-> CC )
714	713	a1i	|- ( ph -> ( w e. CC |-> w ) e. ( CC -cn-> CC ) )
715	79	a1i	|- ( ( 1 / 2 ) e. CC -> CC C_ CC )
716		id	|- ( ( 1 / 2 ) e. CC -> ( 1 / 2 ) e. CC )
717	715 716 715	constcncfg	|- ( ( 1 / 2 ) e. CC -> ( w e. CC |-> ( 1 / 2 ) ) e. ( CC -cn-> CC ) )
718	44 717	mp1i	|- ( ph -> ( w e. CC |-> ( 1 / 2 ) ) e. ( CC -cn-> CC ) )
719	714 718	mulcncf	|- ( ph -> ( w e. CC |-> ( w x. ( 1 / 2 ) ) ) e. ( CC -cn-> CC ) )
720	709 462	eqeltrrd	|- ( ( ph /\ w e. ( A (,) B ) ) -> ( w x. ( 1 / 2 ) ) e. CC )
721	711 719 349 80 720	cncfmptssg	|- ( ph -> ( w e. ( A (,) B ) |-> ( w x. ( 1 / 2 ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
722	710 721	eqeltrd	|- ( ph -> ( w e. ( A (,) B ) |-> ( w / 2 ) ) e. ( ( A (,) B ) -cn-> CC ) )
723	701 722	cncfmpt1f	|- ( ph -> ( w e. ( A (,) B ) |-> ( cos ` ( w / 2 ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
724	706 723	mulcncf	|- ( ph -> ( w e. ( A (,) B ) |-> ( _pi x. ( cos ` ( w / 2 ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
725		ssid	|- ( A (,) B ) C_ ( A (,) B )
726	725	a1i	|- ( ph -> ( A (,) B ) C_ ( A (,) B ) )
727		difssd	|- ( ph -> ( CC \ { 0 } ) C_ CC )
728	655	adantl	|- ( ( ph /\ w e. ( A (,) B ) ) -> ( _pi x. ( cos ` ( w / 2 ) ) ) e. CC )
729	156	a1i	|- ( ( ph /\ w e. ( A (,) B ) ) -> _pi e. CC )
730	654	adantl	|- ( ( ph /\ w e. ( A (,) B ) ) -> ( cos ` ( w / 2 ) ) e. CC )
731	240	a1i	|- ( ( ph /\ w e. ( A (,) B ) ) -> _pi =/= 0 )
732	592	adantl	|- ( ( ph /\ w = Y ) -> ( cos ` ( w / 2 ) ) = ( cos ` ( Y / 2 ) ) )
733	630	adantr	|- ( ( ph /\ w = Y ) -> ( cos ` ( Y / 2 ) ) =/= 0 )
734	732 733	eqnetrd	|- ( ( ph /\ w = Y ) -> ( cos ` ( w / 2 ) ) =/= 0 )
735	734	adantlr	|- ( ( ( ph /\ w e. ( A (,) B ) ) /\ w = Y ) -> ( cos ` ( w / 2 ) ) =/= 0 )
736	735 665	pm2.61dan	|- ( ( ph /\ w e. ( A (,) B ) ) -> ( cos ` ( w / 2 ) ) =/= 0 )
737	729 730 731 736	mulne0d	|- ( ( ph /\ w e. ( A (,) B ) ) -> ( _pi x. ( cos ` ( w / 2 ) ) ) =/= 0 )
738	737	neneqd	|- ( ( ph /\ w e. ( A (,) B ) ) -> -. ( _pi x. ( cos ` ( w / 2 ) ) ) = 0 )
739		elsng	|- ( ( _pi x. ( cos ` ( w / 2 ) ) ) e. CC -> ( ( _pi x. ( cos ` ( w / 2 ) ) ) e. { 0 } <-> ( _pi x. ( cos ` ( w / 2 ) ) ) = 0 ) )
740	728 739	syl	|- ( ( ph /\ w e. ( A (,) B ) ) -> ( ( _pi x. ( cos ` ( w / 2 ) ) ) e. { 0 } <-> ( _pi x. ( cos ` ( w / 2 ) ) ) = 0 ) )
741	738 740	mtbird	|- ( ( ph /\ w e. ( A (,) B ) ) -> -. ( _pi x. ( cos ` ( w / 2 ) ) ) e. { 0 } )
742	728 741	eldifd	|- ( ( ph /\ w e. ( A (,) B ) ) -> ( _pi x. ( cos ` ( w / 2 ) ) ) e. ( CC \ { 0 } ) )
743	705 724 726 727 742	cncfmptssg	|- ( ph -> ( w e. ( A (,) B ) |-> ( _pi x. ( cos ` ( w / 2 ) ) ) ) e. ( ( A (,) B ) -cn-> ( CC \ { 0 } ) ) )
744	704 743	divcncf	|- ( ph -> ( w e. ( A (,) B ) |-> ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) / ( _pi x. ( cos ` ( w / 2 ) ) ) ) ) e. ( ( A (,) B ) -cn-> CC ) )
745	744 487	eleqtrd	|- ( ph -> ( w e. ( A (,) B ) |-> ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. w ) ) ) / ( _pi x. ( cos ` ( w / 2 ) ) ) ) ) e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) )
746	576 745	eqeltrd	|- ( ph -> L e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) )
747		cncnp	|- ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) e. ( TopOn ` ( A (,) B ) ) /\ ( TopOpen ` CCfld ) e. ( TopOn ` CC ) ) -> ( L e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) <-> ( L : ( A (,) B ) --> CC /\ A. y e. ( A (,) B ) L e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) ) ) )
748	355 353 747	sylancl	|- ( ph -> ( L e. ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) Cn ( TopOpen ` CCfld ) ) <-> ( L : ( A (,) B ) --> CC /\ A. y e. ( A (,) B ) L e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) ) ) )
749	746 748	mpbid	|- ( ph -> ( L : ( A (,) B ) --> CC /\ A. y e. ( A (,) B ) L e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) ) )
750	749	simprd	|- ( ph -> A. y e. ( A (,) B ) L e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) )
751	360	eleq2d	|- ( y = Y -> ( L e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) <-> L e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) ) )
752	751	rspccva	|- ( ( A. y e. ( A (,) B ) L e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` y ) /\ Y e. ( A (,) B ) ) -> L e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) )
753	750 9 752	syl2anc	|- ( ph -> L e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) )
754	682 753	eqeltrd	|- ( ph -> ( w e. ( A (,) B ) |-> if ( w = Y , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) ` w ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( A (,) B ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) )
755	307	mpteq1d	|- ( ph -> ( w e. ( ( ( A (,) B ) \ { Y } ) u. { Y } ) |-> if ( w = Y , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) ` w ) ) ) = ( w e. ( A (,) B ) |-> if ( w = Y , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) ` w ) ) ) )
756	754 755 500	3eltr4d	|- ( ph -> ( w e. ( ( ( A (,) B ) \ { Y } ) u. { Y } ) |-> if ( w = Y , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) ` w ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) )
757		eqid	|- ( w e. ( ( ( A (,) B ) \ { Y } ) u. { Y } ) |-> if ( w = Y , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) ` w ) ) ) = ( w e. ( ( ( A (,) B ) \ { Y } ) u. { Y } ) |-> if ( w = Y , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) ` w ) ) )
758	5	fvmpt2	|- ( ( y e. ( ( A (,) B ) \ { Y } ) /\ ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) e. CC ) -> ( H ` y ) = ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
759	557 110 758	syl2anc	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( H ` y ) = ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
760	759 559	oveq12d	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( H ` y ) / ( I ` y ) ) = ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) / ( _pi x. ( cos ` ( y / 2 ) ) ) ) )
761	110 203 562	divcld	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) / ( _pi x. ( cos ` ( y / 2 ) ) ) ) e. CC )
762	760 761	eqeltrd	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( H ` y ) / ( I ` y ) ) e. CC )
763		eqid	|- ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) )
764	762 763	fmptd	|- ( ph -> ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) : ( ( A (,) B ) \ { Y } ) --> CC )
765	371 56 757 764 374 264	ellimc	|- ( ph -> ( ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) e. ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) limCC Y ) <-> ( w e. ( ( ( A (,) B ) \ { Y } ) u. { Y } ) |-> if ( w = Y , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) ` w ) ) ) e. ( ( ( ( TopOpen ` CCfld ) |`t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) CnP ( TopOpen ` CCfld ) ) ` Y ) ) )
766	756 765	mpbird	|- ( ph -> ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) e. ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) limCC Y ) )
767	107	eqcomd	|- ( ph -> H = ( RR _D F ) )
768	767	fveq1d	|- ( ph -> ( H ` y ) = ( ( RR _D F ) ` y ) )
769	201	eqcomd	|- ( ph -> I = ( RR _D G ) )
770	769	fveq1d	|- ( ph -> ( I ` y ) = ( ( RR _D G ) ` y ) )
771	768 770	oveq12d	|- ( ph -> ( ( H ` y ) / ( I ` y ) ) = ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) )
772	771	mpteq2dv	|- ( ph -> ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) ) )
773	772	oveq1d	|- ( ph -> ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( H ` y ) / ( I ` y ) ) ) limCC Y ) = ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) ) limCC Y ) )
774	766 773	eleqtrd	|- ( ph -> ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) e. ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) ) limCC Y ) )
775	575 774	eqeltrd	|- ( ph -> if ( ( Y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. Y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( Y / 2 ) ) ) ) ) e. ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) ) limCC Y ) )
776	574 775	eqeltrd	|- ( ph -> ( ( D ` N ) ` Y ) e. ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( ( RR _D F ) ` y ) / ( ( RR _D G ) ` y ) ) ) limCC Y ) )
777	15 24 30 32 9 33 114 207 431 506 556 572 776	lhop	|- ( ph -> ( ( D ` N ) ` Y ) e. ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( F ` y ) / ( G ` y ) ) ) limCC Y ) )
778	1	dirkerval	|- ( N e. NN -> ( D ` N ) = ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
779	8 778	syl	|- ( ph -> ( D ` N ) = ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
780	779	reseq1d	|- ( ph -> ( ( D ` N ) |` ( ( A (,) B ) \ { Y } ) ) = ( ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) |` ( ( A (,) B ) \ { Y } ) ) )
781	15	resmptd	|- ( ph -> ( ( y e. RR |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) |` ( ( A (,) B ) \ { Y } ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) )
782	257	iffalsed	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) )
783	23	recnd	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) e. CC )
784	2	fvmpt2	|- ( ( y e. ( ( A (,) B ) \ { Y } ) /\ ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) e. CC ) -> ( F ` y ) = ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) )
785	557 783 784	syl2anc	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( F ` y ) = ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) )
786	557 503 525	syl2anc	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( G ` y ) = ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) )
787	785 786	oveq12d	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( F ` y ) / ( G ` y ) ) = ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) )
788	782 787	eqtr4d	|- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) = ( ( F ` y ) / ( G ` y ) ) )
789	788	mpteq2dva	|- ( ph -> ( y e. ( ( A (,) B ) \ { Y } ) |-> if ( ( y mod ( 2 x. _pi ) ) = 0 , ( ( ( 2 x. N ) + 1 ) / ( 2 x. _pi ) ) , ( ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) / ( ( 2 x. _pi ) x. ( sin ` ( y / 2 ) ) ) ) ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( F ` y ) / ( G ` y ) ) ) )
790	780 781 789	3eqtrrd	|- ( ph -> ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( F ` y ) / ( G ` y ) ) ) = ( ( D ` N ) |` ( ( A (,) B ) \ { Y } ) ) )
791	790	oveq1d	|- ( ph -> ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( F ` y ) / ( G ` y ) ) ) limCC Y ) = ( ( ( D ` N ) |` ( ( A (,) B ) \ { Y } ) ) limCC Y ) )
792	777 791	eleqtrd	|- ( ph -> ( ( D ` N ) ` Y ) e. ( ( ( D ` N ) |` ( ( A (,) B ) \ { Y } ) ) limCC Y ) )