Theorem dirkercncflem2 38078

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 3549	. . . . 5 |- ( ( A (,) B ) \ { Y } ) C_ ( A (,) B )
2		ioossre 11721	. . . . 5 |- ( A (,) B ) C_ RR
3	1, 2	sstri 3427	. . . 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 472	. . . . . . . 8 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> N e. NN )
7	6	nnred 10646	. . . . . . 7 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> N e. RR )
8		halfre 10851	. . . . . . . 8 |- ( 1 / 2 ) e. RR
9	8	a1i 11	. . . . . . 7 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( 1 / 2 ) e. RR )
10	7, 9	readdcld 9688	. . . . . 6 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( N + ( 1 / 2 ) ) e. RR )
11	4	sselda 3418	. . . . . 6 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> y e. RR )
12	10, 11	remulcld 9689	. . . . 5 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. y ) e. RR )
13	12	resincld 14274	. . . 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 10701	. . . . . . 7 |- 2 e. RR
17		pire 23492	. . . . . . 7 |- pi e. RR
18	16, 17	remulcli 9675	. . . . . 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 10882	. . . . . 6 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( y / 2 ) e. RR )
21	20	resincld 14274	. . . . 5 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( sin ` ( y / 2 ) ) e. RR )
22	19, 21	remulcld 9689	. . . 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 21864	. . . 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 2471	. . 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 6324	. . . . . . 7 |- ( ph -> ( RR _D F ) = ( RR _D ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
31		resmpt 5160	. . . . . . . . . . . 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 2480	. . . . . . . . . 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 6324	. . . . . . . 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 9614	. . . . . . . . . 10 |- RR C_ CC
37	36	a1i 11	. . . . . . . . 9 |- ( ph -> RR C_ CC )
38	5	nncnd 10647	. . . . . . . . . . . . . 14 |- ( ph -> N e. CC )
39		halfcn 10852	. . . . . . . . . . . . . . 15 |- ( 1 / 2 ) e. CC
40	39	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 / 2 ) e. CC )
41	38, 40	addcld 9680	. . . . . . . . . . . . 13 |- ( ph -> ( N + ( 1 / 2 ) ) e. CC )
42	41	adantr 472	. . . . . . . . . . . 12 |- ( ( ph /\ y e. RR ) -> ( N + ( 1 / 2 ) ) e. CC )
43	37	sselda 3418	. . . . . . . . . . . 12 |- ( ( ph /\ y e. RR ) -> y e. CC )
44	42, 43	mulcld 9681	. . . . . . . . . . 11 |- ( ( ph /\ y e. RR ) -> ( ( N + ( 1 / 2 ) ) x. y ) e. CC )
45	44	sincld 14261	. . . . . . . . . 10 |- ( ( ph /\ y e. RR ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) e. CC )
46		eqid 2471	. . . . . . . . . 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 3437	. . . . . . . . . . 11 |- RR C_ RR
49	48, 3	pm3.2i 462	. . . . . . . . . 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 2471	. . . . . . . . . 10 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
52	51	tgioo2 21899	. . . . . . . . . 10 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
53	51, 52	dvres 22945	. . . . . . . . 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 1291	. . . . . . . 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 21860	. . . . . . . . . . 11 |- ( topGen ` ran (,) ) e. Top
56		rehaus 21895	. . . . . . . . . . . . 13 |- ( topGen ` ran (,) ) e. Haus
57	2, 27	sseldi 3416	. . . . . . . . . . . . 13 |- ( ph -> Y e. RR )
58		uniretop 21861	. . . . . . . . . . . . . 14 |- RR = U. ( topGen ` ran (,) )
59	58	sncld 20464	. . . . . . . . . . . . 13 |- ( ( ( topGen ` ran (,) ) e. Haus /\ Y e. RR ) -> { Y } e. ( Clsd ` ( topGen ` ran (,) ) ) )
60	56, 57, 59	sylancr 676	. . . . . . . . . . . 12 |- ( ph -> { Y } e. ( Clsd ` ( topGen ` ran (,) ) ) )
61	58	difopn 20126	. . . . . . . . . . . 12 |- ( ( ( A (,) B ) e. ( topGen ` ran (,) ) /\ { Y } e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( ( A (,) B ) \ { Y } ) e. ( topGen ` ran (,) ) )
62	25, 60, 61	sylancr 676	. . . . . . . . . . 11 |- ( ph -> ( ( A (,) B ) \ { Y } ) e. ( topGen ` ran (,) ) )
63		isopn3i 20175	. . . . . . . . . . 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 676	. . . . . . . . . 10 |- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) \ { Y } ) ) = ( ( A (,) B ) \ { Y } ) )
65	64	reseq2d 5111	. . . . . . . . 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 9649	. . . . . . . . . . . . 13 |- RR e. { RR , CC }
67	66	a1i 11	. . . . . . . . . . . 12 |- ( ph -> RR e. { RR , CC } )
68	41	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. CC ) -> ( N + ( 1 / 2 ) ) e. CC )
69		simpr 468	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. CC ) -> y e. CC )
70	68, 69	mulcld 9681	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. CC ) -> ( ( N + ( 1 / 2 ) ) x. y ) e. CC )
71	70	sincld 14261	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. CC ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) e. CC )
72		eqid 2471	. . . . . . . . . . . . 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 3437	. . . . . . . . . . . . 13 |- CC C_ CC
75	74	a1i 11	. . . . . . . . . . . 12 |- ( ph -> CC C_ CC )
76		dvsinax 37880	. . . . . . . . . . . . . . . 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 5042	. . . . . . . . . . . . . 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 2471	. . . . . . . . . . . . . . 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 14262	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. CC ) -> ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) e. CC )
81	68, 80	mulcld 9681	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. CC ) -> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) e. CC )
82	79, 81	dmmptd 5718	. . . . . . . . . . . . . 14 |- ( ph -> dom ( y e. CC |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = CC )
83	78, 82	eqtrd 2505	. . . . . . . . . . . . 13 |- ( ph -> dom ( CC _D ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = CC )
84	36, 83	syl5sseqr 3467	. . . . . . . . . . . 12 |- ( ph -> RR C_ dom ( CC _D ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
85		dvres3 22947	. . . . . . . . . . . 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 1293	. . . . . . . . . . 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 5160	. . . . . . . . . . . . 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 6324	. . . . . . . . . . 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 5110	. . . . . . . . . . . 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 5160	. . . . . . . . . . . . 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 2521	. . . . . . . . . . 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 2513	. . . . . . . . . 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 5110	. . . . . . . . 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 5160	. . . . . . . . . 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 2509	. . . . . . . 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 2509	. . . . . . 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 2477	. . . . . . 7 |- ( ph -> ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = H )
103	30, 99, 102	3eqtrd 2509	. . . . . 6 |- ( ph -> ( RR _D F ) = H )
104	103	dmeqd 5042	. . . . 5 |- ( ph -> dom ( RR _D F ) = dom H )
105	11	recnd 9687	. . . . . . 7 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> y e. CC )
106	105, 81	syldan 478	. . . . . 6 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) e. CC )
107	100, 106	dmmptd 5718	. . . . 5 |- ( ph -> dom H = ( ( A (,) B ) \ { Y } ) )
108	104, 107	eqtr2d 2506	. . . 4 |- ( ph -> ( ( A (,) B ) \ { Y } ) = dom ( RR _D F ) )
109		eqimss 3470	. . . 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 5160	. . . . . . . . . . . . 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 2480	. . . . . . . . . . 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 6319	. . . . . . . . . 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 10702	. . . . . . . . . . . . . 14 |- 2 e. CC
119		picn 23493	. . . . . . . . . . . . . 14 |- pi e. CC
120	118, 119	mulcli 9666	. . . . . . . . . . . . 13 |- ( 2 x. pi ) e. CC
121	120	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ y e. RR ) -> ( 2 x. pi ) e. CC )
122	43	halfcld 10880	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. RR ) -> ( y / 2 ) e. CC )
123	122	sincld 14261	. . . . . . . . . . . 12 |- ( ( ph /\ y e. RR ) -> ( sin ` ( y / 2 ) ) e. CC )
124	121, 123	mulcld 9681	. . . . . . . . . . 11 |- ( ( ph /\ y e. RR ) -> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) e. CC )
125		eqid 2471	. . . . . . . . . . 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 22945	. . . . . . . . . 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 1291	. . . . . . . . 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 5111	. . . . . . . . . 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 3414	. . . . . . . . . . . . . . . 16 |- ( y e. RR -> y e. CC )
131		1cnd 9677	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. CC -> 1 e. CC )
132		2cnd 10704	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. CC -> 2 e. CC )
133		id 22	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. CC -> y e. CC )
134		2ne0 10724	. . . . . . . . . . . . . . . . . . . . . 22 |- 2 =/= 0
135	134	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. CC -> 2 =/= 0 )
136	131, 132, 133, 135	div13d 10429	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. CC -> ( ( 1 / 2 ) x. y ) = ( ( y / 2 ) x. 1 ) )
137		halfcl 10861	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. CC -> ( y / 2 ) e. CC )
138	137	mulid1d 9678	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. CC -> ( ( y / 2 ) x. 1 ) = ( y / 2 ) )
139	136, 138	eqtrd 2505	. . . . . . . . . . . . . . . . . . 19 |- ( y e. CC -> ( ( 1 / 2 ) x. y ) = ( y / 2 ) )
140	139	fveq2d 5883	. . . . . . . . . . . . . . . . . 18 |- ( y e. CC -> ( sin ` ( ( 1 / 2 ) x. y ) ) = ( sin ` ( y / 2 ) ) )
141	140	oveq2d 6324	. . . . . . . . . . . . . . . . 17 |- ( y e. CC -> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) = ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) )
142	141	eqcomd 2477	. . . . . . . . . . . . . . . 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 473	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. RR ) -> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) = ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) )
145	144	mpteq2dva 4482	. . . . . . . . . . . . 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 6324	. . . . . . . . . . . 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 9681	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. CC ) -> ( ( 1 / 2 ) x. y ) e. CC )
150	149	sincld 14261	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. CC ) -> ( sin ` ( ( 1 / 2 ) x. y ) ) e. CC )
151	147, 150	mulcld 9681	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. CC ) -> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) e. CC )
152		eqid 2471	. . . . . . . . . . . . . . . 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 10704	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> 2 e. CC )
155	119	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> pi e. CC )
156	154, 155	mulcld 9681	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 2 x. pi ) e. CC )
157		dvasinbx 37889	. . . . . . . . . . . . . . . . . . . 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 675	. . . . . . . . . . . . . . . . . . 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 10704	. . . . . . . . . . . . . . . . . . . . . . 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 9861	. . . . . . . . . . . . . . . . . . . . . 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 10400	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ y e. CC ) -> ( 2 x. ( 1 / 2 ) ) = 1 )
164	163	oveq1d 6323	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ y e. CC ) -> ( ( 2 x. ( 1 / 2 ) ) x. pi ) = ( 1 x. pi ) )
165	160	mulid2d 9679	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ y e. CC ) -> ( 1 x. pi ) = pi )
166	161, 164, 165	3eqtrd 2509	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ y e. CC ) -> ( ( 2 x. pi ) x. ( 1 / 2 ) ) = pi )
167	139	fveq2d 5883	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. CC -> ( cos ` ( ( 1 / 2 ) x. y ) ) = ( cos ` ( y / 2 ) ) )
168	167	adantl 473	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ y e. CC ) -> ( cos ` ( ( 1 / 2 ) x. y ) ) = ( cos ` ( y / 2 ) ) )
169	166, 168	oveq12d 6326	. . . . . . . . . . . . . . . . . . . 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 4482	. . . . . . . . . . . . . . . . . . 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 2505	. . . . . . . . . . . . . . . . . 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 5042	. . . . . . . . . . . . . . . . 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 2471	. . . . . . . . . . . . . . . . . 18 |- ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) = ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) )
174	69	halfcld 10880	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ y e. CC ) -> ( y / 2 ) e. CC )
175	174	coscld 14262	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ y e. CC ) -> ( cos ` ( y / 2 ) ) e. CC )
176	160, 175	mulcld 9681	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. CC ) -> ( pi x. ( cos ` ( y / 2 ) ) ) e. CC )
177	173, 176	dmmptd 5718	. . . . . . . . . . . . . . . . 17 |- ( ph -> dom ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) = CC )
178	172, 177	eqtrd 2505	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( CC _D ( y e. CC |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) = CC )
179	36, 178	syl5sseqr 3467	. . . . . . . . . . . . . . 15 |- ( ph -> RR C_ dom ( CC _D ( y e. CC |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) )
180		dvres3 22947	. . . . . . . . . . . . . . 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 1293	. . . . . . . . . . . . . 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 5160	. . . . . . . . . . . . . . . 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 6324	. . . . . . . . . . . . . 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 5110	. . . . . . . . . . . . . 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 2513	. . . . . . . . . . . . 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 5160	. . . . . . . . . . . . . 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 2521	. . . . . . . . . . . 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 2505	. . . . . . . . . . 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 5110	. . . . . . . . . 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 5162	. . . . . . . . . 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 2509	. . . . . . . . 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 2509	. . . . . . . 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 2477	. . . . . . 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 6324	. . . . . . . 8 |- ( ph -> ( RR _D G ) = ( RR _D ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) )
198	197	eqcomd 2477	. . . . . . 7 |- ( ph -> ( RR _D ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) = ( RR _D G ) )
199	112, 195, 198	3eqtrrd 2510	. . . . . 6 |- ( ph -> ( RR _D G ) = I )
200	199	dmeqd 5042	. . . . 5 |- ( ph -> dom ( RR _D G ) = dom I )
201	105, 176	syldan 478	. . . . . 6 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( pi x. ( cos ` ( y / 2 ) ) ) e. CC )
202	111, 201	dmmptd 5718	. . . . 5 |- ( ph -> dom I = ( ( A (,) B ) \ { Y } ) )
203	200, 202	eqtr2d 2506	. . . 4 |- ( ph -> ( ( A (,) B ) \ { Y } ) = dom ( RR _D G ) )
204		eqimss 3470	. . . 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 478	. . . . . . . 8 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. y ) e. CC )
207	206	ralrimiva 2809	. . . . . . 7 |- ( ph -> A. y e. ( ( A (,) B ) \ { Y } ) ( ( N + ( 1 / 2 ) ) x. y ) e. CC )
208		eqid 2471	. . . . . . . 8 |- ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) )
209	208	fnmpt 5714	. . . . . . 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 2472	. . . . . . . . . 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 468	. . . . . . . . . . 11 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ y = w ) -> y = w )
213	212	oveq2d 6324	. . . . . . . . . 10 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ y = w ) -> ( ( N + ( 1 / 2 ) ) x. y ) = ( ( N + ( 1 / 2 ) ) x. w ) )
214		simpr 468	. . . . . . . . . 10 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> w e. ( ( A (,) B ) \ { Y } ) )
215	38	adantr 472	. . . . . . . . . . . 12 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> N e. CC )
216		1cnd 9677	. . . . . . . . . . . . 13 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> 1 e. CC )
217	216	halfcld 10880	. . . . . . . . . . . 12 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( 1 / 2 ) e. CC )
218	215, 217	addcld 9680	. . . . . . . . . . 11 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( N + ( 1 / 2 ) ) e. CC )
219		eldifi 3544	. . . . . . . . . . . . . 14 |- ( w e. ( ( A (,) B ) \ { Y } ) -> w e. ( A (,) B ) )
220		elioore 11691	. . . . . . . . . . . . . 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 9687	. . . . . . . . . . . 12 |- ( w e. ( ( A (,) B ) \ { Y } ) -> w e. CC )
223	222	adantl 473	. . . . . . . . . . 11 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> w e. CC )
224	218, 223	mulcld 9681	. . . . . . . . . 10 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. w ) e. CC )
225	211, 213, 214, 224	fvmptd 5969	. . . . . . . . 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 2537	. . . . . . . . . . . . . . . 16 |- ( y = w -> ( y e. ( ( A (,) B ) \ { Y } ) <-> w e. ( ( A (,) B ) \ { Y } ) ) )
227	226	anbi2d 718	. . . . . . . . . . . . . . 15 |- ( y = w -> ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) <-> ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) ) )
228		oveq1 6315	. . . . . . . . . . . . . . . 16 |- ( y = w -> ( y mod ( 2 x. pi ) ) = ( w mod ( 2 x. pi ) ) )
229	228	neeq1d 2702	. . . . . . . . . . . . . . 15 |- ( y = w -> ( ( y mod ( 2 x. pi ) ) =/= 0 <-> ( w mod ( 2 x. pi ) ) =/= 0 ) )
230	227, 229	imbi12d 327	. . . . . . . . . . . . . 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 3544	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ( A (,) B ) \ { Y } ) -> y e. ( A (,) B ) )
232		elioore 11691	. . . . . . . . . . . . . . . . . . . . 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 10704	. . . . . . . . . . . . . . . . . . . 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 9661	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 e. RR
238		pipos 23494	. . . . . . . . . . . . . . . . . . . . . 22 |- 0 < pi
239	237, 238	gtneii 9764	. . . . . . . . . . . . . . . . . . . . 21 |- pi =/= 0
240	239	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. ( ( A (,) B ) \ { Y } ) -> pi =/= 0 )
241	233, 234, 235, 236, 240	divdiv1d 10436	. . . . . . . . . . . . . . . . . . 19 |- ( y e. ( ( A (,) B ) \ { Y } ) -> ( ( y / 2 ) / pi ) = ( y / ( 2 x. pi ) ) )
242	241	eqcomd 2477	. . . . . . . . . . . . . . . . . 18 |- ( y e. ( ( A (,) B ) \ { Y } ) -> ( y / ( 2 x. pi ) ) = ( ( y / 2 ) / pi ) )
243	242	adantl 473	. . . . . . . . . . . . . . . . 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 2648	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> -. ( sin ` ( y / 2 ) ) = 0 )
246	105	halfcld 10880	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( y / 2 ) e. CC )
247		sineq0 23555	. . . . . . . . . . . . . . . . . . 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 307	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> -. ( ( y / 2 ) / pi ) e. ZZ )
250	243, 249	eqneltrd 2568	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> -. ( y / ( 2 x. pi ) ) e. ZZ )
251		2rp 11330	. . . . . . . . . . . . . . . . . 18 |- 2 e. RR+
252		pirp 23495	. . . . . . . . . . . . . . . . . 18 |- pi e. RR+
253		rpmulcl 11347	. . . . . . . . . . . . . . . . . 18 |- ( ( 2 e. RR+ /\ pi e. RR+ ) -> ( 2 x. pi ) e. RR+ )
254	251, 252, 253	mp2an 686	. . . . . . . . . . . . . . . . 17 |- ( 2 x. pi ) e. RR+
255		mod0 12136	. . . . . . . . . . . . . . . . 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 675	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( y mod ( 2 x. pi ) ) = 0 <-> ( y / ( 2 x. pi ) ) e. ZZ ) )
257	250, 256	mtbird 308	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> -. ( y mod ( 2 x. pi ) ) = 0 )
258	257	neqned 2650	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( y mod ( 2 x. pi ) ) =/= 0 )
259	230, 258	chvarv 2120	. . . . . . . . . . . . 13 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( w mod ( 2 x. pi ) ) =/= 0 )
260	259	neneqd 2648	. . . . . . . . . . . 12 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> -. ( w mod ( 2 x. pi ) ) = 0 )
261		simpll 768	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> ph )
262		simpr 468	. . . . . . . . . . . . . 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 741	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> w e. CC )
264	57	recnd 9687	. . . . . . . . . . . . . . . 16 |- ( ph -> Y e. CC )
265	264	ad2antrr 740	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> Y e. CC )
266		0red 9662	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> 0 e. RR )
267	5	nnred 10646	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N e. RR )
268		1red 9676	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> 1 e. RR )
269	268	rehalfcld 10882	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 / 2 ) e. RR )
270	267, 269	readdcld 9688	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( N + ( 1 / 2 ) ) e. RR )
271	5	nngt0d 10675	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> 0 < N )
272	251	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> 2 e. RR+ )
273	272	rpreccld 11374	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 / 2 ) e. RR+ )
274	267, 273	ltaddrpd 11394	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N < ( N + ( 1 / 2 ) ) )
275	266, 267, 270, 271, 274	lttrd 9813	. . . . . . . . . . . . . . . . . 18 |- ( ph -> 0 < ( N + ( 1 / 2 ) ) )
276	275	gt0ne0d 10199	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( N + ( 1 / 2 ) ) =/= 0 )
277	41, 276	jca 541	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( N + ( 1 / 2 ) ) e. CC /\ ( N + ( 1 / 2 ) ) =/= 0 ) )
278	277	ad2antrr 740	. . . . . . . . . . . . . . 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 10271	. . . . . . . . . . . . . . 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 1292	. . . . . . . . . . . . . 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 215	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> w = Y )
282		oveq1 6315	. . . . . . . . . . . . . 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 2527	. . . . . . . . . . . . 13 |- ( ( ph /\ w = Y ) -> ( w mod ( 2 x. pi ) ) = 0 )
285	261, 281, 284	syl2anc 673	. . . . . . . . . . . 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 671	. . . . . . . . . . 11 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> -. ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) )
287	41, 264	mulcld 9681	. . . . . . . . . . . . 13 |- ( ph -> ( ( N + ( 1 / 2 ) ) x. Y ) e. CC )
288	287	adantr 472	. . . . . . . . . . . 12 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. Y ) e. CC )
289		elsnc2g 3990	. . . . . . . . . . . 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 308	. . . . . . . . . 10 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> -. ( ( N + ( 1 / 2 ) ) x. w ) e. { ( ( N + ( 1 / 2 ) ) x. Y ) } )
292	224, 291	eldifd 3401	. . . . . . . . 9 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. w ) e. ( CC \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) )
293	225, 292	eqeltrd 2549	. . . . . . . 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 14255	. . . . . . . . . . . 12 |- sin : CC --> CC
295	294	fdmi 5746	. . . . . . . . . . 11 |- dom sin = CC
296	295	eqcomi 2480	. . . . . . . . . 10 |- CC = dom sin
297	296	a1i 11	. . . . . . . . 9 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> CC = dom sin )
298	297	difeq1d 3539	. . . . . . . 8 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( CC \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) = ( dom sin \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) )
299	293, 298	eleqtrd 2551	. . . . . . 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 2809	. . . . . 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 673	. . . . 5 |- ( ph -> ran ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) C_ ( dom sin \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) )
303		uncom 3569	. . . . . . . . . 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 4108	. . . . . . . . . 10 |- ( ph -> { Y } C_ ( A (,) B ) )
306		undif 3839	. . . . . . . . . 10 |- ( { Y } C_ ( A (,) B ) <-> ( { Y } u. ( ( A (,) B ) \ { Y } ) ) = ( A (,) B ) )
307	305, 306	sylib 201	. . . . . . . . 9 |- ( ph -> ( { Y } u. ( ( A (,) B ) \ { Y } ) ) = ( A (,) B ) )
308	304, 307	eqtrd 2505	. . . . . . . 8 |- ( ph -> ( ( ( A (,) B ) \ { Y } ) u. { Y } ) = ( A (,) B ) )
309	308	mpteq1d 4477	. . . . . . 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 3878	. . . . . . . . . . . . 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 6316	. . . . . . . . . . . . 13 |- ( w = Y -> ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) )
312	310, 311	eqtr4d 2508	. . . . . . . . . . . 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 473	. . . . . . . . . . 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 3881	. . . . . . . . . . . . 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 473	. . . . . . . . . . . 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 2472	. . . . . . . . . . . . 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 6316	. . . . . . . . . . . . . 14 |- ( y = w -> ( ( N + ( 1 / 2 ) ) x. y ) = ( ( N + ( 1 / 2 ) ) x. w ) )
318	317	adantl 473	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) /\ y = w ) -> ( ( N + ( 1 / 2 ) ) x. y ) = ( ( N + ( 1 / 2 ) ) x. w ) )
319		simpl 464	. . . . . . . . . . . . . . 15 |- ( ( w e. ( A (,) B ) /\ -. w = Y ) -> w e. ( A (,) B ) )
320		id 22	. . . . . . . . . . . . . . . . 17 |- ( -. w = Y -> -. w = Y )
321		elsn 3973	. . . . . . . . . . . . . . . . 17 |- ( w e. { Y } <-> w = Y )
322	320, 321	sylnibr 312	. . . . . . . . . . . . . . . 16 |- ( -. w = Y -> -. w e. { Y } )
323	322	adantl 473	. . . . . . . . . . . . . . 15 |- ( ( w e. ( A (,) B ) /\ -. w = Y ) -> -. w e. { Y } )
324	319, 323	eldifd 3401	. . . . . . . . . . . . . 14 |- ( ( w e. ( A (,) B ) /\ -. w = Y ) -> w e. ( ( A (,) B ) \ { Y } ) )
325	324	adantll 728	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> w e. ( ( A (,) B ) \ { Y } ) )
326	41	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ph /\ w e. ( A (,) B ) ) -> ( N + ( 1 / 2 ) ) e. CC )
327	220	recnd 9687	. . . . . . . . . . . . . . . 16 |- ( w e. ( A (,) B ) -> w e. CC )
328	327	adantl 473	. . . . . . . . . . . . . . 15 |- ( ( ph /\ w e. ( A (,) B ) ) -> w e. CC )
329	326, 328	mulcld 9681	. . . . . . . . . . . . . 14 |- ( ( ph /\ w e. ( A (,) B ) ) -> ( ( N + ( 1 / 2 ) ) x. w ) e. CC )
330	329	adantr 472	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) -> ( ( N + ( 1 / 2 ) ) x. w ) e. CC )
331	316, 318, 325, 330	fvmptd 5969	. . . . . . . . . . . 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 2505	. . . . . . . . . . 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 808	. . . . . . . . . 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 4482	. . . . . . . . 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 37687	. . . . . . . . . . . . . 14 |- ( A (,) B ) C_ CC
336		resmpt 5160	. . . . . . . . . . . . . 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 2471	. . . . . . . . . . . . . . . . 17 |- ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) ) = ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) )
339	338	mulc1cncf 22015	. . . . . . . . . . . . . . . 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 21882	. . . . . . . . . . . . . . . . . . 19 |- ( TopOpen ` ℂfld ) e. Top
342		unicntop 37433	. . . . . . . . . . . . . . . . . . . 20 |- CC = U. ( TopOpen ` ℂfld )
343	342	restid 15410	. . . . . . . . . . . . . . . . . . 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 2480	. . . . . . . . . . . . . . . . 17 |- ( TopOpen ` ℂfld ) = ( ( TopOpen ` ℂfld ) ↾t CC )
346	51, 345, 345	cncfcn 22019	. . . . . . . . . . . . . . . 16 |- ( ( CC C_ CC /\ CC C_ CC ) -> ( CC -cn-> CC ) = ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) )
347	74, 75, 346	sylancr 676	. . . . . . . . . . . . . . 15 |- ( ph -> ( CC -cn-> CC ) = ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) )
348	340, 347	eleqtrd 2551	. . . . . . . . . . . . . 14 |- ( ph -> ( w e. CC |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( TopOpen ` ℂfld ) Cn ( TopOpen ` ℂfld ) ) )
349	2, 37	syl5ss 3429	. . . . . . . . . . . . . 14 |- ( ph -> ( A (,) B ) C_ CC )
350	342	cnrest 20378	. . . . . . . . . . . . . 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 673	. . . . . . . . . . . . 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 2554	. . . . . . . . . . . 12 |- ( ph -> ( w e. ( A (,) B ) |-> ( ( N + ( 1 / 2 ) ) x. w ) ) e. ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) Cn ( TopOpen ` ℂfld ) ) )
353	51	cnfldtopon 21881	. . . . . . . . . . . . . 14 |- ( TopOpen ` ℂfld ) e. (TopOn ` CC )
354		resttopon 20254	. . . . . . . . . . . . . 14 |- ( ( ( TopOpen ` ℂfld ) e. (TopOn ` CC ) /\ ( A (,) B ) C_ CC ) -> ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) e. (TopOn ` ( A (,) B ) ) )
355	353, 349, 354	sylancr 676	. . . . . . . . . . . . 13 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) e. (TopOn ` ( A (,) B ) ) )
356		cncnp 20373	. . . . . . . . . . . . 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 675	. . . . . . . . . . . 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 215	. . . . . . . . . . 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 470	. . . . . . . . . 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 5879	. . . . . . . . . . . 12 |- ( y = Y -> ( ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` y ) = ( ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) ` Y ) )
361	360	eleq2d 2534	. . . . . . . . . . 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 3135	. . . . . . . . . 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 673	. . . . . . . . 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 2549	. . . . . . . 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 2477	. . . . . . . . . . 11 |- ( ph -> ( A (,) B ) = ( ( ( A (,) B ) \ { Y } ) u. { Y } ) )
366	365	oveq2d 6324	. . . . . . . . . 10 |- ( ph -> ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) )
367	366	oveq1d 6323	. . . . . . . . 9 |- ( ph -> ( ( ( TopOpen ` ℂfld ) ↾t ( A (,) B ) ) CnP ( TopOpen ` ℂfld ) ) = ( ( ( TopOpen ` ℂfld ) ↾t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) CnP ( TopOpen ` ℂfld ) ) )
368	367	fveq1d 5881	. . . . . . . 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 2551	. . . . . . 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 2549	. . . . . 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 2471	. . . . . . 7 |- ( ( TopOpen ` ℂfld ) ↾t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) ) = ( ( TopOpen ` ℂfld ) ↾t ( ( ( A (,) B ) \ { Y } ) u. { Y } ) )
372		eqid 2471	. . . . . . 7 |- ( w e. ( ( ( A (,) B ) \ { Y } ) u. { Y } ) |-> if ( w = Y , ( ( N + ( 1 / 2 ) ) x. Y ) , ( ( y e.