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

Metamath Proof Explorer

Theorem fourierswlem

Proof