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

Metamath Proof Explorer

Theorem dirkercncflem2

Proof