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	$⊢ D = (n \in ℕ ⟼ (y \in ℝ ⟼ if (y \mod 2 π = 0, \frac{2 n + 1}{2 π}, \frac{\sin (n + (\frac{1}{2})) y}{2 π \sin (\frac{y}{2})})))$
	dirkercncflem2.f	$⊢ F = (y \in ((A, B) ∖ \{Y\}) ⟼ \sin (N + (\frac{1}{2})) y)$
	dirkercncflem2.g	$⊢ G = (y \in ((A, B) ∖ \{Y\}) ⟼ 2 π \sin (\frac{y}{2}))$
	dirkercncflem2.yne0	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \sin (\frac{y}{2}) \neq 0$
	dirkercncflem2.h	$⊢ H = (y \in ((A, B) ∖ \{Y\}) ⟼ (N + (\frac{1}{2})) \cos (N + (\frac{1}{2})) y)$
	dirkercncflem2.i	$⊢ I = (y \in ((A, B) ∖ \{Y\}) ⟼ π \cos (\frac{y}{2}))$
	dirkercncflem2.l	$⊢ L = (w \in (A, B) ⟼ \frac{(N + (\frac{1}{2})) \cos (N + (\frac{1}{2})) w}{π \cos (\frac{w}{2})})$
	dirkercncflem2.n	$⊢ φ \to N \in ℕ$
	dirkercncflem2.y	$⊢ φ \to Y \in (A, B)$
	dirkercncflem2.ymod	$⊢ φ \to Y \mod 2 π = 0$
	dirkercncflem2.11	$⊢ (φ \land y \in ((A, B) ∖ \{Y\})) \to \cos (\frac{y}{2}) \neq 0$
Assertion	dirkercncflem2	$⊢ φ \to D (N) (Y) \in (({D (N) ↾}_{((A, B) ∖ \{Y\})}) {lim}_{ℂ} Y)$

Proof

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

Metamath Proof Explorer

Theorem dirkercncflem2

Proof