Theorem dirkercncflem2

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

	Ref	Expression
Hypotheses	dirkercncflem2.d	⊢ 𝐷 = ( 𝑛 ∈ ℕ ↦ ( 𝑦 ∈ ℝ ↦ if ( ( 𝑦 mod ( 2 · π ) ) = 0 , ( ( ( 2 · 𝑛 ) + 1 ) / ( 2 · π ) ) , ( ( sin ‘ ( ( 𝑛 + ( 1 / 2 ) ) · 𝑦 ) ) / ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) ) ) ) )
	dirkercncflem2.f	⊢ 𝐹 = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( sin ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) )
	dirkercncflem2.g	⊢ 𝐺 = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 2 · π ) · ( sin ‘ ( 𝑦 / 2 ) ) ) )
	dirkercncflem2.yne0	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( sin ‘ ( 𝑦 / 2 ) ) ≠ 0 )
	dirkercncflem2.h	⊢ 𝐻 = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑦 ) ) ) )
	dirkercncflem2.i	⊢ 𝐼 = ( 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ↦ ( π · ( cos ‘ ( 𝑦 / 2 ) ) ) )
	dirkercncflem2.l	⊢ 𝐿 = ( 𝑤 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( ( 𝑁 + ( 1 / 2 ) ) · ( cos ‘ ( ( 𝑁 + ( 1 / 2 ) ) · 𝑤 ) ) ) / ( π · ( cos ‘ ( 𝑤 / 2 ) ) ) ) )
	dirkercncflem2.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
	dirkercncflem2.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝐴 (,) 𝐵 ) )
	dirkercncflem2.ymod	⊢ ( 𝜑 → ( 𝑌 mod ( 2 · π ) ) = 0 )
	dirkercncflem2.11	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) → ( cos ‘ ( 𝑦 / 2 ) ) ≠ 0 )
Assertion	dirkercncflem2	⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝑁 ) ‘ 𝑌 ) ∈ ( ( ( 𝐷 ‘ 𝑁 ) ↾ ( ( 𝐴 (,) 𝐵 ) ∖ { 𝑌 } ) ) limℂ 𝑌 ) )

Proof

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