fouriersw

Description: Fourier series convergence, for the square wave function. Where F is discontinuous, the series converges to 0 , the average value of the left and the right limits. Notice that F is an odd function and its Fourier expansion has only sine terms (coefficients for cosine terms are zero). (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fouriersw.t	$⊢ T = 2 π$
	fouriersw.f	$⊢ F = (x \in ℝ ⟼ if (x \mod T < π, 1, - 1))$
	fouriersw.x	$⊢ X \in ℝ$
	fouriersw.z	$⊢ S = (n \in ℕ ⟼ \frac{\sin (2 n - 1) X}{2 n - 1})$
	fouriersw.y	$⊢ Y = if (X \mod π = 0, 0, F (X))$
Assertion	fouriersw	$⊢ ((\frac{4}{π}) \sum_{k \in ℕ} (\frac{\sin (2 k - 1) X}{2 k - 1}) = Y \land seq 1 (+ S) ⇝ (\frac{π}{4}) Y)$

Proof

Step	Hyp	Ref	Expression
1		fouriersw.t	$⊢ T = 2 π$
2		fouriersw.f	$⊢ F = (x \in ℝ ⟼ if (x \mod T < π, 1, - 1))$
3		fouriersw.x	$⊢ X \in ℝ$
4		fouriersw.z	$⊢ S = (n \in ℕ ⟼ \frac{\sin (2 n - 1) X}{2 n - 1})$
5		fouriersw.y	$⊢ Y = if (X \mod π = 0, 0, F (X))$
6		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
7		1zzd	$⊢ ⊤ \to 1 \in ℤ$
8		eqidd	$⊢ k \in ℕ \to (n \in ℕ ⟼ \frac{\sin (2 n - 1) X}{2 n - 1}) = (n \in ℕ ⟼ \frac{\sin (2 n - 1) X}{2 n - 1})$
9		oveq2	$⊢ n = k \to 2 n = 2 k$
10	9	oveq1d	$⊢ n = k \to 2 n - 1 = 2 k - 1$
11	10	oveq1d	$⊢ n = k \to (2 n - 1) X = (2 k - 1) X$
12	11	fveq2d	$⊢ n = k \to \sin (2 n - 1) X = \sin (2 k - 1) X$
13	12 10	oveq12d	$⊢ n = k \to \frac{\sin (2 n - 1) X}{2 n - 1} = \frac{\sin (2 k - 1) X}{2 k - 1}$
14	13	adantl	$⊢ (k \in ℕ \land n = k) \to \frac{\sin (2 n - 1) X}{2 n - 1} = \frac{\sin (2 k - 1) X}{2 k - 1}$
15		id	$⊢ k \in ℕ \to k \in ℕ$
16		ovex	$⊢ \frac{\sin (2 k - 1) X}{2 k - 1} \in V$
17	16	a1i	$⊢ k \in ℕ \to \frac{\sin (2 k - 1) X}{2 k - 1} \in V$
18	8 14 15 17	fvmptd	$⊢ k \in ℕ \to (n \in ℕ ⟼ \frac{\sin (2 n - 1) X}{2 n - 1}) (k) = \frac{\sin (2 k - 1) X}{2 k - 1}$
19	18	adantl	$⊢ (⊤ \land k \in ℕ) \to (n \in ℕ ⟼ \frac{\sin (2 n - 1) X}{2 n - 1}) (k) = \frac{\sin (2 k - 1) X}{2 k - 1}$
20		2z	$⊢ 2 \in ℤ$
21	20	a1i	$⊢ k \in ℕ \to 2 \in ℤ$
22		nnz	$⊢ k \in ℕ \to k \in ℤ$
23	21 22	zmulcld	$⊢ k \in ℕ \to 2 k \in ℤ$
24		1zzd	$⊢ k \in ℕ \to 1 \in ℤ$
25	23 24	zsubcld	$⊢ k \in ℕ \to 2 k - 1 \in ℤ$
26	25	zcnd	$⊢ k \in ℕ \to 2 k - 1 \in ℂ$
27	3	recni	$⊢ X \in ℂ$
28	27	a1i	$⊢ k \in ℕ \to X \in ℂ$
29	26 28	mulcld	$⊢ k \in ℕ \to (2 k - 1) X \in ℂ$
30	29	sincld	$⊢ k \in ℕ \to \sin (2 k - 1) X \in ℂ$
31		0red	$⊢ k \in ℕ \to 0 \in ℝ$
32		2re	$⊢ 2 \in ℝ$
33	32	a1i	$⊢ k \in ℕ \to 2 \in ℝ$
34		1red	$⊢ k \in ℕ \to 1 \in ℝ$
35	33 34	remulcld	$⊢ k \in ℕ \to 2 \cdot 1 \in ℝ$
36	35 34	resubcld	$⊢ k \in ℕ \to 2 \cdot 1 - 1 \in ℝ$
37	25	zred	$⊢ k \in ℕ \to 2 k - 1 \in ℝ$
38		0lt1	$⊢ 0 < 1$
39		2t1e2	$⊢ 2 \cdot 1 = 2$
40	39	oveq1i	$⊢ 2 \cdot 1 - 1 = 2 - 1$
41		2m1e1	$⊢ 2 - 1 = 1$
42	40 41	eqtr2i	$⊢ 1 = 2 \cdot 1 - 1$
43	38 42	breqtri	$⊢ 0 < 2 \cdot 1 - 1$
44	43	a1i	$⊢ k \in ℕ \to 0 < 2 \cdot 1 - 1$
45	23	zred	$⊢ k \in ℕ \to 2 k \in ℝ$
46		nnre	$⊢ k \in ℕ \to k \in ℝ$
47		0le2	$⊢ 0 \leq 2$
48	47	a1i	$⊢ k \in ℕ \to 0 \leq 2$
49		nnge1	$⊢ k \in ℕ \to 1 \leq k$
50	34 46 33 48 49	lemul2ad	$⊢ k \in ℕ \to 2 \cdot 1 \leq 2 k$
51	35 45 34 50	lesub1dd	$⊢ k \in ℕ \to 2 \cdot 1 - 1 \leq 2 k - 1$
52	31 36 37 44 51	ltletrd	$⊢ k \in ℕ \to 0 < 2 k - 1$
53	31 52	gtned	$⊢ k \in ℕ \to 2 k - 1 \neq 0$
54	30 26 53	divcld	$⊢ k \in ℕ \to \frac{\sin (2 k - 1) X}{2 k - 1} \in ℂ$
55	54	adantl	$⊢ (⊤ \land k \in ℕ) \to \frac{\sin (2 k - 1) X}{2 k - 1} \in ℂ$
56		picn	$⊢ π \in ℂ$
57	56	a1i	$⊢ ⊤ \to π \in ℂ$
58		4cn	$⊢ 4 \in ℂ$
59	58	a1i	$⊢ ⊤ \to 4 \in ℂ$
60		4ne0	$⊢ 4 \neq 0$
61	60	a1i	$⊢ ⊤ \to 4 \neq 0$
62	57 59 61	divcld	$⊢ ⊤ \to \frac{π}{4} \in ℂ$
63		eqid	$⊢ (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) = (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X))$
64		0cnd	$⊢ n \in ℕ \to 0 \in ℂ$
65	58	a1i	$⊢ n \in ℕ \to 4 \in ℂ$
66		nncn	$⊢ n \in ℕ \to n \in ℂ$
67		mulcl	$⊢ (n \in ℂ \land π \in ℂ) \to n π \in ℂ$
68	66 56 67	sylancl	$⊢ n \in ℕ \to n π \in ℂ$
69	56	a1i	$⊢ n \in ℕ \to π \in ℂ$
70		nnne0	$⊢ n \in ℕ \to n \neq 0$
71		0re	$⊢ 0 \in ℝ$
72		pipos	$⊢ 0 < π$
73	71 72	gtneii	$⊢ π \neq 0$
74	73	a1i	$⊢ n \in ℕ \to π \neq 0$
75	66 69 70 74	mulne0d	$⊢ n \in ℕ \to n π \neq 0$
76	65 68 75	divcld	$⊢ n \in ℕ \to \frac{4}{n π} \in ℂ$
77	27	a1i	$⊢ n \in ℕ \to X \in ℂ$
78	66 77	mulcld	$⊢ n \in ℕ \to n X \in ℂ$
79	78	sincld	$⊢ n \in ℕ \to \sin n X \in ℂ$
80	76 79	mulcld	$⊢ n \in ℕ \to (\frac{4}{n π}) \sin n X \in ℂ$
81	64 80	ifcld	$⊢ n \in ℕ \to if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X) \in ℂ$
82	63 81	fmpti	$⊢ (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) : ℕ ⟶ ℂ$
83	82	a1i	$⊢ ⊤ \to (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) : ℕ ⟶ ℂ$
84		eqidd	$⊢ k \in ℕ \to (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) = (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X))$
85		breq2	$⊢ n = k \to (2 ∥ n \leftrightarrow 2 ∥ k)$
86		oveq1	$⊢ n = k \to n π = k π$
87	86	oveq2d	$⊢ n = k \to \frac{4}{n π} = \frac{4}{k π}$
88		oveq1	$⊢ n = k \to n X = k X$
89	88	fveq2d	$⊢ n = k \to \sin n X = \sin k X$
90	87 89	oveq12d	$⊢ n = k \to (\frac{4}{n π}) \sin n X = (\frac{4}{k π}) \sin k X$
91	85 90	ifbieq2d	$⊢ n = k \to if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X) = if (2 ∥ k, 0, (\frac{4}{k π}) \sin k X)$
92	91	adantl	$⊢ (k \in ℕ \land n = k) \to if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X) = if (2 ∥ k, 0, (\frac{4}{k π}) \sin k X)$
93		c0ex	$⊢ 0 \in V$
94		ovex	$⊢ (\frac{4}{k π}) \sin k X \in V$
95	93 94	ifex	$⊢ if (2 ∥ k, 0, (\frac{4}{k π}) \sin k X) \in V$
96	95	a1i	$⊢ k \in ℕ \to if (2 ∥ k, 0, (\frac{4}{k π}) \sin k X) \in V$
97	84 92 15 96	fvmptd	$⊢ k \in ℕ \to (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) (k) = if (2 ∥ k, 0, (\frac{4}{k π}) \sin k X)$
98	97	adantr	$⊢ (k \in ℕ \land \frac{k}{2} \in ℕ) \to (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) (k) = if (2 ∥ k, 0, (\frac{4}{k π}) \sin k X)$
99		simpr	$⊢ (k \in ℕ \land \frac{k}{2} \in ℕ) \to \frac{k}{2} \in ℕ$
100		simpl	$⊢ (k \in ℕ \land \frac{k}{2} \in ℕ) \to k \in ℕ$
101		2nn	$⊢ 2 \in ℕ$
102		nndivdvds	$⊢ (k \in ℕ \land 2 \in ℕ) \to (2 ∥ k \leftrightarrow \frac{k}{2} \in ℕ)$
103	100 101 102	sylancl	$⊢ (k \in ℕ \land \frac{k}{2} \in ℕ) \to (2 ∥ k \leftrightarrow \frac{k}{2} \in ℕ)$
104	99 103	mpbird	$⊢ (k \in ℕ \land \frac{k}{2} \in ℕ) \to 2 ∥ k$
105	104	iftrued	$⊢ (k \in ℕ \land \frac{k}{2} \in ℕ) \to if (2 ∥ k, 0, (\frac{4}{k π}) \sin k X) = 0$
106	98 105	eqtrd	$⊢ (k \in ℕ \land \frac{k}{2} \in ℕ) \to (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) (k) = 0$
107	106	3adant1	$⊢ (⊤ \land k \in ℕ \land \frac{k}{2} \in ℕ) \to (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) (k) = 0$
108		1re	$⊢ 1 \in ℝ$
109	108	renegcli	$⊢ - 1 \in ℝ$
110	108 109	ifcli	$⊢ if (x \mod T < π, 1, - 1) \in ℝ$
111	110	a1i	$⊢ x \in ℝ \to if (x \mod T < π, 1, - 1) \in ℝ$
112	2 111	fmpti	$⊢ F : ℝ ⟶ ℝ$
113		oveq1	$⊢ x = y \to x \mod T = y \mod T$
114	113	breq1d	$⊢ x = y \to (x \mod T < π \leftrightarrow y \mod T < π)$
115	114	ifbid	$⊢ x = y \to if (x \mod T < π, 1, - 1) = if (y \mod T < π, 1, - 1)$
116	115	cbvmptv	$⊢ (x \in ℝ ⟼ if (x \mod T < π, 1, - 1)) = (y \in ℝ ⟼ if (y \mod T < π, 1, - 1))$
117	2 116	eqtri	$⊢ F = (y \in ℝ ⟼ if (y \mod T < π, 1, - 1))$
118	117	a1i	$⊢ x \in ℝ \to F = (y \in ℝ ⟼ if (y \mod T < π, 1, - 1))$
119		oveq1	$⊢ y = x + T \to y \mod T = (x + T) \mod T$
120		pire	$⊢ π \in ℝ$
121	32 120	remulcli	$⊢ 2 π \in ℝ$
122	1 121	eqeltri	$⊢ T \in ℝ$
123	122	recni	$⊢ T \in ℂ$
124	123	mullidi	$⊢ 1 T = T$
125	124	eqcomi	$⊢ T = 1 T$
126	125	oveq2i	$⊢ x + T = x + 1 T$
127	126	oveq1i	$⊢ (x + T) \mod T = (x + 1 T) \mod T$
128	119 127	eqtrdi	$⊢ y = x + T \to y \mod T = (x + 1 T) \mod T$
129	128	adantl	$⊢ (x \in ℝ \land y = x + T) \to y \mod T = (x + 1 T) \mod T$
130		simpl	$⊢ (x \in ℝ \land y = x + T) \to x \in ℝ$
131		2pos	$⊢ 0 < 2$
132	32 120 131 72	mulgt0ii	$⊢ 0 < 2 π$
133	1	eqcomi	$⊢ 2 π = T$
134	132 133	breqtri	$⊢ 0 < T$
135	122 134	elrpii	$⊢ T \in ℝ^{+}$
136	135	a1i	$⊢ (x \in ℝ \land y = x + T) \to T \in ℝ^{+}$
137		1zzd	$⊢ (x \in ℝ \land y = x + T) \to 1 \in ℤ$
138		modcyc	$⊢ (x \in ℝ \land T \in ℝ^{+} \land 1 \in ℤ) \to (x + 1 T) \mod T = x \mod T$
139	130 136 137 138	syl3anc	$⊢ (x \in ℝ \land y = x + T) \to (x + 1 T) \mod T = x \mod T$
140	129 139	eqtrd	$⊢ (x \in ℝ \land y = x + T) \to y \mod T = x \mod T$
141	140	breq1d	$⊢ (x \in ℝ \land y = x + T) \to (y \mod T < π \leftrightarrow x \mod T < π)$
142	141	ifbid	$⊢ (x \in ℝ \land y = x + T) \to if (y \mod T < π, 1, - 1) = if (x \mod T < π, 1, - 1)$
143		id	$⊢ x \in ℝ \to x \in ℝ$
144	122	a1i	$⊢ x \in ℝ \to T \in ℝ$
145	143 144	readdcld	$⊢ x \in ℝ \to x + T \in ℝ$
146	118 142 145 111	fvmptd	$⊢ x \in ℝ \to F (x + T) = if (x \mod T < π, 1, - 1)$
147	2	fvmpt2	$⊢ (x \in ℝ \land if (x \mod T < π, 1, - 1) \in ℝ) \to F (x) = if (x \mod T < π, 1, - 1)$
148	110 147	mpan2	$⊢ x \in ℝ \to F (x) = if (x \mod T < π, 1, - 1)$
149	146 148	eqtr4d	$⊢ x \in ℝ \to F (x + T) = F (x)$
150		eqid	$⊢ {F_{ℝ}^{'} ↾}_{(- π, π)} = {F_{ℝ}^{'} ↾}_{(- π, π)}$
151		snfi	$⊢ \{0\} \in Fin$
152		eldifi	$⊢ x \in ((- π, π) ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \to x \in (- π, π)$
153		0xr	$⊢ 0 \in ℝ^{*}$
154	153	a1i	$⊢ (x \in (- π, π) \land 0 < x) \to 0 \in ℝ^{*}$
155	120	rexri	$⊢ π \in ℝ^{*}$
156	155	a1i	$⊢ (x \in (- π, π) \land 0 < x) \to π \in ℝ^{*}$
157		elioore	$⊢ x \in (- π, π) \to x \in ℝ$
158	157	adantr	$⊢ (x \in (- π, π) \land 0 < x) \to x \in ℝ$
159		simpr	$⊢ (x \in (- π, π) \land 0 < x) \to 0 < x$
160	120	renegcli	$⊢ - π \in ℝ$
161	160	rexri	$⊢ - π \in ℝ^{*}$
162		iooltub	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land x \in (- π, π)) \to x < π$
163	161 155 162	mp3an12	$⊢ x \in (- π, π) \to x < π$
164	163	adantr	$⊢ (x \in (- π, π) \land 0 < x) \to x < π$
165	154 156 158 159 164	eliood	$⊢ (x \in (- π, π) \land 0 < x) \to x \in (0, π)$
166		negpilt0	$⊢ - π < 0$
167	160 71 166	ltleii	$⊢ - π \leq 0$
168		iooss1	$⊢ (- π \in ℝ^{*} \land - π \leq 0) \to (0, π) \subseteq (- π, π)$
169	161 167 168	mp2an	$⊢ (0, π) \subseteq (- π, π)$
170	169	sseli	$⊢ x \in (0, π) \to x \in (- π, π)$
171	2	reseq1i	$⊢ {F ↾}_{(0, π)} = {(x \in ℝ ⟼ if (x \mod T < π, 1, - 1)) ↾}_{(0, π)}$
172		ioossre	$⊢ (0, π) \subseteq ℝ$
173		resmpt	$⊢ (0, π) \subseteq ℝ \to {(x \in ℝ ⟼ if (x \mod T < π, 1, - 1)) ↾}_{(0, π)} = (x \in (0, π) ⟼ if (x \mod T < π, 1, - 1))$
174	172 173	ax-mp	$⊢ {(x \in ℝ ⟼ if (x \mod T < π, 1, - 1)) ↾}_{(0, π)} = (x \in (0, π) ⟼ if (x \mod T < π, 1, - 1))$
175		elioore	$⊢ x \in (0, π) \to x \in ℝ$
176	135	a1i	$⊢ x \in (0, π) \to T \in ℝ^{+}$
177		0red	$⊢ x \in (0, π) \to 0 \in ℝ$
178		ioogtlb	$⊢ (0 \in ℝ^{} \land π \in ℝ^{} \land x \in (0, π)) \to 0 < x$
179	153 155 178	mp3an12	$⊢ x \in (0, π) \to 0 < x$
180	177 175 179	ltled	$⊢ x \in (0, π) \to 0 \leq x$
181	120	a1i	$⊢ x \in (0, π) \to π \in ℝ$
182	122	a1i	$⊢ x \in (0, π) \to T \in ℝ$
183	170 163	syl	$⊢ x \in (0, π) \to x < π$
184		pirp	$⊢ π \in ℝ^{+}$
185		2timesgt	$⊢ π \in ℝ^{+} \to π < 2 π$
186	184 185	ax-mp	$⊢ π < 2 π$
187	186 133	breqtri	$⊢ π < T$
188	187	a1i	$⊢ x \in (0, π) \to π < T$
189	175 181 182 183 188	lttrd	$⊢ x \in (0, π) \to x < T$
190		modid	$⊢ ((x \in ℝ \land T \in ℝ^{+}) \land (0 \leq x \land x < T)) \to x \mod T = x$
191	175 176 180 189 190	syl22anc	$⊢ x \in (0, π) \to x \mod T = x$
192	191 183	eqbrtrd	$⊢ x \in (0, π) \to x \mod T < π$
193	192	iftrued	$⊢ x \in (0, π) \to if (x \mod T < π, 1, - 1) = 1$
194	193	mpteq2ia	$⊢ (x \in (0, π) ⟼ if (x \mod T < π, 1, - 1)) = (x \in (0, π) ⟼ 1)$
195	171 174 194	3eqtrri	$⊢ (x \in (0, π) ⟼ 1) = {F ↾}_{(0, π)}$
196	195	oveq2i	$⊢ \frac{d (x \in (0, π)⟼ 1)}{d_{ℝ} x} = ℝ D ({F ↾}_{(0, π)})$
197		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
198	197	a1i	$⊢ ⊤ \to ℝ \in \{ℝ, ℂ\}$
199		iooretop	$⊢ (0, π) \in topGen (ran (.))$
200		tgioo4	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
201	199 200	eleqtri	$⊢ (0, π) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
202	201	a1i	$⊢ ⊤ \to (0, π) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
203		1cnd	$⊢ ⊤ \to 1 \in ℂ$
204	198 202 203	dvmptconst	$⊢ ⊤ \to \frac{d (x \in (0, π)⟼ 1)}{d_{ℝ} x} = (x \in (0, π) ⟼ 0)$
205	204	mptru	$⊢ \frac{d (x \in (0, π)⟼ 1)}{d_{ℝ} x} = (x \in (0, π) ⟼ 0)$
206		ssid	$⊢ ℝ \subseteq ℝ$
207		ax-resscn	$⊢ ℝ \subseteq ℂ$
208		fss	$⊢ (F : ℝ ⟶ ℝ \land ℝ \subseteq ℂ) \to F : ℝ ⟶ ℂ$
209	112 207 208	mp2an	$⊢ F : ℝ ⟶ ℂ$
210		dvresioo	$⊢ (ℝ \subseteq ℝ \land F : ℝ ⟶ ℂ) \to ℝ D ({F ↾}_{(0, π)}) = {F_{ℝ}^{'} ↾}_{(0, π)}$
211	206 209 210	mp2an	$⊢ ℝ D ({F ↾}_{(0, π)}) = {F_{ℝ}^{'} ↾}_{(0, π)}$
212	196 205 211	3eqtr3i	$⊢ (x \in (0, π) ⟼ 0) = {F_{ℝ}^{'} ↾}_{(0, π)}$
213	212	dmeqi	$⊢ dom (x \in (0, π) ⟼ 0) = dom ({F_{ℝ}^{'} ↾}_{(0, π)})$
214		eqid	$⊢ (x \in (0, π) ⟼ 0) = (x \in (0, π) ⟼ 0)$
215	93 214	dmmpti	$⊢ dom (x \in (0, π) ⟼ 0) = (0, π)$
216	213 215	eqtr3i	$⊢ dom ({F_{ℝ}^{'} ↾}_{(0, π)}) = (0, π)$
217		ssdmres	$⊢ (0, π) \subseteq dom F_{ℝ}^{'} \leftrightarrow dom ({F_{ℝ}^{'} ↾}_{(0, π)}) = (0, π)$
218	216 217	mpbir	$⊢ (0, π) \subseteq dom F_{ℝ}^{'}$
219	218	sseli	$⊢ x \in (0, π) \to x \in dom F_{ℝ}^{'}$
220	170 219	elind	$⊢ x \in (0, π) \to x \in ((- π, π) \cap dom F_{ℝ}^{'})$
221		dmres	$⊢ dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) = (- π, π) \cap dom F_{ℝ}^{'}$
222	220 221	eleqtrrdi	$⊢ x \in (0, π) \to x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
223	165 222	syl	$⊢ (x \in (- π, π) \land 0 < x) \to x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
224	223	adantlr	$⊢ ((x \in (- π, π) \land \neg x = 0) \land 0 < x) \to x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
225	161	a1i	$⊢ ((x \in (- π, π) \land \neg x = 0) \land \neg 0 < x) \to - π \in ℝ^{*}$
226	153	a1i	$⊢ ((x \in (- π, π) \land \neg x = 0) \land \neg 0 < x) \to 0 \in ℝ^{*}$
227	157	ad2antrr	$⊢ ((x \in (- π, π) \land \neg x = 0) \land \neg 0 < x) \to x \in ℝ$
228		ioogtlb	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land x \in (- π, π)) \to - π < x$
229	161 155 228	mp3an12	$⊢ x \in (- π, π) \to - π < x$
230	229	ad2antrr	$⊢ ((x \in (- π, π) \land \neg x = 0) \land \neg 0 < x) \to - π < x$
231		0red	$⊢ ((x \in (- π, π) \land \neg x = 0) \land \neg 0 < x) \to 0 \in ℝ$
232		neqne	$⊢ \neg x = 0 \to x \neq 0$
233	232	ad2antlr	$⊢ ((x \in (- π, π) \land \neg x = 0) \land \neg 0 < x) \to x \neq 0$
234		simpr	$⊢ ((x \in (- π, π) \land \neg x = 0) \land \neg 0 < x) \to \neg 0 < x$
235	227 231 233 234	lttri5d	$⊢ ((x \in (- π, π) \land \neg x = 0) \land \neg 0 < x) \to x < 0$
236	225 226 227 230 235	eliood	$⊢ ((x \in (- π, π) \land \neg x = 0) \land \neg 0 < x) \to x \in (- π, 0)$
237	71 120 72	ltleii	$⊢ 0 \leq π$
238		iooss2	$⊢ (π \in ℝ^{*} \land 0 \leq π) \to (- π, 0) \subseteq (- π, π)$
239	155 237 238	mp2an	$⊢ (- π, 0) \subseteq (- π, π)$
240	239	sseli	$⊢ x \in (- π, 0) \to x \in (- π, π)$
241	2	reseq1i	$⊢ {F ↾}_{(- π, 0)} = {(x \in ℝ ⟼ if (x \mod T < π, 1, - 1)) ↾}_{(- π, 0)}$
242		ioossre	$⊢ (- π, 0) \subseteq ℝ$
243		resmpt	$⊢ (- π, 0) \subseteq ℝ \to {(x \in ℝ ⟼ if (x \mod T < π, 1, - 1)) ↾}_{(- π, 0)} = (x \in (- π, 0) ⟼ if (x \mod T < π, 1, - 1))$
244	242 243	ax-mp	$⊢ {(x \in ℝ ⟼ if (x \mod T < π, 1, - 1)) ↾}_{(- π, 0)} = (x \in (- π, 0) ⟼ if (x \mod T < π, 1, - 1))$
245	120	a1i	$⊢ x \in (- π, 0) \to π \in ℝ$
246		elioore	$⊢ x \in (- π, 0) \to x \in ℝ$
247	135	a1i	$⊢ x \in (- π, 0) \to T \in ℝ^{+}$
248	246 247	modcld	$⊢ x \in (- π, 0) \to x \mod T \in ℝ$
249	246 145	syl	$⊢ x \in (- π, 0) \to x + T \in ℝ$
250	56	2timesi	$⊢ 2 π = π + π$
251	1 250	eqtri	$⊢ T = π + π$
252	251	oveq2i	$⊢ - π + T = (- π) + π + π$
253		negpicn	$⊢ - π \in ℂ$
254	253 56 56	addassi	$⊢ (- π) + π + π = (- π) + π + π$
255	254	eqcomi	$⊢ (- π) + π + π = (- π) + π + π$
256	56	negidi	$⊢ π + (- π) = 0$
257	56 253 256	addcomli	$⊢ - π + π = 0$
258	257	oveq1i	$⊢ (- π) + π + π = 0 + π$
259	56	addlidi	$⊢ 0 + π = π$
260	258 259	eqtri	$⊢ (- π) + π + π = π$
261	252 255 260	3eqtrri	$⊢ π = - π + T$
262	261	a1i	$⊢ x \in (- π, 0) \to π = - π + T$
263	160	a1i	$⊢ x \in (- π, 0) \to - π \in ℝ$
264	122	a1i	$⊢ x \in (- π, 0) \to T \in ℝ$
265	240 229	syl	$⊢ x \in (- π, 0) \to - π < x$
266	263 246 264 265	ltadd1dd	$⊢ x \in (- π, 0) \to - π + T < x + T$
267	262 266	eqbrtrd	$⊢ x \in (- π, 0) \to π < x + T$
268	245 249 267	ltled	$⊢ x \in (- π, 0) \to π \leq x + T$
269		0red	$⊢ x \in (- π, 0) \to 0 \in ℝ$
270	160 122	readdcli	$⊢ - π + T \in ℝ$
271	270	a1i	$⊢ x \in (- π, 0) \to - π + T \in ℝ$
272	72	a1i	$⊢ x \in (- π, 0) \to 0 < π$
273	272 261	breqtrdi	$⊢ x \in (- π, 0) \to 0 < - π + T$
274	269 271 249 273 266	lttrd	$⊢ x \in (- π, 0) \to 0 < x + T$
275	269 249 274	ltled	$⊢ x \in (- π, 0) \to 0 \leq x + T$
276	246	recnd	$⊢ x \in (- π, 0) \to x \in ℂ$
277	123	a1i	$⊢ x \in (- π, 0) \to T \in ℂ$
278	276 277	addcomd	$⊢ x \in (- π, 0) \to x + T = T + x$
279		iooltub	$⊢ (- π \in ℝ^{} \land 0 \in ℝ^{} \land x \in (- π, 0)) \to x < 0$
280	161 153 279	mp3an12	$⊢ x \in (- π, 0) \to x < 0$
281		ltaddneg	$⊢ (x \in ℝ \land T \in ℝ) \to (x < 0 \leftrightarrow T + x < T)$
282	246 122 281	sylancl	$⊢ x \in (- π, 0) \to (x < 0 \leftrightarrow T + x < T)$
283	280 282	mpbid	$⊢ x \in (- π, 0) \to T + x < T$
284	278 283	eqbrtrd	$⊢ x \in (- π, 0) \to x + T < T$
285	275 284	jca	$⊢ x \in (- π, 0) \to (0 \leq x + T \land x + T < T)$
286		modid2	$⊢ (x + T \in ℝ \land T \in ℝ^{+}) \to ((x + T) \mod T = x + T \leftrightarrow (0 \leq x + T \land x + T < T))$
287	249 135 286	sylancl	$⊢ x \in (- π, 0) \to ((x + T) \mod T = x + T \leftrightarrow (0 \leq x + T \land x + T < T))$
288	285 287	mpbird	$⊢ x \in (- π, 0) \to (x + T) \mod T = x + T$
289	127	a1i	$⊢ x \in ℝ \to (x + T) \mod T = (x + 1 T) \mod T$
290	135	a1i	$⊢ x \in ℝ \to T \in ℝ^{+}$
291		1zzd	$⊢ x \in ℝ \to 1 \in ℤ$
292	143 290 291 138	syl3anc	$⊢ x \in ℝ \to (x + 1 T) \mod T = x \mod T$
293	289 292	eqtrd	$⊢ x \in ℝ \to (x + T) \mod T = x \mod T$
294	246 293	syl	$⊢ x \in (- π, 0) \to (x + T) \mod T = x \mod T$
295	288 294	eqtr3d	$⊢ x \in (- π, 0) \to x + T = x \mod T$
296	268 295	breqtrd	$⊢ x \in (- π, 0) \to π \leq x \mod T$
297	245 248 296	lensymd	$⊢ x \in (- π, 0) \to \neg x \mod T < π$
298	297	iffalsed	$⊢ x \in (- π, 0) \to if (x \mod T < π, 1, - 1) = - 1$
299	298	mpteq2ia	$⊢ (x \in (- π, 0) ⟼ if (x \mod T < π, 1, - 1)) = (x \in (- π, 0) ⟼ - 1)$
300	241 244 299	3eqtrri	$⊢ (x \in (- π, 0) ⟼ - 1) = {F ↾}_{(- π, 0)}$
301	300	oveq2i	$⊢ \frac{d (x \in (- π, 0)⟼ - 1)}{d_{ℝ} x} = ℝ D ({F ↾}_{(- π, 0)})$
302		iooretop	$⊢ (- π, 0) \in topGen (ran (.))$
303	302 200	eleqtri	$⊢ (- π, 0) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
304	303	a1i	$⊢ ⊤ \to (- π, 0) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ)$
305	203	negcld	$⊢ ⊤ \to - 1 \in ℂ$
306	198 304 305	dvmptconst	$⊢ ⊤ \to \frac{d (x \in (- π, 0)⟼ - 1)}{d_{ℝ} x} = (x \in (- π, 0) ⟼ 0)$
307	306	mptru	$⊢ \frac{d (x \in (- π, 0)⟼ - 1)}{d_{ℝ} x} = (x \in (- π, 0) ⟼ 0)$
308		dvresioo	$⊢ (ℝ \subseteq ℝ \land F : ℝ ⟶ ℂ) \to ℝ D ({F ↾}_{(- π, 0)}) = {F_{ℝ}^{'} ↾}_{(- π, 0)}$
309	206 209 308	mp2an	$⊢ ℝ D ({F ↾}_{(- π, 0)}) = {F_{ℝ}^{'} ↾}_{(- π, 0)}$
310	301 307 309	3eqtr3i	$⊢ (x \in (- π, 0) ⟼ 0) = {F_{ℝ}^{'} ↾}_{(- π, 0)}$
311	310	dmeqi	$⊢ dom (x \in (- π, 0) ⟼ 0) = dom ({F_{ℝ}^{'} ↾}_{(- π, 0)})$
312		eqid	$⊢ (x \in (- π, 0) ⟼ 0) = (x \in (- π, 0) ⟼ 0)$
313	93 312	dmmpti	$⊢ dom (x \in (- π, 0) ⟼ 0) = (- π, 0)$
314	311 313	eqtr3i	$⊢ dom ({F_{ℝ}^{'} ↾}_{(- π, 0)}) = (- π, 0)$
315		ssdmres	$⊢ (- π, 0) \subseteq dom F_{ℝ}^{'} \leftrightarrow dom ({F_{ℝ}^{'} ↾}_{(- π, 0)}) = (- π, 0)$
316	314 315	mpbir	$⊢ (- π, 0) \subseteq dom F_{ℝ}^{'}$
317	316	sseli	$⊢ x \in (- π, 0) \to x \in dom F_{ℝ}^{'}$
318	240 317	elind	$⊢ x \in (- π, 0) \to x \in ((- π, π) \cap dom F_{ℝ}^{'})$
319	318 221	eleqtrrdi	$⊢ x \in (- π, 0) \to x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
320	236 319	syl	$⊢ ((x \in (- π, π) \land \neg x = 0) \land \neg 0 < x) \to x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
321	224 320	pm2.61dan	$⊢ (x \in (- π, π) \land \neg x = 0) \to x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
322	152 321	sylan	$⊢ (x \in ((- π, π) ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \land \neg x = 0) \to x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
323		eldifn	$⊢ x \in ((- π, π) ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \to \neg x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
324	323	adantr	$⊢ (x \in ((- π, π) ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \land \neg x = 0) \to \neg x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
325	322 324	condan	$⊢ x \in ((- π, π) ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \to x = 0$
326		velsn	$⊢ x \in \{0\} \leftrightarrow x = 0$
327	325 326	sylibr	$⊢ x \in ((- π, π) ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \to x \in \{0\}$
328	327	ssriv	$⊢ (- π, π) ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \subseteq \{0\}$
329		ssfi	$⊢ (\{0\} \in Fin \land (- π, π) ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \subseteq \{0\}) \to (- π, π) ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \in Fin$
330	151 328 329	mp2an	$⊢ (- π, π) ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \in Fin$
331		inss1	$⊢ (- π, π) \cap dom F_{ℝ}^{'} \subseteq (- π, π)$
332	221 331	eqsstri	$⊢ dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \subseteq (- π, π)$
333		ioosscn	$⊢ (- π, π) \subseteq ℂ$
334	332 333	sstri	$⊢ dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \subseteq ℂ$
335	334	a1i	$⊢ ⊤ \to dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \subseteq ℂ$
336		dvf	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ$
337		fresin	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ \to ({F_{ℝ}^{'} ↾}_{(- π, π)}) : dom F_{ℝ}^{'} \cap (- π, π) ⟶ ℂ$
338		ffdm	$⊢ ({F_{ℝ}^{'} ↾}_{(- π, π)}) : dom F_{ℝ}^{'} \cap (- π, π) ⟶ ℂ \to (({F_{ℝ}^{'} ↾}_{(- π, π)}) : dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) ⟶ ℂ \land dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \subseteq dom F_{ℝ}^{'} \cap (- π, π))$
339	336 337 338	mp2b	$⊢ (({F_{ℝ}^{'} ↾}_{(- π, π)}) : dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) ⟶ ℂ \land dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \subseteq dom F_{ℝ}^{'} \cap (- π, π))$
340	339	simpli	$⊢ ({F_{ℝ}^{'} ↾}_{(- π, π)}) : dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) ⟶ ℂ$
341	340	a1i	$⊢ ⊤ \to ({F_{ℝ}^{'} ↾}_{(- π, π)}) : dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) ⟶ ℂ$
342	161	a1i	$⊢ (x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \land x < 0) \to - π \in ℝ^{*}$
343	153	a1i	$⊢ (x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \land x < 0) \to 0 \in ℝ^{*}$
344		ioossre	$⊢ (- π, π) \subseteq ℝ$
345	332	sseli	$⊢ x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \to x \in (- π, π)$
346	344 345	sselid	$⊢ x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \to x \in ℝ$
347	346	adantr	$⊢ (x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \land x < 0) \to x \in ℝ$
348	345 229	syl	$⊢ x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \to - π < x$
349	348	adantr	$⊢ (x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \land x < 0) \to - π < x$
350		simpr	$⊢ (x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \land x < 0) \to x < 0$
351	342 343 347 349 350	eliood	$⊢ (x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \land x < 0) \to x \in (- π, 0)$
352		elun1	$⊢ x \in (- π, 0) \to x \in ((- π, 0) \cup (0, π))$
353	351 352	syl	$⊢ (x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \land x < 0) \to x \in ((- π, 0) \cup (0, π))$
354		simpl	$⊢ (x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \land \neg x < 0) \to x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
355		0red	$⊢ (x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \land \neg x < 0) \to 0 \in ℝ$
356	346	adantr	$⊢ (x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \land \neg x < 0) \to x \in ℝ$
357		simpr	$⊢ (x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \land \neg x < 0) \to \neg x < 0$
358	355 356 357	nltled	$⊢ (x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \land \neg x < 0) \to 0 \leq x$
359		id	$⊢ x = 0 \to x = 0$
360		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
361	206	a1i	$⊢ ⊤ \to ℝ \subseteq ℝ$
362		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
363	209	a1i	$⊢ ⊤ \to F : ℝ ⟶ ℂ$
364		0red	$⊢ ⊤ \to 0 \in ℝ$
365		mnfxr	$⊢ −∞ \in ℝ^{*}$
366	365	a1i	$⊢ ⊤ \to −∞ \in ℝ^{*}$
367	364	mnfltd	$⊢ ⊤ \to −∞ < 0$
368	362 366 364 367	lptioo2	$⊢ ⊤ \to 0 \in limPt (topGen (ran (.))) ((−∞, 0))$
369		incom	$⊢ ℝ \cap (−∞, 0) = (−∞, 0) \cap ℝ$
370		ioossre	$⊢ (−∞, 0) \subseteq ℝ$
371		dfss2	$⊢ (−∞, 0) \subseteq ℝ \leftrightarrow (−∞, 0) \cap ℝ = (−∞, 0)$
372	370 371	mpbi	$⊢ (−∞, 0) \cap ℝ = (−∞, 0)$
373	369 372	eqtr2i	$⊢ (−∞, 0) = ℝ \cap (−∞, 0)$
374	373	fveq2i	$⊢ limPt (topGen (ran (.))) ((−∞, 0)) = limPt (topGen (ran (.))) (ℝ \cap (−∞, 0))$
375	368 374	eleqtrdi	$⊢ ⊤ \to 0 \in limPt (topGen (ran (.))) (ℝ \cap (−∞, 0))$
376		pnfxr	$⊢ +∞ \in ℝ^{*}$
377	376	a1i	$⊢ ⊤ \to +∞ \in ℝ^{*}$
378	364	ltpnfd	$⊢ ⊤ \to 0 < +∞$
379	362 364 377 378	lptioo1	$⊢ ⊤ \to 0 \in limPt (topGen (ran (.))) ((0, +∞))$
380		incom	$⊢ ℝ \cap (0, +∞) = (0, +∞) \cap ℝ$
381		ioossre	$⊢ (0, +∞) \subseteq ℝ$
382		dfss2	$⊢ (0, +∞) \subseteq ℝ \leftrightarrow (0, +∞) \cap ℝ = (0, +∞)$
383	381 382	mpbi	$⊢ (0, +∞) \cap ℝ = (0, +∞)$
384	380 383	eqtr2i	$⊢ (0, +∞) = ℝ \cap (0, +∞)$
385	384	fveq2i	$⊢ limPt (topGen (ran (.))) ((0, +∞)) = limPt (topGen (ran (.))) (ℝ \cap (0, +∞))$
386	379 385	eleqtrdi	$⊢ ⊤ \to 0 \in limPt (topGen (ran (.))) (ℝ \cap (0, +∞))$
387		eqid	$⊢ (x \in (- π, 0) ⟼ - 1) = (x \in (- π, 0) ⟼ - 1)$
388		mnfle	$⊢ - π \in ℝ^{*} \to −∞ \leq - π$
389	161 388	ax-mp	$⊢ −∞ \leq - π$
390		iooss1	$⊢ (−∞ \in ℝ^{*} \land −∞ \leq - π) \to (- π, 0) \subseteq (−∞, 0)$
391	365 389 390	mp2an	$⊢ (- π, 0) \subseteq (−∞, 0)$
392	391	a1i	$⊢ ⊤ \to (- π, 0) \subseteq (−∞, 0)$
393		ioosscn	$⊢ (−∞, 0) \subseteq ℂ$
394	392 393	sstrdi	$⊢ ⊤ \to (- π, 0) \subseteq ℂ$
395		0cnd	$⊢ ⊤ \to 0 \in ℂ$
396	387 394 305 395	constlimc	$⊢ ⊤ \to - 1 \in ((x \in (- π, 0) ⟼ - 1) {lim}_{ℂ} 0)$
397		resabs1	$⊢ (- π, 0) \subseteq (−∞, 0) \to {({F ↾}_{(−∞, 0)}) ↾}_{(- π, 0)} = {F ↾}_{(- π, 0)}$
398	391 397	ax-mp	$⊢ {({F ↾}_{(−∞, 0)}) ↾}_{(- π, 0)} = {F ↾}_{(- π, 0)}$
399	300 398	eqtr4i	$⊢ (x \in (- π, 0) ⟼ - 1) = {({F ↾}_{(−∞, 0)}) ↾}_{(- π, 0)}$
400	399	oveq1i	$⊢ (x \in (- π, 0) ⟼ - 1) {lim}_{ℂ} 0 = ({({F ↾}_{(−∞, 0)}) ↾}_{(- π, 0)}) {lim}_{ℂ} 0$
401		fssres	$⊢ (F : ℝ ⟶ ℂ \land (−∞, 0) \subseteq ℝ) \to ({F ↾}_{(−∞, 0)}) : (−∞, 0) ⟶ ℂ$
402	209 370 401	mp2an	$⊢ ({F ↾}_{(−∞, 0)}) : (−∞, 0) ⟶ ℂ$
403	402	a1i	$⊢ ⊤ \to ({F ↾}_{(−∞, 0)}) : (−∞, 0) ⟶ ℂ$
404	393	a1i	$⊢ ⊤ \to (−∞, 0) \subseteq ℂ$
405		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ((−∞, 0) \cup \{0\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((−∞, 0) \cup \{0\})$
406		0le0	$⊢ 0 \leq 0$
407		elioc2	$⊢ (- π \in ℝ^{*} \land 0 \in ℝ) \to (0 \in (- π, 0] \leftrightarrow (0 \in ℝ \land - π < 0 \land 0 \leq 0))$
408	161 71 407	mp2an	$⊢ 0 \in (- π, 0] \leftrightarrow (0 \in ℝ \land - π < 0 \land 0 \leq 0)$
409	71 166 406 408	mpbir3an	$⊢ 0 \in (- π, 0]$
410	360	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
411		ovex	$⊢ (−∞, 0] \in V$
412		resttop	$⊢ (TopOpen (ℂ_{fld}) \in Top \land (−∞, 0] \in V) \to TopOpen (ℂ_{fld}) ↾_{𝑡} (−∞, 0] \in Top$
413	410 411 412	mp2an	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (−∞, 0] \in Top$
414	161	a1i	$⊢ ⊤ \to - π \in ℝ^{*}$
415		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} (−∞, 0] = topGen (ran (.)) ↾_{𝑡} (−∞, 0]$
416	389	a1i	$⊢ ⊤ \to −∞ \leq - π$
417	366 414 364 362 415 416 364	iocopn	$⊢ ⊤ \to (- π, 0] \in (topGen (ran (.)) ↾_{𝑡} (−∞, 0])$
418	417	mptru	$⊢ (- π, 0] \in (topGen (ran (.)) ↾_{𝑡} (−∞, 0])$
419	200	oveq1i	$⊢ topGen (ran (.)) ↾_{𝑡} (−∞, 0] = (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} (−∞, 0]$
420		iocssre	$⊢ (−∞ \in ℝ^{*} \land 0 \in ℝ) \to (−∞, 0] \subseteq ℝ$
421	365 71 420	mp2an	$⊢ (−∞, 0] \subseteq ℝ$
422	197	elexi	$⊢ ℝ \in V$
423		restabs	$⊢ (TopOpen (ℂ_{fld}) \in Top \land (−∞, 0] \subseteq ℝ \land ℝ \in V) \to (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} (−∞, 0] = TopOpen (ℂ_{fld}) ↾_{𝑡} (−∞, 0]$
424	410 421 422 423	mp3an	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} (−∞, 0] = TopOpen (ℂ_{fld}) ↾_{𝑡} (−∞, 0]$
425	419 424	eqtri	$⊢ topGen (ran (.)) ↾_{𝑡} (−∞, 0] = TopOpen (ℂ_{fld}) ↾_{𝑡} (−∞, 0]$
426	418 425	eleqtri	$⊢ (- π, 0] \in (TopOpen (ℂ_{fld}) ↾_{𝑡} (−∞, 0])$
427		isopn3i	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} (−∞, 0] \in Top \land (- π, 0] \in (TopOpen (ℂ_{fld}) ↾_{𝑡} (−∞, 0])) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} (−∞, 0]) ((- π, 0]) = (- π, 0]$
428	413 426 427	mp2an	$⊢ int (TopOpen (ℂ_{fld}) ↾_{𝑡} (−∞, 0]) ((- π, 0]) = (- π, 0]$
429		mnflt0	$⊢ −∞ < 0$
430		ioounsn	$⊢ (−∞ \in ℝ^{} \land 0 \in ℝ^{} \land −∞ < 0) \to (−∞, 0) \cup \{0\} = (−∞, 0]$
431	365 153 429 430	mp3an	$⊢ (−∞, 0) \cup \{0\} = (−∞, 0]$
432	431	eqcomi	$⊢ (−∞, 0] = (−∞, 0) \cup \{0\}$
433	432	oveq2i	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (−∞, 0] = TopOpen (ℂ_{fld}) ↾_{𝑡} ((−∞, 0) \cup \{0\})$
434	433	fveq2i	$⊢ int (TopOpen (ℂ_{fld}) ↾_{𝑡} (−∞, 0]) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((−∞, 0) \cup \{0\}))$
435		ioounsn	$⊢ (- π \in ℝ^{} \land 0 \in ℝ^{} \land - π < 0) \to (- π, 0) \cup \{0\} = (- π, 0]$
436	161 153 166 435	mp3an	$⊢ (- π, 0) \cup \{0\} = (- π, 0]$
437	436	eqcomi	$⊢ (- π, 0] = (- π, 0) \cup \{0\}$
438	434 437	fveq12i	$⊢ int (TopOpen (ℂ_{fld}) ↾_{𝑡} (−∞, 0]) ((- π, 0]) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((−∞, 0) \cup \{0\})) ((- π, 0) \cup \{0\})$
439	428 438	eqtr3i	$⊢ (- π, 0] = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((−∞, 0) \cup \{0\})) ((- π, 0) \cup \{0\})$
440	409 439	eleqtri	$⊢ 0 \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((−∞, 0) \cup \{0\})) ((- π, 0) \cup \{0\})$
441	440	a1i	$⊢ ⊤ \to 0 \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((−∞, 0) \cup \{0\})) ((- π, 0) \cup \{0\})$
442	403 392 404 360 405 441	limcres	$⊢ ⊤ \to ({({F ↾}_{(−∞, 0)}) ↾}_{(- π, 0)}) {lim}_{ℂ} 0 = ({F ↾}_{(−∞, 0)}) {lim}_{ℂ} 0$
443	442	mptru	$⊢ ({({F ↾}_{(−∞, 0)}) ↾}_{(- π, 0)}) {lim}_{ℂ} 0 = ({F ↾}_{(−∞, 0)}) {lim}_{ℂ} 0$
444	400 443	eqtri	$⊢ (x \in (- π, 0) ⟼ - 1) {lim}_{ℂ} 0 = ({F ↾}_{(−∞, 0)}) {lim}_{ℂ} 0$
445	396 444	eleqtrdi	$⊢ ⊤ \to - 1 \in (({F ↾}_{(−∞, 0)}) {lim}_{ℂ} 0)$
446		eqid	$⊢ (x \in (0, π) ⟼ 1) = (x \in (0, π) ⟼ 1)$
447		ioosscn	$⊢ (0, π) \subseteq ℂ$
448	447	a1i	$⊢ ⊤ \to (0, π) \subseteq ℂ$
449	446 448 203 395	constlimc	$⊢ ⊤ \to 1 \in ((x \in (0, π) ⟼ 1) {lim}_{ℂ} 0)$
450		ltpnf	$⊢ π \in ℝ \to π < +∞$
451		xrltle	$⊢ (π \in ℝ^{} \land +∞ \in ℝ^{}) \to (π < +∞ \to π \leq +∞)$
452	155 376 451	mp2an	$⊢ π < +∞ \to π \leq +∞$
453	120 450 452	mp2b	$⊢ π \leq +∞$
454		iooss2	$⊢ (+∞ \in ℝ^{*} \land π \leq +∞) \to (0, π) \subseteq (0, +∞)$
455	376 453 454	mp2an	$⊢ (0, π) \subseteq (0, +∞)$
456		resabs1	$⊢ (0, π) \subseteq (0, +∞) \to {({F ↾}_{(0, +∞)}) ↾}_{(0, π)} = {F ↾}_{(0, π)}$
457	455 456	ax-mp	$⊢ {({F ↾}_{(0, +∞)}) ↾}_{(0, π)} = {F ↾}_{(0, π)}$
458	195 457	eqtr4i	$⊢ (x \in (0, π) ⟼ 1) = {({F ↾}_{(0, +∞)}) ↾}_{(0, π)}$
459	458	oveq1i	$⊢ (x \in (0, π) ⟼ 1) {lim}_{ℂ} 0 = ({({F ↾}_{(0, +∞)}) ↾}_{(0, π)}) {lim}_{ℂ} 0$
460		fssres	$⊢ (F : ℝ ⟶ ℂ \land (0, +∞) \subseteq ℝ) \to ({F ↾}_{(0, +∞)}) : (0, +∞) ⟶ ℂ$
461	209 381 460	mp2an	$⊢ ({F ↾}_{(0, +∞)}) : (0, +∞) ⟶ ℂ$
462	461	a1i	$⊢ ⊤ \to ({F ↾}_{(0, +∞)}) : (0, +∞) ⟶ ℂ$
463	455	a1i	$⊢ ⊤ \to (0, π) \subseteq (0, +∞)$
464		ioosscn	$⊢ (0, +∞) \subseteq ℂ$
465	464	a1i	$⊢ ⊤ \to (0, +∞) \subseteq ℂ$
466		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ((0, +∞) \cup \{0\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((0, +∞) \cup \{0\})$
467		elico2	$⊢ (0 \in ℝ \land π \in ℝ^{*}) \to (0 \in [0, π) \leftrightarrow (0 \in ℝ \land 0 \leq 0 \land 0 < π))$
468	71 155 467	mp2an	$⊢ 0 \in [0, π) \leftrightarrow (0 \in ℝ \land 0 \leq 0 \land 0 < π)$
469	71 406 72 468	mpbir3an	$⊢ 0 \in [0, π)$
470		ovex	$⊢ [0, +∞) \in V$
471		resttop	$⊢ (TopOpen (ℂ_{fld}) \in Top \land [0, +∞) \in V) \to TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞) \in Top$
472	410 470 471	mp2an	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞) \in Top$
473	155	a1i	$⊢ ⊤ \to π \in ℝ^{*}$
474		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [0, +∞) = topGen (ran (.)) ↾_{𝑡} [0, +∞)$
475	453	a1i	$⊢ ⊤ \to π \leq +∞$
476	364 473 377 362 474 475	icoopn	$⊢ ⊤ \to [0, π) \in (topGen (ran (.)) ↾_{𝑡} [0, +∞))$
477	476	mptru	$⊢ [0, π) \in (topGen (ran (.)) ↾_{𝑡} [0, +∞))$
478	200	oveq1i	$⊢ topGen (ran (.)) ↾_{𝑡} [0, +∞) = (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} [0, +∞)$
479		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
480		restabs	$⊢ (TopOpen (ℂ_{fld}) \in Top \land [0, +∞) \subseteq ℝ \land ℝ \in V) \to (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} [0, +∞) = TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞)$
481	410 479 422 480	mp3an	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} [0, +∞) = TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞)$
482	478 481	eqtri	$⊢ topGen (ran (.)) ↾_{𝑡} [0, +∞) = TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞)$
483	477 482	eleqtri	$⊢ [0, π) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞))$
484		isopn3i	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞) \in Top \land [0, π) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞))) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞)) ([0, π)) = [0, π)$
485	472 483 484	mp2an	$⊢ int (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞)) ([0, π)) = [0, π)$
486		0ltpnf	$⊢ 0 < +∞$
487		snunioo1	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land 0 < +∞) \to (0, +∞) \cup \{0\} = [0, +∞)$
488	153 376 486 487	mp3an	$⊢ (0, +∞) \cup \{0\} = [0, +∞)$
489	488	eqcomi	$⊢ [0, +∞) = (0, +∞) \cup \{0\}$
490	489	oveq2i	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((0, +∞) \cup \{0\})$
491	490	fveq2i	$⊢ int (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞)) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((0, +∞) \cup \{0\}))$
492		snunioo1	$⊢ (0 \in ℝ^{} \land π \in ℝ^{} \land 0 < π) \to (0, π) \cup \{0\} = [0, π)$
493	153 155 72 492	mp3an	$⊢ (0, π) \cup \{0\} = [0, π)$
494	493	eqcomi	$⊢ [0, π) = (0, π) \cup \{0\}$
495	491 494	fveq12i	$⊢ int (TopOpen (ℂ_{fld}) ↾_{𝑡} [0, +∞)) ([0, π)) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((0, +∞) \cup \{0\})) ((0, π) \cup \{0\})$
496	485 495	eqtr3i	$⊢ [0, π) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((0, +∞) \cup \{0\})) ((0, π) \cup \{0\})$
497	469 496	eleqtri	$⊢ 0 \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((0, +∞) \cup \{0\})) ((0, π) \cup \{0\})$
498	497	a1i	$⊢ ⊤ \to 0 \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} ((0, +∞) \cup \{0\})) ((0, π) \cup \{0\})$
499	462 463 465 360 466 498	limcres	$⊢ ⊤ \to ({({F ↾}_{(0, +∞)}) ↾}_{(0, π)}) {lim}_{ℂ} 0 = ({F ↾}_{(0, +∞)}) {lim}_{ℂ} 0$
500	499	mptru	$⊢ ({({F ↾}_{(0, +∞)}) ↾}_{(0, π)}) {lim}_{ℂ} 0 = ({F ↾}_{(0, +∞)}) {lim}_{ℂ} 0$
501	459 500	eqtri	$⊢ (x \in (0, π) ⟼ 1) {lim}_{ℂ} 0 = ({F ↾}_{(0, +∞)}) {lim}_{ℂ} 0$
502	449 501	eleqtrdi	$⊢ ⊤ \to 1 \in (({F ↾}_{(0, +∞)}) {lim}_{ℂ} 0)$
503		neg1lt0	$⊢ - 1 < 0$
504	109 71 108	lttri	$⊢ (- 1 < 0 \land 0 < 1) \to - 1 < 1$
505	503 38 504	mp2an	$⊢ - 1 < 1$
506	109 505	ltneii	$⊢ - 1 \neq 1$
507	506	a1i	$⊢ ⊤ \to - 1 \neq 1$
508	360 361 362 363 364 375 386 445 502 507	jumpncnp	$⊢ ⊤ \to \neg F \in (topGen (ran (.)) CnP TopOpen (ℂ_{fld})) (0)$
509	508	mptru	$⊢ \neg F \in (topGen (ran (.)) CnP TopOpen (ℂ_{fld})) (0)$
510	207	a1i	$⊢ 0 \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \to ℝ \subseteq ℂ$
511	209	a1i	$⊢ 0 \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \to F : ℝ ⟶ ℂ$
512	206	a1i	$⊢ 0 \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \to ℝ \subseteq ℝ$
513		inss2	$⊢ (- π, π) \cap dom F_{ℝ}^{'} \subseteq dom F_{ℝ}^{'}$
514	221 513	eqsstri	$⊢ dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \subseteq dom F_{ℝ}^{'}$
515	514	sseli	$⊢ 0 \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \to 0 \in dom F_{ℝ}^{'}$
516	200 360	dvcnp2	$⊢ ((ℝ \subseteq ℂ \land F : ℝ ⟶ ℂ \land ℝ \subseteq ℝ) \land 0 \in dom F_{ℝ}^{'}) \to F \in (topGen (ran (.)) CnP TopOpen (ℂ_{fld})) (0)$
517	510 511 512 515 516	syl31anc	$⊢ 0 \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \to F \in (topGen (ran (.)) CnP TopOpen (ℂ_{fld})) (0)$
518	509 517	mto	$⊢ \neg 0 \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
519	518	a1i	$⊢ x = 0 \to \neg 0 \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
520	359 519	eqneltrd	$⊢ x = 0 \to \neg x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
521	520	necon2ai	$⊢ x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \to x \neq 0$
522	521	adantr	$⊢ (x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \land \neg x < 0) \to x \neq 0$
523	355 356 358 522	leneltd	$⊢ (x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \land \neg x < 0) \to 0 < x$
524	345 165	sylan	$⊢ (x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \land 0 < x) \to x \in (0, π)$
525		elun2	$⊢ x \in (0, π) \to x \in ((- π, 0) \cup (0, π))$
526	524 525	syl	$⊢ (x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \land 0 < x) \to x \in ((- π, 0) \cup (0, π))$
527	354 523 526	syl2anc	$⊢ (x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \land \neg x < 0) \to x \in ((- π, 0) \cup (0, π))$
528	353 527	pm2.61dan	$⊢ x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \to x \in ((- π, 0) \cup (0, π))$
529		ovex	$⊢ (- π, 0) \in V$
530		ovex	$⊢ (0, π) \in V$
531	529 530	unipr	$⊢ ⋃ \{(- π, 0), (0, π)\} = (- π, 0) \cup (0, π)$
532	528 531	eleqtrrdi	$⊢ x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \to x \in ⋃ \{(- π, 0), (0, π)\}$
533	532	ssriv	$⊢ dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \subseteq ⋃ \{(- π, 0), (0, π)\}$
534	533	a1i	$⊢ ⊤ \to dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \subseteq ⋃ \{(- π, 0), (0, π)\}$
535		ineq2	$⊢ x = (- π, 0) \to dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap x = dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap (- π, 0)$
536		retop	$⊢ topGen (ran (.)) \in Top$
537		ovex	$⊢ ℝ D F \in V$
538	537	resex	$⊢ {F_{ℝ}^{'} ↾}_{(- π, π)} \in V$
539	538	dmex	$⊢ dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \in V$
540	536 539	pm3.2i	$⊢ (topGen (ran (.)) \in Top \land dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \in V)$
541	319	ssriv	$⊢ (- π, 0) \subseteq dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
542		ssid	$⊢ (- π, 0) \subseteq (- π, 0)$
543	302 541 542	3pm3.2i	$⊢ ((- π, 0) \in topGen (ran (.)) \land (- π, 0) \subseteq dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \land (- π, 0) \subseteq (- π, 0))$
544		restopnb	$⊢ ((topGen (ran (.)) \in Top \land dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \in V) \land ((- π, 0) \in topGen (ran (.)) \land (- π, 0) \subseteq dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \land (- π, 0) \subseteq (- π, 0))) \to ((- π, 0) \in topGen (ran (.)) \leftrightarrow (- π, 0) \in (topGen (ran (.)) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)})))$
545	540 543 544	mp2an	$⊢ (- π, 0) \in topGen (ran (.)) \leftrightarrow (- π, 0) \in (topGen (ran (.)) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)}))$
546	302 545	mpbi	$⊢ (- π, 0) \in (topGen (ran (.)) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)}))$
547		inss2	$⊢ dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap (- π, 0) \subseteq (- π, 0)$
548	541 542	ssini	$⊢ (- π, 0) \subseteq dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap (- π, 0)$
549	547 548	eqssi	$⊢ dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap (- π, 0) = (- π, 0)$
550	200	oveq1i	$⊢ topGen (ran (.)) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) = (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
551	332 344	sstri	$⊢ dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \subseteq ℝ$
552		restabs	$⊢ (TopOpen (ℂ_{fld}) \in Top \land dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \subseteq ℝ \land ℝ \in V) \to (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) = TopOpen (ℂ_{fld}) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
553	410 551 422 552	mp3an	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) = TopOpen (ℂ_{fld}) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
554	550 553	eqtr2i	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) = topGen (ran (.)) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
555	546 549 554	3eltr4i	$⊢ dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap (- π, 0) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)}))$
556	535 555	eqeltrdi	$⊢ x = (- π, 0) \to dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap x \in (TopOpen (ℂ_{fld}) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)}))$
557	556	adantl	$⊢ (x \in \{(- π, 0), (0, π)\} \land x = (- π, 0)) \to dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap x \in (TopOpen (ℂ_{fld}) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)}))$
558		neqne	$⊢ \neg x = (- π, 0) \to x \neq (- π, 0)$
559		elprn1	$⊢ (x \in \{(- π, 0), (0, π)\} \land x \neq (- π, 0)) \to x = (0, π)$
560	558 559	sylan2	$⊢ (x \in \{(- π, 0), (0, π)\} \land \neg x = (- π, 0)) \to x = (0, π)$
561		ineq2	$⊢ x = (0, π) \to dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap x = dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap (0, π)$
562	222	ssriv	$⊢ (0, π) \subseteq dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
563		ssid	$⊢ (0, π) \subseteq (0, π)$
564	199 562 563	3pm3.2i	$⊢ ((0, π) \in topGen (ran (.)) \land (0, π) \subseteq dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \land (0, π) \subseteq (0, π))$
565		restopnb	$⊢ ((topGen (ran (.)) \in Top \land dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \in V) \land ((0, π) \in topGen (ran (.)) \land (0, π) \subseteq dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \land (0, π) \subseteq (0, π))) \to ((0, π) \in topGen (ran (.)) \leftrightarrow (0, π) \in (topGen (ran (.)) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)})))$
566	540 564 565	mp2an	$⊢ (0, π) \in topGen (ran (.)) \leftrightarrow (0, π) \in (topGen (ran (.)) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)}))$
567	199 566	mpbi	$⊢ (0, π) \in (topGen (ran (.)) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)}))$
568		inss2	$⊢ dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap (0, π) \subseteq (0, π)$
569	562 563	ssini	$⊢ (0, π) \subseteq dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap (0, π)$
570	568 569	eqssi	$⊢ dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap (0, π) = (0, π)$
571	567 570 554	3eltr4i	$⊢ dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap (0, π) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)}))$
572	561 571	eqeltrdi	$⊢ x = (0, π) \to dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap x \in (TopOpen (ℂ_{fld}) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)}))$
573	560 572	syl	$⊢ (x \in \{(- π, 0), (0, π)\} \land \neg x = (- π, 0)) \to dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap x \in (TopOpen (ℂ_{fld}) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)}))$
574	557 573	pm2.61dan	$⊢ x \in \{(- π, 0), (0, π)\} \to dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap x \in (TopOpen (ℂ_{fld}) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)}))$
575	574	adantl	$⊢ (⊤ \land x \in \{(- π, 0), (0, π)\}) \to dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap x \in (TopOpen (ℂ_{fld}) ↾_{𝑡} dom ({F_{ℝ}^{'} ↾}_{(- π, π)}))$
576		ssid	$⊢ ℂ \subseteq ℂ$
577	576	a1i	$⊢ ⊤ \to ℂ \subseteq ℂ$
578	394 395 577	constcncfg	$⊢ ⊤ \to (x \in (- π, 0) ⟼ 0) : (- π, 0) \underset{cn}{⟶} ℂ$
579	578	mptru	$⊢ (x \in (- π, 0) ⟼ 0) : (- π, 0) \underset{cn}{⟶} ℂ$
580	579	a1i	$⊢ x = (- π, 0) \to (x \in (- π, 0) ⟼ 0) : (- π, 0) \underset{cn}{⟶} ℂ$
581		reseq2	$⊢ x = (- π, 0) \to {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{x} = {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(- π, 0)}$
582		resabs1	$⊢ (- π, 0) \subseteq (- π, π) \to {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(- π, 0)} = {F_{ℝ}^{'} ↾}_{(- π, 0)}$
583	239 582	ax-mp	$⊢ {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(- π, 0)} = {F_{ℝ}^{'} ↾}_{(- π, 0)}$
584	583 310	eqtr4i	$⊢ {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(- π, 0)} = (x \in (- π, 0) ⟼ 0)$
585	581 584	eqtrdi	$⊢ x = (- π, 0) \to {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{x} = (x \in (- π, 0) ⟼ 0)$
586	535 549	eqtrdi	$⊢ x = (- π, 0) \to dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap x = (- π, 0)$
587	586	oveq1d	$⊢ x = (- π, 0) \to (dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap x) \underset{cn}{⟶} ℂ = (- π, 0) \underset{cn}{⟶} ℂ$
588	580 585 587	3eltr4d	$⊢ x = (- π, 0) \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{x}) : (dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap x) \underset{cn}{⟶} ℂ$
589	588	adantl	$⊢ (x \in \{(- π, 0), (0, π)\} \land x = (- π, 0)) \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{x}) : (dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap x) \underset{cn}{⟶} ℂ$
590	448 395 577	constcncfg	$⊢ ⊤ \to (x \in (0, π) ⟼ 0) : (0, π) \underset{cn}{⟶} ℂ$
591	590	mptru	$⊢ (x \in (0, π) ⟼ 0) : (0, π) \underset{cn}{⟶} ℂ$
592	591	a1i	$⊢ x = (0, π) \to (x \in (0, π) ⟼ 0) : (0, π) \underset{cn}{⟶} ℂ$
593		reseq2	$⊢ x = (0, π) \to {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{x} = {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(0, π)}$
594		resabs1	$⊢ (0, π) \subseteq (- π, π) \to {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(0, π)} = {F_{ℝ}^{'} ↾}_{(0, π)}$
595	169 594	ax-mp	$⊢ {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(0, π)} = {F_{ℝ}^{'} ↾}_{(0, π)}$
596	595 212	eqtr4i	$⊢ {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(0, π)} = (x \in (0, π) ⟼ 0)$
597	593 596	eqtrdi	$⊢ x = (0, π) \to {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{x} = (x \in (0, π) ⟼ 0)$
598	561 570	eqtrdi	$⊢ x = (0, π) \to dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap x = (0, π)$
599	598	oveq1d	$⊢ x = (0, π) \to (dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap x) \underset{cn}{⟶} ℂ = (0, π) \underset{cn}{⟶} ℂ$
600	592 597 599	3eltr4d	$⊢ x = (0, π) \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{x}) : (dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap x) \underset{cn}{⟶} ℂ$
601	560 600	syl	$⊢ (x \in \{(- π, 0), (0, π)\} \land \neg x = (- π, 0)) \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{x}) : (dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap x) \underset{cn}{⟶} ℂ$
602	589 601	pm2.61dan	$⊢ x \in \{(- π, 0), (0, π)\} \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{x}) : (dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap x) \underset{cn}{⟶} ℂ$
603	602	adantl	$⊢ (⊤ \land x \in \{(- π, 0), (0, π)\}) \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{x}) : (dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \cap x) \underset{cn}{⟶} ℂ$
604	335 341 534 575 603	cncfuni	$⊢ ⊤ \to ({F_{ℝ}^{'} ↾}_{(- π, π)}) : dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \underset{cn}{⟶} ℂ$
605	604	mptru	$⊢ ({F_{ℝ}^{'} ↾}_{(- π, π)}) : dom ({F_{ℝ}^{'} ↾}_{(- π, π)}) \underset{cn}{⟶} ℂ$
606		oveq1	$⊢ x = - π \to (x, +∞) = (- π, +∞)$
607	606	reseq2d	$⊢ x = - π \to {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(x, +∞)} = {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(- π, +∞)}$
608		iooss2	$⊢ (+∞ \in ℝ^{*} \land π \leq +∞) \to (- π, π) \subseteq (- π, +∞)$
609	376 453 608	mp2an	$⊢ (- π, π) \subseteq (- π, +∞)$
610		resabs2	$⊢ (- π, π) \subseteq (- π, +∞) \to {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(- π, +∞)} = {F_{ℝ}^{'} ↾}_{(- π, π)}$
611	609 610	ax-mp	$⊢ {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(- π, +∞)} = {F_{ℝ}^{'} ↾}_{(- π, π)}$
612	607 611	eqtrdi	$⊢ x = - π \to {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(x, +∞)} = {F_{ℝ}^{'} ↾}_{(- π, π)}$
613		id	$⊢ x = - π \to x = - π$
614	612 613	oveq12d	$⊢ x = - π \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(x, +∞)}) {lim}_{ℂ} x = ({F_{ℝ}^{'} ↾}_{(- π, π)}) {lim}_{ℂ} (- π)$
615	253	a1i	$⊢ ⊤ \to - π \in ℂ$
616	312 394 395 615	constlimc	$⊢ ⊤ \to 0 \in ((x \in (- π, 0) ⟼ 0) {lim}_{ℂ} (- π))$
617	616	mptru	$⊢ 0 \in ((x \in (- π, 0) ⟼ 0) {lim}_{ℂ} (- π))$
618	310	oveq1i	$⊢ (x \in (- π, 0) ⟼ 0) {lim}_{ℂ} (- π) = ({F_{ℝ}^{'} ↾}_{(- π, 0)}) {lim}_{ℂ} (- π)$
619	336	a1i	$⊢ ⊤ \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ$
620	160	a1i	$⊢ ⊤ \to - π \in ℝ$
621	153	a1i	$⊢ ⊤ \to 0 \in ℝ^{*}$
622	166	a1i	$⊢ ⊤ \to - π < 0$
623	316	a1i	$⊢ ⊤ \to (- π, 0) \subseteq dom F_{ℝ}^{'}$
624	237	a1i	$⊢ ⊤ \to 0 \leq π$
625	619 620 621 622 623 473 624	limcresioolb	$⊢ ⊤ \to ({F_{ℝ}^{'} ↾}_{(- π, 0)}) {lim}_{ℂ} (- π) = ({F_{ℝ}^{'} ↾}_{(- π, π)}) {lim}_{ℂ} (- π)$
626	625	mptru	$⊢ ({F_{ℝ}^{'} ↾}_{(- π, 0)}) {lim}_{ℂ} (- π) = ({F_{ℝ}^{'} ↾}_{(- π, π)}) {lim}_{ℂ} (- π)$
627	618 626	eqtri	$⊢ (x \in (- π, 0) ⟼ 0) {lim}_{ℂ} (- π) = ({F_{ℝ}^{'} ↾}_{(- π, π)}) {lim}_{ℂ} (- π)$
628	617 627	eleqtri	$⊢ 0 \in (({F_{ℝ}^{'} ↾}_{(- π, π)}) {lim}_{ℂ} (- π))$
629	628	ne0ii	$⊢ ({F_{ℝ}^{'} ↾}_{(- π, π)}) {lim}_{ℂ} (- π) \neq \emptyset$
630	629	a1i	$⊢ x = - π \to ({F_{ℝ}^{'} ↾}_{(- π, π)}) {lim}_{ℂ} (- π) \neq \emptyset$
631	614 630	eqnetrd	$⊢ x = - π \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
632	631	adantl	$⊢ (x \in ([- π, π) ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \land x = - π) \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
633		eldifi	$⊢ x \in ([- π, π) ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \to x \in [- π, π)$
634	161	a1i	$⊢ (x \in [- π, π) \land \neg x = - π) \to - π \in ℝ^{*}$
635	155	a1i	$⊢ (x \in [- π, π) \land \neg x = - π) \to π \in ℝ^{*}$
636		icossre	$⊢ (- π \in ℝ \land π \in ℝ^{*}) \to [- π, π) \subseteq ℝ$
637	160 155 636	mp2an	$⊢ [- π, π) \subseteq ℝ$
638	637	sseli	$⊢ x \in [- π, π) \to x \in ℝ$
639	638	adantr	$⊢ (x \in [- π, π) \land \neg x = - π) \to x \in ℝ$
640	160	a1i	$⊢ (x \in [- π, π) \land \neg x = - π) \to - π \in ℝ$
641		icogelb	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land x \in [- π, π)) \to - π \leq x$
642	161 155 641	mp3an12	$⊢ x \in [- π, π) \to - π \leq x$
643	642	adantr	$⊢ (x \in [- π, π) \land \neg x = - π) \to - π \leq x$
644		neqne	$⊢ \neg x = - π \to x \neq - π$
645	644	adantl	$⊢ (x \in [- π, π) \land \neg x = - π) \to x \neq - π$
646	640 639 643 645	leneltd	$⊢ (x \in [- π, π) \land \neg x = - π) \to - π < x$
647		icoltub	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land x \in [- π, π)) \to x < π$
648	161 155 647	mp3an12	$⊢ x \in [- π, π) \to x < π$
649	648	adantr	$⊢ (x \in [- π, π) \land \neg x = - π) \to x < π$
650	634 635 639 646 649	eliood	$⊢ (x \in [- π, π) \land \neg x = - π) \to x \in (- π, π)$
651	633 650	sylan	$⊢ (x \in ([- π, π) ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \land \neg x = - π) \to x \in (- π, π)$
652		eldifn	$⊢ x \in ([- π, π) ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \to \neg x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
653	652	adantr	$⊢ (x \in ([- π, π) ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \land \neg x = - π) \to \neg x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
654	651 653	eldifd	$⊢ (x \in ([- π, π) ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \land \neg x = - π) \to x \in ((- π, π) ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)}))$
655		oveq1	$⊢ x = 0 \to (x, +∞) = (0, +∞)$
656	655	reseq2d	$⊢ x = 0 \to {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(x, +∞)} = {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(0, +∞)}$
657	656 359	oveq12d	$⊢ x = 0 \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(x, +∞)}) {lim}_{ℂ} x = ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(0, +∞)}) {lim}_{ℂ} 0$
658	214 448 395 395	constlimc	$⊢ ⊤ \to 0 \in ((x \in (0, π) ⟼ 0) {lim}_{ℂ} 0)$
659	658	mptru	$⊢ 0 \in ((x \in (0, π) ⟼ 0) {lim}_{ℂ} 0)$
660		resres	$⊢ {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(0, +∞)} = {F_{ℝ}^{'} ↾}_{((- π, π) \cap (0, +∞))}$
661		iooin	$⊢ ((- π \in ℝ^{} \land π \in ℝ^{}) \land (0 \in ℝ^{} \land +∞ \in ℝ^{})) \to (- π, π) \cap (0, +∞) = (if (- π \leq 0, 0, - π), if (π \leq +∞, π, +∞))$
662	161 155 153 376 661	mp4an	$⊢ (- π, π) \cap (0, +∞) = (if (- π \leq 0, 0, - π), if (π \leq +∞, π, +∞))$
663	167	iftruei	$⊢ if (- π \leq 0, 0, - π) = 0$
664	453	iftruei	$⊢ if (π \leq +∞, π, +∞) = π$
665	663 664	oveq12i	$⊢ (if (- π \leq 0, 0, - π), if (π \leq +∞, π, +∞)) = (0, π)$
666	662 665	eqtri	$⊢ (- π, π) \cap (0, +∞) = (0, π)$
667	666	reseq2i	$⊢ {F_{ℝ}^{'} ↾}_{((- π, π) \cap (0, +∞))} = {F_{ℝ}^{'} ↾}_{(0, π)}$
668	212	eqcomi	$⊢ {F_{ℝ}^{'} ↾}_{(0, π)} = (x \in (0, π) ⟼ 0)$
669	660 667 668	3eqtrri	$⊢ (x \in (0, π) ⟼ 0) = {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(0, +∞)}$
670	669	oveq1i	$⊢ (x \in (0, π) ⟼ 0) {lim}_{ℂ} 0 = ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(0, +∞)}) {lim}_{ℂ} 0$
671	659 670	eleqtri	$⊢ 0 \in (({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(0, +∞)}) {lim}_{ℂ} 0)$
672	671	ne0ii	$⊢ ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(0, +∞)}) {lim}_{ℂ} 0 \neq \emptyset$
673	672	a1i	$⊢ x = 0 \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(0, +∞)}) {lim}_{ℂ} 0 \neq \emptyset$
674	657 673	eqnetrd	$⊢ x = 0 \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
675	654 325 674	3syl	$⊢ (x \in ([- π, π) ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \land \neg x = - π) \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
676	632 675	pm2.61dan	$⊢ x \in ([- π, π) ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(x, +∞)}) {lim}_{ℂ} x \neq \emptyset$
677		oveq2	$⊢ x = π \to (−∞, x) = (−∞, π)$
678	677	reseq2d	$⊢ x = π \to {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, x)} = {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, π)}$
679		id	$⊢ x = π \to x = π$
680	678 679	oveq12d	$⊢ x = π \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, x)}) {lim}_{ℂ} x = ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, π)}) {lim}_{ℂ} π$
681		iooss1	$⊢ (−∞ \in ℝ^{*} \land −∞ \leq - π) \to (- π, π) \subseteq (−∞, π)$
682	365 389 681	mp2an	$⊢ (- π, π) \subseteq (−∞, π)$
683		resabs2	$⊢ (- π, π) \subseteq (−∞, π) \to {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, π)} = {F_{ℝ}^{'} ↾}_{(- π, π)}$
684	682 683	ax-mp	$⊢ {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, π)} = {F_{ℝ}^{'} ↾}_{(- π, π)}$
685	684	oveq1i	$⊢ ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, π)}) {lim}_{ℂ} π = ({F_{ℝ}^{'} ↾}_{(- π, π)}) {lim}_{ℂ} π$
686	680 685	eqtrdi	$⊢ x = π \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, x)}) {lim}_{ℂ} x = ({F_{ℝ}^{'} ↾}_{(- π, π)}) {lim}_{ℂ} π$
687	214 448 395 57	constlimc	$⊢ ⊤ \to 0 \in ((x \in (0, π) ⟼ 0) {lim}_{ℂ} π)$
688	687	mptru	$⊢ 0 \in ((x \in (0, π) ⟼ 0) {lim}_{ℂ} π)$
689	212	oveq1i	$⊢ (x \in (0, π) ⟼ 0) {lim}_{ℂ} π = ({F_{ℝ}^{'} ↾}_{(0, π)}) {lim}_{ℂ} π$
690	120	a1i	$⊢ ⊤ \to π \in ℝ$
691	72	a1i	$⊢ ⊤ \to 0 < π$
692	218	a1i	$⊢ ⊤ \to (0, π) \subseteq dom F_{ℝ}^{'}$
693	167	a1i	$⊢ ⊤ \to - π \leq 0$
694	619 621 690 691 692 414 693	limcresiooub	$⊢ ⊤ \to ({F_{ℝ}^{'} ↾}_{(0, π)}) {lim}_{ℂ} π = ({F_{ℝ}^{'} ↾}_{(- π, π)}) {lim}_{ℂ} π$
695	694	mptru	$⊢ ({F_{ℝ}^{'} ↾}_{(0, π)}) {lim}_{ℂ} π = ({F_{ℝ}^{'} ↾}_{(- π, π)}) {lim}_{ℂ} π$
696	689 695	eqtri	$⊢ (x \in (0, π) ⟼ 0) {lim}_{ℂ} π = ({F_{ℝ}^{'} ↾}_{(- π, π)}) {lim}_{ℂ} π$
697	688 696	eleqtri	$⊢ 0 \in (({F_{ℝ}^{'} ↾}_{(- π, π)}) {lim}_{ℂ} π)$
698	697	ne0ii	$⊢ ({F_{ℝ}^{'} ↾}_{(- π, π)}) {lim}_{ℂ} π \neq \emptyset$
699	698	a1i	$⊢ x = π \to ({F_{ℝ}^{'} ↾}_{(- π, π)}) {lim}_{ℂ} π \neq \emptyset$
700	686 699	eqnetrd	$⊢ x = π \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
701	700	adantl	$⊢ (x \in ((- π, π] ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \land x = π) \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
702	161	a1i	$⊢ (x \in ((- π, π] ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \land \neg x = π) \to - π \in ℝ^{*}$
703	155	a1i	$⊢ (x \in ((- π, π] ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \land \neg x = π) \to π \in ℝ^{*}$
704		negpitopissre	$⊢ (- π, π] \subseteq ℝ$
705		eldifi	$⊢ x \in ((- π, π] ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \to x \in (- π, π]$
706	704 705	sselid	$⊢ x \in ((- π, π] ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \to x \in ℝ$
707	706	adantr	$⊢ (x \in ((- π, π] ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \land \neg x = π) \to x \in ℝ$
708	161	a1i	$⊢ x \in ((- π, π] ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \to - π \in ℝ^{*}$
709	155	a1i	$⊢ x \in ((- π, π] ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \to π \in ℝ^{*}$
710		iocgtlb	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land x \in (- π, π]) \to - π < x$
711	708 709 705 710	syl3anc	$⊢ x \in ((- π, π] ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \to - π < x$
712	711	adantr	$⊢ (x \in ((- π, π] ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \land \neg x = π) \to - π < x$
713	120	a1i	$⊢ (x \in ((- π, π] ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \land \neg x = π) \to π \in ℝ$
714		iocleub	$⊢ (- π \in ℝ^{} \land π \in ℝ^{} \land x \in (- π, π]) \to x \leq π$
715	708 709 705 714	syl3anc	$⊢ x \in ((- π, π] ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \to x \leq π$
716	715	adantr	$⊢ (x \in ((- π, π] ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \land \neg x = π) \to x \leq π$
717		id	$⊢ π = x \to π = x$
718	717	eqcomd	$⊢ π = x \to x = π$
719	718	necon3bi	$⊢ \neg x = π \to π \neq x$
720	719	adantl	$⊢ (x \in ((- π, π] ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \land \neg x = π) \to π \neq x$
721	707 713 716 720	leneltd	$⊢ (x \in ((- π, π] ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \land \neg x = π) \to x < π$
722	702 703 707 712 721	eliood	$⊢ (x \in ((- π, π] ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \land \neg x = π) \to x \in (- π, π)$
723		eldifn	$⊢ x \in ((- π, π] ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \to \neg x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
724	723	adantr	$⊢ (x \in ((- π, π] ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \land \neg x = π) \to \neg x \in dom ({F_{ℝ}^{'} ↾}_{(- π, π)})$
725	722 724	eldifd	$⊢ (x \in ((- π, π] ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \land \neg x = π) \to x \in ((- π, π) ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)}))$
726		oveq2	$⊢ x = 0 \to (−∞, x) = (−∞, 0)$
727	726	reseq2d	$⊢ x = 0 \to {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, x)} = {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, 0)}$
728	727 359	oveq12d	$⊢ x = 0 \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, x)}) {lim}_{ℂ} x = ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, 0)}) {lim}_{ℂ} 0$
729	312 394 395 395	constlimc	$⊢ ⊤ \to 0 \in ((x \in (- π, 0) ⟼ 0) {lim}_{ℂ} 0)$
730	729	mptru	$⊢ 0 \in ((x \in (- π, 0) ⟼ 0) {lim}_{ℂ} 0)$
731		resres	$⊢ {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, 0)} = {F_{ℝ}^{'} ↾}_{((- π, π) \cap (−∞, 0))}$
732		iooin	$⊢ ((- π \in ℝ^{} \land π \in ℝ^{}) \land (−∞ \in ℝ^{} \land 0 \in ℝ^{})) \to (- π, π) \cap (−∞, 0) = (if (- π \leq −∞, −∞, - π), if (π \leq 0, π, 0))$
733	161 155 365 153 732	mp4an	$⊢ (- π, π) \cap (−∞, 0) = (if (- π \leq −∞, −∞, - π), if (π \leq 0, π, 0))$
734		mnflt	$⊢ - π \in ℝ \to −∞ < - π$
735	160 734	ax-mp	$⊢ −∞ < - π$
736		xrltnle	$⊢ (−∞ \in ℝ^{} \land - π \in ℝ^{}) \to (−∞ < - π \leftrightarrow \neg - π \leq −∞)$
737	365 161 736	mp2an	$⊢ −∞ < - π \leftrightarrow \neg - π \leq −∞$
738	735 737	mpbi	$⊢ \neg - π \leq −∞$
739	738	iffalsei	$⊢ if (- π \leq −∞, −∞, - π) = - π$
740		xrltnle	$⊢ (0 \in ℝ^{} \land π \in ℝ^{}) \to (0 < π \leftrightarrow \neg π \leq 0)$
741	153 155 740	mp2an	$⊢ 0 < π \leftrightarrow \neg π \leq 0$
742	72 741	mpbi	$⊢ \neg π \leq 0$
743	742	iffalsei	$⊢ if (π \leq 0, π, 0) = 0$
744	739 743	oveq12i	$⊢ (if (- π \leq −∞, −∞, - π), if (π \leq 0, π, 0)) = (- π, 0)$
745	733 744	eqtri	$⊢ (- π, π) \cap (−∞, 0) = (- π, 0)$
746	745	reseq2i	$⊢ {F_{ℝ}^{'} ↾}_{((- π, π) \cap (−∞, 0))} = {F_{ℝ}^{'} ↾}_{(- π, 0)}$
747	310	eqcomi	$⊢ {F_{ℝ}^{'} ↾}_{(- π, 0)} = (x \in (- π, 0) ⟼ 0)$
748	731 746 747	3eqtrri	$⊢ (x \in (- π, 0) ⟼ 0) = {({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, 0)}$
749	748	oveq1i	$⊢ (x \in (- π, 0) ⟼ 0) {lim}_{ℂ} 0 = ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, 0)}) {lim}_{ℂ} 0$
750	730 749	eleqtri	$⊢ 0 \in (({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, 0)}) {lim}_{ℂ} 0)$
751	750	ne0ii	$⊢ ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, 0)}) {lim}_{ℂ} 0 \neq \emptyset$
752	751	a1i	$⊢ x = 0 \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, 0)}) {lim}_{ℂ} 0 \neq \emptyset$
753	728 752	eqnetrd	$⊢ x = 0 \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
754	725 325 753	3syl	$⊢ (x \in ((- π, π] ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \land \neg x = π) \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
755	701 754	pm2.61dan	$⊢ x \in ((- π, π] ∖ dom ({F_{ℝ}^{'} ↾}_{(- π, π)})) \to ({({F_{ℝ}^{'} ↾}_{(- π, π)}) ↾}_{(−∞, x)}) {lim}_{ℂ} x \neq \emptyset$
756		eqid	$⊢ (x \in (X - (X \mod T), X) ⟼ 1) = (x \in (X - (X \mod T), X) ⟼ 1)$
757		ioosscn	$⊢ (X - (X \mod T), X) \subseteq ℂ$
758	757	a1i	$⊢ X \mod T \in (0, π) \to (X - (X \mod T), X) \subseteq ℂ$
759		1cnd	$⊢ X \mod T \in (0, π) \to 1 \in ℂ$
760	27	a1i	$⊢ X \mod T \in (0, π) \to X \in ℂ$
761	756 758 759 760	constlimc	$⊢ X \mod T \in (0, π) \to 1 \in ((x \in (X - (X \mod T), X) ⟼ 1) {lim}_{ℂ} X)$
762		ioossioc	$⊢ (0, π) \subseteq (0, π]$
763	762	sseli	$⊢ X \mod T \in (0, π) \to X \mod T \in (0, π]$
764	763	iftrued	$⊢ X \mod T \in (0, π) \to if (X \mod T \in (0, π], 1, - 1) = 1$
765	209	a1i	$⊢ X \mod T \in (0, π) \to F : ℝ ⟶ ℂ$
766		modcl	$⊢ (X \in ℝ \land T \in ℝ^{+}) \to X \mod T \in ℝ$
767	3 135 766	mp2an	$⊢ X \mod T \in ℝ$
768	3 767	resubcli	$⊢ X - (X \mod T) \in ℝ$
769	768	rexri	$⊢ X - (X \mod T) \in ℝ^{*}$
770	769	a1i	$⊢ X \mod T \in (0, π) \to X - (X \mod T) \in ℝ^{*}$
771	3	a1i	$⊢ X \mod T \in (0, π) \to X \in ℝ$
772		elioore	$⊢ X \mod T \in (0, π) \to X \mod T \in ℝ$
773		ioogtlb	$⊢ (0 \in ℝ^{} \land π \in ℝ^{} \land X \mod T \in (0, π)) \to 0 < X \mod T$
774	153 155 773	mp3an12	$⊢ X \mod T \in (0, π) \to 0 < X \mod T$
775	772 774	elrpd	$⊢ X \mod T \in (0, π) \to X \mod T \in ℝ^{+}$
776	771 775	ltsubrpd	$⊢ X \mod T \in (0, π) \to X - (X \mod T) < X$
777		ioossre	$⊢ (X - (X \mod T), X) \subseteq ℝ$
778	777	a1i	$⊢ X \mod T \in (0, π) \to (X - (X \mod T), X) \subseteq ℝ$
779	365	a1i	$⊢ X \mod T \in (0, π) \to −∞ \in ℝ^{*}$
780		mnflt	$⊢ X - (X \mod T) \in ℝ \to −∞ < X - (X \mod T)$
781		xrltle	$⊢ (−∞ \in ℝ^{} \land X - (X \mod T) \in ℝ^{}) \to (−∞ < X - (X \mod T) \to −∞ \leq X - (X \mod T))$
782	365 769 781	mp2an	$⊢ −∞ < X - (X \mod T) \to −∞ \leq X - (X \mod T)$
783	768 780 782	mp2b	$⊢ −∞ \leq X - (X \mod T)$
784	783	a1i	$⊢ X \mod T \in (0, π) \to −∞ \leq X - (X \mod T)$
785	765 770 771 776 778 779 784	limcresiooub	$⊢ X \mod T \in (0, π) \to ({F ↾}_{(X - (X \mod T), X)}) {lim}_{ℂ} X = ({F ↾}_{(−∞, X)}) {lim}_{ℂ} X$
786		iooltub	$⊢ (0 \in ℝ^{} \land π \in ℝ^{} \land X \mod T \in (0, π)) \to X \mod T < π$
787	153 155 786	mp3an12	$⊢ X \mod T \in (0, π) \to X \mod T < π$
788	209	a1i	$⊢ X \mod T < π \to F : ℝ ⟶ ℂ$
789	777	a1i	$⊢ X \mod T < π \to (X - (X \mod T), X) \subseteq ℝ$
790	788 789	feqresmpt	$⊢ X \mod T < π \to {F ↾}_{(X - (X \mod T), X)} = (x \in (X - (X \mod T), X) ⟼ F (x))$
791		elioore	$⊢ x \in (X - (X \mod T), X) \to x \in ℝ$
792	791 110 147	sylancl	$⊢ x \in (X - (X \mod T), X) \to F (x) = if (x \mod T < π, 1, - 1)$
793	792	adantl	$⊢ (X \mod T < π \land x \in (X - (X \mod T), X)) \to F (x) = if (x \mod T < π, 1, - 1)$
794	791	adantl	$⊢ (X \mod T < π \land x \in (X - (X \mod T), X)) \to x \in ℝ$
795	135	a1i	$⊢ (X \mod T < π \land x \in (X - (X \mod T), X)) \to T \in ℝ^{+}$
796	794 795	modcld	$⊢ (X \mod T < π \land x \in (X - (X \mod T), X)) \to x \mod T \in ℝ$
797	767	a1i	$⊢ (X \mod T < π \land x \in (X - (X \mod T), X)) \to X \mod T \in ℝ$
798	120	a1i	$⊢ (X \mod T < π \land x \in (X - (X \mod T), X)) \to π \in ℝ$
799	3	a1i	$⊢ x \in (X - (X \mod T), X) \to X \in ℝ$
800	135	a1i	$⊢ x \in (X - (X \mod T), X) \to T \in ℝ^{+}$
801		ioossico	$⊢ (X - (X \mod T), X) \subseteq [X - (X \mod T), X)$
802	801	sseli	$⊢ x \in (X - (X \mod T), X) \to x \in [X - (X \mod T), X)$
803	799 800 802	ltmod	$⊢ x \in (X - (X \mod T), X) \to x \mod T < X \mod T$
804	803	adantl	$⊢ (X \mod T < π \land x \in (X - (X \mod T), X)) \to x \mod T < X \mod T$
805		simpl	$⊢ (X \mod T < π \land x \in (X - (X \mod T), X)) \to X \mod T < π$
806	796 797 798 804 805	lttrd	$⊢ (X \mod T < π \land x \in (X - (X \mod T), X)) \to x \mod T < π$
807	806	iftrued	$⊢ (X \mod T < π \land x \in (X - (X \mod T), X)) \to if (x \mod T < π, 1, - 1) = 1$
808	793 807	eqtrd	$⊢ (X \mod T < π \land x \in (X - (X \mod T), X)) \to F (x) = 1$
809	808	mpteq2dva	$⊢ X \mod T < π \to (x \in (X - (X \mod T), X) ⟼ F (x)) = (x \in (X - (X \mod T), X) ⟼ 1)$
810	790 809	eqtrd	$⊢ X \mod T < π \to {F ↾}_{(X - (X \mod T), X)} = (x \in (X - (X \mod T), X) ⟼ 1)$
811	787 810	syl	$⊢ X \mod T \in (0, π) \to {F ↾}_{(X - (X \mod T), X)} = (x \in (X - (X \mod T), X) ⟼ 1)$
812	811	oveq1d	$⊢ X \mod T \in (0, π) \to ({F ↾}_{(X - (X \mod T), X)}) {lim}_{ℂ} X = (x \in (X - (X \mod T), X) ⟼ 1) {lim}_{ℂ} X$
813	785 812	eqtr3d	$⊢ X \mod T \in (0, π) \to ({F ↾}_{(−∞, X)}) {lim}_{ℂ} X = (x \in (X - (X \mod T), X) ⟼ 1) {lim}_{ℂ} X$
814	761 764 813	3eltr4d	$⊢ X \mod T \in (0, π) \to if (X \mod T \in (0, π], 1, - 1) \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
815		eqid	$⊢ (x \in (X - π, X) ⟼ - 1) = (x \in (X - π, X) ⟼ - 1)$
816		ioossre	$⊢ (X - π, X) \subseteq ℝ$
817	816	a1i	$⊢ ⊤ \to (X - π, X) \subseteq ℝ$
818	817 207	sstrdi	$⊢ ⊤ \to (X - π, X) \subseteq ℂ$
819	27	a1i	$⊢ ⊤ \to X \in ℂ$
820	815 818 305 819	constlimc	$⊢ ⊤ \to - 1 \in ((x \in (X - π, X) ⟼ - 1) {lim}_{ℂ} X)$
821	820	mptru	$⊢ - 1 \in ((x \in (X - π, X) ⟼ - 1) {lim}_{ℂ} X)$
822	821	a1i	$⊢ X \mod T = 0 \to - 1 \in ((x \in (X - π, X) ⟼ - 1) {lim}_{ℂ} X)$
823		id	$⊢ X \mod T = 0 \to X \mod T = 0$
824		lbioc	$⊢ \neg 0 \in (0, π]$
825	824	a1i	$⊢ X \mod T = 0 \to \neg 0 \in (0, π]$
826	823 825	eqneltrd	$⊢ X \mod T = 0 \to \neg X \mod T \in (0, π]$
827	826	iffalsed	$⊢ X \mod T = 0 \to if (X \mod T \in (0, π], 1, - 1) = - 1$
828	209	a1i	$⊢ X \mod T = 0 \to F : ℝ ⟶ ℂ$
829	816	a1i	$⊢ X \mod T = 0 \to (X - π, X) \subseteq ℝ$
830	828 829	feqresmpt	$⊢ X \mod T = 0 \to {F ↾}_{(X - π, X)} = (x \in (X - π, X) ⟼ F (x))$
831	829	sselda	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to x \in ℝ$
832	831 110 147	sylancl	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to F (x) = if (x \mod T < π, 1, - 1)$
833	120	a1i	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to π \in ℝ$
834	135	a1i	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to T \in ℝ^{+}$
835	831 834	modcld	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to x \mod T \in ℝ$
836	3 120	resubcli	$⊢ X - π \in ℝ$
837	836	a1i	$⊢ x \in (X - π, X) \to X - π \in ℝ$
838	122	a1i	$⊢ x \in (X - π, X) \to T \in ℝ$
839	837 838	readdcld	$⊢ x \in (X - π, X) \to X - π + T \in ℝ$
840		elioore	$⊢ x \in (X - π, X) \to x \in ℝ$
841	840 838	readdcld	$⊢ x \in (X - π, X) \to x + T \in ℝ$
842	3	a1i	$⊢ x \in (X - π, X) \to X \in ℝ$
843	836	rexri	$⊢ X - π \in ℝ^{*}$
844	843	a1i	$⊢ x \in (X - π, X) \to X - π \in ℝ^{*}$
845	842	rexrd	$⊢ x \in (X - π, X) \to X \in ℝ^{*}$
846		id	$⊢ x \in (X - π, X) \to x \in (X - π, X)$
847		ioogtlb	$⊢ (X - π \in ℝ^{} \land X \in ℝ^{} \land x \in (X - π, X)) \to X - π < x$
848	844 845 846 847	syl3anc	$⊢ x \in (X - π, X) \to X - π < x$
849	837 840 838 848	ltadd1dd	$⊢ x \in (X - π, X) \to X - π + T < x + T$
850	839 841 842 849	ltsub1dd	$⊢ x \in (X - π, X) \to (X - π) + T - X < x + T - X$
851	850	adantl	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to (X - π) + T - X < x + T - X$
852	251	oveq2i	$⊢ X - π + T = (X - π) + π + π$
853	56 56	addcli	$⊢ π + π \in ℂ$
854		subadd23	$⊢ (X \in ℂ \land π \in ℂ \land π + π \in ℂ) \to (X - π) + π + π = X + (π + π) - π$
855	27 56 853 854	mp3an	$⊢ (X - π) + π + π = X + (π + π) - π$
856	56 56	pncan3oi	$⊢ π + π - π = π$
857	856	oveq2i	$⊢ X + (π + π) - π = X + π$
858	852 855 857	3eqtri	$⊢ X - π + T = X + π$
859	858	oveq1i	$⊢ (X - π) + T - X = X + π - X$
860		pncan2	$⊢ (X \in ℂ \land π \in ℂ) \to X + π - X = π$
861	27 56 860	mp2an	$⊢ X + π - X = π$
862	859 861	eqtr2i	$⊢ π = (X - π) + T - X$
863	862	a1i	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to π = (X - π) + T - X$
864	841 842	resubcld	$⊢ x \in (X - π, X) \to x + T - X \in ℝ$
865		modabs2	$⊢ (x + T - X \in ℝ \land T \in ℝ^{+}) \to ((x + T - X) \mod T) \mod T = (x + T - X) \mod T$
866	864 135 865	sylancl	$⊢ x \in (X - π, X) \to ((x + T - X) \mod T) \mod T = (x + T - X) \mod T$
867	135	a1i	$⊢ x \in (X - π, X) \to T \in ℝ^{+}$
868		0red	$⊢ x \in (X - π, X) \to 0 \in ℝ$
869	839 842	resubcld	$⊢ x \in (X - π, X) \to (X - π) + T - X \in ℝ$
870	72 862	breqtri	$⊢ 0 < (X - π) + T - X$
871	870	a1i	$⊢ x \in (X - π, X) \to 0 < (X - π) + T - X$
872	868 869 864 871 850	lttrd	$⊢ x \in (X - π, X) \to 0 < x + T - X$
873	868 864 872	ltled	$⊢ x \in (X - π, X) \to 0 \leq x + T - X$
874	842 838	readdcld	$⊢ x \in (X - π, X) \to X + T \in ℝ$
875		iooltub	$⊢ (X - π \in ℝ^{} \land X \in ℝ^{} \land x \in (X - π, X)) \to x < X$
876	844 845 846 875	syl3anc	$⊢ x \in (X - π, X) \to x < X$
877	840 842 838 876	ltadd1dd	$⊢ x \in (X - π, X) \to x + T < X + T$
878	841 874 842 877	ltsub1dd	$⊢ x \in (X - π, X) \to x + T - X < X + T - X$
879		pncan2	$⊢ (X \in ℂ \land T \in ℂ) \to X + T - X = T$
880	27 123 879	mp2an	$⊢ X + T - X = T$
881	878 880	breqtrdi	$⊢ x \in (X - π, X) \to x + T - X < T$
882		modid	$⊢ ((x + T - X \in ℝ \land T \in ℝ^{+}) \land (0 \leq x + T - X \land x + T - X < T)) \to (x + T - X) \mod T = x + T - X$
883	864 867 873 881 882	syl22anc	$⊢ x \in (X - π, X) \to (x + T - X) \mod T = x + T - X$
884	866 883	eqtr2d	$⊢ x \in (X - π, X) \to x + T - X = ((x + T - X) \mod T) \mod T$
885	884	adantl	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to x + T - X = ((x + T - X) \mod T) \mod T$
886		oveq2	$⊢ X \mod T = 0 \to ((x + T - X) \mod T) + (X \mod T) = ((x + T - X) \mod T) + 0$
887	886	adantr	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to ((x + T - X) \mod T) + (X \mod T) = ((x + T - X) \mod T) + 0$
888	864 867	modcld	$⊢ x \in (X - π, X) \to (x + T - X) \mod T \in ℝ$
889	888	recnd	$⊢ x \in (X - π, X) \to (x + T - X) \mod T \in ℂ$
890	889	addridd	$⊢ x \in (X - π, X) \to ((x + T - X) \mod T) + 0 = (x + T - X) \mod T$
891	890	adantl	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to ((x + T - X) \mod T) + 0 = (x + T - X) \mod T$
892	887 891	eqtr2d	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to (x + T - X) \mod T = ((x + T - X) \mod T) + (X \mod T)$
893	892	oveq1d	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to ((x + T - X) \mod T) \mod T = (((x + T - X) \mod T) + (X \mod T)) \mod T$
894		modaddabs	$⊢ (x + T - X \in ℝ \land X \in ℝ \land T \in ℝ^{+}) \to (((x + T - X) \mod T) + (X \mod T)) \mod T = ((x + T) - X + X) \mod T$
895	864 842 867 894	syl3anc	$⊢ x \in (X - π, X) \to (((x + T - X) \mod T) + (X \mod T)) \mod T = ((x + T) - X + X) \mod T$
896	895	adantl	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to (((x + T - X) \mod T) + (X \mod T)) \mod T = ((x + T) - X + X) \mod T$
897	885 893 896	3eqtrd	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to x + T - X = ((x + T) - X + X) \mod T$
898	145	recnd	$⊢ x \in ℝ \to x + T \in ℂ$
899	27	a1i	$⊢ x \in ℝ \to X \in ℂ$
900	898 899	npcand	$⊢ x \in ℝ \to (x + T) - X + X = x + T$
901	124	a1i	$⊢ x \in ℝ \to 1 T = T$
902	901	oveq2d	$⊢ x \in ℝ \to x + 1 T = x + T$
903	900 902	eqtr4d	$⊢ x \in ℝ \to (x + T) - X + X = x + 1 T$
904	903	oveq1d	$⊢ x \in ℝ \to ((x + T) - X + X) \mod T = (x + 1 T) \mod T$
905	840 904	syl	$⊢ x \in (X - π, X) \to ((x + T) - X + X) \mod T = (x + 1 T) \mod T$
906	905	adantl	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to ((x + T) - X + X) \mod T = (x + 1 T) \mod T$
907		1zzd	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to 1 \in ℤ$
908	831 834 907 138	syl3anc	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to (x + 1 T) \mod T = x \mod T$
909	897 906 908	3eqtrrd	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to x \mod T = x + T - X$
910	851 863 909	3brtr4d	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to π < x \mod T$
911	833 835 910	ltled	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to π \leq x \mod T$
912	833 835 911	lensymd	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to \neg x \mod T < π$
913	912	iffalsed	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to if (x \mod T < π, 1, - 1) = - 1$
914	832 913	eqtrd	$⊢ (X \mod T = 0 \land x \in (X - π, X)) \to F (x) = - 1$
915	914	mpteq2dva	$⊢ X \mod T = 0 \to (x \in (X - π, X) ⟼ F (x)) = (x \in (X - π, X) ⟼ - 1)$
916	830 915	eqtr2d	$⊢ X \mod T = 0 \to (x \in (X - π, X) ⟼ - 1) = {F ↾}_{(X - π, X)}$
917	916	oveq1d	$⊢ X \mod T = 0 \to (x \in (X - π, X) ⟼ - 1) {lim}_{ℂ} X = ({F ↾}_{(X - π, X)}) {lim}_{ℂ} X$
918	843	a1i	$⊢ ⊤ \to X - π \in ℝ^{*}$
919	3	a1i	$⊢ ⊤ \to X \in ℝ$
920		ltsubrp	$⊢ (X \in ℝ \land π \in ℝ^{+}) \to X - π < X$
921	3 184 920	mp2an	$⊢ X - π < X$
922	921	a1i	$⊢ ⊤ \to X - π < X$
923		mnflt	$⊢ X - π \in ℝ \to −∞ < X - π$
924		xrltle	$⊢ (−∞ \in ℝ^{} \land X - π \in ℝ^{}) \to (−∞ < X - π \to −∞ \leq X - π)$
925	365 843 924	mp2an	$⊢ −∞ < X - π \to −∞ \leq X - π$
926	836 923 925	mp2b	$⊢ −∞ \leq X - π$
927	926	a1i	$⊢ ⊤ \to −∞ \leq X - π$
928	363 918 919 922 817 366 927	limcresiooub	$⊢ ⊤ \to ({F ↾}_{(X - π, X)}) {lim}_{ℂ} X = ({F ↾}_{(−∞, X)}) {lim}_{ℂ} X$
929	928	mptru	$⊢ ({F ↾}_{(X - π, X)}) {lim}_{ℂ} X = ({F ↾}_{(−∞, X)}) {lim}_{ℂ} X$
930	917 929	eqtr2di	$⊢ X \mod T = 0 \to ({F ↾}_{(−∞, X)}) {lim}_{ℂ} X = (x \in (X - π, X) ⟼ - 1) {lim}_{ℂ} X$
931	822 827 930	3eltr4d	$⊢ X \mod T = 0 \to if (X \mod T \in (0, π], 1, - 1) \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
932	931	adantl	$⊢ (\neg X \mod T \in (0, π) \land X \mod T = 0) \to if (X \mod T \in (0, π], 1, - 1) \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
933	155	a1i	$⊢ (\neg X \mod T \in (0, π) \land \neg X \mod T = 0) \to π \in ℝ^{*}$
934	122	rexri	$⊢ T \in ℝ^{*}$
935	934	a1i	$⊢ (\neg X \mod T \in (0, π) \land \neg X \mod T = 0) \to T \in ℝ^{*}$
936	767	rexri	$⊢ X \mod T \in ℝ^{*}$
937	936	a1i	$⊢ (\neg X \mod T \in (0, π) \land \neg X \mod T = 0) \to X \mod T \in ℝ^{*}$
938	120	a1i	$⊢ (\neg X \mod T \in (0, π) \land \neg X \mod T = 0) \to π \in ℝ$
939	767	a1i	$⊢ (\neg X \mod T \in (0, π) \land \neg X \mod T = 0) \to X \mod T \in ℝ$
940		pm4.56	$⊢ (\neg X \mod T \in (0, π) \land \neg X \mod T = 0) \leftrightarrow \neg (X \mod T \in (0, π) \lor X \mod T = 0)$
941	940	biimpi	$⊢ (\neg X \mod T \in (0, π) \land \neg X \mod T = 0) \to \neg (X \mod T \in (0, π) \lor X \mod T = 0)$
942		olc	$⊢ X \mod T = 0 \to (X \mod T \in (0, π) \lor X \mod T = 0)$
943	942	adantl	$⊢ (X \mod T < π \land X \mod T = 0) \to (X \mod T \in (0, π) \lor X \mod T = 0)$
944	153	a1i	$⊢ (X \mod T < π \land X \mod T \neq 0) \to 0 \in ℝ^{*}$
945	155	a1i	$⊢ (X \mod T < π \land X \mod T \neq 0) \to π \in ℝ^{*}$
946	767	a1i	$⊢ (X \mod T < π \land X \mod T \neq 0) \to X \mod T \in ℝ$
947		0red	$⊢ X \mod T \neq 0 \to 0 \in ℝ$
948	767	a1i	$⊢ X \mod T \neq 0 \to X \mod T \in ℝ$
949		modge0	$⊢ (X \in ℝ \land T \in ℝ^{+}) \to 0 \leq X \mod T$
950	3 135 949	mp2an	$⊢ 0 \leq X \mod T$
951	950	a1i	$⊢ X \mod T \neq 0 \to 0 \leq X \mod T$
952		id	$⊢ X \mod T \neq 0 \to X \mod T \neq 0$
953	947 948 951 952	leneltd	$⊢ X \mod T \neq 0 \to 0 < X \mod T$
954	953	adantl	$⊢ (X \mod T < π \land X \mod T \neq 0) \to 0 < X \mod T$
955		simpl	$⊢ (X \mod T < π \land X \mod T \neq 0) \to X \mod T < π$
956	944 945 946 954 955	eliood	$⊢ (X \mod T < π \land X \mod T \neq 0) \to X \mod T \in (0, π)$
957	956	orcd	$⊢ (X \mod T < π \land X \mod T \neq 0) \to (X \mod T \in (0, π) \lor X \mod T = 0)$
958	943 957	pm2.61dane	$⊢ X \mod T < π \to (X \mod T \in (0, π) \lor X \mod T = 0)$
959	941 958	nsyl	$⊢ (\neg X \mod T \in (0, π) \land \neg X \mod T = 0) \to \neg X \mod T < π$
960	938 939 959	nltled	$⊢ (\neg X \mod T \in (0, π) \land \neg X \mod T = 0) \to π \leq X \mod T$
961		modlt	$⊢ (X \in ℝ \land T \in ℝ^{+}) \to X \mod T < T$
962	3 135 961	mp2an	$⊢ X \mod T < T$
963	962	a1i	$⊢ (\neg X \mod T \in (0, π) \land \neg X \mod T = 0) \to X \mod T < T$
964	933 935 937 960 963	elicod	$⊢ (\neg X \mod T \in (0, π) \land \neg X \mod T = 0) \to X \mod T \in [π, T)$
965		eqid	$⊢ (x \in (X - π, X) ⟼ 1) = (x \in (X - π, X) ⟼ 1)$
966	965 818 203 819	constlimc	$⊢ ⊤ \to 1 \in ((x \in (X - π, X) ⟼ 1) {lim}_{ℂ} X)$
967	966	mptru	$⊢ 1 \in ((x \in (X - π, X) ⟼ 1) {lim}_{ℂ} X)$
968	967	a1i	$⊢ X \mod T = π \to 1 \in ((x \in (X - π, X) ⟼ 1) {lim}_{ℂ} X)$
969		id	$⊢ X \mod T = π \to X \mod T = π$
970		ubioc1	$⊢ (0 \in ℝ^{} \land π \in ℝ^{} \land 0 < π) \to π \in (0, π]$
971	153 155 72 970	mp3an	$⊢ π \in (0, π]$
972	969 971	eqeltrdi	$⊢ X \mod T = π \to X \mod T \in (0, π]$
973	972	iftrued	$⊢ X \mod T = π \to if (X \mod T \in (0, π], 1, - 1) = 1$
974	363 817	feqresmpt	$⊢ ⊤ \to {F ↾}_{(X - π, X)} = (x \in (X - π, X) ⟼ F (x))$
975	974	mptru	$⊢ {F ↾}_{(X - π, X)} = (x \in (X - π, X) ⟼ F (x))$
976	840 110 147	sylancl	$⊢ x \in (X - π, X) \to F (x) = if (x \mod T < π, 1, - 1)$
977	976	adantl	$⊢ (X \mod T = π \land x \in (X - π, X)) \to F (x) = if (x \mod T < π, 1, - 1)$
978		simpr	$⊢ (X \mod T = π \land x \in (X - π, X)) \to x \in (X - π, X)$
979	969	eqcomd	$⊢ X \mod T = π \to π = X \mod T$
980	979	oveq2d	$⊢ X \mod T = π \to X - π = X - (X \mod T)$
981	980	oveq1d	$⊢ X \mod T = π \to (X - π, X) = (X - (X \mod T), X)$
982	981	adantr	$⊢ (X \mod T = π \land x \in (X - π, X)) \to (X - π, X) = (X - (X \mod T), X)$
983	978 982	eleqtrd	$⊢ (X \mod T = π \land x \in (X - π, X)) \to x \in (X - (X \mod T), X)$
984	983 803	syl	$⊢ (X \mod T = π \land x \in (X - π, X)) \to x \mod T < X \mod T$
985		simpl	$⊢ (X \mod T = π \land x \in (X - π, X)) \to X \mod T = π$
986	984 985	breqtrd	$⊢ (X \mod T = π \land x \in (X - π, X)) \to x \mod T < π$
987	986	iftrued	$⊢ (X \mod T = π \land x \in (X - π, X)) \to if (x \mod T < π, 1, - 1) = 1$
988	977 987	eqtrd	$⊢ (X \mod T = π \land x \in (X - π, X)) \to F (x) = 1$
989	988	mpteq2dva	$⊢ X \mod T = π \to (x \in (X - π, X) ⟼ F (x)) = (x \in (X - π, X) ⟼ 1)$
990	975 989	eqtr2id	$⊢ X \mod T = π \to (x \in (X - π, X) ⟼ 1) = {F ↾}_{(X - π, X)}$
991	990	oveq1d	$⊢ X \mod T = π \to (x \in (X - π, X) ⟼ 1) {lim}_{ℂ} X = ({F ↾}_{(X - π, X)}) {lim}_{ℂ} X$
992	991 929	eqtr2di	$⊢ X \mod T = π \to ({F ↾}_{(−∞, X)}) {lim}_{ℂ} X = (x \in (X - π, X) ⟼ 1) {lim}_{ℂ} X$
993	968 973 992	3eltr4d	$⊢ X \mod T = π \to if (X \mod T \in (0, π], 1, - 1) \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
994	993	adantl	$⊢ (X \mod T \in [π, T) \land X \mod T = π) \to if (X \mod T \in (0, π], 1, - 1) \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
995	155	a1i	$⊢ (X \mod T \in [π, T) \land \neg X \mod T = π) \to π \in ℝ^{*}$
996	934	a1i	$⊢ (X \mod T \in [π, T) \land \neg X \mod T = π) \to T \in ℝ^{*}$
997	767	a1i	$⊢ (X \mod T \in [π, T) \land \neg X \mod T = π) \to X \mod T \in ℝ$
998	120	a1i	$⊢ (X \mod T \in [π, T) \land \neg X \mod T = π) \to π \in ℝ$
999		icogelb	$⊢ (π \in ℝ^{} \land T \in ℝ^{} \land X \mod T \in [π, T)) \to π \leq X \mod T$
1000	155 934 999	mp3an12	$⊢ X \mod T \in [π, T) \to π \leq X \mod T$
1001	1000	adantr	$⊢ (X \mod T \in [π, T) \land \neg X \mod T = π) \to π \leq X \mod T$
1002		neqne	$⊢ \neg X \mod T = π \to X \mod T \neq π$
1003	1002	adantl	$⊢ (X \mod T \in [π, T) \land \neg X \mod T = π) \to X \mod T \neq π$
1004	998 997 1001 1003	leneltd	$⊢ (X \mod T \in [π, T) \land \neg X \mod T = π) \to π < X \mod T$
1005	962	a1i	$⊢ (X \mod T \in [π, T) \land \neg X \mod T = π) \to X \mod T < T$
1006	995 996 997 1004 1005	eliood	$⊢ (X \mod T \in [π, T) \land \neg X \mod T = π) \to X \mod T \in (π, T)$
1007		eqid	$⊢ (x \in (X + π - (X \mod T), X) ⟼ - 1) = (x \in (X + π - (X \mod T), X) ⟼ - 1)$
1008		ioossre	$⊢ (X + π - (X \mod T), X) \subseteq ℝ$
1009	1008	a1i	$⊢ X \mod T \in (π, T) \to (X + π - (X \mod T), X) \subseteq ℝ$
1010	1009 207	sstrdi	$⊢ X \mod T \in (π, T) \to (X + π - (X \mod T), X) \subseteq ℂ$
1011		neg1cn	$⊢ - 1 \in ℂ$
1012	1011	a1i	$⊢ X \mod T \in (π, T) \to - 1 \in ℂ$
1013	27	a1i	$⊢ X \mod T \in (π, T) \to X \in ℂ$
1014	1007 1010 1012 1013	constlimc	$⊢ X \mod T \in (π, T) \to - 1 \in ((x \in (X + π - (X \mod T), X) ⟼ - 1) {lim}_{ℂ} X)$
1015	153	a1i	$⊢ X \mod T \in (π, T) \to 0 \in ℝ^{*}$
1016	120	a1i	$⊢ X \mod T \in (π, T) \to π \in ℝ$
1017	936	a1i	$⊢ X \mod T \in (π, T) \to X \mod T \in ℝ^{*}$
1018		ioogtlb	$⊢ (π \in ℝ^{} \land T \in ℝ^{} \land X \mod T \in (π, T)) \to π < X \mod T$
1019	155 934 1018	mp3an12	$⊢ X \mod T \in (π, T) \to π < X \mod T$
1020	1015 1016 1017 1019	gtnelioc	$⊢ X \mod T \in (π, T) \to \neg X \mod T \in (0, π]$
1021	1020	iffalsed	$⊢ X \mod T \in (π, T) \to if (X \mod T \in (0, π], 1, - 1) = - 1$
1022	1008	a1i	$⊢ ⊤ \to (X + π - (X \mod T), X) \subseteq ℝ$
1023	363 1022	feqresmpt	$⊢ ⊤ \to {F ↾}_{(X + π - (X \mod T), X)} = (x \in (X + π - (X \mod T), X) ⟼ F (x))$
1024	1023	mptru	$⊢ {F ↾}_{(X + π - (X \mod T), X)} = (x \in (X + π - (X \mod T), X) ⟼ F (x))$
1025		elioore	$⊢ x \in (X + π - (X \mod T), X) \to x \in ℝ$
1026	1025 110 147	sylancl	$⊢ x \in (X + π - (X \mod T), X) \to F (x) = if (x \mod T < π, 1, - 1)$
1027	1026	adantl	$⊢ (X \mod T \in (π, T) \land x \in (X + π - (X \mod T), X)) \to F (x) = if (x \mod T < π, 1, - 1)$
1028	120	a1i	$⊢ (X \mod T \in (π, T) \land x \in (X + π - (X \mod T), X)) \to π \in ℝ$
1029	135	a1i	$⊢ x \in (X + π - (X \mod T), X) \to T \in ℝ^{+}$
1030	1025 1029	modcld	$⊢ x \in (X + π - (X \mod T), X) \to x \mod T \in ℝ$
1031	1030	adantl	$⊢ (X \mod T \in (π, T) \land x \in (X + π - (X \mod T), X)) \to x \mod T \in ℝ$
1032	3 120	readdcli	$⊢ X + π \in ℝ$
1033	1032	recni	$⊢ X + π \in ℂ$
1034	1033	a1i	$⊢ x \in (X + π - (X \mod T), X) \to X + π \in ℂ$
1035	27	a1i	$⊢ x \in (X + π - (X \mod T), X) \to X \in ℂ$
1036	767	recni	$⊢ X \mod T \in ℂ$
1037	1036	a1i	$⊢ x \in (X + π - (X \mod T), X) \to X \mod T \in ℂ$
1038	1034 1035 1037	nnncan2d	$⊢ x \in (X + π - (X \mod T), X) \to (X + π) - (X \mod T) - (X - (X \mod T)) = X + π - X$
1039	1038 861	eqtr2di	$⊢ x \in (X + π - (X \mod T), X) \to π = (X + π) - (X \mod T) - (X - (X \mod T))$
1040	1032 767	resubcli	$⊢ X + π - (X \mod T) \in ℝ$
1041	1040	a1i	$⊢ x \in (X + π - (X \mod T), X) \to X + π - (X \mod T) \in ℝ$
1042	768	a1i	$⊢ x \in (X + π - (X \mod T), X) \to X - (X \mod T) \in ℝ$
1043	1040	rexri	$⊢ X + π - (X \mod T) \in ℝ^{*}$
1044	1043	a1i	$⊢ x \in (X + π - (X \mod T), X) \to X + π - (X \mod T) \in ℝ^{*}$
1045	3	a1i	$⊢ x \in (X + π - (X \mod T), X) \to X \in ℝ$
1046	1045	rexrd	$⊢ x \in (X + π - (X \mod T), X) \to X \in ℝ^{*}$
1047		id	$⊢ x \in (X + π - (X \mod T), X) \to x \in (X + π - (X \mod T), X)$
1048		ioogtlb	$⊢ (X + π - (X \mod T) \in ℝ^{} \land X \in ℝ^{} \land x \in (X + π - (X \mod T), X)) \to X + π - (X \mod T) < x$
1049	1044 1046 1047 1048	syl3anc	$⊢ x \in (X + π - (X \mod T), X) \to X + π - (X \mod T) < x$
1050	1041 1025 1042 1049	ltsub1dd	$⊢ x \in (X + π - (X \mod T), X) \to (X + π) - (X \mod T) - (X - (X \mod T)) < x - (X - (X \mod T))$
1051	1039 1050	eqbrtrd	$⊢ x \in (X + π - (X \mod T), X) \to π < x - (X - (X \mod T))$
1052	1025	recnd	$⊢ x \in (X + π - (X \mod T), X) \to x \in ℂ$
1053		sub31	$⊢ (x \in ℂ \land X \in ℂ \land X \mod T \in ℂ) \to x - (X - (X \mod T)) = (X \mod T) - (X - x)$
1054	1052 1035 1037 1053	syl3anc	$⊢ x \in (X + π - (X \mod T), X) \to x - (X - (X \mod T)) = (X \mod T) - (X - x)$
1055	1051 1054	breqtrd	$⊢ x \in (X + π - (X \mod T), X) \to π < (X \mod T) - (X - x)$
1056	1055	adantl	$⊢ (π < X \mod T \land x \in (X + π - (X \mod T), X)) \to π < (X \mod T) - (X - x)$
1057	1045 1025	resubcld	$⊢ x \in (X + π - (X \mod T), X) \to X - x \in ℝ$
1058		0red	$⊢ x \in (X + π - (X \mod T), X) \to 0 \in ℝ$
1059		iooltub	$⊢ (X + π - (X \mod T) \in ℝ^{} \land X \in ℝ^{} \land x \in (X + π - (X \mod T), X)) \to x < X$
1060	1044 1046 1047 1059	syl3anc	$⊢ x \in (X + π - (X \mod T), X) \to x < X$
1061	1025 1045	posdifd	$⊢ x \in (X + π - (X \mod T), X) \to (x < X \leftrightarrow 0 < X - x)$
1062	1060 1061	mpbid	$⊢ x \in (X + π - (X \mod T), X) \to 0 < X - x$
1063	1058 1057 1062	ltled	$⊢ x \in (X + π - (X \mod T), X) \to 0 \leq X - x$
1064	1045 1041	resubcld	$⊢ x \in (X + π - (X \mod T), X) \to X - (X + π - (X \mod T)) \in ℝ$
1065	122	a1i	$⊢ x \in (X + π - (X \mod T), X) \to T \in ℝ$
1066	1041 1025 1045 1049	ltsub2dd	$⊢ x \in (X + π - (X \mod T), X) \to X - x < X - (X + π - (X \mod T))$
1067		sub31	$⊢ (X \in ℂ \land X + π \in ℂ \land X \mod T \in ℂ) \to X - (X + π - (X \mod T)) = (X \mod T) - (X + π - X)$
1068	27 1033 1036 1067	mp3an	$⊢ X - (X + π - (X \mod T)) = (X \mod T) - (X + π - X)$
1069	861	oveq2i	$⊢ (X \mod T) - (X + π - X) = (X \mod T) - π$
1070	1068 1069	eqtri	$⊢ X - (X + π - (X \mod T)) = (X \mod T) - π$
1071		ltsubrp	$⊢ (X \mod T \in ℝ \land π \in ℝ^{+}) \to (X \mod T) - π < X \mod T$
1072	767 184 1071	mp2an	$⊢ (X \mod T) - π < X \mod T$
1073	767 120	resubcli	$⊢ (X \mod T) - π \in ℝ$
1074	1073 767 122	lttri	$⊢ ((X \mod T) - π < X \mod T \land X \mod T < T) \to (X \mod T) - π < T$
1075	1072 962 1074	mp2an	$⊢ (X \mod T) - π < T$
1076	1070 1075	eqbrtri	$⊢ X - (X + π - (X \mod T)) < T$
1077	1076	a1i	$⊢ x \in (X + π - (X \mod T), X) \to X - (X + π - (X \mod T)) < T$
1078	1057 1064 1065 1066 1077	lttrd	$⊢ x \in (X + π - (X \mod T), X) \to X - x < T$
1079		modid	$⊢ ((X - x \in ℝ \land T \in ℝ^{+}) \land (0 \leq X - x \land X - x < T)) \to (X - x) \mod T = X - x$
1080	1057 1029 1063 1078 1079	syl22anc	$⊢ x \in (X + π - (X \mod T), X) \to (X - x) \mod T = X - x$
1081	1080	oveq2d	$⊢ x \in (X + π - (X \mod T), X) \to (X \mod T) - ((X - x) \mod T) = (X \mod T) - (X - x)$
1082	1081	oveq1d	$⊢ x \in (X + π - (X \mod T), X) \to ((X \mod T) - ((X - x) \mod T)) \mod T = ((X \mod T) - (X - x)) \mod T$
1083	767	a1i	$⊢ x \in (X + π - (X \mod T), X) \to X \mod T \in ℝ$
1084	1083 1057	resubcld	$⊢ x \in (X + π - (X \mod T), X) \to (X \mod T) - (X - x) \in ℝ$
1085	120	a1i	$⊢ x \in (X + π - (X \mod T), X) \to π \in ℝ$
1086	1054 1084	eqeltrd	$⊢ x \in (X + π - (X \mod T), X) \to x - (X - (X \mod T)) \in ℝ$
1087	72	a1i	$⊢ x \in (X + π - (X \mod T), X) \to 0 < π$
1088	1058 1085 1086 1087 1051	lttrd	$⊢ x \in (X + π - (X \mod T), X) \to 0 < x - (X - (X \mod T))$
1089	1088 1054	breqtrd	$⊢ x \in (X + π - (X \mod T), X) \to 0 < (X \mod T) - (X - x)$
1090	1058 1084 1089	ltled	$⊢ x \in (X + π - (X \mod T), X) \to 0 \leq (X \mod T) - (X - x)$
1091	1045 1042	resubcld	$⊢ x \in (X + π - (X \mod T), X) \to X - (X - (X \mod T)) \in ℝ$
1092	1025 1045 1042 1060	ltsub1dd	$⊢ x \in (X + π - (X \mod T), X) \to x - (X - (X \mod T)) < X - (X - (X \mod T))$
1093		nncan	$⊢ (X \in ℂ \land X \mod T \in ℂ) \to X - (X - (X \mod T)) = X \mod T$
1094	27 1036 1093	mp2an	$⊢ X - (X - (X \mod T)) = X \mod T$
1095	1094 962	eqbrtri	$⊢ X - (X - (X \mod T)) < T$
1096	1095	a1i	$⊢ x \in (X + π - (X \mod T), X) \to X - (X - (X \mod T)) < T$
1097	1086 1091 1065 1092 1096	lttrd	$⊢ x \in (X + π - (X \mod T), X) \to x - (X - (X \mod T)) < T$
1098	1054 1097	eqbrtrrd	$⊢ x \in (X + π - (X \mod T), X) \to (X \mod T) - (X - x) < T$
1099		modid	$⊢ (((X \mod T) - (X - x) \in ℝ \land T \in ℝ^{+}) \land (0 \leq (X \mod T) - (X - x) \land (X \mod T) - (X - x) < T)) \to ((X \mod T) - (X - x)) \mod T = (X \mod T) - (X - x)$
1100	1084 1029 1090 1098 1099	syl22anc	$⊢ x \in (X + π - (X \mod T), X) \to ((X \mod T) - (X - x)) \mod T = (X \mod T) - (X - x)$
1101	1082 1100	eqtr2d	$⊢ x \in (X + π - (X \mod T), X) \to (X \mod T) - (X - x) = ((X \mod T) - ((X - x) \mod T)) \mod T$
1102		modsubmodmod	$⊢ (X \in ℝ \land X - x \in ℝ \land T \in ℝ^{+}) \to ((X \mod T) - ((X - x) \mod T)) \mod T = (X - (X - x)) \mod T$
1103	1045 1057 1029 1102	syl3anc	$⊢ x \in (X + π - (X \mod T), X) \to ((X \mod T) - ((X - x) \mod T)) \mod T = (X - (X - x)) \mod T$
1104	1035 1052	nncand	$⊢ x \in (X + π - (X \mod T), X) \to X - (X - x) = x$
1105	1104	oveq1d	$⊢ x \in (X + π - (X \mod T), X) \to (X - (X - x)) \mod T = x \mod T$
1106	1101 1103 1105	3eqtrd	$⊢ x \in (X + π - (X \mod T), X) \to (X \mod T) - (X - x) = x \mod T$
1107	1106	adantl	$⊢ (π < X \mod T \land x \in (X + π - (X \mod T), X)) \to (X \mod T) - (X - x) = x \mod T$
1108	1056 1107	breqtrd	$⊢ (π < X \mod T \land x \in (X + π - (X \mod T), X)) \to π < x \mod T$
1109	1019 1108	sylan	$⊢ (X \mod T \in (π, T) \land x \in (X + π - (X \mod T), X)) \to π < x \mod T$
1110	1028 1031 1109	ltled	$⊢ (X \mod T \in (π, T) \land x \in (X + π - (X \mod T), X)) \to π \leq x \mod T$
1111	1028 1031 1110	lensymd	$⊢ (X \mod T \in (π, T) \land x \in (X + π - (X \mod T), X)) \to \neg x \mod T < π$
1112	1111	iffalsed	$⊢ (X \mod T \in (π, T) \land x \in (X + π - (X \mod T), X)) \to if (x \mod T < π, 1, - 1) = - 1$
1113	1027 1112	eqtrd	$⊢ (X \mod T \in (π, T) \land x \in (X + π - (X \mod T), X)) \to F (x) = - 1$
1114	1113	mpteq2dva	$⊢ X \mod T \in (π, T) \to (x \in (X + π - (X \mod T), X) ⟼ F (x)) = (x \in (X + π - (X \mod T), X) ⟼ - 1)$
1115	1024 1114	eqtr2id	$⊢ X \mod T \in (π, T) \to (x \in (X + π - (X \mod T), X) ⟼ - 1) = {F ↾}_{(X + π - (X \mod T), X)}$
1116	1115	oveq1d	$⊢ X \mod T \in (π, T) \to (x \in (X + π - (X \mod T), X) ⟼ - 1) {lim}_{ℂ} X = ({F ↾}_{(X + π - (X \mod T), X)}) {lim}_{ℂ} X$
1117	209	a1i	$⊢ X \mod T \in (π, T) \to F : ℝ ⟶ ℂ$
1118	1043	a1i	$⊢ X \mod T \in (π, T) \to X + π - (X \mod T) \in ℝ^{*}$
1119	3	a1i	$⊢ X \mod T \in (π, T) \to X \in ℝ$
1120		elioore	$⊢ X \mod T \in (π, T) \to X \mod T \in ℝ$
1121		ltaddsublt	$⊢ (X \in ℝ \land π \in ℝ \land X \mod T \in ℝ) \to (π < X \mod T \leftrightarrow X + π - (X \mod T) < X)$
1122	1119 1016 1120 1121	syl3anc	$⊢ X \mod T \in (π, T) \to (π < X \mod T \leftrightarrow X + π - (X \mod T) < X)$
1123	1019 1122	mpbid	$⊢ X \mod T \in (π, T) \to X + π - (X \mod T) < X$
1124	365	a1i	$⊢ X \mod T \in (π, T) \to −∞ \in ℝ^{*}$
1125		mnflt	$⊢ X + π - (X \mod T) \in ℝ \to −∞ < X + π - (X \mod T)$
1126		xrltle	$⊢ (−∞ \in ℝ^{} \land X + π - (X \mod T) \in ℝ^{}) \to (−∞ < X + π - (X \mod T) \to −∞ \leq X + π - (X \mod T))$
1127	365 1043 1126	mp2an	$⊢ −∞ < X + π - (X \mod T) \to −∞ \leq X + π - (X \mod T)$
1128	1040 1125 1127	mp2b	$⊢ −∞ \leq X + π - (X \mod T)$
1129	1128	a1i	$⊢ X \mod T \in (π, T) \to −∞ \leq X + π - (X \mod T)$
1130	1117 1118 1119 1123 1009 1124 1129	limcresiooub	$⊢ X \mod T \in (π, T) \to ({F ↾}_{(X + π - (X \mod T), X)}) {lim}_{ℂ} X = ({F ↾}_{(−∞, X)}) {lim}_{ℂ} X$
1131	1116 1130	eqtr2d	$⊢ X \mod T \in (π, T) \to ({F ↾}_{(−∞, X)}) {lim}_{ℂ} X = (x \in (X + π - (X \mod T), X) ⟼ - 1) {lim}_{ℂ} X$
1132	1014 1021 1131	3eltr4d	$⊢ X \mod T \in (π, T) \to if (X \mod T \in (0, π], 1, - 1) \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
1133	1006 1132	syl	$⊢ (X \mod T \in [π, T) \land \neg X \mod T = π) \to if (X \mod T \in (0, π], 1, - 1) \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
1134	994 1133	pm2.61dan	$⊢ X \mod T \in [π, T) \to if (X \mod T \in (0, π], 1, - 1) \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
1135	964 1134	syl	$⊢ (\neg X \mod T \in (0, π) \land \neg X \mod T = 0) \to if (X \mod T \in (0, π], 1, - 1) \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
1136	932 1135	pm2.61dan	$⊢ \neg X \mod T \in (0, π) \to if (X \mod T \in (0, π], 1, - 1) \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
1137	814 1136	pm2.61i	$⊢ if (X \mod T \in (0, π], 1, - 1) \in (({F ↾}_{(−∞, X)}) {lim}_{ℂ} X)$
1138		eqid	$⊢ (x \in (X, X + π - (X \mod T)) ⟼ 1) = (x \in (X, X + π - (X \mod T)) ⟼ 1)$
1139		ioossre	$⊢ (X, X + π - (X \mod T)) \subseteq ℝ$
1140	1139	a1i	$⊢ ⊤ \to (X, X + π - (X \mod T)) \subseteq ℝ$
1141	1140 207	sstrdi	$⊢ ⊤ \to (X, X + π - (X \mod T)) \subseteq ℂ$
1142	1138 1141 203 819	constlimc	$⊢ ⊤ \to 1 \in ((x \in (X, X + π - (X \mod T)) ⟼ 1) {lim}_{ℂ} X)$
1143	1142	mptru	$⊢ 1 \in ((x \in (X, X + π - (X \mod T)) ⟼ 1) {lim}_{ℂ} X)$
1144	1143	a1i	$⊢ X \mod T \in [0, π) \to 1 \in ((x \in (X, X + π - (X \mod T)) ⟼ 1) {lim}_{ℂ} X)$
1145	2	a1i	$⊢ X \mod T \in [0, π) \to F = (x \in ℝ ⟼ if (x \mod T < π, 1, - 1))$
1146		oveq1	$⊢ x = X \to x \mod T = X \mod T$
1147	1146	breq1d	$⊢ x = X \to (x \mod T < π \leftrightarrow X \mod T < π)$
1148	1147	ifbid	$⊢ x = X \to if (x \mod T < π, 1, - 1) = if (X \mod T < π, 1, - 1)$
1149	1148	adantl	$⊢ (X \mod T \in [0, π) \land x = X) \to if (x \mod T < π, 1, - 1) = if (X \mod T < π, 1, - 1)$
1150	3	a1i	$⊢ X \mod T \in [0, π) \to X \in ℝ$
1151	108 109	ifcli	$⊢ if (X \mod T < π, 1, - 1) \in ℝ$
1152	1151	a1i	$⊢ X \mod T \in [0, π) \to if (X \mod T < π, 1, - 1) \in ℝ$
1153	1145 1149 1150 1152	fvmptd	$⊢ X \mod T \in [0, π) \to F (X) = if (X \mod T < π, 1, - 1)$
1154		icoltub	$⊢ (0 \in ℝ^{} \land π \in ℝ^{} \land X \mod T \in [0, π)) \to X \mod T < π$
1155	153 155 1154	mp3an12	$⊢ X \mod T \in [0, π) \to X \mod T < π$
1156	1155	iftrued	$⊢ X \mod T \in [0, π) \to if (X \mod T < π, 1, - 1) = 1$
1157	1153 1156	eqtrd	$⊢ X \mod T \in [0, π) \to F (X) = 1$
1158	363 1140	feqresmpt	$⊢ ⊤ \to {F ↾}_{(X, X + π - (X \mod T))} = (x \in (X, X + π - (X \mod T)) ⟼ F (x))$
1159	1158	mptru	$⊢ {F ↾}_{(X, X + π - (X \mod T))} = (x \in (X, X + π - (X \mod T)) ⟼ F (x))$
1160		elioore	$⊢ x \in (X, X + π - (X \mod T)) \to x \in ℝ$
1161	1160 110 147	sylancl	$⊢ x \in (X, X + π - (X \mod T)) \to F (x) = if (x \mod T < π, 1, - 1)$
1162	1161	adantl	$⊢ (X \mod T \in [0, π) \land x \in (X, X + π - (X \mod T))) \to F (x) = if (x \mod T < π, 1, - 1)$
1163	3	a1i	$⊢ x \in (X, X + π - (X \mod T)) \to X \in ℝ$
1164	1160 1163	resubcld	$⊢ x \in (X, X + π - (X \mod T)) \to x - X \in ℝ$
1165	135	a1i	$⊢ x \in (X, X + π - (X \mod T)) \to T \in ℝ^{+}$
1166		0red	$⊢ x \in (X, X + π - (X \mod T)) \to 0 \in ℝ$
1167	1163	rexrd	$⊢ x \in (X, X + π - (X \mod T)) \to X \in ℝ^{*}$
1168	120 767	resubcli	$⊢ π - (X \mod T) \in ℝ$
1169	3 1168	readdcli	$⊢ X + π - (X \mod T) \in ℝ$
1170	1169	rexri	$⊢ X + π - (X \mod T) \in ℝ^{*}$
1171	1170	a1i	$⊢ x \in (X, X + π - (X \mod T)) \to X + π - (X \mod T) \in ℝ^{*}$
1172		id	$⊢ x \in (X, X + π - (X \mod T)) \to x \in (X, X + π - (X \mod T))$
1173		ioogtlb	$⊢ (X \in ℝ^{} \land X + π - (X \mod T) \in ℝ^{} \land x \in (X, X + π - (X \mod T))) \to X < x$
1174	1167 1171 1172 1173	syl3anc	$⊢ x \in (X, X + π - (X \mod T)) \to X < x$
1175	1163 1160	posdifd	$⊢ x \in (X, X + π - (X \mod T)) \to (X < x \leftrightarrow 0 < x - X)$
1176	1174 1175	mpbid	$⊢ x \in (X, X + π - (X \mod T)) \to 0 < x - X$
1177	1166 1164 1176	ltled	$⊢ x \in (X, X + π - (X \mod T)) \to 0 \leq x - X$
1178	120	a1i	$⊢ x \in (X, X + π - (X \mod T)) \to π \in ℝ$
1179	122	a1i	$⊢ x \in (X, X + π - (X \mod T)) \to T \in ℝ$
1180	1169	a1i	$⊢ x \in (X, X + π - (X \mod T)) \to X + π - (X \mod T) \in ℝ$
1181	1180 1163	resubcld	$⊢ x \in (X, X + π - (X \mod T)) \to X + (π - (X \mod T)) - X \in ℝ$
1182		iooltub	$⊢ (X \in ℝ^{} \land X + π - (X \mod T) \in ℝ^{} \land x \in (X, X + π - (X \mod T))) \to x < X + π - (X \mod T)$
1183	1167 1171 1172 1182	syl3anc	$⊢ x \in (X, X + π - (X \mod T)) \to x < X + π - (X \mod T)$
1184	1160 1180 1163 1183	ltsub1dd	$⊢ x \in (X, X + π - (X \mod T)) \to x - X < X + (π - (X \mod T)) - X$
1185	1168	recni	$⊢ π - (X \mod T) \in ℂ$
1186		pncan2	$⊢ (X \in ℂ \land π - (X \mod T) \in ℂ) \to X + (π - (X \mod T)) - X = π - (X \mod T)$
1187	27 1185 1186	mp2an	$⊢ X + (π - (X \mod T)) - X = π - (X \mod T)$
1188		subge02	$⊢ (π \in ℝ \land X \mod T \in ℝ) \to (0 \leq X \mod T \leftrightarrow π - (X \mod T) \leq π)$
1189	120 767 1188	mp2an	$⊢ 0 \leq X \mod T \leftrightarrow π - (X \mod T) \leq π$
1190	950 1189	mpbi	$⊢ π - (X \mod T) \leq π$
1191	1187 1190	eqbrtri	$⊢ X + (π - (X \mod T)) - X \leq π$
1192	1191	a1i	$⊢ x \in (X, X + π - (X \mod T)) \to X + (π - (X \mod T)) - X \leq π$
1193	1164 1181 1178 1184 1192	ltletrd	$⊢ x \in (X, X + π - (X \mod T)) \to x - X < π$
1194	187	a1i	$⊢ x \in (X, X + π - (X \mod T)) \to π < T$
1195	1164 1178 1179 1193 1194	lttrd	$⊢ x \in (X, X + π - (X \mod T)) \to x - X < T$
1196		modid	$⊢ ((x - X \in ℝ \land T \in ℝ^{+}) \land (0 \leq x - X \land x - X < T)) \to (x - X) \mod T = x - X$
1197	1164 1165 1177 1195 1196	syl22anc	$⊢ x \in (X, X + π - (X \mod T)) \to (x - X) \mod T = x - X$
1198	1197	oveq2d	$⊢ x \in (X, X + π - (X \mod T)) \to (X \mod T) + ((x - X) \mod T) = (X \mod T) + x - X$
1199	1198	oveq1d	$⊢ x \in (X, X + π - (X \mod T)) \to ((X \mod T) + ((x - X) \mod T)) \mod T = ((X \mod T) + x - X) \mod T$
1200	767	a1i	$⊢ x \in (X, X + π - (X \mod T)) \to X \mod T \in ℝ$
1201	1200 1164	readdcld	$⊢ x \in (X, X + π - (X \mod T)) \to (X \mod T) + x - X \in ℝ$
1202	1163 1163	resubcld	$⊢ x \in (X, X + π - (X \mod T)) \to X - X \in ℝ$
1203	1200 1202	readdcld	$⊢ x \in (X, X + π - (X \mod T)) \to (X \mod T) + X - X \in ℝ$
1204	27	subidi	$⊢ X - X = 0$
1205	1204	oveq2i	$⊢ (X \mod T) + X - X = (X \mod T) + 0$
1206	1036	addridi	$⊢ (X \mod T) + 0 = X \mod T$
1207	1205 1206	eqtr2i	$⊢ X \mod T = (X \mod T) + X - X$
1208	950 1207	breqtri	$⊢ 0 \leq (X \mod T) + X - X$
1209	1208	a1i	$⊢ x \in (X, X + π - (X \mod T)) \to 0 \leq (X \mod T) + X - X$
1210	1163 1160 1163 1174	ltsub1dd	$⊢ x \in (X, X + π - (X \mod T)) \to X - X < x - X$
1211	1202 1164 1200 1210	ltadd2dd	$⊢ x \in (X, X + π - (X \mod T)) \to (X \mod T) + X - X < (X \mod T) + x - X$
1212	1166 1203 1201 1209 1211	lelttrd	$⊢ x \in (X, X + π - (X \mod T)) \to 0 < (X \mod T) + x - X$
1213	1166 1201 1212	ltled	$⊢ x \in (X, X + π - (X \mod T)) \to 0 \leq (X \mod T) + x - X$
1214	1164 1181 1200 1184	ltadd2dd	$⊢ x \in (X, X + π - (X \mod T)) \to (X \mod T) + x - X < (X \mod T) + (X + π - (X \mod T)) - X$
1215	1187	oveq2i	$⊢ (X \mod T) + (X + π - (X \mod T)) - X = (X \mod T) + π - (X \mod T)$
1216	1036 56	pncan3i	$⊢ (X \mod T) + π - (X \mod T) = π$
1217	1215 1216	eqtri	$⊢ (X \mod T) + (X + π - (X \mod T)) - X = π$
1218	1214 1217	breqtrdi	$⊢ x \in (X, X + π - (X \mod T)) \to (X \mod T) + x - X < π$
1219	1201 1178 1179 1218 1194	lttrd	$⊢ x \in (X, X + π - (X \mod T)) \to (X \mod T) + x - X < T$
1220		modid	$⊢ (((X \mod T) + x - X \in ℝ \land T \in ℝ^{+}) \land (0 \leq (X \mod T) + x - X \land (X \mod T) + x - X < T)) \to ((X \mod T) + x - X) \mod T = (X \mod T) + x - X$
1221	1201 1165 1213 1219 1220	syl22anc	$⊢ x \in (X, X + π - (X \mod T)) \to ((X \mod T) + x - X) \mod T = (X \mod T) + x - X$
1222	1199 1221	eqtr2d	$⊢ x \in (X, X + π - (X \mod T)) \to (X \mod T) + x - X = ((X \mod T) + ((x - X) \mod T)) \mod T$
1223		modaddabs	$⊢ (X \in ℝ \land x - X \in ℝ \land T \in ℝ^{+}) \to ((X \mod T) + ((x - X) \mod T)) \mod T = (X + x - X) \mod T$
1224	1163 1164 1165 1223	syl3anc	$⊢ x \in (X, X + π - (X \mod T)) \to ((X \mod T) + ((x - X) \mod T)) \mod T = (X + x - X) \mod T$
1225	27	a1i	$⊢ x \in (X, X + π - (X \mod T)) \to X \in ℂ$
1226	1160	recnd	$⊢ x \in (X, X + π - (X \mod T)) \to x \in ℂ$
1227	1225 1226	pncan3d	$⊢ x \in (X, X + π - (X \mod T)) \to X + x - X = x$
1228	1227	oveq1d	$⊢ x \in (X, X + π - (X \mod T)) \to (X + x - X) \mod T = x \mod T$
1229	1222 1224 1228	3eqtrrd	$⊢ x \in (X, X + π - (X \mod T)) \to x \mod T = (X \mod T) + x - X$
1230	1229	adantl	$⊢ (X \mod T < π \land x \in (X, X + π - (X \mod T))) \to x \mod T = (X \mod T) + x - X$
1231	1218	adantl	$⊢ (X \mod T < π \land x \in (X, X + π - (X \mod T))) \to (X \mod T) + x - X < π$
1232	1230 1231	eqbrtrd	$⊢ (X \mod T < π \land x \in (X, X + π - (X \mod T))) \to x \mod T < π$
1233	1155 1232	sylan	$⊢ (X \mod T \in [0, π) \land x \in (X, X + π - (X \mod T))) \to x \mod T < π$
1234	1233	iftrued	$⊢ (X \mod T \in [0, π) \land x \in (X, X + π - (X \mod T))) \to if (x \mod T < π, 1, - 1) = 1$
1235	1162 1234	eqtrd	$⊢ (X \mod T \in [0, π) \land x \in (X, X + π - (X \mod T))) \to F (x) = 1$
1236	1235	mpteq2dva	$⊢ X \mod T \in [0, π) \to (x \in (X, X + π - (X \mod T)) ⟼ F (x)) = (x \in (X, X + π - (X \mod T)) ⟼ 1)$
1237	1159 1236	eqtr2id	$⊢ X \mod T \in [0, π) \to (x \in (X, X + π - (X \mod T)) ⟼ 1) = {F ↾}_{(X, X + π - (X \mod T))}$
1238	1237	oveq1d	$⊢ X \mod T \in [0, π) \to (x \in (X, X + π - (X \mod T)) ⟼ 1) {lim}_{ℂ} X = ({F ↾}_{(X, X + π - (X \mod T))}) {lim}_{ℂ} X$
1239	209	a1i	$⊢ X \mod T \in [0, π) \to F : ℝ ⟶ ℂ$
1240	1170	a1i	$⊢ X \mod T \in [0, π) \to X + π - (X \mod T) \in ℝ^{*}$
1241	1168	a1i	$⊢ X \mod T \in [0, π) \to π - (X \mod T) \in ℝ$
1242	767	a1i	$⊢ X \mod T \in [0, π) \to X \mod T \in ℝ$
1243	120	a1i	$⊢ X \mod T \in [0, π) \to π \in ℝ$
1244	1242 1243	posdifd	$⊢ X \mod T \in [0, π) \to (X \mod T < π \leftrightarrow 0 < π - (X \mod T))$
1245	1155 1244	mpbid	$⊢ X \mod T \in [0, π) \to 0 < π - (X \mod T)$
1246	1241 1245	elrpd	$⊢ X \mod T \in [0, π) \to π - (X \mod T) \in ℝ^{+}$
1247	1150 1246	ltaddrpd	$⊢ X \mod T \in [0, π) \to X < X + π - (X \mod T)$
1248	1139	a1i	$⊢ X \mod T \in [0, π) \to (X, X + π - (X \mod T)) \subseteq ℝ$
1249	376	a1i	$⊢ X \mod T \in [0, π) \to +∞ \in ℝ^{*}$
1250		ltpnf	$⊢ X + π - (X \mod T) \in ℝ \to X + π - (X \mod T) < +∞$
1251		xrltle	$⊢ (X + π - (X \mod T) \in ℝ^{} \land +∞ \in ℝ^{}) \to (X + π - (X \mod T) < +∞ \to X + π - (X \mod T) \leq +∞)$
1252	1170 376 1251	mp2an	$⊢ X + π - (X \mod T) < +∞ \to X + π - (X \mod T) \leq +∞$
1253	1169 1250 1252	mp2b	$⊢ X + π - (X \mod T) \leq +∞$
1254	1253	a1i	$⊢ X \mod T \in [0, π) \to X + π - (X \mod T) \leq +∞$
1255	1239 1150 1240 1247 1248 1249 1254	limcresioolb	$⊢ X \mod T \in [0, π) \to ({F ↾}_{(X, X + π - (X \mod T))}) {lim}_{ℂ} X = ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X$
1256	1238 1255	eqtr2d	$⊢ X \mod T \in [0, π) \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X = (x \in (X, X + π - (X \mod T)) ⟼ 1) {lim}_{ℂ} X$
1257	1144 1157 1256	3eltr4d	$⊢ X \mod T \in [0, π) \to F (X) \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
1258	155	a1i	$⊢ \neg X \mod T \in [0, π) \to π \in ℝ^{*}$
1259	934	a1i	$⊢ \neg X \mod T \in [0, π) \to T \in ℝ^{*}$
1260	936	a1i	$⊢ \neg X \mod T \in [0, π) \to X \mod T \in ℝ^{*}$
1261	153	a1i	$⊢ (\neg X \mod T \in [0, π) \land \neg π \leq X \mod T) \to 0 \in ℝ^{*}$
1262	155	a1i	$⊢ (\neg X \mod T \in [0, π) \land \neg π \leq X \mod T) \to π \in ℝ^{*}$
1263	936	a1i	$⊢ (\neg X \mod T \in [0, π) \land \neg π \leq X \mod T) \to X \mod T \in ℝ^{*}$
1264	950	a1i	$⊢ (\neg X \mod T \in [0, π) \land \neg π \leq X \mod T) \to 0 \leq X \mod T$
1265	767	a1i	$⊢ \neg π \leq X \mod T \to X \mod T \in ℝ$
1266	120	a1i	$⊢ \neg π \leq X \mod T \to π \in ℝ$
1267	1265 1266	ltnled	$⊢ \neg π \leq X \mod T \to (X \mod T < π \leftrightarrow \neg π \leq X \mod T)$
1268	1267	ibir	$⊢ \neg π \leq X \mod T \to X \mod T < π$
1269	1268	adantl	$⊢ (\neg X \mod T \in [0, π) \land \neg π \leq X \mod T) \to X \mod T < π$
1270	1261 1262 1263 1264 1269	elicod	$⊢ (\neg X \mod T \in [0, π) \land \neg π \leq X \mod T) \to X \mod T \in [0, π)$
1271		simpl	$⊢ (\neg X \mod T \in [0, π) \land \neg π \leq X \mod T) \to \neg X \mod T \in [0, π)$
1272	1270 1271	condan	$⊢ \neg X \mod T \in [0, π) \to π \leq X \mod T$
1273	962	a1i	$⊢ \neg X \mod T \in [0, π) \to X \mod T < T$
1274	1258 1259 1260 1272 1273	elicod	$⊢ \neg X \mod T \in [0, π) \to X \mod T \in [π, T)$
1275		eqid	$⊢ (x \in (X, X + T - (X \mod T)) ⟼ - 1) = (x \in (X, X + T - (X \mod T)) ⟼ - 1)$
1276		ioossre	$⊢ (X, X + T - (X \mod T)) \subseteq ℝ$
1277	1276	a1i	$⊢ ⊤ \to (X, X + T - (X \mod T)) \subseteq ℝ$
1278	1277 207	sstrdi	$⊢ ⊤ \to (X, X + T - (X \mod T)) \subseteq ℂ$
1279	1275 1278 305 819	constlimc	$⊢ ⊤ \to - 1 \in ((x \in (X, X + T - (X \mod T)) ⟼ - 1) {lim}_{ℂ} X)$
1280	1279	mptru	$⊢ - 1 \in ((x \in (X, X + T - (X \mod T)) ⟼ - 1) {lim}_{ℂ} X)$
1281	1280	a1i	$⊢ X \mod T \in [π, T) \to - 1 \in ((x \in (X, X + T - (X \mod T)) ⟼ - 1) {lim}_{ℂ} X)$
1282		1ex	$⊢ 1 \in V$
1283	109	elexi	$⊢ - 1 \in V$
1284	1282 1283	ifex	$⊢ if (X \mod T < π, 1, - 1) \in V$
1285	1148 2 1284	fvmpt	$⊢ X \in ℝ \to F (X) = if (X \mod T < π, 1, - 1)$
1286	3 1285	ax-mp	$⊢ F (X) = if (X \mod T < π, 1, - 1)$
1287	1286	a1i	$⊢ X \mod T \in [π, T) \to F (X) = if (X \mod T < π, 1, - 1)$
1288	120	a1i	$⊢ X \mod T \in [π, T) \to π \in ℝ$
1289	767	a1i	$⊢ X \mod T \in [π, T) \to X \mod T \in ℝ$
1290	1288 1289 1000	lensymd	$⊢ X \mod T \in [π, T) \to \neg X \mod T < π$
1291	1290	iffalsed	$⊢ X \mod T \in [π, T) \to if (X \mod T < π, 1, - 1) = - 1$
1292	1287 1291	eqtrd	$⊢ X \mod T \in [π, T) \to F (X) = - 1$
1293	363 1277	feqresmpt	$⊢ ⊤ \to {F ↾}_{(X, X + T - (X \mod T))} = (x \in (X, X + T - (X \mod T)) ⟼ F (x))$
1294	1293	mptru	$⊢ {F ↾}_{(X, X + T - (X \mod T))} = (x \in (X, X + T - (X \mod T)) ⟼ F (x))$
1295		elioore	$⊢ x \in (X, X + T - (X \mod T)) \to x \in ℝ$
1296	1295 110 147	sylancl	$⊢ x \in (X, X + T - (X \mod T)) \to F (x) = if (x \mod T < π, 1, - 1)$
1297	1296	adantl	$⊢ (X \mod T \in [π, T) \land x \in (X, X + T - (X \mod T))) \to F (x) = if (x \mod T < π, 1, - 1)$
1298	120	a1i	$⊢ (X \mod T \in [π, T) \land x \in (X, X + T - (X \mod T))) \to π \in ℝ$
1299	3	a1i	$⊢ x \in (X, X + T - (X \mod T)) \to X \in ℝ$
1300	1295 1299	resubcld	$⊢ x \in (X, X + T - (X \mod T)) \to x - X \in ℝ$
1301	135	a1i	$⊢ x \in (X, X + T - (X \mod T)) \to T \in ℝ^{+}$
1302		0red	$⊢ x \in (X, X + T - (X \mod T)) \to 0 \in ℝ$
1303	1299	rexrd	$⊢ x \in (X, X + T - (X \mod T)) \to X \in ℝ^{*}$
1304	122 767	resubcli	$⊢ T - (X \mod T) \in ℝ$
1305	3 1304	readdcli	$⊢ X + T - (X \mod T) \in ℝ$
1306	1305	rexri	$⊢ X + T - (X \mod T) \in ℝ^{*}$
1307	1306	a1i	$⊢ x \in (X, X + T - (X \mod T)) \to X + T - (X \mod T) \in ℝ^{*}$
1308		id	$⊢ x \in (X, X + T - (X \mod T)) \to x \in (X, X + T - (X \mod T))$
1309		ioogtlb	$⊢ (X \in ℝ^{} \land X + T - (X \mod T) \in ℝ^{} \land x \in (X, X + T - (X \mod T))) \to X < x$
1310	1303 1307 1308 1309	syl3anc	$⊢ x \in (X, X + T - (X \mod T)) \to X < x$
1311	1299 1295	posdifd	$⊢ x \in (X, X + T - (X \mod T)) \to (X < x \leftrightarrow 0 < x - X)$
1312	1310 1311	mpbid	$⊢ x \in (X, X + T - (X \mod T)) \to 0 < x - X$
1313	1302 1300 1312	ltled	$⊢ x \in (X, X + T - (X \mod T)) \to 0 \leq x - X$
1314	1305	a1i	$⊢ x \in (X, X + T - (X \mod T)) \to X + T - (X \mod T) \in ℝ$
1315	1314 1299	resubcld	$⊢ x \in (X, X + T - (X \mod T)) \to X + (T - (X \mod T)) - X \in ℝ$
1316	122	a1i	$⊢ x \in (X, X + T - (X \mod T)) \to T \in ℝ$
1317		iooltub	$⊢ (X \in ℝ^{} \land X + T - (X \mod T) \in ℝ^{} \land x \in (X, X + T - (X \mod T))) \to x < X + T - (X \mod T)$
1318	1303 1307 1308 1317	syl3anc	$⊢ x \in (X, X + T - (X \mod T)) \to x < X + T - (X \mod T)$
1319	1295 1314 1299 1318	ltsub1dd	$⊢ x \in (X, X + T - (X \mod T)) \to x - X < X + (T - (X \mod T)) - X$
1320	1304	recni	$⊢ T - (X \mod T) \in ℂ$
1321		pncan2	$⊢ (X \in ℂ \land T - (X \mod T) \in ℂ) \to X + (T - (X \mod T)) - X = T - (X \mod T)$
1322	27 1320 1321	mp2an	$⊢ X + (T - (X \mod T)) - X = T - (X \mod T)$
1323		subge02	$⊢ (T \in ℝ \land X \mod T \in ℝ) \to (0 \leq X \mod T \leftrightarrow T - (X \mod T) \leq T)$
1324	122 767 1323	mp2an	$⊢ 0 \leq X \mod T \leftrightarrow T - (X \mod T) \leq T$
1325	950 1324	mpbi	$⊢ T - (X \mod T) \leq T$
1326	1322 1325	eqbrtri	$⊢ X + (T - (X \mod T)) - X \leq T$
1327	1326	a1i	$⊢ x \in (X, X + T - (X \mod T)) \to X + (T - (X \mod T)) - X \leq T$
1328	1300 1315 1316 1319 1327	ltletrd	$⊢ x \in (X, X + T - (X \mod T)) \to x - X < T$
1329	1300 1301 1313 1328 1196	syl22anc	$⊢ x \in (X, X + T - (X \mod T)) \to (x - X) \mod T = x - X$
1330	1329	oveq2d	$⊢ x \in (X, X + T - (X \mod T)) \to (X \mod T) + ((x - X) \mod T) = (X \mod T) + x - X$
1331	1330	oveq1d	$⊢ x \in (X, X + T - (X \mod T)) \to ((X \mod T) + ((x - X) \mod T)) \mod T = ((X \mod T) + x - X) \mod T$
1332		readdcl	$⊢ (X \mod T \in ℝ \land x - X \in ℝ) \to (X \mod T) + x - X \in ℝ$
1333	767 1300 1332	sylancr	$⊢ x \in (X, X + T - (X \mod T)) \to (X \mod T) + x - X \in ℝ$
1334	767	a1i	$⊢ x \in (X, X + T - (X \mod T)) \to X \mod T \in ℝ$
1335	950	a1i	$⊢ x \in (X, X + T - (X \mod T)) \to 0 \leq X \mod T$
1336	1334 1300 1335 1312	addgegt0d	$⊢ x \in (X, X + T - (X \mod T)) \to 0 < (X \mod T) + x - X$
1337	1302 1333 1336	ltled	$⊢ x \in (X, X + T - (X \mod T)) \to 0 \leq (X \mod T) + x - X$
1338	1300 1315 1334 1319	ltadd2dd	$⊢ x \in (X, X + T - (X \mod T)) \to (X \mod T) + x - X < (X \mod T) + (X + T - (X \mod T)) - X$
1339	1322	oveq2i	$⊢ (X \mod T) + (X + T - (X \mod T)) - X = (X \mod T) + T - (X \mod T)$
1340	1036 123	pncan3i	$⊢ (X \mod T) + T - (X \mod T) = T$
1341	1339 1340	eqtri	$⊢ (X \mod T) + (X + T - (X \mod T)) - X = T$
1342	1338 1341	breqtrdi	$⊢ x \in (X, X + T - (X \mod T)) \to (X \mod T) + x - X < T$
1343	1333 1301 1337 1342 1220	syl22anc	$⊢ x \in (X, X + T - (X \mod T)) \to ((X \mod T) + x - X) \mod T = (X \mod T) + x - X$
1344	1331 1343	eqtr2d	$⊢ x \in (X, X + T - (X \mod T)) \to (X \mod T) + x - X = ((X \mod T) + ((x - X) \mod T)) \mod T$
1345	1299 1300 1301 1223	syl3anc	$⊢ x \in (X, X + T - (X \mod T)) \to ((X \mod T) + ((x - X) \mod T)) \mod T = (X + x - X) \mod T$
1346	27	a1i	$⊢ x \in (X, X + T - (X \mod T)) \to X \in ℂ$
1347	1295	recnd	$⊢ x \in (X, X + T - (X \mod T)) \to x \in ℂ$
1348	1346 1347	pncan3d	$⊢ x \in (X, X + T - (X \mod T)) \to X + x - X = x$
1349	1348	oveq1d	$⊢ x \in (X, X + T - (X \mod T)) \to (X + x - X) \mod T = x \mod T$
1350	1344 1345 1349	3eqtrd	$⊢ x \in (X, X + T - (X \mod T)) \to (X \mod T) + x - X = x \mod T$
1351	1350	adantl	$⊢ (X \mod T \in [π, T) \land x \in (X, X + T - (X \mod T))) \to (X \mod T) + x - X = x \mod T$
1352	1333	adantl	$⊢ (X \mod T \in [π, T) \land x \in (X, X + T - (X \mod T))) \to (X \mod T) + x - X \in ℝ$
1353	1351 1352	eqeltrrd	$⊢ (X \mod T \in [π, T) \land x \in (X, X + T - (X \mod T))) \to x \mod T \in ℝ$
1354	767	a1i	$⊢ (X \mod T \in [π, T) \land x \in (X, X + T - (X \mod T))) \to X \mod T \in ℝ$
1355	1000	adantr	$⊢ (X \mod T \in [π, T) \land x \in (X, X + T - (X \mod T))) \to π \leq X \mod T$
1356	1300 1312	elrpd	$⊢ x \in (X, X + T - (X \mod T)) \to x - X \in ℝ^{+}$
1357	1334 1356	ltaddrpd	$⊢ x \in (X, X + T - (X \mod T)) \to X \mod T < (X \mod T) + x - X$
1358	1357	adantl	$⊢ (X \mod T \in [π, T) \land x \in (X, X + T - (X \mod T))) \to X \mod T < (X \mod T) + x - X$
1359	1298 1354 1352 1355 1358	lelttrd	$⊢ (X \mod T \in [π, T) \land x \in (X, X + T - (X \mod T))) \to π < (X \mod T) + x - X$
1360	1298 1352 1359	ltled	$⊢ (X \mod T \in [π, T) \land x \in (X, X + T - (X \mod T))) \to π \leq (X \mod T) + x - X$
1361	1360 1351	breqtrd	$⊢ (X \mod T \in [π, T) \land x \in (X, X + T - (X \mod T))) \to π \leq x \mod T$
1362	1298 1353 1361	lensymd	$⊢ (X \mod T \in [π, T) \land x \in (X, X + T - (X \mod T))) \to \neg x \mod T < π$
1363	1362	iffalsed	$⊢ (X \mod T \in [π, T) \land x \in (X, X + T - (X \mod T))) \to if (x \mod T < π, 1, - 1) = - 1$
1364	1297 1363	eqtrd	$⊢ (X \mod T \in [π, T) \land x \in (X, X + T - (X \mod T))) \to F (x) = - 1$
1365	1364	mpteq2dva	$⊢ X \mod T \in [π, T) \to (x \in (X, X + T - (X \mod T)) ⟼ F (x)) = (x \in (X, X + T - (X \mod T)) ⟼ - 1)$
1366	1294 1365	eqtr2id	$⊢ X \mod T \in [π, T) \to (x \in (X, X + T - (X \mod T)) ⟼ - 1) = {F ↾}_{(X, X + T - (X \mod T))}$
1367	1366	oveq1d	$⊢ X \mod T \in [π, T) \to (x \in (X, X + T - (X \mod T)) ⟼ - 1) {lim}_{ℂ} X = ({F ↾}_{(X, X + T - (X \mod T))}) {lim}_{ℂ} X$
1368	209	a1i	$⊢ X \mod T \in [π, T) \to F : ℝ ⟶ ℂ$
1369	3	a1i	$⊢ X \mod T \in [π, T) \to X \in ℝ$
1370	1306	a1i	$⊢ X \mod T \in [π, T) \to X + T - (X \mod T) \in ℝ^{*}$
1371	1304	a1i	$⊢ X \mod T \in [π, T) \to T - (X \mod T) \in ℝ$
1372	962	a1i	$⊢ X \mod T \in [π, T) \to X \mod T < T$
1373	122	a1i	$⊢ X \mod T \in [π, T) \to T \in ℝ$
1374	1289 1373	posdifd	$⊢ X \mod T \in [π, T) \to (X \mod T < T \leftrightarrow 0 < T - (X \mod T))$
1375	1372 1374	mpbid	$⊢ X \mod T \in [π, T) \to 0 < T - (X \mod T)$
1376	1371 1375	elrpd	$⊢ X \mod T \in [π, T) \to T - (X \mod T) \in ℝ^{+}$
1377	1369 1376	ltaddrpd	$⊢ X \mod T \in [π, T) \to X < X + T - (X \mod T)$
1378	1276	a1i	$⊢ X \mod T \in [π, T) \to (X, X + T - (X \mod T)) \subseteq ℝ$
1379	376	a1i	$⊢ X \mod T \in [π, T) \to +∞ \in ℝ^{*}$
1380		ltpnf	$⊢ X + T - (X \mod T) \in ℝ \to X + T - (X \mod T) < +∞$
1381		xrltle	$⊢ (X + T - (X \mod T) \in ℝ^{} \land +∞ \in ℝ^{}) \to (X + T - (X \mod T) < +∞ \to X + T - (X \mod T) \leq +∞)$
1382	1306 376 1381	mp2an	$⊢ X + T - (X \mod T) < +∞ \to X + T - (X \mod T) \leq +∞$
1383	1305 1380 1382	mp2b	$⊢ X + T - (X \mod T) \leq +∞$
1384	1383	a1i	$⊢ X \mod T \in [π, T) \to X + T - (X \mod T) \leq +∞$
1385	1368 1369 1370 1377 1378 1379 1384	limcresioolb	$⊢ X \mod T \in [π, T) \to ({F ↾}_{(X, X + T - (X \mod T))}) {lim}_{ℂ} X = ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X$
1386	1367 1385	eqtr2d	$⊢ X \mod T \in [π, T) \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X = (x \in (X, X + T - (X \mod T)) ⟼ - 1) {lim}_{ℂ} X$
1387	1281 1292 1386	3eltr4d	$⊢ X \mod T \in [π, T) \to F (X) \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
1388	1274 1387	syl	$⊢ \neg X \mod T \in [0, π) \to F (X) \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
1389	1257 1388	pm2.61i	$⊢ F (X) \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
1390		id	$⊢ n \in ℕ_{0} \to n \in ℕ_{0}$
1391	1 2 1390	sqwvfoura	$⊢ n \in ℕ_{0} \to \frac{\int_{(- π, π)} F (x) \cos n x d x}{π} = 0$
1392	1391	eqcomd	$⊢ n \in ℕ_{0} \to 0 = \frac{\int_{(- π, π)} F (x) \cos n x d x}{π}$
1393	1392	mpteq2ia	$⊢ (n \in ℕ_{0} ⟼ 0) = (n \in ℕ_{0} ⟼ \frac{\int_{(- π, π)} F (x) \cos n x d x}{π})$
1394		id	$⊢ n \in ℕ \to n \in ℕ$
1395	1 2 1394	sqwvfourb	$⊢ n \in ℕ \to \frac{\int_{(- π, π)} F (x) \sin n x d x}{π} = if (2 ∥ n, 0, \frac{4}{n π})$
1396	1395	eqcomd	$⊢ n \in ℕ \to if (2 ∥ n, 0, \frac{4}{n π}) = \frac{\int_{(- π, π)} F (x) \sin n x d x}{π}$
1397	1396	mpteq2ia	$⊢ (n \in ℕ ⟼ if (2 ∥ n, 0, \frac{4}{n π})) = (n \in ℕ ⟼ \frac{\int_{(- π, π)} F (x) \sin n x d x}{π})$
1398		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
1399		0red	$⊢ n \in ℕ \to 0 \in ℝ$
1400		eqid	$⊢ (n \in ℕ_{0} ⟼ 0) = (n \in ℕ_{0} ⟼ 0)$
1401	1400	fvmpt2	$⊢ (n \in ℕ_{0} \land 0 \in ℝ) \to (n \in ℕ_{0} ⟼ 0) (n) = 0$
1402	1398 1399 1401	syl2anc	$⊢ n \in ℕ \to (n \in ℕ_{0} ⟼ 0) (n) = 0$
1403	1402	oveq1d	$⊢ n \in ℕ \to (n \in ℕ_{0} ⟼ 0) (n) \cos n X = 0 \cdot \cos n X$
1404	78	coscld	$⊢ n \in ℕ \to \cos n X \in ℂ$
1405	1404	mul02d	$⊢ n \in ℕ \to 0 \cdot \cos n X = 0$
1406	1403 1405	eqtrd	$⊢ n \in ℕ \to (n \in ℕ_{0} ⟼ 0) (n) \cos n X = 0$
1407		ovex	$⊢ \frac{4}{n π} \in V$
1408	93 1407	ifex	$⊢ if (2 ∥ n, 0, \frac{4}{n π}) \in V$
1409		eqid	$⊢ (n \in ℕ ⟼ if (2 ∥ n, 0, \frac{4}{n π})) = (n \in ℕ ⟼ if (2 ∥ n, 0, \frac{4}{n π}))$
1410	1409	fvmpt2	$⊢ (n \in ℕ \land if (2 ∥ n, 0, \frac{4}{n π}) \in V) \to (n \in ℕ ⟼ if (2 ∥ n, 0, \frac{4}{n π})) (n) = if (2 ∥ n, 0, \frac{4}{n π})$
1411	1408 1410	mpan2	$⊢ n \in ℕ \to (n \in ℕ ⟼ if (2 ∥ n, 0, \frac{4}{n π})) (n) = if (2 ∥ n, 0, \frac{4}{n π})$
1412	1411	oveq1d	$⊢ n \in ℕ \to (n \in ℕ ⟼ if (2 ∥ n, 0, \frac{4}{n π})) (n) \sin n X = if (2 ∥ n, 0, \frac{4}{n π}) \sin n X$
1413	1406 1412	oveq12d	$⊢ n \in ℕ \to (n \in ℕ_{0} ⟼ 0) (n) \cos n X + (n \in ℕ ⟼ if (2 ∥ n, 0, \frac{4}{n π})) (n) \sin n X = 0 + if (2 ∥ n, 0, \frac{4}{n π}) \sin n X$
1414	64 76	ifcld	$⊢ n \in ℕ \to if (2 ∥ n, 0, \frac{4}{n π}) \in ℂ$
1415	1414 79	mulcld	$⊢ n \in ℕ \to if (2 ∥ n, 0, \frac{4}{n π}) \sin n X \in ℂ$
1416	1415	addlidd	$⊢ n \in ℕ \to 0 + if (2 ∥ n, 0, \frac{4}{n π}) \sin n X = if (2 ∥ n, 0, \frac{4}{n π}) \sin n X$
1417		iftrue	$⊢ 2 ∥ n \to if (2 ∥ n, 0, \frac{4}{n π}) = 0$
1418	1417	oveq1d	$⊢ 2 ∥ n \to if (2 ∥ n, 0, \frac{4}{n π}) \sin n X = 0 \cdot \sin n X$
1419	79	mul02d	$⊢ n \in ℕ \to 0 \cdot \sin n X = 0$
1420	1418 1419	sylan9eqr	$⊢ (n \in ℕ \land 2 ∥ n) \to if (2 ∥ n, 0, \frac{4}{n π}) \sin n X = 0$
1421		iftrue	$⊢ 2 ∥ n \to if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X) = 0$
1422	1421	eqcomd	$⊢ 2 ∥ n \to 0 = if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)$
1423	1422	adantl	$⊢ (n \in ℕ \land 2 ∥ n) \to 0 = if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)$
1424	1420 1423	eqtrd	$⊢ (n \in ℕ \land 2 ∥ n) \to if (2 ∥ n, 0, \frac{4}{n π}) \sin n X = if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)$
1425		iffalse	$⊢ \neg 2 ∥ n \to if (2 ∥ n, 0, \frac{4}{n π}) = \frac{4}{n π}$
1426	1425	oveq1d	$⊢ \neg 2 ∥ n \to if (2 ∥ n, 0, \frac{4}{n π}) \sin n X = (\frac{4}{n π}) \sin n X$
1427	1426	adantl	$⊢ (n \in ℕ \land \neg 2 ∥ n) \to if (2 ∥ n, 0, \frac{4}{n π}) \sin n X = (\frac{4}{n π}) \sin n X$
1428		iffalse	$⊢ \neg 2 ∥ n \to if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X) = (\frac{4}{n π}) \sin n X$
1429	1428	eqcomd	$⊢ \neg 2 ∥ n \to (\frac{4}{n π}) \sin n X = if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)$
1430	1429	adantl	$⊢ (n \in ℕ \land \neg 2 ∥ n) \to (\frac{4}{n π}) \sin n X = if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)$
1431	1427 1430	eqtrd	$⊢ (n \in ℕ \land \neg 2 ∥ n) \to if (2 ∥ n, 0, \frac{4}{n π}) \sin n X = if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)$
1432	1424 1431	pm2.61dan	$⊢ n \in ℕ \to if (2 ∥ n, 0, \frac{4}{n π}) \sin n X = if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)$
1433	1413 1416 1432	3eqtrrd	$⊢ n \in ℕ \to if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X) = (n \in ℕ_{0} ⟼ 0) (n) \cos n X + (n \in ℕ ⟼ if (2 ∥ n, 0, \frac{4}{n π})) (n) \sin n X$
1434	1433	mpteq2ia	$⊢ (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) = (n \in ℕ ⟼ (n \in ℕ_{0} ⟼ 0) (n) \cos n X + (n \in ℕ ⟼ if (2 ∥ n, 0, \frac{4}{n π})) (n) \sin n X)$
1435	112 1 149 150 330 605 676 755 3 1137 1389 1393 1397 1434	fourierclim	$⊢ seq 1 (+ (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X))) ⇝ ((\frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2}) - (\frac{(n \in ℕ_{0} ⟼ 0) (0)}{2}))$
1436		0nn0	$⊢ 0 \in ℕ_{0}$
1437		eqidd	$⊢ n = 0 \to 0 = 0$
1438	1437 1400 93	fvmpt	$⊢ 0 \in ℕ_{0} \to (n \in ℕ_{0} ⟼ 0) (0) = 0$
1439	1436 1438	ax-mp	$⊢ (n \in ℕ_{0} ⟼ 0) (0) = 0$
1440	1439	oveq1i	$⊢ \frac{(n \in ℕ_{0} ⟼ 0) (0)}{2} = \frac{0}{2}$
1441	32	recni	$⊢ 2 \in ℂ$
1442	71 131	gtneii	$⊢ 2 \neq 0$
1443	1441 1442	div0i	$⊢ \frac{0}{2} = 0$
1444	1440 1443	eqtri	$⊢ \frac{(n \in ℕ_{0} ⟼ 0) (0)}{2} = 0$
1445	1444	oveq2i	$⊢ (\frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2}) - (\frac{(n \in ℕ_{0} ⟼ 0) (0)}{2}) = (\frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2}) - 0$
1446	203	mptru	$⊢ 1 \in ℂ$
1447	1446 1011	ifcli	$⊢ if (X \mod T \in (0, π], 1, - 1) \in ℂ$
1448	1151	recni	$⊢ if (X \mod T < π, 1, - 1) \in ℂ$
1449	1286 1448	eqeltri	$⊢ F (X) \in ℂ$
1450	1447 1449	addcli	$⊢ if (X \mod T \in (0, π], 1, - 1) + F (X) \in ℂ$
1451	1450 1441 1442	divcli	$⊢ \frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2} \in ℂ$
1452	1451	subid1i	$⊢ (\frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2}) - 0 = \frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2}$
1453	1445 1452	eqtri	$⊢ (\frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2}) - (\frac{(n \in ℕ_{0} ⟼ 0) (0)}{2}) = \frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2}$
1454	1435 1453	breqtri	$⊢ seq 1 (+ (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X))) ⇝ (\frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2})$
1455	1454	a1i	$⊢ ⊤ \to seq 1 (+ (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X))) ⇝ (\frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2})$
1456	83 107 1455	sumnnodd	$⊢ ⊤ \to (seq 1 (+ (k \in ℕ ⟼ (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) (2 k - 1))) ⇝ (\frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2}) \land \sum_{k \in ℕ} (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) (k) = \sum_{k \in ℕ} (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) (2 k - 1))$
1457	1456	mptru	$⊢ (seq 1 (+ (k \in ℕ ⟼ (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) (2 k - 1))) ⇝ (\frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2}) \land \sum_{k \in ℕ} (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) (k) = \sum_{k \in ℕ} (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) (2 k - 1))$
1458	1457	simpli	$⊢ seq 1 (+ (k \in ℕ ⟼ (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) (2 k - 1))) ⇝ (\frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2})$
1459		breq2	$⊢ n = 2 k - 1 \to (2 ∥ n \leftrightarrow 2 ∥ (2 k - 1))$
1460		oveq1	$⊢ n = 2 k - 1 \to n π = (2 k - 1) π$
1461	1460	oveq2d	$⊢ n = 2 k - 1 \to \frac{4}{n π} = \frac{4}{(2 k - 1) π}$
1462		oveq1	$⊢ n = 2 k - 1 \to n X = (2 k - 1) X$
1463	1462	fveq2d	$⊢ n = 2 k - 1 \to \sin n X = \sin (2 k - 1) X$
1464	1461 1463	oveq12d	$⊢ n = 2 k - 1 \to (\frac{4}{n π}) \sin n X = (\frac{4}{(2 k - 1) π}) \sin (2 k - 1) X$
1465	1459 1464	ifbieq2d	$⊢ n = 2 k - 1 \to if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X) = if (2 ∥ (2 k - 1), 0, (\frac{4}{(2 k - 1) π}) \sin (2 k - 1) X)$
1466	1465	adantl	$⊢ (k \in ℕ \land n = 2 k - 1) \to if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X) = if (2 ∥ (2 k - 1), 0, (\frac{4}{(2 k - 1) π}) \sin (2 k - 1) X)$
1467		elnnz	$⊢ 2 k - 1 \in ℕ \leftrightarrow (2 k - 1 \in ℤ \land 0 < 2 k - 1)$
1468	25 52 1467	sylanbrc	$⊢ k \in ℕ \to 2 k - 1 \in ℕ$
1469		ovex	$⊢ (\frac{4}{(2 k - 1) π}) \sin (2 k - 1) X \in V$
1470	93 1469	ifex	$⊢ if (2 ∥ (2 k - 1), 0, (\frac{4}{(2 k - 1) π}) \sin (2 k - 1) X) \in V$
1471	1470	a1i	$⊢ k \in ℕ \to if (2 ∥ (2 k - 1), 0, (\frac{4}{(2 k - 1) π}) \sin (2 k - 1) X) \in V$
1472	84 1466 1468 1471	fvmptd	$⊢ k \in ℕ \to (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) (2 k - 1) = if (2 ∥ (2 k - 1), 0, (\frac{4}{(2 k - 1) π}) \sin (2 k - 1) X)$
1473		dvdsmul1	$⊢ (2 \in ℤ \land k \in ℤ) \to 2 ∥ 2 k$
1474	20 22 1473	sylancr	$⊢ k \in ℕ \to 2 ∥ 2 k$
1475	23	zcnd	$⊢ k \in ℕ \to 2 k \in ℂ$
1476		1cnd	$⊢ k \in ℕ \to 1 \in ℂ$
1477	1475 1476	npcand	$⊢ k \in ℕ \to 2 k - 1 + 1 = 2 k$
1478	1477	eqcomd	$⊢ k \in ℕ \to 2 k = 2 k - 1 + 1$
1479	1474 1478	breqtrd	$⊢ k \in ℕ \to 2 ∥ (2 k - 1 + 1)$
1480		oddp1even	$⊢ 2 k - 1 \in ℤ \to (\neg 2 ∥ (2 k - 1) \leftrightarrow 2 ∥ (2 k - 1 + 1))$
1481	25 1480	syl	$⊢ k \in ℕ \to (\neg 2 ∥ (2 k - 1) \leftrightarrow 2 ∥ (2 k - 1 + 1))$
1482	1479 1481	mpbird	$⊢ k \in ℕ \to \neg 2 ∥ (2 k - 1)$
1483	1482	iffalsed	$⊢ k \in ℕ \to if (2 ∥ (2 k - 1), 0, (\frac{4}{(2 k - 1) π}) \sin (2 k - 1) X) = (\frac{4}{(2 k - 1) π}) \sin (2 k - 1) X$
1484	56	a1i	$⊢ k \in ℕ \to π \in ℂ$
1485	26 1484	mulcomd	$⊢ k \in ℕ \to (2 k - 1) π = π (2 k - 1)$
1486	1485	oveq2d	$⊢ k \in ℕ \to \frac{4}{(2 k - 1) π} = \frac{4}{π (2 k - 1)}$
1487	58	a1i	$⊢ k \in ℕ \to 4 \in ℂ$
1488	73	a1i	$⊢ k \in ℕ \to π \neq 0$
1489	1487 1484 26 1488 53	divdiv1d	$⊢ k \in ℕ \to \frac{\frac{4}{π}}{2 k - 1} = \frac{4}{π (2 k - 1)}$
1490	1486 1489	eqtr4d	$⊢ k \in ℕ \to \frac{4}{(2 k - 1) π} = \frac{\frac{4}{π}}{2 k - 1}$
1491	1490	oveq1d	$⊢ k \in ℕ \to (\frac{4}{(2 k - 1) π}) \sin (2 k - 1) X = (\frac{\frac{4}{π}}{2 k - 1}) \sin (2 k - 1) X$
1492	1487 1484 1488	divcld	$⊢ k \in ℕ \to \frac{4}{π} \in ℂ$
1493	1492 26 30 53	div32d	$⊢ k \in ℕ \to (\frac{\frac{4}{π}}{2 k - 1}) \sin (2 k - 1) X = (\frac{4}{π}) (\frac{\sin (2 k - 1) X}{2 k - 1})$
1494	1491 1493	eqtrd	$⊢ k \in ℕ \to (\frac{4}{(2 k - 1) π}) \sin (2 k - 1) X = (\frac{4}{π}) (\frac{\sin (2 k - 1) X}{2 k - 1})$
1495	1472 1483 1494	3eqtrd	$⊢ k \in ℕ \to (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) (2 k - 1) = (\frac{4}{π}) (\frac{\sin (2 k - 1) X}{2 k - 1})$
1496	1495	mpteq2ia	$⊢ (k \in ℕ ⟼ (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) (2 k - 1)) = (k \in ℕ ⟼ (\frac{4}{π}) (\frac{\sin (2 k - 1) X}{2 k - 1}))$
1497		oveq2	$⊢ k = n \to 2 k = 2 n$
1498	1497	oveq1d	$⊢ k = n \to 2 k - 1 = 2 n - 1$
1499	1498	oveq1d	$⊢ k = n \to (2 k - 1) X = (2 n - 1) X$
1500	1499	fveq2d	$⊢ k = n \to \sin (2 k - 1) X = \sin (2 n - 1) X$
1501	1500 1498	oveq12d	$⊢ k = n \to \frac{\sin (2 k - 1) X}{2 k - 1} = \frac{\sin (2 n - 1) X}{2 n - 1}$
1502	1501	oveq2d	$⊢ k = n \to (\frac{4}{π}) (\frac{\sin (2 k - 1) X}{2 k - 1}) = (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1})$
1503	1502	cbvmptv	$⊢ (k \in ℕ ⟼ (\frac{4}{π}) (\frac{\sin (2 k - 1) X}{2 k - 1})) = (n \in ℕ ⟼ (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1}))$
1504	1496 1503	eqtri	$⊢ (k \in ℕ ⟼ (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) (2 k - 1)) = (n \in ℕ ⟼ (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1}))$
1505		seqeq3	$⊢ (k \in ℕ ⟼ (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) (2 k - 1)) = (n \in ℕ ⟼ (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1})) \to seq 1 (+ (k \in ℕ ⟼ (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) (2 k - 1))) = seq 1 (+ (n \in ℕ ⟼ (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1})))$
1506	1504 1505	ax-mp	$⊢ seq 1 (+ (k \in ℕ ⟼ (n \in ℕ ⟼ if (2 ∥ n, 0, (\frac{4}{n π}) \sin n X)) (2 k - 1))) = seq 1 (+ (n \in ℕ ⟼ (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1})))$
1507	1 2 3 5	fourierswlem	$⊢ Y = \frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2}$
1508	1507	eqcomi	$⊢ \frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2} = Y$
1509	1458 1506 1508	3brtr3i	$⊢ seq 1 (+ (n \in ℕ ⟼ (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1}))) ⇝ Y$
1510	1509	a1i	$⊢ ⊤ \to seq 1 (+ (n \in ℕ ⟼ (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1}))) ⇝ Y$
1511		eqid	$⊢ (n \in ℕ ⟼ (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1})) = (n \in ℕ ⟼ (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1}))$
1512	65 69 74	divcld	$⊢ n \in ℕ \to \frac{4}{π} \in ℂ$
1513	1441	a1i	$⊢ n \in ℕ \to 2 \in ℂ$
1514	1513 66	mulcld	$⊢ n \in ℕ \to 2 n \in ℂ$
1515		id	$⊢ 2 n \in ℂ \to 2 n \in ℂ$
1516		1cnd	$⊢ 2 n \in ℂ \to 1 \in ℂ$
1517	1515 1516	subcld	$⊢ 2 n \in ℂ \to 2 n - 1 \in ℂ$
1518	1514 1517	syl	$⊢ n \in ℕ \to 2 n - 1 \in ℂ$
1519	1518 77	mulcld	$⊢ n \in ℕ \to (2 n - 1) X \in ℂ$
1520	1519	sincld	$⊢ n \in ℕ \to \sin (2 n - 1) X \in ℂ$
1521	32	a1i	$⊢ n \in ℕ \to 2 \in ℝ$
1522		nnre	$⊢ n \in ℕ \to n \in ℝ$
1523	1521 1522	remulcld	$⊢ n \in ℕ \to 2 n \in ℝ$
1524	1523	recnd	$⊢ n \in ℕ \to 2 n \in ℂ$
1525		1cnd	$⊢ n \in ℕ \to 1 \in ℂ$
1526	1524 1525	subcld	$⊢ n \in ℕ \to 2 n - 1 \in ℂ$
1527		1red	$⊢ n \in ℕ \to 1 \in ℝ$
1528	39 1521	eqeltrid	$⊢ n \in ℕ \to 2 \cdot 1 \in ℝ$
1529		1lt2	$⊢ 1 < 2$
1530	1529	a1i	$⊢ n \in ℕ \to 1 < 2$
1531	1530 39	breqtrrdi	$⊢ n \in ℕ \to 1 < 2 \cdot 1$
1532	47	a1i	$⊢ n \in ℕ \to 0 \leq 2$
1533		nnge1	$⊢ n \in ℕ \to 1 \leq n$
1534	1527 1522 1521 1532 1533	lemul2ad	$⊢ n \in ℕ \to 2 \cdot 1 \leq 2 n$
1535	1527 1528 1523 1531 1534	ltletrd	$⊢ n \in ℕ \to 1 < 2 n$
1536	1527 1535	gtned	$⊢ n \in ℕ \to 2 n \neq 1$
1537	1524 1525 1536	subne0d	$⊢ n \in ℕ \to 2 n - 1 \neq 0$
1538	1520 1526 1537	divcld	$⊢ n \in ℕ \to \frac{\sin (2 n - 1) X}{2 n - 1} \in ℂ$
1539	1512 1538	mulcld	$⊢ n \in ℕ \to (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1}) \in ℂ$
1540	1511 1539	fmpti	$⊢ (n \in ℕ ⟼ (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1})) : ℕ ⟶ ℂ$
1541	1540	a1i	$⊢ ⊤ \to (n \in ℕ ⟼ (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1})) : ℕ ⟶ ℂ$
1542	1541	ffvelcdmda	$⊢ (⊤ \land k \in ℕ) \to (n \in ℕ ⟼ (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1})) (k) \in ℂ$
1543		divcan6	$⊢ ((π \in ℂ \land π \neq 0) \land (4 \in ℂ \land 4 \neq 0)) \to (\frac{π}{4}) (\frac{4}{π}) = 1$
1544	56 73 58 60 1543	mp4an	$⊢ (\frac{π}{4}) (\frac{4}{π}) = 1$
1545	1544	eqcomi	$⊢ 1 = (\frac{π}{4}) (\frac{4}{π})$
1546	1545	oveq1i	$⊢ 1 (\frac{\sin (2 k - 1) X}{2 k - 1}) = (\frac{π}{4}) (\frac{4}{π}) (\frac{\sin (2 k - 1) X}{2 k - 1})$
1547	54	mullidd	$⊢ k \in ℕ \to 1 (\frac{\sin (2 k - 1) X}{2 k - 1}) = \frac{\sin (2 k - 1) X}{2 k - 1}$
1548	60	a1i	$⊢ k \in ℕ \to 4 \neq 0$
1549	1484 1487 1548	divcld	$⊢ k \in ℕ \to \frac{π}{4} \in ℂ$
1550	1549 1492 54	mulassd	$⊢ k \in ℕ \to (\frac{π}{4}) (\frac{4}{π}) (\frac{\sin (2 k - 1) X}{2 k - 1}) = (\frac{π}{4}) (\frac{4}{π}) (\frac{\sin (2 k - 1) X}{2 k - 1})$
1551	1546 1547 1550	3eqtr3a	$⊢ k \in ℕ \to \frac{\sin (2 k - 1) X}{2 k - 1} = (\frac{π}{4}) (\frac{4}{π}) (\frac{\sin (2 k - 1) X}{2 k - 1})$
1552		eqidd	$⊢ k \in ℕ \to (n \in ℕ ⟼ (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1})) = (n \in ℕ ⟼ (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1}))$
1553	13	oveq2d	$⊢ n = k \to (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1}) = (\frac{4}{π}) (\frac{\sin (2 k - 1) X}{2 k - 1})$
1554	1553	adantl	$⊢ (k \in ℕ \land n = k) \to (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1}) = (\frac{4}{π}) (\frac{\sin (2 k - 1) X}{2 k - 1})$
1555	1494 1469	eqeltrrdi	$⊢ k \in ℕ \to (\frac{4}{π}) (\frac{\sin (2 k - 1) X}{2 k - 1}) \in V$
1556	1552 1554 15 1555	fvmptd	$⊢ k \in ℕ \to (n \in ℕ ⟼ (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1})) (k) = (\frac{4}{π}) (\frac{\sin (2 k - 1) X}{2 k - 1})$
1557	1556	oveq2d	$⊢ k \in ℕ \to (\frac{π}{4}) (n \in ℕ ⟼ (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1})) (k) = (\frac{π}{4}) (\frac{4}{π}) (\frac{\sin (2 k - 1) X}{2 k - 1})$
1558	1557	eqcomd	$⊢ k \in ℕ \to (\frac{π}{4}) (\frac{4}{π}) (\frac{\sin (2 k - 1) X}{2 k - 1}) = (\frac{π}{4}) (n \in ℕ ⟼ (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1})) (k)$
1559	18 1551 1558	3eqtrd	$⊢ k \in ℕ \to (n \in ℕ ⟼ \frac{\sin (2 n - 1) X}{2 n - 1}) (k) = (\frac{π}{4}) (n \in ℕ ⟼ (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1})) (k)$
1560	1559	adantl	$⊢ (⊤ \land k \in ℕ) \to (n \in ℕ ⟼ \frac{\sin (2 n - 1) X}{2 n - 1}) (k) = (\frac{π}{4}) (n \in ℕ ⟼ (\frac{4}{π}) (\frac{\sin (2 n - 1) X}{2 n - 1})) (k)$
1561	6 7 62 1510 1542 1560	isermulc2	$⊢ ⊤ \to seq 1 (+ (n \in ℕ ⟼ \frac{\sin (2 n - 1) X}{2 n - 1})) ⇝ (\frac{π}{4}) Y$
1562		climrel	$⊢ Rel ⇝$
1563	1562	releldmi	$⊢ seq 1 (+ (n \in ℕ ⟼ \frac{\sin (2 n - 1) X}{2 n - 1})) ⇝ (\frac{π}{4}) Y \to seq 1 (+ (n \in ℕ ⟼ \frac{\sin (2 n - 1) X}{2 n - 1})) \in dom ⇝$
1564	1561 1563	syl	$⊢ ⊤ \to seq 1 (+ (n \in ℕ ⟼ \frac{\sin (2 n - 1) X}{2 n - 1})) \in dom ⇝$
1565	6 7 19 55 1564	isumclim2	$⊢ ⊤ \to seq 1 (+ (n \in ℕ ⟼ \frac{\sin (2 n - 1) X}{2 n - 1})) ⇝ \sum_{k \in ℕ} (\frac{\sin (2 k - 1) X}{2 k - 1})$
1566	1565	mptru	$⊢ seq 1 (+ (n \in ℕ ⟼ \frac{\sin (2 n - 1) X}{2 n - 1})) ⇝ \sum_{k \in ℕ} (\frac{\sin (2 k - 1) X}{2 k - 1})$
1567	1561	mptru	$⊢ seq 1 (+ (n \in ℕ ⟼ \frac{\sin (2 n - 1) X}{2 n - 1})) ⇝ (\frac{π}{4}) Y$
1568		climuni	$⊢ (seq 1 (+ (n \in ℕ ⟼ \frac{\sin (2 n - 1) X}{2 n - 1})) ⇝ \sum_{k \in ℕ} (\frac{\sin (2 k - 1) X}{2 k - 1}) \land seq 1 (+ (n \in ℕ ⟼ \frac{\sin (2 n - 1) X}{2 n - 1})) ⇝ (\frac{π}{4}) Y) \to \sum_{k \in ℕ} (\frac{\sin (2 k - 1) X}{2 k - 1}) = (\frac{π}{4}) Y$
1569	1566 1567 1568	mp2an	$⊢ \sum_{k \in ℕ} (\frac{\sin (2 k - 1) X}{2 k - 1}) = (\frac{π}{4}) Y$
1570	1569	oveq2i	$⊢ (\frac{4}{π}) \sum_{k \in ℕ} (\frac{\sin (2 k - 1) X}{2 k - 1}) = (\frac{4}{π}) (\frac{π}{4}) Y$
1571	58 56 73	divcli	$⊢ \frac{4}{π} \in ℂ$
1572	56 58 60	divcli	$⊢ \frac{π}{4} \in ℂ$
1573	1286 1151	eqeltri	$⊢ F (X) \in ℝ$
1574	71 1573	ifcli	$⊢ if (X \mod π = 0, 0, F (X)) \in ℝ$
1575	5 1574	eqeltri	$⊢ Y \in ℝ$
1576	1575	recni	$⊢ Y \in ℂ$
1577	1571 1572 1576	mulassi	$⊢ (\frac{4}{π}) (\frac{π}{4}) Y = (\frac{4}{π}) (\frac{π}{4}) Y$
1578	1572 1571 1544	mulcomli	$⊢ (\frac{4}{π}) (\frac{π}{4}) = 1$
1579	1578	oveq1i	$⊢ (\frac{4}{π}) (\frac{π}{4}) Y = 1 Y$
1580	1576	mullidi	$⊢ 1 Y = Y$
1581	1579 1580	eqtri	$⊢ (\frac{4}{π}) (\frac{π}{4}) Y = Y$
1582	1570 1577 1581	3eqtr2i	$⊢ (\frac{4}{π}) \sum_{k \in ℕ} (\frac{\sin (2 k - 1) X}{2 k - 1}) = Y$
1583		seqeq3	$⊢ S = (n \in ℕ ⟼ \frac{\sin (2 n - 1) X}{2 n - 1}) \to seq 1 (+ S) = seq 1 (+ (n \in ℕ ⟼ \frac{\sin (2 n - 1) X}{2 n - 1}))$
1584	4 1583	ax-mp	$⊢ seq 1 (+ S) = seq 1 (+ (n \in ℕ ⟼ \frac{\sin (2 n - 1) X}{2 n - 1}))$
1585	1584 1567	eqbrtri	$⊢ seq 1 (+ S) ⇝ (\frac{π}{4}) Y$
1586	1582 1585	pm3.2i	$⊢ ((\frac{4}{π}) \sum_{k \in ℕ} (\frac{\sin (2 k - 1) X}{2 k - 1}) = Y \land seq 1 (+ S) ⇝ (\frac{π}{4}) Y)$

Metamath Proof Explorer

Theorem fouriersw

Proof