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