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 x. _pi )
	fourierswlem.f	\|- F = ( x e. RR \|-> if ( ( x mod T ) < _pi , 1 , -u 1 ) )
	fourierswlem.x	\|- X e. RR
	fourierswlem.y	\|- Y = if ( ( X mod _pi ) = 0 , 0 , ( F ` X ) )
Assertion	fourierswlem	\|- Y = ( ( if ( ( X mod T ) e. ( 0 (,] _pi ) , 1 , -u 1 ) + ( F ` X ) ) / 2 )

Proof

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

Metamath Proof Explorer

Theorem fourierswlem

Proof