Metamath Proof Explorer

Theorem 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 )