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

Metamath Proof Explorer

Theorem fourierswlem

Proof