fourierdlem62

Description: The function K is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Hypothesis	fourierdlem62.k	$⊢ K = (y \in [- π, π] ⟼ if (y = 0, 1, \frac{y}{2 \sin (\frac{y}{2})}))$
	Assertion	fourierdlem62	$⊢ K : [- π, π] \underset{cn}{⟶} ℝ$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem62.k	$⊢ K = (y \in [- π, π] ⟼ if (y = 0, 1, \frac{y}{2 \sin (\frac{y}{2})}))$
2		eqeq1	$⊢ y = s \to (y = 0 \leftrightarrow s = 0)$
3		id	$⊢ y = s \to y = s$
4		oveq1	$⊢ y = s \to \frac{y}{2} = \frac{s}{2}$
5	4	fveq2d	$⊢ y = s \to \sin (\frac{y}{2}) = \sin (\frac{s}{2})$
6	5	oveq2d	$⊢ y = s \to 2 \sin (\frac{y}{2}) = 2 \sin (\frac{s}{2})$
7	3 6	oveq12d	$⊢ y = s \to \frac{y}{2 \sin (\frac{y}{2})} = \frac{s}{2 \sin (\frac{s}{2})}$
8	2 7	ifbieq2d	$⊢ y = s \to if (y = 0, 1, \frac{y}{2 \sin (\frac{y}{2})}) = if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})$
9	8	cbvmptv	$⊢ (y \in [- π, π] ⟼ if (y = 0, 1, \frac{y}{2 \sin (\frac{y}{2})})) = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
10	1 9	eqtri	$⊢ K = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
11	10	fourierdlem43	$⊢ K : [- π, π] ⟶ ℝ$
12		ax-resscn	$⊢ ℝ \subseteq ℂ$
13		fss	$⊢ (K : [- π, π] ⟶ ℝ \land ℝ \subseteq ℂ) \to K : [- π, π] ⟶ ℂ$
14	11 12 13	mp2an	$⊢ K : [- π, π] ⟶ ℂ$
15	14	a1i	$⊢ s = 0 \to K : [- π, π] ⟶ ℂ$
16		difss	$⊢ (- π, π) ∖ \{0\} \subseteq (- π, π)$
17		elioore	$⊢ s \in (- π, π) \to s \in ℝ$
18	17	ssriv	$⊢ (- π, π) \subseteq ℝ$
19	16 18	sstri	$⊢ (- π, π) ∖ \{0\} \subseteq ℝ$
20	19	a1i	$⊢ ⊤ \to (- π, π) ∖ \{0\} \subseteq ℝ$
21		eqid	$⊢ (x \in ((- π, π) ∖ \{0\}) ⟼ x) = (x \in ((- π, π) ∖ \{0\}) ⟼ x)$
22	19	sseli	$⊢ x \in ((- π, π) ∖ \{0\}) \to x \in ℝ$
23	21 22	fmpti	$⊢ (x \in ((- π, π) ∖ \{0\}) ⟼ x) : (- π, π) ∖ \{0\} ⟶ ℝ$
24	23	a1i	$⊢ ⊤ \to (x \in ((- π, π) ∖ \{0\}) ⟼ x) : (- π, π) ∖ \{0\} ⟶ ℝ$
25		eqid	$⊢ (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) = (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2}))$
26		2re	$⊢ 2 \in ℝ$
27	26	a1i	$⊢ x \in ((- π, π) ∖ \{0\}) \to 2 \in ℝ$
28	22	rehalfcld	$⊢ x \in ((- π, π) ∖ \{0\}) \to \frac{x}{2} \in ℝ$
29	28	resincld	$⊢ x \in ((- π, π) ∖ \{0\}) \to \sin (\frac{x}{2}) \in ℝ$
30	27 29	remulcld	$⊢ x \in ((- π, π) ∖ \{0\}) \to 2 \sin (\frac{x}{2}) \in ℝ$
31	25 30	fmpti	$⊢ (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) : (- π, π) ∖ \{0\} ⟶ ℝ$
32	31	a1i	$⊢ ⊤ \to (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) : (- π, π) ∖ \{0\} ⟶ ℝ$
33		iooretop	$⊢ (- π, π) \in topGen (ran (.))$
34	33	a1i	$⊢ ⊤ \to (- π, π) \in topGen (ran (.))$
35		0re	$⊢ 0 \in ℝ$
36		negpilt0	$⊢ - π < 0$
37		pipos	$⊢ 0 < π$
38		pire	$⊢ π \in ℝ$
39	38	renegcli	$⊢ - π \in ℝ$
40	39	rexri	$⊢ - π \in ℝ^{*}$
41	38	rexri	$⊢ π \in ℝ^{*}$
42		elioo2	$⊢ (- π \in ℝ^{} \land π \in ℝ^{}) \to (0 \in (- π, π) \leftrightarrow (0 \in ℝ \land - π < 0 \land 0 < π))$
43	40 41 42	mp2an	$⊢ 0 \in (- π, π) \leftrightarrow (0 \in ℝ \land - π < 0 \land 0 < π)$
44	35 36 37 43	mpbir3an	$⊢ 0 \in (- π, π)$
45	44	a1i	$⊢ ⊤ \to 0 \in (- π, π)$
46		eqid	$⊢ (- π, π) ∖ \{0\} = (- π, π) ∖ \{0\}$
47		1ex	$⊢ 1 \in V$
48		eqid	$⊢ (x \in ((- π, π) ∖ \{0\}) ⟼ 1) = (x \in ((- π, π) ∖ \{0\}) ⟼ 1)$
49	47 48	dmmpti	$⊢ dom (x \in ((- π, π) ∖ \{0\}) ⟼ 1) = (- π, π) ∖ \{0\}$
50		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
51	50	a1i	$⊢ ⊤ \to ℝ \in \{ℝ, ℂ\}$
52	12	sseli	$⊢ x \in ℝ \to x \in ℂ$
53	52	adantl	$⊢ (⊤ \land x \in ℝ) \to x \in ℂ$
54		1red	$⊢ (⊤ \land x \in ℝ) \to 1 \in ℝ$
55	51	dvmptid	$⊢ ⊤ \to \frac{d (x \in ℝ⟼ x)}{d_{ℝ} x} = (x \in ℝ ⟼ 1)$
56		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
57	56	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
58		sncldre	$⊢ 0 \in ℝ \to \{0\} \in Clsd (topGen (ran (.)))$
59	35 58	ax-mp	$⊢ \{0\} \in Clsd (topGen (ran (.)))$
60		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
61	60	toponunii	$⊢ ℝ = ⋃ topGen (ran (.))$
62	61	difopn	$⊢ ((- π, π) \in topGen (ran (.)) \land \{0\} \in Clsd (topGen (ran (.)))) \to (- π, π) ∖ \{0\} \in topGen (ran (.))$
63	33 59 62	mp2an	$⊢ (- π, π) ∖ \{0\} \in topGen (ran (.))$
64	63	a1i	$⊢ ⊤ \to (- π, π) ∖ \{0\} \in topGen (ran (.))$
65	51 53 54 55 20 57 56 64	dvmptres	$⊢ ⊤ \to \frac{d (x \in ((- π, π) ∖ \{0\})⟼ x)}{d_{ℝ} x} = (x \in ((- π, π) ∖ \{0\}) ⟼ 1)$
66	65	mptru	$⊢ \frac{d (x \in ((- π, π) ∖ \{0\})⟼ x)}{d_{ℝ} x} = (x \in ((- π, π) ∖ \{0\}) ⟼ 1)$
67	66	eqcomi	$⊢ (x \in ((- π, π) ∖ \{0\}) ⟼ 1) = \frac{d (x \in ((- π, π) ∖ \{0\})⟼ x)}{d_{ℝ} x}$
68	67	dmeqi	$⊢ dom (x \in ((- π, π) ∖ \{0\}) ⟼ 1) = dom \frac{d (x \in ((- π, π) ∖ \{0\})⟼ x)}{d_{ℝ} x}$
69	49 68	eqtr3i	$⊢ (- π, π) ∖ \{0\} = dom \frac{d (x \in ((- π, π) ∖ \{0\})⟼ x)}{d_{ℝ} x}$
70	69	eqimssi	$⊢ (- π, π) ∖ \{0\} \subseteq dom \frac{d (x \in ((- π, π) ∖ \{0\})⟼ x)}{d_{ℝ} x}$
71	70	a1i	$⊢ ⊤ \to (- π, π) ∖ \{0\} \subseteq dom \frac{d (x \in ((- π, π) ∖ \{0\})⟼ x)}{d_{ℝ} x}$
72		fvex	$⊢ \cos (\frac{x}{2}) \in V$
73		eqid	$⊢ (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2})) = (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2}))$
74	72 73	dmmpti	$⊢ dom (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2})) = (- π, π) ∖ \{0\}$
75		2cnd	$⊢ (⊤ \land x \in ℝ) \to 2 \in ℂ$
76	53	halfcld	$⊢ (⊤ \land x \in ℝ) \to \frac{x}{2} \in ℂ$
77	76	sincld	$⊢ (⊤ \land x \in ℝ) \to \sin (\frac{x}{2}) \in ℂ$
78	75 77	mulcld	$⊢ (⊤ \land x \in ℝ) \to 2 \sin (\frac{x}{2}) \in ℂ$
79	76	coscld	$⊢ (⊤ \land x \in ℝ) \to \cos (\frac{x}{2}) \in ℂ$
80		2cnd	$⊢ x \in ℝ \to 2 \in ℂ$
81		2ne0	$⊢ 2 \neq 0$
82	81	a1i	$⊢ x \in ℝ \to 2 \neq 0$
83	52 80 82	divrec2d	$⊢ x \in ℝ \to \frac{x}{2} = (\frac{1}{2}) x$
84	83	fveq2d	$⊢ x \in ℝ \to \sin (\frac{x}{2}) = \sin (\frac{1}{2}) x$
85	84	oveq2d	$⊢ x \in ℝ \to 2 \sin (\frac{x}{2}) = 2 \sin (\frac{1}{2}) x$
86	85	mpteq2ia	$⊢ (x \in ℝ ⟼ 2 \sin (\frac{x}{2})) = (x \in ℝ ⟼ 2 \sin (\frac{1}{2}) x)$
87	86	oveq2i	$⊢ \frac{d (x \in ℝ⟼ 2 \sin (\frac{x}{2}))}{d_{ℝ} x} = \frac{d (x \in ℝ⟼ 2 \sin (\frac{1}{2}) x)}{d_{ℝ} x}$
88		resmpt	$⊢ ℝ \subseteq ℂ \to {(x \in ℂ ⟼ 2 \sin (\frac{1}{2}) x) ↾}_{ℝ} = (x \in ℝ ⟼ 2 \sin (\frac{1}{2}) x)$
89	12 88	ax-mp	$⊢ {(x \in ℂ ⟼ 2 \sin (\frac{1}{2}) x) ↾}_{ℝ} = (x \in ℝ ⟼ 2 \sin (\frac{1}{2}) x)$
90	89	eqcomi	$⊢ (x \in ℝ ⟼ 2 \sin (\frac{1}{2}) x) = {(x \in ℂ ⟼ 2 \sin (\frac{1}{2}) x) ↾}_{ℝ}$
91	90	oveq2i	$⊢ \frac{d (x \in ℝ⟼ 2 \sin (\frac{1}{2}) x)}{d_{ℝ} x} = ℝ D ({(x \in ℂ ⟼ 2 \sin (\frac{1}{2}) x) ↾}_{ℝ})$
92		eqid	$⊢ (x \in ℂ ⟼ 2 \sin (\frac{1}{2}) x) = (x \in ℂ ⟼ 2 \sin (\frac{1}{2}) x)$
93		2cnd	$⊢ x \in ℂ \to 2 \in ℂ$
94		halfcn	$⊢ \frac{1}{2} \in ℂ$
95	94	a1i	$⊢ x \in ℂ \to \frac{1}{2} \in ℂ$
96		id	$⊢ x \in ℂ \to x \in ℂ$
97	95 96	mulcld	$⊢ x \in ℂ \to (\frac{1}{2}) x \in ℂ$
98	97	sincld	$⊢ x \in ℂ \to \sin (\frac{1}{2}) x \in ℂ$
99	93 98	mulcld	$⊢ x \in ℂ \to 2 \sin (\frac{1}{2}) x \in ℂ$
100	92 99	fmpti	$⊢ (x \in ℂ ⟼ 2 \sin (\frac{1}{2}) x) : ℂ ⟶ ℂ$
101		eqid	$⊢ (x \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) x) = (x \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) x)$
102		2cn	$⊢ 2 \in ℂ$
103	102 94	mulcli	$⊢ 2 (\frac{1}{2}) \in ℂ$
104	103	a1i	$⊢ x \in ℂ \to 2 (\frac{1}{2}) \in ℂ$
105	97	coscld	$⊢ x \in ℂ \to \cos (\frac{1}{2}) x \in ℂ$
106	104 105	mulcld	$⊢ x \in ℂ \to 2 (\frac{1}{2}) \cos (\frac{1}{2}) x \in ℂ$
107	106	adantl	$⊢ (⊤ \land x \in ℂ) \to 2 (\frac{1}{2}) \cos (\frac{1}{2}) x \in ℂ$
108	101 107	dmmptd	$⊢ ⊤ \to dom (x \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) x) = ℂ$
109	108	mptru	$⊢ dom (x \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) x) = ℂ$
110	12 109	sseqtrri	$⊢ ℝ \subseteq dom (x \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) x)$
111		dvasinbx	$⊢ (2 \in ℂ \land \frac{1}{2} \in ℂ) \to \frac{d (x \in ℂ⟼ 2 \sin (\frac{1}{2}) x)}{d_{ℂ} x} = (x \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) x)$
112	102 94 111	mp2an	$⊢ \frac{d (x \in ℂ⟼ 2 \sin (\frac{1}{2}) x)}{d_{ℂ} x} = (x \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) x)$
113	112	dmeqi	$⊢ dom \frac{d (x \in ℂ⟼ 2 \sin (\frac{1}{2}) x)}{d_{ℂ} x} = dom (x \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) x)$
114	110 113	sseqtrri	$⊢ ℝ \subseteq dom \frac{d (x \in ℂ⟼ 2 \sin (\frac{1}{2}) x)}{d_{ℂ} x}$
115		dvcnre	$⊢ ((x \in ℂ ⟼ 2 \sin (\frac{1}{2}) x) : ℂ ⟶ ℂ \land ℝ \subseteq dom \frac{d (x \in ℂ⟼ 2 \sin (\frac{1}{2}) x)}{d_{ℂ} x}) \to ℝ D ({(x \in ℂ ⟼ 2 \sin (\frac{1}{2}) x) ↾}_{ℝ}) = {\frac{d (x \in ℂ⟼ 2 \sin (\frac{1}{2}) x)}{d_{ℂ} x} ↾}_{ℝ}$
116	100 114 115	mp2an	$⊢ ℝ D ({(x \in ℂ ⟼ 2 \sin (\frac{1}{2}) x) ↾}_{ℝ}) = {\frac{d (x \in ℂ⟼ 2 \sin (\frac{1}{2}) x)}{d_{ℂ} x} ↾}_{ℝ}$
117	112	reseq1i	$⊢ {\frac{d (x \in ℂ⟼ 2 \sin (\frac{1}{2}) x)}{d_{ℂ} x} ↾}_{ℝ} = {(x \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) x) ↾}_{ℝ}$
118		resmpt	$⊢ ℝ \subseteq ℂ \to {(x \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) x) ↾}_{ℝ} = (x \in ℝ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) x)$
119	12 118	ax-mp	$⊢ {(x \in ℂ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) x) ↾}_{ℝ} = (x \in ℝ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) x)$
120	102 81	recidi	$⊢ 2 (\frac{1}{2}) = 1$
121	120	a1i	$⊢ x \in ℝ \to 2 (\frac{1}{2}) = 1$
122	83	eqcomd	$⊢ x \in ℝ \to (\frac{1}{2}) x = \frac{x}{2}$
123	122	fveq2d	$⊢ x \in ℝ \to \cos (\frac{1}{2}) x = \cos (\frac{x}{2})$
124	121 123	oveq12d	$⊢ x \in ℝ \to 2 (\frac{1}{2}) \cos (\frac{1}{2}) x = 1 \cos (\frac{x}{2})$
125	52	halfcld	$⊢ x \in ℝ \to \frac{x}{2} \in ℂ$
126	125	coscld	$⊢ x \in ℝ \to \cos (\frac{x}{2}) \in ℂ$
127	126	mulid2d	$⊢ x \in ℝ \to 1 \cos (\frac{x}{2}) = \cos (\frac{x}{2})$
128	124 127	eqtrd	$⊢ x \in ℝ \to 2 (\frac{1}{2}) \cos (\frac{1}{2}) x = \cos (\frac{x}{2})$
129	128	mpteq2ia	$⊢ (x \in ℝ ⟼ 2 (\frac{1}{2}) \cos (\frac{1}{2}) x) = (x \in ℝ ⟼ \cos (\frac{x}{2}))$
130	117 119 129	3eqtri	$⊢ {\frac{d (x \in ℂ⟼ 2 \sin (\frac{1}{2}) x)}{d_{ℂ} x} ↾}_{ℝ} = (x \in ℝ ⟼ \cos (\frac{x}{2}))$
131	91 116 130	3eqtri	$⊢ \frac{d (x \in ℝ⟼ 2 \sin (\frac{1}{2}) x)}{d_{ℝ} x} = (x \in ℝ ⟼ \cos (\frac{x}{2}))$
132	87 131	eqtri	$⊢ \frac{d (x \in ℝ⟼ 2 \sin (\frac{x}{2}))}{d_{ℝ} x} = (x \in ℝ ⟼ \cos (\frac{x}{2}))$
133	132	a1i	$⊢ ⊤ \to \frac{d (x \in ℝ⟼ 2 \sin (\frac{x}{2}))}{d_{ℝ} x} = (x \in ℝ ⟼ \cos (\frac{x}{2}))$
134	51 78 79 133 20 57 56 64	dvmptres	$⊢ ⊤ \to \frac{d (x \in ((- π, π) ∖ \{0\})⟼ 2 \sin (\frac{x}{2}))}{d_{ℝ} x} = (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2}))$
135	134	mptru	$⊢ \frac{d (x \in ((- π, π) ∖ \{0\})⟼ 2 \sin (\frac{x}{2}))}{d_{ℝ} x} = (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2}))$
136	135	eqcomi	$⊢ (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2})) = \frac{d (x \in ((- π, π) ∖ \{0\})⟼ 2 \sin (\frac{x}{2}))}{d_{ℝ} x}$
137	136	dmeqi	$⊢ dom (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2})) = dom \frac{d (x \in ((- π, π) ∖ \{0\})⟼ 2 \sin (\frac{x}{2}))}{d_{ℝ} x}$
138	74 137	eqtr3i	$⊢ (- π, π) ∖ \{0\} = dom \frac{d (x \in ((- π, π) ∖ \{0\})⟼ 2 \sin (\frac{x}{2}))}{d_{ℝ} x}$
139	138	eqimssi	$⊢ (- π, π) ∖ \{0\} \subseteq dom \frac{d (x \in ((- π, π) ∖ \{0\})⟼ 2 \sin (\frac{x}{2}))}{d_{ℝ} x}$
140	139	a1i	$⊢ ⊤ \to (- π, π) ∖ \{0\} \subseteq dom \frac{d (x \in ((- π, π) ∖ \{0\})⟼ 2 \sin (\frac{x}{2}))}{d_{ℝ} x}$
141	17	recnd	$⊢ s \in (- π, π) \to s \in ℂ$
142	141	ssriv	$⊢ (- π, π) \subseteq ℂ$
143	142	a1i	$⊢ ⊤ \to (- π, π) \subseteq ℂ$
144		ssid	$⊢ ℂ \subseteq ℂ$
145	144	a1i	$⊢ ⊤ \to ℂ \subseteq ℂ$
146	143 145	idcncfg	$⊢ ⊤ \to (x \in (- π, π) ⟼ x) : (- π, π) \underset{cn}{⟶} ℂ$
147	146	mptru	$⊢ (x \in (- π, π) ⟼ x) : (- π, π) \underset{cn}{⟶} ℂ$
148		cnlimc	$⊢ (- π, π) \subseteq ℂ \to ((x \in (- π, π) ⟼ x) : (- π, π) \underset{cn}{⟶} ℂ \leftrightarrow ((x \in (- π, π) ⟼ x) : (- π, π) ⟶ ℂ \land \forall y \in (- π, π) (x \in (- π, π) ⟼ x) (y) \in ((x \in (- π, π) ⟼ x) {lim}_{ℂ} y)))$
149	142 148	ax-mp	$⊢ (x \in (- π, π) ⟼ x) : (- π, π) \underset{cn}{⟶} ℂ \leftrightarrow ((x \in (- π, π) ⟼ x) : (- π, π) ⟶ ℂ \land \forall y \in (- π, π) (x \in (- π, π) ⟼ x) (y) \in ((x \in (- π, π) ⟼ x) {lim}_{ℂ} y))$
150	147 149	mpbi	$⊢ ((x \in (- π, π) ⟼ x) : (- π, π) ⟶ ℂ \land \forall y \in (- π, π) (x \in (- π, π) ⟼ x) (y) \in ((x \in (- π, π) ⟼ x) {lim}_{ℂ} y))$
151	150	simpri	$⊢ \forall y \in (- π, π) (x \in (- π, π) ⟼ x) (y) \in ((x \in (- π, π) ⟼ x) {lim}_{ℂ} y)$
152		fveq2	$⊢ y = 0 \to (x \in (- π, π) ⟼ x) (y) = (x \in (- π, π) ⟼ x) (0)$
153		oveq2	$⊢ y = 0 \to (x \in (- π, π) ⟼ x) {lim}_{ℂ} y = (x \in (- π, π) ⟼ x) {lim}_{ℂ} 0$
154	152 153	eleq12d	$⊢ y = 0 \to ((x \in (- π, π) ⟼ x) (y) \in ((x \in (- π, π) ⟼ x) {lim}_{ℂ} y) \leftrightarrow (x \in (- π, π) ⟼ x) (0) \in ((x \in (- π, π) ⟼ x) {lim}_{ℂ} 0))$
155	154	rspccva	$⊢ (\forall y \in (- π, π) (x \in (- π, π) ⟼ x) (y) \in ((x \in (- π, π) ⟼ x) {lim}_{ℂ} y) \land 0 \in (- π, π)) \to (x \in (- π, π) ⟼ x) (0) \in ((x \in (- π, π) ⟼ x) {lim}_{ℂ} 0)$
156	151 44 155	mp2an	$⊢ (x \in (- π, π) ⟼ x) (0) \in ((x \in (- π, π) ⟼ x) {lim}_{ℂ} 0)$
157		id	$⊢ x = 0 \to x = 0$
158		eqid	$⊢ (x \in (- π, π) ⟼ x) = (x \in (- π, π) ⟼ x)$
159		c0ex	$⊢ 0 \in V$
160	157 158 159	fvmpt	$⊢ 0 \in (- π, π) \to (x \in (- π, π) ⟼ x) (0) = 0$
161	44 160	ax-mp	$⊢ (x \in (- π, π) ⟼ x) (0) = 0$
162		elioore	$⊢ x \in (- π, π) \to x \in ℝ$
163	162	recnd	$⊢ x \in (- π, π) \to x \in ℂ$
164	158 163	fmpti	$⊢ (x \in (- π, π) ⟼ x) : (- π, π) ⟶ ℂ$
165	164	a1i	$⊢ ⊤ \to (x \in (- π, π) ⟼ x) : (- π, π) ⟶ ℂ$
166	165	limcdif	$⊢ ⊤ \to (x \in (- π, π) ⟼ x) {lim}_{ℂ} 0 = ({(x \in (- π, π) ⟼ x) ↾}_{((- π, π) ∖ \{0\})}) {lim}_{ℂ} 0$
167	166	mptru	$⊢ (x \in (- π, π) ⟼ x) {lim}_{ℂ} 0 = ({(x \in (- π, π) ⟼ x) ↾}_{((- π, π) ∖ \{0\})}) {lim}_{ℂ} 0$
168		resmpt	$⊢ (- π, π) ∖ \{0\} \subseteq (- π, π) \to {(x \in (- π, π) ⟼ x) ↾}_{((- π, π) ∖ \{0\})} = (x \in ((- π, π) ∖ \{0\}) ⟼ x)$
169	16 168	ax-mp	$⊢ {(x \in (- π, π) ⟼ x) ↾}_{((- π, π) ∖ \{0\})} = (x \in ((- π, π) ∖ \{0\}) ⟼ x)$
170	169	oveq1i	$⊢ ({(x \in (- π, π) ⟼ x) ↾}_{((- π, π) ∖ \{0\})}) {lim}_{ℂ} 0 = (x \in ((- π, π) ∖ \{0\}) ⟼ x) {lim}_{ℂ} 0$
171	167 170	eqtri	$⊢ (x \in (- π, π) ⟼ x) {lim}_{ℂ} 0 = (x \in ((- π, π) ∖ \{0\}) ⟼ x) {lim}_{ℂ} 0$
172	156 161 171	3eltr3i	$⊢ 0 \in ((x \in ((- π, π) ∖ \{0\}) ⟼ x) {lim}_{ℂ} 0)$
173	172	a1i	$⊢ ⊤ \to 0 \in ((x \in ((- π, π) ∖ \{0\}) ⟼ x) {lim}_{ℂ} 0)$
174		eqid	$⊢ (x \in ℂ ⟼ 2) = (x \in ℂ ⟼ 2)$
175	144	a1i	$⊢ 2 \in ℂ \to ℂ \subseteq ℂ$
176		2cnd	$⊢ 2 \in ℂ \to 2 \in ℂ$
177	175 176 175	constcncfg	$⊢ 2 \in ℂ \to (x \in ℂ ⟼ 2) : ℂ \underset{cn}{⟶} ℂ$
178	102 177	mp1i	$⊢ ⊤ \to (x \in ℂ ⟼ 2) : ℂ \underset{cn}{⟶} ℂ$
179		2cnd	$⊢ (⊤ \land x \in (- π, π)) \to 2 \in ℂ$
180	174 178 143 145 179	cncfmptssg	$⊢ ⊤ \to (x \in (- π, π) ⟼ 2) : (- π, π) \underset{cn}{⟶} ℂ$
181		sincn	$⊢ \sin : ℂ \underset{cn}{⟶} ℂ$
182	181	a1i	$⊢ ⊤ \to \sin : ℂ \underset{cn}{⟶} ℂ$
183		eqid	$⊢ (x \in ℂ ⟼ \frac{x}{2}) = (x \in ℂ ⟼ \frac{x}{2})$
184	183	divccncf	$⊢ (2 \in ℂ \land 2 \neq 0) \to (x \in ℂ ⟼ \frac{x}{2}) : ℂ \underset{cn}{⟶} ℂ$
185	102 81 184	mp2an	$⊢ (x \in ℂ ⟼ \frac{x}{2}) : ℂ \underset{cn}{⟶} ℂ$
186	185	a1i	$⊢ ⊤ \to (x \in ℂ ⟼ \frac{x}{2}) : ℂ \underset{cn}{⟶} ℂ$
187	163	adantl	$⊢ (⊤ \land x \in (- π, π)) \to x \in ℂ$
188	187	halfcld	$⊢ (⊤ \land x \in (- π, π)) \to \frac{x}{2} \in ℂ$
189	183 186 143 145 188	cncfmptssg	$⊢ ⊤ \to (x \in (- π, π) ⟼ \frac{x}{2}) : (- π, π) \underset{cn}{⟶} ℂ$
190	182 189	cncfmpt1f	$⊢ ⊤ \to (x \in (- π, π) ⟼ \sin (\frac{x}{2})) : (- π, π) \underset{cn}{⟶} ℂ$
191	180 190	mulcncf	$⊢ ⊤ \to (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) : (- π, π) \underset{cn}{⟶} ℂ$
192	191	mptru	$⊢ (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) : (- π, π) \underset{cn}{⟶} ℂ$
193		cnlimc	$⊢ (- π, π) \subseteq ℂ \to ((x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) : (- π, π) \underset{cn}{⟶} ℂ \leftrightarrow ((x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) : (- π, π) ⟶ ℂ \land \forall y \in (- π, π) (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) (y) \in ((x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) {lim}_{ℂ} y)))$
194	142 193	ax-mp	$⊢ (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) : (- π, π) \underset{cn}{⟶} ℂ \leftrightarrow ((x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) : (- π, π) ⟶ ℂ \land \forall y \in (- π, π) (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) (y) \in ((x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) {lim}_{ℂ} y))$
195	192 194	mpbi	$⊢ ((x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) : (- π, π) ⟶ ℂ \land \forall y \in (- π, π) (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) (y) \in ((x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) {lim}_{ℂ} y))$
196	195	simpri	$⊢ \forall y \in (- π, π) (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) (y) \in ((x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) {lim}_{ℂ} y)$
197		fveq2	$⊢ y = 0 \to (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) (y) = (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) (0)$
198		oveq2	$⊢ y = 0 \to (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) {lim}_{ℂ} y = (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) {lim}_{ℂ} 0$
199	197 198	eleq12d	$⊢ y = 0 \to ((x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) (y) \in ((x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) {lim}_{ℂ} y) \leftrightarrow (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) (0) \in ((x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) {lim}_{ℂ} 0))$
200	199	rspccva	$⊢ (\forall y \in (- π, π) (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) (y) \in ((x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) {lim}_{ℂ} y) \land 0 \in (- π, π)) \to (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) (0) \in ((x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) {lim}_{ℂ} 0)$
201	196 44 200	mp2an	$⊢ (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) (0) \in ((x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) {lim}_{ℂ} 0)$
202		oveq1	$⊢ x = 0 \to \frac{x}{2} = \frac{0}{2}$
203	102 81	div0i	$⊢ \frac{0}{2} = 0$
204	202 203	syl6eq	$⊢ x = 0 \to \frac{x}{2} = 0$
205	204	fveq2d	$⊢ x = 0 \to \sin (\frac{x}{2}) = \sin 0$
206		sin0	$⊢ \sin 0 = 0$
207	205 206	syl6eq	$⊢ x = 0 \to \sin (\frac{x}{2}) = 0$
208	207	oveq2d	$⊢ x = 0 \to 2 \sin (\frac{x}{2}) = 2 \cdot 0$
209		2t0e0	$⊢ 2 \cdot 0 = 0$
210	208 209	syl6eq	$⊢ x = 0 \to 2 \sin (\frac{x}{2}) = 0$
211		eqid	$⊢ (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) = (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2}))$
212	210 211 159	fvmpt	$⊢ 0 \in (- π, π) \to (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) (0) = 0$
213	44 212	ax-mp	$⊢ (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) (0) = 0$
214		2cnd	$⊢ x \in (- π, π) \to 2 \in ℂ$
215	163	halfcld	$⊢ x \in (- π, π) \to \frac{x}{2} \in ℂ$
216	215	sincld	$⊢ x \in (- π, π) \to \sin (\frac{x}{2}) \in ℂ$
217	214 216	mulcld	$⊢ x \in (- π, π) \to 2 \sin (\frac{x}{2}) \in ℂ$
218	211 217	fmpti	$⊢ (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) : (- π, π) ⟶ ℂ$
219	218	a1i	$⊢ ⊤ \to (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) : (- π, π) ⟶ ℂ$
220	219	limcdif	$⊢ ⊤ \to (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) {lim}_{ℂ} 0 = ({(x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) ↾}_{((- π, π) ∖ \{0\})}) {lim}_{ℂ} 0$
221	220	mptru	$⊢ (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) {lim}_{ℂ} 0 = ({(x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) ↾}_{((- π, π) ∖ \{0\})}) {lim}_{ℂ} 0$
222		resmpt	$⊢ (- π, π) ∖ \{0\} \subseteq (- π, π) \to {(x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) ↾}_{((- π, π) ∖ \{0\})} = (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2}))$
223	16 222	ax-mp	$⊢ {(x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) ↾}_{((- π, π) ∖ \{0\})} = (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2}))$
224	223	oveq1i	$⊢ ({(x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) ↾}_{((- π, π) ∖ \{0\})}) {lim}_{ℂ} 0 = (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) {lim}_{ℂ} 0$
225	221 224	eqtri	$⊢ (x \in (- π, π) ⟼ 2 \sin (\frac{x}{2})) {lim}_{ℂ} 0 = (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) {lim}_{ℂ} 0$
226	201 213 225	3eltr3i	$⊢ 0 \in ((x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) {lim}_{ℂ} 0)$
227	226	a1i	$⊢ ⊤ \to 0 \in ((x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) {lim}_{ℂ} 0)$
228		eqidd	$⊢ y \in ((- π, π) ∖ \{0\}) \to (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) = (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2}))$
229		oveq1	$⊢ x = y \to \frac{x}{2} = \frac{y}{2}$
230	229	fveq2d	$⊢ x = y \to \sin (\frac{x}{2}) = \sin (\frac{y}{2})$
231	230	oveq2d	$⊢ x = y \to 2 \sin (\frac{x}{2}) = 2 \sin (\frac{y}{2})$
232	231	adantl	$⊢ (y \in ((- π, π) ∖ \{0\}) \land x = y) \to 2 \sin (\frac{x}{2}) = 2 \sin (\frac{y}{2})$
233		id	$⊢ y \in ((- π, π) ∖ \{0\}) \to y \in ((- π, π) ∖ \{0\})$
234	26	a1i	$⊢ y \in ((- π, π) ∖ \{0\}) \to 2 \in ℝ$
235	19	sseli	$⊢ y \in ((- π, π) ∖ \{0\}) \to y \in ℝ$
236	235	rehalfcld	$⊢ y \in ((- π, π) ∖ \{0\}) \to \frac{y}{2} \in ℝ$
237	236	resincld	$⊢ y \in ((- π, π) ∖ \{0\}) \to \sin (\frac{y}{2}) \in ℝ$
238	234 237	remulcld	$⊢ y \in ((- π, π) ∖ \{0\}) \to 2 \sin (\frac{y}{2}) \in ℝ$
239	228 232 233 238	fvmptd	$⊢ y \in ((- π, π) ∖ \{0\}) \to (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) (y) = 2 \sin (\frac{y}{2})$
240		2cnd	$⊢ y \in ((- π, π) ∖ \{0\}) \to 2 \in ℂ$
241	237	recnd	$⊢ y \in ((- π, π) ∖ \{0\}) \to \sin (\frac{y}{2}) \in ℂ$
242	81	a1i	$⊢ y \in ((- π, π) ∖ \{0\}) \to 2 \neq 0$
243		ioossicc	$⊢ (- π, π) \subseteq [- π, π]$
244		eldifi	$⊢ y \in ((- π, π) ∖ \{0\}) \to y \in (- π, π)$
245	243 244	sseldi	$⊢ y \in ((- π, π) ∖ \{0\}) \to y \in [- π, π]$
246		eldifsni	$⊢ y \in ((- π, π) ∖ \{0\}) \to y \neq 0$
247		fourierdlem44	$⊢ (y \in [- π, π] \land y \neq 0) \to \sin (\frac{y}{2}) \neq 0$
248	245 246 247	syl2anc	$⊢ y \in ((- π, π) ∖ \{0\}) \to \sin (\frac{y}{2}) \neq 0$
249	240 241 242 248	mulne0d	$⊢ y \in ((- π, π) ∖ \{0\}) \to 2 \sin (\frac{y}{2}) \neq 0$
250	239 249	eqnetrd	$⊢ y \in ((- π, π) ∖ \{0\}) \to (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) (y) \neq 0$
251	250	neneqd	$⊢ y \in ((- π, π) ∖ \{0\}) \to \neg (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) (y) = 0$
252	251	nrex	$⊢ \neg \exists y \in ((- π, π) ∖ \{0\}) (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) (y) = 0$
253	25	fnmpt	$⊢ \forall x \in ((- π, π) ∖ \{0\}) 2 \sin (\frac{x}{2}) \in ℝ \to (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) Fn ((- π, π) ∖ \{0\})$
254	253 30	mprg	$⊢ (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) Fn ((- π, π) ∖ \{0\})$
255		ssid	$⊢ (- π, π) ∖ \{0\} \subseteq (- π, π) ∖ \{0\}$
256		fvelimab	$⊢ ((x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) Fn ((- π, π) ∖ \{0\}) \land (- π, π) ∖ \{0\} \subseteq (- π, π) ∖ \{0\}) \to (0 \in (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) [(- π, π) ∖ \{0\}] \leftrightarrow \exists y \in ((- π, π) ∖ \{0\}) (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) (y) = 0)$
257	254 255 256	mp2an	$⊢ 0 \in (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) [(- π, π) ∖ \{0\}] \leftrightarrow \exists y \in ((- π, π) ∖ \{0\}) (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) (y) = 0$
258	252 257	mtbir	$⊢ \neg 0 \in (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) [(- π, π) ∖ \{0\}]$
259	258	a1i	$⊢ ⊤ \to \neg 0 \in (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) [(- π, π) ∖ \{0\}]$
260		eqidd	$⊢ y \in ((- π, π) ∖ \{0\}) \to (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2})) = (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2}))$
261	229	fveq2d	$⊢ x = y \to \cos (\frac{x}{2}) = \cos (\frac{y}{2})$
262	261	adantl	$⊢ (y \in ((- π, π) ∖ \{0\}) \land x = y) \to \cos (\frac{x}{2}) = \cos (\frac{y}{2})$
263	235	recnd	$⊢ y \in ((- π, π) ∖ \{0\}) \to y \in ℂ$
264	263	halfcld	$⊢ y \in ((- π, π) ∖ \{0\}) \to \frac{y}{2} \in ℂ$
265	264	coscld	$⊢ y \in ((- π, π) ∖ \{0\}) \to \cos (\frac{y}{2}) \in ℂ$
266	260 262 233 265	fvmptd	$⊢ y \in ((- π, π) ∖ \{0\}) \to (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2})) (y) = \cos (\frac{y}{2})$
267	236	rered	$⊢ y \in ((- π, π) ∖ \{0\}) \to ℜ (\frac{y}{2}) = \frac{y}{2}$
268		halfpire	$⊢ \frac{π}{2} \in ℝ$
269	268	renegcli	$⊢ - \frac{π}{2} \in ℝ$
270	269	a1i	$⊢ y \in ((- π, π) ∖ \{0\}) \to - \frac{π}{2} \in ℝ$
271	270	rexrd	$⊢ y \in ((- π, π) ∖ \{0\}) \to - \frac{π}{2} \in ℝ^{*}$
272	268	a1i	$⊢ y \in ((- π, π) ∖ \{0\}) \to \frac{π}{2} \in ℝ$
273	272	rexrd	$⊢ y \in ((- π, π) ∖ \{0\}) \to \frac{π}{2} \in ℝ^{*}$
274		picn	$⊢ π \in ℂ$
275		divneg	$⊢ (π \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to - \frac{π}{2} = \frac{- π}{2}$
276	274 102 81 275	mp3an	$⊢ - \frac{π}{2} = \frac{- π}{2}$
277	39	a1i	$⊢ y \in ((- π, π) ∖ \{0\}) \to - π \in ℝ$
278		2rp	$⊢ 2 \in ℝ^{+}$
279	278	a1i	$⊢ y \in ((- π, π) ∖ \{0\}) \to 2 \in ℝ^{+}$
280	40	a1i	$⊢ y \in ((- π, π) ∖ \{0\}) \to - π \in ℝ^{*}$
281	41	a1i	$⊢ y \in ((- π, π) ∖ \{0\}) \to π \in ℝ^{*}$
282		ioogtlb	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land y \in (- π, π)) \to - π < y$
283	280 281 244 282	syl3anc	$⊢ y \in ((- π, π) ∖ \{0\}) \to - π < y$
284	277 235 279 283	ltdiv1dd	$⊢ y \in ((- π, π) ∖ \{0\}) \to \frac{- π}{2} < \frac{y}{2}$
285	276 284	eqbrtrid	$⊢ y \in ((- π, π) ∖ \{0\}) \to - \frac{π}{2} < \frac{y}{2}$
286	38	a1i	$⊢ y \in ((- π, π) ∖ \{0\}) \to π \in ℝ$
287		iooltub	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land y \in (- π, π)) \to y < π$
288	280 281 244 287	syl3anc	$⊢ y \in ((- π, π) ∖ \{0\}) \to y < π$
289	235 286 279 288	ltdiv1dd	$⊢ y \in ((- π, π) ∖ \{0\}) \to \frac{y}{2} < \frac{π}{2}$
290	271 273 236 285 289	eliood	$⊢ y \in ((- π, π) ∖ \{0\}) \to \frac{y}{2} \in (- \frac{π}{2}, \frac{π}{2})$
291	267 290	eqeltrd	$⊢ y \in ((- π, π) ∖ \{0\}) \to ℜ (\frac{y}{2}) \in (- \frac{π}{2}, \frac{π}{2})$
292		cosne0	$⊢ (\frac{y}{2} \in ℂ \land ℜ (\frac{y}{2}) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos (\frac{y}{2}) \neq 0$
293	264 291 292	syl2anc	$⊢ y \in ((- π, π) ∖ \{0\}) \to \cos (\frac{y}{2}) \neq 0$
294	266 293	eqnetrd	$⊢ y \in ((- π, π) ∖ \{0\}) \to (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2})) (y) \neq 0$
295	294	neneqd	$⊢ y \in ((- π, π) ∖ \{0\}) \to \neg (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2})) (y) = 0$
296	295	nrex	$⊢ \neg \exists y \in ((- π, π) ∖ \{0\}) (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2})) (y) = 0$
297	72 73	fnmpti	$⊢ (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2})) Fn ((- π, π) ∖ \{0\})$
298		fvelimab	$⊢ ((x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2})) Fn ((- π, π) ∖ \{0\}) \land (- π, π) ∖ \{0\} \subseteq (- π, π) ∖ \{0\}) \to (0 \in (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2})) [(- π, π) ∖ \{0\}] \leftrightarrow \exists y \in ((- π, π) ∖ \{0\}) (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2})) (y) = 0)$
299	297 255 298	mp2an	$⊢ 0 \in (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2})) [(- π, π) ∖ \{0\}] \leftrightarrow \exists y \in ((- π, π) ∖ \{0\}) (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2})) (y) = 0$
300	296 299	mtbir	$⊢ \neg 0 \in (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2})) [(- π, π) ∖ \{0\}]$
301	135	imaeq1i	$⊢ \frac{d (x \in ((- π, π) ∖ \{0\})⟼ 2 \sin (\frac{x}{2}))}{d_{ℝ} x} [(- π, π) ∖ \{0\}] = (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2})) [(- π, π) ∖ \{0\}]$
302	301	eleq2i	$⊢ 0 \in \frac{d (x \in ((- π, π) ∖ \{0\})⟼ 2 \sin (\frac{x}{2}))}{d_{ℝ} x} [(- π, π) ∖ \{0\}] \leftrightarrow 0 \in (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2})) [(- π, π) ∖ \{0\}]$
303	300 302	mtbir	$⊢ \neg 0 \in \frac{d (x \in ((- π, π) ∖ \{0\})⟼ 2 \sin (\frac{x}{2}))}{d_{ℝ} x} [(- π, π) ∖ \{0\}]$
304	303	a1i	$⊢ ⊤ \to \neg 0 \in \frac{d (x \in ((- π, π) ∖ \{0\})⟼ 2 \sin (\frac{x}{2}))}{d_{ℝ} x} [(- π, π) ∖ \{0\}]$
305		eqid	$⊢ (s \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{s}{2})) = (s \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{s}{2}))$
306		eqid	$⊢ (s \in ((- π, π) ∖ \{0\}) ⟼ \frac{1}{\cos (\frac{s}{2})}) = (s \in ((- π, π) ∖ \{0\}) ⟼ \frac{1}{\cos (\frac{s}{2})})$
307	19	sseli	$⊢ s \in ((- π, π) ∖ \{0\}) \to s \in ℝ$
308	307	recnd	$⊢ s \in ((- π, π) ∖ \{0\}) \to s \in ℂ$
309	308	halfcld	$⊢ s \in ((- π, π) ∖ \{0\}) \to \frac{s}{2} \in ℂ$
310	309	coscld	$⊢ s \in ((- π, π) ∖ \{0\}) \to \cos (\frac{s}{2}) \in ℂ$
311	307	rehalfcld	$⊢ s \in ((- π, π) ∖ \{0\}) \to \frac{s}{2} \in ℝ$
312	311	rered	$⊢ s \in ((- π, π) ∖ \{0\}) \to ℜ (\frac{s}{2}) = \frac{s}{2}$
313	269	a1i	$⊢ s \in ((- π, π) ∖ \{0\}) \to - \frac{π}{2} \in ℝ$
314	313	rexrd	$⊢ s \in ((- π, π) ∖ \{0\}) \to - \frac{π}{2} \in ℝ^{*}$
315	268	a1i	$⊢ s \in ((- π, π) ∖ \{0\}) \to \frac{π}{2} \in ℝ$
316	315	rexrd	$⊢ s \in ((- π, π) ∖ \{0\}) \to \frac{π}{2} \in ℝ^{*}$
317	38	a1i	$⊢ s \in ((- π, π) ∖ \{0\}) \to π \in ℝ$
318	317	renegcld	$⊢ s \in ((- π, π) ∖ \{0\}) \to - π \in ℝ$
319	278	a1i	$⊢ s \in ((- π, π) ∖ \{0\}) \to 2 \in ℝ^{+}$
320	40	a1i	$⊢ s \in ((- π, π) ∖ \{0\}) \to - π \in ℝ^{*}$
321	41	a1i	$⊢ s \in ((- π, π) ∖ \{0\}) \to π \in ℝ^{*}$
322		eldifi	$⊢ s \in ((- π, π) ∖ \{0\}) \to s \in (- π, π)$
323		ioogtlb	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land s \in (- π, π)) \to - π < s$
324	320 321 322 323	syl3anc	$⊢ s \in ((- π, π) ∖ \{0\}) \to - π < s$
325	318 307 319 324	ltdiv1dd	$⊢ s \in ((- π, π) ∖ \{0\}) \to \frac{- π}{2} < \frac{s}{2}$
326	276 325	eqbrtrid	$⊢ s \in ((- π, π) ∖ \{0\}) \to - \frac{π}{2} < \frac{s}{2}$
327		iooltub	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land s \in (- π, π)) \to s < π$
328	320 321 322 327	syl3anc	$⊢ s \in ((- π, π) ∖ \{0\}) \to s < π$
329	307 317 319 328	ltdiv1dd	$⊢ s \in ((- π, π) ∖ \{0\}) \to \frac{s}{2} < \frac{π}{2}$
330	314 316 311 326 329	eliood	$⊢ s \in ((- π, π) ∖ \{0\}) \to \frac{s}{2} \in (- \frac{π}{2}, \frac{π}{2})$
331	312 330	eqeltrd	$⊢ s \in ((- π, π) ∖ \{0\}) \to ℜ (\frac{s}{2}) \in (- \frac{π}{2}, \frac{π}{2})$
332		cosne0	$⊢ (\frac{s}{2} \in ℂ \land ℜ (\frac{s}{2}) \in (- \frac{π}{2}, \frac{π}{2})) \to \cos (\frac{s}{2}) \neq 0$
333	309 331 332	syl2anc	$⊢ s \in ((- π, π) ∖ \{0\}) \to \cos (\frac{s}{2}) \neq 0$
334	333	neneqd	$⊢ s \in ((- π, π) ∖ \{0\}) \to \neg \cos (\frac{s}{2}) = 0$
335	311	recoscld	$⊢ s \in ((- π, π) ∖ \{0\}) \to \cos (\frac{s}{2}) \in ℝ$
336		elsng	$⊢ \cos (\frac{s}{2}) \in ℝ \to (\cos (\frac{s}{2}) \in \{0\} \leftrightarrow \cos (\frac{s}{2}) = 0)$
337	335 336	syl	$⊢ s \in ((- π, π) ∖ \{0\}) \to (\cos (\frac{s}{2}) \in \{0\} \leftrightarrow \cos (\frac{s}{2}) = 0)$
338	334 337	mtbird	$⊢ s \in ((- π, π) ∖ \{0\}) \to \neg \cos (\frac{s}{2}) \in \{0\}$
339	310 338	eldifd	$⊢ s \in ((- π, π) ∖ \{0\}) \to \cos (\frac{s}{2}) \in (ℂ ∖ \{0\})$
340	339	adantl	$⊢ (⊤ \land s \in ((- π, π) ∖ \{0\})) \to \cos (\frac{s}{2}) \in (ℂ ∖ \{0\})$
341	309	ad2antrl	$⊢ (⊤ \land (s \in ((- π, π) ∖ \{0\}) \land \frac{s}{2} \neq 0)) \to \frac{s}{2} \in ℂ$
342		cosf	$⊢ \cos : ℂ ⟶ ℂ$
343	342	a1i	$⊢ ⊤ \to \cos : ℂ ⟶ ℂ$
344	343	ffvelrnda	$⊢ (⊤ \land x \in ℂ) \to \cos x \in ℂ$
345		eqid	$⊢ (s \in ℂ ⟼ \frac{s}{2}) = (s \in ℂ ⟼ \frac{s}{2})$
346	345	divccncf	$⊢ (2 \in ℂ \land 2 \neq 0) \to (s \in ℂ ⟼ \frac{s}{2}) : ℂ \underset{cn}{⟶} ℂ$
347	102 81 346	mp2an	$⊢ (s \in ℂ ⟼ \frac{s}{2}) : ℂ \underset{cn}{⟶} ℂ$
348	347	a1i	$⊢ ⊤ \to (s \in ℂ ⟼ \frac{s}{2}) : ℂ \underset{cn}{⟶} ℂ$
349	141	adantl	$⊢ (⊤ \land s \in (- π, π)) \to s \in ℂ$
350	349	halfcld	$⊢ (⊤ \land s \in (- π, π)) \to \frac{s}{2} \in ℂ$
351	345 348 143 145 350	cncfmptssg	$⊢ ⊤ \to (s \in (- π, π) ⟼ \frac{s}{2}) : (- π, π) \underset{cn}{⟶} ℂ$
352		oveq1	$⊢ s = 0 \to \frac{s}{2} = \frac{0}{2}$
353	352 203	syl6eq	$⊢ s = 0 \to \frac{s}{2} = 0$
354	351 45 353	cnmptlimc	$⊢ ⊤ \to 0 \in ((s \in (- π, π) ⟼ \frac{s}{2}) {lim}_{ℂ} 0)$
355		eqid	$⊢ (s \in (- π, π) ⟼ \frac{s}{2}) = (s \in (- π, π) ⟼ \frac{s}{2})$
356	141	halfcld	$⊢ s \in (- π, π) \to \frac{s}{2} \in ℂ$
357	355 356	fmpti	$⊢ (s \in (- π, π) ⟼ \frac{s}{2}) : (- π, π) ⟶ ℂ$
358	357	a1i	$⊢ ⊤ \to (s \in (- π, π) ⟼ \frac{s}{2}) : (- π, π) ⟶ ℂ$
359	358	limcdif	$⊢ ⊤ \to (s \in (- π, π) ⟼ \frac{s}{2}) {lim}_{ℂ} 0 = ({(s \in (- π, π) ⟼ \frac{s}{2}) ↾}_{((- π, π) ∖ \{0\})}) {lim}_{ℂ} 0$
360	359	mptru	$⊢ (s \in (- π, π) ⟼ \frac{s}{2}) {lim}_{ℂ} 0 = ({(s \in (- π, π) ⟼ \frac{s}{2}) ↾}_{((- π, π) ∖ \{0\})}) {lim}_{ℂ} 0$
361		resmpt	$⊢ (- π, π) ∖ \{0\} \subseteq (- π, π) \to {(s \in (- π, π) ⟼ \frac{s}{2}) ↾}_{((- π, π) ∖ \{0\})} = (s \in ((- π, π) ∖ \{0\}) ⟼ \frac{s}{2})$
362	16 361	ax-mp	$⊢ {(s \in (- π, π) ⟼ \frac{s}{2}) ↾}_{((- π, π) ∖ \{0\})} = (s \in ((- π, π) ∖ \{0\}) ⟼ \frac{s}{2})$
363	362	oveq1i	$⊢ ({(s \in (- π, π) ⟼ \frac{s}{2}) ↾}_{((- π, π) ∖ \{0\})}) {lim}_{ℂ} 0 = (s \in ((- π, π) ∖ \{0\}) ⟼ \frac{s}{2}) {lim}_{ℂ} 0$
364	360 363	eqtri	$⊢ (s \in (- π, π) ⟼ \frac{s}{2}) {lim}_{ℂ} 0 = (s \in ((- π, π) ∖ \{0\}) ⟼ \frac{s}{2}) {lim}_{ℂ} 0$
365	354 364	eleqtrdi	$⊢ ⊤ \to 0 \in ((s \in ((- π, π) ∖ \{0\}) ⟼ \frac{s}{2}) {lim}_{ℂ} 0)$
366		ffn	$⊢ \cos : ℂ ⟶ ℂ \to \cos Fn ℂ$
367	342 366	ax-mp	$⊢ \cos Fn ℂ$
368		dffn5	$⊢ \cos Fn ℂ \leftrightarrow \cos = (x \in ℂ ⟼ \cos x)$
369	367 368	mpbi	$⊢ \cos = (x \in ℂ ⟼ \cos x)$
370		coscn	$⊢ \cos : ℂ \underset{cn}{⟶} ℂ$
371	369 370	eqeltrri	$⊢ (x \in ℂ ⟼ \cos x) : ℂ \underset{cn}{⟶} ℂ$
372	371	a1i	$⊢ ⊤ \to (x \in ℂ ⟼ \cos x) : ℂ \underset{cn}{⟶} ℂ$
373		0cnd	$⊢ ⊤ \to 0 \in ℂ$
374		fveq2	$⊢ x = 0 \to \cos x = \cos 0$
375		cos0	$⊢ \cos 0 = 1$
376	374 375	syl6eq	$⊢ x = 0 \to \cos x = 1$
377	372 373 376	cnmptlimc	$⊢ ⊤ \to 1 \in ((x \in ℂ ⟼ \cos x) {lim}_{ℂ} 0)$
378		fveq2	$⊢ x = \frac{s}{2} \to \cos x = \cos (\frac{s}{2})$
379		fveq2	$⊢ \frac{s}{2} = 0 \to \cos (\frac{s}{2}) = \cos 0$
380	379 375	syl6eq	$⊢ \frac{s}{2} = 0 \to \cos (\frac{s}{2}) = 1$
381	380	ad2antll	$⊢ (⊤ \land (s \in ((- π, π) ∖ \{0\}) \land \frac{s}{2} = 0)) \to \cos (\frac{s}{2}) = 1$
382	341 344 365 377 378 381	limcco	$⊢ ⊤ \to 1 \in ((s \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{s}{2})) {lim}_{ℂ} 0)$
383		ax-1ne0	$⊢ 1 \neq 0$
384	383	a1i	$⊢ ⊤ \to 1 \neq 0$
385	305 306 340 382 384	reclimc	$⊢ ⊤ \to \frac{1}{1} \in ((s \in ((- π, π) ∖ \{0\}) ⟼ \frac{1}{\cos (\frac{s}{2})}) {lim}_{ℂ} 0)$
386		1div1e1	$⊢ \frac{1}{1} = 1$
387	66	fveq1i	$⊢ \frac{d (x \in ((- π, π) ∖ \{0\})⟼ x)}{d_{ℝ} x} (s) = (x \in ((- π, π) ∖ \{0\}) ⟼ 1) (s)$
388		eqidd	$⊢ s \in ((- π, π) ∖ \{0\}) \to (x \in ((- π, π) ∖ \{0\}) ⟼ 1) = (x \in ((- π, π) ∖ \{0\}) ⟼ 1)$
389		eqidd	$⊢ (s \in ((- π, π) ∖ \{0\}) \land x = s) \to 1 = 1$
390		id	$⊢ s \in ((- π, π) ∖ \{0\}) \to s \in ((- π, π) ∖ \{0\})$
391		1red	$⊢ s \in ((- π, π) ∖ \{0\}) \to 1 \in ℝ$
392	388 389 390 391	fvmptd	$⊢ s \in ((- π, π) ∖ \{0\}) \to (x \in ((- π, π) ∖ \{0\}) ⟼ 1) (s) = 1$
393	387 392	syl5req	$⊢ s \in ((- π, π) ∖ \{0\}) \to 1 = \frac{d (x \in ((- π, π) ∖ \{0\})⟼ x)}{d_{ℝ} x} (s)$
394	135	a1i	$⊢ s \in ((- π, π) ∖ \{0\}) \to \frac{d (x \in ((- π, π) ∖ \{0\})⟼ 2 \sin (\frac{x}{2}))}{d_{ℝ} x} = (x \in ((- π, π) ∖ \{0\}) ⟼ \cos (\frac{x}{2}))$
395		oveq1	$⊢ x = s \to \frac{x}{2} = \frac{s}{2}$
396	395	fveq2d	$⊢ x = s \to \cos (\frac{x}{2}) = \cos (\frac{s}{2})$
397	396	adantl	$⊢ (s \in ((- π, π) ∖ \{0\}) \land x = s) \to \cos (\frac{x}{2}) = \cos (\frac{s}{2})$
398	394 397 390 335	fvmptd	$⊢ s \in ((- π, π) ∖ \{0\}) \to \frac{d (x \in ((- π, π) ∖ \{0\})⟼ 2 \sin (\frac{x}{2}))}{d_{ℝ} x} (s) = \cos (\frac{s}{2})$
399	398	eqcomd	$⊢ s \in ((- π, π) ∖ \{0\}) \to \cos (\frac{s}{2}) = \frac{d (x \in ((- π, π) ∖ \{0\})⟼ 2 \sin (\frac{x}{2}))}{d_{ℝ} x} (s)$
400	393 399	oveq12d	$⊢ s \in ((- π, π) ∖ \{0\}) \to \frac{1}{\cos (\frac{s}{2})} = \frac{\frac{d (x \in ((- π, π) ∖ \{0\})⟼ x)}{d_{ℝ} x} (s)}{\frac{d (x \in ((- π, π) ∖ \{0\})⟼ 2 \sin (\frac{x}{2}))}{d_{ℝ} x} (s)}$
401	400	mpteq2ia	$⊢ (s \in ((- π, π) ∖ \{0\}) ⟼ \frac{1}{\cos (\frac{s}{2})}) = (s \in ((- π, π) ∖ \{0\}) ⟼ \frac{\frac{d (x \in ((- π, π) ∖ \{0\})⟼ x)}{d_{ℝ} x} (s)}{\frac{d (x \in ((- π, π) ∖ \{0\})⟼ 2 \sin (\frac{x}{2}))}{d_{ℝ} x} (s)})$
402	401	oveq1i	$⊢ (s \in ((- π, π) ∖ \{0\}) ⟼ \frac{1}{\cos (\frac{s}{2})}) {lim}_{ℂ} 0 = (s \in ((- π, π) ∖ \{0\}) ⟼ \frac{\frac{d (x \in ((- π, π) ∖ \{0\})⟼ x)}{d_{ℝ} x} (s)}{\frac{d (x \in ((- π, π) ∖ \{0\})⟼ 2 \sin (\frac{x}{2}))}{d_{ℝ} x} (s)}) {lim}_{ℂ} 0$
403	385 386 402	3eltr3g	$⊢ ⊤ \to 1 \in ((s \in ((- π, π) ∖ \{0\}) ⟼ \frac{\frac{d (x \in ((- π, π) ∖ \{0\})⟼ x)}{d_{ℝ} x} (s)}{\frac{d (x \in ((- π, π) ∖ \{0\})⟼ 2 \sin (\frac{x}{2}))}{d_{ℝ} x} (s)}) {lim}_{ℂ} 0)$
404	20 24 32 34 45 46 71 140 173 227 259 304 403	lhop	$⊢ ⊤ \to 1 \in ((s \in ((- π, π) ∖ \{0\}) ⟼ \frac{(x \in ((- π, π) ∖ \{0\}) ⟼ x) (s)}{(x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) (s)}) {lim}_{ℂ} 0)$
405	404	mptru	$⊢ 1 \in ((s \in ((- π, π) ∖ \{0\}) ⟼ \frac{(x \in ((- π, π) ∖ \{0\}) ⟼ x) (s)}{(x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) (s)}) {lim}_{ℂ} 0)$
406		eqidd	$⊢ s \in ((- π, π) ∖ \{0\}) \to (x \in ((- π, π) ∖ \{0\}) ⟼ x) = (x \in ((- π, π) ∖ \{0\}) ⟼ x)$
407		simpr	$⊢ (s \in ((- π, π) ∖ \{0\}) \land x = s) \to x = s$
408	406 407 390 307	fvmptd	$⊢ s \in ((- π, π) ∖ \{0\}) \to (x \in ((- π, π) ∖ \{0\}) ⟼ x) (s) = s$
409		eqidd	$⊢ s \in ((- π, π) ∖ \{0\}) \to (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) = (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2}))$
410	407	oveq1d	$⊢ (s \in ((- π, π) ∖ \{0\}) \land x = s) \to \frac{x}{2} = \frac{s}{2}$
411	410	fveq2d	$⊢ (s \in ((- π, π) ∖ \{0\}) \land x = s) \to \sin (\frac{x}{2}) = \sin (\frac{s}{2})$
412	411	oveq2d	$⊢ (s \in ((- π, π) ∖ \{0\}) \land x = s) \to 2 \sin (\frac{x}{2}) = 2 \sin (\frac{s}{2})$
413	26	a1i	$⊢ s \in ((- π, π) ∖ \{0\}) \to 2 \in ℝ$
414	311	resincld	$⊢ s \in ((- π, π) ∖ \{0\}) \to \sin (\frac{s}{2}) \in ℝ$
415	413 414	remulcld	$⊢ s \in ((- π, π) ∖ \{0\}) \to 2 \sin (\frac{s}{2}) \in ℝ$
416	409 412 390 415	fvmptd	$⊢ s \in ((- π, π) ∖ \{0\}) \to (x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) (s) = 2 \sin (\frac{s}{2})$
417	408 416	oveq12d	$⊢ s \in ((- π, π) ∖ \{0\}) \to \frac{(x \in ((- π, π) ∖ \{0\}) ⟼ x) (s)}{(x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) (s)} = \frac{s}{2 \sin (\frac{s}{2})}$
418	417	mpteq2ia	$⊢ (s \in ((- π, π) ∖ \{0\}) ⟼ \frac{(x \in ((- π, π) ∖ \{0\}) ⟼ x) (s)}{(x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) (s)}) = (s \in ((- π, π) ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})})$
419	418	oveq1i	$⊢ (s \in ((- π, π) ∖ \{0\}) ⟼ \frac{(x \in ((- π, π) ∖ \{0\}) ⟼ x) (s)}{(x \in ((- π, π) ∖ \{0\}) ⟼ 2 \sin (\frac{x}{2})) (s)}) {lim}_{ℂ} 0 = (s \in ((- π, π) ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})}) {lim}_{ℂ} 0$
420	405 419	eleqtri	$⊢ 1 \in ((s \in ((- π, π) ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})}) {lim}_{ℂ} 0)$
421	10	oveq1i	$⊢ K {lim}_{ℂ} 0 = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) {lim}_{ℂ} 0$
422	10	feq1i	$⊢ K : [- π, π] ⟶ ℂ \leftrightarrow (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) : [- π, π] ⟶ ℂ$
423	14 422	mpbi	$⊢ (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) : [- π, π] ⟶ ℂ$
424	423	a1i	$⊢ ⊤ \to (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) : [- π, π] ⟶ ℂ$
425	243	a1i	$⊢ ⊤ \to (- π, π) \subseteq [- π, π]$
426		iccssre	$⊢ (- π \in ℝ \land π \in ℝ) \to [- π, π] \subseteq ℝ$
427	39 38 426	mp2an	$⊢ [- π, π] \subseteq ℝ$
428	427	a1i	$⊢ ⊤ \to [- π, π] \subseteq ℝ$
429	428 12	sstrdi	$⊢ ⊤ \to [- π, π] \subseteq ℂ$
430		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ([- π, π] \cup \{0\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ([- π, π] \cup \{0\})$
431	39 35 36	ltleii	$⊢ - π \leq 0$
432	35 38 37	ltleii	$⊢ 0 \leq π$
433	39 38	elicc2i	$⊢ 0 \in [- π, π] \leftrightarrow (0 \in ℝ \land - π \leq 0 \land 0 \leq π)$
434	35 431 432 433	mpbir3an	$⊢ 0 \in [- π, π]$
435	159	snss	$⊢ 0 \in [- π, π] \leftrightarrow \{0\} \subseteq [- π, π]$
436	434 435	mpbi	$⊢ \{0\} \subseteq [- π, π]$
437		ssequn2	$⊢ \{0\} \subseteq [- π, π] \leftrightarrow [- π, π] \cup \{0\} = [- π, π]$
438	436 437	mpbi	$⊢ [- π, π] \cup \{0\} = [- π, π]$
439	438	oveq2i	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ([- π, π] \cup \{0\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} [- π, π]$
440		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
441	56 440	rerest	$⊢ [- π, π] \subseteq ℝ \to TopOpen (ℂ_{fld}) ↾_{𝑡} [- π, π] = topGen (ran (.)) ↾_{𝑡} [- π, π]$
442	427 441	ax-mp	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} [- π, π] = topGen (ran (.)) ↾_{𝑡} [- π, π]$
443	439 442	eqtri	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ([- π, π] \cup \{0\}) = topGen (ran (.)) ↾_{𝑡} [- π, π]$
444	443	fveq2i	$⊢ int (TopOpen (ℂ_{fld}) ↾_{𝑡} ([- π, π] \cup \{0\})) = int (topGen (ran (.)) ↾_{𝑡} [- π, π])$
445	159	snss	$⊢ 0 \in (- π, π) \leftrightarrow \{0\} \subseteq (- π, π)$
446	44 445	mpbi	$⊢ \{0\} \subseteq (- π, π)$
447		ssequn2	$⊢ \{0\} \subseteq (- π, π) \leftrightarrow (- π, π) \cup \{0\} = (- π, π)$
448	446 447	mpbi	$⊢ (- π, π) \cup \{0\} = (- π, π)$
449	444 448	fveq12i	$⊢ int (TopOpen (ℂ_{fld}) ↾_{𝑡} ([- π, π] \cup \{0\})) ((- π, π) \cup \{0\}) = int (topGen (ran (.)) ↾_{𝑡} [- π, π]) ((- π, π))$
450		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [- π, π] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [- π, π] \in TopOn ([- π, π])$
451	60 427 450	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [- π, π] \in TopOn ([- π, π])$
452	451	topontopi	$⊢ topGen (ran (.)) ↾_{𝑡} [- π, π] \in Top$
453		retop	$⊢ topGen (ran (.)) \in Top$
454		ovex	$⊢ [- π, π] \in V$
455	453 454	pm3.2i	$⊢ (topGen (ran (.)) \in Top \land [- π, π] \in V)$
456		ssid	$⊢ (- π, π) \subseteq (- π, π)$
457	33 243 456	3pm3.2i	$⊢ ((- π, π) \in topGen (ran (.)) \land (- π, π) \subseteq [- π, π] \land (- π, π) \subseteq (- π, π))$
458		restopnb	$⊢ ((topGen (ran (.)) \in Top \land [- π, π] \in V) \land ((- π, π) \in topGen (ran (.)) \land (- π, π) \subseteq [- π, π] \land (- π, π) \subseteq (- π, π))) \to ((- π, π) \in topGen (ran (.)) \leftrightarrow (- π, π) \in (topGen (ran (.)) ↾_{𝑡} [- π, π]))$
459	455 457 458	mp2an	$⊢ (- π, π) \in topGen (ran (.)) \leftrightarrow (- π, π) \in (topGen (ran (.)) ↾_{𝑡} [- π, π])$
460	33 459	mpbi	$⊢ (- π, π) \in (topGen (ran (.)) ↾_{𝑡} [- π, π])$
461		isopn3i	$⊢ (topGen (ran (.)) ↾_{𝑡} [- π, π] \in Top \land (- π, π) \in (topGen (ran (.)) ↾_{𝑡} [- π, π])) \to int (topGen (ran (.)) ↾_{𝑡} [- π, π]) ((- π, π)) = (- π, π)$
462	452 460 461	mp2an	$⊢ int (topGen (ran (.)) ↾_{𝑡} [- π, π]) ((- π, π)) = (- π, π)$
463		eqid	$⊢ (- π, π) = (- π, π)$
464	449 462 463	3eqtrri	$⊢ (- π, π) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ([- π, π] \cup \{0\})) ((- π, π) \cup \{0\})$
465	44 464	eleqtri	$⊢ 0 \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} ([- π, π] \cup \{0\})) ((- π, π) \cup \{0\})$
466	465	a1i	$⊢ ⊤ \to 0 \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} ([- π, π] \cup \{0\})) ((- π, π) \cup \{0\})$
467	424 425 429 56 430 466	limcres	$⊢ ⊤ \to ({(s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) ↾}_{(- π, π)}) {lim}_{ℂ} 0 = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) {lim}_{ℂ} 0$
468	467	mptru	$⊢ ({(s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) ↾}_{(- π, π)}) {lim}_{ℂ} 0 = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) {lim}_{ℂ} 0$
469	468	eqcomi	$⊢ (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) {lim}_{ℂ} 0 = ({(s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) ↾}_{(- π, π)}) {lim}_{ℂ} 0$
470		resmpt	$⊢ (- π, π) \subseteq [- π, π] \to {(s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) ↾}_{(- π, π)} = (s \in (- π, π) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
471	243 470	ax-mp	$⊢ {(s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) ↾}_{(- π, π)} = (s \in (- π, π) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
472	471	oveq1i	$⊢ ({(s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) ↾}_{(- π, π)}) {lim}_{ℂ} 0 = (s \in (- π, π) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) {lim}_{ℂ} 0$
473	421 469 472	3eqtri	$⊢ K {lim}_{ℂ} 0 = (s \in (- π, π) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) {lim}_{ℂ} 0$
474		eqid	$⊢ (s \in (- π, π) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) = (s \in (- π, π) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
475		iftrue	$⊢ s = 0 \to if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}) = 1$
476		1cnd	$⊢ s = 0 \to 1 \in ℂ$
477	475 476	eqeltrd	$⊢ s = 0 \to if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}) \in ℂ$
478	477	adantl	$⊢ (s \in (- π, π) \land s = 0) \to if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}) \in ℂ$
479		iffalse	$⊢ \neg s = 0 \to if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}) = \frac{s}{2 \sin (\frac{s}{2})}$
480	479	adantl	$⊢ (s \in (- π, π) \land \neg s = 0) \to if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}) = \frac{s}{2 \sin (\frac{s}{2})}$
481	141	adantr	$⊢ (s \in (- π, π) \land \neg s = 0) \to s \in ℂ$
482		2cnd	$⊢ (s \in (- π, π) \land \neg s = 0) \to 2 \in ℂ$
483	481	halfcld	$⊢ (s \in (- π, π) \land \neg s = 0) \to \frac{s}{2} \in ℂ$
484	483	sincld	$⊢ (s \in (- π, π) \land \neg s = 0) \to \sin (\frac{s}{2}) \in ℂ$
485	482 484	mulcld	$⊢ (s \in (- π, π) \land \neg s = 0) \to 2 \sin (\frac{s}{2}) \in ℂ$
486	81	a1i	$⊢ (s \in (- π, π) \land \neg s = 0) \to 2 \neq 0$
487	243	sseli	$⊢ s \in (- π, π) \to s \in [- π, π]$
488		neqne	$⊢ \neg s = 0 \to s \neq 0$
489		fourierdlem44	$⊢ (s \in [- π, π] \land s \neq 0) \to \sin (\frac{s}{2}) \neq 0$
490	487 488 489	syl2an	$⊢ (s \in (- π, π) \land \neg s = 0) \to \sin (\frac{s}{2}) \neq 0$
491	482 484 486 490	mulne0d	$⊢ (s \in (- π, π) \land \neg s = 0) \to 2 \sin (\frac{s}{2}) \neq 0$
492	481 485 491	divcld	$⊢ (s \in (- π, π) \land \neg s = 0) \to \frac{s}{2 \sin (\frac{s}{2})} \in ℂ$
493	480 492	eqeltrd	$⊢ (s \in (- π, π) \land \neg s = 0) \to if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}) \in ℂ$
494	478 493	pm2.61dan	$⊢ s \in (- π, π) \to if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}) \in ℂ$
495	474 494	fmpti	$⊢ (s \in (- π, π) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) : (- π, π) ⟶ ℂ$
496	495	a1i	$⊢ ⊤ \to (s \in (- π, π) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) : (- π, π) ⟶ ℂ$
497	496	limcdif	$⊢ ⊤ \to (s \in (- π, π) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) {lim}_{ℂ} 0 = ({(s \in (- π, π) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) ↾}_{((- π, π) ∖ \{0\})}) {lim}_{ℂ} 0$
498	497	mptru	$⊢ (s \in (- π, π) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) {lim}_{ℂ} 0 = ({(s \in (- π, π) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) ↾}_{((- π, π) ∖ \{0\})}) {lim}_{ℂ} 0$
499		resmpt	$⊢ (- π, π) ∖ \{0\} \subseteq (- π, π) \to {(s \in (- π, π) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) ↾}_{((- π, π) ∖ \{0\})} = (s \in ((- π, π) ∖ \{0\}) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
500	16 499	ax-mp	$⊢ {(s \in (- π, π) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) ↾}_{((- π, π) ∖ \{0\})} = (s \in ((- π, π) ∖ \{0\}) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
501		eldifn	$⊢ s \in ((- π, π) ∖ \{0\}) \to \neg s \in \{0\}$
502		velsn	$⊢ s \in \{0\} \leftrightarrow s = 0$
503	501 502	sylnib	$⊢ s \in ((- π, π) ∖ \{0\}) \to \neg s = 0$
504	503 479	syl	$⊢ s \in ((- π, π) ∖ \{0\}) \to if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}) = \frac{s}{2 \sin (\frac{s}{2})}$
505	504	mpteq2ia	$⊢ (s \in ((- π, π) ∖ \{0\}) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) = (s \in ((- π, π) ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})})$
506	500 505	eqtri	$⊢ {(s \in (- π, π) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) ↾}_{((- π, π) ∖ \{0\})} = (s \in ((- π, π) ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})})$
507	506	oveq1i	$⊢ ({(s \in (- π, π) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) ↾}_{((- π, π) ∖ \{0\})}) {lim}_{ℂ} 0 = (s \in ((- π, π) ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})}) {lim}_{ℂ} 0$
508	473 498 507	3eqtrri	$⊢ (s \in ((- π, π) ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})}) {lim}_{ℂ} 0 = K {lim}_{ℂ} 0$
509	420 508	eleqtri	$⊢ 1 \in (K {lim}_{ℂ} 0)$
510	509	a1i	$⊢ s = 0 \to 1 \in (K {lim}_{ℂ} 0)$
511		fveq2	$⊢ s = 0 \to K (s) = K (0)$
512	475 10 47	fvmpt	$⊢ 0 \in [- π, π] \to K (0) = 1$
513	434 512	ax-mp	$⊢ K (0) = 1$
514	511 513	syl6eq	$⊢ s = 0 \to K (s) = 1$
515		oveq2	$⊢ s = 0 \to K {lim}_{ℂ} s = K {lim}_{ℂ} 0$
516	510 514 515	3eltr4d	$⊢ s = 0 \to K (s) \in (K {lim}_{ℂ} s)$
517	427 12	sstri	$⊢ [- π, π] \subseteq ℂ$
518	517	a1i	$⊢ s = 0 \to [- π, π] \subseteq ℂ$
519	38	a1i	$⊢ s = 0 \to π \in ℝ$
520	519	renegcld	$⊢ s = 0 \to - π \in ℝ$
521		id	$⊢ s = 0 \to s = 0$
522	35	a1i	$⊢ s = 0 \to 0 \in ℝ$
523	521 522	eqeltrd	$⊢ s = 0 \to s \in ℝ$
524	431 521	breqtrrid	$⊢ s = 0 \to - π \leq s$
525	521 432	eqbrtrdi	$⊢ s = 0 \to s \leq π$
526	520 519 523 524 525	eliccd	$⊢ s = 0 \to s \in [- π, π]$
527	57	oveq1i	$⊢ topGen (ran (.)) ↾_{𝑡} [- π, π] = (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} [- π, π]$
528	56	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
529		reex	$⊢ ℝ \in V$
530		restabs	$⊢ (TopOpen (ℂ_{fld}) \in Top \land [- π, π] \subseteq ℝ \land ℝ \in V) \to (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} [- π, π] = TopOpen (ℂ_{fld}) ↾_{𝑡} [- π, π]$
531	528 427 529 530	mp3an	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} [- π, π] = TopOpen (ℂ_{fld}) ↾_{𝑡} [- π, π]$
532	527 531	eqtri	$⊢ topGen (ran (.)) ↾_{𝑡} [- π, π] = TopOpen (ℂ_{fld}) ↾_{𝑡} [- π, π]$
533	56 532	cnplimc	$⊢ ([- π, π] \subseteq ℂ \land s \in [- π, π]) \to (K \in ((topGen (ran (.)) ↾_{𝑡} [- π, π]) CnP TopOpen (ℂ_{fld})) (s) \leftrightarrow (K : [- π, π] ⟶ ℂ \land K (s) \in (K {lim}_{ℂ} s)))$
534	518 526 533	syl2anc	$⊢ s = 0 \to (K \in ((topGen (ran (.)) ↾_{𝑡} [- π, π]) CnP TopOpen (ℂ_{fld})) (s) \leftrightarrow (K : [- π, π] ⟶ ℂ \land K (s) \in (K {lim}_{ℂ} s)))$
535	15 516 534	mpbir2and	$⊢ s = 0 \to K \in ((topGen (ran (.)) ↾_{𝑡} [- π, π]) CnP TopOpen (ℂ_{fld})) (s)$
536	535	adantl	$⊢ (s \in [- π, π] \land s = 0) \to K \in ((topGen (ran (.)) ↾_{𝑡} [- π, π]) CnP TopOpen (ℂ_{fld})) (s)$
537		simpl	$⊢ (s \in [- π, π] \land \neg s = 0) \to s \in [- π, π]$
538	502	notbii	$⊢ \neg s \in \{0\} \leftrightarrow \neg s = 0$
539	538	biimpri	$⊢ \neg s = 0 \to \neg s \in \{0\}$
540	539	adantl	$⊢ (s \in [- π, π] \land \neg s = 0) \to \neg s \in \{0\}$
541	537 540	eldifd	$⊢ (s \in [- π, π] \land \neg s = 0) \to s \in ([- π, π] ∖ \{0\})$
542		fveq2	$⊢ x = s \to ((topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\})) CnP TopOpen (ℂ_{fld})) (x) = ((topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\})) CnP TopOpen (ℂ_{fld})) (s)$
543	542	eleq2d	$⊢ x = s \to ((s \in ([- π, π] ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})}) \in ((topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\})) CnP TopOpen (ℂ_{fld})) (x) \leftrightarrow (s \in ([- π, π] ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})}) \in ((topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\})) CnP TopOpen (ℂ_{fld})) (s))$
544	429	ssdifssd	$⊢ ⊤ \to [- π, π] ∖ \{0\} \subseteq ℂ$
545	544 145	idcncfg	$⊢ ⊤ \to (s \in ([- π, π] ∖ \{0\}) ⟼ s) : ([- π, π] ∖ \{0\}) \underset{cn}{⟶} ℂ$
546		eqid	$⊢ (s \in ([- π, π] ∖ \{0\}) ⟼ 2 \sin (\frac{s}{2})) = (s \in ([- π, π] ∖ \{0\}) ⟼ 2 \sin (\frac{s}{2}))$
547		2cnd	$⊢ s \in ([- π, π] ∖ \{0\}) \to 2 \in ℂ$
548		eldifi	$⊢ s \in ([- π, π] ∖ \{0\}) \to s \in [- π, π]$
549	517 548	sseldi	$⊢ s \in ([- π, π] ∖ \{0\}) \to s \in ℂ$
550	549	halfcld	$⊢ s \in ([- π, π] ∖ \{0\}) \to \frac{s}{2} \in ℂ$
551	550	sincld	$⊢ s \in ([- π, π] ∖ \{0\}) \to \sin (\frac{s}{2}) \in ℂ$
552	547 551	mulcld	$⊢ s \in ([- π, π] ∖ \{0\}) \to 2 \sin (\frac{s}{2}) \in ℂ$
553	81	a1i	$⊢ s \in ([- π, π] ∖ \{0\}) \to 2 \neq 0$
554		eldifsni	$⊢ s \in ([- π, π] ∖ \{0\}) \to s \neq 0$
555	548 554 489	syl2anc	$⊢ s \in ([- π, π] ∖ \{0\}) \to \sin (\frac{s}{2}) \neq 0$
556	547 551 553 555	mulne0d	$⊢ s \in ([- π, π] ∖ \{0\}) \to 2 \sin (\frac{s}{2}) \neq 0$
557	556	neneqd	$⊢ s \in ([- π, π] ∖ \{0\}) \to \neg 2 \sin (\frac{s}{2}) = 0$
558		elsng	$⊢ 2 \sin (\frac{s}{2}) \in ℂ \to (2 \sin (\frac{s}{2}) \in \{0\} \leftrightarrow 2 \sin (\frac{s}{2}) = 0)$
559	552 558	syl	$⊢ s \in ([- π, π] ∖ \{0\}) \to (2 \sin (\frac{s}{2}) \in \{0\} \leftrightarrow 2 \sin (\frac{s}{2}) = 0)$
560	557 559	mtbird	$⊢ s \in ([- π, π] ∖ \{0\}) \to \neg 2 \sin (\frac{s}{2}) \in \{0\}$
561	552 560	eldifd	$⊢ s \in ([- π, π] ∖ \{0\}) \to 2 \sin (\frac{s}{2}) \in (ℂ ∖ \{0\})$
562	546 561	fmpti	$⊢ (s \in ([- π, π] ∖ \{0\}) ⟼ 2 \sin (\frac{s}{2})) : [- π, π] ∖ \{0\} ⟶ ℂ ∖ \{0\}$
563		difss	$⊢ ℂ ∖ \{0\} \subseteq ℂ$
564		eqid	$⊢ (s \in ℂ ⟼ 2) = (s \in ℂ ⟼ 2)$
565	175 176 175	constcncfg	$⊢ 2 \in ℂ \to (s \in ℂ ⟼ 2) : ℂ \underset{cn}{⟶} ℂ$
566	102 565	mp1i	$⊢ ⊤ \to (s \in ℂ ⟼ 2) : ℂ \underset{cn}{⟶} ℂ$
567		2cnd	$⊢ (⊤ \land s \in ([- π, π] ∖ \{0\})) \to 2 \in ℂ$
568	564 566 544 145 567	cncfmptssg	$⊢ ⊤ \to (s \in ([- π, π] ∖ \{0\}) ⟼ 2) : ([- π, π] ∖ \{0\}) \underset{cn}{⟶} ℂ$
569	549 547 553	divrecd	$⊢ s \in ([- π, π] ∖ \{0\}) \to \frac{s}{2} = s (\frac{1}{2})$
570	569	mpteq2ia	$⊢ (s \in ([- π, π] ∖ \{0\}) ⟼ \frac{s}{2}) = (s \in ([- π, π] ∖ \{0\}) ⟼ s (\frac{1}{2}))$
571		eqid	$⊢ (s \in ℂ ⟼ \frac{1}{2}) = (s \in ℂ ⟼ \frac{1}{2})$
572	144	a1i	$⊢ \frac{1}{2} \in ℂ \to ℂ \subseteq ℂ$
573		id	$⊢ \frac{1}{2} \in ℂ \to \frac{1}{2} \in ℂ$
574	572 573 572	constcncfg	$⊢ \frac{1}{2} \in ℂ \to (s \in ℂ ⟼ \frac{1}{2}) : ℂ \underset{cn}{⟶} ℂ$
575	94 574	mp1i	$⊢ ⊤ \to (s \in ℂ ⟼ \frac{1}{2}) : ℂ \underset{cn}{⟶} ℂ$
576	94	a1i	$⊢ (⊤ \land s \in ([- π, π] ∖ \{0\})) \to \frac{1}{2} \in ℂ$
577	571 575 544 145 576	cncfmptssg	$⊢ ⊤ \to (s \in ([- π, π] ∖ \{0\}) ⟼ \frac{1}{2}) : ([- π, π] ∖ \{0\}) \underset{cn}{⟶} ℂ$
578	545 577	mulcncf	$⊢ ⊤ \to (s \in ([- π, π] ∖ \{0\}) ⟼ s (\frac{1}{2})) : ([- π, π] ∖ \{0\}) \underset{cn}{⟶} ℂ$
579	570 578	eqeltrid	$⊢ ⊤ \to (s \in ([- π, π] ∖ \{0\}) ⟼ \frac{s}{2}) : ([- π, π] ∖ \{0\}) \underset{cn}{⟶} ℂ$
580	182 579	cncfmpt1f	$⊢ ⊤ \to (s \in ([- π, π] ∖ \{0\}) ⟼ \sin (\frac{s}{2})) : ([- π, π] ∖ \{0\}) \underset{cn}{⟶} ℂ$
581	568 580	mulcncf	$⊢ ⊤ \to (s \in ([- π, π] ∖ \{0\}) ⟼ 2 \sin (\frac{s}{2})) : ([- π, π] ∖ \{0\}) \underset{cn}{⟶} ℂ$
582	581	mptru	$⊢ (s \in ([- π, π] ∖ \{0\}) ⟼ 2 \sin (\frac{s}{2})) : ([- π, π] ∖ \{0\}) \underset{cn}{⟶} ℂ$
583		cncffvrn	$⊢ (ℂ ∖ \{0\} \subseteq ℂ \land (s \in ([- π, π] ∖ \{0\}) ⟼ 2 \sin (\frac{s}{2})) : ([- π, π] ∖ \{0\}) \underset{cn}{⟶} ℂ) \to ((s \in ([- π, π] ∖ \{0\}) ⟼ 2 \sin (\frac{s}{2})) : ([- π, π] ∖ \{0\}) \underset{cn}{⟶} (ℂ ∖ \{0\}) \leftrightarrow (s \in ([- π, π] ∖ \{0\}) ⟼ 2 \sin (\frac{s}{2})) : [- π, π] ∖ \{0\} ⟶ ℂ ∖ \{0\})$
584	563 582 583	mp2an	$⊢ (s \in ([- π, π] ∖ \{0\}) ⟼ 2 \sin (\frac{s}{2})) : ([- π, π] ∖ \{0\}) \underset{cn}{⟶} (ℂ ∖ \{0\}) \leftrightarrow (s \in ([- π, π] ∖ \{0\}) ⟼ 2 \sin (\frac{s}{2})) : [- π, π] ∖ \{0\} ⟶ ℂ ∖ \{0\}$
585	562 584	mpbir	$⊢ (s \in ([- π, π] ∖ \{0\}) ⟼ 2 \sin (\frac{s}{2})) : ([- π, π] ∖ \{0\}) \underset{cn}{⟶} (ℂ ∖ \{0\})$
586	585	a1i	$⊢ ⊤ \to (s \in ([- π, π] ∖ \{0\}) ⟼ 2 \sin (\frac{s}{2})) : ([- π, π] ∖ \{0\}) \underset{cn}{⟶} (ℂ ∖ \{0\})$
587	545 586	divcncf	$⊢ ⊤ \to (s \in ([- π, π] ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})}) : ([- π, π] ∖ \{0\}) \underset{cn}{⟶} ℂ$
588	587	mptru	$⊢ (s \in ([- π, π] ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})}) : ([- π, π] ∖ \{0\}) \underset{cn}{⟶} ℂ$
589	428	ssdifssd	$⊢ ⊤ \to [- π, π] ∖ \{0\} \subseteq ℝ$
590	589	mptru	$⊢ [- π, π] ∖ \{0\} \subseteq ℝ$
591	590 12	sstri	$⊢ [- π, π] ∖ \{0\} \subseteq ℂ$
592	57	oveq1i	$⊢ topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\}) = (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} ([- π, π] ∖ \{0\})$
593		restabs	$⊢ (TopOpen (ℂ_{fld}) \in Top \land [- π, π] ∖ \{0\} \subseteq ℝ \land ℝ \in V) \to (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} ([- π, π] ∖ \{0\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ([- π, π] ∖ \{0\})$
594	528 590 529 593	mp3an	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} ([- π, π] ∖ \{0\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ([- π, π] ∖ \{0\})$
595	592 594	eqtri	$⊢ topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ([- π, π] ∖ \{0\})$
596		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
597	596	restid	$⊢ TopOpen (ℂ_{fld}) \in Top \to TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
598	528 597	ax-mp	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ = TopOpen (ℂ_{fld})$
599	598	eqcomi	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
600	56 595 599	cncfcn	$⊢ ([- π, π] ∖ \{0\} \subseteq ℂ \land ℂ \subseteq ℂ) \to ([- π, π] ∖ \{0\}) \underset{cn}{⟶} ℂ = (topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\})) Cn TopOpen (ℂ_{fld})$
601	591 144 600	mp2an	$⊢ ([- π, π] ∖ \{0\}) \underset{cn}{⟶} ℂ = (topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\})) Cn TopOpen (ℂ_{fld})$
602	588 601	eleqtri	$⊢ (s \in ([- π, π] ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})}) \in ((topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\})) Cn TopOpen (ℂ_{fld}))$
603		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [- π, π] ∖ \{0\} \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\}) \in TopOn ([- π, π] ∖ \{0\})$
604	60 590 603	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\}) \in TopOn ([- π, π] ∖ \{0\})$
605	56	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
606		cncnp	$⊢ (topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\}) \in TopOn ([- π, π] ∖ \{0\}) \land TopOpen (ℂ_{fld}) \in TopOn (ℂ)) \to ((s \in ([- π, π] ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})}) \in ((topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\})) Cn TopOpen (ℂ_{fld})) \leftrightarrow ((s \in ([- π, π] ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})}) : [- π, π] ∖ \{0\} ⟶ ℂ \land \forall x \in ([- π, π] ∖ \{0\}) (s \in ([- π, π] ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})}) \in ((topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\})) CnP TopOpen (ℂ_{fld})) (x)))$
607	604 605 606	mp2an	$⊢ (s \in ([- π, π] ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})}) \in ((topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\})) Cn TopOpen (ℂ_{fld})) \leftrightarrow ((s \in ([- π, π] ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})}) : [- π, π] ∖ \{0\} ⟶ ℂ \land \forall x \in ([- π, π] ∖ \{0\}) (s \in ([- π, π] ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})}) \in ((topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\})) CnP TopOpen (ℂ_{fld})) (x))$
608	602 607	mpbi	$⊢ ((s \in ([- π, π] ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})}) : [- π, π] ∖ \{0\} ⟶ ℂ \land \forall x \in ([- π, π] ∖ \{0\}) (s \in ([- π, π] ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})}) \in ((topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\})) CnP TopOpen (ℂ_{fld})) (x))$
609	608	simpri	$⊢ \forall x \in ([- π, π] ∖ \{0\}) (s \in ([- π, π] ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})}) \in ((topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\})) CnP TopOpen (ℂ_{fld})) (x)$
610	543 609	vtoclri	$⊢ s \in ([- π, π] ∖ \{0\}) \to (s \in ([- π, π] ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})}) \in ((topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\})) CnP TopOpen (ℂ_{fld})) (s)$
611	541 610	syl	$⊢ (s \in [- π, π] \land \neg s = 0) \to (s \in ([- π, π] ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})}) \in ((topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\})) CnP TopOpen (ℂ_{fld})) (s)$
612	10	reseq1i	$⊢ {K ↾}_{([- π, π] ∖ \{0\})} = {(s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) ↾}_{([- π, π] ∖ \{0\})}$
613		difss	$⊢ [- π, π] ∖ \{0\} \subseteq [- π, π]$
614		resmpt	$⊢ [- π, π] ∖ \{0\} \subseteq [- π, π] \to {(s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) ↾}_{([- π, π] ∖ \{0\})} = (s \in ([- π, π] ∖ \{0\}) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
615	613 614	ax-mp	$⊢ {(s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) ↾}_{([- π, π] ∖ \{0\})} = (s \in ([- π, π] ∖ \{0\}) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
616		eldifn	$⊢ s \in ([- π, π] ∖ \{0\}) \to \neg s \in \{0\}$
617	616 502	sylnib	$⊢ s \in ([- π, π] ∖ \{0\}) \to \neg s = 0$
618	617 479	syl	$⊢ s \in ([- π, π] ∖ \{0\}) \to if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}) = \frac{s}{2 \sin (\frac{s}{2})}$
619	618	mpteq2ia	$⊢ (s \in ([- π, π] ∖ \{0\}) ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})})) = (s \in ([- π, π] ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})})$
620	612 615 619	3eqtri	$⊢ {K ↾}_{([- π, π] ∖ \{0\})} = (s \in ([- π, π] ∖ \{0\}) ⟼ \frac{s}{2 \sin (\frac{s}{2})})$
621		restabs	$⊢ (topGen (ran (.)) \in Top \land [- π, π] ∖ \{0\} \subseteq [- π, π] \land [- π, π] \in V) \to (topGen (ran (.)) ↾_{𝑡} [- π, π]) ↾_{𝑡} ([- π, π] ∖ \{0\}) = topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\})$
622	453 613 454 621	mp3an	$⊢ (topGen (ran (.)) ↾_{𝑡} [- π, π]) ↾_{𝑡} ([- π, π] ∖ \{0\}) = topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\})$
623	622	oveq1i	$⊢ ((topGen (ran (.)) ↾_{𝑡} [- π, π]) ↾_{𝑡} ([- π, π] ∖ \{0\})) CnP TopOpen (ℂ_{fld}) = (topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\})) CnP TopOpen (ℂ_{fld})$
624	623	fveq1i	$⊢ (((topGen (ran (.)) ↾_{𝑡} [- π, π]) ↾_{𝑡} ([- π, π] ∖ \{0\})) CnP TopOpen (ℂ_{fld})) (s) = ((topGen (ran (.)) ↾_{𝑡} ([- π, π] ∖ \{0\})) CnP TopOpen (ℂ_{fld})) (s)$
625	611 620 624	3eltr4g	$⊢ (s \in [- π, π] \land \neg s = 0) \to {K ↾}_{([- π, π] ∖ \{0\})} \in (((topGen (ran (.)) ↾_{𝑡} [- π, π]) ↾_{𝑡} ([- π, π] ∖ \{0\})) CnP TopOpen (ℂ_{fld})) (s)$
626	452 613	pm3.2i	$⊢ (topGen (ran (.)) ↾_{𝑡} [- π, π] \in Top \land [- π, π] ∖ \{0\} \subseteq [- π, π])$
627	626	a1i	$⊢ (s \in [- π, π] \land \neg s = 0) \to (topGen (ran (.)) ↾_{𝑡} [- π, π] \in Top \land [- π, π] ∖ \{0\} \subseteq [- π, π])$
628		ssdif	$⊢ [- π, π] \subseteq ℝ \to [- π, π] ∖ \{0\} \subseteq ℝ ∖ \{0\}$
629	427 628	ax-mp	$⊢ [- π, π] ∖ \{0\} \subseteq ℝ ∖ \{0\}$
630	629 541	sseldi	$⊢ (s \in [- π, π] \land \neg s = 0) \to s \in (ℝ ∖ \{0\})$
631		sscon	$⊢ \{0\} \subseteq [- π, π] \to ℝ ∖ [- π, π] \subseteq ℝ ∖ \{0\}$
632	436 631	ax-mp	$⊢ ℝ ∖ [- π, π] \subseteq ℝ ∖ \{0\}$
633	629 632	unssi	$⊢ ([- π, π] ∖ \{0\}) \cup (ℝ ∖ [- π, π]) \subseteq ℝ ∖ \{0\}$
634		simpr	$⊢ (s \in (ℝ ∖ \{0\}) \land s \in [- π, π]) \to s \in [- π, π]$
635		eldifn	$⊢ s \in (ℝ ∖ \{0\}) \to \neg s \in \{0\}$
636	635	adantr	$⊢ (s \in (ℝ ∖ \{0\}) \land s \in [- π, π]) \to \neg s \in \{0\}$
637	634 636	eldifd	$⊢ (s \in (ℝ ∖ \{0\}) \land s \in [- π, π]) \to s \in ([- π, π] ∖ \{0\})$
638		elun1	$⊢ s \in ([- π, π] ∖ \{0\}) \to s \in (([- π, π] ∖ \{0\}) \cup (ℝ ∖ [- π, π]))$
639	637 638	syl	$⊢ (s \in (ℝ ∖ \{0\}) \land s \in [- π, π]) \to s \in (([- π, π] ∖ \{0\}) \cup (ℝ ∖ [- π, π]))$
640		eldifi	$⊢ s \in (ℝ ∖ \{0\}) \to s \in ℝ$
641	640	adantr	$⊢ (s \in (ℝ ∖ \{0\}) \land \neg s \in [- π, π]) \to s \in ℝ$
642		simpr	$⊢ (s \in (ℝ ∖ \{0\}) \land \neg s \in [- π, π]) \to \neg s \in [- π, π]$
643	641 642	eldifd	$⊢ (s \in (ℝ ∖ \{0\}) \land \neg s \in [- π, π]) \to s \in (ℝ ∖ [- π, π])$
644		elun2	$⊢ s \in (ℝ ∖ [- π, π]) \to s \in (([- π, π] ∖ \{0\}) \cup (ℝ ∖ [- π, π]))$
645	643 644	syl	$⊢ (s \in (ℝ ∖ \{0\}) \land \neg s \in [- π, π]) \to s \in (([- π, π] ∖ \{0\}) \cup (ℝ ∖ [- π, π]))$
646	639 645	pm2.61dan	$⊢ s \in (ℝ ∖ \{0\}) \to s \in (([- π, π] ∖ \{0\}) \cup (ℝ ∖ [- π, π]))$
647	646	ssriv	$⊢ ℝ ∖ \{0\} \subseteq ([- π, π] ∖ \{0\}) \cup (ℝ ∖ [- π, π])$
648	633 647	eqssi	$⊢ ([- π, π] ∖ \{0\}) \cup (ℝ ∖ [- π, π]) = ℝ ∖ \{0\}$
649	648	fveq2i	$⊢ int (topGen (ran (.))) (([- π, π] ∖ \{0\}) \cup (ℝ ∖ [- π, π])) = int (topGen (ran (.))) (ℝ ∖ \{0\})$
650	61	cldopn	$⊢ \{0\} \in Clsd (topGen (ran (.))) \to ℝ ∖ \{0\} \in topGen (ran (.))$
651	59 650	ax-mp	$⊢ ℝ ∖ \{0\} \in topGen (ran (.))$
652		isopn3i	$⊢ (topGen (ran (.)) \in Top \land ℝ ∖ \{0\} \in topGen (ran (.))) \to int (topGen (ran (.))) (ℝ ∖ \{0\}) = ℝ ∖ \{0\}$
653	453 651 652	mp2an	$⊢ int (topGen (ran (.))) (ℝ ∖ \{0\}) = ℝ ∖ \{0\}$
654	649 653	eqtri	$⊢ int (topGen (ran (.))) (([- π, π] ∖ \{0\}) \cup (ℝ ∖ [- π, π])) = ℝ ∖ \{0\}$
655	630 654	eleqtrrdi	$⊢ (s \in [- π, π] \land \neg s = 0) \to s \in int (topGen (ran (.))) (([- π, π] ∖ \{0\}) \cup (ℝ ∖ [- π, π]))$
656	655 537	elind	$⊢ (s \in [- π, π] \land \neg s = 0) \to s \in (int (topGen (ran (.))) (([- π, π] ∖ \{0\}) \cup (ℝ ∖ [- π, π])) \cap [- π, π])$
657		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [- π, π] = topGen (ran (.)) ↾_{𝑡} [- π, π]$
658	61 657	restntr	$⊢ (topGen (ran (.)) \in Top \land [- π, π] \subseteq ℝ \land [- π, π] ∖ \{0\} \subseteq [- π, π]) \to int (topGen (ran (.)) ↾_{𝑡} [- π, π]) ([- π, π] ∖ \{0\}) = int (topGen (ran (.))) (([- π, π] ∖ \{0\}) \cup (ℝ ∖ [- π, π])) \cap [- π, π]$
659	453 427 613 658	mp3an	$⊢ int (topGen (ran (.)) ↾_{𝑡} [- π, π]) ([- π, π] ∖ \{0\}) = int (topGen (ran (.))) (([- π, π] ∖ \{0\}) \cup (ℝ ∖ [- π, π])) \cap [- π, π]$
660	656 659	eleqtrrdi	$⊢ (s \in [- π, π] \land \neg s = 0) \to s \in int (topGen (ran (.)) ↾_{𝑡} [- π, π]) ([- π, π] ∖ \{0\})$
661	14	a1i	$⊢ (s \in [- π, π] \land \neg s = 0) \to K : [- π, π] ⟶ ℂ$
662	451	toponunii	$⊢ [- π, π] = ⋃ (topGen (ran (.)) ↾_{𝑡} [- π, π])$
663	662 596	cnprest	$⊢ ((topGen (ran (.)) ↾_{𝑡} [- π, π] \in Top \land [- π, π] ∖ \{0\} \subseteq [- π, π]) \land (s \in int (topGen (ran (.)) ↾_{𝑡} [- π, π]) ([- π, π] ∖ \{0\}) \land K : [- π, π] ⟶ ℂ)) \to (K \in ((topGen (ran (.)) ↾_{𝑡} [- π, π]) CnP TopOpen (ℂ_{fld})) (s) \leftrightarrow {K ↾}_{([- π, π] ∖ \{0\})} \in (((topGen (ran (.)) ↾_{𝑡} [- π, π]) ↾_{𝑡} ([- π, π] ∖ \{0\})) CnP TopOpen (ℂ_{fld})) (s))$
664	627 660 661 663	syl12anc	$⊢ (s \in [- π, π] \land \neg s = 0) \to (K \in ((topGen (ran (.)) ↾_{𝑡} [- π, π]) CnP TopOpen (ℂ_{fld})) (s) \leftrightarrow {K ↾}_{([- π, π] ∖ \{0\})} \in (((topGen (ran (.)) ↾_{𝑡} [- π, π]) ↾_{𝑡} ([- π, π] ∖ \{0\})) CnP TopOpen (ℂ_{fld})) (s))$
665	625 664	mpbird	$⊢ (s \in [- π, π] \land \neg s = 0) \to K \in ((topGen (ran (.)) ↾_{𝑡} [- π, π]) CnP TopOpen (ℂ_{fld})) (s)$
666	536 665	pm2.61dan	$⊢ s \in [- π, π] \to K \in ((topGen (ran (.)) ↾_{𝑡} [- π, π]) CnP TopOpen (ℂ_{fld})) (s)$
667	666	rgen	$⊢ \forall s \in [- π, π] K \in ((topGen (ran (.)) ↾_{𝑡} [- π, π]) CnP TopOpen (ℂ_{fld})) (s)$
668		cncnp	$⊢ (topGen (ran (.)) ↾_{𝑡} [- π, π] \in TopOn ([- π, π]) \land TopOpen (ℂ_{fld}) \in TopOn (ℂ)) \to (K \in ((topGen (ran (.)) ↾_{𝑡} [- π, π]) Cn TopOpen (ℂ_{fld})) \leftrightarrow (K : [- π, π] ⟶ ℂ \land \forall s \in [- π, π] K \in ((topGen (ran (.)) ↾_{𝑡} [- π, π]) CnP TopOpen (ℂ_{fld})) (s)))$
669	451 605 668	mp2an	$⊢ K \in ((topGen (ran (.)) ↾_{𝑡} [- π, π]) Cn TopOpen (ℂ_{fld})) \leftrightarrow (K : [- π, π] ⟶ ℂ \land \forall s \in [- π, π] K \in ((topGen (ran (.)) ↾_{𝑡} [- π, π]) CnP TopOpen (ℂ_{fld})) (s))$
670	14 667 669	mpbir2an	$⊢ K \in ((topGen (ran (.)) ↾_{𝑡} [- π, π]) Cn TopOpen (ℂ_{fld}))$
671	56 532 599	cncfcn	$⊢ ([- π, π] \subseteq ℂ \land ℂ \subseteq ℂ) \to [- π, π] \underset{cn}{⟶} ℂ = (topGen (ran (.)) ↾_{𝑡} [- π, π]) Cn TopOpen (ℂ_{fld})$
672	517 144 671	mp2an	$⊢ [- π, π] \underset{cn}{⟶} ℂ = (topGen (ran (.)) ↾_{𝑡} [- π, π]) Cn TopOpen (ℂ_{fld})$
673	672	eqcomi	$⊢ (topGen (ran (.)) ↾_{𝑡} [- π, π]) Cn TopOpen (ℂ_{fld}) = [- π, π] \underset{cn}{⟶} ℂ$
674	670 673	eleqtri	$⊢ K : [- π, π] \underset{cn}{⟶} ℂ$
675		cncffvrn	$⊢ (ℝ \subseteq ℂ \land K : [- π, π] \underset{cn}{⟶} ℂ) \to (K : [- π, π] \underset{cn}{⟶} ℝ \leftrightarrow K : [- π, π] ⟶ ℝ)$
676	12 674 675	mp2an	$⊢ K : [- π, π] \underset{cn}{⟶} ℝ \leftrightarrow K : [- π, π] ⟶ ℝ$
677	11 676	mpbir	$⊢ K : [- π, π] \underset{cn}{⟶} ℝ$

Metamath Proof Explorer

Theorem fourierdlem62

Proof