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 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 mulid2i 
 |-  ( 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 syl5eq 
 |-  ( ( 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 syl5eq 
 |-  ( ( 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 syl5eq 
 |-  ( ( 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 syl5eq 
 |-  ( ( 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 )