Theorem dirkercncflem2 31727

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

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		difss 3636	. . . . 5 |- ( ( A (,) B ) \ { Y } ) C_ ( A (,) B )
2		ioossre 11598	. . . . 5 |- ( A (,) B ) C_ RR
3	1, 2	sstri 3518	. . . 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 465	. . . . . . . 8 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> N e. NN )
7	6	nnred 10563	. . . . . . 7 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> N e. RR )
8		1re 9607	. . . . . . . . 9 |- 1 e. RR
9	8	rehalfcli 10799	. . . . . . . 8 |- ( 1 / 2 ) e. RR
10	9	a1i 11	. . . . . . 7 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( 1 / 2 ) e. RR )
11	7, 10	readdcld 9635	. . . . . 6 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( N + ( 1 / 2 ) ) e. RR )
12	4	sselda 3509	. . . . . 6 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> y e. RR )
13	11, 12	remulcld 9636	. . . . 5 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. y ) e. RR )
14	13	resincld 13756	. . . 4 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) e. RR )
15		dirkercncflem2.f	. . . 4 |- F = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) )
16	14, 15	fmptd 6056	. . 3 |- ( ph -> F : ( ( A (,) B ) \ { Y } ) --> RR )
17		2re 10617	. . . . . . . 8 |- 2 e. RR
18		pire 22718	. . . . . . . 8 |- pi e. RR
19	17, 18	remulcli 9622	. . . . . . 7 |- ( 2 x. pi ) e. RR
20	19	a1i 11	. . . . . 6 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( 2 x. pi ) e. RR )
21		rehalfcl 10777	. . . . . . . 8 |- ( y e. RR -> ( y / 2 ) e. RR )
22	12, 21	syl 16	. . . . . . 7 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( y / 2 ) e. RR )
23		resincl 13753	. . . . . . 7 |- ( ( y / 2 ) e. RR -> ( sin ` ( y / 2 ) ) e. RR )
24	22, 23	syl 16	. . . . . 6 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( sin ` ( y / 2 ) ) e. RR )
25	20, 24	jca 532	. . . . 5 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( 2 x. pi ) e. RR /\ ( sin ` ( y / 2 ) ) e. RR ) )
26		remulcl 9589	. . . . 5 |- ( ( ( 2 x. pi ) e. RR /\ ( sin ` ( y / 2 ) ) e. RR ) -> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) e. RR )
27	25, 26	syl 16	. . . 4 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) e. RR )
28		dirkercncflem2.g	. . . 4 |- G = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) )
29	27, 28	fmptd 6056	. . 3 |- ( ph -> G : ( ( A (,) B ) \ { Y } ) --> RR )
30		iooretop 21141	. . . 4 |- ( A (,) B ) e. ( topGen ` ran (,) )
31	30	a1i 11	. . 3 |- ( ph -> ( A (,) B ) e. ( topGen ` ran (,) ) )
32		dirkercncflem2.y	. . 3 |- ( ph -> Y e. ( A (,) B ) )
33		eqid 2467	. . 3 |- ( ( A (,) B ) \ { Y } ) = ( ( A (,) B ) \ { Y } )
34	15	a1i 11	. . . . . . . 8 |- ( ph -> F = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
35	34	oveq2d 6311	. . . . . . 7 |- ( ph -> ( RR _D F ) = ( RR _D ( y e. ( ( A (,) B ) \ { Y } ) |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
36		resmpt 5329	. . . . . . . . . . . 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 ) ) ) )
37	3, 36	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 ) ) )
38	37	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 } ) )
39	38	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 } ) ) )
40	39	oveq2d 6311	. . . . . . . 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 } ) ) ) )
41		ax-resscn 9561	. . . . . . . . . . 11 |- RR C_ CC
42	41	a1i 11	. . . . . . . . . 10 |- ( ph -> RR C_ CC )
43	5	nncnd 10564	. . . . . . . . . . . . . . 15 |- ( ph -> N e. CC )
44		ax-1cn 9562	. . . . . . . . . . . . . . . . 17 |- 1 e. CC
45		halfcl 10776	. . . . . . . . . . . . . . . . 17 |- ( 1 e. CC -> ( 1 / 2 ) e. CC )
46	44, 45	ax-mp 5	. . . . . . . . . . . . . . . 16 |- ( 1 / 2 ) e. CC
47	46	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 / 2 ) e. CC )
48	43, 47	addcld 9627	. . . . . . . . . . . . . 14 |- ( ph -> ( N + ( 1 / 2 ) ) e. CC )
49	48	adantr 465	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. RR ) -> ( N + ( 1 / 2 ) ) e. CC )
50	42	sselda 3509	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. RR ) -> y e. CC )
51	49, 50	mulcld 9628	. . . . . . . . . . . 12 |- ( ( ph /\ y e. RR ) -> ( ( N + ( 1 / 2 ) ) x. y ) e. CC )
52	51	sincld 13743	. . . . . . . . . . 11 |- ( ( ph /\ y e. RR ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) e. CC )
53		eqid 2467	. . . . . . . . . . 11 |- ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) = ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) )
54	52, 53	fmptd 6056	. . . . . . . . . 10 |- ( ph -> ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) : RR --> CC )
55	42, 54	jca 532	. . . . . . . . 9 |- ( ph -> ( RR C_ CC /\ ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) : RR --> CC ) )
56		ssid 3528	. . . . . . . . . . 11 |- RR C_ RR
57	56, 3	pm3.2i 455	. . . . . . . . . 10 |- ( RR C_ RR /\ ( ( A (,) B ) \ { Y } ) C_ RR )
58	57	a1i 11	. . . . . . . . 9 |- ( ph -> ( RR C_ RR /\ ( ( A (,) B ) \ { Y } ) C_ RR ) )
59		eqid 2467	. . . . . . . . . 10 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
60	59	tgioo2 21176	. . . . . . . . . 10 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
61	59, 60	dvres 22183	. . . . . . . . 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 } ) ) ) )
62	55, 58, 61	syl2anc 661	. . . . . . . 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 } ) ) ) )
63		retop 21136	. . . . . . . . . . . 12 |- ( topGen ` ran (,) ) e. Top
64	63	a1i 11	. . . . . . . . . . 11 |- ( ph -> ( topGen ` ran (,) ) e. Top )
65		rehaus 21172	. . . . . . . . . . . . . 14 |- ( topGen ` ran (,) ) e. Haus
66	65	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> ( topGen ` ran (,) ) e. Haus )
67	2, 32	sseldi 3507	. . . . . . . . . . . . 13 |- ( ph -> Y e. RR )
68		uniretop 21137	. . . . . . . . . . . . . 14 |- RR = U. ( topGen ` ran (,) )
69	68	sncld 19740	. . . . . . . . . . . . 13 |- ( ( ( topGen ` ran (,) ) e. Haus /\ Y e. RR ) -> { Y } e. ( Clsd ` ( topGen ` ran (,) ) ) )
70	66, 67, 69	syl2anc 661	. . . . . . . . . . . 12 |- ( ph -> { Y } e. ( Clsd ` ( topGen ` ran (,) ) ) )
71	68	difopn 19403	. . . . . . . . . . . 12 |- ( ( ( A (,) B ) e. ( topGen ` ran (,) ) /\ { Y } e. ( Clsd ` ( topGen ` ran (,) ) ) ) -> ( ( A (,) B ) \ { Y } ) e. ( topGen ` ran (,) ) )
72	31, 70, 71	syl2anc 661	. . . . . . . . . . 11 |- ( ph -> ( ( A (,) B ) \ { Y } ) e. ( topGen ` ran (,) ) )
73		isopn3i 19451	. . . . . . . . . . 11 |- ( ( ( topGen ` ran (,) ) e. Top /\ ( ( A (,) B ) \ { Y } ) e. ( topGen ` ran (,) ) ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) \ { Y } ) ) = ( ( A (,) B ) \ { Y } ) )
74	64, 72, 73	syl2anc 661	. . . . . . . . . 10 |- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( ( A (,) B ) \ { Y } ) ) = ( ( A (,) B ) \ { Y } ) )
75	74	reseq2d 5279	. . . . . . . . 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 } ) ) )
76		reex 9595	. . . . . . . . . . . . . . . . 17 |- RR e. _V
77	76	prid1 4141	. . . . . . . . . . . . . . . 16 |- RR e. { RR , CC }
78	77	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> RR e. { RR , CC } )
79	48	adantr 465	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. CC ) -> ( N + ( 1 / 2 ) ) e. CC )
80		simpr 461	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. CC ) -> y e. CC )
81	79, 80	mulcld 9628	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. CC ) -> ( ( N + ( 1 / 2 ) ) x. y ) e. CC )
82	81	sincld 13743	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. CC ) -> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) e. CC )
83		eqid 2467	. . . . . . . . . . . . . . . 16 |- ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) = ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) )
84	82, 83	fmptd 6056	. . . . . . . . . . . . . . 15 |- ( ph -> ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) : CC --> CC )
85	78, 84	jca 532	. . . . . . . . . . . . . 14 |- ( ph -> ( RR e. { RR , CC } /\ ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) : CC --> CC ) )
86		ssid 3528	. . . . . . . . . . . . . . . 16 |- CC C_ CC
87	86	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> CC C_ CC )
88		dvsinax 31564	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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 ) ) ) ) )
89	48, 88	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( 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 ) ) ) ) )
90		dmeq 5209	. . . . . . . . . . . . . . . . . 18 |- ( ( CC _D ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = ( y e. CC |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) -> 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 ) ) ) ) )
91	89, 90	syl 16	. . . . . . . . . . . . . . . . 17 |- ( 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 ) ) ) ) )
92		coscl 13740	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( N + ( 1 / 2 ) ) x. y ) e. CC -> ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) e. CC )
93	81, 92	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ y e. CC ) -> ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) e. CC )
94	79, 93	jca 532	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ y e. CC ) -> ( ( N + ( 1 / 2 ) ) e. CC /\ ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) e. CC ) )
95		mulcl 9588	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( N + ( 1 / 2 ) ) e. CC /\ ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) e. CC ) -> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) e. CC )
96	94, 95	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ y e. CC ) -> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) e. CC )
97		eqid 2467	. . . . . . . . . . . . . . . . . . 19 |- ( 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 ) ) ) )
98	96, 97	fmptd 6056	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( y e. CC |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) : CC --> CC )
99		fdm 5741	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. CC |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) : CC --> CC -> dom ( y e. CC |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = CC )
100	98, 99	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ph -> dom ( y e. CC |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = CC )
101	91, 100	eqtrd 2508	. . . . . . . . . . . . . . . 16 |- ( ph -> dom ( CC _D ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = CC )
102	42, 101	sseqtr4d 3546	. . . . . . . . . . . . . . 15 |- ( ph -> RR C_ dom ( CC _D ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
103	87, 102	jca 532	. . . . . . . . . . . . . 14 |- ( ph -> ( CC C_ CC /\ RR C_ dom ( CC _D ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) ) )
104		dvres3 22185	. . . . . . . . . . . . . 14 |- ( ( ( 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 ) )
105	85, 103, 104	syl2anc 661	. . . . . . . . . . . . 13 |- ( 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 ) )
106	89	reseq1d 5278	. . . . . . . . . . . . . 14 |- ( 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 ) )
107		resmpt 5329	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) ) )
108	41, 107	ax-mp 5	. . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) )
109	108	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( ( 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 ) ) ) ) )
110	106, 109	eqtrd 2508	. . . . . . . . . . . . 13 |- ( 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 ) ) ) ) )
111	105, 110	eqtrd 2508	. . . . . . . . . . . 12 |- ( ph -> ( RR _D ( ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` RR ) ) = ( y e. RR |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
112		resmpt 5329	. . . . . . . . . . . . . . 15 |- ( RR C_ CC -> ( ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` RR ) = ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
113	41, 112	ax-mp 5	. . . . . . . . . . . . . 14 |- ( ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` RR ) = ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) )
114	113	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> ( ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` RR ) = ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
115	114	oveq2d 6311	. . . . . . . . . . . 12 |- ( ph -> ( RR _D ( ( y e. CC |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) |` RR ) ) = ( RR _D ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
116	111, 115	eqtr3d 2510	. . . . . . . . . . 11 |- ( ph -> ( y e. RR |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = ( RR _D ( y e. RR |-> ( sin ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
117	116	eqcomd 2475	. . . . . . . . . 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 ) ) ) ) )
118	117	reseq1d 5278	. . . . . . . . 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 } ) ) )
119		resmpt 5329	. . . . . . . . . . 11 |- ( ( ( 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 ) ) ) ) )
120	3, 119	ax-mp 5	. . . . . . . . . 10 |- ( ( 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 ) ) ) )
121	120	a1i 11	. . . . . . . . 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 ) ) ) ) )
122	75, 118, 121	3eqtrd 2512	. . . . . . . 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 ) ) ) ) )
123	40, 62, 122	3eqtrd 2512	. . . . . . 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 ) ) ) ) )
124		dirkercncflem2.h	. . . . . . . . 9 |- H = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) )
125	124	a1i 11	. . . . . . . 8 |- ( ph -> H = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) )
126	125	eqcomd 2475	. . . . . . 7 |- ( ph -> ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) ) = H )
127	35, 123, 126	3eqtrd 2512	. . . . . 6 |- ( ph -> ( RR _D F ) = H )
128	127	dmeqd 5211	. . . . 5 |- ( ph -> dom ( RR _D F ) = dom H )
129		simpl 457	. . . . . . . . 9 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ph )
130	12, 50	syldan 470	. . . . . . . . 9 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> y e. CC )
131	129, 130	jca 532	. . . . . . . 8 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ph /\ y e. CC ) )
132	131, 96	syl 16	. . . . . . 7 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. ( cos ` ( ( N + ( 1 / 2 ) ) x. y ) ) ) e. CC )
133	132, 124	fmptd 6056	. . . . . 6 |- ( ph -> H : ( ( A (,) B ) \ { Y } ) --> CC )
134		fdm 5741	. . . . . 6 |- ( H : ( ( A (,) B ) \ { Y } ) --> CC -> dom H = ( ( A (,) B ) \ { Y } ) )
135	133, 134	syl 16	. . . . 5 |- ( ph -> dom H = ( ( A (,) B ) \ { Y } ) )
136	128, 135	eqtr2d 2509	. . . 4 |- ( ph -> ( ( A (,) B ) \ { Y } ) = dom ( RR _D F ) )
137		eqimss 3561	. . . 4 |- ( ( ( A (,) B ) \ { Y } ) = dom ( RR _D F ) -> ( ( A (,) B ) \ { Y } ) C_ dom ( RR _D F ) )
138	136, 137	syl 16	. . 3 |- ( ph -> ( ( A (,) B ) \ { Y } ) C_ dom ( RR _D F ) )
139		dirkercncflem2.i	. . . . . . . 8 |- I = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( pi x. ( cos ` ( y / 2 ) ) ) )
140	139	a1i 11	. . . . . . 7 |- ( ph -> I = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) )
141		resmpt 5329	. . . . . . . . . . . . 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 ) ) ) ) )
142	3, 141	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 ) ) ) )
143	142	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 } ) )
144	143	oveq2i 6306	. . . . . . . . . 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 } ) ) )
145	144	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 } ) ) ) )
146		2cn 10618	. . . . . . . . . . . . . . . 16 |- 2 e. CC
147	41, 18	sselii 3506	. . . . . . . . . . . . . . . 16 |- pi e. CC
148	146, 147	mulcli 9613	. . . . . . . . . . . . . . 15 |- ( 2 x. pi ) e. CC
149	148	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. RR ) -> ( 2 x. pi ) e. CC )
150		id 22	. . . . . . . . . . . . . . . . 17 |- ( y e. CC -> y e. CC )
151	146	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( y e. CC -> 2 e. CC )
152		2ne0 10640	. . . . . . . . . . . . . . . . . 18 |- 2 =/= 0
153	152	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( y e. CC -> 2 =/= 0 )
154	150, 151, 153	divcld 10332	. . . . . . . . . . . . . . . 16 |- ( y e. CC -> ( y / 2 ) e. CC )
155	50, 154	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. RR ) -> ( y / 2 ) e. CC )
156		sincl 13739	. . . . . . . . . . . . . . 15 |- ( ( y / 2 ) e. CC -> ( sin ` ( y / 2 ) ) e. CC )
157	155, 156	syl 16	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. RR ) -> ( sin ` ( y / 2 ) ) e. CC )
158	149, 157	jca 532	. . . . . . . . . . . . 13 |- ( ( ph /\ y e. RR ) -> ( ( 2 x. pi ) e. CC /\ ( sin ` ( y / 2 ) ) e. CC ) )
159		mulcl 9588	. . . . . . . . . . . . 13 |- ( ( ( 2 x. pi ) e. CC /\ ( sin ` ( y / 2 ) ) e. CC ) -> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) e. CC )
160	158, 159	syl 16	. . . . . . . . . . . 12 |- ( ( ph /\ y e. RR ) -> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) e. CC )
161		eqid 2467	. . . . . . . . . . . 12 |- ( y e. RR |-> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) = ( y e. RR |-> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) )
162	160, 161	fmptd 6056	. . . . . . . . . . 11 |- ( ph -> ( y e. RR |-> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) : RR --> CC )
163	42, 162	jca 532	. . . . . . . . . 10 |- ( ph -> ( RR C_ CC /\ ( y e. RR |-> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) : RR --> CC ) )
164	59, 60	dvres 22183	. . . . . . . . . 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 } ) ) ) )
165	163, 58, 164	syl2anc 661	. . . . . . . . 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 } ) ) ) )
166	74	reseq2d 5279	. . . . . . . . . 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 } ) ) )
167	41	sseli 3505	. . . . . . . . . . . . . . . 16 |- ( y e. RR -> y e. CC )
168	44	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. CC -> 1 e. CC )
169	168, 151, 150, 153	div13d 10356	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. CC -> ( ( 1 / 2 ) x. y ) = ( ( y / 2 ) x. 1 ) )
170	154	mulid1d 9625	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. CC -> ( ( y / 2 ) x. 1 ) = ( y / 2 ) )
171	169, 170	eqtrd 2508	. . . . . . . . . . . . . . . . . . 19 |- ( y e. CC -> ( ( 1 / 2 ) x. y ) = ( y / 2 ) )
172	171	fveq2d 5876	. . . . . . . . . . . . . . . . . 18 |- ( y e. CC -> ( sin ` ( ( 1 / 2 ) x. y ) ) = ( sin ` ( y / 2 ) ) )
173	172	oveq2d 6311	. . . . . . . . . . . . . . . . 17 |- ( y e. CC -> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) = ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) )
174	173	eqcomd 2475	. . . . . . . . . . . . . . . 16 |- ( y e. CC -> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) = ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) )
175	167, 174	syl 16	. . . . . . . . . . . . . . 15 |- ( y e. RR -> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) = ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) )
176	175	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ y e. RR ) -> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) = ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) )
177	176	mpteq2dva 4539	. . . . . . . . . . . . 13 |- ( ph -> ( y e. RR |-> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) = ( y e. RR |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) )
178	177	oveq2d 6311	. . . . . . . . . . . 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 ) ) ) ) ) )
179		resmpt 5329	. . . . . . . . . . . . . . . . . 18 |- ( 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 ) ) ) ) )
180	41, 179	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( ( 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 ) ) ) )
181	180	a1i 11	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) ) )
182	181	oveq2d 6311	. . . . . . . . . . . . . . 15 |- ( 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 ) ) ) ) ) )
183	182	eqcomd 2475	. . . . . . . . . . . . . 14 |- ( ph -> ( RR _D ( y e. RR |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) = ( RR _D ( ( y e. CC |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) |` RR ) ) )
184	148	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ y e. CC ) -> ( 2 x. pi ) e. CC )
185	46	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ y e. CC ) -> ( 1 / 2 ) e. CC )
186	185, 80	jca 532	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ y e. CC ) -> ( ( 1 / 2 ) e. CC /\ y e. CC ) )
187		mulcl 9588	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 1 / 2 ) e. CC /\ y e. CC ) -> ( ( 1 / 2 ) x. y ) e. CC )
188	186, 187	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ y e. CC ) -> ( ( 1 / 2 ) x. y ) e. CC )
189		sincl 13739	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 1 / 2 ) x. y ) e. CC -> ( sin ` ( ( 1 / 2 ) x. y ) ) e. CC )
190	188, 189	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ y e. CC ) -> ( sin ` ( ( 1 / 2 ) x. y ) ) e. CC )
191	184, 190	jca 532	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. CC ) -> ( ( 2 x. pi ) e. CC /\ ( sin ` ( ( 1 / 2 ) x. y ) ) e. CC ) )
192		mulcl 9588	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 2 x. pi ) e. CC /\ ( sin ` ( ( 1 / 2 ) x. y ) ) e. CC ) -> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) e. CC )
193	191, 192	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. CC ) -> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) e. CC )
194		eqid 2467	. . . . . . . . . . . . . . . . 17 |- ( y e. CC |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) = ( y e. CC |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) )
195	193, 194	fmptd 6056	. . . . . . . . . . . . . . . 16 |- ( ph -> ( y e. CC |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) : CC --> CC )
196	78, 195	jca 532	. . . . . . . . . . . . . . 15 |- ( ph -> ( RR e. { RR , CC } /\ ( y e. CC |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) : CC --> CC ) )
197	146	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> 2 e. CC )
198	147	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> pi e. CC )
199	197, 198	mulcld 9628	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( 2 x. pi ) e. CC )
200		dvasinbx 31573	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 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 ) ) ) ) )
201	199, 47, 200	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) ) ) ) )
202	146	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ y e. CC ) -> 2 e. CC )
203	147	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ y e. CC ) -> pi e. CC )
204	202, 203, 185	mul32d 9801	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ y e. CC ) -> ( ( 2 x. pi ) x. ( 1 / 2 ) ) = ( ( 2 x. ( 1 / 2 ) ) x. pi ) )
205	44	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ y e. CC ) -> 1 e. CC )
206	152	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ y e. CC ) -> 2 =/= 0 )
207	205, 202, 206	divcan2d 10334	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ y e. CC ) -> ( 2 x. ( 1 / 2 ) ) = 1 )
208	207	oveq1d 6310	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ y e. CC ) -> ( ( 2 x. ( 1 / 2 ) ) x. pi ) = ( 1 x. pi ) )
209	203	mulid2d 9626	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ y e. CC ) -> ( 1 x. pi ) = pi )
210	204, 208, 209	3eqtrd 2512	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ y e. CC ) -> ( ( 2 x. pi ) x. ( 1 / 2 ) ) = pi )
211	171	fveq2d 5876	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( y e. CC -> ( cos ` ( ( 1 / 2 ) x. y ) ) = ( cos ` ( y / 2 ) ) )
212	211	adantl 466	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ y e. CC ) -> ( cos ` ( ( 1 / 2 ) x. y ) ) = ( cos ` ( y / 2 ) ) )
213	210, 212	oveq12d 6313	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ y e. CC ) -> ( ( ( 2 x. pi ) x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. y ) ) ) = ( pi x. ( cos ` ( y / 2 ) ) ) )
214	213	mpteq2dva 4539	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( y e. CC |-> ( ( ( 2 x. pi ) x. ( 1 / 2 ) ) x. ( cos ` ( ( 1 / 2 ) x. y ) ) ) ) = ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) )
215	201, 214	eqtrd 2508	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( CC _D ( y e. CC |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) = ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) )
216		dmeq 5209	. . . . . . . . . . . . . . . . . . 19 |- ( ( CC _D ( y e. CC |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) = ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) -> dom ( CC _D ( y e. CC |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) = dom ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) )
217	215, 216	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( 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 ) ) ) ) )
218	80, 154	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ y e. CC ) -> ( y / 2 ) e. CC )
219		coscl 13740	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( y / 2 ) e. CC -> ( cos ` ( y / 2 ) ) e. CC )
220	218, 219	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ y e. CC ) -> ( cos ` ( y / 2 ) ) e. CC )
221	203, 220	jca 532	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ y e. CC ) -> ( pi e. CC /\ ( cos ` ( y / 2 ) ) e. CC ) )
222		mulcl 9588	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( pi e. CC /\ ( cos ` ( y / 2 ) ) e. CC ) -> ( pi x. ( cos ` ( y / 2 ) ) ) e. CC )
223	221, 222	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ y e. CC ) -> ( pi x. ( cos ` ( y / 2 ) ) ) e. CC )
224		eqid 2467	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) = ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) )
225	223, 224	fmptd 6056	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) : CC --> CC )
226		fdm 5741	. . . . . . . . . . . . . . . . . . 19 |- ( ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) : CC --> CC -> dom ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) = CC )
227	225, 226	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ph -> dom ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) = CC )
228	217, 227	eqtrd 2508	. . . . . . . . . . . . . . . . 17 |- ( ph -> dom ( CC _D ( y e. CC |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) = CC )
229	42, 228	sseqtr4d 3546	. . . . . . . . . . . . . . . 16 |- ( ph -> RR C_ dom ( CC _D ( y e. CC |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) )
230	87, 229	jca 532	. . . . . . . . . . . . . . 15 |- ( ph -> ( CC C_ CC /\ RR C_ dom ( CC _D ( y e. CC |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) ) )
231		dvres3 22185	. . . . . . . . . . . . . . 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 ) )
232	196, 230, 231	syl2anc 661	. . . . . . . . . . . . . 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 ) )
233	215	reseq1d 5278	. . . . . . . . . . . . . 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 ) )
234	183, 232, 233	3eqtrd 2512	. . . . . . . . . . . . 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 ) )
235		resmpt 5329	. . . . . . . . . . . . . . 15 |- ( RR C_ CC -> ( ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) |` RR ) = ( y e. RR |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) )
236	41, 235	ax-mp 5	. . . . . . . . . . . . . 14 |- ( ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) |` RR ) = ( y e. RR |-> ( pi x. ( cos ` ( y / 2 ) ) ) )
237	236	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> ( ( y e. CC |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) |` RR ) = ( y e. RR |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) )
238	234, 237	eqtrd 2508	. . . . . . . . . . . 12 |- ( ph -> ( RR _D ( y e. RR |-> ( ( 2 x. pi ) x. ( sin ` ( ( 1 / 2 ) x. y ) ) ) ) ) = ( y e. RR |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) )
239	178, 238	eqtrd 2508	. . . . . . . . . . 11 |- ( ph -> ( RR _D ( y e. RR |-> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) = ( y e. RR |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) )
240	239	reseq1d 5278	. . . . . . . . . 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 } ) ) )
241		resmpt 5329	. . . . . . . . . . 11 |- ( ( ( A (,) B ) \ { Y } ) C_ RR -> ( ( y e. RR |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) |` ( ( A (,) B ) \ { Y } ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) )
242	4, 241	syl 16	. . . . . . . . . 10 |- ( ph -> ( ( y e. RR |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) |` ( ( A (,) B ) \ { Y } ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( pi x. ( cos ` ( y / 2 ) ) ) ) )
243	166, 240, 242	3eqtrd 2512	. . . . . . . . 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 ) ) ) ) )
244	145, 165, 243	3eqtrd 2512	. . . . . . . 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 ) ) ) ) )
245	244	eqcomd 2475	. . . . . . 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 ) ) ) ) ) )
246	28	a1i 11	. . . . . . . . 9 |- ( ph -> G = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) )
247	246	oveq2d 6311	. . . . . . . 8 |- ( ph -> ( RR _D G ) = ( RR _D ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) )
248	247	eqcomd 2475	. . . . . . 7 |- ( ph -> ( RR _D ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( 2 x. pi ) x. ( sin ` ( y / 2 ) ) ) ) ) = ( RR _D G ) )
249	140, 245, 248	3eqtrrd 2513	. . . . . 6 |- ( ph -> ( RR _D G ) = I )
250	249	dmeqd 5211	. . . . 5 |- ( ph -> dom ( RR _D G ) = dom I )
251	131, 223	syl 16	. . . . . . 7 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( pi x. ( cos ` ( y / 2 ) ) ) e. CC )
252	251, 139	fmptd 6056	. . . . . 6 |- ( ph -> I : ( ( A (,) B ) \ { Y } ) --> CC )
253		fdm 5741	. . . . . 6 |- ( I : ( ( A (,) B ) \ { Y } ) --> CC -> dom I = ( ( A (,) B ) \ { Y } ) )
254	252, 253	syl 16	. . . . 5 |- ( ph -> dom I = ( ( A (,) B ) \ { Y } ) )
255	250, 254	eqtr2d 2509	. . . 4 |- ( ph -> ( ( A (,) B ) \ { Y } ) = dom ( RR _D G ) )
256		eqimss 3561	. . . 4 |- ( ( ( A (,) B ) \ { Y } ) = dom ( RR _D G ) -> ( ( A (,) B ) \ { Y } ) C_ dom ( RR _D G ) )
257	255, 256	syl 16	. . 3 |- ( ph -> ( ( A (,) B ) \ { Y } ) C_ dom ( RR _D G ) )
258	131, 81	syl 16	. . . . . . . 8 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. y ) e. CC )
259	258	ralrimiva 2881	. . . . . . 7 |- ( ph -> A. y e. ( ( A (,) B ) \ { Y } ) ( ( N + ( 1 / 2 ) ) x. y ) e. CC )
260		eqid 2467	. . . . . . . 8 |- ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) = ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) )
261	260	fnmpt 5713	. . . . . . 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 } ) )
262	259, 261	syl 16	. . . . . 6 |- ( ph -> ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) Fn ( ( A (,) B ) \ { Y } ) )
263		eqidd 2468	. . . . . . . . . 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 ) ) )
264		simpr 461	. . . . . . . . . . 11 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ y = w ) -> y = w )
265	264	oveq2d 6311	. . . . . . . . . 10 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ y = w ) -> ( ( N + ( 1 / 2 ) ) x. y ) = ( ( N + ( 1 / 2 ) ) x. w ) )
266		simpr 461	. . . . . . . . . 10 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> w e. ( ( A (,) B ) \ { Y } ) )
267	43	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> N e. CC )
268	44	a1i 11	. . . . . . . . . . . . 13 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> 1 e. CC )
269	268	halfcld 10795	. . . . . . . . . . . 12 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( 1 / 2 ) e. CC )
270	267, 269	addcld 9627	. . . . . . . . . . 11 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( N + ( 1 / 2 ) ) e. CC )
271	1	sseli 3505	. . . . . . . . . . . . . 14 |- ( w e. ( ( A (,) B ) \ { Y } ) -> w e. ( A (,) B ) )
272	2	sseli 3505	. . . . . . . . . . . . . 14 |- ( w e. ( A (,) B ) -> w e. RR )
273	271, 272	syl 16	. . . . . . . . . . . . 13 |- ( w e. ( ( A (,) B ) \ { Y } ) -> w e. RR )
274	41, 273	sseldi 3507	. . . . . . . . . . . 12 |- ( w e. ( ( A (,) B ) \ { Y } ) -> w e. CC )
275	274	adantl 466	. . . . . . . . . . 11 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> w e. CC )
276	270, 275	mulcld 9628	. . . . . . . . . 10 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. w ) e. CC )
277	263, 265, 266, 276	fvmptd 5962	. . . . . . . . 9 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) ` w ) = ( ( N + ( 1 / 2 ) ) x. w ) )
278		simpll 753	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> ph )
279		simpr 461	. . . . . . . . . . . . . 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 ) )
280	275	adantr 465	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> w e. CC )
281	41, 67	sseldi 3507	. . . . . . . . . . . . . . . 16 |- ( ph -> Y e. CC )
282	278, 281	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> Y e. CC )
283		0re 9608	. . . . . . . . . . . . . . . . . . 19 |- 0 e. RR
284	283	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ph -> 0 e. RR )
285	5	nnred 10563	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N e. RR )
286	8	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> 1 e. RR )
287	286	rehalfcld 10797	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 / 2 ) e. RR )
288	285, 287	readdcld 9635	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( N + ( 1 / 2 ) ) e. RR )
289	5	nngt0d 10591	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> 0 < N )
290		2rp 11237	. . . . . . . . . . . . . . . . . . . . . 22 |- 2 e. RR+
291	290	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> 2 e. RR+ )
292	291	rpreccld 11278	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( 1 / 2 ) e. RR+ )
293	285, 292	ltaddrpd 11297	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> N < ( N + ( 1 / 2 ) ) )
294	284, 285, 288, 289, 293	lttrd 9754	. . . . . . . . . . . . . . . . . 18 |- ( ph -> 0 < ( N + ( 1 / 2 ) ) )
295	284, 294	gtned 9731	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( N + ( 1 / 2 ) ) =/= 0 )
296	48, 295	jca 532	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( N + ( 1 / 2 ) ) e. CC /\ ( N + ( 1 / 2 ) ) =/= 0 ) )
297	296	ad2antrr 725	. . . . . . . . . . . . . . 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 ) )
298		mulcan 10198	. . . . . . . . . . . . . . 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 ) )
299	280, 282, 297, 298	syl3anc 1228	. . . . . . . . . . . . . 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 ) )
300	279, 299	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> w = Y )
301		oveq1 6302	. . . . . . . . . . . . . . 15 |- ( w = Y -> ( w mod ( 2 x. pi ) ) = ( Y mod ( 2 x. pi ) ) )
302	301	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ w = Y ) -> ( w mod ( 2 x. pi ) ) = ( Y mod ( 2 x. pi ) ) )
303		dirkercncflem2.ymod	. . . . . . . . . . . . . . 15 |- ( ph -> ( Y mod ( 2 x. pi ) ) = 0 )
304	303	adantr 465	. . . . . . . . . . . . . 14 |- ( ( ph /\ w = Y ) -> ( Y mod ( 2 x. pi ) ) = 0 )
305	302, 304	eqtrd 2508	. . . . . . . . . . . . 13 |- ( ( ph /\ w = Y ) -> ( w mod ( 2 x. pi ) ) = 0 )
306	278, 300, 305	syl2anc 661	. . . . . . . . . . . 12 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> ( w mod ( 2 x. pi ) ) = 0 )
307		nfv 1683	. . . . . . . . . . . . . . 15 |- F/ y ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( w mod ( 2 x. pi ) ) =/= 0 )
308		eleq1 2539	. . . . . . . . . . . . . . . . 17 |- ( y = w -> ( y e. ( ( A (,) B ) \ { Y } ) <-> w e. ( ( A (,) B ) \ { Y } ) ) )
309	308	anbi2d 703	. . . . . . . . . . . . . . . 16 |- ( y = w -> ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) <-> ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) ) )
310		oveq1 6302	. . . . . . . . . . . . . . . . 17 |- ( y = w -> ( y mod ( 2 x. pi ) ) = ( w mod ( 2 x. pi ) ) )
311	310	neeq1d 2744	. . . . . . . . . . . . . . . 16 |- ( y = w -> ( ( y mod ( 2 x. pi ) ) =/= 0 <-> ( w mod ( 2 x. pi ) ) =/= 0 ) )
312	309, 311	imbi12d 320	. . . . . . . . . . . . . . 15 |- ( 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 ) ) )
313	1	sseli 3505	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. ( ( A (,) B ) \ { Y } ) -> y e. ( A (,) B ) )
314		elioore 11571	. . . . . . . . . . . . . . . . . . . . . 22 |- ( y e. ( A (,) B ) -> y e. RR )
315	313, 314, 167	3syl 20	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ( A (,) B ) \ { Y } ) -> y e. CC )
316	146	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ( A (,) B ) \ { Y } ) -> 2 e. CC )
317	147	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ( A (,) B ) \ { Y } ) -> pi e. CC )
318	152	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ( A (,) B ) \ { Y } ) -> 2 =/= 0 )
319		pipos 22720	. . . . . . . . . . . . . . . . . . . . . . 23 |- 0 < pi
320	283, 319	gtneii 9708	. . . . . . . . . . . . . . . . . . . . . 22 |- pi =/= 0
321	320	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( y e. ( ( A (,) B ) \ { Y } ) -> pi =/= 0 )
322	315, 316, 317, 318, 321	divdiv1d 10363	. . . . . . . . . . . . . . . . . . . 20 |- ( y e. ( ( A (,) B ) \ { Y } ) -> ( ( y / 2 ) / pi ) = ( y / ( 2 x. pi ) ) )
323	322	eqcomd 2475	. . . . . . . . . . . . . . . . . . 19 |- ( y e. ( ( A (,) B ) \ { Y } ) -> ( y / ( 2 x. pi ) ) = ( ( y / 2 ) / pi ) )
324	323	adantl 466	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( y / ( 2 x. pi ) ) = ( ( y / 2 ) / pi ) )
325		dirkercncflem2.yne0	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( sin ` ( y / 2 ) ) =/= 0 )
326	325	neneqd 2669	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> -. ( sin ` ( y / 2 ) ) = 0 )
327	130, 154	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( y / 2 ) e. CC )
328		sineq0 22780	. . . . . . . . . . . . . . . . . . . 20 |- ( ( y / 2 ) e. CC -> ( ( sin ` ( y / 2 ) ) = 0 <-> ( ( y / 2 ) / pi ) e. ZZ ) )
329	327, 328	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( sin ` ( y / 2 ) ) = 0 <-> ( ( y / 2 ) / pi ) e. ZZ ) )
330	326, 329	mtbid 300	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> -. ( ( y / 2 ) / pi ) e. ZZ )
331	324, 330	eqneltrd 2576	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> -. ( y / ( 2 x. pi ) ) e. ZZ )
332	18, 319	pm3.2i 455	. . . . . . . . . . . . . . . . . . . . . 22 |- ( pi e. RR /\ 0 < pi )
333		elrp 11234	. . . . . . . . . . . . . . . . . . . . . 22 |- ( pi e. RR+ <-> ( pi e. RR /\ 0 < pi ) )
334	332, 333	mpbir 209	. . . . . . . . . . . . . . . . . . . . 21 |- pi e. RR+
335	290, 334	pm3.2i 455	. . . . . . . . . . . . . . . . . . . 20 |- ( 2 e. RR+ /\ pi e. RR+ )
336		rpmulcl 11253	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 2 e. RR+ /\ pi e. RR+ ) -> ( 2 x. pi ) e. RR+ )
337	335, 336	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 |- ( 2 x. pi ) e. RR+
338	337	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( 2 x. pi ) e. RR+ )
339		mod0 11983	. . . . . . . . . . . . . . . . . 18 |- ( ( y e. RR /\ ( 2 x. pi ) e. RR+ ) -> ( ( y mod ( 2 x. pi ) ) = 0 <-> ( y / ( 2 x. pi ) ) e. ZZ ) )
340	12, 338, 339	syl2anc 661	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( ( y mod ( 2 x. pi ) ) = 0 <-> ( y / ( 2 x. pi ) ) e. ZZ ) )
341	331, 340	mtbird 301	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> -. ( y mod ( 2 x. pi ) ) = 0 )
342	341	neqned 2670	. . . . . . . . . . . . . . 15 |- ( ( ph /\ y e. ( ( A (,) B ) \ { Y } ) ) -> ( y mod ( 2 x. pi ) ) =/= 0 )
343	307, 312, 342	chvar 1982	. . . . . . . . . . . . . 14 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( w mod ( 2 x. pi ) ) =/= 0 )
344	343	neneqd 2669	. . . . . . . . . . . . 13 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> -. ( w mod ( 2 x. pi ) ) = 0 )
345	344	adantr 465	. . . . . . . . . . . 12 |- ( ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) /\ ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) ) -> -. ( w mod ( 2 x. pi ) ) = 0 )
346	306, 345	pm2.65da 576	. . . . . . . . . . 11 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> -. ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) )
347	48, 281	mulcld 9628	. . . . . . . . . . . . 13 |- ( ph -> ( ( N + ( 1 / 2 ) ) x. Y ) e. CC )
348	347	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. Y ) e. CC )
349		elsnc2g 4063	. . . . . . . . . . . 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 ) ) )
350	348, 349	syl 16	. . . . . . . . . . 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 ) ) )
351	346, 350	mtbird 301	. . . . . . . . . 10 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> -. ( ( N + ( 1 / 2 ) ) x. w ) e. { ( ( N + ( 1 / 2 ) ) x. Y ) } )
352	276, 351	eldifd 3492	. . . . . . . . 9 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( ( N + ( 1 / 2 ) ) x. w ) e. ( CC \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) )
353	277, 352	eqeltrd 2555	. . . . . . . 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 ) } ) )
354		sinf 13737	. . . . . . . . . . . 12 |- sin : CC --> CC
355	354	fdmi 5742	. . . . . . . . . . 11 |- dom sin = CC
356	355	eqcomi 2480	. . . . . . . . . 10 |- CC = dom sin
357	356	a1i 11	. . . . . . . . 9 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> CC = dom sin )
358	357	difeq1d 3626	. . . . . . . 8 |- ( ( ph /\ w e. ( ( A (,) B ) \ { Y } ) ) -> ( CC \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) = ( dom sin \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) )
359	353, 358	eleqtrd 2557	. . . . . . 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 ) } ) )
360	359	ralrimiva 2881	. . . . . 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 ) } ) )
361		fnfvrnss 6060	. . . . . 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 ) } ) )
362	262, 360, 361	syl2anc 661	. . . . 5 |- ( ph -> ran ( y e. ( ( A (,) B ) \ { Y } ) |-> ( ( N + ( 1 / 2 ) ) x. y ) ) C_ ( dom sin \ { ( ( N + ( 1 / 2 ) ) x. Y ) } ) )
363		id 22	. . . . . . . . 9 |- ( ph -> ph )
364		uncom 3653	. . . . . . . . . . 11 |- ( ( ( A (,) B ) \ { Y } ) u. { Y } ) = ( { Y } u. ( ( A (,) B ) \ { Y } ) )
365	364	a1i 11	. . . . . . . . . 10 |- ( ph -> ( ( ( A (,) B ) \ { Y } ) u. { Y } ) = ( { Y } u. ( ( A (,) B ) \ { Y } ) ) )
366	32	snssd 4178	. . . . . . . . . . 11 |- ( ph -> { Y } C_ ( A (,) B ) )
367		undif 3913	. . . . . . . . . . 11 |- ( { Y } C_ ( A (,) B ) <-> ( { Y } u. ( ( A (,) B ) \ { Y } ) ) = ( A (,) B ) )
368	366, 367	sylib 196	. . . . . . . . . 10 |- ( ph -> ( { Y } u. ( ( A (,) B ) \ { Y } ) ) = ( A (,) B ) )
369	365, 368	eqtrd 2508	. . . . . . . . 9 |- ( ph -> ( ( ( A (,) B ) \ { Y } ) u. { Y } ) = ( A (,) B ) )
370	363, 369	syl 16	. . . . . . . 8 |- ( ph -> ( ( ( A (,) B ) \ { Y } ) u. { Y } ) = ( A (,) B ) )
371	370	mpteq1d 4534	. . . . . . 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 ) ) ) )
372		iftrue 3951	. . . . . . . . . . . . 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 ) )
373		oveq2 6303	. . . . . . . . . . . . . 14 |- ( w = Y -> ( ( N + ( 1 / 2 ) ) x. w ) = ( ( N + ( 1 / 2 ) ) x. Y ) )
374	373	eqcomd 2475	. . . . . . . . . . . . 13 |- ( w = Y -> ( ( N + ( 1 / 2 ) ) x. Y ) = ( ( N + ( 1 / 2 ) ) x. w ) )
375	372, 374	eqtrd 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 ) )
376	375	adantl 466	. . . . . . . . . . 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 ) )
377		iffalse 3954	. . . . . . . . . . . . 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 ) )
378	377	adantl 466	. . . . . . . . . . . 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 ) )
379		eqidd 2468	. . . . . . . . . . . . 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 ) ) )
380		oveq2 6303	. . . . . . . . . . . . . 14 |- ( y = w -> ( ( N + ( 1 / 2 ) ) x. y ) = ( ( N + ( 1 / 2 ) ) x. w ) )
381	380	adantl 466	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ w e. ( A (,) B ) ) /\ -. w = Y ) /\ y = w ) -> ( ( N + ( 1 / 2 ) ) x. y ) = ( ( N + ( 1 / 2 ) ) x. w ) )
382		simpl 457	. . . . . . . . . . . . . . . 16 |- ( ( w e. ( A (,) B ) /\ -. w = Y ) -> w e. ( A (,) B ) )
383		id 22	. . . . . . . . . . . . . . . . . 18 |- ( -. w = Y -> -. w = Y )
384		elsn 4047	. . . . . . . . . . . . . . . . . 18 |- ( w e. { Y } <-> w = Y )
385	383, 384	sylnibr 305	. . . . . . . . . . . . . . . . 17 |- ( -. w = Y -> -. w e. { Y } )
386	385	adantl 466	. . . . . . . . . . . . . . . 16 |- ( ( w e. ( A (,) B ) /\ -. w = Y ) -> -. w e. { Y } )
387	382, 386	jca 532	. . . . . . . . . . . . . . 15 |- ( ( w e. ( A (,) B ) /\ -. w = Y ) -> ( w e. ( A (,) B ) /\ -. w e. { Y } ) )
388		eldif 3491	. . . . . . . . . . . . . . 15 |- ( w e. ( ( A (,) B ) \ { Y } ) <-> ( w e. (