fourierswlem

Description: The Fourier series for the square wave F converges to Y , a simpler expression for this special case. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierswlem.t	$⊢ T = 2 π$
	fourierswlem.f	$⊢ F = (x \in ℝ ⟼ if (x \mod T < π, 1, - 1))$
	fourierswlem.x	$⊢ X \in ℝ$
	fourierswlem.y	$⊢ Y = if (X \mod π = 0, 0, F (X))$
Assertion	fourierswlem	$⊢ Y = \frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2}$

Proof

Step	Hyp	Ref	Expression
1		fourierswlem.t	$⊢ T = 2 π$
2		fourierswlem.f	$⊢ F = (x \in ℝ ⟼ if (x \mod T < π, 1, - 1))$
3		fourierswlem.x	$⊢ X \in ℝ$
4		fourierswlem.y	$⊢ Y = if (X \mod π = 0, 0, F (X))$
5		simpr	$⊢ (X \mod π = 0 \land 2 ∥ (\frac{X}{π})) \to 2 ∥ (\frac{X}{π})$
6		2z	$⊢ 2 \in ℤ$
7	6	a1i	$⊢ (X \mod π = 0 \land 2 ∥ (\frac{X}{π})) \to 2 \in ℤ$
8		pirp	$⊢ π \in ℝ^{+}$
9		mod0	$⊢ (X \in ℝ \land π \in ℝ^{+}) \to (X \mod π = 0 \leftrightarrow \frac{X}{π} \in ℤ)$
10	3 8 9	mp2an	$⊢ X \mod π = 0 \leftrightarrow \frac{X}{π} \in ℤ$
11	10	birani	$⊢ (X \mod π = 0 \land 2 ∥ (\frac{X}{π})) \to \frac{X}{π} \in ℤ$
12		divides	$⊢ (2 \in ℤ \land \frac{X}{π} \in ℤ) \to (2 ∥ (\frac{X}{π}) \leftrightarrow \exists k \in ℤ k \cdot 2 = \frac{X}{π})$
13	7 11 12	syl2anc	$⊢ (X \mod π = 0 \land 2 ∥ (\frac{X}{π})) \to (2 ∥ (\frac{X}{π}) \leftrightarrow \exists k \in ℤ k \cdot 2 = \frac{X}{π})$
14	5 13	mpbid	$⊢ (X \mod π = 0 \land 2 ∥ (\frac{X}{π})) \to \exists k \in ℤ k \cdot 2 = \frac{X}{π}$
15		2cnd	$⊢ k \in ℤ \to 2 \in ℂ$
16		picn	$⊢ π \in ℂ$
17	16	a1i	$⊢ k \in ℤ \to π \in ℂ$
18		zcn	$⊢ k \in ℤ \to k \in ℂ$
19	15 17 18	mulassd	$⊢ k \in ℤ \to 2 π k = 2 π k$
20	17 18	mulcld	$⊢ k \in ℤ \to π k \in ℂ$
21	15 20	mulcomd	$⊢ k \in ℤ \to 2 π k = π k \cdot 2$
22	19 21	eqtrd	$⊢ k \in ℤ \to 2 π k = π k \cdot 2$
23	22	adantr	$⊢ (k \in ℤ \land k \cdot 2 = \frac{X}{π}) \to 2 π k = π k \cdot 2$
24	17 18 15	mulassd	$⊢ k \in ℤ \to π k \cdot 2 = π k \cdot 2$
25	24	adantr	$⊢ (k \in ℤ \land k \cdot 2 = \frac{X}{π}) \to π k \cdot 2 = π k \cdot 2$
26		id	$⊢ k \cdot 2 = \frac{X}{π} \to k \cdot 2 = \frac{X}{π}$
27	26	eqcomd	$⊢ k \cdot 2 = \frac{X}{π} \to \frac{X}{π} = k \cdot 2$
28	27	adantl	$⊢ (k \in ℤ \land k \cdot 2 = \frac{X}{π}) \to \frac{X}{π} = k \cdot 2$
29	3	recni	$⊢ X \in ℂ$
30	29	a1i	$⊢ (k \in ℤ \land k \cdot 2 = \frac{X}{π}) \to X \in ℂ$
31	16	a1i	$⊢ (k \in ℤ \land k \cdot 2 = \frac{X}{π}) \to π \in ℂ$
32	18	adantr	$⊢ (k \in ℤ \land k \cdot 2 = \frac{X}{π}) \to k \in ℂ$
33		2cnd	$⊢ (k \in ℤ \land k \cdot 2 = \frac{X}{π}) \to 2 \in ℂ$
34	32 33	mulcld	$⊢ (k \in ℤ \land k \cdot 2 = \frac{X}{π}) \to k \cdot 2 \in ℂ$
35		pire	$⊢ π \in ℝ$
36		pipos	$⊢ 0 < π$
37	35 36	gt0ne0ii	$⊢ π \neq 0$
38	37	a1i	$⊢ (k \in ℤ \land k \cdot 2 = \frac{X}{π}) \to π \neq 0$
39	30 31 34 38	divmuld	$⊢ (k \in ℤ \land k \cdot 2 = \frac{X}{π}) \to (\frac{X}{π} = k \cdot 2 \leftrightarrow π k \cdot 2 = X)$
40	28 39	mpbid	$⊢ (k \in ℤ \land k \cdot 2 = \frac{X}{π}) \to π k \cdot 2 = X$
41	23 25 40	3eqtrrd	$⊢ (k \in ℤ \land k \cdot 2 = \frac{X}{π}) \to X = 2 π k$
42	1	a1i	$⊢ (k \in ℤ \land k \cdot 2 = \frac{X}{π}) \to T = 2 π$
43	41 42	oveq12d	$⊢ (k \in ℤ \land k \cdot 2 = \frac{X}{π}) \to \frac{X}{T} = \frac{2 π k}{2 π}$
44	15 17	mulcld	$⊢ k \in ℤ \to 2 π \in ℂ$
45		2ne0	$⊢ 2 \neq 0$
46	45	a1i	$⊢ k \in ℤ \to 2 \neq 0$
47	37	a1i	$⊢ k \in ℤ \to π \neq 0$
48	15 17 46 47	mulne0d	$⊢ k \in ℤ \to 2 π \neq 0$
49	18 44 48	divcan3d	$⊢ k \in ℤ \to \frac{2 π k}{2 π} = k$
50	49	adantr	$⊢ (k \in ℤ \land k \cdot 2 = \frac{X}{π}) \to \frac{2 π k}{2 π} = k$
51	43 50	eqtrd	$⊢ (k \in ℤ \land k \cdot 2 = \frac{X}{π}) \to \frac{X}{T} = k$
52		simpl	$⊢ (k \in ℤ \land k \cdot 2 = \frac{X}{π}) \to k \in ℤ$
53	51 52	eqeltrd	$⊢ (k \in ℤ \land k \cdot 2 = \frac{X}{π}) \to \frac{X}{T} \in ℤ$
54	53	ex	$⊢ k \in ℤ \to (k \cdot 2 = \frac{X}{π} \to \frac{X}{T} \in ℤ)$
55	54	a1i	$⊢ (X \mod π = 0 \land 2 ∥ (\frac{X}{π})) \to (k \in ℤ \to (k \cdot 2 = \frac{X}{π} \to \frac{X}{T} \in ℤ))$
56	55	rexlimdv	$⊢ (X \mod π = 0 \land 2 ∥ (\frac{X}{π})) \to (\exists k \in ℤ k \cdot 2 = \frac{X}{π} \to \frac{X}{T} \in ℤ)$
57	14 56	mpd	$⊢ (X \mod π = 0 \land 2 ∥ (\frac{X}{π})) \to \frac{X}{T} \in ℤ$
58		2re	$⊢ 2 \in ℝ$
59	58 35	remulcli	$⊢ 2 π \in ℝ$
60	1 59	eqeltri	$⊢ T \in ℝ$
61		2pos	$⊢ 0 < 2$
62	58 35 61 36	mulgt0ii	$⊢ 0 < 2 π$
63	62 1	breqtrri	$⊢ 0 < T$
64	60 63	elrpii	$⊢ T \in ℝ^{+}$
65		mod0	$⊢ (X \in ℝ \land T \in ℝ^{+}) \to (X \mod T = 0 \leftrightarrow \frac{X}{T} \in ℤ)$
66	3 64 65	mp2an	$⊢ X \mod T = 0 \leftrightarrow \frac{X}{T} \in ℤ$
67	57 66	sylibr	$⊢ (X \mod π = 0 \land 2 ∥ (\frac{X}{π})) \to X \mod T = 0$
68	67	orcd	$⊢ (X \mod π = 0 \land 2 ∥ (\frac{X}{π})) \to (X \mod T = 0 \lor X \mod T = π)$
69		odd2np1	$⊢ \frac{X}{π} \in ℤ \to (\neg 2 ∥ (\frac{X}{π}) \leftrightarrow \exists k \in ℤ 2 k + 1 = \frac{X}{π})$
70	10 69	sylbi	$⊢ X \mod π = 0 \to (\neg 2 ∥ (\frac{X}{π}) \leftrightarrow \exists k \in ℤ 2 k + 1 = \frac{X}{π})$
71	70	biimpa	$⊢ (X \mod π = 0 \land \neg 2 ∥ (\frac{X}{π})) \to \exists k \in ℤ 2 k + 1 = \frac{X}{π}$
72	15 18	mulcld	$⊢ k \in ℤ \to 2 k \in ℂ$
73	72	adantr	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to 2 k \in ℂ$
74		1cnd	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to 1 \in ℂ$
75	16	a1i	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to π \in ℂ$
76	73 74 75	adddird	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to (2 k + 1) π = 2 k π + 1 π$
77	15 18	mulcomd	$⊢ k \in ℤ \to 2 k = k \cdot 2$
78	77	oveq1d	$⊢ k \in ℤ \to 2 k π = k \cdot 2 π$
79	18 15 17	mulassd	$⊢ k \in ℤ \to k \cdot 2 π = k 2 π$
80	1	eqcomi	$⊢ 2 π = T$
81	80	a1i	$⊢ k \in ℤ \to 2 π = T$
82	81	oveq2d	$⊢ k \in ℤ \to k 2 π = k T$
83	78 79 82	3eqtrd	$⊢ k \in ℤ \to 2 k π = k T$
84	16	mullidi	$⊢ 1 π = π$
85	84	a1i	$⊢ k \in ℤ \to 1 π = π$
86	83 85	oveq12d	$⊢ k \in ℤ \to 2 k π + 1 π = k T + π$
87	86	adantr	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to 2 k π + 1 π = k T + π$
88	1 44	eqeltrid	$⊢ k \in ℤ \to T \in ℂ$
89	18 88	mulcld	$⊢ k \in ℤ \to k T \in ℂ$
90	89 17	addcomd	$⊢ k \in ℤ \to k T + π = π + k T$
91	90	adantr	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to k T + π = π + k T$
92	76 87 91	3eqtrrd	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to π + k T = (2 k + 1) π$
93		peano2cn	$⊢ 2 k \in ℂ \to 2 k + 1 \in ℂ$
94	72 93	syl	$⊢ k \in ℤ \to 2 k + 1 \in ℂ$
95	94 17	mulcomd	$⊢ k \in ℤ \to (2 k + 1) π = π (2 k + 1)$
96	95	adantr	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to (2 k + 1) π = π (2 k + 1)$
97		id	$⊢ 2 k + 1 = \frac{X}{π} \to 2 k + 1 = \frac{X}{π}$
98	97	eqcomd	$⊢ 2 k + 1 = \frac{X}{π} \to \frac{X}{π} = 2 k + 1$
99	98	adantl	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to \frac{X}{π} = 2 k + 1$
100	29	a1i	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to X \in ℂ$
101	94	adantr	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to 2 k + 1 \in ℂ$
102	37	a1i	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to π \neq 0$
103	100 75 101 102	divmuld	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to (\frac{X}{π} = 2 k + 1 \leftrightarrow π (2 k + 1) = X)$
104	99 103	mpbid	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to π (2 k + 1) = X$
105	92 96 104	3eqtrrd	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to X = π + k T$
106	105	oveq1d	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to X \mod T = (π + k T) \mod T$
107		modcyc	$⊢ (π \in ℝ \land T \in ℝ^{+} \land k \in ℤ) \to (π + k T) \mod T = π \mod T$
108	35 64 107	mp3an12	$⊢ k \in ℤ \to (π + k T) \mod T = π \mod T$
109	108	adantr	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to (π + k T) \mod T = π \mod T$
110	35	a1i	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to π \in ℝ$
111	64	a1i	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to T \in ℝ^{+}$
112		0re	$⊢ 0 \in ℝ$
113	112 35 36	ltleii	$⊢ 0 \leq π$
114	113	a1i	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to 0 \leq π$
115		2timesgt	$⊢ π \in ℝ^{+} \to π < 2 π$
116	8 115	ax-mp	$⊢ π < 2 π$
117	116 1	breqtrri	$⊢ π < T$
118	117	a1i	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to π < T$
119		modid	$⊢ ((π \in ℝ \land T \in ℝ^{+}) \land (0 \leq π \land π < T)) \to π \mod T = π$
120	110 111 114 118 119	syl22anc	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to π \mod T = π$
121	106 109 120	3eqtrd	$⊢ (k \in ℤ \land 2 k + 1 = \frac{X}{π}) \to X \mod T = π$
122	121	ex	$⊢ k \in ℤ \to (2 k + 1 = \frac{X}{π} \to X \mod T = π)$
123	122	a1i	$⊢ (X \mod π = 0 \land \neg 2 ∥ (\frac{X}{π})) \to (k \in ℤ \to (2 k + 1 = \frac{X}{π} \to X \mod T = π))$
124	123	rexlimdv	$⊢ (X \mod π = 0 \land \neg 2 ∥ (\frac{X}{π})) \to (\exists k \in ℤ 2 k + 1 = \frac{X}{π} \to X \mod T = π)$
125	71 124	mpd	$⊢ (X \mod π = 0 \land \neg 2 ∥ (\frac{X}{π})) \to X \mod T = π$
126	125	olcd	$⊢ (X \mod π = 0 \land \neg 2 ∥ (\frac{X}{π})) \to (X \mod T = 0 \lor X \mod T = π)$
127	68 126	pm2.61dan	$⊢ X \mod π = 0 \to (X \mod T = 0 \lor X \mod T = π)$
128		0xr	$⊢ 0 \in ℝ^{*}$
129	35	rexri	$⊢ π \in ℝ^{*}$
130		iocgtlb	$⊢ (0 \in ℝ^{} \land π \in ℝ^{} \land X \mod T \in (0, π]) \to 0 < X \mod T$
131	128 129 130	mp3an12	$⊢ X \mod T \in (0, π] \to 0 < X \mod T$
132	131	gt0ne0d	$⊢ X \mod T \in (0, π] \to X \mod T \neq 0$
133	132	neneqd	$⊢ X \mod T \in (0, π] \to \neg X \mod T = 0$
134		pm2.53	$⊢ (X \mod T = 0 \lor X \mod T = π) \to (\neg X \mod T = 0 \to X \mod T = π)$
135	134	imp	$⊢ ((X \mod T = 0 \lor X \mod T = π) \land \neg X \mod T = 0) \to X \mod T = π$
136	127 133 135	syl2anr	$⊢ (X \mod T \in (0, π] \land X \mod π = 0) \to X \mod T = π$
137	128	a1i	$⊢ X \mod T = π \to 0 \in ℝ^{*}$
138	129	a1i	$⊢ X \mod T = π \to π \in ℝ^{*}$
139		modcl	$⊢ (X \in ℝ \land T \in ℝ^{+}) \to X \mod T \in ℝ$
140	3 64 139	mp2an	$⊢ X \mod T \in ℝ$
141	140	rexri	$⊢ X \mod T \in ℝ^{*}$
142	141	a1i	$⊢ X \mod T = π \to X \mod T \in ℝ^{*}$
143		id	$⊢ X \mod T = π \to X \mod T = π$
144	36 143	breqtrrid	$⊢ X \mod T = π \to 0 < X \mod T$
145	35	eqlei2	$⊢ X \mod T = π \to X \mod T \leq π$
146	137 138 142 144 145	eliocd	$⊢ X \mod T = π \to X \mod T \in (0, π]$
147	146	iftrued	$⊢ X \mod T = π \to if (X \mod T \in (0, π], 1, - 1) = 1$
148	147	adantl	$⊢ (X \mod π = 0 \land X \mod T = π) \to if (X \mod T \in (0, π], 1, - 1) = 1$
149		oveq1	$⊢ x = X \to x \mod T = X \mod T$
150	149	breq1d	$⊢ x = X \to (x \mod T < π \leftrightarrow X \mod T < π)$
151	150	ifbid	$⊢ x = X \to if (x \mod T < π, 1, - 1) = if (X \mod T < π, 1, - 1)$
152		1ex	$⊢ 1 \in V$
153		negex	$⊢ - 1 \in V$
154	152 153	ifex	$⊢ if (X \mod T < π, 1, - 1) \in V$
155	151 2 154	fvmpt	$⊢ X \in ℝ \to F (X) = if (X \mod T < π, 1, - 1)$
156	3 155	ax-mp	$⊢ F (X) = if (X \mod T < π, 1, - 1)$
157	140	a1i	$⊢ X \mod T < π \to X \mod T \in ℝ$
158		id	$⊢ X \mod T < π \to X \mod T < π$
159	157 158	ltned	$⊢ X \mod T < π \to X \mod T \neq π$
160	159	necon2bi	$⊢ X \mod T = π \to \neg X \mod T < π$
161	160	iffalsed	$⊢ X \mod T = π \to if (X \mod T < π, 1, - 1) = - 1$
162	156 161	eqtrid	$⊢ X \mod T = π \to F (X) = - 1$
163	162	adantl	$⊢ (X \mod π = 0 \land X \mod T = π) \to F (X) = - 1$
164	148 163	oveq12d	$⊢ (X \mod π = 0 \land X \mod T = π) \to if (X \mod T \in (0, π], 1, - 1) + F (X) = 1 + -1$
165		1pneg1e0	$⊢ 1 + -1 = 0$
166	164 165	eqtrdi	$⊢ (X \mod π = 0 \land X \mod T = π) \to if (X \mod T \in (0, π], 1, - 1) + F (X) = 0$
167	166	oveq1d	$⊢ (X \mod π = 0 \land X \mod T = π) \to \frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2} = \frac{0}{2}$
168	167	adantll	$⊢ ((X \mod T \in (0, π] \land X \mod π = 0) \land X \mod T = π) \to \frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2} = \frac{0}{2}$
169		2cn	$⊢ 2 \in ℂ$
170	169 45	div0i	$⊢ \frac{0}{2} = 0$
171	170	a1i	$⊢ ((X \mod T \in (0, π] \land X \mod π = 0) \land X \mod T = π) \to \frac{0}{2} = 0$
172		iftrue	$⊢ X \mod π = 0 \to if (X \mod π = 0, 0, F (X)) = 0$
173	4 172	eqtr2id	$⊢ X \mod π = 0 \to 0 = Y$
174	173	ad2antlr	$⊢ ((X \mod T \in (0, π] \land X \mod π = 0) \land X \mod T = π) \to 0 = Y$
175	168 171 174	3eqtrrd	$⊢ ((X \mod T \in (0, π] \land X \mod π = 0) \land X \mod T = π) \to Y = \frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2}$
176	136 175	mpdan	$⊢ (X \mod T \in (0, π] \land X \mod π = 0) \to Y = \frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2}$
177		iftrue	$⊢ X \mod T \in (0, π] \to if (X \mod T \in (0, π], 1, - 1) = 1$
178	177	adantr	$⊢ (X \mod T \in (0, π] \land \neg X \mod π = 0) \to if (X \mod T \in (0, π], 1, - 1) = 1$
179	140	a1i	$⊢ (X \mod T \in (0, π] \land \neg X \mod π = 0) \to X \mod T \in ℝ$
180	35	a1i	$⊢ (X \mod T \in (0, π] \land \neg X \mod π = 0) \to π \in ℝ$
181		iocleub	$⊢ (0 \in ℝ^{} \land π \in ℝ^{} \land X \mod T \in (0, π]) \to X \mod T \leq π$
182	128 129 181	mp3an12	$⊢ X \mod T \in (0, π] \to X \mod T \leq π$
183	182	adantr	$⊢ (X \mod T \in (0, π] \land \neg X \mod π = 0) \to X \mod T \leq π$
184		ax-1cn	$⊢ 1 \in ℂ$
185	184 16	mulcomi	$⊢ 1 π = π \cdot 1$
186	84 185	eqtr3i	$⊢ π = π \cdot 1$
187	186	oveq1i	$⊢ π + π 2 ⌊\frac{X}{T}⌋ = π \cdot 1 + π 2 ⌊\frac{X}{T}⌋$
188	169 16	mulcomi	$⊢ 2 π = π \cdot 2$
189	1 188	eqtri	$⊢ T = π \cdot 2$
190	189	oveq1i	$⊢ T ⌊\frac{X}{T}⌋ = π \cdot 2 ⌊\frac{X}{T}⌋$
191	112 63	gtneii	$⊢ T \neq 0$
192	3 60 191	redivcli	$⊢ \frac{X}{T} \in ℝ$
193		flcl	$⊢ \frac{X}{T} \in ℝ \to ⌊\frac{X}{T}⌋ \in ℤ$
194	192 193	ax-mp	$⊢ ⌊\frac{X}{T}⌋ \in ℤ$
195		zcn	$⊢ ⌊\frac{X}{T}⌋ \in ℤ \to ⌊\frac{X}{T}⌋ \in ℂ$
196	194 195	ax-mp	$⊢ ⌊\frac{X}{T}⌋ \in ℂ$
197	16 169 196	mulassi	$⊢ π \cdot 2 ⌊\frac{X}{T}⌋ = π 2 ⌊\frac{X}{T}⌋$
198	190 197	eqtri	$⊢ T ⌊\frac{X}{T}⌋ = π 2 ⌊\frac{X}{T}⌋$
199	198	oveq2i	$⊢ π + T ⌊\frac{X}{T}⌋ = π + π 2 ⌊\frac{X}{T}⌋$
200	169 196	mulcli	$⊢ 2 ⌊\frac{X}{T}⌋ \in ℂ$
201	16 184 200	adddii	$⊢ π (1 + 2 ⌊\frac{X}{T}⌋) = π \cdot 1 + π 2 ⌊\frac{X}{T}⌋$
202	187 199 201	3eqtr4ri	$⊢ π (1 + 2 ⌊\frac{X}{T}⌋) = π + T ⌊\frac{X}{T}⌋$
203	202	a1i	$⊢ π = X \mod T \to π (1 + 2 ⌊\frac{X}{T}⌋) = π + T ⌊\frac{X}{T}⌋$
204		id	$⊢ π = X \mod T \to π = X \mod T$
205		modval	$⊢ (X \in ℝ \land T \in ℝ^{+}) \to X \mod T = X - T ⌊\frac{X}{T}⌋$
206	3 64 205	mp2an	$⊢ X \mod T = X - T ⌊\frac{X}{T}⌋$
207	204 206	eqtrdi	$⊢ π = X \mod T \to π = X - T ⌊\frac{X}{T}⌋$
208	207	oveq1d	$⊢ π = X \mod T \to π + T ⌊\frac{X}{T}⌋ = X - T ⌊\frac{X}{T}⌋ + T ⌊\frac{X}{T}⌋$
209	29	a1i	$⊢ π = X \mod T \to X \in ℂ$
210	60	recni	$⊢ T \in ℂ$
211	210 196	mulcli	$⊢ T ⌊\frac{X}{T}⌋ \in ℂ$
212	211	a1i	$⊢ π = X \mod T \to T ⌊\frac{X}{T}⌋ \in ℂ$
213	209 212	npcand	$⊢ π = X \mod T \to X - T ⌊\frac{X}{T}⌋ + T ⌊\frac{X}{T}⌋ = X$
214	203 208 213	3eqtrrd	$⊢ π = X \mod T \to X = π (1 + 2 ⌊\frac{X}{T}⌋)$
215	214	oveq1d	$⊢ π = X \mod T \to \frac{X}{π} = \frac{π (1 + 2 ⌊\frac{X}{T}⌋)}{π}$
216	184 200	addcli	$⊢ 1 + 2 ⌊\frac{X}{T}⌋ \in ℂ$
217	216 16 37	divcan3i	$⊢ \frac{π (1 + 2 ⌊\frac{X}{T}⌋)}{π} = 1 + 2 ⌊\frac{X}{T}⌋$
218	215 217	eqtrdi	$⊢ π = X \mod T \to \frac{X}{π} = 1 + 2 ⌊\frac{X}{T}⌋$
219		1z	$⊢ 1 \in ℤ$
220		zmulcl	$⊢ (2 \in ℤ \land ⌊\frac{X}{T}⌋ \in ℤ) \to 2 ⌊\frac{X}{T}⌋ \in ℤ$
221	6 194 220	mp2an	$⊢ 2 ⌊\frac{X}{T}⌋ \in ℤ$
222		zaddcl	$⊢ (1 \in ℤ \land 2 ⌊\frac{X}{T}⌋ \in ℤ) \to 1 + 2 ⌊\frac{X}{T}⌋ \in ℤ$
223	219 221 222	mp2an	$⊢ 1 + 2 ⌊\frac{X}{T}⌋ \in ℤ$
224	223	a1i	$⊢ π = X \mod T \to 1 + 2 ⌊\frac{X}{T}⌋ \in ℤ$
225	218 224	eqeltrd	$⊢ π = X \mod T \to \frac{X}{π} \in ℤ$
226	225 10	sylibr	$⊢ π = X \mod T \to X \mod π = 0$
227	226	necon3bi	$⊢ \neg X \mod π = 0 \to π \neq X \mod T$
228	227	adantl	$⊢ (X \mod T \in (0, π] \land \neg X \mod π = 0) \to π \neq X \mod T$
229	179 180 183 228	leneltd	$⊢ (X \mod T \in (0, π] \land \neg X \mod π = 0) \to X \mod T < π$
230		iftrue	$⊢ X \mod T < π \to if (X \mod T < π, 1, - 1) = 1$
231	156 230	eqtrid	$⊢ X \mod T < π \to F (X) = 1$
232	229 231	syl	$⊢ (X \mod T \in (0, π] \land \neg X \mod π = 0) \to F (X) = 1$
233	178 232	oveq12d	$⊢ (X \mod T \in (0, π] \land \neg X \mod π = 0) \to if (X \mod T \in (0, π], 1, - 1) + F (X) = 1 + 1$
234	233	oveq1d	$⊢ (X \mod T \in (0, π] \land \neg X \mod π = 0) \to \frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2} = \frac{1 + 1}{2}$
235		1p1e2	$⊢ 1 + 1 = 2$
236	235	oveq1i	$⊢ \frac{1 + 1}{2} = \frac{2}{2}$
237		2div2e1	$⊢ \frac{2}{2} = 1$
238	236 237	eqtr2i	$⊢ 1 = \frac{1 + 1}{2}$
239	232 238	eqtr2di	$⊢ (X \mod T \in (0, π] \land \neg X \mod π = 0) \to \frac{1 + 1}{2} = F (X)$
240		iffalse	$⊢ \neg X \mod π = 0 \to if (X \mod π = 0, 0, F (X)) = F (X)$
241	4 240	eqtr2id	$⊢ \neg X \mod π = 0 \to F (X) = Y$
242	241	adantl	$⊢ (X \mod T \in (0, π] \land \neg X \mod π = 0) \to F (X) = Y$
243	234 239 242	3eqtrrd	$⊢ (X \mod T \in (0, π] \land \neg X \mod π = 0) \to Y = \frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2}$
244	176 243	pm2.61dan	$⊢ X \mod T \in (0, π] \to Y = \frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2}$
245	132	necon2bi	$⊢ X \mod T = 0 \to \neg X \mod T \in (0, π]$
246	245	iffalsed	$⊢ X \mod T = 0 \to if (X \mod T \in (0, π], 1, - 1) = - 1$
247		id	$⊢ X \mod T = 0 \to X \mod T = 0$
248	247 36	eqbrtrdi	$⊢ X \mod T = 0 \to X \mod T < π$
249	248	iftrued	$⊢ X \mod T = 0 \to if (X \mod T < π, 1, - 1) = 1$
250	156 249	eqtrid	$⊢ X \mod T = 0 \to F (X) = 1$
251	246 250	oveq12d	$⊢ X \mod T = 0 \to if (X \mod T \in (0, π], 1, - 1) + F (X) = - 1 + 1$
252	251	oveq1d	$⊢ X \mod T = 0 \to \frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2} = \frac{- 1 + 1}{2}$
253		neg1cn	$⊢ - 1 \in ℂ$
254	184 253 165	addcomli	$⊢ - 1 + 1 = 0$
255	254	oveq1i	$⊢ \frac{- 1 + 1}{2} = \frac{0}{2}$
256	255 170	eqtri	$⊢ \frac{- 1 + 1}{2} = 0$
257	256	a1i	$⊢ X \mod T = 0 \to \frac{- 1 + 1}{2} = 0$
258	1	oveq2i	$⊢ \frac{X}{T} = \frac{X}{2 π}$
259		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
260	16 37	pm3.2i	$⊢ (π \in ℂ \land π \neq 0)$
261		divdiv1	$⊢ (X \in ℂ \land (2 \in ℂ \land 2 \neq 0) \land (π \in ℂ \land π \neq 0)) \to \frac{\frac{X}{2}}{π} = \frac{X}{2 π}$
262	29 259 260 261	mp3an	$⊢ \frac{\frac{X}{2}}{π} = \frac{X}{2 π}$
263	29 169 16 45 37	divdiv32i	$⊢ \frac{\frac{X}{2}}{π} = \frac{\frac{X}{π}}{2}$
264	258 262 263	3eqtr2i	$⊢ \frac{X}{T} = \frac{\frac{X}{π}}{2}$
265	264	oveq2i	$⊢ 2 (\frac{X}{T}) = 2 (\frac{\frac{X}{π}}{2})$
266	29 16 37	divcli	$⊢ \frac{X}{π} \in ℂ$
267	266 169 45	divcan2i	$⊢ 2 (\frac{\frac{X}{π}}{2}) = \frac{X}{π}$
268	265 267	eqtr2i	$⊢ \frac{X}{π} = 2 (\frac{X}{T})$
269	6	a1i	$⊢ \frac{X}{T} \in ℤ \to 2 \in ℤ$
270		id	$⊢ \frac{X}{T} \in ℤ \to \frac{X}{T} \in ℤ$
271	269 270	zmulcld	$⊢ \frac{X}{T} \in ℤ \to 2 (\frac{X}{T}) \in ℤ$
272	268 271	eqeltrid	$⊢ \frac{X}{T} \in ℤ \to \frac{X}{π} \in ℤ$
273	66 272	sylbi	$⊢ X \mod T = 0 \to \frac{X}{π} \in ℤ$
274	273 10	sylibr	$⊢ X \mod T = 0 \to X \mod π = 0$
275	274	iftrued	$⊢ X \mod T = 0 \to if (X \mod π = 0, 0, F (X)) = 0$
276	4 275	eqtr2id	$⊢ X \mod T = 0 \to 0 = Y$
277	252 257 276	3eqtrrd	$⊢ X \mod T = 0 \to Y = \frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2}$
278	277	adantl	$⊢ (\neg X \mod T \in (0, π] \land X \mod T = 0) \to Y = \frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2}$
279	129	a1i	$⊢ (\neg X \mod T \in (0, π] \land \neg X \mod T = 0) \to π \in ℝ^{*}$
280	60	rexri	$⊢ T \in ℝ^{*}$
281	280	a1i	$⊢ (\neg X \mod T \in (0, π] \land \neg X \mod T = 0) \to T \in ℝ^{*}$
282	140	a1i	$⊢ (\neg X \mod T \in (0, π] \land \neg X \mod T = 0) \to X \mod T \in ℝ$
283		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)$
284	283	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)$
285		olc	$⊢ X \mod T = 0 \to (X \mod T \in (0, π] \lor X \mod T = 0)$
286	285	adantl	$⊢ (X \mod T \leq π \land X \mod T = 0) \to (X \mod T \in (0, π] \lor X \mod T = 0)$
287	128	a1i	$⊢ (X \mod T \leq π \land \neg X \mod T = 0) \to 0 \in ℝ^{*}$
288	129	a1i	$⊢ (X \mod T \leq π \land \neg X \mod T = 0) \to π \in ℝ^{*}$
289	141	a1i	$⊢ (X \mod T \leq π \land \neg X \mod T = 0) \to X \mod T \in ℝ^{*}$
290		0red	$⊢ \neg X \mod T = 0 \to 0 \in ℝ$
291	140	a1i	$⊢ \neg X \mod T = 0 \to X \mod T \in ℝ$
292		modge0	$⊢ (X \in ℝ \land T \in ℝ^{+}) \to 0 \leq X \mod T$
293	3 64 292	mp2an	$⊢ 0 \leq X \mod T$
294	293	a1i	$⊢ \neg X \mod T = 0 \to 0 \leq X \mod T$
295		neqne	$⊢ \neg X \mod T = 0 \to X \mod T \neq 0$
296	290 291 294 295	leneltd	$⊢ \neg X \mod T = 0 \to 0 < X \mod T$
297	296	adantl	$⊢ (X \mod T \leq π \land \neg X \mod T = 0) \to 0 < X \mod T$
298		simpl	$⊢ (X \mod T \leq π \land \neg X \mod T = 0) \to X \mod T \leq π$
299	287 288 289 297 298	eliocd	$⊢ (X \mod T \leq π \land \neg X \mod T = 0) \to X \mod T \in (0, π]$
300	299	orcd	$⊢ (X \mod T \leq π \land \neg X \mod T = 0) \to (X \mod T \in (0, π] \lor X \mod T = 0)$
301	286 300	pm2.61dan	$⊢ X \mod T \leq π \to (X \mod T \in (0, π] \lor X \mod T = 0)$
302	284 301	nsyl	$⊢ (\neg X \mod T \in (0, π] \land \neg X \mod T = 0) \to \neg X \mod T \leq π$
303	35	a1i	$⊢ (\neg X \mod T \in (0, π] \land \neg X \mod T = 0) \to π \in ℝ$
304	303 282	ltnled	$⊢ (\neg X \mod T \in (0, π] \land \neg X \mod T = 0) \to (π < X \mod T \leftrightarrow \neg X \mod T \leq π)$
305	302 304	mpbird	$⊢ (\neg X \mod T \in (0, π] \land \neg X \mod T = 0) \to π < X \mod T$
306		modlt	$⊢ (X \in ℝ \land T \in ℝ^{+}) \to X \mod T < T$
307	3 64 306	mp2an	$⊢ X \mod T < T$
308	307	a1i	$⊢ (\neg X \mod T \in (0, π] \land \neg X \mod T = 0) \to X \mod T < T$
309	279 281 282 305 308	eliood	$⊢ (\neg X \mod T \in (0, π] \land \neg X \mod T = 0) \to X \mod T \in (π, T)$
310	128	a1i	$⊢ X \mod T \in (π, T) \to 0 \in ℝ^{*}$
311	35	a1i	$⊢ X \mod T \in (π, T) \to π \in ℝ$
312	141	a1i	$⊢ X \mod T \in (π, T) \to X \mod T \in ℝ^{*}$
313		ioogtlb	$⊢ (π \in ℝ^{} \land T \in ℝ^{} \land X \mod T \in (π, T)) \to π < X \mod T$
314	129 280 313	mp3an12	$⊢ X \mod T \in (π, T) \to π < X \mod T$
315	310 311 312 314	gtnelioc	$⊢ X \mod T \in (π, T) \to \neg X \mod T \in (0, π]$
316	315	iffalsed	$⊢ X \mod T \in (π, T) \to if (X \mod T \in (0, π], 1, - 1) = - 1$
317	140	a1i	$⊢ X \mod T \in (π, T) \to X \mod T \in ℝ$
318	311 317 314	ltnsymd	$⊢ X \mod T \in (π, T) \to \neg X \mod T < π$
319	318	iffalsed	$⊢ X \mod T \in (π, T) \to if (X \mod T < π, 1, - 1) = - 1$
320	156 319	eqtrid	$⊢ X \mod T \in (π, T) \to F (X) = - 1$
321	316 320	oveq12d	$⊢ X \mod T \in (π, T) \to if (X \mod T \in (0, π], 1, - 1) + F (X) = - 1 + -1$
322	321	oveq1d	$⊢ X \mod T \in (π, T) \to \frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2} = \frac{- 1 + -1}{2}$
323		df-2	$⊢ 2 = 1 + 1$
324	323	negeqi	$⊢ - 2 = - (1 + 1)$
325	184 184	negdii	$⊢ - (1 + 1) = - 1 + -1$
326	324 325	eqtr2i	$⊢ - 1 + -1 = - 2$
327	326	oveq1i	$⊢ \frac{- 1 + -1}{2} = \frac{- 2}{2}$
328		divneg	$⊢ (2 \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to - \frac{2}{2} = \frac{- 2}{2}$
329	169 169 45 328	mp3an	$⊢ - \frac{2}{2} = \frac{- 2}{2}$
330	237	negeqi	$⊢ - \frac{2}{2} = - 1$
331	327 329 330	3eqtr2i	$⊢ \frac{- 1 + -1}{2} = - 1$
332	331	a1i	$⊢ X \mod T \in (π, T) \to \frac{- 1 + -1}{2} = - 1$
333	4	a1i	$⊢ X \mod T \in (π, T) \to Y = if (X \mod π = 0, 0, F (X))$
334	311 317	ltnled	$⊢ X \mod T \in (π, T) \to (π < X \mod T \leftrightarrow \neg X \mod T \leq π)$
335	314 334	mpbid	$⊢ X \mod T \in (π, T) \to \neg X \mod T \leq π$
336	247 113	eqbrtrdi	$⊢ X \mod T = 0 \to X \mod T \leq π$
337	336	adantl	$⊢ (X \mod π = 0 \land X \mod T = 0) \to X \mod T \leq π$
338	127	orcanai	$⊢ (X \mod π = 0 \land \neg X \mod T = 0) \to X \mod T = π$
339	338 145	syl	$⊢ (X \mod π = 0 \land \neg X \mod T = 0) \to X \mod T \leq π$
340	337 339	pm2.61dan	$⊢ X \mod π = 0 \to X \mod T \leq π$
341	335 340	nsyl	$⊢ X \mod T \in (π, T) \to \neg X \mod π = 0$
342	341	iffalsed	$⊢ X \mod T \in (π, T) \to if (X \mod π = 0, 0, F (X)) = F (X)$
343	333 342 320	3eqtrrd	$⊢ X \mod T \in (π, T) \to - 1 = Y$
344	322 332 343	3eqtrrd	$⊢ X \mod T \in (π, T) \to Y = \frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2}$
345	309 344	syl	$⊢ (\neg X \mod T \in (0, π] \land \neg X \mod T = 0) \to Y = \frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2}$
346	278 345	pm2.61dan	$⊢ \neg X \mod T \in (0, π] \to Y = \frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2}$
347	244 346	pm2.61i	$⊢ Y = \frac{if (X \mod T \in (0, π], 1, - 1) + F (X)}{2}$

Metamath Proof Explorer

Theorem fourierswlem

Proof