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

Metamath Proof Explorer

Theorem dirkercncflem2

Proof