Metamath Proof Explorer

Theorem fouriersw

Description: Fourier series convergence, for the square wave function. Where F is discontinuous, the series converges to 0 , the average value of the left and the right limits. Notice that F is an odd function and its Fourier expansion has only sine terms (coefficients for cosine terms are zero). (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fouriersw.t ⊢T=2⁢π
fouriersw.f ⊢F=x∈ℝ⟼ifxmodT<π1−1
fouriersw.x ⊢X∈ℝ
fouriersw.z ⊢S=n∈ℕ⟼sin⁡2⁢n−1⁢X2⁢n−1
fouriersw.y ⊢Y=ifXmodπ=00F⁡X
Assertion fouriersw ⊢4π⁢∑k∈ℕsin⁡2⁢k−1⁢X2⁢k−1=Y∧seq1+S⇝π4⁢Y

Proof

Step Hyp Ref Expression
1 fouriersw.t ⊢T=2⁢π
2 fouriersw.f ⊢F=x∈ℝ⟼ifxmodT<π1−1
3 fouriersw.x ⊢X∈ℝ
4 fouriersw.z ⊢S=n∈ℕ⟼sin⁡2⁢n−1⁢X2⁢n−1
5 fouriersw.y ⊢Y=ifXmodπ=00F⁡X
6 nnuz ⊢ℕ=ℤ≥1
7 1zzd ⊢⊤→1∈ℤ
8 eqidd ⊢k∈ℕ→n∈ℕ⟼sin⁡2⁢n−1⁢X2⁢n−1=n∈ℕ⟼sin⁡2⁢n−1⁢X2⁢n−1
9 oveq2 ⊢n=k→2⁢n=2⁢k
10 9 oveq1d ⊢n=k→2⁢n−1=2⁢k−1
11 10 oveq1d ⊢n=k→2⁢n−1⁢X=2⁢k−1⁢X
12 11 fveq2d ⊢n=k→sin⁡2⁢n−1⁢X=sin⁡2⁢k−1⁢X
13 12 10 oveq12d ⊢n=k→sin⁡2⁢n−1⁢X2⁢n−1=sin⁡2⁢k−1⁢X2⁢k−1
14 13 adantl ⊢k∈ℕ∧n=k→sin⁡2⁢n−1⁢X2⁢n−1=sin⁡2⁢k−1⁢X2⁢k−1
15 id ⊢k∈ℕ→k∈ℕ
16 ovex ⊢sin⁡2⁢k−1⁢X2⁢k−1∈V
17 16 a1i ⊢k∈ℕ→sin⁡2⁢k−1⁢X2⁢k−1∈V
18 8 14 15 17 fvmptd ⊢k∈ℕ→n∈ℕ⟼sin⁡2⁢n−1⁢X2⁢n−1⁡k=sin⁡2⁢k−1⁢X2⁢k−1
19 18 adantl ⊢⊤∧k∈ℕ→n∈ℕ⟼sin⁡2⁢n−1⁢X2⁢n−1⁡k=sin⁡2⁢k−1⁢X2⁢k−1
20 2z ⊢2∈ℤ
21 20 a1i ⊢k∈ℕ→2∈ℤ
22 nnz ⊢k∈ℕ→k∈ℤ
23 21 22 zmulcld ⊢k∈ℕ→2⁢k∈ℤ
24 1zzd ⊢k∈ℕ→1∈ℤ
25 23 24 zsubcld ⊢k∈ℕ→2⁢k−1∈ℤ
26 25 zcnd ⊢k∈ℕ→2⁢k−1∈ℂ
27 3 recni ⊢X∈ℂ
28 27 a1i ⊢k∈ℕ→X∈ℂ
29 26 28 mulcld ⊢k∈ℕ→2⁢k−1⁢X∈ℂ
30 29 sincld ⊢k∈ℕ→sin⁡2⁢k−1⁢X∈ℂ
31 0red ⊢k∈ℕ→0∈ℝ
32 2re ⊢2∈ℝ
33 32 a1i ⊢k∈ℕ→2∈ℝ
34 1red ⊢k∈ℕ→1∈ℝ
35 33 34 remulcld ⊢k∈ℕ→2⋅1∈ℝ
36 35 34 resubcld ⊢k∈ℕ→2⋅1−1∈ℝ
37 25 zred ⊢k∈ℕ→2⁢k−1∈ℝ
38 0lt1 ⊢0<1
39 2t1e2 ⊢2⋅1=2
40 39 oveq1i ⊢2⋅1−1=2−1
41 2m1e1 ⊢2−1=1
42 40 41 eqtr2i ⊢1=2⋅1−1
43 38 42 breqtri ⊢0<2⋅1−1
44 43 a1i ⊢k∈ℕ→0<2⋅1−1
45 23 zred ⊢k∈ℕ→2⁢k∈ℝ
46 nnre ⊢k∈ℕ→k∈ℝ
47 0le2 ⊢0≤2
48 47 a1i ⊢k∈ℕ→0≤2
49 nnge1 ⊢k∈ℕ→1≤k
50 34 46 33 48 49 lemul2ad ⊢k∈ℕ→2⋅1≤2⁢k
51 35 45 34 50 lesub1dd ⊢k∈ℕ→2⋅1−1≤2⁢k−1
52 31 36 37 44 51 ltletrd ⊢k∈ℕ→0<2⁢k−1
53 31 52 gtned ⊢k∈ℕ→2⁢k−1≠0
54 30 26 53 divcld ⊢k∈ℕ→sin⁡2⁢k−1⁢X2⁢k−1∈ℂ
55 54 adantl ⊢⊤∧k∈ℕ→sin⁡2⁢k−1⁢X2⁢k−1∈ℂ
56 picn ⊢π∈ℂ
57 56 a1i ⊢⊤→π∈ℂ
58 4cn ⊢4∈ℂ
59 58 a1i ⊢⊤→4∈ℂ
60 4ne0 ⊢4≠0
61 60 a1i ⊢⊤→4≠0
62 57 59 61 divcld ⊢⊤→π4∈ℂ
63 eqid ⊢n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X=n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X
64 0cnd ⊢n∈ℕ→0∈ℂ
65 58 a1i ⊢n∈ℕ→4∈ℂ
66 nncn ⊢n∈ℕ→n∈ℂ
67 mulcl ⊢n∈ℂ∧π∈ℂ→n⁢π∈ℂ
68 66 56 67 sylancl ⊢n∈ℕ→n⁢π∈ℂ
69 56 a1i ⊢n∈ℕ→π∈ℂ
70 nnne0 ⊢n∈ℕ→n≠0
71 0re ⊢0∈ℝ
72 pipos ⊢0<π
73 71 72 gtneii ⊢π≠0
74 73 a1i ⊢n∈ℕ→π≠0
75 66 69 70 74 mulne0d ⊢n∈ℕ→n⁢π≠0
76 65 68 75 divcld ⊢n∈ℕ→4n⁢π∈ℂ
77 27 a1i ⊢n∈ℕ→X∈ℂ
78 66 77 mulcld ⊢n∈ℕ→n⁢X∈ℂ
79 78 sincld ⊢n∈ℕ→sin⁡n⁢X∈ℂ
80 76 79 mulcld ⊢n∈ℕ→4n⁢π⁢sin⁡n⁢X∈ℂ
81 64 80 ifcld ⊢n∈ℕ→if2∥n04n⁢π⁢sin⁡n⁢X∈ℂ
82 63 81 fmpti ⊢n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X:ℕ⟶ℂ
83 82 a1i ⊢⊤→n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X:ℕ⟶ℂ
84 eqidd ⊢k∈ℕ→n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X=n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X
85 breq2 ⊢n=k→2∥n↔2∥k
86 oveq1 ⊢n=k→n⁢π=k⁢π
87 86 oveq2d ⊢n=k→4n⁢π=4k⁢π
88 oveq1 ⊢n=k→n⁢X=k⁢X
89 88 fveq2d ⊢n=k→sin⁡n⁢X=sin⁡k⁢X
90 87 89 oveq12d ⊢n=k→4n⁢π⁢sin⁡n⁢X=4k⁢π⁢sin⁡k⁢X
91 85 90 ifbieq2d ⊢n=k→if2∥n04n⁢π⁢sin⁡n⁢X=if2∥k04k⁢π⁢sin⁡k⁢X
92 91 adantl ⊢k∈ℕ∧n=k→if2∥n04n⁢π⁢sin⁡n⁢X=if2∥k04k⁢π⁢sin⁡k⁢X
93 c0ex ⊢0∈V
94 ovex ⊢4k⁢π⁢sin⁡k⁢X∈V
95 93 94 ifex ⊢if2∥k04k⁢π⁢sin⁡k⁢X∈V
96 95 a1i ⊢k∈ℕ→if2∥k04k⁢π⁢sin⁡k⁢X∈V
97 84 92 15 96 fvmptd ⊢k∈ℕ→n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X⁡k=if2∥k04k⁢π⁢sin⁡k⁢X
98 97 adantr ⊢k∈ℕ∧k2∈ℕ→n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X⁡k=if2∥k04k⁢π⁢sin⁡k⁢X
99 simpr ⊢k∈ℕ∧k2∈ℕ→k2∈ℕ
100 simpl ⊢k∈ℕ∧k2∈ℕ→k∈ℕ
101 2nn ⊢2∈ℕ
102 nndivdvds ⊢k∈ℕ∧2∈ℕ→2∥k↔k2∈ℕ
103 100 101 102 sylancl ⊢k∈ℕ∧k2∈ℕ→2∥k↔k2∈ℕ
104 99 103 mpbird ⊢k∈ℕ∧k2∈ℕ→2∥k
105 104 iftrued ⊢k∈ℕ∧k2∈ℕ→if2∥k04k⁢π⁢sin⁡k⁢X=0
106 98 105 eqtrd ⊢k∈ℕ∧k2∈ℕ→n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X⁡k=0
107 106 3adant1 ⊢⊤∧k∈ℕ∧k2∈ℕ→n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X⁡k=0
108 1re ⊢1∈ℝ
109 108 renegcli ⊢−1∈ℝ
110 108 109 ifcli ⊢ifxmodT<π1−1∈ℝ
111 110 a1i ⊢x∈ℝ→ifxmodT<π1−1∈ℝ
112 2 111 fmpti ⊢F:ℝ⟶ℝ
113 oveq1 ⊢x=y→xmodT=ymodT
114 113 breq1d ⊢x=y→xmodT<π↔ymodT<π
115 114 ifbid ⊢x=y→ifxmodT<π1−1=ifymodT<π1−1
116 115 cbvmptv ⊢x∈ℝ⟼ifxmodT<π1−1=y∈ℝ⟼ifymodT<π1−1
117 2 116 eqtri ⊢F=y∈ℝ⟼ifymodT<π1−1
118 117 a1i ⊢x∈ℝ→F=y∈ℝ⟼ifymodT<π1−1
119 oveq1 ⊢y=x+T→ymodT=x+TmodT
120 pire ⊢π∈ℝ
121 32 120 remulcli ⊢2⁢π∈ℝ
122 1 121 eqeltri ⊢T∈ℝ
123 122 recni ⊢T∈ℂ
124 123 mullidi ⊢1⁢T=T
125 124 eqcomi ⊢T=1⁢T
126 125 oveq2i ⊢x+T=x+1⁢T
127 126 oveq1i ⊢x+TmodT=x+1⁢TmodT
128 119 127 eqtrdi ⊢y=x+T→ymodT=x+1⁢TmodT
129 128 adantl ⊢x∈ℝ∧y=x+T→ymodT=x+1⁢TmodT
130 simpl ⊢x∈ℝ∧y=x+T→x∈ℝ
131 2pos ⊢0<2
132 32 120 131 72 mulgt0ii ⊢0<2⁢π
133 1 eqcomi ⊢2⁢π=T
134 132 133 breqtri ⊢0<T
135 122 134 elrpii ⊢T∈ℝ+
136 135 a1i ⊢x∈ℝ∧y=x+T→T∈ℝ+
137 1zzd ⊢x∈ℝ∧y=x+T→1∈ℤ
138 modcyc ⊢x∈ℝ∧T∈ℝ+∧1∈ℤ→x+1⁢TmodT=xmodT
139 130 136 137 138 syl3anc ⊢x∈ℝ∧y=x+T→x+1⁢TmodT=xmodT
140 129 139 eqtrd ⊢x∈ℝ∧y=x+T→ymodT=xmodT
141 140 breq1d ⊢x∈ℝ∧y=x+T→ymodT<π↔xmodT<π
142 141 ifbid ⊢x∈ℝ∧y=x+T→ifymodT<π1−1=ifxmodT<π1−1
143 id ⊢x∈ℝ→x∈ℝ
144 122 a1i ⊢x∈ℝ→T∈ℝ
145 143 144 readdcld ⊢x∈ℝ→x+T∈ℝ
146 118 142 145 111 fvmptd ⊢x∈ℝ→F⁡x+T=ifxmodT<π1−1
147 2 fvmpt2 ⊢x∈ℝ∧ifxmodT<π1−1∈ℝ→F⁡x=ifxmodT<π1−1
148 110 147 mpan2 ⊢x∈ℝ→F⁡x=ifxmodT<π1−1
149 146 148 eqtr4d ⊢x∈ℝ→F⁡x+T=F⁡x
150 eqid ⊢Fℝ′↾−ππ=Fℝ′↾−ππ
151 snfi ⊢0∈Fin
152 eldifi ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ→x∈−ππ
153 0xr ⊢0∈ℝ*
154 153 a1i ⊢x∈−ππ∧0<x→0∈ℝ*
155 120 rexri ⊢π∈ℝ*
156 155 a1i ⊢x∈−ππ∧0<x→π∈ℝ*
157 elioore ⊢x∈−ππ→x∈ℝ
158 157 adantr ⊢x∈−ππ∧0<x→x∈ℝ
159 simpr ⊢x∈−ππ∧0<x→0<x
160 120 renegcli ⊢−π∈ℝ
161 160 rexri ⊢−π∈ℝ*
162 iooltub ⊢−π∈ℝ*∧π∈ℝ*∧x∈−ππ→x<π
163 161 155 162 mp3an12 ⊢x∈−ππ→x<π
164 163 adantr ⊢x∈−ππ∧0<x→x<π
165 154 156 158 159 164 eliood ⊢x∈−ππ∧0<x→x∈0π
166 negpilt0 ⊢−π<0
167 160 71 166 ltleii ⊢−π≤0
168 iooss1 ⊢−π∈ℝ*∧−π≤0→0π⊆−ππ
169 161 167 168 mp2an ⊢0π⊆−ππ
170 169 sseli ⊢x∈0π→x∈−ππ
171 2 reseq1i ⊢F↾0π=x∈ℝ⟼ifxmodT<π1−1↾0π
172 ioossre ⊢0π⊆ℝ
173 resmpt ⊢0π⊆ℝ→x∈ℝ⟼ifxmodT<π1−1↾0π=x∈0π⟼ifxmodT<π1−1
174 172 173 ax-mp ⊢x∈ℝ⟼ifxmodT<π1−1↾0π=x∈0π⟼ifxmodT<π1−1
175 elioore ⊢x∈0π→x∈ℝ
176 135 a1i ⊢x∈0π→T∈ℝ+
177 0red ⊢x∈0π→0∈ℝ
178 ioogtlb ⊢0∈ℝ*∧π∈ℝ*∧x∈0π→0<x
179 153 155 178 mp3an12 ⊢x∈0π→0<x
180 177 175 179 ltled ⊢x∈0π→0≤x
181 120 a1i ⊢x∈0π→π∈ℝ
182 122 a1i ⊢x∈0π→T∈ℝ
183 170 163 syl ⊢x∈0π→x<π
184 pirp ⊢π∈ℝ+
185 2timesgt ⊢π∈ℝ+→π<2⁢π
186 184 185 ax-mp ⊢π<2⁢π
187 186 133 breqtri ⊢π<T
188 187 a1i ⊢x∈0π→π<T
189 175 181 182 183 188 lttrd ⊢x∈0π→x<T
190 modid ⊢x∈ℝ∧T∈ℝ+∧0≤x∧x<T→xmodT=x
191 175 176 180 189 190 syl22anc ⊢x∈0π→xmodT=x
192 191 183 eqbrtrd ⊢x∈0π→xmodT<π
193 192 iftrued ⊢x∈0π→ifxmodT<π1−1=1
194 193 mpteq2ia ⊢x∈0π⟼ifxmodT<π1−1=x∈0π⟼1
195 171 174 194 3eqtrri ⊢x∈0π⟼1=F↾0π
196 195 oveq2i ⊢dx∈0π1dℝx=ℝDF↾0π
197 reelprrecn ⊢ℝ∈ℝℂ
198 197 a1i ⊢⊤→ℝ∈ℝℂ
199 iooretop ⊢0π∈topGen⁡ran⁡.
200 eqid ⊢TopOpen⁡ℂfld=TopOpen⁡ℂfld
201 200 tgioo2 ⊢topGen⁡ran⁡.=TopOpen⁡ℂfld↾𝑡ℝ
202 199 201 eleqtri ⊢0π∈TopOpen⁡ℂfld↾𝑡ℝ
203 202 a1i ⊢⊤→0π∈TopOpen⁡ℂfld↾𝑡ℝ
204 1cnd ⊢⊤→1∈ℂ
205 198 203 204 dvmptconst ⊢⊤→dx∈0π1dℝx=x∈0π⟼0
206 205 mptru ⊢dx∈0π1dℝx=x∈0π⟼0
207 ssid ⊢ℝ⊆ℝ
208 ax-resscn ⊢ℝ⊆ℂ
209 fss ⊢F:ℝ⟶ℝ∧ℝ⊆ℂ→F:ℝ⟶ℂ
210 112 208 209 mp2an ⊢F:ℝ⟶ℂ
211 dvresioo ⊢ℝ⊆ℝ∧F:ℝ⟶ℂ→ℝDF↾0π=Fℝ′↾0π
212 207 210 211 mp2an ⊢ℝDF↾0π=Fℝ′↾0π
213 196 206 212 3eqtr3i ⊢x∈0π⟼0=Fℝ′↾0π
214 213 dmeqi ⊢dom⁡x∈0π⟼0=dom⁡Fℝ′↾0π
215 eqid ⊢x∈0π⟼0=x∈0π⟼0
216 93 215 dmmpti ⊢dom⁡x∈0π⟼0=0π
217 214 216 eqtr3i ⊢dom⁡Fℝ′↾0π=0π
218 ssdmres ⊢0π⊆dom⁡Fℝ′↔dom⁡Fℝ′↾0π=0π
219 217 218 mpbir ⊢0π⊆dom⁡Fℝ′
220 219 sseli ⊢x∈0π→x∈dom⁡Fℝ′
221 170 220 elind ⊢x∈0π→x∈−ππ∩dom⁡Fℝ′
222 dmres ⊢dom⁡Fℝ′↾−ππ=−ππ∩dom⁡Fℝ′
223 221 222 eleqtrrdi ⊢x∈0π→x∈dom⁡Fℝ′↾−ππ
224 165 223 syl ⊢x∈−ππ∧0<x→x∈dom⁡Fℝ′↾−ππ
225 224 adantlr ⊢x∈−ππ∧¬x=0∧0<x→x∈dom⁡Fℝ′↾−ππ
226 161 a1i ⊢x∈−ππ∧¬x=0∧¬0<x→−π∈ℝ*
227 153 a1i ⊢x∈−ππ∧¬x=0∧¬0<x→0∈ℝ*
228 157 ad2antrr ⊢x∈−ππ∧¬x=0∧¬0<x→x∈ℝ
229 ioogtlb ⊢−π∈ℝ*∧π∈ℝ*∧x∈−ππ→−π<x
230 161 155 229 mp3an12 ⊢x∈−ππ→−π<x
231 230 ad2antrr ⊢x∈−ππ∧¬x=0∧¬0<x→−π<x
232 0red ⊢x∈−ππ∧¬x=0∧¬0<x→0∈ℝ
233 neqne ⊢¬x=0→x≠0
234 233 ad2antlr ⊢x∈−ππ∧¬x=0∧¬0<x→x≠0
235 simpr ⊢x∈−ππ∧¬x=0∧¬0<x→¬0<x
236 228 232 234 235 lttri5d ⊢x∈−ππ∧¬x=0∧¬0<x→x<0
237 226 227 228 231 236 eliood ⊢x∈−ππ∧¬x=0∧¬0<x→x∈−π0
238 71 120 72 ltleii ⊢0≤π
239 iooss2 ⊢π∈ℝ*∧0≤π→−π0⊆−ππ
240 155 238 239 mp2an ⊢−π0⊆−ππ
241 240 sseli ⊢x∈−π0→x∈−ππ
242 2 reseq1i ⊢F↾−π0=x∈ℝ⟼ifxmodT<π1−1↾−π0
243 ioossre ⊢−π0⊆ℝ
244 resmpt ⊢−π0⊆ℝ→x∈ℝ⟼ifxmodT<π1−1↾−π0=x∈−π0⟼ifxmodT<π1−1
245 243 244 ax-mp ⊢x∈ℝ⟼ifxmodT<π1−1↾−π0=x∈−π0⟼ifxmodT<π1−1
246 120 a1i ⊢x∈−π0→π∈ℝ
247 elioore ⊢x∈−π0→x∈ℝ
248 135 a1i ⊢x∈−π0→T∈ℝ+
249 247 248 modcld ⊢x∈−π0→xmodT∈ℝ
250 247 145 syl ⊢x∈−π0→x+T∈ℝ
251 56 2timesi ⊢2⁢π=π+π
252 1 251 eqtri ⊢T=π+π
253 252 oveq2i ⊢-π+T=−π+π+π
254 negpicn ⊢−π∈ℂ
255 254 56 56 addassi ⊢−π+π+π=−π+π+π
256 255 eqcomi ⊢−π+π+π=−π+π+π
257 56 negidi ⊢π+−π=0
258 56 254 257 addcomli ⊢-π+π=0
259 258 oveq1i ⊢−π+π+π=0+π
260 56 addlidi ⊢0+π=π
261 259 260 eqtri ⊢−π+π+π=π
262 253 256 261 3eqtrri ⊢π=-π+T
263 262 a1i ⊢x∈−π0→π=-π+T
264 160 a1i ⊢x∈−π0→−π∈ℝ
265 122 a1i ⊢x∈−π0→T∈ℝ
266 241 230 syl ⊢x∈−π0→−π<x
267 264 247 265 266 ltadd1dd ⊢x∈−π0→-π+T<x+T
268 263 267 eqbrtrd ⊢x∈−π0→π<x+T
269 246 250 268 ltled ⊢x∈−π0→π≤x+T
270 0red ⊢x∈−π0→0∈ℝ
271 160 122 readdcli ⊢-π+T∈ℝ
272 271 a1i ⊢x∈−π0→-π+T∈ℝ
273 72 a1i ⊢x∈−π0→0<π
274 273 262 breqtrdi ⊢x∈−π0→0<-π+T
275 270 272 250 274 267 lttrd ⊢x∈−π0→0<x+T
276 270 250 275 ltled ⊢x∈−π0→0≤x+T
277 247 recnd ⊢x∈−π0→x∈ℂ
278 123 a1i ⊢x∈−π0→T∈ℂ
279 277 278 addcomd ⊢x∈−π0→x+T=T+x
280 iooltub ⊢−π∈ℝ*∧0∈ℝ*∧x∈−π0→x<0
281 161 153 280 mp3an12 ⊢x∈−π0→x<0
282 ltaddneg ⊢x∈ℝ∧T∈ℝ→x<0↔T+x<T
283 247 122 282 sylancl ⊢x∈−π0→x<0↔T+x<T
284 281 283 mpbid ⊢x∈−π0→T+x<T
285 279 284 eqbrtrd ⊢x∈−π0→x+T<T
286 276 285 jca ⊢x∈−π0→0≤x+T∧x+T<T
287 modid2 ⊢x+T∈ℝ∧T∈ℝ+→x+TmodT=x+T↔0≤x+T∧x+T<T
288 250 135 287 sylancl ⊢x∈−π0→x+TmodT=x+T↔0≤x+T∧x+T<T
289 286 288 mpbird ⊢x∈−π0→x+TmodT=x+T
290 127 a1i ⊢x∈ℝ→x+TmodT=x+1⁢TmodT
291 135 a1i ⊢x∈ℝ→T∈ℝ+
292 1zzd ⊢x∈ℝ→1∈ℤ
293 143 291 292 138 syl3anc ⊢x∈ℝ→x+1⁢TmodT=xmodT
294 290 293 eqtrd ⊢x∈ℝ→x+TmodT=xmodT
295 247 294 syl ⊢x∈−π0→x+TmodT=xmodT
296 289 295 eqtr3d ⊢x∈−π0→x+T=xmodT
297 269 296 breqtrd ⊢x∈−π0→π≤xmodT
298 246 249 297 lensymd ⊢x∈−π0→¬xmodT<π
299 298 iffalsed ⊢x∈−π0→ifxmodT<π1−1=−1
300 299 mpteq2ia ⊢x∈−π0⟼ifxmodT<π1−1=x∈−π0⟼−1
301 242 245 300 3eqtrri ⊢x∈−π0⟼−1=F↾−π0
302 301 oveq2i ⊢dx∈−π0−1dℝx=ℝDF↾−π0
303 iooretop ⊢−π0∈topGen⁡ran⁡.
304 303 201 eleqtri ⊢−π0∈TopOpen⁡ℂfld↾𝑡ℝ
305 304 a1i ⊢⊤→−π0∈TopOpen⁡ℂfld↾𝑡ℝ
306 204 negcld ⊢⊤→−1∈ℂ
307 198 305 306 dvmptconst ⊢⊤→dx∈−π0−1dℝx=x∈−π0⟼0
308 307 mptru ⊢dx∈−π0−1dℝx=x∈−π0⟼0
309 dvresioo ⊢ℝ⊆ℝ∧F:ℝ⟶ℂ→ℝDF↾−π0=Fℝ′↾−π0
310 207 210 309 mp2an ⊢ℝDF↾−π0=Fℝ′↾−π0
311 302 308 310 3eqtr3i ⊢x∈−π0⟼0=Fℝ′↾−π0
312 311 dmeqi ⊢dom⁡x∈−π0⟼0=dom⁡Fℝ′↾−π0
313 eqid ⊢x∈−π0⟼0=x∈−π0⟼0
314 93 313 dmmpti ⊢dom⁡x∈−π0⟼0=−π0
315 312 314 eqtr3i ⊢dom⁡Fℝ′↾−π0=−π0
316 ssdmres ⊢−π0⊆dom⁡Fℝ′↔dom⁡Fℝ′↾−π0=−π0
317 315 316 mpbir ⊢−π0⊆dom⁡Fℝ′
318 317 sseli ⊢x∈−π0→x∈dom⁡Fℝ′
319 241 318 elind ⊢x∈−π0→x∈−ππ∩dom⁡Fℝ′
320 319 222 eleqtrrdi ⊢x∈−π0→x∈dom⁡Fℝ′↾−ππ
321 237 320 syl ⊢x∈−ππ∧¬x=0∧¬0<x→x∈dom⁡Fℝ′↾−ππ
322 225 321 pm2.61dan ⊢x∈−ππ∧¬x=0→x∈dom⁡Fℝ′↾−ππ
323 152 322 sylan ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ∧¬x=0→x∈dom⁡Fℝ′↾−ππ
324 eldifn ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ→¬x∈dom⁡Fℝ′↾−ππ
325 324 adantr ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ∧¬x=0→¬x∈dom⁡Fℝ′↾−ππ
326 323 325 condan ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ→x=0
327 velsn ⊢x∈0↔x=0
328 326 327 sylibr ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ→x∈0
329 328 ssriv ⊢−ππ∖dom⁡Fℝ′↾−ππ⊆0
330 ssfi ⊢0∈Fin∧−ππ∖dom⁡Fℝ′↾−ππ⊆0→−ππ∖dom⁡Fℝ′↾−ππ∈Fin
331 151 329 330 mp2an ⊢−ππ∖dom⁡Fℝ′↾−ππ∈Fin
332 inss1 ⊢−ππ∩dom⁡Fℝ′⊆−ππ
333 222 332 eqsstri ⊢dom⁡Fℝ′↾−ππ⊆−ππ
334 ioosscn ⊢−ππ⊆ℂ
335 333 334 sstri ⊢dom⁡Fℝ′↾−ππ⊆ℂ
336 335 a1i ⊢⊤→dom⁡Fℝ′↾−ππ⊆ℂ
337 dvf ⊢Fℝ′:dom⁡Fℝ′⟶ℂ
338 fresin ⊢Fℝ′:dom⁡Fℝ′⟶ℂ→Fℝ′↾−ππ:dom⁡Fℝ′∩−ππ⟶ℂ
339 ffdm ⊢Fℝ′↾−ππ:dom⁡Fℝ′∩−ππ⟶ℂ→Fℝ′↾−ππ:dom⁡Fℝ′↾−ππ⟶ℂ∧dom⁡Fℝ′↾−ππ⊆dom⁡Fℝ′∩−ππ
340 337 338 339 mp2b ⊢Fℝ′↾−ππ:dom⁡Fℝ′↾−ππ⟶ℂ∧dom⁡Fℝ′↾−ππ⊆dom⁡Fℝ′∩−ππ
341 340 simpli ⊢Fℝ′↾−ππ:dom⁡Fℝ′↾−ππ⟶ℂ
342 341 a1i ⊢⊤→Fℝ′↾−ππ:dom⁡Fℝ′↾−ππ⟶ℂ
343 161 a1i ⊢x∈dom⁡Fℝ′↾−ππ∧x<0→−π∈ℝ*
344 153 a1i ⊢x∈dom⁡Fℝ′↾−ππ∧x<0→0∈ℝ*
345 ioossre ⊢−ππ⊆ℝ
346 333 sseli ⊢x∈dom⁡Fℝ′↾−ππ→x∈−ππ
347 345 346 sselid ⊢x∈dom⁡Fℝ′↾−ππ→x∈ℝ
348 347 adantr ⊢x∈dom⁡Fℝ′↾−ππ∧x<0→x∈ℝ
349 346 230 syl ⊢x∈dom⁡Fℝ′↾−ππ→−π<x
350 349 adantr ⊢x∈dom⁡Fℝ′↾−ππ∧x<0→−π<x
351 simpr ⊢x∈dom⁡Fℝ′↾−ππ∧x<0→x<0
352 343 344 348 350 351 eliood ⊢x∈dom⁡Fℝ′↾−ππ∧x<0→x∈−π0
353 elun1 ⊢x∈−π0→x∈−π0∪0π
354 352 353 syl ⊢x∈dom⁡Fℝ′↾−ππ∧x<0→x∈−π0∪0π
355 simpl ⊢x∈dom⁡Fℝ′↾−ππ∧¬x<0→x∈dom⁡Fℝ′↾−ππ
356 0red ⊢x∈dom⁡Fℝ′↾−ππ∧¬x<0→0∈ℝ
357 347 adantr ⊢x∈dom⁡Fℝ′↾−ππ∧¬x<0→x∈ℝ
358 simpr ⊢x∈dom⁡Fℝ′↾−ππ∧¬x<0→¬x<0
359 356 357 358 nltled ⊢x∈dom⁡Fℝ′↾−ππ∧¬x<0→0≤x
360 id ⊢x=0→x=0
361 207 a1i ⊢⊤→ℝ⊆ℝ
362 eqid ⊢topGen⁡ran⁡.=topGen⁡ran⁡.
363 210 a1i ⊢⊤→F:ℝ⟶ℂ
364 0red ⊢⊤→0∈ℝ
365 mnfxr ⊢−∞∈ℝ*
366 365 a1i ⊢⊤→−∞∈ℝ*
367 364 mnfltd ⊢⊤→−∞<0
368 362 366 364 367 lptioo2 ⊢⊤→0∈limPt⁡topGen⁡ran⁡.⁡−∞0
369 incom ⊢ℝ∩−∞0=−∞0∩ℝ
370 ioossre ⊢−∞0⊆ℝ
371 df-ss ⊢−∞0⊆ℝ↔−∞0∩ℝ=−∞0
372 370 371 mpbi ⊢−∞0∩ℝ=−∞0
373 369 372 eqtr2i ⊢−∞0=ℝ∩−∞0
374 373 fveq2i ⊢limPt⁡topGen⁡ran⁡.⁡−∞0=limPt⁡topGen⁡ran⁡.⁡ℝ∩−∞0
375 368 374 eleqtrdi ⊢⊤→0∈limPt⁡topGen⁡ran⁡.⁡ℝ∩−∞0
376 pnfxr ⊢+∞∈ℝ*
377 376 a1i ⊢⊤→+∞∈ℝ*
378 364 ltpnfd ⊢⊤→0<+∞
379 362 364 377 378 lptioo1 ⊢⊤→0∈limPt⁡topGen⁡ran⁡.⁡0+∞
380 incom ⊢ℝ∩0+∞=0+∞∩ℝ
381 ioossre ⊢0+∞⊆ℝ
382 df-ss ⊢0+∞⊆ℝ↔0+∞∩ℝ=0+∞
383 381 382 mpbi ⊢0+∞∩ℝ=0+∞
384 380 383 eqtr2i ⊢0+∞=ℝ∩0+∞
385 384 fveq2i ⊢limPt⁡topGen⁡ran⁡.⁡0+∞=limPt⁡topGen⁡ran⁡.⁡ℝ∩0+∞
386 379 385 eleqtrdi ⊢⊤→0∈limPt⁡topGen⁡ran⁡.⁡ℝ∩0+∞
387 eqid ⊢x∈−π0⟼−1=x∈−π0⟼−1
388 mnfle ⊢−π∈ℝ*→−∞≤−π
389 161 388 ax-mp ⊢−∞≤−π
390 iooss1 ⊢−∞∈ℝ*∧−∞≤−π→−π0⊆−∞0
391 365 389 390 mp2an ⊢−π0⊆−∞0
392 391 a1i ⊢⊤→−π0⊆−∞0
393 ioosscn ⊢−∞0⊆ℂ
394 392 393 sstrdi ⊢⊤→−π0⊆ℂ
395 0cnd ⊢⊤→0∈ℂ
396 387 394 306 395 constlimc ⊢⊤→−1∈x∈−π0⟼−1limℂ0
397 resabs1 ⊢−π0⊆−∞0→F↾−∞0↾−π0=F↾−π0
398 391 397 ax-mp ⊢F↾−∞0↾−π0=F↾−π0
399 301 398 eqtr4i ⊢x∈−π0⟼−1=F↾−∞0↾−π0
400 399 oveq1i ⊢x∈−π0⟼−1limℂ0=F↾−∞0↾−π0limℂ0
401 fssres ⊢F:ℝ⟶ℂ∧−∞0⊆ℝ→F↾−∞0:−∞0⟶ℂ
402 210 370 401 mp2an ⊢F↾−∞0:−∞0⟶ℂ
403 402 a1i ⊢⊤→F↾−∞0:−∞0⟶ℂ
404 393 a1i ⊢⊤→−∞0⊆ℂ
405 eqid ⊢TopOpen⁡ℂfld↾𝑡−∞0∪0=TopOpen⁡ℂfld↾𝑡−∞0∪0
406 0le0 ⊢0≤0
407 elioc2 ⊢−π∈ℝ*∧0∈ℝ→0∈−π0↔0∈ℝ∧−π<0∧0≤0
408 161 71 407 mp2an ⊢0∈−π0↔0∈ℝ∧−π<0∧0≤0
409 71 166 406 408 mpbir3an ⊢0∈−π0
410 200 cnfldtop ⊢TopOpen⁡ℂfld∈Top
411 ovex ⊢−∞0∈V
412 resttop ⊢TopOpen⁡ℂfld∈Top∧−∞0∈V→TopOpen⁡ℂfld↾𝑡−∞0∈Top
413 410 411 412 mp2an ⊢TopOpen⁡ℂfld↾𝑡−∞0∈Top
414 161 a1i ⊢⊤→−π∈ℝ*
415 eqid ⊢topGen⁡ran⁡.↾𝑡−∞0=topGen⁡ran⁡.↾𝑡−∞0
416 389 a1i ⊢⊤→−∞≤−π
417 366 414 364 362 415 416 364 iocopn ⊢⊤→−π0∈topGen⁡ran⁡.↾𝑡−∞0
418 417 mptru ⊢−π0∈topGen⁡ran⁡.↾𝑡−∞0
419 201 oveq1i ⊢topGen⁡ran⁡.↾𝑡−∞0=TopOpen⁡ℂfld↾𝑡ℝ↾𝑡−∞0
420 iocssre ⊢−∞∈ℝ*∧0∈ℝ→−∞0⊆ℝ
421 365 71 420 mp2an ⊢−∞0⊆ℝ
422 197 elexi ⊢ℝ∈V
423 restabs ⊢TopOpen⁡ℂfld∈Top∧−∞0⊆ℝ∧ℝ∈V→TopOpen⁡ℂfld↾𝑡ℝ↾𝑡−∞0=TopOpen⁡ℂfld↾𝑡−∞0
424 410 421 422 423 mp3an ⊢TopOpen⁡ℂfld↾𝑡ℝ↾𝑡−∞0=TopOpen⁡ℂfld↾𝑡−∞0
425 419 424 eqtri ⊢topGen⁡ran⁡.↾𝑡−∞0=TopOpen⁡ℂfld↾𝑡−∞0
426 418 425 eleqtri ⊢−π0∈TopOpen⁡ℂfld↾𝑡−∞0
427 isopn3i ⊢TopOpen⁡ℂfld↾𝑡−∞0∈Top∧−π0∈TopOpen⁡ℂfld↾𝑡−∞0→int⁡TopOpen⁡ℂfld↾𝑡−∞0⁡−π0=−π0
428 413 426 427 mp2an ⊢int⁡TopOpen⁡ℂfld↾𝑡−∞0⁡−π0=−π0
429 mnflt0 ⊢−∞<0
430 ioounsn ⊢−∞∈ℝ*∧0∈ℝ*∧−∞<0→−∞0∪0=−∞0
431 365 153 429 430 mp3an ⊢−∞0∪0=−∞0
432 431 eqcomi ⊢−∞0=−∞0∪0
433 432 oveq2i ⊢TopOpen⁡ℂfld↾𝑡−∞0=TopOpen⁡ℂfld↾𝑡−∞0∪0
434 433 fveq2i ⊢int⁡TopOpen⁡ℂfld↾𝑡−∞0=int⁡TopOpen⁡ℂfld↾𝑡−∞0∪0
435 ioounsn ⊢−π∈ℝ*∧0∈ℝ*∧−π<0→−π0∪0=−π0
436 161 153 166 435 mp3an ⊢−π0∪0=−π0
437 436 eqcomi ⊢−π0=−π0∪0
438 434 437 fveq12i ⊢int⁡TopOpen⁡ℂfld↾𝑡−∞0⁡−π0=int⁡TopOpen⁡ℂfld↾𝑡−∞0∪0⁡−π0∪0
439 428 438 eqtr3i ⊢−π0=int⁡TopOpen⁡ℂfld↾𝑡−∞0∪0⁡−π0∪0
440 409 439 eleqtri ⊢0∈int⁡TopOpen⁡ℂfld↾𝑡−∞0∪0⁡−π0∪0
441 440 a1i ⊢⊤→0∈int⁡TopOpen⁡ℂfld↾𝑡−∞0∪0⁡−π0∪0
442 403 392 404 200 405 441 limcres ⊢⊤→F↾−∞0↾−π0limℂ0=F↾−∞0limℂ0
443 442 mptru ⊢F↾−∞0↾−π0limℂ0=F↾−∞0limℂ0
444 400 443 eqtri ⊢x∈−π0⟼−1limℂ0=F↾−∞0limℂ0
445 396 444 eleqtrdi ⊢⊤→−1∈F↾−∞0limℂ0
446 eqid ⊢x∈0π⟼1=x∈0π⟼1
447 ioosscn ⊢0π⊆ℂ
448 447 a1i ⊢⊤→0π⊆ℂ
449 446 448 204 395 constlimc ⊢⊤→1∈x∈0π⟼1limℂ0
450 ltpnf ⊢π∈ℝ→π<+∞
451 xrltle ⊢π∈ℝ*∧+∞∈ℝ*→π<+∞→π≤+∞
452 155 376 451 mp2an ⊢π<+∞→π≤+∞
453 120 450 452 mp2b ⊢π≤+∞
454 iooss2 ⊢+∞∈ℝ*∧π≤+∞→0π⊆0+∞
455 376 453 454 mp2an ⊢0π⊆0+∞
456 resabs1 ⊢0π⊆0+∞→F↾0+∞↾0π=F↾0π
457 455 456 ax-mp ⊢F↾0+∞↾0π=F↾0π
458 195 457 eqtr4i ⊢x∈0π⟼1=F↾0+∞↾0π
459 458 oveq1i ⊢x∈0π⟼1limℂ0=F↾0+∞↾0πlimℂ0
460 fssres ⊢F:ℝ⟶ℂ∧0+∞⊆ℝ→F↾0+∞:0+∞⟶ℂ
461 210 381 460 mp2an ⊢F↾0+∞:0+∞⟶ℂ
462 461 a1i ⊢⊤→F↾0+∞:0+∞⟶ℂ
463 455 a1i ⊢⊤→0π⊆0+∞
464 ioosscn ⊢0+∞⊆ℂ
465 464 a1i ⊢⊤→0+∞⊆ℂ
466 eqid ⊢TopOpen⁡ℂfld↾𝑡0+∞∪0=TopOpen⁡ℂfld↾𝑡0+∞∪0
467 elico2 ⊢0∈ℝ∧π∈ℝ*→0∈0π↔0∈ℝ∧0≤0∧0<π
468 71 155 467 mp2an ⊢0∈0π↔0∈ℝ∧0≤0∧0<π
469 71 406 72 468 mpbir3an ⊢0∈0π
470 ovex ⊢0+∞∈V
471 resttop ⊢TopOpen⁡ℂfld∈Top∧0+∞∈V→TopOpen⁡ℂfld↾𝑡0+∞∈Top
472 410 470 471 mp2an ⊢TopOpen⁡ℂfld↾𝑡0+∞∈Top
473 155 a1i ⊢⊤→π∈ℝ*
474 eqid ⊢topGen⁡ran⁡.↾𝑡0+∞=topGen⁡ran⁡.↾𝑡0+∞
475 453 a1i ⊢⊤→π≤+∞
476 364 473 377 362 474 475 icoopn ⊢⊤→0π∈topGen⁡ran⁡.↾𝑡0+∞
477 476 mptru ⊢0π∈topGen⁡ran⁡.↾𝑡0+∞
478 201 oveq1i ⊢topGen⁡ran⁡.↾𝑡0+∞=TopOpen⁡ℂfld↾𝑡ℝ↾𝑡0+∞
479 rge0ssre ⊢0+∞⊆ℝ
480 restabs ⊢TopOpen⁡ℂfld∈Top∧0+∞⊆ℝ∧ℝ∈V→TopOpen⁡ℂfld↾𝑡ℝ↾𝑡0+∞=TopOpen⁡ℂfld↾𝑡0+∞
481 410 479 422 480 mp3an ⊢TopOpen⁡ℂfld↾𝑡ℝ↾𝑡0+∞=TopOpen⁡ℂfld↾𝑡0+∞
482 478 481 eqtri ⊢topGen⁡ran⁡.↾𝑡0+∞=TopOpen⁡ℂfld↾𝑡0+∞
483 477 482 eleqtri ⊢0π∈TopOpen⁡ℂfld↾𝑡0+∞
484 isopn3i ⊢TopOpen⁡ℂfld↾𝑡0+∞∈Top∧0π∈TopOpen⁡ℂfld↾𝑡0+∞→int⁡TopOpen⁡ℂfld↾𝑡0+∞⁡0π=0π
485 472 483 484 mp2an ⊢int⁡TopOpen⁡ℂfld↾𝑡0+∞⁡0π=0π
486 0ltpnf ⊢0<+∞
487 snunioo1 ⊢0∈ℝ*∧+∞∈ℝ*∧0<+∞→0+∞∪0=0+∞
488 153 376 486 487 mp3an ⊢0+∞∪0=0+∞
489 488 eqcomi ⊢0+∞=0+∞∪0
490 489 oveq2i ⊢TopOpen⁡ℂfld↾𝑡0+∞=TopOpen⁡ℂfld↾𝑡0+∞∪0
491 490 fveq2i ⊢int⁡TopOpen⁡ℂfld↾𝑡0+∞=int⁡TopOpen⁡ℂfld↾𝑡0+∞∪0
492 snunioo1 ⊢0∈ℝ*∧π∈ℝ*∧0<π→0π∪0=0π
493 153 155 72 492 mp3an ⊢0π∪0=0π
494 493 eqcomi ⊢0π=0π∪0
495 491 494 fveq12i ⊢int⁡TopOpen⁡ℂfld↾𝑡0+∞⁡0π=int⁡TopOpen⁡ℂfld↾𝑡0+∞∪0⁡0π∪0
496 485 495 eqtr3i ⊢0π=int⁡TopOpen⁡ℂfld↾𝑡0+∞∪0⁡0π∪0
497 469 496 eleqtri ⊢0∈int⁡TopOpen⁡ℂfld↾𝑡0+∞∪0⁡0π∪0
498 497 a1i ⊢⊤→0∈int⁡TopOpen⁡ℂfld↾𝑡0+∞∪0⁡0π∪0
499 462 463 465 200 466 498 limcres ⊢⊤→F↾0+∞↾0πlimℂ0=F↾0+∞limℂ0
500 499 mptru ⊢F↾0+∞↾0πlimℂ0=F↾0+∞limℂ0
501 459 500 eqtri ⊢x∈0π⟼1limℂ0=F↾0+∞limℂ0
502 449 501 eleqtrdi ⊢⊤→1∈F↾0+∞limℂ0
503 neg1lt0 ⊢−1<0
504 109 71 108 lttri ⊢−1<0∧0<1→−1<1
505 503 38 504 mp2an ⊢−1<1
506 109 505 ltneii ⊢−1≠1
507 506 a1i ⊢⊤→−1≠1
508 200 361 362 363 364 375 386 445 502 507 jumpncnp ⊢⊤→¬F∈topGen⁡ran⁡.CnPTopOpen⁡ℂfld⁡0
509 508 mptru ⊢¬F∈topGen⁡ran⁡.CnPTopOpen⁡ℂfld⁡0
510 208 a1i ⊢0∈dom⁡Fℝ′↾−ππ→ℝ⊆ℂ
511 210 a1i ⊢0∈dom⁡Fℝ′↾−ππ→F:ℝ⟶ℂ
512 207 a1i ⊢0∈dom⁡Fℝ′↾−ππ→ℝ⊆ℝ
513 inss2 ⊢−ππ∩dom⁡Fℝ′⊆dom⁡Fℝ′
514 222 513 eqsstri ⊢dom⁡Fℝ′↾−ππ⊆dom⁡Fℝ′
515 514 sseli ⊢0∈dom⁡Fℝ′↾−ππ→0∈dom⁡Fℝ′
516 201 200 dvcnp2 ⊢ℝ⊆ℂ∧F:ℝ⟶ℂ∧ℝ⊆ℝ∧0∈dom⁡Fℝ′→F∈topGen⁡ran⁡.CnPTopOpen⁡ℂfld⁡0
517 510 511 512 515 516 syl31anc ⊢0∈dom⁡Fℝ′↾−ππ→F∈topGen⁡ran⁡.CnPTopOpen⁡ℂfld⁡0
518 509 517 mto ⊢¬0∈dom⁡Fℝ′↾−ππ
519 518 a1i ⊢x=0→¬0∈dom⁡Fℝ′↾−ππ
520 360 519 eqneltrd ⊢x=0→¬x∈dom⁡Fℝ′↾−ππ
521 520 necon2ai ⊢x∈dom⁡Fℝ′↾−ππ→x≠0
522 521 adantr ⊢x∈dom⁡Fℝ′↾−ππ∧¬x<0→x≠0
523 356 357 359 522 leneltd ⊢x∈dom⁡Fℝ′↾−ππ∧¬x<0→0<x
524 346 165 sylan ⊢x∈dom⁡Fℝ′↾−ππ∧0<x→x∈0π
525 elun2 ⊢x∈0π→x∈−π0∪0π
526 524 525 syl ⊢x∈dom⁡Fℝ′↾−ππ∧0<x→x∈−π0∪0π
527 355 523 526 syl2anc ⊢x∈dom⁡Fℝ′↾−ππ∧¬x<0→x∈−π0∪0π
528 354 527 pm2.61dan ⊢x∈dom⁡Fℝ′↾−ππ→x∈−π0∪0π
529 ovex ⊢−π0∈V
530 ovex ⊢0π∈V
531 529 530 unipr ⊢⋃−π00π=−π0∪0π
532 528 531 eleqtrrdi ⊢x∈dom⁡Fℝ′↾−ππ→x∈⋃−π00π
533 532 ssriv ⊢dom⁡Fℝ′↾−ππ⊆⋃−π00π
534 533 a1i ⊢⊤→dom⁡Fℝ′↾−ππ⊆⋃−π00π
535 ineq2 ⊢x=−π0→dom⁡Fℝ′↾−ππ∩x=dom⁡Fℝ′↾−ππ∩−π0
536 retop ⊢topGen⁡ran⁡.∈Top
537 ovex ⊢ℝDF∈V
538 537 resex ⊢Fℝ′↾−ππ∈V
539 538 dmex ⊢dom⁡Fℝ′↾−ππ∈V
540 536 539 pm3.2i ⊢topGen⁡ran⁡.∈Top∧dom⁡Fℝ′↾−ππ∈V
541 320 ssriv ⊢−π0⊆dom⁡Fℝ′↾−ππ
542 ssid ⊢−π0⊆−π0
543 303 541 542 3pm3.2i ⊢−π0∈topGen⁡ran⁡.∧−π0⊆dom⁡Fℝ′↾−ππ∧−π0⊆−π0
544 restopnb ⊢topGen⁡ran⁡.∈Top∧dom⁡Fℝ′↾−ππ∈V∧−π0∈topGen⁡ran⁡.∧−π0⊆dom⁡Fℝ′↾−ππ∧−π0⊆−π0→−π0∈topGen⁡ran⁡.↔−π0∈topGen⁡ran⁡.↾𝑡dom⁡Fℝ′↾−ππ
545 540 543 544 mp2an ⊢−π0∈topGen⁡ran⁡.↔−π0∈topGen⁡ran⁡.↾𝑡dom⁡Fℝ′↾−ππ
546 303 545 mpbi ⊢−π0∈topGen⁡ran⁡.↾𝑡dom⁡Fℝ′↾−ππ
547 inss2 ⊢dom⁡Fℝ′↾−ππ∩−π0⊆−π0
548 541 542 ssini ⊢−π0⊆dom⁡Fℝ′↾−ππ∩−π0
549 547 548 eqssi ⊢dom⁡Fℝ′↾−ππ∩−π0=−π0
550 201 oveq1i ⊢topGen⁡ran⁡.↾𝑡dom⁡Fℝ′↾−ππ=TopOpen⁡ℂfld↾𝑡ℝ↾𝑡dom⁡Fℝ′↾−ππ
551 333 345 sstri ⊢dom⁡Fℝ′↾−ππ⊆ℝ
552 restabs ⊢TopOpen⁡ℂfld∈Top∧dom⁡Fℝ′↾−ππ⊆ℝ∧ℝ∈V→TopOpen⁡ℂfld↾𝑡ℝ↾𝑡dom⁡Fℝ′↾−ππ=TopOpen⁡ℂfld↾𝑡dom⁡Fℝ′↾−ππ
553 410 551 422 552 mp3an ⊢TopOpen⁡ℂfld↾𝑡ℝ↾𝑡dom⁡Fℝ′↾−ππ=TopOpen⁡ℂfld↾𝑡dom⁡Fℝ′↾−ππ
554 550 553 eqtr2i ⊢TopOpen⁡ℂfld↾𝑡dom⁡Fℝ′↾−ππ=topGen⁡ran⁡.↾𝑡dom⁡Fℝ′↾−ππ
555 546 549 554 3eltr4i ⊢dom⁡Fℝ′↾−ππ∩−π0∈TopOpen⁡ℂfld↾𝑡dom⁡Fℝ′↾−ππ
556 535 555 eqeltrdi ⊢x=−π0→dom⁡Fℝ′↾−ππ∩x∈TopOpen⁡ℂfld↾𝑡dom⁡Fℝ′↾−ππ
557 556 adantl ⊢x∈−π00π∧x=−π0→dom⁡Fℝ′↾−ππ∩x∈TopOpen⁡ℂfld↾𝑡dom⁡Fℝ′↾−ππ
558 neqne ⊢¬x=−π0→x≠−π0
559 elprn1 ⊢x∈−π00π∧x≠−π0→x=0π
560 558 559 sylan2 ⊢x∈−π00π∧¬x=−π0→x=0π
561 ineq2 ⊢x=0π→dom⁡Fℝ′↾−ππ∩x=dom⁡Fℝ′↾−ππ∩0π
562 223 ssriv ⊢0π⊆dom⁡Fℝ′↾−ππ
563 ssid ⊢0π⊆0π
564 199 562 563 3pm3.2i ⊢0π∈topGen⁡ran⁡.∧0π⊆dom⁡Fℝ′↾−ππ∧0π⊆0π
565 restopnb ⊢topGen⁡ran⁡.∈Top∧dom⁡Fℝ′↾−ππ∈V∧0π∈topGen⁡ran⁡.∧0π⊆dom⁡Fℝ′↾−ππ∧0π⊆0π→0π∈topGen⁡ran⁡.↔0π∈topGen⁡ran⁡.↾𝑡dom⁡Fℝ′↾−ππ
566 540 564 565 mp2an ⊢0π∈topGen⁡ran⁡.↔0π∈topGen⁡ran⁡.↾𝑡dom⁡Fℝ′↾−ππ
567 199 566 mpbi ⊢0π∈topGen⁡ran⁡.↾𝑡dom⁡Fℝ′↾−ππ
568 inss2 ⊢dom⁡Fℝ′↾−ππ∩0π⊆0π
569 562 563 ssini ⊢0π⊆dom⁡Fℝ′↾−ππ∩0π
570 568 569 eqssi ⊢dom⁡Fℝ′↾−ππ∩0π=0π
571 567 570 554 3eltr4i ⊢dom⁡Fℝ′↾−ππ∩0π∈TopOpen⁡ℂfld↾𝑡dom⁡Fℝ′↾−ππ
572 561 571 eqeltrdi ⊢x=0π→dom⁡Fℝ′↾−ππ∩x∈TopOpen⁡ℂfld↾𝑡dom⁡Fℝ′↾−ππ
573 560 572 syl ⊢x∈−π00π∧¬x=−π0→dom⁡Fℝ′↾−ππ∩x∈TopOpen⁡ℂfld↾𝑡dom⁡Fℝ′↾−ππ
574 557 573 pm2.61dan ⊢x∈−π00π→dom⁡Fℝ′↾−ππ∩x∈TopOpen⁡ℂfld↾𝑡dom⁡Fℝ′↾−ππ
575 574 adantl ⊢⊤∧x∈−π00π→dom⁡Fℝ′↾−ππ∩x∈TopOpen⁡ℂfld↾𝑡dom⁡Fℝ′↾−ππ
576 ssid ⊢ℂ⊆ℂ
577 576 a1i ⊢⊤→ℂ⊆ℂ
578 394 395 577 constcncfg ⊢⊤→x∈−π0⟼0:−π0⟶cnℂ
579 578 mptru ⊢x∈−π0⟼0:−π0⟶cnℂ
580 579 a1i ⊢x=−π0→x∈−π0⟼0:−π0⟶cnℂ
581 reseq2 ⊢x=−π0→Fℝ′↾−ππ↾x=Fℝ′↾−ππ↾−π0
582 resabs1 ⊢−π0⊆−ππ→Fℝ′↾−ππ↾−π0=Fℝ′↾−π0
583 240 582 ax-mp ⊢Fℝ′↾−ππ↾−π0=Fℝ′↾−π0
584 583 311 eqtr4i ⊢Fℝ′↾−ππ↾−π0=x∈−π0⟼0
585 581 584 eqtrdi ⊢x=−π0→Fℝ′↾−ππ↾x=x∈−π0⟼0
586 535 549 eqtrdi ⊢x=−π0→dom⁡Fℝ′↾−ππ∩x=−π0
587 586 oveq1d ⊢x=−π0→dom⁡Fℝ′↾−ππ∩x⟶cnℂ=−π0⟶cnℂ
588 580 585 587 3eltr4d ⊢x=−π0→Fℝ′↾−ππ↾x:dom⁡Fℝ′↾−ππ∩x⟶cnℂ
589 588 adantl ⊢x∈−π00π∧x=−π0→Fℝ′↾−ππ↾x:dom⁡Fℝ′↾−ππ∩x⟶cnℂ
590 448 395 577 constcncfg ⊢⊤→x∈0π⟼0:0π⟶cnℂ
591 590 mptru ⊢x∈0π⟼0:0π⟶cnℂ
592 591 a1i ⊢x=0π→x∈0π⟼0:0π⟶cnℂ
593 reseq2 ⊢x=0π→Fℝ′↾−ππ↾x=Fℝ′↾−ππ↾0π
594 resabs1 ⊢0π⊆−ππ→Fℝ′↾−ππ↾0π=Fℝ′↾0π
595 169 594 ax-mp ⊢Fℝ′↾−ππ↾0π=Fℝ′↾0π
596 595 213 eqtr4i ⊢Fℝ′↾−ππ↾0π=x∈0π⟼0
597 593 596 eqtrdi ⊢x=0π→Fℝ′↾−ππ↾x=x∈0π⟼0
598 561 570 eqtrdi ⊢x=0π→dom⁡Fℝ′↾−ππ∩x=0π
599 598 oveq1d ⊢x=0π→dom⁡Fℝ′↾−ππ∩x⟶cnℂ=0π⟶cnℂ
600 592 597 599 3eltr4d ⊢x=0π→Fℝ′↾−ππ↾x:dom⁡Fℝ′↾−ππ∩x⟶cnℂ
601 560 600 syl ⊢x∈−π00π∧¬x=−π0→Fℝ′↾−ππ↾x:dom⁡Fℝ′↾−ππ∩x⟶cnℂ
602 589 601 pm2.61dan ⊢x∈−π00π→Fℝ′↾−ππ↾x:dom⁡Fℝ′↾−ππ∩x⟶cnℂ
603 602 adantl ⊢⊤∧x∈−π00π→Fℝ′↾−ππ↾x:dom⁡Fℝ′↾−ππ∩x⟶cnℂ
604 336 342 534 575 603 cncfuni ⊢⊤→Fℝ′↾−ππ:dom⁡Fℝ′↾−ππ⟶cnℂ
605 604 mptru ⊢Fℝ′↾−ππ:dom⁡Fℝ′↾−ππ⟶cnℂ
606 oveq1 ⊢x=−π→x+∞=−π+∞
607 606 reseq2d ⊢x=−π→Fℝ′↾−ππ↾x+∞=Fℝ′↾−ππ↾−π+∞
608 iooss2 ⊢+∞∈ℝ*∧π≤+∞→−ππ⊆−π+∞
609 376 453 608 mp2an ⊢−ππ⊆−π+∞
610 resabs2 ⊢−ππ⊆−π+∞→Fℝ′↾−ππ↾−π+∞=Fℝ′↾−ππ
611 609 610 ax-mp ⊢Fℝ′↾−ππ↾−π+∞=Fℝ′↾−ππ
612 607 611 eqtrdi ⊢x=−π→Fℝ′↾−ππ↾x+∞=Fℝ′↾−ππ
613 id ⊢x=−π→x=−π
614 612 613 oveq12d ⊢x=−π→Fℝ′↾−ππ↾x+∞limℂx=Fℝ′↾−ππlimℂ−π
615 254 a1i ⊢⊤→−π∈ℂ
616 313 394 395 615 constlimc ⊢⊤→0∈x∈−π0⟼0limℂ−π
617 616 mptru ⊢0∈x∈−π0⟼0limℂ−π
618 311 oveq1i ⊢x∈−π0⟼0limℂ−π=Fℝ′↾−π0limℂ−π
619 337 a1i ⊢⊤→Fℝ′:dom⁡Fℝ′⟶ℂ
620 160 a1i ⊢⊤→−π∈ℝ
621 153 a1i ⊢⊤→0∈ℝ*
622 166 a1i ⊢⊤→−π<0
623 317 a1i ⊢⊤→−π0⊆dom⁡Fℝ′
624 238 a1i ⊢⊤→0≤π
625 619 620 621 622 623 473 624 limcresioolb ⊢⊤→Fℝ′↾−π0limℂ−π=Fℝ′↾−ππlimℂ−π
626 625 mptru ⊢Fℝ′↾−π0limℂ−π=Fℝ′↾−ππlimℂ−π
627 618 626 eqtri ⊢x∈−π0⟼0limℂ−π=Fℝ′↾−ππlimℂ−π
628 617 627 eleqtri ⊢0∈Fℝ′↾−ππlimℂ−π
629 628 ne0ii ⊢Fℝ′↾−ππlimℂ−π≠∅
630 629 a1i ⊢x=−π→Fℝ′↾−ππlimℂ−π≠∅
631 614 630 eqnetrd ⊢x=−π→Fℝ′↾−ππ↾x+∞limℂx≠∅
632 631 adantl ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ∧x=−π→Fℝ′↾−ππ↾x+∞limℂx≠∅
633 eldifi ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ→x∈−ππ
634 161 a1i ⊢x∈−ππ∧¬x=−π→−π∈ℝ*
635 155 a1i ⊢x∈−ππ∧¬x=−π→π∈ℝ*
636 icossre ⊢−π∈ℝ∧π∈ℝ*→−ππ⊆ℝ
637 160 155 636 mp2an ⊢−ππ⊆ℝ
638 637 sseli ⊢x∈−ππ→x∈ℝ
639 638 adantr ⊢x∈−ππ∧¬x=−π→x∈ℝ
640 160 a1i ⊢x∈−ππ∧¬x=−π→−π∈ℝ
641 icogelb ⊢−π∈ℝ*∧π∈ℝ*∧x∈−ππ→−π≤x
642 161 155 641 mp3an12 ⊢x∈−ππ→−π≤x
643 642 adantr ⊢x∈−ππ∧¬x=−π→−π≤x
644 neqne ⊢¬x=−π→x≠−π
645 644 adantl ⊢x∈−ππ∧¬x=−π→x≠−π
646 640 639 643 645 leneltd ⊢x∈−ππ∧¬x=−π→−π<x
647 icoltub ⊢−π∈ℝ*∧π∈ℝ*∧x∈−ππ→x<π
648 161 155 647 mp3an12 ⊢x∈−ππ→x<π
649 648 adantr ⊢x∈−ππ∧¬x=−π→x<π
650 634 635 639 646 649 eliood ⊢x∈−ππ∧¬x=−π→x∈−ππ
651 633 650 sylan ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ∧¬x=−π→x∈−ππ
652 eldifn ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ→¬x∈dom⁡Fℝ′↾−ππ
653 652 adantr ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ∧¬x=−π→¬x∈dom⁡Fℝ′↾−ππ
654 651 653 eldifd ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ∧¬x=−π→x∈−ππ∖dom⁡Fℝ′↾−ππ
655 oveq1 ⊢x=0→x+∞=0+∞
656 655 reseq2d ⊢x=0→Fℝ′↾−ππ↾x+∞=Fℝ′↾−ππ↾0+∞
657 656 360 oveq12d ⊢x=0→Fℝ′↾−ππ↾x+∞limℂx=Fℝ′↾−ππ↾0+∞limℂ0
658 215 448 395 395 constlimc ⊢⊤→0∈x∈0π⟼0limℂ0
659 658 mptru ⊢0∈x∈0π⟼0limℂ0
660 resres ⊢Fℝ′↾−ππ↾0+∞=Fℝ′↾−ππ∩0+∞
661 iooin ⊢−π∈ℝ*∧π∈ℝ*∧0∈ℝ*∧+∞∈ℝ*→−ππ∩0+∞=if−π≤00−πifπ≤+∞π+∞
662 161 155 153 376 661 mp4an ⊢−ππ∩0+∞=if−π≤00−πifπ≤+∞π+∞
663 167 iftruei ⊢if−π≤00−π=0
664 453 iftruei ⊢ifπ≤+∞π+∞=π
665 663 664 oveq12i ⊢if−π≤00−πifπ≤+∞π+∞=0π
666 662 665 eqtri ⊢−ππ∩0+∞=0π
667 666 reseq2i ⊢Fℝ′↾−ππ∩0+∞=Fℝ′↾0π
668 213 eqcomi ⊢Fℝ′↾0π=x∈0π⟼0
669 660 667 668 3eqtrri ⊢x∈0π⟼0=Fℝ′↾−ππ↾0+∞
670 669 oveq1i ⊢x∈0π⟼0limℂ0=Fℝ′↾−ππ↾0+∞limℂ0
671 659 670 eleqtri ⊢0∈Fℝ′↾−ππ↾0+∞limℂ0
672 671 ne0ii ⊢Fℝ′↾−ππ↾0+∞limℂ0≠∅
673 672 a1i ⊢x=0→Fℝ′↾−ππ↾0+∞limℂ0≠∅
674 657 673 eqnetrd ⊢x=0→Fℝ′↾−ππ↾x+∞limℂx≠∅
675 654 326 674 3syl ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ∧¬x=−π→Fℝ′↾−ππ↾x+∞limℂx≠∅
676 632 675 pm2.61dan ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ→Fℝ′↾−ππ↾x+∞limℂx≠∅
677 oveq2 ⊢x=π→−∞x=−∞π
678 677 reseq2d ⊢x=π→Fℝ′↾−ππ↾−∞x=Fℝ′↾−ππ↾−∞π
679 id ⊢x=π→x=π
680 678 679 oveq12d ⊢x=π→Fℝ′↾−ππ↾−∞xlimℂx=Fℝ′↾−ππ↾−∞πlimℂπ
681 iooss1 ⊢−∞∈ℝ*∧−∞≤−π→−ππ⊆−∞π
682 365 389 681 mp2an ⊢−ππ⊆−∞π
683 resabs2 ⊢−ππ⊆−∞π→Fℝ′↾−ππ↾−∞π=Fℝ′↾−ππ
684 682 683 ax-mp ⊢Fℝ′↾−ππ↾−∞π=Fℝ′↾−ππ
685 684 oveq1i ⊢Fℝ′↾−ππ↾−∞πlimℂπ=Fℝ′↾−ππlimℂπ
686 680 685 eqtrdi ⊢x=π→Fℝ′↾−ππ↾−∞xlimℂx=Fℝ′↾−ππlimℂπ
687 215 448 395 57 constlimc ⊢⊤→0∈x∈0π⟼0limℂπ
688 687 mptru ⊢0∈x∈0π⟼0limℂπ
689 213 oveq1i ⊢x∈0π⟼0limℂπ=Fℝ′↾0πlimℂπ
690 120 a1i ⊢⊤→π∈ℝ
691 72 a1i ⊢⊤→0<π
692 219 a1i ⊢⊤→0π⊆dom⁡Fℝ′
693 167 a1i ⊢⊤→−π≤0
694 619 621 690 691 692 414 693 limcresiooub ⊢⊤→Fℝ′↾0πlimℂπ=Fℝ′↾−ππlimℂπ
695 694 mptru ⊢Fℝ′↾0πlimℂπ=Fℝ′↾−ππlimℂπ
696 689 695 eqtri ⊢x∈0π⟼0limℂπ=Fℝ′↾−ππlimℂπ
697 688 696 eleqtri ⊢0∈Fℝ′↾−ππlimℂπ
698 697 ne0ii ⊢Fℝ′↾−ππlimℂπ≠∅
699 698 a1i ⊢x=π→Fℝ′↾−ππlimℂπ≠∅
700 686 699 eqnetrd ⊢x=π→Fℝ′↾−ππ↾−∞xlimℂx≠∅
701 700 adantl ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ∧x=π→Fℝ′↾−ππ↾−∞xlimℂx≠∅
702 161 a1i ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ∧¬x=π→−π∈ℝ*
703 155 a1i ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ∧¬x=π→π∈ℝ*
704 negpitopissre ⊢−ππ⊆ℝ
705 eldifi ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ→x∈−ππ
706 704 705 sselid ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ→x∈ℝ
707 706 adantr ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ∧¬x=π→x∈ℝ
708 161 a1i ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ→−π∈ℝ*
709 155 a1i ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ→π∈ℝ*
710 iocgtlb ⊢−π∈ℝ*∧π∈ℝ*∧x∈−ππ→−π<x
711 708 709 705 710 syl3anc ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ→−π<x
712 711 adantr ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ∧¬x=π→−π<x
713 120 a1i ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ∧¬x=π→π∈ℝ
714 iocleub ⊢−π∈ℝ*∧π∈ℝ*∧x∈−ππ→x≤π
715 708 709 705 714 syl3anc ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ→x≤π
716 715 adantr ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ∧¬x=π→x≤π
717 id ⊢π=x→π=x
718 717 eqcomd ⊢π=x→x=π
719 718 necon3bi ⊢¬x=π→π≠x
720 719 adantl ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ∧¬x=π→π≠x
721 707 713 716 720 leneltd ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ∧¬x=π→x<π
722 702 703 707 712 721 eliood ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ∧¬x=π→x∈−ππ
723 eldifn ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ→¬x∈dom⁡Fℝ′↾−ππ
724 723 adantr ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ∧¬x=π→¬x∈dom⁡Fℝ′↾−ππ
725 722 724 eldifd ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ∧¬x=π→x∈−ππ∖dom⁡Fℝ′↾−ππ
726 oveq2 ⊢x=0→−∞x=−∞0
727 726 reseq2d ⊢x=0→Fℝ′↾−ππ↾−∞x=Fℝ′↾−ππ↾−∞0
728 727 360 oveq12d ⊢x=0→Fℝ′↾−ππ↾−∞xlimℂx=Fℝ′↾−ππ↾−∞0limℂ0
729 313 394 395 395 constlimc ⊢⊤→0∈x∈−π0⟼0limℂ0
730 729 mptru ⊢0∈x∈−π0⟼0limℂ0
731 resres ⊢Fℝ′↾−ππ↾−∞0=Fℝ′↾−ππ∩−∞0
732 iooin ⊢−π∈ℝ*∧π∈ℝ*∧−∞∈ℝ*∧0∈ℝ*→−ππ∩−∞0=if−π≤−∞−∞−πifπ≤0π0
733 161 155 365 153 732 mp4an ⊢−ππ∩−∞0=if−π≤−∞−∞−πifπ≤0π0
734 mnflt ⊢−π∈ℝ→−∞<−π
735 160 734 ax-mp ⊢−∞<−π
736 xrltnle ⊢−∞∈ℝ*∧−π∈ℝ*→−∞<−π↔¬−π≤−∞
737 365 161 736 mp2an ⊢−∞<−π↔¬−π≤−∞
738 735 737 mpbi ⊢¬−π≤−∞
739 738 iffalsei ⊢if−π≤−∞−∞−π=−π
740 xrltnle ⊢0∈ℝ*∧π∈ℝ*→0<π↔¬π≤0
741 153 155 740 mp2an ⊢0<π↔¬π≤0
742 72 741 mpbi ⊢¬π≤0
743 742 iffalsei ⊢ifπ≤0π0=0
744 739 743 oveq12i ⊢if−π≤−∞−∞−πifπ≤0π0=−π0
745 733 744 eqtri ⊢−ππ∩−∞0=−π0
746 745 reseq2i ⊢Fℝ′↾−ππ∩−∞0=Fℝ′↾−π0
747 311 eqcomi ⊢Fℝ′↾−π0=x∈−π0⟼0
748 731 746 747 3eqtrri ⊢x∈−π0⟼0=Fℝ′↾−ππ↾−∞0
749 748 oveq1i ⊢x∈−π0⟼0limℂ0=Fℝ′↾−ππ↾−∞0limℂ0
750 730 749 eleqtri ⊢0∈Fℝ′↾−ππ↾−∞0limℂ0
751 750 ne0ii ⊢Fℝ′↾−ππ↾−∞0limℂ0≠∅
752 751 a1i ⊢x=0→Fℝ′↾−ππ↾−∞0limℂ0≠∅
753 728 752 eqnetrd ⊢x=0→Fℝ′↾−ππ↾−∞xlimℂx≠∅
754 725 326 753 3syl ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ∧¬x=π→Fℝ′↾−ππ↾−∞xlimℂx≠∅
755 701 754 pm2.61dan ⊢x∈−ππ∖dom⁡Fℝ′↾−ππ→Fℝ′↾−ππ↾−∞xlimℂx≠∅
756 eqid ⊢x∈X−XmodTX⟼1=x∈X−XmodTX⟼1
757 ioosscn ⊢X−XmodTX⊆ℂ
758 757 a1i ⊢XmodT∈0π→X−XmodTX⊆ℂ
759 1cnd ⊢XmodT∈0π→1∈ℂ
760 27 a1i ⊢XmodT∈0π→X∈ℂ
761 756 758 759 760 constlimc ⊢XmodT∈0π→1∈x∈X−XmodTX⟼1limℂX
762 ioossioc ⊢0π⊆0π
763 762 sseli ⊢XmodT∈0π→XmodT∈0π
764 763 iftrued ⊢XmodT∈0π→ifXmodT∈0π1−1=1
765 210 a1i ⊢XmodT∈0π→F:ℝ⟶ℂ
766 modcl ⊢X∈ℝ∧T∈ℝ+→XmodT∈ℝ
767 3 135 766 mp2an ⊢XmodT∈ℝ
768 3 767 resubcli ⊢X−XmodT∈ℝ
769 768 rexri ⊢X−XmodT∈ℝ*
770 769 a1i ⊢XmodT∈0π→X−XmodT∈ℝ*
771 3 a1i ⊢XmodT∈0π→X∈ℝ
772 elioore ⊢XmodT∈0π→XmodT∈ℝ
773 ioogtlb ⊢0∈ℝ*∧π∈ℝ*∧XmodT∈0π→0<XmodT
774 153 155 773 mp3an12 ⊢XmodT∈0π→0<XmodT
775 772 774 elrpd ⊢XmodT∈0π→XmodT∈ℝ+
776 771 775 ltsubrpd ⊢XmodT∈0π→X−XmodT<X
777 ioossre ⊢X−XmodTX⊆ℝ
778 777 a1i ⊢XmodT∈0π→X−XmodTX⊆ℝ
779 365 a1i ⊢XmodT∈0π→−∞∈ℝ*
780 mnflt ⊢X−XmodT∈ℝ→−∞<X−XmodT
781 xrltle ⊢−∞∈ℝ*∧X−XmodT∈ℝ*→−∞<X−XmodT→−∞≤X−XmodT
782 365 769 781 mp2an ⊢−∞<X−XmodT→−∞≤X−XmodT
783 768 780 782 mp2b ⊢−∞≤X−XmodT
784 783 a1i ⊢XmodT∈0π→−∞≤X−XmodT
785 765 770 771 776 778 779 784 limcresiooub ⊢XmodT∈0π→F↾X−XmodTXlimℂX=F↾−∞XlimℂX
786 iooltub ⊢0∈ℝ*∧π∈ℝ*∧XmodT∈0π→XmodT<π
787 153 155 786 mp3an12 ⊢XmodT∈0π→XmodT<π
788 210 a1i ⊢XmodT<π→F:ℝ⟶ℂ
789 777 a1i ⊢XmodT<π→X−XmodTX⊆ℝ
790 788 789 feqresmpt ⊢XmodT<π→F↾X−XmodTX=x∈X−XmodTX⟼F⁡x
791 elioore ⊢x∈X−XmodTX→x∈ℝ
792 791 110 147 sylancl ⊢x∈X−XmodTX→F⁡x=ifxmodT<π1−1
793 792 adantl ⊢XmodT<π∧x∈X−XmodTX→F⁡x=ifxmodT<π1−1
794 791 adantl ⊢XmodT<π∧x∈X−XmodTX→x∈ℝ
795 135 a1i ⊢XmodT<π∧x∈X−XmodTX→T∈ℝ+
796 794 795 modcld ⊢XmodT<π∧x∈X−XmodTX→xmodT∈ℝ
797 767 a1i ⊢XmodT<π∧x∈X−XmodTX→XmodT∈ℝ
798 120 a1i ⊢XmodT<π∧x∈X−XmodTX→π∈ℝ
799 3 a1i ⊢x∈X−XmodTX→X∈ℝ
800 135 a1i ⊢x∈X−XmodTX→T∈ℝ+
801 ioossico ⊢X−XmodTX⊆X−XmodTX
802 801 sseli ⊢x∈X−XmodTX→x∈X−XmodTX
803 799 800 802 ltmod ⊢x∈X−XmodTX→xmodT<XmodT
804 803 adantl ⊢XmodT<π∧x∈X−XmodTX→xmodT<XmodT
805 simpl ⊢XmodT<π∧x∈X−XmodTX→XmodT<π
806 796 797 798 804 805 lttrd ⊢XmodT<π∧x∈X−XmodTX→xmodT<π
807 806 iftrued ⊢XmodT<π∧x∈X−XmodTX→ifxmodT<π1−1=1
808 793 807 eqtrd ⊢XmodT<π∧x∈X−XmodTX→F⁡x=1
809 808 mpteq2dva ⊢XmodT<π→x∈X−XmodTX⟼F⁡x=x∈X−XmodTX⟼1
810 790 809 eqtrd ⊢XmodT<π→F↾X−XmodTX=x∈X−XmodTX⟼1
811 787 810 syl ⊢XmodT∈0π→F↾X−XmodTX=x∈X−XmodTX⟼1
812 811 oveq1d ⊢XmodT∈0π→F↾X−XmodTXlimℂX=x∈X−XmodTX⟼1limℂX
813 785 812 eqtr3d ⊢XmodT∈0π→F↾−∞XlimℂX=x∈X−XmodTX⟼1limℂX
814 761 764 813 3eltr4d ⊢XmodT∈0π→ifXmodT∈0π1−1∈F↾−∞XlimℂX
815 eqid ⊢x∈X−πX⟼−1=x∈X−πX⟼−1
816 ioossre ⊢X−πX⊆ℝ
817 816 a1i ⊢⊤→X−πX⊆ℝ
818 817 208 sstrdi ⊢⊤→X−πX⊆ℂ
819 27 a1i ⊢⊤→X∈ℂ
820 815 818 306 819 constlimc ⊢⊤→−1∈x∈X−πX⟼−1limℂX
821 820 mptru ⊢−1∈x∈X−πX⟼−1limℂX
822 821 a1i ⊢XmodT=0→−1∈x∈X−πX⟼−1limℂX
823 id ⊢XmodT=0→XmodT=0
824 lbioc ⊢¬0∈0π
825 824 a1i ⊢XmodT=0→¬0∈0π
826 823 825 eqneltrd ⊢XmodT=0→¬XmodT∈0π
827 826 iffalsed ⊢XmodT=0→ifXmodT∈0π1−1=−1
828 210 a1i ⊢XmodT=0→F:ℝ⟶ℂ
829 816 a1i ⊢XmodT=0→X−πX⊆ℝ
830 828 829 feqresmpt ⊢XmodT=0→F↾X−πX=x∈X−πX⟼F⁡x
831 829 sselda ⊢XmodT=0∧x∈X−πX→x∈ℝ
832 831 110 147 sylancl ⊢XmodT=0∧x∈X−πX→F⁡x=ifxmodT<π1−1
833 120 a1i ⊢XmodT=0∧x∈X−πX→π∈ℝ
834 135 a1i ⊢XmodT=0∧x∈X−πX→T∈ℝ+
835 831 834 modcld ⊢XmodT=0∧x∈X−πX→xmodT∈ℝ
836 3 120 resubcli ⊢X−π∈ℝ
837 836 a1i ⊢x∈X−πX→X−π∈ℝ
838 122 a1i ⊢x∈X−πX→T∈ℝ
839 837 838 readdcld ⊢x∈X−πX→X-π+T∈ℝ
840 elioore ⊢x∈X−πX→x∈ℝ
841 840 838 readdcld ⊢x∈X−πX→x+T∈ℝ
842 3 a1i ⊢x∈X−πX→X∈ℝ
843 836 rexri ⊢X−π∈ℝ*
844 843 a1i ⊢x∈X−πX→X−π∈ℝ*
845 842 rexrd ⊢x∈X−πX→X∈ℝ*
846 id ⊢x∈X−πX→x∈X−πX
847 ioogtlb ⊢X−π∈ℝ*∧X∈ℝ*∧x∈X−πX→X−π<x
848 844 845 846 847 syl3anc ⊢x∈X−πX→X−π<x
849 837 840 838 848 ltadd1dd ⊢x∈X−πX→X-π+T<x+T
850 839 841 842 849 ltsub1dd ⊢x∈X−πX→X−π+T-X<x+T-X
851 850 adantl ⊢XmodT=0∧x∈X−πX→X−π+T-X<x+T-X
852 252 oveq2i ⊢X-π+T=X−π+π+π
853 56 56 addcli ⊢π+π∈ℂ
854 subadd23 ⊢X∈ℂ∧π∈ℂ∧π+π∈ℂ→X−π+π+π=X+π+π-π
855 27 56 853 854 mp3an ⊢X−π+π+π=X+π+π-π
856 56 56 pncan3oi ⊢π+π-π=π
857 856 oveq2i ⊢X+π+π-π=X+π
858 852 855 857 3eqtri ⊢X-π+T=X+π
859 858 oveq1i ⊢X−π+T-X=X+π-X
860 pncan2 ⊢X∈ℂ∧π∈ℂ→X+π-X=π
861 27 56 860 mp2an ⊢X+π-X=π
862 859 861 eqtr2i ⊢π=X−π+T-X
863 862 a1i ⊢XmodT=0∧x∈X−πX→π=X−π+T-X
864 841 842 resubcld ⊢x∈X−πX→x+T-X∈ℝ
865 modabs2 ⊢x+T-X∈ℝ∧T∈ℝ+→x+T-XmodTmodT=x+T-XmodT
866 864 135 865 sylancl ⊢x∈X−πX→x+T-XmodTmodT=x+T-XmodT
867 135 a1i ⊢x∈X−πX→T∈ℝ+
868 0red ⊢x∈X−πX→0∈ℝ
869 839 842 resubcld ⊢x∈X−πX→X−π+T-X∈ℝ
870 72 862 breqtri ⊢0<X−π+T-X
871 870 a1i ⊢x∈X−πX→0<X−π+T-X
872 868 869 864 871 850 lttrd ⊢x∈X−πX→0<x+T-X
873 868 864 872 ltled ⊢x∈X−πX→0≤x+T-X
874 842 838 readdcld ⊢x∈X−πX→X+T∈ℝ
875 iooltub ⊢X−π∈ℝ*∧X∈ℝ*∧x∈X−πX→x<X
876 844 845 846 875 syl3anc ⊢x∈X−πX→x<X
877 840 842 838 876 ltadd1dd ⊢x∈X−πX→x+T<X+T
878 841 874 842 877 ltsub1dd ⊢x∈X−πX→x+T-X<X+T-X
879 pncan2 ⊢X∈ℂ∧T∈ℂ→X+T-X=T
880 27 123 879 mp2an ⊢X+T-X=T
881 878 880 breqtrdi ⊢x∈X−πX→x+T-X<T
882 modid ⊢x+T-X∈ℝ∧T∈ℝ+∧0≤x+T-X∧x+T-X<T→x+T-XmodT=x+T-X
883 864 867 873 881 882 syl22anc ⊢x∈X−πX→x+T-XmodT=x+T-X
884 866 883 eqtr2d ⊢x∈X−πX→x+T-X=x+T-XmodTmodT
885 884 adantl ⊢XmodT=0∧x∈X−πX→x+T-X=x+T-XmodTmodT
886 oveq2 ⊢XmodT=0→x+T-XmodT+XmodT=x+T-XmodT+0
887 886 adantr ⊢XmodT=0∧x∈X−πX→x+T-XmodT+XmodT=x+T-XmodT+0
888 864 867 modcld ⊢x∈X−πX→x+T-XmodT∈ℝ
889 888 recnd ⊢x∈X−πX→x+T-XmodT∈ℂ
890 889 addridd ⊢x∈X−πX→x+T-XmodT+0=x+T-XmodT
891 890 adantl ⊢XmodT=0∧x∈X−πX→x+T-XmodT+0=x+T-XmodT
892 887 891 eqtr2d ⊢XmodT=0∧x∈X−πX→x+T-XmodT=x+T-XmodT+XmodT
893 892 oveq1d ⊢XmodT=0∧x∈X−πX→x+T-XmodTmodT=x+T-XmodT+XmodTmodT
894 modaddabs ⊢x+T-X∈ℝ∧X∈ℝ∧T∈ℝ+→x+T-XmodT+XmodTmodT=x+T-X+XmodT
895 864 842 867 894 syl3anc ⊢x∈X−πX→x+T-XmodT+XmodTmodT=x+T-X+XmodT
896 895 adantl ⊢XmodT=0∧x∈X−πX→x+T-XmodT+XmodTmodT=x+T-X+XmodT
897 885 893 896 3eqtrd ⊢XmodT=0∧x∈X−πX→x+T-X=x+T-X+XmodT
898 145 recnd ⊢x∈ℝ→x+T∈ℂ
899 27 a1i ⊢x∈ℝ→X∈ℂ
900 898 899 npcand ⊢x∈ℝ→x+T-X+X=x+T
901 124 a1i ⊢x∈ℝ→1⁢T=T
902 901 oveq2d ⊢x∈ℝ→x+1⁢T=x+T
903 900 902 eqtr4d ⊢x∈ℝ→x+T-X+X=x+1⁢T
904 903 oveq1d ⊢x∈ℝ→x+T-X+XmodT=x+1⁢TmodT
905 840 904 syl ⊢x∈X−πX→x+T-X+XmodT=x+1⁢TmodT
906 905 adantl ⊢XmodT=0∧x∈X−πX→x+T-X+XmodT=x+1⁢TmodT
907 1zzd ⊢XmodT=0∧x∈X−πX→1∈ℤ
908 831 834 907 138 syl3anc ⊢XmodT=0∧x∈X−πX→x+1⁢TmodT=xmodT
909 897 906 908 3eqtrrd ⊢XmodT=0∧x∈X−πX→xmodT=x+T-X
910 851 863 909 3brtr4d ⊢XmodT=0∧x∈X−πX→π<xmodT
911 833 835 910 ltled ⊢XmodT=0∧x∈X−πX→π≤xmodT
912 833 835 911 lensymd ⊢XmodT=0∧x∈X−πX→¬xmodT<π
913 912 iffalsed ⊢XmodT=0∧x∈X−πX→ifxmodT<π1−1=−1
914 832 913 eqtrd ⊢XmodT=0∧x∈X−πX→F⁡x=−1
915 914 mpteq2dva ⊢XmodT=0→x∈X−πX⟼F⁡x=x∈X−πX⟼−1
916 830 915 eqtr2d ⊢XmodT=0→x∈X−πX⟼−1=F↾X−πX
917 916 oveq1d ⊢XmodT=0→x∈X−πX⟼−1limℂX=F↾X−πXlimℂX
918 843 a1i ⊢⊤→X−π∈ℝ*
919 3 a1i ⊢⊤→X∈ℝ
920 ltsubrp ⊢X∈ℝ∧π∈ℝ+→X−π<X
921 3 184 920 mp2an ⊢X−π<X
922 921 a1i ⊢⊤→X−π<X
923 mnflt ⊢X−π∈ℝ→−∞<X−π
924 xrltle ⊢−∞∈ℝ*∧X−π∈ℝ*→−∞<X−π→−∞≤X−π
925 365 843 924 mp2an ⊢−∞<X−π→−∞≤X−π
926 836 923 925 mp2b ⊢−∞≤X−π
927 926 a1i ⊢⊤→−∞≤X−π
928 363 918 919 922 817 366 927 limcresiooub ⊢⊤→F↾X−πXlimℂX=F↾−∞XlimℂX
929 928 mptru ⊢F↾X−πXlimℂX=F↾−∞XlimℂX
930 917 929 eqtr2di ⊢XmodT=0→F↾−∞XlimℂX=x∈X−πX⟼−1limℂX
931 822 827 930 3eltr4d ⊢XmodT=0→ifXmodT∈0π1−1∈F↾−∞XlimℂX
932 931 adantl ⊢¬XmodT∈0π∧XmodT=0→ifXmodT∈0π1−1∈F↾−∞XlimℂX
933 155 a1i ⊢¬XmodT∈0π∧¬XmodT=0→π∈ℝ*
934 122 rexri ⊢T∈ℝ*
935 934 a1i ⊢¬XmodT∈0π∧¬XmodT=0→T∈ℝ*
936 767 rexri ⊢XmodT∈ℝ*
937 936 a1i ⊢¬XmodT∈0π∧¬XmodT=0→XmodT∈ℝ*
938 120 a1i ⊢¬XmodT∈0π∧¬XmodT=0→π∈ℝ
939 767 a1i ⊢¬XmodT∈0π∧¬XmodT=0→XmodT∈ℝ
940 pm4.56 ⊢¬XmodT∈0π∧¬XmodT=0↔¬XmodT∈0π∨XmodT=0
941 940 biimpi ⊢¬XmodT∈0π∧¬XmodT=0→¬XmodT∈0π∨XmodT=0
942 olc ⊢XmodT=0→XmodT∈0π∨XmodT=0
943 942 adantl ⊢XmodT<π∧XmodT=0→XmodT∈0π∨XmodT=0
944 153 a1i ⊢XmodT<π∧XmodT≠0→0∈ℝ*
945 155 a1i ⊢XmodT<π∧XmodT≠0→π∈ℝ*
946 767 a1i ⊢XmodT<π∧XmodT≠0→XmodT∈ℝ
947 0red ⊢XmodT≠0→0∈ℝ
948 767 a1i ⊢XmodT≠0→XmodT∈ℝ
949 modge0 ⊢X∈ℝ∧T∈ℝ+→0≤XmodT
950 3 135 949 mp2an ⊢0≤XmodT
951 950 a1i ⊢XmodT≠0→0≤XmodT
952 id ⊢XmodT≠0→XmodT≠0
953 947 948 951 952 leneltd ⊢XmodT≠0→0<XmodT
954 953 adantl ⊢XmodT<π∧XmodT≠0→0<XmodT
955 simpl ⊢XmodT<π∧XmodT≠0→XmodT<π
956 944 945 946 954 955 eliood ⊢XmodT<π∧XmodT≠0→XmodT∈0π
957 956 orcd ⊢XmodT<π∧XmodT≠0→XmodT∈0π∨XmodT=0
958 943 957 pm2.61dane ⊢XmodT<π→XmodT∈0π∨XmodT=0
959 941 958 nsyl ⊢¬XmodT∈0π∧¬XmodT=0→¬XmodT<π
960 938 939 959 nltled ⊢¬XmodT∈0π∧¬XmodT=0→π≤XmodT
961 modlt ⊢X∈ℝ∧T∈ℝ+→XmodT<T
962 3 135 961 mp2an ⊢XmodT<T
963 962 a1i ⊢¬XmodT∈0π∧¬XmodT=0→XmodT<T
964 933 935 937 960 963 elicod ⊢¬XmodT∈0π∧¬XmodT=0→XmodT∈πT
965 eqid ⊢x∈X−πX⟼1=x∈X−πX⟼1
966 965 818 204 819 constlimc ⊢⊤→1∈x∈X−πX⟼1limℂX
967 966 mptru ⊢1∈x∈X−πX⟼1limℂX
968 967 a1i ⊢XmodT=π→1∈x∈X−πX⟼1limℂX
969 id ⊢XmodT=π→XmodT=π
970 ubioc1 ⊢0∈ℝ*∧π∈ℝ*∧0<π→π∈0π
971 153 155 72 970 mp3an ⊢π∈0π
972 969 971 eqeltrdi ⊢XmodT=π→XmodT∈0π
973 972 iftrued ⊢XmodT=π→ifXmodT∈0π1−1=1
974 363 817 feqresmpt ⊢⊤→F↾X−πX=x∈X−πX⟼F⁡x
975 974 mptru ⊢F↾X−πX=x∈X−πX⟼F⁡x
976 840 110 147 sylancl ⊢x∈X−πX→F⁡x=ifxmodT<π1−1
977 976 adantl ⊢XmodT=π∧x∈X−πX→F⁡x=ifxmodT<π1−1
978 simpr ⊢XmodT=π∧x∈X−πX→x∈X−πX
979 969 eqcomd ⊢XmodT=π→π=XmodT
980 979 oveq2d ⊢XmodT=π→X−π=X−XmodT
981 980 oveq1d ⊢XmodT=π→X−πX=X−XmodTX
982 981 adantr ⊢XmodT=π∧x∈X−πX→X−πX=X−XmodTX
983 978 982 eleqtrd ⊢XmodT=π∧x∈X−πX→x∈X−XmodTX
984 983 803 syl ⊢XmodT=π∧x∈X−πX→xmodT<XmodT
985 simpl ⊢XmodT=π∧x∈X−πX→XmodT=π
986 984 985 breqtrd ⊢XmodT=π∧x∈X−πX→xmodT<π
987 986 iftrued ⊢XmodT=π∧x∈X−πX→ifxmodT<π1−1=1
988 977 987 eqtrd ⊢XmodT=π∧x∈X−πX→F⁡x=1
989 988 mpteq2dva ⊢XmodT=π→x∈X−πX⟼F⁡x=x∈X−πX⟼1
990 975 989 eqtr2id ⊢XmodT=π→x∈X−πX⟼1=F↾X−πX
991 990 oveq1d ⊢XmodT=π→x∈X−πX⟼1limℂX=F↾X−πXlimℂX
992 991 929 eqtr2di ⊢XmodT=π→F↾−∞XlimℂX=x∈X−πX⟼1limℂX
993 968 973 992 3eltr4d ⊢XmodT=π→ifXmodT∈0π1−1∈F↾−∞XlimℂX
994 993 adantl ⊢XmodT∈πT∧XmodT=π→ifXmodT∈0π1−1∈F↾−∞XlimℂX
995 155 a1i ⊢XmodT∈πT∧¬XmodT=π→π∈ℝ*
996 934 a1i ⊢XmodT∈πT∧¬XmodT=π→T∈ℝ*
997 767 a1i ⊢XmodT∈πT∧¬XmodT=π→XmodT∈ℝ
998 120 a1i ⊢XmodT∈πT∧¬XmodT=π→π∈ℝ
999 icogelb ⊢π∈ℝ*∧T∈ℝ*∧XmodT∈πT→π≤XmodT
1000 155 934 999 mp3an12 ⊢XmodT∈πT→π≤XmodT
1001 1000 adantr ⊢XmodT∈πT∧¬XmodT=π→π≤XmodT
1002 neqne ⊢¬XmodT=π→XmodT≠π
1003 1002 adantl ⊢XmodT∈πT∧¬XmodT=π→XmodT≠π
1004 998 997 1001 1003 leneltd ⊢XmodT∈πT∧¬XmodT=π→π<XmodT
1005 962 a1i ⊢XmodT∈πT∧¬XmodT=π→XmodT<T
1006 995 996 997 1004 1005 eliood ⊢XmodT∈πT∧¬XmodT=π→XmodT∈πT
1007 eqid ⊢x∈X+π-XmodTX⟼−1=x∈X+π-XmodTX⟼−1
1008 ioossre ⊢X+π-XmodTX⊆ℝ
1009 1008 a1i ⊢XmodT∈πT→X+π-XmodTX⊆ℝ
1010 1009 208 sstrdi ⊢XmodT∈πT→X+π-XmodTX⊆ℂ
1011 neg1cn ⊢−1∈ℂ
1012 1011 a1i ⊢XmodT∈πT→−1∈ℂ
1013 27 a1i ⊢XmodT∈πT→X∈ℂ
1014 1007 1010 1012 1013 constlimc ⊢XmodT∈πT→−1∈x∈X+π-XmodTX⟼−1limℂX
1015 153 a1i ⊢XmodT∈πT→0∈ℝ*
1016 120 a1i ⊢XmodT∈πT→π∈ℝ
1017 936 a1i ⊢XmodT∈πT→XmodT∈ℝ*
1018 ioogtlb ⊢π∈ℝ*∧T∈ℝ*∧XmodT∈πT→π<XmodT
1019 155 934 1018 mp3an12 ⊢XmodT∈πT→π<XmodT
1020 1015 1016 1017 1019 gtnelioc ⊢XmodT∈πT→¬XmodT∈0π
1021 1020 iffalsed ⊢XmodT∈πT→ifXmodT∈0π1−1=−1
1022 1008 a1i ⊢⊤→X+π-XmodTX⊆ℝ
1023 363 1022 feqresmpt ⊢⊤→F↾X+π-XmodTX=x∈X+π-XmodTX⟼F⁡x
1024 1023 mptru ⊢F↾X+π-XmodTX=x∈X+π-XmodTX⟼F⁡x
1025 elioore ⊢x∈X+π-XmodTX→x∈ℝ
1026 1025 110 147 sylancl ⊢x∈X+π-XmodTX→F⁡x=ifxmodT<π1−1
1027 1026 adantl ⊢XmodT∈πT∧x∈X+π-XmodTX→F⁡x=ifxmodT<π1−1
1028 120 a1i ⊢XmodT∈πT∧x∈X+π-XmodTX→π∈ℝ
1029 135 a1i ⊢x∈X+π-XmodTX→T∈ℝ+
1030 1025 1029 modcld ⊢x∈X+π-XmodTX→xmodT∈ℝ
1031 1030 adantl ⊢XmodT∈πT∧x∈X+π-XmodTX→xmodT∈ℝ
1032 3 120 readdcli ⊢X+π∈ℝ
1033 1032 recni ⊢X+π∈ℂ
1034 1033 a1i ⊢x∈X+π-XmodTX→X+π∈ℂ
1035 27 a1i ⊢x∈X+π-XmodTX→X∈ℂ
1036 767 recni ⊢XmodT∈ℂ
1037 1036 a1i ⊢x∈X+π-XmodTX→XmodT∈ℂ
1038 1034 1035 1037 nnncan2d ⊢x∈X+π-XmodTX→X+π-XmodT-X−XmodT=X+π-X
1039 1038 861 eqtr2di ⊢x∈X+π-XmodTX→π=X+π-XmodT-X−XmodT
1040 1032 767 resubcli ⊢X+π-XmodT∈ℝ
1041 1040 a1i ⊢x∈X+π-XmodTX→X+π-XmodT∈ℝ
1042 768 a1i ⊢x∈X+π-XmodTX→X−XmodT∈ℝ
1043 1040 rexri ⊢X+π-XmodT∈ℝ*
1044 1043 a1i ⊢x∈X+π-XmodTX→X+π-XmodT∈ℝ*
1045 3 a1i ⊢x∈X+π-XmodTX→X∈ℝ
1046 1045 rexrd ⊢x∈X+π-XmodTX→X∈ℝ*
1047 id ⊢x∈X+π-XmodTX→x∈X+π-XmodTX
1048 ioogtlb ⊢X+π-XmodT∈ℝ*∧X∈ℝ*∧x∈X+π-XmodTX→X+π-XmodT<x
1049 1044 1046 1047 1048 syl3anc ⊢x∈X+π-XmodTX→X+π-XmodT<x
1050 1041 1025 1042 1049 ltsub1dd ⊢x∈X+π-XmodTX→X+π-XmodT-X−XmodT<x−X−XmodT
1051 1039 1050 eqbrtrd ⊢x∈X+π-XmodTX→π<x−X−XmodT
1052 1025 recnd ⊢x∈X+π-XmodTX→x∈ℂ
1053 sub31 ⊢x∈ℂ∧X∈ℂ∧XmodT∈ℂ→x−X−XmodT=XmodT−X−x
1054 1052 1035 1037 1053 syl3anc ⊢x∈X+π-XmodTX→x−X−XmodT=XmodT−X−x
1055 1051 1054 breqtrd ⊢x∈X+π-XmodTX→π<XmodT−X−x
1056 1055 adantl ⊢π<XmodT∧x∈X+π-XmodTX→π<XmodT−X−x
1057 1045 1025 resubcld ⊢x∈X+π-XmodTX→X−x∈ℝ
1058 0red ⊢x∈X+π-XmodTX→0∈ℝ
1059 iooltub ⊢X+π-XmodT∈ℝ*∧X∈ℝ*∧x∈X+π-XmodTX→x<X
1060 1044 1046 1047 1059 syl3anc ⊢x∈X+π-XmodTX→x<X
1061 1025 1045 posdifd ⊢x∈X+π-XmodTX→x<X↔0<X−x
1062 1060 1061 mpbid ⊢x∈X+π-XmodTX→0<X−x
1063 1058 1057 1062 ltled ⊢x∈X+π-XmodTX→0≤X−x
1064 1045 1041 resubcld ⊢x∈X+π-XmodTX→X−X+π-XmodT∈ℝ
1065 122 a1i ⊢x∈X+π-XmodTX→T∈ℝ
1066 1041 1025 1045 1049 ltsub2dd ⊢x∈X+π-XmodTX→X−x<X−X+π-XmodT
1067 sub31 ⊢X∈ℂ∧X+π∈ℂ∧XmodT∈ℂ→X−X+π-XmodT=XmodT−X+π-X
1068 27 1033 1036 1067 mp3an ⊢X−X+π-XmodT=XmodT−X+π-X
1069 861 oveq2i ⊢XmodT−X+π-X=XmodT−π
1070 1068 1069 eqtri ⊢X−X+π-XmodT=XmodT−π
1071 ltsubrp ⊢XmodT∈ℝ∧π∈ℝ+→XmodT−π<XmodT
1072 767 184 1071 mp2an ⊢XmodT−π<XmodT
1073 767 120 resubcli ⊢XmodT−π∈ℝ
1074 1073 767 122 lttri ⊢XmodT−π<XmodT∧XmodT<T→XmodT−π<T
1075 1072 962 1074 mp2an ⊢XmodT−π<T
1076 1070 1075 eqbrtri ⊢X−X+π-XmodT<T
1077 1076 a1i ⊢x∈X+π-XmodTX→X−X+π-XmodT<T
1078 1057 1064 1065 1066 1077 lttrd ⊢x∈X+π-XmodTX→X−x<T
1079 modid ⊢X−x∈ℝ∧T∈ℝ+∧0≤X−x∧X−x<T→X−xmodT=X−x
1080 1057 1029 1063 1078 1079 syl22anc ⊢x∈X+π-XmodTX→X−xmodT=X−x
1081 1080 oveq2d ⊢x∈X+π-XmodTX→XmodT−X−xmodT=XmodT−X−x
1082 1081 oveq1d ⊢x∈X+π-XmodTX→XmodT−X−xmodTmodT=XmodT−X−xmodT
1083 767 a1i ⊢x∈X+π-XmodTX→XmodT∈ℝ
1084 1083 1057 resubcld ⊢x∈X+π-XmodTX→XmodT−X−x∈ℝ
1085 120 a1i ⊢x∈X+π-XmodTX→π∈ℝ
1086 1054 1084 eqeltrd ⊢x∈X+π-XmodTX→x−X−XmodT∈ℝ
1087 72 a1i ⊢x∈X+π-XmodTX→0<π
1088 1058 1085 1086 1087 1051 lttrd ⊢x∈X+π-XmodTX→0<x−X−XmodT
1089 1088 1054 breqtrd ⊢x∈X+π-XmodTX→0<XmodT−X−x
1090 1058 1084 1089 ltled ⊢x∈X+π-XmodTX→0≤XmodT−X−x
1091 1045 1042 resubcld ⊢x∈X+π-XmodTX→X−X−XmodT∈ℝ
1092 1025 1045 1042 1060 ltsub1dd ⊢x∈X+π-XmodTX→x−X−XmodT<X−X−XmodT
1093 nncan ⊢X∈ℂ∧XmodT∈ℂ→X−X−XmodT=XmodT
1094 27 1036 1093 mp2an ⊢X−X−XmodT=XmodT
1095 1094 962 eqbrtri ⊢X−X−XmodT<T
1096 1095 a1i ⊢x∈X+π-XmodTX→X−X−XmodT<T
1097 1086 1091 1065 1092 1096 lttrd ⊢x∈X+π-XmodTX→x−X−XmodT<T
1098 1054 1097 eqbrtrrd ⊢x∈X+π-XmodTX→XmodT−X−x<T
1099 modid ⊢XmodT−X−x∈ℝ∧T∈ℝ+∧0≤XmodT−X−x∧XmodT−X−x<T→XmodT−X−xmodT=XmodT−X−x
1100 1084 1029 1090 1098 1099 syl22anc ⊢x∈X+π-XmodTX→XmodT−X−xmodT=XmodT−X−x
1101 1082 1100 eqtr2d ⊢x∈X+π-XmodTX→XmodT−X−x=XmodT−X−xmodTmodT
1102 modsubmodmod ⊢X∈ℝ∧X−x∈ℝ∧T∈ℝ+→XmodT−X−xmodTmodT=X−X−xmodT
1103 1045 1057 1029 1102 syl3anc ⊢x∈X+π-XmodTX→XmodT−X−xmodTmodT=X−X−xmodT
1104 1035 1052 nncand ⊢x∈X+π-XmodTX→X−X−x=x
1105 1104 oveq1d ⊢x∈X+π-XmodTX→X−X−xmodT=xmodT
1106 1101 1103 1105 3eqtrd ⊢x∈X+π-XmodTX→XmodT−X−x=xmodT
1107 1106 adantl ⊢π<XmodT∧x∈X+π-XmodTX→XmodT−X−x=xmodT
1108 1056 1107 breqtrd ⊢π<XmodT∧x∈X+π-XmodTX→π<xmodT
1109 1019 1108 sylan ⊢XmodT∈πT∧x∈X+π-XmodTX→π<xmodT
1110 1028 1031 1109 ltled ⊢XmodT∈πT∧x∈X+π-XmodTX→π≤xmodT
1111 1028 1031 1110 lensymd ⊢XmodT∈πT∧x∈X+π-XmodTX→¬xmodT<π
1112 1111 iffalsed ⊢XmodT∈πT∧x∈X+π-XmodTX→ifxmodT<π1−1=−1
1113 1027 1112 eqtrd ⊢XmodT∈πT∧x∈X+π-XmodTX→F⁡x=−1
1114 1113 mpteq2dva ⊢XmodT∈πT→x∈X+π-XmodTX⟼F⁡x=x∈X+π-XmodTX⟼−1
1115 1024 1114 eqtr2id ⊢XmodT∈πT→x∈X+π-XmodTX⟼−1=F↾X+π-XmodTX
1116 1115 oveq1d ⊢XmodT∈πT→x∈X+π-XmodTX⟼−1limℂX=F↾X+π-XmodTXlimℂX
1117 210 a1i ⊢XmodT∈πT→F:ℝ⟶ℂ
1118 1043 a1i ⊢XmodT∈πT→X+π-XmodT∈ℝ*
1119 3 a1i ⊢XmodT∈πT→X∈ℝ
1120 elioore ⊢XmodT∈πT→XmodT∈ℝ
1121 ltaddsublt ⊢X∈ℝ∧π∈ℝ∧XmodT∈ℝ→π<XmodT↔X+π-XmodT<X
1122 1119 1016 1120 1121 syl3anc ⊢XmodT∈πT→π<XmodT↔X+π-XmodT<X
1123 1019 1122 mpbid ⊢XmodT∈πT→X+π-XmodT<X
1124 365 a1i ⊢XmodT∈πT→−∞∈ℝ*
1125 mnflt ⊢X+π-XmodT∈ℝ→−∞<X+π-XmodT
1126 xrltle ⊢−∞∈ℝ*∧X+π-XmodT∈ℝ*→−∞<X+π-XmodT→−∞≤X+π-XmodT
1127 365 1043 1126 mp2an ⊢−∞<X+π-XmodT→−∞≤X+π-XmodT
1128 1040 1125 1127 mp2b ⊢−∞≤X+π-XmodT
1129 1128 a1i ⊢XmodT∈πT→−∞≤X+π-XmodT
1130 1117 1118 1119 1123 1009 1124 1129 limcresiooub ⊢XmodT∈πT→F↾X+π-XmodTXlimℂX=F↾−∞XlimℂX
1131 1116 1130 eqtr2d ⊢XmodT∈πT→F↾−∞XlimℂX=x∈X+π-XmodTX⟼−1limℂX
1132 1014 1021 1131 3eltr4d ⊢XmodT∈πT→ifXmodT∈0π1−1∈F↾−∞XlimℂX
1133 1006 1132 syl ⊢XmodT∈πT∧¬XmodT=π→ifXmodT∈0π1−1∈F↾−∞XlimℂX
1134 994 1133 pm2.61dan ⊢XmodT∈πT→ifXmodT∈0π1−1∈F↾−∞XlimℂX
1135 964 1134 syl ⊢¬XmodT∈0π∧¬XmodT=0→ifXmodT∈0π1−1∈F↾−∞XlimℂX
1136 932 1135 pm2.61dan ⊢¬XmodT∈0π→ifXmodT∈0π1−1∈F↾−∞XlimℂX
1137 814 1136 pm2.61i ⊢ifXmodT∈0π1−1∈F↾−∞XlimℂX
1138 eqid ⊢x∈XX+π-XmodT⟼1=x∈XX+π-XmodT⟼1
1139 ioossre ⊢XX+π-XmodT⊆ℝ
1140 1139 a1i ⊢⊤→XX+π-XmodT⊆ℝ
1141 1140 208 sstrdi ⊢⊤→XX+π-XmodT⊆ℂ
1142 1138 1141 204 819 constlimc ⊢⊤→1∈x∈XX+π-XmodT⟼1limℂX
1143 1142 mptru ⊢1∈x∈XX+π-XmodT⟼1limℂX
1144 1143 a1i ⊢XmodT∈0π→1∈x∈XX+π-XmodT⟼1limℂX
1145 2 a1i ⊢XmodT∈0π→F=x∈ℝ⟼ifxmodT<π1−1
1146 oveq1 ⊢x=X→xmodT=XmodT
1147 1146 breq1d ⊢x=X→xmodT<π↔XmodT<π
1148 1147 ifbid ⊢x=X→ifxmodT<π1−1=ifXmodT<π1−1
1149 1148 adantl ⊢XmodT∈0π∧x=X→ifxmodT<π1−1=ifXmodT<π1−1
1150 3 a1i ⊢XmodT∈0π→X∈ℝ
1151 108 109 ifcli ⊢ifXmodT<π1−1∈ℝ
1152 1151 a1i ⊢XmodT∈0π→ifXmodT<π1−1∈ℝ
1153 1145 1149 1150 1152 fvmptd ⊢XmodT∈0π→F⁡X=ifXmodT<π1−1
1154 icoltub ⊢0∈ℝ*∧π∈ℝ*∧XmodT∈0π→XmodT<π
1155 153 155 1154 mp3an12 ⊢XmodT∈0π→XmodT<π
1156 1155 iftrued ⊢XmodT∈0π→ifXmodT<π1−1=1
1157 1153 1156 eqtrd ⊢XmodT∈0π→F⁡X=1
1158 363 1140 feqresmpt ⊢⊤→F↾XX+π-XmodT=x∈XX+π-XmodT⟼F⁡x
1159 1158 mptru ⊢F↾XX+π-XmodT=x∈XX+π-XmodT⟼F⁡x
1160 elioore ⊢x∈XX+π-XmodT→x∈ℝ
1161 1160 110 147 sylancl ⊢x∈XX+π-XmodT→F⁡x=ifxmodT<π1−1
1162 1161 adantl ⊢XmodT∈0π∧x∈XX+π-XmodT→F⁡x=ifxmodT<π1−1
1163 3 a1i ⊢x∈XX+π-XmodT→X∈ℝ
1164 1160 1163 resubcld ⊢x∈XX+π-XmodT→x−X∈ℝ
1165 135 a1i ⊢x∈XX+π-XmodT→T∈ℝ+
1166 0red ⊢x∈XX+π-XmodT→0∈ℝ
1167 1163 rexrd ⊢x∈XX+π-XmodT→X∈ℝ*
1168 120 767 resubcli ⊢π−XmodT∈ℝ
1169 3 1168 readdcli ⊢X+π-XmodT∈ℝ
1170 1169 rexri ⊢X+π-XmodT∈ℝ*
1171 1170 a1i ⊢x∈XX+π-XmodT→X+π-XmodT∈ℝ*
1172 id ⊢x∈XX+π-XmodT→x∈XX+π-XmodT
1173 ioogtlb ⊢X∈ℝ*∧X+π-XmodT∈ℝ*∧x∈XX+π-XmodT→X<x
1174 1167 1171 1172 1173 syl3anc ⊢x∈XX+π-XmodT→X<x
1175 1163 1160 posdifd ⊢x∈XX+π-XmodT→X<x↔0<x−X
1176 1174 1175 mpbid ⊢x∈XX+π-XmodT→0<x−X
1177 1166 1164 1176 ltled ⊢x∈XX+π-XmodT→0≤x−X
1178 120 a1i ⊢x∈XX+π-XmodT→π∈ℝ
1179 122 a1i ⊢x∈XX+π-XmodT→T∈ℝ
1180 1169 a1i ⊢x∈XX+π-XmodT→X+π-XmodT∈ℝ
1181 1180 1163 resubcld ⊢x∈XX+π-XmodT→X+π−XmodT-X∈ℝ
1182 iooltub ⊢X∈ℝ*∧X+π-XmodT∈ℝ*∧x∈XX+π-XmodT→x<X+π-XmodT
1183 1167 1171 1172 1182 syl3anc ⊢x∈XX+π-XmodT→x<X+π-XmodT
1184 1160 1180 1163 1183 ltsub1dd ⊢x∈XX+π-XmodT→x−X<X+π−XmodT-X
1185 1168 recni ⊢π−XmodT∈ℂ
1186 pncan2 ⊢X∈ℂ∧π−XmodT∈ℂ→X+π−XmodT-X=π−XmodT
1187 27 1185 1186 mp2an ⊢X+π−XmodT-X=π−XmodT
1188 subge02 ⊢π∈ℝ∧XmodT∈ℝ→0≤XmodT↔π−XmodT≤π
1189 120 767 1188 mp2an ⊢0≤XmodT↔π−XmodT≤π
1190 950 1189 mpbi ⊢π−XmodT≤π
1191 1187 1190 eqbrtri ⊢X+π−XmodT-X≤π
1192 1191 a1i ⊢x∈XX+π-XmodT→X+π−XmodT-X≤π
1193 1164 1181 1178 1184 1192 ltletrd ⊢x∈XX+π-XmodT→x−X<π
1194 187 a1i ⊢x∈XX+π-XmodT→π<T
1195 1164 1178 1179 1193 1194 lttrd ⊢x∈XX+π-XmodT→x−X<T
1196 modid ⊢x−X∈ℝ∧T∈ℝ+∧0≤x−X∧x−X<T→x−XmodT=x−X
1197 1164 1165 1177 1195 1196 syl22anc ⊢x∈XX+π-XmodT→x−XmodT=x−X
1198 1197 oveq2d ⊢x∈XX+π-XmodT→XmodT+x−XmodT=XmodT+x-X
1199 1198 oveq1d ⊢x∈XX+π-XmodT→XmodT+x−XmodTmodT=XmodT+x-XmodT
1200 767 a1i ⊢x∈XX+π-XmodT→XmodT∈ℝ
1201 1200 1164 readdcld ⊢x∈XX+π-XmodT→XmodT+x-X∈ℝ
1202 1163 1163 resubcld ⊢x∈XX+π-XmodT→X−X∈ℝ
1203 1200 1202 readdcld ⊢x∈XX+π-XmodT→XmodT+X-X∈ℝ
1204 27 subidi ⊢X−X=0
1205 1204 oveq2i ⊢XmodT+X-X=XmodT+0
1206 1036 addridi ⊢XmodT+0=XmodT
1207 1205 1206 eqtr2i ⊢XmodT=XmodT+X-X
1208 950 1207 breqtri ⊢0≤XmodT+X-X
1209 1208 a1i ⊢x∈XX+π-XmodT→0≤XmodT+X-X
1210 1163 1160 1163 1174 ltsub1dd ⊢x∈XX+π-XmodT→X−X<x−X
1211 1202 1164 1200 1210 ltadd2dd ⊢x∈XX+π-XmodT→XmodT+X-X<XmodT+x-X
1212 1166 1203 1201 1209 1211 lelttrd ⊢x∈XX+π-XmodT→0<XmodT+x-X
1213 1166 1201 1212 ltled ⊢x∈XX+π-XmodT→0≤XmodT+x-X
1214 1164 1181 1200 1184 ltadd2dd ⊢x∈XX+π-XmodT→XmodT+x-X<XmodT+X+π-XmodT-X
1215 1187 oveq2i ⊢XmodT+X+π-XmodT-X=XmodT+π-XmodT
1216 1036 56 pncan3i ⊢XmodT+π-XmodT=π
1217 1215 1216 eqtri ⊢XmodT+X+π-XmodT-X=π
1218 1214 1217 breqtrdi ⊢x∈XX+π-XmodT→XmodT+x-X<π
1219 1201 1178 1179 1218 1194 lttrd ⊢x∈XX+π-XmodT→XmodT+x-X<T
1220 modid ⊢XmodT+x-X∈ℝ∧T∈ℝ+∧0≤XmodT+x-X∧XmodT+x-X<T→XmodT+x-XmodT=XmodT+x-X
1221 1201 1165 1213 1219 1220 syl22anc ⊢x∈XX+π-XmodT→XmodT+x-XmodT=XmodT+x-X
1222 1199 1221 eqtr2d ⊢x∈XX+π-XmodT→XmodT+x-X=XmodT+x−XmodTmodT
1223 modaddabs ⊢X∈ℝ∧x−X∈ℝ∧T∈ℝ+→XmodT+x−XmodTmodT=X+x-XmodT
1224 1163 1164 1165 1223 syl3anc ⊢x∈XX+π-XmodT→XmodT+x−XmodTmodT=X+x-XmodT
1225 27 a1i ⊢x∈XX+π-XmodT→X∈ℂ
1226 1160 recnd ⊢x∈XX+π-XmodT→x∈ℂ
1227 1225 1226 pncan3d ⊢x∈XX+π-XmodT→X+x-X=x
1228 1227 oveq1d ⊢x∈XX+π-XmodT→X+x-XmodT=xmodT
1229 1222 1224 1228 3eqtrrd ⊢x∈XX+π-XmodT→xmodT=XmodT+x-X
1230 1229 adantl ⊢XmodT<π∧x∈XX+π-XmodT→xmodT=XmodT+x-X
1231 1218 adantl ⊢XmodT<π∧x∈XX+π-XmodT→XmodT+x-X<π
1232 1230 1231 eqbrtrd ⊢XmodT<π∧x∈XX+π-XmodT→xmodT<π
1233 1155 1232 sylan ⊢XmodT∈0π∧x∈XX+π-XmodT→xmodT<π
1234 1233 iftrued ⊢XmodT∈0π∧x∈XX+π-XmodT→ifxmodT<π1−1=1
1235 1162 1234 eqtrd ⊢XmodT∈0π∧x∈XX+π-XmodT→F⁡x=1
1236 1235 mpteq2dva ⊢XmodT∈0π→x∈XX+π-XmodT⟼F⁡x=x∈XX+π-XmodT⟼1
1237 1159 1236 eqtr2id ⊢XmodT∈0π→x∈XX+π-XmodT⟼1=F↾XX+π-XmodT
1238 1237 oveq1d ⊢XmodT∈0π→x∈XX+π-XmodT⟼1limℂX=F↾XX+π-XmodTlimℂX
1239 210 a1i ⊢XmodT∈0π→F:ℝ⟶ℂ
1240 1170 a1i ⊢XmodT∈0π→X+π-XmodT∈ℝ*
1241 1168 a1i ⊢XmodT∈0π→π−XmodT∈ℝ
1242 767 a1i ⊢XmodT∈0π→XmodT∈ℝ
1243 120 a1i ⊢XmodT∈0π→π∈ℝ
1244 1242 1243 posdifd ⊢XmodT∈0π→XmodT<π↔0<π−XmodT
1245 1155 1244 mpbid ⊢XmodT∈0π→0<π−XmodT
1246 1241 1245 elrpd ⊢XmodT∈0π→π−XmodT∈ℝ+
1247 1150 1246 ltaddrpd ⊢XmodT∈0π→X<X+π-XmodT
1248 1139 a1i ⊢XmodT∈0π→XX+π-XmodT⊆ℝ
1249 376 a1i ⊢XmodT∈0π→+∞∈ℝ*
1250 ltpnf ⊢X+π-XmodT∈ℝ→X+π-XmodT<+∞
1251 xrltle ⊢X+π-XmodT∈ℝ*∧+∞∈ℝ*→X+π-XmodT<+∞→X+π-XmodT≤+∞
1252 1170 376 1251 mp2an ⊢X+π-XmodT<+∞→X+π-XmodT≤+∞
1253 1169 1250 1252 mp2b ⊢X+π-XmodT≤+∞
1254 1253 a1i ⊢XmodT∈0π→X+π-XmodT≤+∞
1255 1239 1150 1240 1247 1248 1249 1254 limcresioolb ⊢XmodT∈0π→F↾XX+π-XmodTlimℂX=F↾X+∞limℂX
1256 1238 1255 eqtr2d ⊢XmodT∈0π→F↾X+∞limℂX=x∈XX+π-XmodT⟼1limℂX
1257 1144 1157 1256 3eltr4d ⊢XmodT∈0π→F⁡X∈F↾X+∞limℂX
1258 155 a1i ⊢¬XmodT∈0π→π∈ℝ*
1259 934 a1i ⊢¬XmodT∈0π→T∈ℝ*
1260 936 a1i ⊢¬XmodT∈0π→XmodT∈ℝ*
1261 153 a1i ⊢¬XmodT∈0π∧¬π≤XmodT→0∈ℝ*
1262 155 a1i ⊢¬XmodT∈0π∧¬π≤XmodT→π∈ℝ*
1263 936 a1i ⊢¬XmodT∈0π∧¬π≤XmodT→XmodT∈ℝ*
1264 950 a1i ⊢¬XmodT∈0π∧¬π≤XmodT→0≤XmodT
1265 767 a1i ⊢¬π≤XmodT→XmodT∈ℝ
1266 120 a1i ⊢¬π≤XmodT→π∈ℝ
1267 1265 1266 ltnled ⊢¬π≤XmodT→XmodT<π↔¬π≤XmodT
1268 1267 ibir ⊢¬π≤XmodT→XmodT<π
1269 1268 adantl ⊢¬XmodT∈0π∧¬π≤XmodT→XmodT<π
1270 1261 1262 1263 1264 1269 elicod ⊢¬XmodT∈0π∧¬π≤XmodT→XmodT∈0π
1271 simpl ⊢¬XmodT∈0π∧¬π≤XmodT→¬XmodT∈0π
1272 1270 1271 condan ⊢¬XmodT∈0π→π≤XmodT
1273 962 a1i ⊢¬XmodT∈0π→XmodT<T
1274 1258 1259 1260 1272 1273 elicod ⊢¬XmodT∈0π→XmodT∈πT
1275 eqid ⊢x∈XX+T-XmodT⟼−1=x∈XX+T-XmodT⟼−1
1276 ioossre ⊢XX+T-XmodT⊆ℝ
1277 1276 a1i ⊢⊤→XX+T-XmodT⊆ℝ
1278 1277 208 sstrdi ⊢⊤→XX+T-XmodT⊆ℂ
1279 1275 1278 306 819 constlimc ⊢⊤→−1∈x∈XX+T-XmodT⟼−1limℂX
1280 1279 mptru ⊢−1∈x∈XX+T-XmodT⟼−1limℂX
1281 1280 a1i ⊢XmodT∈πT→−1∈x∈XX+T-XmodT⟼−1limℂX
1282 1ex ⊢1∈V
1283 109 elexi ⊢−1∈V
1284 1282 1283 ifex ⊢ifXmodT<π1−1∈V
1285 1148 2 1284 fvmpt ⊢X∈ℝ→F⁡X=ifXmodT<π1−1
1286 3 1285 ax-mp ⊢F⁡X=ifXmodT<π1−1
1287 1286 a1i ⊢XmodT∈πT→F⁡X=ifXmodT<π1−1
1288 120 a1i ⊢XmodT∈πT→π∈ℝ
1289 767 a1i ⊢XmodT∈πT→XmodT∈ℝ
1290 1288 1289 1000 lensymd ⊢XmodT∈πT→¬XmodT<π
1291 1290 iffalsed ⊢XmodT∈πT→ifXmodT<π1−1=−1
1292 1287 1291 eqtrd ⊢XmodT∈πT→F⁡X=−1
1293 363 1277 feqresmpt ⊢⊤→F↾XX+T-XmodT=x∈XX+T-XmodT⟼F⁡x
1294 1293 mptru ⊢F↾XX+T-XmodT=x∈XX+T-XmodT⟼F⁡x
1295 elioore ⊢x∈XX+T-XmodT→x∈ℝ
1296 1295 110 147 sylancl ⊢x∈XX+T-XmodT→F⁡x=ifxmodT<π1−1
1297 1296 adantl ⊢XmodT∈πT∧x∈XX+T-XmodT→F⁡x=ifxmodT<π1−1
1298 120 a1i ⊢XmodT∈πT∧x∈XX+T-XmodT→π∈ℝ
1299 3 a1i ⊢x∈XX+T-XmodT→X∈ℝ
1300 1295 1299 resubcld ⊢x∈XX+T-XmodT→x−X∈ℝ
1301 135 a1i ⊢x∈XX+T-XmodT→T∈ℝ+
1302 0red ⊢x∈XX+T-XmodT→0∈ℝ
1303 1299 rexrd ⊢x∈XX+T-XmodT→X∈ℝ*
1304 122 767 resubcli ⊢T−XmodT∈ℝ
1305 3 1304 readdcli ⊢X+T-XmodT∈ℝ
1306 1305 rexri ⊢X+T-XmodT∈ℝ*
1307 1306 a1i ⊢x∈XX+T-XmodT→X+T-XmodT∈ℝ*
1308 id ⊢x∈XX+T-XmodT→x∈XX+T-XmodT
1309 ioogtlb ⊢X∈ℝ*∧X+T-XmodT∈ℝ*∧x∈XX+T-XmodT→X<x
1310 1303 1307 1308 1309 syl3anc ⊢x∈XX+T-XmodT→X<x
1311 1299 1295 posdifd ⊢x∈XX+T-XmodT→X<x↔0<x−X
1312 1310 1311 mpbid ⊢x∈XX+T-XmodT→0<x−X
1313 1302 1300 1312 ltled ⊢x∈XX+T-XmodT→0≤x−X
1314 1305 a1i ⊢x∈XX+T-XmodT→X+T-XmodT∈ℝ
1315 1314 1299 resubcld ⊢x∈XX+T-XmodT→X+T−XmodT-X∈ℝ
1316 122 a1i ⊢x∈XX+T-XmodT→T∈ℝ
1317 iooltub ⊢X∈ℝ*∧X+T-XmodT∈ℝ*∧x∈XX+T-XmodT→x<X+T-XmodT
1318 1303 1307 1308 1317 syl3anc ⊢x∈XX+T-XmodT→x<X+T-XmodT
1319 1295 1314 1299 1318 ltsub1dd ⊢x∈XX+T-XmodT→x−X<X+T−XmodT-X
1320 1304 recni ⊢T−XmodT∈ℂ
1321 pncan2 ⊢X∈ℂ∧T−XmodT∈ℂ→X+T−XmodT-X=T−XmodT
1322 27 1320 1321 mp2an ⊢X+T−XmodT-X=T−XmodT
1323 subge02 ⊢T∈ℝ∧XmodT∈ℝ→0≤XmodT↔T−XmodT≤T
1324 122 767 1323 mp2an ⊢0≤XmodT↔T−XmodT≤T
1325 950 1324 mpbi ⊢T−XmodT≤T
1326 1322 1325 eqbrtri ⊢X+T−XmodT-X≤T
1327 1326 a1i ⊢x∈XX+T-XmodT→X+T−XmodT-X≤T
1328 1300 1315 1316 1319 1327 ltletrd ⊢x∈XX+T-XmodT→x−X<T
1329 1300 1301 1313 1328 1196 syl22anc ⊢x∈XX+T-XmodT→x−XmodT=x−X
1330 1329 oveq2d ⊢x∈XX+T-XmodT→XmodT+x−XmodT=XmodT+x-X
1331 1330 oveq1d ⊢x∈XX+T-XmodT→XmodT+x−XmodTmodT=XmodT+x-XmodT
1332 readdcl ⊢XmodT∈ℝ∧x−X∈ℝ→XmodT+x-X∈ℝ
1333 767 1300 1332 sylancr ⊢x∈XX+T-XmodT→XmodT+x-X∈ℝ
1334 767 a1i ⊢x∈XX+T-XmodT→XmodT∈ℝ
1335 950 a1i ⊢x∈XX+T-XmodT→0≤XmodT
1336 1334 1300 1335 1312 addgegt0d ⊢x∈XX+T-XmodT→0<XmodT+x-X
1337 1302 1333 1336 ltled ⊢x∈XX+T-XmodT→0≤XmodT+x-X
1338 1300 1315 1334 1319 ltadd2dd ⊢x∈XX+T-XmodT→XmodT+x-X<XmodT+X+T-XmodT-X
1339 1322 oveq2i ⊢XmodT+X+T-XmodT-X=XmodT+T-XmodT
1340 1036 123 pncan3i ⊢XmodT+T-XmodT=T
1341 1339 1340 eqtri ⊢XmodT+X+T-XmodT-X=T
1342 1338 1341 breqtrdi ⊢x∈XX+T-XmodT→XmodT+x-X<T
1343 1333 1301 1337 1342 1220 syl22anc ⊢x∈XX+T-XmodT→XmodT+x-XmodT=XmodT+x-X
1344 1331 1343 eqtr2d ⊢x∈XX+T-XmodT→XmodT+x-X=XmodT+x−XmodTmodT
1345 1299 1300 1301 1223 syl3anc ⊢x∈XX+T-XmodT→XmodT+x−XmodTmodT=X+x-XmodT
1346 27 a1i ⊢x∈XX+T-XmodT→X∈ℂ
1347 1295 recnd ⊢x∈XX+T-XmodT→x∈ℂ
1348 1346 1347 pncan3d ⊢x∈XX+T-XmodT→X+x-X=x
1349 1348 oveq1d ⊢x∈XX+T-XmodT→X+x-XmodT=xmodT
1350 1344 1345 1349 3eqtrd ⊢x∈XX+T-XmodT→XmodT+x-X=xmodT
1351 1350 adantl ⊢XmodT∈πT∧x∈XX+T-XmodT→XmodT+x-X=xmodT
1352 1333 adantl ⊢XmodT∈πT∧x∈XX+T-XmodT→XmodT+x-X∈ℝ
1353 1351 1352 eqeltrrd ⊢XmodT∈πT∧x∈XX+T-XmodT→xmodT∈ℝ
1354 767 a1i ⊢XmodT∈πT∧x∈XX+T-XmodT→XmodT∈ℝ
1355 1000 adantr ⊢XmodT∈πT∧x∈XX+T-XmodT→π≤XmodT
1356 1300 1312 elrpd ⊢x∈XX+T-XmodT→x−X∈ℝ+
1357 1334 1356 ltaddrpd ⊢x∈XX+T-XmodT→XmodT<XmodT+x-X
1358 1357 adantl ⊢XmodT∈πT∧x∈XX+T-XmodT→XmodT<XmodT+x-X
1359 1298 1354 1352 1355 1358 lelttrd ⊢XmodT∈πT∧x∈XX+T-XmodT→π<XmodT+x-X
1360 1298 1352 1359 ltled ⊢XmodT∈πT∧x∈XX+T-XmodT→π≤XmodT+x-X
1361 1360 1351 breqtrd ⊢XmodT∈πT∧x∈XX+T-XmodT→π≤xmodT
1362 1298 1353 1361 lensymd ⊢XmodT∈πT∧x∈XX+T-XmodT→¬xmodT<π
1363 1362 iffalsed ⊢XmodT∈πT∧x∈XX+T-XmodT→ifxmodT<π1−1=−1
1364 1297 1363 eqtrd ⊢XmodT∈πT∧x∈XX+T-XmodT→F⁡x=−1
1365 1364 mpteq2dva ⊢XmodT∈πT→x∈XX+T-XmodT⟼F⁡x=x∈XX+T-XmodT⟼−1
1366 1294 1365 eqtr2id ⊢XmodT∈πT→x∈XX+T-XmodT⟼−1=F↾XX+T-XmodT
1367 1366 oveq1d ⊢XmodT∈πT→x∈XX+T-XmodT⟼−1limℂX=F↾XX+T-XmodTlimℂX
1368 210 a1i ⊢XmodT∈πT→F:ℝ⟶ℂ
1369 3 a1i ⊢XmodT∈πT→X∈ℝ
1370 1306 a1i ⊢XmodT∈πT→X+T-XmodT∈ℝ*
1371 1304 a1i ⊢XmodT∈πT→T−XmodT∈ℝ
1372 962 a1i ⊢XmodT∈πT→XmodT<T
1373 122 a1i ⊢XmodT∈πT→T∈ℝ
1374 1289 1373 posdifd ⊢XmodT∈πT→XmodT<T↔0<T−XmodT
1375 1372 1374 mpbid ⊢XmodT∈πT→0<T−XmodT
1376 1371 1375 elrpd ⊢XmodT∈πT→T−XmodT∈ℝ+
1377 1369 1376 ltaddrpd ⊢XmodT∈πT→X<X+T-XmodT
1378 1276 a1i ⊢XmodT∈πT→XX+T-XmodT⊆ℝ
1379 376 a1i ⊢XmodT∈πT→+∞∈ℝ*
1380 ltpnf ⊢X+T-XmodT∈ℝ→X+T-XmodT<+∞
1381 xrltle ⊢X+T-XmodT∈ℝ*∧+∞∈ℝ*→X+T-XmodT<+∞→X+T-XmodT≤+∞
1382 1306 376 1381 mp2an ⊢X+T-XmodT<+∞→X+T-XmodT≤+∞
1383 1305 1380 1382 mp2b ⊢X+T-XmodT≤+∞
1384 1383 a1i ⊢XmodT∈πT→X+T-XmodT≤+∞
1385 1368 1369 1370 1377 1378 1379 1384 limcresioolb ⊢XmodT∈πT→F↾XX+T-XmodTlimℂX=F↾X+∞limℂX
1386 1367 1385 eqtr2d ⊢XmodT∈πT→F↾X+∞limℂX=x∈XX+T-XmodT⟼−1limℂX
1387 1281 1292 1386 3eltr4d ⊢XmodT∈πT→F⁡X∈F↾X+∞limℂX
1388 1274 1387 syl ⊢¬XmodT∈0π→F⁡X∈F↾X+∞limℂX
1389 1257 1388 pm2.61i ⊢F⁡X∈F↾X+∞limℂX
1390 id ⊢n∈ℕ0→n∈ℕ0
1391 1 2 1390 sqwvfoura ⊢n∈ℕ0→∫−ππF⁡x⁢cos⁡n⁢xdxπ=0
1392 1391 eqcomd ⊢n∈ℕ0→0=∫−ππF⁡x⁢cos⁡n⁢xdxπ
1393 1392 mpteq2ia ⊢n∈ℕ0⟼0=n∈ℕ0⟼∫−ππF⁡x⁢cos⁡n⁢xdxπ
1394 id ⊢n∈ℕ→n∈ℕ
1395 1 2 1394 sqwvfourb ⊢n∈ℕ→∫−ππF⁡x⁢sin⁡n⁢xdxπ=if2∥n04n⁢π
1396 1395 eqcomd ⊢n∈ℕ→if2∥n04n⁢π=∫−ππF⁡x⁢sin⁡n⁢xdxπ
1397 1396 mpteq2ia ⊢n∈ℕ⟼if2∥n04n⁢π=n∈ℕ⟼∫−ππF⁡x⁢sin⁡n⁢xdxπ
1398 nnnn0 ⊢n∈ℕ→n∈ℕ0
1399 0red ⊢n∈ℕ→0∈ℝ
1400 eqid ⊢n∈ℕ0⟼0=n∈ℕ0⟼0
1401 1400 fvmpt2 ⊢n∈ℕ0∧0∈ℝ→n∈ℕ0⟼0⁡n=0
1402 1398 1399 1401 syl2anc ⊢n∈ℕ→n∈ℕ0⟼0⁡n=0
1403 1402 oveq1d ⊢n∈ℕ→n∈ℕ0⟼0⁡n⁢cos⁡n⁢X=0⋅cos⁡n⁢X
1404 78 coscld ⊢n∈ℕ→cos⁡n⁢X∈ℂ
1405 1404 mul02d ⊢n∈ℕ→0⋅cos⁡n⁢X=0
1406 1403 1405 eqtrd ⊢n∈ℕ→n∈ℕ0⟼0⁡n⁢cos⁡n⁢X=0
1407 ovex ⊢4n⁢π∈V
1408 93 1407 ifex ⊢if2∥n04n⁢π∈V
1409 eqid ⊢n∈ℕ⟼if2∥n04n⁢π=n∈ℕ⟼if2∥n04n⁢π
1410 1409 fvmpt2 ⊢n∈ℕ∧if2∥n04n⁢π∈V→n∈ℕ⟼if2∥n04n⁢π⁡n=if2∥n04n⁢π
1411 1408 1410 mpan2 ⊢n∈ℕ→n∈ℕ⟼if2∥n04n⁢π⁡n=if2∥n04n⁢π
1412 1411 oveq1d ⊢n∈ℕ→n∈ℕ⟼if2∥n04n⁢π⁡n⁢sin⁡n⁢X=if2∥n04n⁢π⁢sin⁡n⁢X
1413 1406 1412 oveq12d ⊢n∈ℕ→n∈ℕ0⟼0⁡n⁢cos⁡n⁢X+n∈ℕ⟼if2∥n04n⁢π⁡n⁢sin⁡n⁢X=0+if2∥n04n⁢π⁢sin⁡n⁢X
1414 64 76 ifcld ⊢n∈ℕ→if2∥n04n⁢π∈ℂ
1415 1414 79 mulcld ⊢n∈ℕ→if2∥n04n⁢π⁢sin⁡n⁢X∈ℂ
1416 1415 addlidd ⊢n∈ℕ→0+if2∥n04n⁢π⁢sin⁡n⁢X=if2∥n04n⁢π⁢sin⁡n⁢X
1417 iftrue ⊢2∥n→if2∥n04n⁢π=0
1418 1417 oveq1d ⊢2∥n→if2∥n04n⁢π⁢sin⁡n⁢X=0⋅sin⁡n⁢X
1419 79 mul02d ⊢n∈ℕ→0⋅sin⁡n⁢X=0
1420 1418 1419 sylan9eqr ⊢n∈ℕ∧2∥n→if2∥n04n⁢π⁢sin⁡n⁢X=0
1421 iftrue ⊢2∥n→if2∥n04n⁢π⁢sin⁡n⁢X=0
1422 1421 eqcomd ⊢2∥n→0=if2∥n04n⁢π⁢sin⁡n⁢X
1423 1422 adantl ⊢n∈ℕ∧2∥n→0=if2∥n04n⁢π⁢sin⁡n⁢X
1424 1420 1423 eqtrd ⊢n∈ℕ∧2∥n→if2∥n04n⁢π⁢sin⁡n⁢X=if2∥n04n⁢π⁢sin⁡n⁢X
1425 iffalse ⊢¬2∥n→if2∥n04n⁢π=4n⁢π
1426 1425 oveq1d ⊢¬2∥n→if2∥n04n⁢π⁢sin⁡n⁢X=4n⁢π⁢sin⁡n⁢X
1427 1426 adantl ⊢n∈ℕ∧¬2∥n→if2∥n04n⁢π⁢sin⁡n⁢X=4n⁢π⁢sin⁡n⁢X
1428 iffalse ⊢¬2∥n→if2∥n04n⁢π⁢sin⁡n⁢X=4n⁢π⁢sin⁡n⁢X
1429 1428 eqcomd ⊢¬2∥n→4n⁢π⁢sin⁡n⁢X=if2∥n04n⁢π⁢sin⁡n⁢X
1430 1429 adantl ⊢n∈ℕ∧¬2∥n→4n⁢π⁢sin⁡n⁢X=if2∥n04n⁢π⁢sin⁡n⁢X
1431 1427 1430 eqtrd ⊢n∈ℕ∧¬2∥n→if2∥n04n⁢π⁢sin⁡n⁢X=if2∥n04n⁢π⁢sin⁡n⁢X
1432 1424 1431 pm2.61dan ⊢n∈ℕ→if2∥n04n⁢π⁢sin⁡n⁢X=if2∥n04n⁢π⁢sin⁡n⁢X
1433 1413 1416 1432 3eqtrrd ⊢n∈ℕ→if2∥n04n⁢π⁢sin⁡n⁢X=n∈ℕ0⟼0⁡n⁢cos⁡n⁢X+n∈ℕ⟼if2∥n04n⁢π⁡n⁢sin⁡n⁢X
1434 1433 mpteq2ia ⊢n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X=n∈ℕ⟼n∈ℕ0⟼0⁡n⁢cos⁡n⁢X+n∈ℕ⟼if2∥n04n⁢π⁡n⁢sin⁡n⁢X
1435 112 1 149 150 331 605 676 755 3 1137 1389 1393 1397 1434 fourierclim ⊢seq1+n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X⇝ifXmodT∈0π1−1+F⁡X2−n∈ℕ0⟼0⁡02
1436 0nn0 ⊢0∈ℕ0
1437 eqidd ⊢n=0→0=0
1438 1437 1400 93 fvmpt ⊢0∈ℕ0→n∈ℕ0⟼0⁡0=0
1439 1436 1438 ax-mp ⊢n∈ℕ0⟼0⁡0=0
1440 1439 oveq1i ⊢n∈ℕ0⟼0⁡02=02
1441 32 recni ⊢2∈ℂ
1442 71 131 gtneii ⊢2≠0
1443 1441 1442 div0i ⊢02=0
1444 1440 1443 eqtri ⊢n∈ℕ0⟼0⁡02=0
1445 1444 oveq2i ⊢ifXmodT∈0π1−1+F⁡X2−n∈ℕ0⟼0⁡02=ifXmodT∈0π1−1+F⁡X2−0
1446 204 mptru ⊢1∈ℂ
1447 1446 1011 ifcli ⊢ifXmodT∈0π1−1∈ℂ
1448 1151 recni ⊢ifXmodT<π1−1∈ℂ
1449 1286 1448 eqeltri ⊢F⁡X∈ℂ
1450 1447 1449 addcli ⊢ifXmodT∈0π1−1+F⁡X∈ℂ
1451 1450 1441 1442 divcli ⊢ifXmodT∈0π1−1+F⁡X2∈ℂ
1452 1451 subid1i ⊢ifXmodT∈0π1−1+F⁡X2−0=ifXmodT∈0π1−1+F⁡X2
1453 1445 1452 eqtri ⊢ifXmodT∈0π1−1+F⁡X2−n∈ℕ0⟼0⁡02=ifXmodT∈0π1−1+F⁡X2
1454 1435 1453 breqtri ⊢seq1+n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X⇝ifXmodT∈0π1−1+F⁡X2
1455 1454 a1i ⊢⊤→seq1+n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X⇝ifXmodT∈0π1−1+F⁡X2
1456 83 107 1455 sumnnodd ⊢⊤→seq1+k∈ℕ⟼n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X⁡2⁢k−1⇝ifXmodT∈0π1−1+F⁡X2∧∑k∈ℕn∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X⁡k=∑k∈ℕn∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X⁡2⁢k−1
1457 1456 mptru ⊢seq1+k∈ℕ⟼n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X⁡2⁢k−1⇝ifXmodT∈0π1−1+F⁡X2∧∑k∈ℕn∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X⁡k=∑k∈ℕn∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X⁡2⁢k−1
1458 1457 simpli ⊢seq1+k∈ℕ⟼n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X⁡2⁢k−1⇝ifXmodT∈0π1−1+F⁡X2
1459 breq2 ⊢n=2⁢k−1→2∥n↔2∥2⁢k−1
1460 oveq1 ⊢n=2⁢k−1→n⁢π=2⁢k−1⁢π
1461 1460 oveq2d ⊢n=2⁢k−1→4n⁢π=42⁢k−1⁢π
1462 oveq1 ⊢n=2⁢k−1→n⁢X=2⁢k−1⁢X
1463 1462 fveq2d ⊢n=2⁢k−1→sin⁡n⁢X=sin⁡2⁢k−1⁢X
1464 1461 1463 oveq12d ⊢n=2⁢k−1→4n⁢π⁢sin⁡n⁢X=42⁢k−1⁢π⁢sin⁡2⁢k−1⁢X
1465 1459 1464 ifbieq2d ⊢n=2⁢k−1→if2∥n04n⁢π⁢sin⁡n⁢X=if2∥2⁢k−1042⁢k−1⁢π⁢sin⁡2⁢k−1⁢X
1466 1465 adantl ⊢k∈ℕ∧n=2⁢k−1→if2∥n04n⁢π⁢sin⁡n⁢X=if2∥2⁢k−1042⁢k−1⁢π⁢sin⁡2⁢k−1⁢X
1467 elnnz ⊢2⁢k−1∈ℕ↔2⁢k−1∈ℤ∧0<2⁢k−1
1468 25 52 1467 sylanbrc ⊢k∈ℕ→2⁢k−1∈ℕ
1469 ovex ⊢42⁢k−1⁢π⁢sin⁡2⁢k−1⁢X∈V
1470 93 1469 ifex ⊢if2∥2⁢k−1042⁢k−1⁢π⁢sin⁡2⁢k−1⁢X∈V
1471 1470 a1i ⊢k∈ℕ→if2∥2⁢k−1042⁢k−1⁢π⁢sin⁡2⁢k−1⁢X∈V
1472 84 1466 1468 1471 fvmptd ⊢k∈ℕ→n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X⁡2⁢k−1=if2∥2⁢k−1042⁢k−1⁢π⁢sin⁡2⁢k−1⁢X
1473 dvdsmul1 ⊢2∈ℤ∧k∈ℤ→2∥2⁢k
1474 20 22 1473 sylancr ⊢k∈ℕ→2∥2⁢k
1475 23 zcnd ⊢k∈ℕ→2⁢k∈ℂ
1476 1cnd ⊢k∈ℕ→1∈ℂ
1477 1475 1476 npcand ⊢k∈ℕ→2⁢k-1+1=2⁢k
1478 1477 eqcomd ⊢k∈ℕ→2⁢k=2⁢k-1+1
1479 1474 1478 breqtrd ⊢k∈ℕ→2∥2⁢k-1+1
1480 oddp1even ⊢2⁢k−1∈ℤ→¬2∥2⁢k−1↔2∥2⁢k-1+1
1481 25 1480 syl ⊢k∈ℕ→¬2∥2⁢k−1↔2∥2⁢k-1+1
1482 1479 1481 mpbird ⊢k∈ℕ→¬2∥2⁢k−1
1483 1482 iffalsed ⊢k∈ℕ→if2∥2⁢k−1042⁢k−1⁢π⁢sin⁡2⁢k−1⁢X=42⁢k−1⁢π⁢sin⁡2⁢k−1⁢X
1484 56 a1i ⊢k∈ℕ→π∈ℂ
1485 26 1484 mulcomd ⊢k∈ℕ→2⁢k−1⁢π=π⁢2⁢k−1
1486 1485 oveq2d ⊢k∈ℕ→42⁢k−1⁢π=4π⁢2⁢k−1
1487 58 a1i ⊢k∈ℕ→4∈ℂ
1488 73 a1i ⊢k∈ℕ→π≠0
1489 1487 1484 26 1488 53 divdiv1d ⊢k∈ℕ→4π2⁢k−1=4π⁢2⁢k−1
1490 1486 1489 eqtr4d ⊢k∈ℕ→42⁢k−1⁢π=4π2⁢k−1
1491 1490 oveq1d ⊢k∈ℕ→42⁢k−1⁢π⁢sin⁡2⁢k−1⁢X=4π2⁢k−1⁢sin⁡2⁢k−1⁢X
1492 1487 1484 1488 divcld ⊢k∈ℕ→4π∈ℂ
1493 1492 26 30 53 div32d ⊢k∈ℕ→4π2⁢k−1⁢sin⁡2⁢k−1⁢X=4π⁢sin⁡2⁢k−1⁢X2⁢k−1
1494 1491 1493 eqtrd ⊢k∈ℕ→42⁢k−1⁢π⁢sin⁡2⁢k−1⁢X=4π⁢sin⁡2⁢k−1⁢X2⁢k−1
1495 1472 1483 1494 3eqtrd ⊢k∈ℕ→n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X⁡2⁢k−1=4π⁢sin⁡2⁢k−1⁢X2⁢k−1
1496 1495 mpteq2ia ⊢k∈ℕ⟼n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X⁡2⁢k−1=k∈ℕ⟼4π⁢sin⁡2⁢k−1⁢X2⁢k−1
1497 oveq2 ⊢k=n→2⁢k=2⁢n
1498 1497 oveq1d ⊢k=n→2⁢k−1=2⁢n−1
1499 1498 oveq1d ⊢k=n→2⁢k−1⁢X=2⁢n−1⁢X
1500 1499 fveq2d ⊢k=n→sin⁡2⁢k−1⁢X=sin⁡2⁢n−1⁢X
1501 1500 1498 oveq12d ⊢k=n→sin⁡2⁢k−1⁢X2⁢k−1=sin⁡2⁢n−1⁢X2⁢n−1
1502 1501 oveq2d ⊢k=n→4π⁢sin⁡2⁢k−1⁢X2⁢k−1=4π⁢sin⁡2⁢n−1⁢X2⁢n−1
1503 1502 cbvmptv ⊢k∈ℕ⟼4π⁢sin⁡2⁢k−1⁢X2⁢k−1=n∈ℕ⟼4π⁢sin⁡2⁢n−1⁢X2⁢n−1
1504 1496 1503 eqtri ⊢k∈ℕ⟼n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X⁡2⁢k−1=n∈ℕ⟼4π⁢sin⁡2⁢n−1⁢X2⁢n−1
1505 seqeq3 ⊢k∈ℕ⟼n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X⁡2⁢k−1=n∈ℕ⟼4π⁢sin⁡2⁢n−1⁢X2⁢n−1→seq1+k∈ℕ⟼n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X⁡2⁢k−1=seq1+n∈ℕ⟼4π⁢sin⁡2⁢n−1⁢X2⁢n−1
1506 1504 1505 ax-mp ⊢seq1+k∈ℕ⟼n∈ℕ⟼if2∥n04n⁢π⁢sin⁡n⁢X⁡2⁢k−1=seq1+n∈ℕ⟼4π⁢sin⁡2⁢n−1⁢X2⁢n−1
1507 1 2 3 5 fourierswlem ⊢Y=ifXmodT∈0π1−1+F⁡X2
1508 1507 eqcomi ⊢ifXmodT∈0π1−1+F⁡X2=Y
1509 1458 1506 1508 3brtr3i ⊢seq1+n∈ℕ⟼4π⁢sin⁡2⁢n−1⁢X2⁢n−1⇝Y
1510 1509 a1i ⊢⊤→seq1+n∈ℕ⟼4π⁢sin⁡2⁢n−1⁢X2⁢n−1⇝Y
1511 eqid ⊢n∈ℕ⟼4π⁢sin⁡2⁢n−1⁢X2⁢n−1=n∈ℕ⟼4π⁢sin⁡2⁢n−1⁢X2⁢n−1
1512 65 69 74 divcld ⊢n∈ℕ→4π∈ℂ
1513 1441 a1i ⊢n∈ℕ→2∈ℂ
1514 1513 66 mulcld ⊢n∈ℕ→2⁢n∈ℂ
1515 id ⊢2⁢n∈ℂ→2⁢n∈ℂ
1516 1cnd ⊢2⁢n∈ℂ→1∈ℂ
1517 1515 1516 subcld ⊢2⁢n∈ℂ→2⁢n−1∈ℂ
1518 1514 1517 syl ⊢n∈ℕ→2⁢n−1∈ℂ
1519 1518 77 mulcld ⊢n∈ℕ→2⁢n−1⁢X∈ℂ
1520 1519 sincld ⊢n∈ℕ→sin⁡2⁢n−1⁢X∈ℂ
1521 32 a1i ⊢n∈ℕ→2∈ℝ
1522 nnre ⊢n∈ℕ→n∈ℝ
1523 1521 1522 remulcld ⊢n∈ℕ→2⁢n∈ℝ
1524 1523 recnd ⊢n∈ℕ→2⁢n∈ℂ
1525 1cnd ⊢n∈ℕ→1∈ℂ
1526 1524 1525 subcld ⊢n∈ℕ→2⁢n−1∈ℂ
1527 1red ⊢n∈ℕ→1∈ℝ
1528 39 1521 eqeltrid ⊢n∈ℕ→2⋅1∈ℝ
1529 1lt2 ⊢1<2
1530 1529 a1i ⊢n∈ℕ→1<2
1531 1530 39 breqtrrdi ⊢n∈ℕ→1<2⋅1
1532 47 a1i ⊢n∈ℕ→0≤2
1533 nnge1 ⊢n∈ℕ→1≤n
1534 1527 1522 1521 1532 1533 lemul2ad ⊢n∈ℕ→2⋅1≤2⁢n
1535 1527 1528 1523 1531 1534 ltletrd ⊢n∈ℕ→1<2⁢n
1536 1527 1535 gtned ⊢n∈ℕ→2⁢n≠1
1537 1524 1525 1536 subne0d ⊢n∈ℕ→2⁢n−1≠0
1538 1520 1526 1537 divcld ⊢n∈ℕ→sin⁡2⁢n−1⁢X2⁢n−1∈ℂ
1539 1512 1538 mulcld ⊢n∈ℕ→4π⁢sin⁡2⁢n−1⁢X2⁢n−1∈ℂ
1540 1511 1539 fmpti ⊢n∈ℕ⟼4π⁢sin⁡2⁢n−1⁢X2⁢n−1:ℕ⟶ℂ
1541 1540 a1i ⊢⊤→n∈ℕ⟼4π⁢sin⁡2⁢n−1⁢X2⁢n−1:ℕ⟶ℂ
1542 1541 ffvelcdmda ⊢⊤∧k∈ℕ→n∈ℕ⟼4π⁢sin⁡2⁢n−1⁢X2⁢n−1⁡k∈ℂ
1543 divcan6 ⊢π∈ℂ∧π≠0∧4∈ℂ∧4≠0→π4⁢4π=1
1544 56 73 58 60 1543 mp4an ⊢π4⁢4π=1
1545 1544 eqcomi ⊢1=π4⁢4π
1546 1545 oveq1i ⊢1⁢sin⁡2⁢k−1⁢X2⁢k−1=π4⁢4π⁢sin⁡2⁢k−1⁢X2⁢k−1
1547 54 mullidd ⊢k∈ℕ→1⁢sin⁡2⁢k−1⁢X2⁢k−1=sin⁡2⁢k−1⁢X2⁢k−1
1548 60 a1i ⊢k∈ℕ→4≠0
1549 1484 1487 1548 divcld ⊢k∈ℕ→π4∈ℂ
1550 1549 1492 54 mulassd ⊢k∈ℕ→π4⁢4π⁢sin⁡2⁢k−1⁢X2⁢k−1=π4⁢4π⁢sin⁡2⁢k−1⁢X2⁢k−1
1551 1546 1547 1550 3eqtr3a ⊢k∈ℕ→sin⁡2⁢k−1⁢X2⁢k−1=π4⁢4π⁢sin⁡2⁢k−1⁢X2⁢k−1
1552 eqidd ⊢k∈ℕ→n∈ℕ⟼4π⁢sin⁡2⁢n−1⁢X2⁢n−1=n∈ℕ⟼4π⁢sin⁡2⁢n−1⁢X2⁢n−1
1553 13 oveq2d ⊢n=k→4π⁢sin⁡2⁢n−1⁢X2⁢n−1=4π⁢sin⁡2⁢k−1⁢X2⁢k−1
1554 1553 adantl ⊢k∈ℕ∧n=k→4π⁢sin⁡2⁢n−1⁢X2⁢n−1=4π⁢sin⁡2⁢k−1⁢X2⁢k−1
1555 1494 1469 eqeltrrdi ⊢k∈ℕ→4π⁢sin⁡2⁢k−1⁢X2⁢k−1∈V
1556 1552 1554 15 1555 fvmptd ⊢k∈ℕ→n∈ℕ⟼4π⁢sin⁡2⁢n−1⁢X2⁢n−1⁡k=4π⁢sin⁡2⁢k−1⁢X2⁢k−1
1557 1556 oveq2d ⊢k∈ℕ→π4⁢n∈ℕ⟼4π⁢sin⁡2⁢n−1⁢X2⁢n−1⁡k=π4⁢4π⁢sin⁡2⁢k−1⁢X2⁢k−1
1558 1557 eqcomd ⊢k∈ℕ→π4⁢4π⁢sin⁡2⁢k−1⁢X2⁢k−1=π4⁢n∈ℕ⟼4π⁢sin⁡2⁢n−1⁢X2⁢n−1⁡k
1559 18 1551 1558 3eqtrd ⊢k∈ℕ→n∈ℕ⟼sin⁡2⁢n−1⁢X2⁢n−1⁡k=π4⁢n∈ℕ⟼4π⁢sin⁡2⁢n−1⁢X2⁢n−1⁡k
1560 1559 adantl ⊢⊤∧k∈ℕ→n∈ℕ⟼sin⁡2⁢n−1⁢X2⁢n−1⁡k=π4⁢n∈ℕ⟼4π⁢sin⁡2⁢n−1⁢X2⁢n−1⁡k
1561 6 7 62 1510 1542 1560 isermulc2 ⊢⊤→seq1+n∈ℕ⟼sin⁡2⁢n−1⁢X2⁢n−1⇝π4⁢Y
1562 climrel ⊢Rel⁡⇝
1563 1562 releldmi ⊢seq1+n∈ℕ⟼sin⁡2⁢n−1⁢X2⁢n−1⇝π4⁢Y→seq1+n∈ℕ⟼sin⁡2⁢n−1⁢X2⁢n−1∈dom⁡⇝
1564 1561 1563 syl ⊢⊤→seq1+n∈ℕ⟼sin⁡2⁢n−1⁢X2⁢n−1∈dom⁡⇝
1565 6 7 19 55 1564 isumclim2 ⊢⊤→seq1+n∈ℕ⟼sin⁡2⁢n−1⁢X2⁢n−1⇝∑k∈ℕsin⁡2⁢k−1⁢X2⁢k−1
1566 1565 mptru ⊢seq1+n∈ℕ⟼sin⁡2⁢n−1⁢X2⁢n−1⇝∑k∈ℕsin⁡2⁢k−1⁢X2⁢k−1
1567 1561 mptru ⊢seq1+n∈ℕ⟼sin⁡2⁢n−1⁢X2⁢n−1⇝π4⁢Y
1568 climuni ⊢seq1+n∈ℕ⟼sin⁡2⁢n−1⁢X2⁢n−1⇝∑k∈ℕsin⁡2⁢k−1⁢X2⁢k−1∧seq1+n∈ℕ⟼sin⁡2⁢n−1⁢X2⁢n−1⇝π4⁢Y→∑k∈ℕsin⁡2⁢k−1⁢X2⁢k−1=π4⁢Y
1569 1566 1567 1568 mp2an ⊢∑k∈ℕsin⁡2⁢k−1⁢X2⁢k−1=π4⁢Y
1570 1569 oveq2i ⊢4π⁢∑k∈ℕsin⁡2⁢k−1⁢X2⁢k−1=4π⁢π4⁢Y
1571 58 56 73 divcli ⊢4π∈ℂ
1572 56 58 60 divcli ⊢π4∈ℂ
1573 1286 1151 eqeltri ⊢F⁡X∈ℝ
1574 71 1573 ifcli ⊢ifXmodπ=00F⁡X∈ℝ
1575 5 1574 eqeltri ⊢Y∈ℝ
1576 1575 recni ⊢Y∈ℂ
1577 1571 1572 1576 mulassi ⊢4π⁢π4⁢Y=4π⁢π4⁢Y
1578 1572 1571 1544 mulcomli ⊢4π⁢π4=1
1579 1578 oveq1i ⊢4π⁢π4⁢Y=1⁢Y
1580 1576 mullidi ⊢1⁢Y=Y
1581 1579 1580 eqtri ⊢4π⁢π4⁢Y=Y
1582 1570 1577 1581 3eqtr2i ⊢4π⁢∑k∈ℕsin⁡2⁢k−1⁢X2⁢k−1=Y
1583 seqeq3 ⊢S=n∈ℕ⟼sin⁡2⁢n−1⁢X2⁢n−1→seq1+S=seq1+n∈ℕ⟼sin⁡2⁢n−1⁢X2⁢n−1
1584 4 1583 ax-mp ⊢seq1+S=seq1+n∈ℕ⟼sin⁡2⁢n−1⁢X2⁢n−1
1585 1584 1567 eqbrtri ⊢seq1+S⇝π4⁢Y
1586 1582 1585 pm3.2i ⊢4π⁢∑k∈ℕsin⁡2⁢k−1⁢X2⁢k−1=Y∧seq1+S⇝π4⁢Y