Theorem dirkercncflem2 37525

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

Hypotheses

Ref	Expression
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

Ref	Expression
dirkercncflem2	|- ( ph -> ( ( D ` N ) ` Y ) e. ( ( ( D ` N ) |` ( ( A (,) B ) \ { Y } ) ) lim CC Y ) )

Distinct variable groups:   w, A, y   w, B, y   y, D   w, F, y   w, G, y   w, H, y   w, I, y   y, L   w, N, y   w, Y, y   y, n   ph, w, y

Allowed substitution hints:   ph( n)   A( n)   B( n)   D( w, n)   F( n)   G( n)   H( n)   I( n)   L( w, n)   N( n)   Y( n)

Proof of Theorem dirkercncflem2

Step	Hyp	Ref	Expression
1		difss 3598	. . . . 5 |- ( ( A (,) B ) \ { Y } ) C_ ( A (,) B )
2		ioossre 11696	. . . . 5 |- ( A (,) B ) C_ RR
3	1, 2	sstri 3479	. . . 4 |- ( ( A (,) B ) \ { Y } ) C_ RR
4	3	a1i 11	. . 3 |- ( ph -> ( ( A (,) B ) \ { Y } ) C_ RR )
5		dirkercncflem2.n	. . . . . . . . 9 |- ( ph -> N e. NN )
6	5	adantr 466	. . . . . . . 8 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> N e. NN )
7	6	nnred 10624	. . . . . . 7 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> N e. RR )
8		halfre 10828	. . . . . . . 8 |- ( 1 / 2 ) e. RR
9	8	a1i 11	. . . . . . 7 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( 1 / 2 ) e. RR )
10	7, 9	readdcld 9669	. . . . . 6 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( N + ( 1 / 2 ) ) e. RR )
11	4	sselda 3470	. . . . . 6 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> y e. RR )
12	10, 11	remulcld 9670	. . . . 5 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. y ) e. RR )
13	12	resincld 14175	. . . 4 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) e. RR )
14		dirkercncflem2.f	. . . 4 |- F = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) )
15	13, 14	fmptd 6061	. . 3 |- ( ph -> F : ( ( A (,) B ) \ { Y } ) --> RR )
16		2re 10679	. . . . . . 7 |- 2 e. RR
17		pire 23269	. . . . . . 7 |- pi e. RR
18	16, 17	remulcli 9656	. . . . . 6 |- ( 2 x. pi ) e. RR
19	18	a1i 11	. . . . 5 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( 2 x. pi ) e. RR )
20	11	rehalfcld 10859	. . . . . 6 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( y / 2 ) e. RR )
21	20	resincld 14175	. . . . 5 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( sin ` ( y / 2 ) ) e. RR )
22	19, 21	remulcld 9670	. . . 4 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) e. RR )
23		dirkercncflem2.g	. . . 4 |- G = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) )
24	22, 23	fmptd 6061	. . 3 |- ( ph -> G : ( ( A (,) B ) \ { Y } ) --> RR )
25		iooretop 21688	. . . 4 |- ( A (,) B ) e. ( topGen ` ran (,) )
26	25	a1i 11	. . 3 |- ( ph -> ( A (,) B ) e. ( topGen ` ran (,) ) )
27		dirkercncflem2.y	. . 3 |- ( ph -> Y e. ( A (,) B ) )
28		eqid 2429	. . 3 |- ( ( A (,) B ) \ { Y } ) = ( ( A (,) B ) \ { Y } )
29	14	a1i 11	. . . . . . . 8 |- ( ph -> F = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
30	29	oveq2d 6321	. . . . . . 7 |- ( ph -> ( RR _D F ) = ( RR _D ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
31		resmpt 5174	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) ) )
32	3, 31	ax-mp 5	. . . . . . . . . . 11 |- ( ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` ( ( A (,) B ) \ { Y } ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) )
33	32	eqcomi 2442	. . . . . . . . . 10 |- ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) = ( ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` ( ( A (,) B ) \ { Y } ) )
34	33	a1i 11	. . . . . . . . 9 |- ( ph -> ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) = ( ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` ( ( A (,) B ) \ { Y } ) ) )
35	34	oveq2d 6321	. . . . . . . 8 |- ( 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 } ) ) ) )
36		ax-resscn 9595	. . . . . . . . . 10 |- RR C_ CC
37	36	a1i 11	. . . . . . . . 9 |- ( ph -> RR C_ CC )
38	5	nncnd 10625	. . . . . . . . . . . . . 14 |- ( ph -> N e. CC )
39		halfcn 10829	. . . . . . . . . . . . . . 15 |- ( 1 / 2 ) e. CC
40	39	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 / 2 ) e. CC )
41	38, 40	addcld 9661	. . . . . . . . . . . . 13 |- ( ph -> ( N + ( 1 / 2 ) ) e. CC )
42	41	adantr 466	. . . . . . . . . . . 12 |- ( ( ph /\ y e. RR ) -> ( N + ( 1 / 2 ) ) e. CC )
43	37	sselda 3470	. . . . . . . . . . . 12 |- ( ( ph /\ y e. RR ) -> y e. CC )
44	42, 43	mulcld 9662	. . . . . . . . . . 11 |- ( ( ph /\ y e. RR ) -> ( ( N + ( 1 / 2 ) ) x. y ) e. CC )
45	44	sincld 14162	. . . . . . . . . 10 |- ( ( ph /\ y e. RR ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) e. CC )
46		eqid 2429	. . . . . . . . . 10 |- ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) = ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) )
47	45, 46	fmptd 6061	. . . . . . . . 9 |- ( ph -> ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) : RR --> CC )
48		ssid 3489	. . . . . . . . . . 11 |- RR C_ RR
49	48, 3	pm3.2i 456	. . . . . . . . . 10 |- ( RR C_ RR /\ ( ( A (,) B ) \ { Y } ) C_ RR )
50	49	a1i 11	. . . . . . . . 9 |- ( ph -> ( RR C_ RR /\ ( ( A (,) B ) \ { Y } ) C_ RR ) )
51		eqid 2429	. . . . . . . . . 10 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
52	51	tgioo2 21723	. . . . . . . . . 10 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
53	51, 52	dvres 22734	. . . . . . . . 9 |- ( ( ( 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 } ) ) ) )
54	37, 47, 50, 53	syl21anc 1263	. . . . . . . 8 |- ( 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 } ) ) ) )
55		retop 21684	. . . . . . . . . . 11 |- ( topGen ` ran (,) ) e. Top
56		rehaus 21719	. . . . . . . . . . . . 13 |- ( topGen ` ran (,) ) e. Haus
57	2, 27	sseldi 3468	. . . . . . . . . . . . 13 |- ( ph -> Y e. RR )
58		uniretop 21685	. . . . . . . . . . . . . 14 |- RR = U. ( topGen ` ran (,) )
59	58	sncld 20309	. . . . . . . . . . . . 13 |- ( ( ( topGen ` ran (,) ) e. Haus /\ Y e. RR ) -> { Y } e. ( Clsd ` ( topGen ` ran (,) ) ) )
60	56, 57, 59	sylancr 667	. . . . . . . . . . . 12 |- ( ph -> { Y } e. ( Clsd ` ( topGen ` ran (,) ) ) )
61	58	difopn 19971	. . . . . . . . . . . 12 |- ( ( ( A (,) B ) e. ( topGen ` ran (,) ) /\ { Y } e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( ( A (,) B ) \ { Y } ) e. ( topGen ` ran (,) ) )
62	25, 60, 61	sylancr 667	. . . . . . . . . . 11 |- ( ph -> ( ( A (,) B ) \ { Y } ) e. ( topGen ` ran (,) ) )
63		isopn3i 20020	. . . . . . . . . . 11 |- ( ( ( topGen ` ran (,) ) e. Top /\ ( ( A (,) B ) \ { Y } ) e. ( topGen ` ran (,) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) \ { Y } ) ) = ( ( A (,) B ) \ { Y } ) )
64	55, 62, 63	sylancr 667	. . . . . . . . . 10 |- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) \ { Y } ) ) = ( ( A (,) B ) \ { Y } ) )
65	64	reseq2d 5125	. . . . . . . . 9 |- ( 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 } ) ) )
66		reelprrecn 9630	. . . . . . . . . . . . 13 |- RR e. { RR , CC }
67	66	a1i 11	. . . . . . . . . . . 12 |- ( ph -> RR e. { RR , CC } )
68	41	adantr 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. CC ) -> ( N + ( 1 / 2 ) ) e. CC )
69		simpr 462	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. CC ) -> y e. CC )
70	68, 69	mulcld 9662	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. CC ) -> ( ( N + ( 1 / 2 ) ) x. y ) e. CC )
71	70	sincld 14162	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. CC ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) e. CC )
72		eqid 2429	. . . . . . . . . . . . 13 |- ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) = ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) )
73	71, 72	fmptd 6061	. . . . . . . . . . . 12 |- ( ph -> ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) : CC --> CC )
74		ssid 3489	. . . . . . . . . . . . 13 |- CC C_ CC
75	74	a1i 11	. . . . . . . . . . . 12 |- ( ph -> CC C_ CC )
76		dvsinax 37345	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) ) ) )
77	41, 76	syl 17	. . . . . . . . . . . . . . 15 |- ( 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 ) ) ) ) )
78	77	dmeqd 5057	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) ) )
79		eqid 2429	. . . . . . . . . . . . . . 15 |- ( 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 ) ) ) )
80	70	coscld 14163	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. CC ) -> ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) e. CC )
81	68, 80	mulcld 9662	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. CC ) -> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) e. CC )
82	79, 81	dmmptd 5726	. . . . . . . . . . . . . 14 |- ( ph -> dom ( y e. CC |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = CC )
83	78, 82	eqtrd 2470	. . . . . . . . . . . . 13 |- ( ph -> dom ( CC _D ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = CC )
84	36, 83	syl5sseqr 3519	. . . . . . . . . . . 12 |- ( ph -> RR C_ dom ( CC _D ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
85		dvres3 22736	. . . . . . . . . . . 12 |- ( ( ( 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 ) )
86	67, 73, 75, 84, 85	syl22anc 1265	. . . . . . . . . . 11 |- ( 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 ) )
87		resmpt 5174	. . . . . . . . . . . . 13 |- ( RR C_ CC -> ( ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` RR ) = ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
88	36, 87	mp1i 13	. . . . . . . . . . . 12 |- ( ph -> ( ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` RR ) = ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
89	88	oveq2d 6321	. . . . . . . . . . 11 |- ( ph -> ( RR _D ( ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` RR ) ) = ( RR _D ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
90	77	reseq1d 5124	. . . . . . . . . . . 12 |- ( 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 ) )
91		resmpt 5174	. . . . . . . . . . . . 13 |- ( 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 ) ) ) ) )
92	36, 91	ax-mp 5	. . . . . . . . . . . 12 |- ( ( 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 ) ) ) )
93	90, 92	syl6eq 2486	. . . . . . . . . . 11 |- ( 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 ) ) ) ) )
94	86, 89, 93	3eqtr3d 2478	. . . . . . . . . 10 |- ( 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 ) ) ) ) )
95	94	reseq1d 5124	. . . . . . . . 9 |- ( 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 } ) ) )
96		resmpt 5174	. . . . . . . . . 10 |- ( ( ( 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 ) ) ) ) )
97	3, 96	mp1i 13	. . . . . . . . 9 |- ( 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 ) ) ) ) )
98	65, 95, 97	3eqtrd 2474	. . . . . . . 8 |- ( 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 ) ) ) ) )
99	35, 54, 98	3eqtrd 2474	. . . . . . 7 |- ( 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 ) ) ) ) )
100		dirkercncflem2.h	. . . . . . . . 9 |- H = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
101	100	a1i 11	. . . . . . . 8 |- ( ph -> H = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
102	101	eqcomd 2437	. . . . . . 7 |- ( ph -> ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = H )
103	30, 99, 102	3eqtrd 2474	. . . . . 6 |- ( ph -> ( RR _D F ) = H )
104	103	dmeqd 5057	. . . . 5 |- ( ph -> dom ( RR _D F ) = dom H )
105	11	recnd 9668	. . . . . . 7 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> y e. CC )
106	105, 81	syldan 472	. . . . . 6 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) e. CC )
107	100, 106	dmmptd 5726	. . . . 5 |- ( ph -> dom H = ( ( A (,) B ) \ { Y } ) )
108	104, 107	eqtr2d 2471	. . . 4 |- ( ph -> ( ( A (,) B ) \ { Y } ) = dom ( RR _D F ) )
109		eqimss 3522	. . . 4 |- ( ( ( A (,) B ) \ { Y } ) = dom ( RR _D F ) -> ( ( A (,) B ) \ { Y } ) C_ dom ( RR _D F ) )
110	108, 109	syl 17	. . 3 |- ( ph -> ( ( A (,) B ) \ { Y } ) C_ dom ( RR _D F ) )
111		dirkercncflem2.i	. . . . . . . 8 |- I = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( pi x. ( cos ` ( y / 2 ) ) ) )
112	111	a1i 11	. . . . . . 7 |- ( ph -> I = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) )
113		resmpt 5174	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) ) ) )
114	3, 113	ax-mp 5	. . . . . . . . . . . 12 |- ( ( 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 ) ) ) )
115	114	eqcomi 2442	. . . . . . . . . . 11 |- ( 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 } ) )
116	115	oveq2i 6316	. . . . . . . . . 10 |- ( 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 } ) ) )
117	116	a1i 11	. . . . . . . . 9 |- ( 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 } ) ) ) )
118		2cn 10680	. . . . . . . . . . . . . 14 |- 2 e. CC
119		picn 23270	. . . . . . . . . . . . . 14 |- pi e. CC
120	118, 119	mulcli 9647	. . . . . . . . . . . . 13 |- ( 2 x. pi ) e. CC
121	120	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ y e. RR ) -> ( 2 x. pi ) e. CC )
122	43	halfcld 10857	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. RR ) -> ( y / 2 ) e. CC )
123	122	sincld 14162	. . . . . . . . . . . 12 |- ( ( ph /\ y e. RR ) -> ( sin ` ( y / 2 ) ) e. CC )
124	121, 123	mulcld 9662	. . . . . . . . . . 11 |- ( ( ph /\ y e. RR ) -> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) e. CC )
125		eqid 2429	. . . . . . . . . . 11 |- ( y e. RR |-> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) = ( y e. RR |-> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) )
126	124, 125	fmptd 6061	. . . . . . . . . 10 |- ( ph -> ( y e. RR |-> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) : RR --> CC )
127	51, 52	dvres 22734	. . . . . . . . . 10 |- ( ( ( 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 } ) ) ) )
128	37, 126, 50, 127	syl21anc 1263	. . . . . . . . 9 |- ( 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 } ) ) ) )
129	64	reseq2d 5125	. . . . . . . . . 10 |- ( 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 } ) ) )
130	36	sseli 3466	. . . . . . . . . . . . . . . 16 |- ( y e. RR -> y e. CC )
131		1cnd 9658	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. CC -> 1 e. CC )
132		2cnd 10682	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. CC -> 2 e. CC )
133		id 23	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. CC -> y e. CC )
134		2ne0 10702	. . . . . . . . . . . . . . . . . . . . . 22 |- 2 =/= 0
135	134	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. CC -> 2 =/= 0 )
136	131, 132, 133, 135	div13d 10406	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. CC -> ( ( 1 / 2 ) x. y ) = ( ( y / 2 ) x. 1 ) )
137		halfcl 10838	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. CC -> ( y / 2 ) e. CC )
138	137	mulid1d 9659	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. CC -> ( ( y / 2 ) x. 1 ) = ( y / 2 ) )
139	136, 138	eqtrd 2470	. . . . . . . . . . . . . . . . . . 19 |- ( y e. CC -> ( ( 1 / 2 ) x. y ) = ( y / 2 ) )
140	139	fveq2d 5885	. . . . . . . . . . . . . . . . . 18 |- ( y e. CC -> ( sin ` ( ( 1 / 2 ) x. y ) ) = ( sin ` ( y / 2 ) ) )
141	140	oveq2d 6321	. . . . . . . . . . . . . . . . 17 |- ( y e. CC -> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) = ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) )
142	141	eqcomd 2437	. . . . . . . . . . . . . . . 16 |- ( y e. CC -> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) = ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) )
143	130, 142	syl 17	. . . . . . . . . . . . . . 15 |- ( y e. RR -> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) = ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) )
144	143	adantl 467	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. RR ) -> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) = ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) )
145	144	mpteq2dva 4512	. . . . . . . . . . . . 13 |- ( ph -> ( y e. RR |-> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) = ( y e. RR |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) )
146	145	oveq2d 6321	. . . . . . . . . . . 12 |- ( 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 ) ) ) ) ) )
147	120	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. CC ) -> ( 2 x. pi ) e. CC )
148	39	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ y e. CC ) -> ( 1 / 2 ) e. CC )
149	148, 69	mulcld 9662	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. CC ) -> ( ( 1 / 2 ) x. y ) e. CC )
150	149	sincld 14162	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. CC ) -> ( sin ` ( ( 1 / 2 ) x. y ) ) e. CC )
151	147, 150	mulcld 9662	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. CC ) -> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) e. CC )
152		eqid 2429	. . . . . . . . . . . . . . . 16 |- ( y e. CC |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) = ( y e. CC |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) )
153	151, 152	fmptd 6061	. . . . . . . . . . . . . . 15 |- ( ph -> ( y e. CC |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) : CC --> CC )
154		2cnd 10682	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> 2 e. CC )
155	119	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> pi e. CC )
156	154, 155	mulcld 9662	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 2 x. pi ) e. CC )
157		dvasinbx 37354	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 ) ) ) ) )
158	156, 39, 157	sylancl 666	. . . . . . . . . . . . . . . . . . 19 |- ( 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 ) ) ) ) )
159		2cnd 10682	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ y e. CC ) -> 2 e. CC )
160	119	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ y e. CC ) -> pi e. CC )
161	159, 160, 148	mul32d 9842	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ y e. CC ) -> ( ( 2 x. pi ) x. ( 1 / 2 ) ) = ( ( 2 x. ( 1 / 2 ) ) x. pi ) )
162	134	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ y e. CC ) -> 2 =/= 0 )
163	159, 162	recidd 10377	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ y e. CC ) -> ( 2 x. ( 1 / 2 ) ) = 1 )
164	163	oveq1d 6320	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ y e. CC ) -> ( ( 2 x. ( 1 / 2 ) ) x. pi ) = ( 1 x. pi ) )
165	160	mulid2d 9660	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ y e. CC ) -> ( 1 x. pi ) = pi )
166	161, 164, 165	3eqtrd 2474	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ y e. CC ) -> ( ( 2 x. pi ) x. ( 1 / 2 ) ) = pi )
167	139	fveq2d 5885	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. CC -> ( cos ` ( ( 1 / 2 ) x. y ) ) = ( cos ` ( y / 2 ) ) )
168	167	adantl 467	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ y e. CC ) -> ( cos ` ( ( 1 / 2 ) x. y ) ) = ( cos ` ( y / 2 ) ) )
169	166, 168	oveq12d 6323	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ y e. CC ) -> ( ( ( 2 x. pi ) x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. y ) ) ) = ( pi x. ( cos ` ( y / 2 ) ) ) )
170	169	mpteq2dva 4512	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( y e. CC |-> ( ( ( 2 x. pi ) x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. y ) ) ) ) = ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) )
171	158, 170	eqtrd 2470	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( CC _D ( y e. CC |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) = ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) )
172	171	dmeqd 5057	. . . . . . . . . . . . . . . . 17 |- ( 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 ) ) ) ) )
173		eqid 2429	. . . . . . . . . . . . . . . . . 18 |- ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) = ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) )
174	69	halfcld 10857	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ y e. CC ) -> ( y / 2 ) e. CC )
175	174	coscld 14163	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ y e. CC ) -> ( cos ` ( y / 2 ) ) e. CC )
176	160, 175	mulcld 9662	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. CC ) -> ( pi x. ( cos ` ( y / 2 ) ) ) e. CC )
177	173, 176	dmmptd 5726	. . . . . . . . . . . . . . . . 17 |- ( ph -> dom ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) = CC )
178	172, 177	eqtrd 2470	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( CC _D ( y e. CC |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) = CC )
179	36, 178	syl5sseqr 3519	. . . . . . . . . . . . . . 15 |- ( ph -> RR C_ dom ( CC _D ( y e. CC |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) )
180		dvres3 22736	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) )
181	67, 153, 75, 179, 180	syl22anc 1265	. . . . . . . . . . . . . 14 |- ( 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 ) )
182		resmpt 5174	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) ) )
183	36, 182	mp1i 13	. . . . . . . . . . . . . . 15 |- ( 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 ) ) ) ) )
184	183	oveq2d 6321	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) ) ) )
185	171	reseq1d 5124	. . . . . . . . . . . . . 14 |- ( 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 ) )
186	181, 184, 185	3eqtr3d 2478	. . . . . . . . . . . . 13 |- ( ph -> ( RR _D ( y e. RR |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) = ( ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) |` RR ) )
187		resmpt 5174	. . . . . . . . . . . . . 14 |- ( RR C_ CC -> ( ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) |` RR ) = ( y e. RR |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) )
188	36, 187	ax-mp 5	. . . . . . . . . . . . 13 |- ( ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) |` RR ) = ( y e. RR |-> ( pi x. ( cos ` ( y / 2 ) ) ) )
189	186, 188	syl6eq 2486	. . . . . . . . . . . 12 |- ( ph -> ( RR _D ( y e. RR |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) = ( y e. RR |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) )
190	146, 189	eqtrd 2470	. . . . . . . . . . 11 |- ( ph -> ( RR _D ( y e. RR |-> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) = ( y e. RR |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) )
191	190	reseq1d 5124	. . . . . . . . . 10 |- ( 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 } ) ) )
192	4	resmptd 5176	. . . . . . . . . 10 |- ( ph -> ( ( y e. RR |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) |` ( ( A (,) B ) \ { Y } ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) )
193	129, 191, 192	3eqtrd 2474	. . . . . . . . 9 |- ( 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 ) ) ) ) )
194	117, 128, 193	3eqtrd 2474	. . . . . . . 8 |- ( 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 ) ) ) ) )
195	194	eqcomd 2437	. . . . . . 7 |- ( 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 ) ) ) ) ) )
196	23	a1i 11	. . . . . . . . 9 |- ( ph -> G = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) )
197	196	oveq2d 6321	. . . . . . . 8 |- ( ph -> ( RR _D G ) = ( RR _D ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) )
198	197	eqcomd 2437	. . . . . . 7 |- ( ph -> ( RR _D ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) = ( RR _D G ) )
199	112, 195, 198	3eqtrrd 2475	. . . . . 6 |- ( ph -> ( RR _D G ) = I )
200	199	dmeqd 5057	. . . . 5 |- ( ph -> dom ( RR _D G ) = dom I )
201	105, 176	syldan 472	. . . . . 6 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( pi x. ( cos ` ( y / 2 ) ) ) e. CC )
202	111, 201	dmmptd 5726	. . . . 5 |- ( ph -> dom I = ( ( A (,) B ) \ { Y } ) )
203	200, 202	eqtr2d 2471	. . . 4 |- ( ph -> ( ( A (,) B ) \ { Y } ) = dom ( RR _D G ) )
204		eqimss 3522	. . . 4 |- ( ( ( A (,) B ) \ { Y } ) = dom ( RR _D G ) -> ( ( A (,) B ) \ { Y } ) C_ dom ( RR _D G ) )
205	203, 204	syl 17	. . 3 |- ( ph -> ( ( A (,) B ) \ { Y } ) C_ dom ( RR _D G ) )
206	105, 70	syldan 472	. . . . . . . 8 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. y ) e. CC )
207	206	ralrimiva 2846	. . . . . . 7 |- ( ph -> A. y e. ( ( A (,) B ) \ { Y } ) ( ( N + ( 1 / 2 ) ) x. y ) e. CC )
208		eqid 2429	. . . . . . . 8 |- ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) )
209	208	fnmpt 5722	. . . . . . 7 |- ( 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 } ) )
210	207, 209	syl 17	. . . . . 6 |- ( ph -> ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) Fn ( ( A (,) B ) \ { Y } ) )
211		eqidd 2430	. . . . . . . . . 10 |- ( ( 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 ) ) )
212		simpr 462	. . . . . . . . . . 11 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ y = w ) -> y = w )
213	212	oveq2d 6321	. . . . . . . . . 10 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ y = w ) -> ( ( N + ( 1 / 2 ) ) x. y ) = ( ( N + ( 1 / 2 ) ) x. w ) )
214		simpr 462	. . . . . . . . . 10 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> w e. ( ( A (,) B ) \ { Y } ) )
215	38	adantr 466	. . . . . . . . . . . 12 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> N e. CC )
216		1cnd 9658	. . . . . . . . . . . . 13 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> 1 e. CC )
217	216	halfcld 10857	. . . . . . . . . . . 12 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( 1 / 2 ) e. CC )
218	215, 217	addcld 9661	. . . . . . . . . . 11 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( N + ( 1 / 2 ) ) e. CC )
219		eldifi 3593	. . . . . . . . . . . . . 14 |- ( w e. ( ( A (,) B ) \ { Y } ) -> w e. ( A (,) B ) )
220		elioore 11666	. . . . . . . . . . . . . 14 |- ( w e. ( A (,) B ) -> w e. RR )
221	219, 220	syl 17	. . . . . . . . . . . . 13 |- ( w e. ( ( A (,) B ) \ { Y } ) -> w e. RR )
222	221	recnd 9668	. . . . . . . . . . . 12 |- ( w e. ( ( A (,) B ) \ { Y } ) -> w e. CC )
223	222	adantl 467	. . . . . . . . . . 11 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> w e. CC )
224	218, 223	mulcld 9662	. . . . . . . . . 10 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. w ) e. CC )
225	211, 213, 214, 224	fvmptd 5970	. . . . . . . . 9 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) = ( ( N + ( 1 / 2 ) ) x. w ) )
226		eleq1 2501	. . . . . . . . . . . . . . . 16 |- ( y = w -> ( y e. ( ( A (,) B ) \ { Y } ) <-> w e. ( ( A (,) B ) \ { Y } ) ) )
227	226	anbi2d 708	. . . . . . . . . . . . . . 15 |- ( y = w -> ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) <-> ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) ) )
228		oveq1 6312	. . . . . . . . . . . . . . . 16 |- ( y = w -> ( y mod ( 2 x. pi ) ) = ( w mod ( 2 x. pi ) ) )
229	228	neeq1d 2708	. . . . . . . . . . . . . . 15 |- ( y = w -> ( ( y mod ( 2 x. pi ) ) =/= 0 <-> ( w mod ( 2 x. pi ) ) =/= 0 ) )
230	227, 229	imbi12d 321	. . . . . . . . . . . . . 14 |- ( 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 ) ) )
231		eldifi 3593	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ( A (,) B ) \ { Y } ) -> y e. ( A (,) B ) )
232		elioore 11666	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( A (,) B ) -> y e. RR )
233	231, 232, 130	3syl 18	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. ( ( A (,) B ) \ { Y } ) -> y e. CC )
234		2cnd 10682	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. ( ( A (,) B ) \ { Y } ) -> 2 e. CC )
235	119	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. ( ( A (,) B ) \ { Y } ) -> pi e. CC )
236	134	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. ( ( A (,) B ) \ { Y } ) -> 2 =/= 0 )
237		0re 9642	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. RR
238		pipos 23271	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 < pi
239	237, 238	gtneii 9745	. . . . . . . . . . . . . . . . . . . . 21 |- pi =/= 0
240	239	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. ( ( A (,) B ) \ { Y } ) -> pi =/= 0 )
241	233, 234, 235, 236, 240	divdiv1d 10413	. . . . . . . . . . . . . . . . . . 19 |- ( y e. ( ( A (,) B ) \ { Y } ) -> ( ( y / 2 ) / pi ) = ( y / ( 2 x. pi ) ) )
242	241	eqcomd 2437	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( ( A (,) B ) \ { Y } ) -> ( y / ( 2 x. pi ) ) = ( ( y / 2 ) / pi ) )
243	242	adantl 467	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( y / ( 2 x. pi ) ) = ( ( y / 2 ) / pi ) )
244		dirkercncflem2.yne0	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( sin ` ( y / 2 ) ) =/= 0 )
245	244	neneqd 2632	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> -. ( sin ` ( y / 2 ) ) = 0 )
246	105	halfcld 10857	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( y / 2 ) e. CC )
247		sineq0 23332	. . . . . . . . . . . . . . . . . . 19 |- ( ( y / 2 ) e. CC -> ( ( sin ` ( y / 2 ) ) = 0 <-> ( ( y / 2 ) / pi ) e. ZZ ) )
248	246, 247	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( sin ` ( y / 2 ) ) = 0 <-> ( ( y / 2 ) / pi ) e. ZZ ) )
249	245, 248	mtbid 301	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> -. ( ( y / 2 ) / pi ) e. ZZ )
250	243, 249	eqneltrd 2538	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> -. ( y / ( 2 x. pi ) ) e. ZZ )
251		2rp 11307	. . . . . . . . . . . . . . . . . 18 |- 2 e. RR+
252		pirp 23272	. . . . . . . . . . . . . . . . . 18 |- pi e. RR+
253		rpmulcl 11324	. . . . . . . . . . . . . . . . . 18 |- ( ( 2 e. RR+ /\ pi e. RR+ ) -> ( 2 x. pi ) e. RR+ )
254	251, 252, 253	mp2an 676	. . . . . . . . . . . . . . . . 17 |- ( 2 x. pi ) e. RR+
255		mod0 12100	. . . . . . . . . . . . . . . . 17 |- ( ( y e. RR /\ ( 2 x. pi ) e. RR+ ) -> ( ( y mod ( 2 x. pi ) ) = 0 <-> ( y / ( 2 x. pi ) ) e. ZZ ) )
256	11, 254, 255	sylancl 666	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( y mod ( 2 x. pi ) ) = 0 <-> ( y / ( 2 x. pi ) ) e. ZZ ) )
257	250, 256	mtbird 302	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> -. ( y mod ( 2 x. pi ) ) = 0 )
258	257	neqned 2634	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( y mod ( 2 x. pi ) ) =/= 0 )
259	230, 258	chvarv 2070	. . . . . . . . . . . . 13 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( w mod ( 2 x. pi ) ) =/= 0 )
260	259	neneqd 2632	. . . . . . . . . . . 12 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> -. ( w mod ( 2 x. pi ) ) = 0 )
261		simpll 758	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> ph )
262		simpr 462	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) )
263	222	ad2antlr 731	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> w e. CC )
264	57	recnd 9668	. . . . . . . . . . . . . . . 16 |- ( ph -> Y e. CC )
265	264	ad2antrr 730	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> Y e. CC )
266		0red 9643	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> 0 e. RR )
267	5	nnred 10624	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N e. RR )
268		1red 9657	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> 1 e. RR )
269	268	rehalfcld 10859	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 / 2 ) e. RR )
270	267, 269	readdcld 9669	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( N + ( 1 / 2 ) ) e. RR )
271	5	nngt0d 10653	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> 0 < N )
272	251	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> 2 e. RR+ )
273	272	rpreccld 11351	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 / 2 ) e. RR+ )
274	267, 273	ltaddrpd 11371	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N < ( N + ( 1 / 2 ) ) )
275	266, 267, 270, 271, 274	lttrd 9795	. . . . . . . . . . . . . . . . . 18 |- ( ph -> 0 < ( N + ( 1 / 2 ) ) )
276	275	gt0ne0d 10177	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( N + ( 1 / 2 ) ) =/= 0 )
277	41, 276	jca 534	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( N + ( 1 / 2 ) ) e. CC /\ ( N + ( 1 / 2 ) ) =/= 0 ) )
278	277	ad2antrr 730	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> ( ( N + ( 1 / 2 ) ) e. CC /\ ( N + ( 1 / 2 ) ) =/= 0 ) )
279		mulcan 10248	. . . . . . . . . . . . . . 15 |- ( ( w e. CC /\ Y e. CC /\ ( ( N + ( 1 / 2 ) ) e. CC /\ ( N + ( 1 / 2 ) ) =/= 0 ) ) -> ( ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) <-> w = Y ) )
280	263, 265, 278, 279	syl3anc 1264	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> ( ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) <-> w = Y ) )
281	262, 280	mpbid 213	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> w = Y )
282		oveq1 6312	. . . . . . . . . . . . . 14 |- ( w = Y -> ( w mod ( 2 x. pi ) ) = ( Y mod ( 2 x. pi ) ) )
283		dirkercncflem2.ymod	. . . . . . . . . . . . . 14 |- ( ph -> ( Y mod ( 2 x. pi ) ) = 0 )
284	282, 283	sylan9eqr 2492	. . . . . . . . . . . . 13 |- ( ( ph /\ w = Y ) -> ( w mod ( 2 x. pi ) ) = 0 )
285	261, 281, 284	syl2anc 665	. . . . . . . . . . . 12 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> ( w mod ( 2 x. pi ) ) = 0 )
286	260, 285	mtand 663	. . . . . . . . . . 11 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> -. ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) )
287	41, 264	mulcld 9662	. . . . . . . . . . . . 13 |- ( ph -> ( ( N + ( 1 / 2 ) ) x. Y ) e. CC )
288	287	adantr 466	. . . . . . . . . . . 12 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. Y ) e. CC )
289		elsnc2g 4032	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
290	288, 289	syl 17	. . . . . . . . . . 11 |- ( ( 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 ) ) )
291	286, 290	mtbird 302	. . . . . . . . . 10 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> -. ( ( N + ( 1 / 2 ) ) x. w ) e. { ( ( N + ( 1 / 2 ) ) x. Y ) } )
292	224, 291	eldifd 3453	. . . . . . . . 9 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. w ) e. ( CC \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) )
293	225, 292	eqeltrd 2517	. . . . . . . 8 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) e. ( CC \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) )
294		sinf 14156	. . . . . . . . . . . 12 |- sin : CC --> CC
295	294	fdmi 5751	. . . . . . . . . . 11 |- dom sin = CC
296	295	eqcomi 2442	. . . . . . . . . 10 |- CC = dom sin
297	296	a1i 11	. . . . . . . . 9 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> CC = dom sin )
298	297	difeq1d 3588	. . . . . . . 8 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( CC \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) = ( dom sin \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) )
299	293, 298	eleqtrd 2519	. . . . . . 7 |- ( ( 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 ) } ) )
300	299	ralrimiva 2846	. . . . . 6 |- ( 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 ) } ) )
301		fnfvrnss 6066	. . . . . 6 |- ( ( ( 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 ) } ) )
302	210, 300, 301	syl2anc 665	. . . . 5 |- ( ph -> ran ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) C_ ( dom sin \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) )
303		uncom 3616	. . . . . . . . . 10 |- ( ( ( A (,) B ) \ { Y } ) u. { Y } ) = ( { Y } u. ( ( A (,) B ) \ { Y } ) )
304	303	a1i 11	. . . . . . . . 9 |- ( ph -> ( ( ( A (,) B ) \ { Y } ) u. { Y } ) = ( { Y } u. ( ( A (,) B ) \ { Y } ) ) )
305	27	snssd 4148	. . . . . . . . . 10 |- ( ph -> { Y } C_ ( A (,) B ) )
306		undif 3882	. . . . . . . . . 10 |- ( { Y } C_ ( A (,) B ) <-> ( { Y } u. ( ( A (,) B ) \ { Y } ) ) = ( A (,) B ) )
307	305, 306	sylib 199	. . . . . . . . 9 |- ( ph -> ( { Y } u. ( ( A (,) B ) \ { Y } ) ) = ( A (,) B ) )
308	304, 307	eqtrd 2470	. . . . . . . 8 |- ( ph -> ( ( ( A (,) B ) \ { Y } ) u. { Y } ) = ( A (,) B ) )
309	308	mpteq1d 4507	. . . . . . 7 |- ( 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 ) ) ) )
310		iftrue 3921	. . . . . . . . . . . . 13 |- ( 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 ) )
311		oveq2 6313	. . . . . . . . . . . . 13 |- ( w = Y -> ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) )
312	310, 311	eqtr4d 2473	. . . . . . . . . . . 12 |- ( w = Y -> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) = ( ( N + ( 1 / 2 ) ) x. w ) )
313	312	adantl 467	. . . . . . . . . . 11 |- ( ( ( 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 ) )
314		iffalse 3924	. . . . . . . . . . . . 13 |- ( -. w = Y -> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) = ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) )
315	314	adantl 467	. . . . . . . . . . . 12 |- ( ( ( 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 ) )
316		eqidd 2430	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
317		oveq2 6313	. . . . . . . . . . . . . 14 |- ( y = w -> ( ( N + ( 1 / 2 ) ) x. y ) = ( ( N + ( 1 / 2 ) ) x. w ) )
318	317	adantl 467	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) /\ y = w ) -> ( ( N + ( 1 / 2 ) ) x. y ) = ( ( N + ( 1 / 2 ) ) x. w ) )
319		simpl 458	. . . . . . . . . . . . . . 15 |- ( ( w e. ( A (,) B ) /\ -. w = Y ) -> w e. ( A (,) B ) )
320		id 23	. . . . . . . . . . . . . . . . 17 |- ( -. w = Y -> -. w = Y )
321		elsn 4016	. . . . . . . . . . . . . . . . 17 |- ( w e. { Y } <-> w = Y )
322	320, 321	sylnibr 306	. . . . . . . . . . . . . . . 16 |- ( -. w = Y -> -. w e. { Y } )
323	322	adantl 467	. . . . . . . . . . . . . . 15 |- ( ( w e. ( A (,) B ) /\ -. w = Y ) -> -. w e. { Y } )
324	319, 323	eldifd 3453	. . . . . . . . . . . . . 14 |- ( ( w e. ( A (,) B ) /\ -. w = Y ) -> w e. ( ( A (,) B ) \ { Y } ) )
325	324	adantll 718	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> w e. ( ( A (,) B ) \ { Y } ) )
326	41	adantr 466	. . . . . . . . . . . . . . 15 |- ( ( ph /\ w e. ( A (,) B ) ) -> ( N + ( 1 / 2 ) ) e. CC )
327	220	recnd 9668	. . . . . . . . . . . . . . . 16 |- ( w e. ( A (,) B ) -> w e. CC )
328	327	adantl 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ w e. ( A (,) B ) ) -> w e. CC )
329	326, 328	mulcld 9662	. . . . . . . . . . . . . 14 |- ( ( ph /\ w e. ( A (,) B ) ) -> ( ( N + ( 1 / 2 ) ) x. w ) e. CC )
330	329	adantr 466	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( ( N + ( 1 / 2 ) ) x. w ) e. CC )
331	316, 318, 325, 330	fvmptd 5970	. . . . . . . . . . . 12 |- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) = ( ( N + ( 1 / 2 ) ) x. w ) )
332	315, 331	eqtrd 2470	. . . . . . . . . . 11 |- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) = ( ( N + ( 1 / 2 ) ) x. w ) )
333	313, 332	pm2.61dan 798	. . . . . . . . . 10 |- ( ( ph /\ w e. ( A (,) B ) ) -> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) = ( ( N + ( 1 / 2 ) ) x. w ) )
334	333	mpteq2dva 4512	. . . . . . . . 9 |- ( ph -> ( w e. ( A (,) B ) |-> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) ) ) = ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) )
335		ioosscn 37166	. . . . . . . . . . . . . 14 |- ( A (,) B ) C_ CC
336		resmpt 5174	. . . . . . . . . . . . . 14 |- ( ( A (,) B ) C_ CC -> ( ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) ) |` ( A (,) B ) ) = ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) )
337	335, 336	ax-mp 5	. . . . . . . . . . . . 13 |- ( ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) ) |` ( A (,) B ) ) = ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) )
338		eqid 2429	. . . . . . . . . . . . . . . . 17 |- ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) ) = ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) )
339	338	mulc1cncf 21824	. . . . . . . . . . . . . . . 16 |- ( ( N + ( 1 / 2 ) ) e. CC -> ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( CC -cn-> CC ) )
340	41, 339	syl 17	. . . . . . . . . . . . . . 15 |- ( ph -> ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( CC -cn-> CC ) )
341	51	cnfldtop 21706	. . . . . . . . . . . . . . . . . . 19 |- ( TopOpen ` ℂfld ) e. Top
342		unicntop 37001	. . . . . . . . . . . . . . . . . . . 20 |- CC = U. ( TopOpen ` ℂfld )
343	342	restid 15282	. . . . . . . . . . . . . . . . . . 19 |- ( ( TopOpen ` ℂfld ) e. Top -> ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld ) )
344	341, 343	ax-mp 5	. . . . . . . . . . . . . . . . . 18 |- ( ( TopOpen ` ℂfld ) ↾t CC ) = ( TopOpen ` ℂfld )
345	344	eqcomi 2442	. . . . . . . . . . . . . . . . 17 |- ( TopOpen ` ℂfld ) = ( ( TopOpen ` ℂfld ) ↾t CC )
346	51, 345, 345	cncfcn 21828	. . . . . . . . . . . . . . . 16 |- ( ( CC C_ CC /\ CC C_ CC ) -> ( CC -cn-> CC ) = ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) )
347	74, 75, 346	sylancr 667	. . . . . . . . . . . . . . 15 |- ( ph -> ( CC -cn-> CC ) = ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) )
348	340, 347	eleqtrd 2519	. . . . . . . . . . . . . 14 |- ( ph -> ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) )
349	2, 37	syl5ss 3481	. . . . . . . . . . . . . 14 |- ( ph -> ( A (,) B ) C_ CC )
350	342	cnrest 20223	. . . . . . . . . . . . . 14 |- ( ( ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) /\ ( A (,) B ) C_ CC ) -> ( ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) ) |` ( A (,) B ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
351	348, 349, 350	syl2anc 665	. . . . . . . . . . . . 13 |- ( ph -> ( ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) ) |` ( A (,) B ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
352	337, 351	syl5eqelr 2522	. . . . . . . . . . . 12 |- ( ph -> ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
353	51	cnfldtopon 21705	. . . . . . . . . . . . . 14 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
354		resttopon 20099	. . . . . . . . . . . . . 14 |- ( ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) /\ ( A (,) B ) C_ CC ) -> ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) e. (TopOn ` ( A (,) B ) ) )
355	353, 349, 354	sylancr 667	. . . . . . . . . . . . 13 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) e. (TopOn ` ( A (,) B ) ) )
356		cncnp 20218	. . . . . . . . . . . . 13 |- ( ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) e. (TopOn ` ( A (,) B ) ) /\ ( TopOpen ` ℂfld ) e. (TopOn ` CC ) ) -> ( ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) <-> ( ( 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 ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) ) ) )
357	355, 353, 356	sylancl 666	. . . . . . . . . . . 12 |- ( ph -> ( ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) <-> ( ( 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 ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) ) ) )
358	352, 357	mpbid 213	. . . . . . . . . . 11 |- ( 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 ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) ) )
359	358	simprd 464	. . . . . . . . . 10 |- ( ph -> A. y e. ( A (,) B ) ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) )
360		fveq2 5881	. . . . . . . . . . . 12 |- ( y = Y -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` Y ) )
361	360	eleq2d 2499	. . . . . . . . . . 11 |- ( y = Y -> ( ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) <-> ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` Y ) ) )
362	361	rspccva 3187	. . . . . . . . . 10 |- ( ( A. y e. ( A (,) B ) ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) /\ Y e. ( A (,) B ) ) -> ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` Y ) )
363	359, 27, 362	syl2anc 665	. . . . . . . . 9 |- ( ph -> ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` Y ) )
364	334, 363	eqeltrd 2517	. . . . . . . 8 |- ( 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 ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` Y ) )
365	308	eqcomd 2437	. . . . . . . . . . 11 |- ( ph -> ( A (,) B ) = ( ( ( A (,) B ) \ { Y } ) u. { Y } ) )
366	365	oveq2d 6321	. . . . . . . . . 10 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) )
367	366	oveq1d 6320	. . . . . . . . 9 |- ( ph -> ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) = ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) CnP ( TopOpen ` ℂfld ) ) )
368	367	fveq1d 5883	. . . . . . . 8 |- ( ph -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` Y ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) CnP ( TopOpen ` ℂfld ) ) ` Y ) )
369	364, 368	eleqtrd 2519	. . . . . . 7 |- ( 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 ` ℂfld ) ↾t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) CnP ( TopOpen ` ℂfld ) ) ` Y ) )
370	309, 369	eqeltrd 2517	. . . . . 6 |- ( 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 ` ℂfld ) ↾t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) CnP ( TopOpen ` ℂfld ) ) ` Y ) )
371		eqid 2429	. . . . . . 7 |- ( ( TopOpen ` ℂfld ) ↾t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) )
372		eqid 2429	. . . . . . 7 |- ( w e. ( ( ( A (,) B ) \ { Y } ) u. { Y } ) |-> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e. ( (