Metamath Proof Explorer

Theorem fourierdlem104

Description: The half upper part of the integral equal to the fourier partial sum, converges to half the right limit of the original function. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem104.f ⊢φ→F:ℝ⟶ℝ
fourierdlem104.xre ⊢φ→X∈ℝ
fourierdlem104.p ⊢P=m∈ℕ⟼p∈ℝ0…m|p⁡0=-π+X∧p⁡m=π+X∧∀i∈0..^mp⁡i<p⁡i+1
fourierdlem104.m ⊢φ→M∈ℕ
fourierdlem104.v ⊢φ→V∈P⁡M
fourierdlem104.x ⊢φ→X∈ran⁡V
fourierdlem104.fcn ⊢φ∧i∈0..^M→F↾V⁡iV⁡i+1:V⁡iV⁡i+1⟶cnℂ
fourierdlem104.fbdioo ⊢φ∧i∈0..^M→∃w∈ℝ∀t∈V⁡iV⁡i+1F⁡t≤w
fourierdlem104.fdvcn ⊢φ∧i∈0..^M→Fℝ′↾V⁡iV⁡i+1:V⁡iV⁡i+1⟶cnℝ
fourierdlem104.fdvbd ⊢φ∧i∈0..^M→∃z∈ℝ∀t∈V⁡iV⁡i+1Fℝ′⁡t≤z
fourierdlem104.r ⊢φ∧i∈0..^M→R∈F↾V⁡iV⁡i+1limℂV⁡i
fourierdlem104.l ⊢φ∧i∈0..^M→L∈F↾V⁡iV⁡i+1limℂV⁡i+1
fourierdlem104.h ⊢H=s∈−ππ⟼ifs=00F⁡X+s−if0<sYWs
fourierdlem104.k ⊢K=s∈−ππ⟼ifs=01s2⁢sin⁡s2
fourierdlem104.u ⊢U=s∈−ππ⟼H⁡s⁢K⁡s
fourierdlem104.s ⊢S=s∈−ππ⟼sin⁡n+12⁢s
fourierdlem104.g ⊢G=s∈−ππ⟼U⁡s⁢S⁡s
fourierdlem104.z ⊢Z=m∈ℕ⟼∫0πF⁡X+s⁢D⁡m⁡sds
fourierdlem104.e ⊢E=n∈ℕ⟼∫0πG⁡sdsπ
fourierdlem104.y ⊢φ→Y∈F↾X+∞limℂX
fourierdlem104.w ⊢φ→W∈F↾−∞XlimℂX
fourierdlem104.a ⊢φ→A∈Fℝ′↾−∞XlimℂX
fourierdlem104.b ⊢φ→B∈Fℝ′↾X+∞limℂX
fourierdlem104.d ⊢D=n∈ℕ⟼s∈ℝ⟼ifsmod2⁢π=02⁢n+12⁢πsin⁡n+12⁢s2⁢π⁢sin⁡s2
fourierdlem104.o ⊢O=U↾dπ
fourierdlem104.t ⊢T=dπ∪ran⁡Q∩dπ
fourierdlem104.n ⊢N=T−1
fourierdlem104.j ⊢J=ιf|fIsom<,<0…NT
fourierdlem104.q ⊢Q=i∈0…M⟼V⁡i−X
fourierdlem104.1 ⊢C=ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1
fourierdlem104.ch ⊢χ↔φ∧e∈ℝ+∧d∈0π∧k∈ℕ∧∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧∫dπU⁡s⁢sin⁡k+12⁢sds<e2
Assertion fourierdlem104 ⊢φ→Z⇝Y2

Proof

Step Hyp Ref Expression
1 fourierdlem104.f ⊢φ→F:ℝ⟶ℝ
2 fourierdlem104.xre ⊢φ→X∈ℝ
3 fourierdlem104.p ⊢P=m∈ℕ⟼p∈ℝ0…m|p⁡0=-π+X∧p⁡m=π+X∧∀i∈0..^mp⁡i<p⁡i+1
4 fourierdlem104.m ⊢φ→M∈ℕ
5 fourierdlem104.v ⊢φ→V∈P⁡M
6 fourierdlem104.x ⊢φ→X∈ran⁡V
7 fourierdlem104.fcn ⊢φ∧i∈0..^M→F↾V⁡iV⁡i+1:V⁡iV⁡i+1⟶cnℂ
8 fourierdlem104.fbdioo ⊢φ∧i∈0..^M→∃w∈ℝ∀t∈V⁡iV⁡i+1F⁡t≤w
9 fourierdlem104.fdvcn ⊢φ∧i∈0..^M→Fℝ′↾V⁡iV⁡i+1:V⁡iV⁡i+1⟶cnℝ
10 fourierdlem104.fdvbd ⊢φ∧i∈0..^M→∃z∈ℝ∀t∈V⁡iV⁡i+1Fℝ′⁡t≤z
11 fourierdlem104.r ⊢φ∧i∈0..^M→R∈F↾V⁡iV⁡i+1limℂV⁡i
12 fourierdlem104.l ⊢φ∧i∈0..^M→L∈F↾V⁡iV⁡i+1limℂV⁡i+1
13 fourierdlem104.h ⊢H=s∈−ππ⟼ifs=00F⁡X+s−if0<sYWs
14 fourierdlem104.k ⊢K=s∈−ππ⟼ifs=01s2⁢sin⁡s2
15 fourierdlem104.u ⊢U=s∈−ππ⟼H⁡s⁢K⁡s
16 fourierdlem104.s ⊢S=s∈−ππ⟼sin⁡n+12⁢s
17 fourierdlem104.g ⊢G=s∈−ππ⟼U⁡s⁢S⁡s
18 fourierdlem104.z ⊢Z=m∈ℕ⟼∫0πF⁡X+s⁢D⁡m⁡sds
19 fourierdlem104.e ⊢E=n∈ℕ⟼∫0πG⁡sdsπ
20 fourierdlem104.y ⊢φ→Y∈F↾X+∞limℂX
21 fourierdlem104.w ⊢φ→W∈F↾−∞XlimℂX
22 fourierdlem104.a ⊢φ→A∈Fℝ′↾−∞XlimℂX
23 fourierdlem104.b ⊢φ→B∈Fℝ′↾X+∞limℂX
24 fourierdlem104.d ⊢D=n∈ℕ⟼s∈ℝ⟼ifsmod2⁢π=02⁢n+12⁢πsin⁡n+12⁢s2⁢π⁢sin⁡s2
25 fourierdlem104.o ⊢O=U↾dπ
26 fourierdlem104.t ⊢T=dπ∪ran⁡Q∩dπ
27 fourierdlem104.n ⊢N=T−1
28 fourierdlem104.j ⊢J=ιf|fIsom<,<0…NT
29 fourierdlem104.q ⊢Q=i∈0…M⟼V⁡i−X
30 fourierdlem104.1 ⊢C=ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1
31 fourierdlem104.ch ⊢χ↔φ∧e∈ℝ+∧d∈0π∧k∈ℕ∧∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧∫dπU⁡s⁢sin⁡k+12⁢sds<e2
32 eqid ⊢ℤ≥1=ℤ≥1
33 1zzd ⊢φ→1∈ℤ
34 nfv ⊢Ⅎnφ
35 nfmpt1 ⊢Ⅎ_nn∈ℕ⟼∫0πG⁡sds
36 nfmpt1 ⊢Ⅎ_nn∈ℕ⟼π
37 nfmpt1 ⊢Ⅎ_nn∈ℕ⟼∫0πG⁡sdsπ
38 19 37 nfcxfr ⊢Ⅎ_nE
39 nnuz ⊢ℕ=ℤ≥1
40 elioore ⊢d∈0π→d∈ℝ
41 40 adantl ⊢φ∧d∈0π→d∈ℝ
42 pire ⊢π∈ℝ
43 42 a1i ⊢φ∧d∈0π→π∈ℝ
44 ioossre ⊢X+∞⊆ℝ
45 44 a1i ⊢φ→X+∞⊆ℝ
46 1 45 fssresd ⊢φ→F↾X+∞:X+∞⟶ℝ
47 ioosscn ⊢X+∞⊆ℂ
48 47 a1i ⊢φ→X+∞⊆ℂ
49 eqid ⊢TopOpen⁡ℂfld=TopOpen⁡ℂfld
50 pnfxr ⊢+∞∈ℝ*
51 50 a1i ⊢φ→+∞∈ℝ*
52 2 ltpnfd ⊢φ→X<+∞
53 49 51 2 52 lptioo1cn ⊢φ→X∈limPt⁡TopOpen⁡ℂfld⁡X+∞
54 46 48 53 20 limcrecl ⊢φ→Y∈ℝ
55 ioossre ⊢−∞X⊆ℝ
56 55 a1i ⊢φ→−∞X⊆ℝ
57 1 56 fssresd ⊢φ→F↾−∞X:−∞X⟶ℝ
58 ioosscn ⊢−∞X⊆ℂ
59 58 a1i ⊢φ→−∞X⊆ℂ
60 mnfxr ⊢−∞∈ℝ*
61 60 a1i ⊢φ→−∞∈ℝ*
62 2 mnfltd ⊢φ→−∞<X
63 49 61 2 62 lptioo2cn ⊢φ→X∈limPt⁡TopOpen⁡ℂfld⁡−∞X
64 57 59 63 21 limcrecl ⊢φ→W∈ℝ
65 1 2 54 64 13 14 15 fourierdlem55 ⊢φ→U:−ππ⟶ℝ
66 ax-resscn ⊢ℝ⊆ℂ
67 66 a1i ⊢φ→ℝ⊆ℂ
68 65 67 fssd ⊢φ→U:−ππ⟶ℂ
69 68 adantr ⊢φ∧d∈0π→U:−ππ⟶ℂ
70 42 renegcli ⊢−π∈ℝ
71 70 a1i ⊢φ∧d∈0π→−π∈ℝ
72 70 a1i ⊢d∈0π→−π∈ℝ
73 0red ⊢d∈0π→0∈ℝ
74 negpilt0 ⊢−π<0
75 74 a1i ⊢d∈0π→−π<0
76 0xr ⊢0∈ℝ*
77 42 rexri ⊢π∈ℝ*
78 ioogtlb ⊢0∈ℝ*∧π∈ℝ*∧d∈0π→0<d
79 76 77 78 mp3an12 ⊢d∈0π→0<d
80 72 73 40 75 79 lttrd ⊢d∈0π→−π<d
81 72 40 80 ltled ⊢d∈0π→−π≤d
82 81 adantl ⊢φ∧d∈0π→−π≤d
83 43 leidd ⊢φ∧d∈0π→π≤π
84 iccss ⊢−π∈ℝ∧π∈ℝ∧−π≤d∧π≤π→dπ⊆−ππ
85 71 43 82 83 84 syl22anc ⊢φ∧d∈0π→dπ⊆−ππ
86 69 85 fssresd ⊢φ∧d∈0π→U↾dπ:dπ⟶ℂ
87 25 a1i ⊢φ∧d∈0π→O=U↾dπ
88 87 feq1d ⊢φ∧d∈0π→O:dπ⟶ℂ↔U↾dπ:dπ⟶ℂ
89 86 88 mpbird ⊢φ∧d∈0π→O:dπ⟶ℂ
90 42 elexi ⊢π∈V
91 90 prid2 ⊢π∈dπ
92 elun1 ⊢π∈dπ→π∈dπ∪ran⁡Q∩dπ
93 91 92 ax-mp ⊢π∈dπ∪ran⁡Q∩dπ
94 93 26 eleqtrri ⊢π∈T
95 94 ne0ii ⊢T≠∅
96 95 a1i ⊢φ→T≠∅
97 prfi ⊢dπ∈Fin
98 97 a1i ⊢φ→dπ∈Fin
99 fzfi ⊢0…M∈Fin
100 29 rnmptfi ⊢0…M∈Fin→ran⁡Q∈Fin
101 99 100 ax-mp ⊢ran⁡Q∈Fin
102 infi ⊢ran⁡Q∈Fin→ran⁡Q∩dπ∈Fin
103 101 102 mp1i ⊢φ→ran⁡Q∩dπ∈Fin
104 unfi ⊢dπ∈Fin∧ran⁡Q∩dπ∈Fin→dπ∪ran⁡Q∩dπ∈Fin
105 98 103 104 syl2anc ⊢φ→dπ∪ran⁡Q∩dπ∈Fin
106 26 105 eqeltrid ⊢φ→T∈Fin
107 hashnncl ⊢T∈Fin→T∈ℕ↔T≠∅
108 106 107 syl ⊢φ→T∈ℕ↔T≠∅
109 96 108 mpbird ⊢φ→T∈ℕ
110 nnm1nn0 ⊢T∈ℕ→T−1∈ℕ0
111 109 110 syl ⊢φ→T−1∈ℕ0
112 27 111 eqeltrid ⊢φ→N∈ℕ0
113 112 adantr ⊢φ∧d∈0π→N∈ℕ0
114 0red ⊢φ∧d∈0π→0∈ℝ
115 1red ⊢φ∧d∈0π→1∈ℝ
116 113 nn0red ⊢φ∧d∈0π→N∈ℝ
117 0lt1 ⊢0<1
118 117 a1i ⊢φ∧d∈0π→0<1
119 2re ⊢2∈ℝ
120 119 a1i ⊢φ∧d∈0π→2∈ℝ
121 109 nnred ⊢φ→T∈ℝ
122 121 adantr ⊢φ∧d∈0π→T∈ℝ
123 iooltub ⊢0∈ℝ*∧π∈ℝ*∧d∈0π→d<π
124 76 77 123 mp3an12 ⊢d∈0π→d<π
125 40 124 ltned ⊢d∈0π→d≠π
126 125 adantl ⊢φ∧d∈0π→d≠π
127 hashprg ⊢d∈ℝ∧π∈ℝ→d≠π↔dπ=2
128 41 42 127 sylancl ⊢φ∧d∈0π→d≠π↔dπ=2
129 126 128 mpbid ⊢φ∧d∈0π→dπ=2
130 129 eqcomd ⊢φ∧d∈0π→2=dπ
131 106 adantr ⊢φ∧d∈0π→T∈Fin
132 ssun1 ⊢dπ⊆dπ∪ran⁡Q∩dπ
133 132 26 sseqtrri ⊢dπ⊆T
134 hashssle ⊢T∈Fin∧dπ⊆T→dπ≤T
135 131 133 134 sylancl ⊢φ∧d∈0π→dπ≤T
136 130 135 eqbrtrd ⊢φ∧d∈0π→2≤T
137 120 122 115 136 lesub1dd ⊢φ∧d∈0π→2−1≤T−1
138 1e2m1 ⊢1=2−1
139 137 138 27 3brtr4g ⊢φ∧d∈0π→1≤N
140 114 115 116 118 139 ltletrd ⊢φ∧d∈0π→0<N
141 140 gt0ne0d ⊢φ∧d∈0π→N≠0
142 elnnne0 ⊢N∈ℕ↔N∈ℕ0∧N≠0
143 113 141 142 sylanbrc ⊢φ∧d∈0π→N∈ℕ
144 41 leidd ⊢φ∧d∈0π→d≤d
145 42 a1i ⊢d∈0π→π∈ℝ
146 40 145 124 ltled ⊢d∈0π→d≤π
147 146 adantl ⊢φ∧d∈0π→d≤π
148 41 43 41 144 147 eliccd ⊢φ∧d∈0π→d∈dπ
149 41 43 43 147 83 eliccd ⊢φ∧d∈0π→π∈dπ
150 148 149 jca ⊢φ∧d∈0π→d∈dπ∧π∈dπ
151 vex ⊢d∈V
152 151 90 prss ⊢d∈dπ∧π∈dπ↔dπ⊆dπ
153 150 152 sylib ⊢φ∧d∈0π→dπ⊆dπ
154 inss2 ⊢ran⁡Q∩dπ⊆dπ
155 154 a1i ⊢φ∧d∈0π→ran⁡Q∩dπ⊆dπ
156 ioossicc ⊢dπ⊆dπ
157 155 156 sstrdi ⊢φ∧d∈0π→ran⁡Q∩dπ⊆dπ
158 153 157 unssd ⊢φ∧d∈0π→dπ∪ran⁡Q∩dπ⊆dπ
159 26 158 eqsstrid ⊢φ∧d∈0π→T⊆dπ
160 151 prid1 ⊢d∈dπ
161 elun1 ⊢d∈dπ→d∈dπ∪ran⁡Q∩dπ
162 160 161 ax-mp ⊢d∈dπ∪ran⁡Q∩dπ
163 162 26 eleqtrri ⊢d∈T
164 163 a1i ⊢φ∧d∈0π→d∈T
165 94 a1i ⊢φ∧d∈0π→π∈T
166 131 27 28 41 43 159 164 165 fourierdlem52 ⊢φ∧d∈0π→J:0…N⟶dπ∧J⁡0=d∧J⁡N=π
167 166 simplld ⊢φ∧d∈0π→J:0…N⟶dπ
168 166 simplrd ⊢φ∧d∈0π→J⁡0=d
169 166 simprd ⊢φ∧d∈0π→J⁡N=π
170 elfzoelz ⊢k∈0..^N→k∈ℤ
171 170 zred ⊢k∈0..^N→k∈ℝ
172 171 adantl ⊢φ∧d∈0π∧k∈0..^N→k∈ℝ
173 172 ltp1d ⊢φ∧d∈0π∧k∈0..^N→k<k+1
174 40 145 jca ⊢d∈0π→d∈ℝ∧π∈ℝ
175 151 90 prss ⊢d∈ℝ∧π∈ℝ↔dπ⊆ℝ
176 174 175 sylib ⊢d∈0π→dπ⊆ℝ
177 176 adantl ⊢φ∧d∈0π→dπ⊆ℝ
178 ioossre ⊢dπ⊆ℝ
179 154 178 sstri ⊢ran⁡Q∩dπ⊆ℝ
180 179 a1i ⊢φ∧d∈0π→ran⁡Q∩dπ⊆ℝ
181 177 180 unssd ⊢φ∧d∈0π→dπ∪ran⁡Q∩dπ⊆ℝ
182 26 181 eqsstrid ⊢φ∧d∈0π→T⊆ℝ
183 131 182 28 27 fourierdlem36 ⊢φ∧d∈0π→JIsom<,<0…NT
184 183 adantr ⊢φ∧d∈0π∧k∈0..^N→JIsom<,<0…NT
185 elfzofz ⊢k∈0..^N→k∈0…N
186 185 adantl ⊢φ∧d∈0π∧k∈0..^N→k∈0…N
187 fzofzp1 ⊢k∈0..^N→k+1∈0…N
188 187 adantl ⊢φ∧d∈0π∧k∈0..^N→k+1∈0…N
189 isorel ⊢JIsom<,<0…NT∧k∈0…N∧k+1∈0…N→k<k+1↔J⁡k<J⁡k+1
190 184 186 188 189 syl12anc ⊢φ∧d∈0π∧k∈0..^N→k<k+1↔J⁡k<J⁡k+1
191 173 190 mpbid ⊢φ∧d∈0π∧k∈0..^N→J⁡k<J⁡k+1
192 65 adantr ⊢φ∧d∈0π→U:−ππ⟶ℝ
193 192 85 feqresmpt ⊢φ∧d∈0π→U↾dπ=s∈dπ⟼U⁡s
194 85 sselda ⊢φ∧d∈0π∧s∈dπ→s∈−ππ
195 1 2 54 64 13 fourierdlem9 ⊢φ→H:−ππ⟶ℝ
196 195 ad2antrr ⊢φ∧d∈0π∧s∈dπ→H:−ππ⟶ℝ
197 196 194 ffvelcdmd ⊢φ∧d∈0π∧s∈dπ→H⁡s∈ℝ
198 14 fourierdlem43 ⊢K:−ππ⟶ℝ
199 198 a1i ⊢φ∧d∈0π∧s∈dπ→K:−ππ⟶ℝ
200 199 194 ffvelcdmd ⊢φ∧d∈0π∧s∈dπ→K⁡s∈ℝ
201 197 200 remulcld ⊢φ∧d∈0π∧s∈dπ→H⁡s⁢K⁡s∈ℝ
202 15 fvmpt2 ⊢s∈−ππ∧H⁡s⁢K⁡s∈ℝ→U⁡s=H⁡s⁢K⁡s
203 194 201 202 syl2anc ⊢φ∧d∈0π∧s∈dπ→U⁡s=H⁡s⁢K⁡s
204 0red ⊢d∈0π∧s∈dπ→0∈ℝ
205 40 adantr ⊢d∈0π∧s∈dπ→d∈ℝ
206 42 a1i ⊢d∈0π∧s∈dπ→π∈ℝ
207 simpr ⊢d∈0π∧s∈dπ→s∈dπ
208 eliccre ⊢d∈ℝ∧π∈ℝ∧s∈dπ→s∈ℝ
209 205 206 207 208 syl3anc ⊢d∈0π∧s∈dπ→s∈ℝ
210 79 adantr ⊢d∈0π∧s∈dπ→0<d
211 205 rexrd ⊢d∈0π∧s∈dπ→d∈ℝ*
212 77 a1i ⊢d∈0π∧s∈dπ→π∈ℝ*
213 iccgelb ⊢d∈ℝ*∧π∈ℝ*∧s∈dπ→d≤s
214 211 212 207 213 syl3anc ⊢d∈0π∧s∈dπ→d≤s
215 204 205 209 210 214 ltletrd ⊢d∈0π∧s∈dπ→0<s
216 215 gt0ne0d ⊢d∈0π∧s∈dπ→s≠0
217 216 adantll ⊢φ∧d∈0π∧s∈dπ→s≠0
218 217 neneqd ⊢φ∧d∈0π∧s∈dπ→¬s=0
219 218 iffalsed ⊢φ∧d∈0π∧s∈dπ→ifs=00F⁡X+s−if0<sYWs=F⁡X+s−if0<sYWs
220 215 adantll ⊢φ∧d∈0π∧s∈dπ→0<s
221 220 iftrued ⊢φ∧d∈0π∧s∈dπ→if0<sYW=Y
222 221 oveq2d ⊢φ∧d∈0π∧s∈dπ→F⁡X+s−if0<sYW=F⁡X+s−Y
223 222 oveq1d ⊢φ∧d∈0π∧s∈dπ→F⁡X+s−if0<sYWs=F⁡X+s−Ys
224 219 223 eqtrd ⊢φ∧d∈0π∧s∈dπ→ifs=00F⁡X+s−if0<sYWs=F⁡X+s−Ys
225 1 ad2antrr ⊢φ∧d∈0π∧s∈dπ→F:ℝ⟶ℝ
226 2 ad2antrr ⊢φ∧d∈0π∧s∈dπ→X∈ℝ
227 iccssre ⊢−π∈ℝ∧π∈ℝ→−ππ⊆ℝ
228 70 42 227 mp2an ⊢−ππ⊆ℝ
229 228 194 sselid ⊢φ∧d∈0π∧s∈dπ→s∈ℝ
230 226 229 readdcld ⊢φ∧d∈0π∧s∈dπ→X+s∈ℝ
231 225 230 ffvelcdmd ⊢φ∧d∈0π∧s∈dπ→F⁡X+s∈ℝ
232 54 ad2antrr ⊢φ∧d∈0π∧s∈dπ→Y∈ℝ
233 231 232 resubcld ⊢φ∧d∈0π∧s∈dπ→F⁡X+s−Y∈ℝ
234 233 229 217 redivcld ⊢φ∧d∈0π∧s∈dπ→F⁡X+s−Ys∈ℝ
235 224 234 eqeltrd ⊢φ∧d∈0π∧s∈dπ→ifs=00F⁡X+s−if0<sYWs∈ℝ
236 13 fvmpt2 ⊢s∈−ππ∧ifs=00F⁡X+s−if0<sYWs∈ℝ→H⁡s=ifs=00F⁡X+s−if0<sYWs
237 194 235 236 syl2anc ⊢φ∧d∈0π∧s∈dπ→H⁡s=ifs=00F⁡X+s−if0<sYWs
238 237 219 223 3eqtrd ⊢φ∧d∈0π∧s∈dπ→H⁡s=F⁡X+s−Ys
239 206 renegcld ⊢d∈0π∧s∈dπ→−π∈ℝ
240 74 a1i ⊢d∈0π∧s∈dπ→−π<0
241 239 204 209 240 215 lttrd ⊢d∈0π∧s∈dπ→−π<s
242 239 209 241 ltled ⊢d∈0π∧s∈dπ→−π≤s
243 iccleub ⊢d∈ℝ*∧π∈ℝ*∧s∈dπ→s≤π
244 211 212 207 243 syl3anc ⊢d∈0π∧s∈dπ→s≤π
245 239 206 209 242 244 eliccd ⊢d∈0π∧s∈dπ→s∈−ππ
246 216 neneqd ⊢d∈0π∧s∈dπ→¬s=0
247 246 iffalsed ⊢d∈0π∧s∈dπ→ifs=01s2⁢sin⁡s2=s2⁢sin⁡s2
248 119 a1i ⊢d∈0π∧s∈dπ→2∈ℝ
249 209 rehalfcld ⊢d∈0π∧s∈dπ→s2∈ℝ
250 249 resincld ⊢d∈0π∧s∈dπ→sin⁡s2∈ℝ
251 248 250 remulcld ⊢d∈0π∧s∈dπ→2⁢sin⁡s2∈ℝ
252 2cnd ⊢d∈0π∧s∈dπ→2∈ℂ
253 209 recnd ⊢d∈0π∧s∈dπ→s∈ℂ
254 253 halfcld ⊢d∈0π∧s∈dπ→s2∈ℂ
255 254 sincld ⊢d∈0π∧s∈dπ→sin⁡s2∈ℂ
256 2ne0 ⊢2≠0
257 256 a1i ⊢d∈0π∧s∈dπ→2≠0
258 fourierdlem44 ⊢s∈−ππ∧s≠0→sin⁡s2≠0
259 245 216 258 syl2anc ⊢d∈0π∧s∈dπ→sin⁡s2≠0
260 252 255 257 259 mulne0d ⊢d∈0π∧s∈dπ→2⁢sin⁡s2≠0
261 209 251 260 redivcld ⊢d∈0π∧s∈dπ→s2⁢sin⁡s2∈ℝ
262 247 261 eqeltrd ⊢d∈0π∧s∈dπ→ifs=01s2⁢sin⁡s2∈ℝ
263 14 fvmpt2 ⊢s∈−ππ∧ifs=01s2⁢sin⁡s2∈ℝ→K⁡s=ifs=01s2⁢sin⁡s2
264 245 262 263 syl2anc ⊢d∈0π∧s∈dπ→K⁡s=ifs=01s2⁢sin⁡s2
265 264 adantll ⊢φ∧d∈0π∧s∈dπ→K⁡s=ifs=01s2⁢sin⁡s2
266 238 265 oveq12d ⊢φ∧d∈0π∧s∈dπ→H⁡s⁢K⁡s=F⁡X+s−Ys⁢ifs=01s2⁢sin⁡s2
267 218 iffalsed ⊢φ∧d∈0π∧s∈dπ→ifs=01s2⁢sin⁡s2=s2⁢sin⁡s2
268 267 oveq2d ⊢φ∧d∈0π∧s∈dπ→F⁡X+s−Ys⁢ifs=01s2⁢sin⁡s2=F⁡X+s−Ys⁢s2⁢sin⁡s2
269 203 266 268 3eqtrd ⊢φ∧d∈0π∧s∈dπ→U⁡s=F⁡X+s−Ys⁢s2⁢sin⁡s2
270 269 mpteq2dva ⊢φ∧d∈0π→s∈dπ⟼U⁡s=s∈dπ⟼F⁡X+s−Ys⁢s2⁢sin⁡s2
271 87 193 270 3eqtrd ⊢φ∧d∈0π→O=s∈dπ⟼F⁡X+s−Ys⁢s2⁢sin⁡s2
272 271 adantr ⊢φ∧d∈0π∧k∈0..^N→O=s∈dπ⟼F⁡X+s−Ys⁢s2⁢sin⁡s2
273 272 reseq1d ⊢φ∧d∈0π∧k∈0..^N→O↾J⁡kJ⁡k+1=s∈dπ⟼F⁡X+s−Ys⁢s2⁢sin⁡s2↾J⁡kJ⁡k+1
274 1 adantr ⊢φ∧d∈0π→F:ℝ⟶ℝ
275 2 adantr ⊢φ∧d∈0π→X∈ℝ
276 4 adantr ⊢φ∧d∈0π→M∈ℕ
277 5 adantr ⊢φ∧d∈0π→V∈P⁡M
278 7 adantlr ⊢φ∧d∈0π∧i∈0..^M→F↾V⁡iV⁡i+1:V⁡iV⁡i+1⟶cnℂ
279 11 adantlr ⊢φ∧d∈0π∧i∈0..^M→R∈F↾V⁡iV⁡i+1limℂV⁡i
280 12 adantlr ⊢φ∧d∈0π∧i∈0..^M→L∈F↾V⁡iV⁡i+1limℂV⁡i+1
281 124 adantl ⊢φ∧d∈0π→d<π
282 73 40 ltnled ⊢d∈0π→0<d↔¬d≤0
283 79 282 mpbid ⊢d∈0π→¬d≤0
284 283 intn3an2d ⊢d∈0π→¬0∈ℝ∧d≤0∧0≤π
285 elicc2 ⊢d∈ℝ∧π∈ℝ→0∈dπ↔0∈ℝ∧d≤0∧0≤π
286 40 42 285 sylancl ⊢d∈0π→0∈dπ↔0∈ℝ∧d≤0∧0≤π
287 284 286 mtbird ⊢d∈0π→¬0∈dπ
288 287 adantl ⊢φ∧d∈0π→¬0∈dπ
289 54 adantr ⊢φ∧d∈0π→Y∈ℝ
290 eqid ⊢s∈dπ⟼F⁡X+s−Ys⁢s2⁢sin⁡s2=s∈dπ⟼F⁡X+s−Ys⁢s2⁢sin⁡s2
291 eqid ⊢ifJ⁡k+1=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌LF⁡X+J⁡k+1−YJ⁡k+1⁢J⁡k+12⁢sin⁡J⁡k+12=ifJ⁡k+1=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌LF⁡X+J⁡k+1−YJ⁡k+1⁢J⁡k+12⁢sin⁡J⁡k+12
292 eqid ⊢ifJ⁡k=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌RF⁡X+J⁡k−YJ⁡k⁢J⁡k2⁢sin⁡J⁡k2=ifJ⁡k=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌RF⁡X+J⁡k−YJ⁡k⁢J⁡k2⁢sin⁡J⁡k2
293 fveq2 ⊢l=i→Q⁡l=Q⁡i
294 oveq1 ⊢l=i→l+1=i+1
295 294 fveq2d ⊢l=i→Q⁡l+1=Q⁡i+1
296 293 295 oveq12d ⊢l=i→Q⁡lQ⁡l+1=Q⁡iQ⁡i+1
297 296 sseq2d ⊢l=i→J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1↔J⁡kJ⁡k+1⊆Q⁡iQ⁡i+1
298 297 cbvriotavw ⊢ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1=ιi∈0..^M|J⁡kJ⁡k+1⊆Q⁡iQ⁡i+1
299 274 275 3 276 277 278 279 280 41 43 281 85 288 289 290 29 26 27 28 291 292 298 fourierdlem86 ⊢φ∧d∈0π∧k∈0..^N→ifJ⁡k+1=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌LF⁡X+J⁡k+1−YJ⁡k+1⁢J⁡k+12⁢sin⁡J⁡k+12∈s∈dπ⟼F⁡X+s−Ys⁢s2⁢sin⁡s2↾J⁡kJ⁡k+1limℂJ⁡k+1∧ifJ⁡k=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌RF⁡X+J⁡k−YJ⁡k⁢J⁡k2⁢sin⁡J⁡k2∈s∈dπ⟼F⁡X+s−Ys⁢s2⁢sin⁡s2↾J⁡kJ⁡k+1limℂJ⁡k∧s∈dπ⟼F⁡X+s−Ys⁢s2⁢sin⁡s2↾J⁡kJ⁡k+1:J⁡kJ⁡k+1⟶cnℂ
300 299 simprd ⊢φ∧d∈0π∧k∈0..^N→s∈dπ⟼F⁡X+s−Ys⁢s2⁢sin⁡s2↾J⁡kJ⁡k+1:J⁡kJ⁡k+1⟶cnℂ
301 273 300 eqeltrd ⊢φ∧d∈0π∧k∈0..^N→O↾J⁡kJ⁡k+1:J⁡kJ⁡k+1⟶cnℂ
302 299 simplld ⊢φ∧d∈0π∧k∈0..^N→ifJ⁡k+1=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌LF⁡X+J⁡k+1−YJ⁡k+1⁢J⁡k+12⁢sin⁡J⁡k+12∈s∈dπ⟼F⁡X+s−Ys⁢s2⁢sin⁡s2↾J⁡kJ⁡k+1limℂJ⁡k+1
303 272 eqcomd ⊢φ∧d∈0π∧k∈0..^N→s∈dπ⟼F⁡X+s−Ys⁢s2⁢sin⁡s2=O
304 303 reseq1d ⊢φ∧d∈0π∧k∈0..^N→s∈dπ⟼F⁡X+s−Ys⁢s2⁢sin⁡s2↾J⁡kJ⁡k+1=O↾J⁡kJ⁡k+1
305 304 oveq1d ⊢φ∧d∈0π∧k∈0..^N→s∈dπ⟼F⁡X+s−Ys⁢s2⁢sin⁡s2↾J⁡kJ⁡k+1limℂJ⁡k+1=O↾J⁡kJ⁡k+1limℂJ⁡k+1
306 302 305 eleqtrd ⊢φ∧d∈0π∧k∈0..^N→ifJ⁡k+1=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌LF⁡X+J⁡k+1−YJ⁡k+1⁢J⁡k+12⁢sin⁡J⁡k+12∈O↾J⁡kJ⁡k+1limℂJ⁡k+1
307 299 simplrd ⊢φ∧d∈0π∧k∈0..^N→ifJ⁡k=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌RF⁡X+J⁡k−YJ⁡k⁢J⁡k2⁢sin⁡J⁡k2∈s∈dπ⟼F⁡X+s−Ys⁢s2⁢sin⁡s2↾J⁡kJ⁡k+1limℂJ⁡k
308 304 oveq1d ⊢φ∧d∈0π∧k∈0..^N→s∈dπ⟼F⁡X+s−Ys⁢s2⁢sin⁡s2↾J⁡kJ⁡k+1limℂJ⁡k=O↾J⁡kJ⁡k+1limℂJ⁡k
309 307 308 eleqtrd ⊢φ∧d∈0π∧k∈0..^N→ifJ⁡k=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌RF⁡X+J⁡k−YJ⁡k⁢J⁡k2⁢sin⁡J⁡k2∈O↾J⁡kJ⁡k+1limℂJ⁡k
310 eqid ⊢ℝDO=ℝDO
311 89 adantr ⊢φ∧d∈0π∧k∈0..^N→O:dπ⟶ℂ
312 41 ad2antrr ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→d∈ℝ
313 42 a1i ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→π∈ℝ
314 elioore ⊢s∈J⁡kJ⁡k+1→s∈ℝ
315 314 adantl ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→s∈ℝ
316 85 228 sstrdi ⊢φ∧d∈0π→dπ⊆ℝ
317 316 adantr ⊢φ∧d∈0π∧k∈0..^N→dπ⊆ℝ
318 167 adantr ⊢φ∧d∈0π∧k∈0..^N→J:0…N⟶dπ
319 318 186 ffvelcdmd ⊢φ∧d∈0π∧k∈0..^N→J⁡k∈dπ
320 317 319 sseldd ⊢φ∧d∈0π∧k∈0..^N→J⁡k∈ℝ
321 320 adantr ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→J⁡k∈ℝ
322 41 adantr ⊢φ∧d∈0π∧k∈0..^N→d∈ℝ
323 322 rexrd ⊢φ∧d∈0π∧k∈0..^N→d∈ℝ*
324 77 a1i ⊢φ∧d∈0π∧k∈0..^N→π∈ℝ*
325 iccgelb ⊢d∈ℝ*∧π∈ℝ*∧J⁡k∈dπ→d≤J⁡k
326 323 324 319 325 syl3anc ⊢φ∧d∈0π∧k∈0..^N→d≤J⁡k
327 326 adantr ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→d≤J⁡k
328 321 rexrd ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→J⁡k∈ℝ*
329 318 188 ffvelcdmd ⊢φ∧d∈0π∧k∈0..^N→J⁡k+1∈dπ
330 317 329 sseldd ⊢φ∧d∈0π∧k∈0..^N→J⁡k+1∈ℝ
331 330 rexrd ⊢φ∧d∈0π∧k∈0..^N→J⁡k+1∈ℝ*
332 331 adantr ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→J⁡k+1∈ℝ*
333 simpr ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→s∈J⁡kJ⁡k+1
334 ioogtlb ⊢J⁡k∈ℝ*∧J⁡k+1∈ℝ*∧s∈J⁡kJ⁡k+1→J⁡k<s
335 328 332 333 334 syl3anc ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→J⁡k<s
336 312 321 315 327 335 lelttrd ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→d<s
337 312 315 336 ltled ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→d≤s
338 330 adantr ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→J⁡k+1∈ℝ
339 iooltub ⊢J⁡k∈ℝ*∧J⁡k+1∈ℝ*∧s∈J⁡kJ⁡k+1→s<J⁡k+1
340 328 332 333 339 syl3anc ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→s<J⁡k+1
341 iccleub ⊢d∈ℝ*∧π∈ℝ*∧J⁡k+1∈dπ→J⁡k+1≤π
342 323 324 329 341 syl3anc ⊢φ∧d∈0π∧k∈0..^N→J⁡k+1≤π
343 342 adantr ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→J⁡k+1≤π
344 315 338 313 340 343 ltletrd ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→s<π
345 315 313 344 ltled ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→s≤π
346 312 313 315 337 345 eliccd ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→s∈dπ
347 346 ralrimiva ⊢φ∧d∈0π∧k∈0..^N→∀s∈J⁡kJ⁡k+1s∈dπ
348 dfss3 ⊢J⁡kJ⁡k+1⊆dπ↔∀s∈J⁡kJ⁡k+1s∈dπ
349 347 348 sylibr ⊢φ∧d∈0π∧k∈0..^N→J⁡kJ⁡k+1⊆dπ
350 311 349 feqresmpt ⊢φ∧d∈0π∧k∈0..^N→O↾J⁡kJ⁡k+1=s∈J⁡kJ⁡k+1⟼O⁡s
351 simplll ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→φ
352 simpllr ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→d∈0π
353 25 fveq1i ⊢O⁡s=U↾dπ⁡s
354 353 a1i ⊢φ∧d∈0π∧s∈dπ→O⁡s=U↾dπ⁡s
355 fvres ⊢s∈dπ→U↾dπ⁡s=U⁡s
356 355 adantl ⊢φ∧d∈0π∧s∈dπ→U↾dπ⁡s=U⁡s
357 265 267 eqtrd ⊢φ∧d∈0π∧s∈dπ→K⁡s=s2⁢sin⁡s2
358 238 357 oveq12d ⊢φ∧d∈0π∧s∈dπ→H⁡s⁢K⁡s=F⁡X+s−Ys⁢s2⁢sin⁡s2
359 233 recnd ⊢φ∧d∈0π∧s∈dπ→F⁡X+s−Y∈ℂ
360 253 adantll ⊢φ∧d∈0π∧s∈dπ→s∈ℂ
361 2cnd ⊢φ∧d∈0π∧s∈dπ→2∈ℂ
362 360 halfcld ⊢φ∧d∈0π∧s∈dπ→s2∈ℂ
363 362 sincld ⊢φ∧d∈0π∧s∈dπ→sin⁡s2∈ℂ
364 361 363 mulcld ⊢φ∧d∈0π∧s∈dπ→2⁢sin⁡s2∈ℂ
365 260 adantll ⊢φ∧d∈0π∧s∈dπ→2⁢sin⁡s2≠0
366 359 360 364 217 365 dmdcan2d ⊢φ∧d∈0π∧s∈dπ→F⁡X+s−Ys⁢s2⁢sin⁡s2=F⁡X+s−Y2⁢sin⁡s2
367 203 358 366 3eqtrd ⊢φ∧d∈0π∧s∈dπ→U⁡s=F⁡X+s−Y2⁢sin⁡s2
368 354 356 367 3eqtrd ⊢φ∧d∈0π∧s∈dπ→O⁡s=F⁡X+s−Y2⁢sin⁡s2
369 351 352 346 368 syl21anc ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→O⁡s=F⁡X+s−Y2⁢sin⁡s2
370 351 352 346 366 syl21anc ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→F⁡X+s−Ys⁢s2⁢sin⁡s2=F⁡X+s−Y2⁢sin⁡s2
371 370 eqcomd ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→F⁡X+s−Y2⁢sin⁡s2=F⁡X+s−Ys⁢s2⁢sin⁡s2
372 eqidd ⊢φ∧k∈0..^N∧s∈J⁡kJ⁡k+1→t∈J⁡kJ⁡k+1⟼F⁡X+t−Yt=t∈J⁡kJ⁡k+1⟼F⁡X+t−Yt
373 oveq2 ⊢t=s→X+t=X+s
374 373 fveq2d ⊢t=s→F⁡X+t=F⁡X+s
375 374 oveq1d ⊢t=s→F⁡X+t−Y=F⁡X+s−Y
376 id ⊢t=s→t=s
377 375 376 oveq12d ⊢t=s→F⁡X+t−Yt=F⁡X+s−Ys
378 377 adantl ⊢φ∧k∈0..^N∧s∈J⁡kJ⁡k+1∧t=s→F⁡X+t−Yt=F⁡X+s−Ys
379 simpr ⊢φ∧k∈0..^N∧s∈J⁡kJ⁡k+1→s∈J⁡kJ⁡k+1
380 ovex ⊢F⁡X+s−Ys∈V
381 380 a1i ⊢φ∧k∈0..^N∧s∈J⁡kJ⁡k+1→F⁡X+s−Ys∈V
382 372 378 379 381 fvmptd ⊢φ∧k∈0..^N∧s∈J⁡kJ⁡k+1→t∈J⁡kJ⁡k+1⟼F⁡X+t−Yt⁡s=F⁡X+s−Ys
383 eqidd ⊢φ∧k∈0..^N∧s∈J⁡kJ⁡k+1→t∈J⁡kJ⁡k+1⟼t2⁢sin⁡t2=t∈J⁡kJ⁡k+1⟼t2⁢sin⁡t2
384 oveq1 ⊢t=s→t2=s2
385 384 fveq2d ⊢t=s→sin⁡t2=sin⁡s2
386 385 oveq2d ⊢t=s→2⁢sin⁡t2=2⁢sin⁡s2
387 376 386 oveq12d ⊢t=s→t2⁢sin⁡t2=s2⁢sin⁡s2
388 387 adantl ⊢φ∧k∈0..^N∧s∈J⁡kJ⁡k+1∧t=s→t2⁢sin⁡t2=s2⁢sin⁡s2
389 ovex ⊢s2⁢sin⁡s2∈V
390 389 a1i ⊢φ∧k∈0..^N∧s∈J⁡kJ⁡k+1→s2⁢sin⁡s2∈V
391 383 388 379 390 fvmptd ⊢φ∧k∈0..^N∧s∈J⁡kJ⁡k+1→t∈J⁡kJ⁡k+1⟼t2⁢sin⁡t2⁡s=s2⁢sin⁡s2
392 382 391 oveq12d ⊢φ∧k∈0..^N∧s∈J⁡kJ⁡k+1→t∈J⁡kJ⁡k+1⟼F⁡X+t−Yt⁡s⁢t∈J⁡kJ⁡k+1⟼t2⁢sin⁡t2⁡s=F⁡X+s−Ys⁢s2⁢sin⁡s2
393 392 eqcomd ⊢φ∧k∈0..^N∧s∈J⁡kJ⁡k+1→F⁡X+s−Ys⁢s2⁢sin⁡s2=t∈J⁡kJ⁡k+1⟼F⁡X+t−Yt⁡s⁢t∈J⁡kJ⁡k+1⟼t2⁢sin⁡t2⁡s
394 393 adantllr ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→F⁡X+s−Ys⁢s2⁢sin⁡s2=t∈J⁡kJ⁡k+1⟼F⁡X+t−Yt⁡s⁢t∈J⁡kJ⁡k+1⟼t2⁢sin⁡t2⁡s
395 369 371 394 3eqtrd ⊢φ∧d∈0π∧k∈0..^N∧s∈J⁡kJ⁡k+1→O⁡s=t∈J⁡kJ⁡k+1⟼F⁡X+t−Yt⁡s⁢t∈J⁡kJ⁡k+1⟼t2⁢sin⁡t2⁡s
396 395 mpteq2dva ⊢φ∧d∈0π∧k∈0..^N→s∈J⁡kJ⁡k+1⟼O⁡s=s∈J⁡kJ⁡k+1⟼t∈J⁡kJ⁡k+1⟼F⁡X+t−Yt⁡s⁢t∈J⁡kJ⁡k+1⟼t2⁢sin⁡t2⁡s
397 350 396 eqtr2d ⊢φ∧d∈0π∧k∈0..^N→s∈J⁡kJ⁡k+1⟼t∈J⁡kJ⁡k+1⟼F⁡X+t−Yt⁡s⁢t∈J⁡kJ⁡k+1⟼t2⁢sin⁡t2⁡s=O↾J⁡kJ⁡k+1
398 397 oveq2d ⊢φ∧d∈0π∧k∈0..^N→ds∈J⁡kJ⁡k+1t∈J⁡kJ⁡k+1⟼F⁡X+t−Yt⁡s⁢t∈J⁡kJ⁡k+1⟼t2⁢sin⁡t2⁡sdℝs=ℝDO↾J⁡kJ⁡k+1
399 66 a1i ⊢φ∧d∈0π∧k∈0..^N→ℝ⊆ℂ
400 349 317 sstrd ⊢φ∧d∈0π∧k∈0..^N→J⁡kJ⁡k+1⊆ℝ
401 49 tgioo2 ⊢topGen⁡ran⁡.=TopOpen⁡ℂfld↾𝑡ℝ
402 49 401 dvres ⊢ℝ⊆ℂ∧O:dπ⟶ℂ∧dπ⊆ℝ∧J⁡kJ⁡k+1⊆ℝ→ℝDO↾J⁡kJ⁡k+1=Oℝ′↾int⁡topGen⁡ran⁡.⁡J⁡kJ⁡k+1
403 399 311 317 400 402 syl22anc ⊢φ∧d∈0π∧k∈0..^N→ℝDO↾J⁡kJ⁡k+1=Oℝ′↾int⁡topGen⁡ran⁡.⁡J⁡kJ⁡k+1
404 ioontr ⊢int⁡topGen⁡ran⁡.⁡J⁡kJ⁡k+1=J⁡kJ⁡k+1
405 404 a1i ⊢φ∧d∈0π∧k∈0..^N→int⁡topGen⁡ran⁡.⁡J⁡kJ⁡k+1=J⁡kJ⁡k+1
406 405 reseq2d ⊢φ∧d∈0π∧k∈0..^N→Oℝ′↾int⁡topGen⁡ran⁡.⁡J⁡kJ⁡k+1=Oℝ′↾J⁡kJ⁡k+1
407 398 403 406 3eqtrrd ⊢φ∧d∈0π∧k∈0..^N→Oℝ′↾J⁡kJ⁡k+1=ds∈J⁡kJ⁡k+1t∈J⁡kJ⁡k+1⟼F⁡X+t−Yt⁡s⁢t∈J⁡kJ⁡k+1⟼t2⁢sin⁡t2⁡sdℝs
408 1 ad2antrr ⊢φ∧d∈0π∧k∈0..^N→F:ℝ⟶ℝ
409 2 ad2antrr ⊢φ∧d∈0π∧k∈0..^N→X∈ℝ
410 4 ad2antrr ⊢φ∧d∈0π∧k∈0..^N→M∈ℕ
411 5 ad2antrr ⊢φ∧d∈0π∧k∈0..^N→V∈P⁡M
412 9 ad4ant14 ⊢φ∧d∈0π∧k∈0..^N∧i∈0..^M→Fℝ′↾V⁡iV⁡i+1:V⁡iV⁡i+1⟶cnℝ
413 85 adantr ⊢φ∧d∈0π∧k∈0..^N→dπ⊆−ππ
414 349 413 sstrd ⊢φ∧d∈0π∧k∈0..^N→J⁡kJ⁡k+1⊆−ππ
415 76 a1i ⊢φ∧d∈0π∧k∈0..^N→0∈ℝ*
416 0red ⊢φ∧d∈0π∧k∈0..^N→0∈ℝ
417 79 ad2antlr ⊢φ∧d∈0π∧k∈0..^N→0<d
418 416 322 320 417 326 ltletrd ⊢φ∧d∈0π∧k∈0..^N→0<J⁡k
419 320 331 415 418 ltnelicc ⊢φ∧d∈0π∧k∈0..^N→¬0∈J⁡kJ⁡k+1
420 54 ad2antrr ⊢φ∧d∈0π∧k∈0..^N→Y∈ℝ
421 42 a1i ⊢φ∧d∈0π∧k∈0..^N→π∈ℝ
422 281 adantr ⊢φ∧d∈0π∧k∈0..^N→d<π
423 simpr ⊢φ∧d∈0π∧k∈0..^N→k∈0..^N
424 biid ⊢φ∧d∈0π∧k∈0..^N∧i∈0..^M∧J⁡kJ⁡k+1⊆Q⁡iQ⁡i+1∧v∈0..^M∧J⁡kJ⁡k+1⊆Q⁡vQ⁡v+1↔φ∧d∈0π∧k∈0..^N∧i∈0..^M∧J⁡kJ⁡k+1⊆Q⁡iQ⁡i+1∧v∈0..^M∧J⁡kJ⁡k+1⊆Q⁡vQ⁡v+1
425 409 3 410 411 322 421 422 413 29 26 27 28 423 298 424 fourierdlem50 ⊢φ∧d∈0π∧k∈0..^N→ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1∈0..^M∧J⁡kJ⁡k+1⊆Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1
426 425 simpld ⊢φ∧d∈0π∧k∈0..^N→ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1∈0..^M
427 425 simprd ⊢φ∧d∈0π∧k∈0..^N→J⁡kJ⁡k+1⊆Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1
428 377 cbvmptv ⊢t∈J⁡kJ⁡k+1⟼F⁡X+t−Yt=s∈J⁡kJ⁡k+1⟼F⁡X+s−Ys
429 387 cbvmptv ⊢t∈J⁡kJ⁡k+1⟼t2⁢sin⁡t2=s∈J⁡kJ⁡k+1⟼s2⁢sin⁡s2
430 eqid ⊢s∈J⁡kJ⁡k+1⟼t∈J⁡kJ⁡k+1⟼F⁡X+t−Yt⁡s⁢t∈J⁡kJ⁡k+1⟼t2⁢sin⁡t2⁡s=s∈J⁡kJ⁡k+1⟼t∈J⁡kJ⁡k+1⟼F⁡X+t−Yt⁡s⁢t∈J⁡kJ⁡k+1⟼t2⁢sin⁡t2⁡s
431 408 409 3 410 411 412 320 330 191 414 419 420 29 426 427 428 429 430 fourierdlem72 ⊢φ∧d∈0π∧k∈0..^N→ds∈J⁡kJ⁡k+1t∈J⁡kJ⁡k+1⟼F⁡X+t−Yt⁡s⁢t∈J⁡kJ⁡k+1⟼t2⁢sin⁡t2⁡sdℝs:J⁡kJ⁡k+1⟶cnℂ
432 407 431 eqeltrd ⊢φ∧d∈0π∧k∈0..^N→Oℝ′↾J⁡kJ⁡k+1:J⁡kJ⁡k+1⟶cnℂ
433 eqid ⊢s∈dπ⟼F⁡X+s−Y2⁢sin⁡s2=s∈dπ⟼F⁡X+s−Y2⁢sin⁡s2
434 eqid ⊢X+J⁡kX+J⁡k+1=X+J⁡kX+J⁡k+1
435 30 426 eqeltrid ⊢φ∧d∈0π∧k∈0..^N→C∈0..^M
436 simpll ⊢φ∧d∈0π∧k∈0..^N→φ
437 436 435 jca ⊢φ∧d∈0π∧k∈0..^N→φ∧C∈0..^M
438 eleq1 ⊢i=C→i∈0..^M↔C∈0..^M
439 438 anbi2d ⊢i=C→φ∧i∈0..^M↔φ∧C∈0..^M
440 fveq2 ⊢i=C→V⁡i=V⁡C
441 oveq1 ⊢i=C→i+1=C+1
442 441 fveq2d ⊢i=C→V⁡i+1=V⁡C+1
443 440 442 oveq12d ⊢i=C→V⁡iV⁡i+1=V⁡CV⁡C+1
444 raleq ⊢V⁡iV⁡i+1=V⁡CV⁡C+1→∀t∈V⁡iV⁡i+1F⁡t≤w↔∀t∈V⁡CV⁡C+1F⁡t≤w
445 443 444 syl ⊢i=C→∀t∈V⁡iV⁡i+1F⁡t≤w↔∀t∈V⁡CV⁡C+1F⁡t≤w
446 445 rexbidv ⊢i=C→∃w∈ℝ∀t∈V⁡iV⁡i+1F⁡t≤w↔∃w∈ℝ∀t∈V⁡CV⁡C+1F⁡t≤w
447 439 446 imbi12d ⊢i=C→φ∧i∈0..^M→∃w∈ℝ∀t∈V⁡iV⁡i+1F⁡t≤w↔φ∧C∈0..^M→∃w∈ℝ∀t∈V⁡CV⁡C+1F⁡t≤w
448 447 8 vtoclg ⊢C∈0..^M→φ∧C∈0..^M→∃w∈ℝ∀t∈V⁡CV⁡C+1F⁡t≤w
449 435 437 448 sylc ⊢φ∧d∈0π∧k∈0..^N→∃w∈ℝ∀t∈V⁡CV⁡C+1F⁡t≤w
450 nfv ⊢Ⅎtφ∧d∈0π∧k∈0..^N
451 nfra1 ⊢Ⅎt∀t∈V⁡CV⁡C+1F⁡t≤w
452 450 451 nfan ⊢Ⅎtφ∧d∈0π∧k∈0..^N∧∀t∈V⁡CV⁡C+1F⁡t≤w
453 simplr ⊢φ∧d∈0π∧k∈0..^N∧∀t∈V⁡CV⁡C+1F⁡t≤w∧t∈X+J⁡kX+J⁡k+1→∀t∈V⁡CV⁡C+1F⁡t≤w
454 70 a1i ⊢φ→−π∈ℝ
455 454 2 readdcld ⊢φ→-π+X∈ℝ
456 42 a1i ⊢φ→π∈ℝ
457 456 2 readdcld ⊢φ→π+X∈ℝ
458 455 457 iccssred ⊢φ→-π+Xπ+X⊆ℝ
459 ressxr ⊢ℝ⊆ℝ*
460 458 459 sstrdi ⊢φ→-π+Xπ+X⊆ℝ*
461 460 ad2antrr ⊢φ∧d∈0π∧k∈0..^N→-π+Xπ+X⊆ℝ*
462 3 410 411 fourierdlem15 ⊢φ∧d∈0π∧k∈0..^N→V:0…M⟶-π+Xπ+X
463 elfzofz ⊢C∈0..^M→C∈0…M
464 435 463 syl ⊢φ∧d∈0π∧k∈0..^N→C∈0…M
465 462 464 ffvelcdmd ⊢φ∧d∈0π∧k∈0..^N→V⁡C∈-π+Xπ+X
466 461 465 sseldd ⊢φ∧d∈0π∧k∈0..^N→V⁡C∈ℝ*
467 466 adantr ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→V⁡C∈ℝ*
468 fzofzp1 ⊢C∈0..^M→C+1∈0…M
469 435 468 syl ⊢φ∧d∈0π∧k∈0..^N→C+1∈0…M
470 462 469 ffvelcdmd ⊢φ∧d∈0π∧k∈0..^N→V⁡C+1∈-π+Xπ+X
471 461 470 sseldd ⊢φ∧d∈0π∧k∈0..^N→V⁡C+1∈ℝ*
472 471 adantr ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→V⁡C+1∈ℝ*
473 elioore ⊢t∈X+J⁡kX+J⁡k+1→t∈ℝ
474 473 adantl ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→t∈ℝ
475 70 a1i ⊢φ∧d∈0π∧k∈0..^N→−π∈ℝ
476 475 421 409 3 410 411 464 29 fourierdlem13 ⊢φ∧d∈0π∧k∈0..^N→Q⁡C=V⁡C−X∧V⁡C=X+Q⁡C
477 476 simprd ⊢φ∧d∈0π∧k∈0..^N→V⁡C=X+Q⁡C
478 477 adantr ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→V⁡C=X+Q⁡C
479 458 ad2antrr ⊢φ∧d∈0π∧k∈0..^N→-π+Xπ+X⊆ℝ
480 479 465 sseldd ⊢φ∧d∈0π∧k∈0..^N→V⁡C∈ℝ
481 480 adantr ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→V⁡C∈ℝ
482 478 481 eqeltrrd ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→X+Q⁡C∈ℝ
483 409 320 readdcld ⊢φ∧d∈0π∧k∈0..^N→X+J⁡k∈ℝ
484 483 adantr ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→X+J⁡k∈ℝ
485 476 simpld ⊢φ∧d∈0π∧k∈0..^N→Q⁡C=V⁡C−X
486 480 409 resubcld ⊢φ∧d∈0π∧k∈0..^N→V⁡C−X∈ℝ
487 485 486 eqeltrd ⊢φ∧d∈0π∧k∈0..^N→Q⁡C∈ℝ
488 475 421 409 3 410 411 469 29 fourierdlem13 ⊢φ∧d∈0π∧k∈0..^N→Q⁡C+1=V⁡C+1−X∧V⁡C+1=X+Q⁡C+1
489 488 simpld ⊢φ∧d∈0π∧k∈0..^N→Q⁡C+1=V⁡C+1−X
490 479 470 sseldd ⊢φ∧d∈0π∧k∈0..^N→V⁡C+1∈ℝ
491 490 409 resubcld ⊢φ∧d∈0π∧k∈0..^N→V⁡C+1−X∈ℝ
492 489 491 eqeltrd ⊢φ∧d∈0π∧k∈0..^N→Q⁡C+1∈ℝ
493 30 eqcomi ⊢ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1=C
494 493 fveq2i ⊢Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1=Q⁡C
495 493 oveq1i ⊢ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1=C+1
496 495 fveq2i ⊢Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1=Q⁡C+1
497 494 496 oveq12i ⊢Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1=Q⁡CQ⁡C+1
498 427 497 sseqtrdi ⊢φ∧d∈0π∧k∈0..^N→J⁡kJ⁡k+1⊆Q⁡CQ⁡C+1
499 487 492 320 330 191 498 fourierdlem10 ⊢φ∧d∈0π∧k∈0..^N→Q⁡C≤J⁡k∧J⁡k+1≤Q⁡C+1
500 499 simpld ⊢φ∧d∈0π∧k∈0..^N→Q⁡C≤J⁡k
501 487 320 409 500 leadd2dd ⊢φ∧d∈0π∧k∈0..^N→X+Q⁡C≤X+J⁡k
502 501 adantr ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→X+Q⁡C≤X+J⁡k
503 484 rexrd ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→X+J⁡k∈ℝ*
504 409 330 readdcld ⊢φ∧d∈0π∧k∈0..^N→X+J⁡k+1∈ℝ
505 504 rexrd ⊢φ∧d∈0π∧k∈0..^N→X+J⁡k+1∈ℝ*
506 505 adantr ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→X+J⁡k+1∈ℝ*
507 simpr ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→t∈X+J⁡kX+J⁡k+1
508 ioogtlb ⊢X+J⁡k∈ℝ*∧X+J⁡k+1∈ℝ*∧t∈X+J⁡kX+J⁡k+1→X+J⁡k<t
509 503 506 507 508 syl3anc ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→X+J⁡k<t
510 482 484 474 502 509 lelttrd ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→X+Q⁡C<t
511 478 510 eqbrtrd ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→V⁡C<t
512 504 adantr ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→X+J⁡k+1∈ℝ
513 488 simprd ⊢φ∧d∈0π∧k∈0..^N→V⁡C+1=X+Q⁡C+1
514 513 490 eqeltrrd ⊢φ∧d∈0π∧k∈0..^N→X+Q⁡C+1∈ℝ
515 514 adantr ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→X+Q⁡C+1∈ℝ
516 iooltub ⊢X+J⁡k∈ℝ*∧X+J⁡k+1∈ℝ*∧t∈X+J⁡kX+J⁡k+1→t<X+J⁡k+1
517 503 506 507 516 syl3anc ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→t<X+J⁡k+1
518 499 simprd ⊢φ∧d∈0π∧k∈0..^N→J⁡k+1≤Q⁡C+1
519 330 492 409 518 leadd2dd ⊢φ∧d∈0π∧k∈0..^N→X+J⁡k+1≤X+Q⁡C+1
520 519 adantr ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→X+J⁡k+1≤X+Q⁡C+1
521 474 512 515 517 520 ltletrd ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→t<X+Q⁡C+1
522 513 eqcomd ⊢φ∧d∈0π∧k∈0..^N→X+Q⁡C+1=V⁡C+1
523 522 adantr ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→X+Q⁡C+1=V⁡C+1
524 521 523 breqtrd ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→t<V⁡C+1
525 467 472 474 511 524 eliood ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→t∈V⁡CV⁡C+1
526 525 adantlr ⊢φ∧d∈0π∧k∈0..^N∧∀t∈V⁡CV⁡C+1F⁡t≤w∧t∈X+J⁡kX+J⁡k+1→t∈V⁡CV⁡C+1
527 rspa ⊢∀t∈V⁡CV⁡C+1F⁡t≤w∧t∈V⁡CV⁡C+1→F⁡t≤w
528 453 526 527 syl2anc ⊢φ∧d∈0π∧k∈0..^N∧∀t∈V⁡CV⁡C+1F⁡t≤w∧t∈X+J⁡kX+J⁡k+1→F⁡t≤w
529 528 ex ⊢φ∧d∈0π∧k∈0..^N∧∀t∈V⁡CV⁡C+1F⁡t≤w→t∈X+J⁡kX+J⁡k+1→F⁡t≤w
530 452 529 ralrimi ⊢φ∧d∈0π∧k∈0..^N∧∀t∈V⁡CV⁡C+1F⁡t≤w→∀t∈X+J⁡kX+J⁡k+1F⁡t≤w
531 530 ex ⊢φ∧d∈0π∧k∈0..^N→∀t∈V⁡CV⁡C+1F⁡t≤w→∀t∈X+J⁡kX+J⁡k+1F⁡t≤w
532 531 reximdv ⊢φ∧d∈0π∧k∈0..^N→∃w∈ℝ∀t∈V⁡CV⁡C+1F⁡t≤w→∃w∈ℝ∀t∈X+J⁡kX+J⁡k+1F⁡t≤w
533 449 532 mpd ⊢φ∧d∈0π∧k∈0..^N→∃w∈ℝ∀t∈X+J⁡kX+J⁡k+1F⁡t≤w
534 443 raleqdv ⊢i=C→∀t∈V⁡iV⁡i+1Fℝ′⁡t≤z↔∀t∈V⁡CV⁡C+1Fℝ′⁡t≤z
535 534 rexbidv ⊢i=C→∃z∈ℝ∀t∈V⁡iV⁡i+1Fℝ′⁡t≤z↔∃z∈ℝ∀t∈V⁡CV⁡C+1Fℝ′⁡t≤z
536 439 535 imbi12d ⊢i=C→φ∧i∈0..^M→∃z∈ℝ∀t∈V⁡iV⁡i+1Fℝ′⁡t≤z↔φ∧C∈0..^M→∃z∈ℝ∀t∈V⁡CV⁡C+1Fℝ′⁡t≤z
537 536 10 vtoclg ⊢C∈0..^M→φ∧C∈0..^M→∃z∈ℝ∀t∈V⁡CV⁡C+1Fℝ′⁡t≤z
538 435 437 537 sylc ⊢φ∧d∈0π∧k∈0..^N→∃z∈ℝ∀t∈V⁡CV⁡C+1Fℝ′⁡t≤z
539 nfra1 ⊢Ⅎt∀t∈V⁡CV⁡C+1Fℝ′⁡t≤z
540 450 539 nfan ⊢Ⅎtφ∧d∈0π∧k∈0..^N∧∀t∈V⁡CV⁡C+1Fℝ′⁡t≤z
541 1 67 fssd ⊢φ→F:ℝ⟶ℂ
542 ssid ⊢ℝ⊆ℝ
543 542 a1i ⊢φ→ℝ⊆ℝ
544 ioossre ⊢X+J⁡kX+J⁡k+1⊆ℝ
545 544 a1i ⊢φ→X+J⁡kX+J⁡k+1⊆ℝ
546 49 401 dvres ⊢ℝ⊆ℂ∧F:ℝ⟶ℂ∧ℝ⊆ℝ∧X+J⁡kX+J⁡k+1⊆ℝ→ℝDF↾X+J⁡kX+J⁡k+1=Fℝ′↾int⁡topGen⁡ran⁡.⁡X+J⁡kX+J⁡k+1
547 67 541 543 545 546 syl22anc ⊢φ→ℝDF↾X+J⁡kX+J⁡k+1=Fℝ′↾int⁡topGen⁡ran⁡.⁡X+J⁡kX+J⁡k+1
548 ioontr ⊢int⁡topGen⁡ran⁡.⁡X+J⁡kX+J⁡k+1=X+J⁡kX+J⁡k+1
549 548 reseq2i ⊢Fℝ′↾int⁡topGen⁡ran⁡.⁡X+J⁡kX+J⁡k+1=Fℝ′↾X+J⁡kX+J⁡k+1
550 547 549 eqtrdi ⊢φ→ℝDF↾X+J⁡kX+J⁡k+1=Fℝ′↾X+J⁡kX+J⁡k+1
551 550 fveq1d ⊢φ→F↾X+J⁡kX+J⁡k+1ℝ′⁡t=Fℝ′↾X+J⁡kX+J⁡k+1⁡t
552 fvres ⊢t∈X+J⁡kX+J⁡k+1→Fℝ′↾X+J⁡kX+J⁡k+1⁡t=Fℝ′⁡t
553 551 552 sylan9eq ⊢φ∧t∈X+J⁡kX+J⁡k+1→F↾X+J⁡kX+J⁡k+1ℝ′⁡t=Fℝ′⁡t
554 553 ad4ant14 ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→F↾X+J⁡kX+J⁡k+1ℝ′⁡t=Fℝ′⁡t
555 554 fveq2d ⊢φ∧d∈0π∧k∈0..^N∧t∈X+J⁡kX+J⁡k+1→F↾X+J⁡kX+J⁡k+1ℝ′⁡t=Fℝ′⁡t
556 555 adantlr ⊢φ∧d∈0π∧k∈0..^N∧∀t∈V⁡CV⁡C+1Fℝ′⁡t≤z∧t∈X+J⁡kX+J⁡k+1→F↾X+J⁡kX+J⁡k+1ℝ′⁡t=Fℝ′⁡t
557 simplr ⊢φ∧d∈0π∧k∈0..^N∧∀t∈V⁡CV⁡C+1Fℝ′⁡t≤z∧t∈X+J⁡kX+J⁡k+1→∀t∈V⁡CV⁡C+1Fℝ′⁡t≤z
558 525 adantlr ⊢φ∧d∈0π∧k∈0..^N∧∀t∈V⁡CV⁡C+1Fℝ′⁡t≤z∧t∈X+J⁡kX+J⁡k+1→t∈V⁡CV⁡C+1
559 rspa ⊢∀t∈V⁡CV⁡C+1Fℝ′⁡t≤z∧t∈V⁡CV⁡C+1→Fℝ′⁡t≤z
560 557 558 559 syl2anc ⊢φ∧d∈0π∧k∈0..^N∧∀t∈V⁡CV⁡C+1Fℝ′⁡t≤z∧t∈X+J⁡kX+J⁡k+1→Fℝ′⁡t≤z
561 556 560 eqbrtrd ⊢φ∧d∈0π∧k∈0..^N∧∀t∈V⁡CV⁡C+1Fℝ′⁡t≤z∧t∈X+J⁡kX+J⁡k+1→F↾X+J⁡kX+J⁡k+1ℝ′⁡t≤z
562 561 ex ⊢φ∧d∈0π∧k∈0..^N∧∀t∈V⁡CV⁡C+1Fℝ′⁡t≤z→t∈X+J⁡kX+J⁡k+1→F↾X+J⁡kX+J⁡k+1ℝ′⁡t≤z
563 540 562 ralrimi ⊢φ∧d∈0π∧k∈0..^N∧∀t∈V⁡CV⁡C+1Fℝ′⁡t≤z→∀t∈X+J⁡kX+J⁡k+1F↾X+J⁡kX+J⁡k+1ℝ′⁡t≤z
564 563 ex ⊢φ∧d∈0π∧k∈0..^N→∀t∈V⁡CV⁡C+1Fℝ′⁡t≤z→∀t∈X+J⁡kX+J⁡k+1F↾X+J⁡kX+J⁡k+1ℝ′⁡t≤z
565 564 reximdv ⊢φ∧d∈0π∧k∈0..^N→∃z∈ℝ∀t∈V⁡CV⁡C+1Fℝ′⁡t≤z→∃z∈ℝ∀t∈X+J⁡kX+J⁡k+1F↾X+J⁡kX+J⁡k+1ℝ′⁡t≤z
566 538 565 mpd ⊢φ∧d∈0π∧k∈0..^N→∃z∈ℝ∀t∈X+J⁡kX+J⁡k+1F↾X+J⁡kX+J⁡k+1ℝ′⁡t≤z
567 323 324 318 423 fourierdlem8 ⊢φ∧d∈0π∧k∈0..^N→J⁡kJ⁡k+1⊆dπ
568 143 ad2antrr ⊢φ∧d∈0π∧r∈dπ∧¬r∈ran⁡J→N∈ℕ
569 167 316 fssd ⊢φ∧d∈0π→J:0…N⟶ℝ
570 569 ad2antrr ⊢φ∧d∈0π∧r∈dπ∧¬r∈ran⁡J→J:0…N⟶ℝ
571 simpr ⊢φ∧d∈0π∧r∈dπ→r∈dπ
572 168 eqcomd ⊢φ∧d∈0π→d=J⁡0
573 169 eqcomd ⊢φ∧d∈0π→π=J⁡N
574 572 573 oveq12d ⊢φ∧d∈0π→dπ=J⁡0J⁡N
575 574 adantr ⊢φ∧d∈0π∧r∈dπ→dπ=J⁡0J⁡N
576 571 575 eleqtrd ⊢φ∧d∈0π∧r∈dπ→r∈J⁡0J⁡N
577 576 adantr ⊢φ∧d∈0π∧r∈dπ∧¬r∈ran⁡J→r∈J⁡0J⁡N
578 simpr ⊢φ∧d∈0π∧r∈dπ∧¬r∈ran⁡J→¬r∈ran⁡J
579 fveq2 ⊢j=k→J⁡j=J⁡k
580 579 breq1d ⊢j=k→J⁡j<r↔J⁡k<r
581 580 cbvrabv ⊢j∈0..^N|J⁡j<r=k∈0..^N|J⁡k<r
582 581 supeq1i ⊢supj∈0..^N|J⁡j<rℝ<=supk∈0..^N|J⁡k<rℝ<
583 568 570 577 578 582 fourierdlem25 ⊢φ∧d∈0π∧r∈dπ∧¬r∈ran⁡J→∃m∈0..^Nr∈J⁡mJ⁡m+1
584 541 ad2antrr ⊢φ∧d∈0π∧k∈0..^N→F:ℝ⟶ℂ
585 542 a1i ⊢φ∧d∈0π∧k∈0..^N→ℝ⊆ℝ
586 544 a1i ⊢φ∧d∈0π∧k∈0..^N→X+J⁡kX+J⁡k+1⊆ℝ
587 399 584 585 586 546 syl22anc ⊢φ∧d∈0π∧k∈0..^N→ℝDF↾X+J⁡kX+J⁡k+1=Fℝ′↾int⁡topGen⁡ran⁡.⁡X+J⁡kX+J⁡k+1
588 525 ralrimiva ⊢φ∧d∈0π∧k∈0..^N→∀t∈X+J⁡kX+J⁡k+1t∈V⁡CV⁡C+1
589 dfss3 ⊢X+J⁡kX+J⁡k+1⊆V⁡CV⁡C+1↔∀t∈X+J⁡kX+J⁡k+1t∈V⁡CV⁡C+1
590 588 589 sylibr ⊢φ∧d∈0π∧k∈0..^N→X+J⁡kX+J⁡k+1⊆V⁡CV⁡C+1
591 resabs2 ⊢X+J⁡kX+J⁡k+1⊆V⁡CV⁡C+1→Fℝ′↾X+J⁡kX+J⁡k+1↾V⁡CV⁡C+1=Fℝ′↾X+J⁡kX+J⁡k+1
592 590 591 syl ⊢φ∧d∈0π∧k∈0..^N→Fℝ′↾X+J⁡kX+J⁡k+1↾V⁡CV⁡C+1=Fℝ′↾X+J⁡kX+J⁡k+1
593 549 587 592 3eqtr4a ⊢φ∧d∈0π∧k∈0..^N→ℝDF↾X+J⁡kX+J⁡k+1=Fℝ′↾X+J⁡kX+J⁡k+1↾V⁡CV⁡C+1
594 590 resabs1d ⊢φ∧d∈0π∧k∈0..^N→Fℝ′↾V⁡CV⁡C+1↾X+J⁡kX+J⁡k+1=Fℝ′↾X+J⁡kX+J⁡k+1
595 594 eqcomd ⊢φ∧d∈0π∧k∈0..^N→Fℝ′↾X+J⁡kX+J⁡k+1=Fℝ′↾V⁡CV⁡C+1↾X+J⁡kX+J⁡k+1
596 593 592 595 3eqtrrd ⊢φ∧d∈0π∧k∈0..^N→Fℝ′↾V⁡CV⁡C+1↾X+J⁡kX+J⁡k+1=ℝDF↾X+J⁡kX+J⁡k+1
597 443 reseq2d ⊢i=C→Fℝ′↾V⁡iV⁡i+1=Fℝ′↾V⁡CV⁡C+1
598 597 443 feq12d ⊢i=C→Fℝ′↾V⁡iV⁡i+1:V⁡iV⁡i+1⟶ℝ↔Fℝ′↾V⁡CV⁡C+1:V⁡CV⁡C+1⟶ℝ
599 439 598 imbi12d ⊢i=C→φ∧i∈0..^M→Fℝ′↾V⁡iV⁡i+1:V⁡iV⁡i+1⟶ℝ↔φ∧C∈0..^M→Fℝ′↾V⁡CV⁡C+1:V⁡CV⁡C+1⟶ℝ
600 cncff ⊢Fℝ′↾V⁡iV⁡i+1:V⁡iV⁡i+1⟶cnℝ→Fℝ′↾V⁡iV⁡i+1:V⁡iV⁡i+1⟶ℝ
601 9 600 syl ⊢φ∧i∈0..^M→Fℝ′↾V⁡iV⁡i+1:V⁡iV⁡i+1⟶ℝ
602 599 601 vtoclg ⊢C∈0..^M→φ∧C∈0..^M→Fℝ′↾V⁡CV⁡C+1:V⁡CV⁡C+1⟶ℝ
603 602 anabsi7 ⊢φ∧C∈0..^M→Fℝ′↾V⁡CV⁡C+1:V⁡CV⁡C+1⟶ℝ
604 437 603 syl ⊢φ∧d∈0π∧k∈0..^N→Fℝ′↾V⁡CV⁡C+1:V⁡CV⁡C+1⟶ℝ
605 604 590 fssresd ⊢φ∧d∈0π∧k∈0..^N→Fℝ′↾V⁡CV⁡C+1↾X+J⁡kX+J⁡k+1:X+J⁡kX+J⁡k+1⟶ℝ
606 596 605 feq1dd ⊢φ∧d∈0π∧k∈0..^N→F↾X+J⁡kX+J⁡k+1ℝ′:X+J⁡kX+J⁡k+1⟶ℝ
607 375 386 oveq12d ⊢t=s→F⁡X+t−Y2⁢sin⁡t2=F⁡X+s−Y2⁢sin⁡s2
608 607 cbvmptv ⊢t∈J⁡kJ⁡k+1⟼F⁡X+t−Y2⁢sin⁡t2=s∈J⁡kJ⁡k+1⟼F⁡X+s−Y2⁢sin⁡s2
609 fveq2 ⊢r=t→F⁡r=F⁡t
610 609 fveq2d ⊢r=t→F⁡r=F⁡t
611 610 breq1d ⊢r=t→F⁡r≤w↔F⁡t≤w
612 611 cbvralvw ⊢∀r∈X+J⁡kX+J⁡k+1F⁡r≤w↔∀t∈X+J⁡kX+J⁡k+1F⁡t≤w
613 612 anbi2i ⊢φ∧d∈0π∧k∈0..^N∧w∈ℝ∧z∈ℝ∧∀r∈X+J⁡kX+J⁡k+1F⁡r≤w↔φ∧d∈0π∧k∈0..^N∧w∈ℝ∧z∈ℝ∧∀t∈X+J⁡kX+J⁡k+1F⁡t≤w
614 fveq2 ⊢r=t→F↾X+J⁡kX+J⁡k+1ℝ′⁡r=F↾X+J⁡kX+J⁡k+1ℝ′⁡t
615 614 fveq2d ⊢r=t→F↾X+J⁡kX+J⁡k+1ℝ′⁡r=F↾X+J⁡kX+J⁡k+1ℝ′⁡t
616 615 breq1d ⊢r=t→F↾X+J⁡kX+J⁡k+1ℝ′⁡r≤z↔F↾X+J⁡kX+J⁡k+1ℝ′⁡t≤z
617 616 cbvralvw ⊢∀r∈X+J⁡kX+J⁡k+1F↾X+J⁡kX+J⁡k+1ℝ′⁡r≤z↔∀t∈X+J⁡kX+J⁡k+1F↾X+J⁡kX+J⁡k+1ℝ′⁡t≤z
618 613 617 anbi12i ⊢φ∧d∈0π∧k∈0..^N∧w∈ℝ∧z∈ℝ∧∀r∈X+J⁡kX+J⁡k+1F⁡r≤w∧∀r∈X+J⁡kX+J⁡k+1F↾X+J⁡kX+J⁡k+1ℝ′⁡r≤z↔φ∧d∈0π∧k∈0..^N∧w∈ℝ∧z∈ℝ∧∀t∈X+J⁡kX+J⁡k+1F⁡t≤w∧∀t∈X+J⁡kX+J⁡k+1F↾X+J⁡kX+J⁡k+1ℝ′⁡t≤z
619 274 275 41 43 85 288 289 433 434 533 566 167 191 567 583 606 608 618 fourierdlem80 ⊢φ∧d∈0π→∃b∈ℝ∀s∈dom⁡ds∈dπF⁡X+s−Y2⁢sin⁡s2dℝsds∈dπF⁡X+s−Y2⁢sin⁡s2dℝs⁡s≤b
620 366 mpteq2dva ⊢φ∧d∈0π→s∈dπ⟼F⁡X+s−Ys⁢s2⁢sin⁡s2=s∈dπ⟼F⁡X+s−Y2⁢sin⁡s2
621 271 620 eqtrd ⊢φ∧d∈0π→O=s∈dπ⟼F⁡X+s−Y2⁢sin⁡s2
622 621 oveq2d ⊢φ∧d∈0π→ℝDO=ds∈dπF⁡X+s−Y2⁢sin⁡s2dℝs
623 622 dmeqd ⊢φ∧d∈0π→dom⁡Oℝ′=dom⁡ds∈dπF⁡X+s−Y2⁢sin⁡s2dℝs
624 nfcv ⊢Ⅎ_sdom⁡Oℝ′
625 nfcv ⊢Ⅎ_sℝ
626 nfcv ⊢Ⅎ_sD
627 nfmpt1 ⊢Ⅎ_ss∈dπ⟼F⁡X+s−Y2⁢sin⁡s2
628 625 626 627 nfov ⊢Ⅎ_sds∈dπF⁡X+s−Y2⁢sin⁡s2dℝs
629 628 nfdm ⊢Ⅎ_sdom⁡ds∈dπF⁡X+s−Y2⁢sin⁡s2dℝs
630 624 629 raleqf ⊢dom⁡Oℝ′=dom⁡ds∈dπF⁡X+s−Y2⁢sin⁡s2dℝs→∀s∈dom⁡Oℝ′Oℝ′⁡s≤b↔∀s∈dom⁡ds∈dπF⁡X+s−Y2⁢sin⁡s2dℝsOℝ′⁡s≤b
631 623 630 syl ⊢φ∧d∈0π→∀s∈dom⁡Oℝ′Oℝ′⁡s≤b↔∀s∈dom⁡ds∈dπF⁡X+s−Y2⁢sin⁡s2dℝsOℝ′⁡s≤b
632 622 fveq1d ⊢φ∧d∈0π→Oℝ′⁡s=ds∈dπF⁡X+s−Y2⁢sin⁡s2dℝs⁡s
633 632 fveq2d ⊢φ∧d∈0π→Oℝ′⁡s=ds∈dπF⁡X+s−Y2⁢sin⁡s2dℝs⁡s
634 633 breq1d ⊢φ∧d∈0π→Oℝ′⁡s≤b↔ds∈dπF⁡X+s−Y2⁢sin⁡s2dℝs⁡s≤b
635 634 ralbidv ⊢φ∧d∈0π→∀s∈dom⁡ds∈dπF⁡X+s−Y2⁢sin⁡s2dℝsOℝ′⁡s≤b↔∀s∈dom⁡ds∈dπF⁡X+s−Y2⁢sin⁡s2dℝsds∈dπF⁡X+s−Y2⁢sin⁡s2dℝs⁡s≤b
636 631 635 bitrd ⊢φ∧d∈0π→∀s∈dom⁡Oℝ′Oℝ′⁡s≤b↔∀s∈dom⁡ds∈dπF⁡X+s−Y2⁢sin⁡s2dℝsds∈dπF⁡X+s−Y2⁢sin⁡s2dℝs⁡s≤b
637 636 rexbidv ⊢φ∧d∈0π→∃b∈ℝ∀s∈dom⁡Oℝ′Oℝ′⁡s≤b↔∃b∈ℝ∀s∈dom⁡ds∈dπF⁡X+s−Y2⁢sin⁡s2dℝsds∈dπF⁡X+s−Y2⁢sin⁡s2dℝs⁡s≤b
638 619 637 mpbird ⊢φ∧d∈0π→∃b∈ℝ∀s∈dom⁡Oℝ′Oℝ′⁡s≤b
639 eqid ⊢l∈ℝ+⟼∫dπO⁡s⁢sin⁡l⁢sds=l∈ℝ+⟼∫dπO⁡s⁢sin⁡l⁢sds
640 eqeq1 ⊢t=s→t=J⁡k↔s=J⁡k
641 fveq2 ⊢h=l→Q⁡h=Q⁡l
642 oveq1 ⊢h=l→h+1=l+1
643 642 fveq2d ⊢h=l→Q⁡h+1=Q⁡l+1
644 641 643 oveq12d ⊢h=l→Q⁡hQ⁡h+1=Q⁡lQ⁡l+1
645 644 sseq2d ⊢h=l→J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1↔J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1
646 645 cbvriotavw ⊢ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1=ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1
647 646 fveq2i ⊢Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1
648 647 eqeq2i ⊢J⁡k=Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1↔J⁡k=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1
649 648 a1i ⊢⊤→J⁡k=Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1↔J⁡k=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1
650 csbeq1 ⊢ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1=ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1→⦋ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1/i⦌R=⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌R
651 646 650 mp1i ⊢⊤→⦋ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1/i⦌R=⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌R
652 649 651 ifbieq1d ⊢⊤→ifJ⁡k=Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1⦋ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1/i⦌RF⁡X+J⁡k=ifJ⁡k=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌RF⁡X+J⁡k
653 652 mptru ⊢ifJ⁡k=Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1⦋ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1/i⦌RF⁡X+J⁡k=ifJ⁡k=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌RF⁡X+J⁡k
654 653 oveq1i ⊢ifJ⁡k=Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1⦋ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1/i⦌RF⁡X+J⁡k−Y=ifJ⁡k=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌RF⁡X+J⁡k−Y
655 654 oveq1i ⊢ifJ⁡k=Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1⦋ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1/i⦌RF⁡X+J⁡k−YJ⁡k=ifJ⁡k=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌RF⁡X+J⁡k−YJ⁡k
656 655 oveq1i ⊢ifJ⁡k=Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1⦋ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1/i⦌RF⁡X+J⁡k−YJ⁡k⁢J⁡k2⁢sin⁡J⁡k2=ifJ⁡k=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌RF⁡X+J⁡k−YJ⁡k⁢J⁡k2⁢sin⁡J⁡k2
657 656 a1i ⊢t=s→ifJ⁡k=Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1⦋ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1/i⦌RF⁡X+J⁡k−YJ⁡k⁢J⁡k2⁢sin⁡J⁡k2=ifJ⁡k=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌RF⁡X+J⁡k−YJ⁡k⁢J⁡k2⁢sin⁡J⁡k2
658 eqeq1 ⊢t=s→t=J⁡k+1↔s=J⁡k+1
659 646 oveq1i ⊢ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1+1=ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1
660 659 fveq2i ⊢Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1+1=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1
661 660 eqeq2i ⊢J⁡k+1=Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1+1↔J⁡k+1=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1
662 661 a1i ⊢⊤→J⁡k+1=Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1+1↔J⁡k+1=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1
663 csbeq1 ⊢ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1=ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1→⦋ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1/i⦌L=⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌L
664 646 663 mp1i ⊢⊤→⦋ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1/i⦌L=⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌L
665 662 664 ifbieq1d ⊢⊤→ifJ⁡k+1=Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1+1⦋ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1/i⦌LF⁡X+J⁡k+1=ifJ⁡k+1=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌LF⁡X+J⁡k+1
666 665 mptru ⊢ifJ⁡k+1=Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1+1⦋ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1/i⦌LF⁡X+J⁡k+1=ifJ⁡k+1=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌LF⁡X+J⁡k+1
667 666 oveq1i ⊢ifJ⁡k+1=Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1+1⦋ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1/i⦌LF⁡X+J⁡k+1−Y=ifJ⁡k+1=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌LF⁡X+J⁡k+1−Y
668 667 oveq1i ⊢ifJ⁡k+1=Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1+1⦋ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1/i⦌LF⁡X+J⁡k+1−YJ⁡k+1=ifJ⁡k+1=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌LF⁡X+J⁡k+1−YJ⁡k+1
669 668 oveq1i ⊢ifJ⁡k+1=Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1+1⦋ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1/i⦌LF⁡X+J⁡k+1−YJ⁡k+1⁢J⁡k+12⁢sin⁡J⁡k+12=ifJ⁡k+1=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌LF⁡X+J⁡k+1−YJ⁡k+1⁢J⁡k+12⁢sin⁡J⁡k+12
670 669 a1i ⊢t=s→ifJ⁡k+1=Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1+1⦋ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1/i⦌LF⁡X+J⁡k+1−YJ⁡k+1⁢J⁡k+12⁢sin⁡J⁡k+12=ifJ⁡k+1=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌LF⁡X+J⁡k+1−YJ⁡k+1⁢J⁡k+12⁢sin⁡J⁡k+12
671 fveq2 ⊢t=s→O⁡t=O⁡s
672 658 670 671 ifbieq12d ⊢t=s→ift=J⁡k+1ifJ⁡k+1=Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1+1⦋ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1/i⦌LF⁡X+J⁡k+1−YJ⁡k+1⁢J⁡k+12⁢sin⁡J⁡k+12O⁡t=ifs=J⁡k+1ifJ⁡k+1=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌LF⁡X+J⁡k+1−YJ⁡k+1⁢J⁡k+12⁢sin⁡J⁡k+12O⁡s
673 640 657 672 ifbieq12d ⊢t=s→ift=J⁡kifJ⁡k=Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1⦋ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1/i⦌RF⁡X+J⁡k−YJ⁡k⁢J⁡k2⁢sin⁡J⁡k2ift=J⁡k+1ifJ⁡k+1=Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1+1⦋ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1/i⦌LF⁡X+J⁡k+1−YJ⁡k+1⁢J⁡k+12⁢sin⁡J⁡k+12O⁡t=ifs=J⁡kifJ⁡k=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌RF⁡X+J⁡k−YJ⁡k⁢J⁡k2⁢sin⁡J⁡k2ifs=J⁡k+1ifJ⁡k+1=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌LF⁡X+J⁡k+1−YJ⁡k+1⁢J⁡k+12⁢sin⁡J⁡k+12O⁡s
674 673 cbvmptv ⊢t∈J⁡kJ⁡k+1⟼ift=J⁡kifJ⁡k=Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1⦋ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1/i⦌RF⁡X+J⁡k−YJ⁡k⁢J⁡k2⁢sin⁡J⁡k2ift=J⁡k+1ifJ⁡k+1=Q⁡ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1+1⦋ιh∈0..^M|J⁡kJ⁡k+1⊆Q⁡hQ⁡h+1/i⦌LF⁡X+J⁡k+1−YJ⁡k+1⁢J⁡k+12⁢sin⁡J⁡k+12O⁡t=s∈J⁡kJ⁡k+1⟼ifs=J⁡kifJ⁡k=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌RF⁡X+J⁡k−YJ⁡k⁢J⁡k2⁢sin⁡J⁡k2ifs=J⁡k+1ifJ⁡k+1=Q⁡ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1+1⦋ιl∈0..^M|J⁡kJ⁡k+1⊆Q⁡lQ⁡l+1/i⦌LF⁡X+J⁡k+1−YJ⁡k+1⁢J⁡k+12⁢sin⁡J⁡k+12O⁡s
675 41 43 89 143 167 168 169 191 301 306 309 310 432 638 639 674 fourierdlem73 ⊢φ∧d∈0π→∀e∈ℝ+∃j∈ℕ∀l∈j+∞∫dπO⁡s⁢sin⁡l⁢sds<e
676 breq2 ⊢e=a→∫dπO⁡s⁢sin⁡l⁢sds<e↔∫dπO⁡s⁢sin⁡l⁢sds<a
677 676 rexralbidv ⊢e=a→∃j∈ℕ∀l∈j+∞∫dπO⁡s⁢sin⁡l⁢sds<e↔∃j∈ℕ∀l∈j+∞∫dπO⁡s⁢sin⁡l⁢sds<a
678 677 cbvralvw ⊢∀e∈ℝ+∃j∈ℕ∀l∈j+∞∫dπO⁡s⁢sin⁡l⁢sds<e↔∀a∈ℝ+∃j∈ℕ∀l∈j+∞∫dπO⁡s⁢sin⁡l⁢sds<a
679 675 678 sylib ⊢φ∧d∈0π→∀a∈ℝ+∃j∈ℕ∀l∈j+∞∫dπO⁡s⁢sin⁡l⁢sds<a
680 679 adantlr ⊢φ∧e∈ℝ+∧d∈0π→∀a∈ℝ+∃j∈ℕ∀l∈j+∞∫dπO⁡s⁢sin⁡l⁢sds<a
681 rphalfcl ⊢e∈ℝ+→e2∈ℝ+
682 681 ad2antlr ⊢φ∧e∈ℝ+∧d∈0π→e2∈ℝ+
683 breq2 ⊢a=e2→∫dπO⁡s⁢sin⁡l⁢sds<a↔∫dπO⁡s⁢sin⁡l⁢sds<e2
684 683 rexralbidv ⊢a=e2→∃j∈ℕ∀l∈j+∞∫dπO⁡s⁢sin⁡l⁢sds<a↔∃j∈ℕ∀l∈j+∞∫dπO⁡s⁢sin⁡l⁢sds<e2
685 684 rspccva ⊢∀a∈ℝ+∃j∈ℕ∀l∈j+∞∫dπO⁡s⁢sin⁡l⁢sds<a∧e2∈ℝ+→∃j∈ℕ∀l∈j+∞∫dπO⁡s⁢sin⁡l⁢sds<e2
686 680 682 685 syl2anc ⊢φ∧e∈ℝ+∧d∈0π→∃j∈ℕ∀l∈j+∞∫dπO⁡s⁢sin⁡l⁢sds<e2
687 156 a1i ⊢φ∧d∈0π→dπ⊆dπ
688 687 sselda ⊢φ∧d∈0π∧s∈dπ→s∈dπ
689 688 355 syl ⊢φ∧d∈0π∧s∈dπ→U↾dπ⁡s=U⁡s
690 353 689 eqtr2id ⊢φ∧d∈0π∧s∈dπ→U⁡s=O⁡s
691 690 oveq1d ⊢φ∧d∈0π∧s∈dπ→U⁡s⁢sin⁡l⁢s=O⁡s⁢sin⁡l⁢s
692 691 itgeq2dv ⊢φ∧d∈0π→∫dπU⁡s⁢sin⁡l⁢sds=∫dπO⁡s⁢sin⁡l⁢sds
693 692 adantr ⊢φ∧d∈0π∧∫dπO⁡s⁢sin⁡l⁢sds<e2→∫dπU⁡s⁢sin⁡l⁢sds=∫dπO⁡s⁢sin⁡l⁢sds
694 693 fveq2d ⊢φ∧d∈0π∧∫dπO⁡s⁢sin⁡l⁢sds<e2→∫dπU⁡s⁢sin⁡l⁢sds=∫dπO⁡s⁢sin⁡l⁢sds
695 simpr ⊢φ∧d∈0π∧∫dπO⁡s⁢sin⁡l⁢sds<e2→∫dπO⁡s⁢sin⁡l⁢sds<e2
696 694 695 eqbrtrd ⊢φ∧d∈0π∧∫dπO⁡s⁢sin⁡l⁢sds<e2→∫dπU⁡s⁢sin⁡l⁢sds<e2
697 696 ex ⊢φ∧d∈0π→∫dπO⁡s⁢sin⁡l⁢sds<e2→∫dπU⁡s⁢sin⁡l⁢sds<e2
698 697 adantlr ⊢φ∧e∈ℝ+∧d∈0π→∫dπO⁡s⁢sin⁡l⁢sds<e2→∫dπU⁡s⁢sin⁡l⁢sds<e2
699 698 ralimdv ⊢φ∧e∈ℝ+∧d∈0π→∀l∈j+∞∫dπO⁡s⁢sin⁡l⁢sds<e2→∀l∈j+∞∫dπU⁡s⁢sin⁡l⁢sds<e2
700 699 reximdv ⊢φ∧e∈ℝ+∧d∈0π→∃j∈ℕ∀l∈j+∞∫dπO⁡s⁢sin⁡l⁢sds<e2→∃j∈ℕ∀l∈j+∞∫dπU⁡s⁢sin⁡l⁢sds<e2
701 686 700 mpd ⊢φ∧e∈ℝ+∧d∈0π→∃j∈ℕ∀l∈j+∞∫dπU⁡s⁢sin⁡l⁢sds<e2
702 701 adantr ⊢φ∧e∈ℝ+∧d∈0π∧∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2→∃j∈ℕ∀l∈j+∞∫dπU⁡s⁢sin⁡l⁢sds<e2
703 nfv ⊢Ⅎkφ∧e∈ℝ+∧d∈0π
704 nfra1 ⊢Ⅎk∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2
705 703 704 nfan ⊢Ⅎkφ∧e∈ℝ+∧d∈0π∧∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2
706 nfv ⊢Ⅎkj∈ℕ
707 705 706 nfan ⊢Ⅎkφ∧e∈ℝ+∧d∈0π∧∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧j∈ℕ
708 nfv ⊢Ⅎk∀l∈j+∞∫dπU⁡s⁢sin⁡l⁢sds<e2
709 707 708 nfan ⊢Ⅎkφ∧e∈ℝ+∧d∈0π∧∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧j∈ℕ∧∀l∈j+∞∫dπU⁡s⁢sin⁡l⁢sds<e2
710 simpll ⊢φ∧e∈ℝ+∧d∈0π∧j∈ℕ∧k∈ℤ≥j→φ∧e∈ℝ+∧d∈0π
711 eluznn ⊢j∈ℕ∧k∈ℤ≥j→k∈ℕ
712 711 adantll ⊢φ∧e∈ℝ+∧d∈0π∧j∈ℕ∧k∈ℤ≥j→k∈ℕ
713 710 712 jca ⊢φ∧e∈ℝ+∧d∈0π∧j∈ℕ∧k∈ℤ≥j→φ∧e∈ℝ+∧d∈0π∧k∈ℕ
714 713 adantllr ⊢φ∧e∈ℝ+∧d∈0π∧∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧j∈ℕ∧k∈ℤ≥j→φ∧e∈ℝ+∧d∈0π∧k∈ℕ
715 simpllr ⊢φ∧e∈ℝ+∧d∈0π∧∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧j∈ℕ∧k∈ℤ≥j→∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2
716 711 adantll ⊢φ∧e∈ℝ+∧d∈0π∧∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧j∈ℕ∧k∈ℤ≥j→k∈ℕ
717 rspa ⊢∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧k∈ℕ→∫0dU⁡s⁢sin⁡k+12⁢sds<e2
718 715 716 717 syl2anc ⊢φ∧e∈ℝ+∧d∈0π∧∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧j∈ℕ∧k∈ℤ≥j→∫0dU⁡s⁢sin⁡k+12⁢sds<e2
719 714 718 jca ⊢φ∧e∈ℝ+∧d∈0π∧∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧j∈ℕ∧k∈ℤ≥j→φ∧e∈ℝ+∧d∈0π∧k∈ℕ∧∫0dU⁡s⁢sin⁡k+12⁢sds<e2
720 719 adantlr ⊢φ∧e∈ℝ+∧d∈0π∧∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧j∈ℕ∧∀l∈j+∞∫dπU⁡s⁢sin⁡l⁢sds<e2∧k∈ℤ≥j→φ∧e∈ℝ+∧d∈0π∧k∈ℕ∧∫0dU⁡s⁢sin⁡k+12⁢sds<e2
721 nnre ⊢j∈ℕ→j∈ℝ
722 721 rexrd ⊢j∈ℕ→j∈ℝ*
723 722 adantr ⊢j∈ℕ∧k∈ℤ≥j→j∈ℝ*
724 50 a1i ⊢j∈ℕ∧k∈ℤ≥j→+∞∈ℝ*
725 eluzelre ⊢k∈ℤ≥j→k∈ℝ
726 halfre ⊢12∈ℝ
727 726 a1i ⊢k∈ℤ≥j→12∈ℝ
728 725 727 readdcld ⊢k∈ℤ≥j→k+12∈ℝ
729 728 adantl ⊢j∈ℕ∧k∈ℤ≥j→k+12∈ℝ
730 721 adantr ⊢j∈ℕ∧k∈ℤ≥j→j∈ℝ
731 725 adantl ⊢j∈ℕ∧k∈ℤ≥j→k∈ℝ
732 eluzle ⊢k∈ℤ≥j→j≤k
733 732 adantl ⊢j∈ℕ∧k∈ℤ≥j→j≤k
734 halfgt0 ⊢0<12
735 734 a1i ⊢j∈ℕ∧k∈ℤ≥j→0<12
736 726 a1i ⊢j∈ℕ∧k∈ℤ≥j→12∈ℝ
737 736 731 ltaddposd ⊢j∈ℕ∧k∈ℤ≥j→0<12↔k<k+12
738 735 737 mpbid ⊢j∈ℕ∧k∈ℤ≥j→k<k+12
739 730 731 729 733 738 lelttrd ⊢j∈ℕ∧k∈ℤ≥j→j<k+12
740 729 ltpnfd ⊢j∈ℕ∧k∈ℤ≥j→k+12<+∞
741 723 724 729 739 740 eliood ⊢j∈ℕ∧k∈ℤ≥j→k+12∈j+∞
742 741 adantlr ⊢j∈ℕ∧∀l∈j+∞∫dπU⁡s⁢sin⁡l⁢sds<e2∧k∈ℤ≥j→k+12∈j+∞
743 simplr ⊢j∈ℕ∧∀l∈j+∞∫dπU⁡s⁢sin⁡l⁢sds<e2∧k∈ℤ≥j→∀l∈j+∞∫dπU⁡s⁢sin⁡l⁢sds<e2
744 oveq1 ⊢l=k+12→l⁢s=k+12⁢s
745 744 fveq2d ⊢l=k+12→sin⁡l⁢s=sin⁡k+12⁢s
746 745 oveq2d ⊢l=k+12→U⁡s⁢sin⁡l⁢s=U⁡s⁢sin⁡k+12⁢s
747 746 adantr ⊢l=k+12∧s∈dπ→U⁡s⁢sin⁡l⁢s=U⁡s⁢sin⁡k+12⁢s
748 747 itgeq2dv ⊢l=k+12→∫dπU⁡s⁢sin⁡l⁢sds=∫dπU⁡s⁢sin⁡k+12⁢sds
749 748 fveq2d ⊢l=k+12→∫dπU⁡s⁢sin⁡l⁢sds=∫dπU⁡s⁢sin⁡k+12⁢sds
750 749 breq1d ⊢l=k+12→∫dπU⁡s⁢sin⁡l⁢sds<e2↔∫dπU⁡s⁢sin⁡k+12⁢sds<e2
751 750 rspcv ⊢k+12∈j+∞→∀l∈j+∞∫dπU⁡s⁢sin⁡l⁢sds<e2→∫dπU⁡s⁢sin⁡k+12⁢sds<e2
752 742 743 751 sylc ⊢j∈ℕ∧∀l∈j+∞∫dπU⁡s⁢sin⁡l⁢sds<e2∧k∈ℤ≥j→∫dπU⁡s⁢sin⁡k+12⁢sds<e2
753 752 adantlll ⊢φ∧e∈ℝ+∧d∈0π∧∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧j∈ℕ∧∀l∈j+∞∫dπU⁡s⁢sin⁡l⁢sds<e2∧k∈ℤ≥j→∫dπU⁡s⁢sin⁡k+12⁢sds<e2
754 720 753 31 sylanbrc ⊢φ∧e∈ℝ+∧d∈0π∧∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧j∈ℕ∧∀l∈j+∞∫dπU⁡s⁢sin⁡l⁢sds<e2∧k∈ℤ≥j→χ
755 0red ⊢χ→0∈ℝ
756 42 a1i ⊢χ→π∈ℝ
757 ioossicc ⊢0π⊆0π
758 31 biimpi ⊢χ→φ∧e∈ℝ+∧d∈0π∧k∈ℕ∧∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧∫dπU⁡s⁢sin⁡k+12⁢sds<e2
759 simp-4r ⊢φ∧e∈ℝ+∧d∈0π∧k∈ℕ∧∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧∫dπU⁡s⁢sin⁡k+12⁢sds<e2→d∈0π
760 758 759 syl ⊢χ→d∈0π
761 757 760 sselid ⊢χ→d∈0π
762 simp-5l ⊢φ∧e∈ℝ+∧d∈0π∧k∈ℕ∧∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧∫dπU⁡s⁢sin⁡k+12⁢sds<e2→φ
763 758 762 syl ⊢χ→φ
764 65 adantr ⊢φ∧s∈0π→U:−ππ⟶ℝ
765 70 rexri ⊢−π∈ℝ*
766 0re ⊢0∈ℝ
767 70 766 74 ltleii ⊢−π≤0
768 iooss1 ⊢−π∈ℝ*∧−π≤0→0π⊆−ππ
769 765 767 768 mp2an ⊢0π⊆−ππ
770 ioossicc ⊢−ππ⊆−ππ
771 769 770 sstri ⊢0π⊆−ππ
772 771 sseli ⊢s∈0π→s∈−ππ
773 772 adantl ⊢φ∧s∈0π→s∈−ππ
774 764 773 ffvelcdmd ⊢φ∧s∈0π→U⁡s∈ℝ
775 763 774 sylan ⊢χ∧s∈0π→U⁡s∈ℝ
776 simpllr ⊢φ∧e∈ℝ+∧d∈0π∧k∈ℕ∧∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧∫dπU⁡s⁢sin⁡k+12⁢sds<e2→k∈ℕ
777 758 776 syl ⊢χ→k∈ℕ
778 777 nnred ⊢χ→k∈ℝ
779 726 a1i ⊢χ→12∈ℝ
780 778 779 readdcld ⊢χ→k+12∈ℝ
781 780 adantr ⊢χ∧s∈0π→k+12∈ℝ
782 elioore ⊢s∈0π→s∈ℝ
783 782 adantl ⊢χ∧s∈0π→s∈ℝ
784 781 783 remulcld ⊢χ∧s∈0π→k+12⁢s∈ℝ
785 784 resincld ⊢χ∧s∈0π→sin⁡k+12⁢s∈ℝ
786 775 785 remulcld ⊢χ∧s∈0π→U⁡s⁢sin⁡k+12⁢s∈ℝ
787 786 recnd ⊢χ∧s∈0π→U⁡s⁢sin⁡k+12⁢s∈ℂ
788 76 a1i ⊢χ→0∈ℝ*
789 77 a1i ⊢χ→π∈ℝ*
790 755 leidd ⊢χ→0≤0
791 ioossre ⊢0π⊆ℝ
792 791 760 sselid ⊢χ→d∈ℝ
793 788 789 760 123 syl3anc ⊢χ→d<π
794 792 756 793 ltled ⊢χ→d≤π
795 ioossioo ⊢0∈ℝ*∧π∈ℝ*∧0≤0∧d≤π→0d⊆0π
796 788 789 790 794 795 syl22anc ⊢χ→0d⊆0π
797 ioombl ⊢0d∈dom⁡vol
798 797 a1i ⊢χ→0d∈dom⁡vol
799 eleq1 ⊢n=k→n∈ℕ↔k∈ℕ
800 799 anbi2d ⊢n=k→φ∧n∈ℕ↔φ∧k∈ℕ
801 simpl ⊢n=k∧s∈0π→n=k
802 801 oveq1d ⊢n=k∧s∈0π→n+12=k+12
803 802 oveq1d ⊢n=k∧s∈0π→n+12⁢s=k+12⁢s
804 803 fveq2d ⊢n=k∧s∈0π→sin⁡n+12⁢s=sin⁡k+12⁢s
805 804 oveq2d ⊢n=k∧s∈0π→U⁡s⁢sin⁡n+12⁢s=U⁡s⁢sin⁡k+12⁢s
806 805 mpteq2dva ⊢n=k→s∈0π⟼U⁡s⁢sin⁡n+12⁢s=s∈0π⟼U⁡s⁢sin⁡k+12⁢s
807 806 eleq1d ⊢n=k→s∈0π⟼U⁡s⁢sin⁡n+12⁢s∈𝐿1↔s∈0π⟼U⁡s⁢sin⁡k+12⁢s∈𝐿1
808 800 807 imbi12d ⊢n=k→φ∧n∈ℕ→s∈0π⟼U⁡s⁢sin⁡n+12⁢s∈𝐿1↔φ∧k∈ℕ→s∈0π⟼U⁡s⁢sin⁡k+12⁢s∈𝐿1
809 771 a1i ⊢φ∧n∈ℕ→0π⊆−ππ
810 ioombl ⊢0π∈dom⁡vol
811 810 a1i ⊢φ∧n∈ℕ→0π∈dom⁡vol
812 65 ffvelcdmda ⊢φ∧s∈−ππ→U⁡s∈ℝ
813 812 adantlr ⊢φ∧n∈ℕ∧s∈−ππ→U⁡s∈ℝ
814 nnre ⊢n∈ℕ→n∈ℝ
815 readdcl ⊢n∈ℝ∧12∈ℝ→n+12∈ℝ
816 814 726 815 sylancl ⊢n∈ℕ→n+12∈ℝ
817 816 adantr ⊢n∈ℕ∧s∈−ππ→n+12∈ℝ
818 simpr ⊢n∈ℕ∧s∈−ππ→s∈−ππ
819 228 818 sselid ⊢n∈ℕ∧s∈−ππ→s∈ℝ
820 817 819 remulcld ⊢n∈ℕ∧s∈−ππ→n+12⁢s∈ℝ
821 820 resincld ⊢n∈ℕ∧s∈−ππ→sin⁡n+12⁢s∈ℝ
822 821 adantll ⊢φ∧n∈ℕ∧s∈−ππ→sin⁡n+12⁢s∈ℝ
823 813 822 remulcld ⊢φ∧n∈ℕ∧s∈−ππ→U⁡s⁢sin⁡n+12⁢s∈ℝ
824 16 fvmpt2 ⊢s∈−ππ∧sin⁡n+12⁢s∈ℝ→S⁡s=sin⁡n+12⁢s
825 818 821 824 syl2anc ⊢n∈ℕ∧s∈−ππ→S⁡s=sin⁡n+12⁢s
826 825 adantll ⊢φ∧n∈ℕ∧s∈−ππ→S⁡s=sin⁡n+12⁢s
827 826 oveq2d ⊢φ∧n∈ℕ∧s∈−ππ→U⁡s⁢S⁡s=U⁡s⁢sin⁡n+12⁢s
828 827 mpteq2dva ⊢φ∧n∈ℕ→s∈−ππ⟼U⁡s⁢S⁡s=s∈−ππ⟼U⁡s⁢sin⁡n+12⁢s
829 17 828 eqtr2id ⊢φ∧n∈ℕ→s∈−ππ⟼U⁡s⁢sin⁡n+12⁢s=G
830 1 adantr ⊢φ∧n∈ℕ→F:ℝ⟶ℝ
831 6 adantr ⊢φ∧n∈ℕ→X∈ran⁡V
832 20 adantr ⊢φ∧n∈ℕ→Y∈F↾X+∞limℂX
833 21 adantr ⊢φ∧n∈ℕ→W∈F↾−∞XlimℂX
834 814 adantl ⊢φ∧n∈ℕ→n∈ℝ
835 4 adantr ⊢φ∧n∈ℕ→M∈ℕ
836 5 adantr ⊢φ∧n∈ℕ→V∈P⁡M
837 7 adantlr ⊢φ∧n∈ℕ∧i∈0..^M→F↾V⁡iV⁡i+1:V⁡iV⁡i+1⟶cnℂ
838 11 adantlr ⊢φ∧n∈ℕ∧i∈0..^M→R∈F↾V⁡iV⁡i+1limℂV⁡i
839 12 adantlr ⊢φ∧n∈ℕ∧i∈0..^M→L∈F↾V⁡iV⁡i+1limℂV⁡i+1
840 eqid ⊢m∈ℕ⟼p∈ℝ0…m|p⁡0=−π∧p⁡m=π∧∀i∈0..^mp⁡i<p⁡i+1=m∈ℕ⟼p∈ℝ0…m|p⁡0=−π∧p⁡m=π∧∀i∈0..^mp⁡i<p⁡i+1
841 eqid ⊢ℝDF=ℝDF
842 601 adantlr ⊢φ∧n∈ℕ∧i∈0..^M→Fℝ′↾V⁡iV⁡i+1:V⁡iV⁡i+1⟶ℝ
843 22 adantr ⊢φ∧n∈ℕ→A∈Fℝ′↾−∞XlimℂX
844 23 adantr ⊢φ∧n∈ℕ→B∈Fℝ′↾X+∞limℂX
845 3 830 831 832 833 13 14 15 834 16 17 835 836 837 838 839 29 840 841 842 843 844 fourierdlem88 ⊢φ∧n∈ℕ→G∈𝐿1
846 829 845 eqeltrd ⊢φ∧n∈ℕ→s∈−ππ⟼U⁡s⁢sin⁡n+12⁢s∈𝐿1
847 809 811 823 846 iblss ⊢φ∧n∈ℕ→s∈0π⟼U⁡s⁢sin⁡n+12⁢s∈𝐿1
848 808 847 chvarvv ⊢φ∧k∈ℕ→s∈0π⟼U⁡s⁢sin⁡k+12⁢s∈𝐿1
849 763 777 848 syl2anc ⊢χ→s∈0π⟼U⁡s⁢sin⁡k+12⁢s∈𝐿1
850 796 798 786 849 iblss ⊢χ→s∈0d⟼U⁡s⁢sin⁡k+12⁢s∈𝐿1
851 788 789 760 78 syl3anc ⊢χ→0<d
852 755 792 851 ltled ⊢χ→0≤d
853 756 leidd ⊢χ→π≤π
854 ioossioo ⊢0∈ℝ*∧π∈ℝ*∧0≤d∧π≤π→dπ⊆0π
855 788 789 852 853 854 syl22anc ⊢χ→dπ⊆0π
856 ioombl ⊢dπ∈dom⁡vol
857 856 a1i ⊢χ→dπ∈dom⁡vol
858 855 857 786 849 iblss ⊢χ→s∈dπ⟼U⁡s⁢sin⁡k+12⁢s∈𝐿1
859 755 756 761 787 850 858 itgsplitioo ⊢χ→∫0πU⁡s⁢sin⁡k+12⁢sds=∫0dU⁡s⁢sin⁡k+12⁢sds+∫dπU⁡s⁢sin⁡k+12⁢sds
860 859 fveq2d ⊢χ→∫0πU⁡s⁢sin⁡k+12⁢sds=∫0dU⁡s⁢sin⁡k+12⁢sds+∫dπU⁡s⁢sin⁡k+12⁢sds
861 796 sselda ⊢χ∧s∈0d→s∈0π
862 861 786 syldan ⊢χ∧s∈0d→U⁡s⁢sin⁡k+12⁢s∈ℝ
863 862 850 itgcl ⊢χ→∫0dU⁡s⁢sin⁡k+12⁢sds∈ℂ
864 855 sselda ⊢χ∧s∈dπ→s∈0π
865 864 786 syldan ⊢χ∧s∈dπ→U⁡s⁢sin⁡k+12⁢s∈ℝ
866 865 858 itgcl ⊢χ→∫dπU⁡s⁢sin⁡k+12⁢sds∈ℂ
867 863 866 addcld ⊢χ→∫0dU⁡s⁢sin⁡k+12⁢sds+∫dπU⁡s⁢sin⁡k+12⁢sds∈ℂ
868 867 abscld ⊢χ→∫0dU⁡s⁢sin⁡k+12⁢sds+∫dπU⁡s⁢sin⁡k+12⁢sds∈ℝ
869 863 abscld ⊢χ→∫0dU⁡s⁢sin⁡k+12⁢sds∈ℝ
870 866 abscld ⊢χ→∫dπU⁡s⁢sin⁡k+12⁢sds∈ℝ
871 869 870 readdcld ⊢χ→∫0dU⁡s⁢sin⁡k+12⁢sds+∫dπU⁡s⁢sin⁡k+12⁢sds∈ℝ
872 simp-5r ⊢φ∧e∈ℝ+∧d∈0π∧k∈ℕ∧∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧∫dπU⁡s⁢sin⁡k+12⁢sds<e2→e∈ℝ+
873 758 872 syl ⊢χ→e∈ℝ+
874 873 rpred ⊢χ→e∈ℝ
875 863 866 abstrid ⊢χ→∫0dU⁡s⁢sin⁡k+12⁢sds+∫dπU⁡s⁢sin⁡k+12⁢sds≤∫0dU⁡s⁢sin⁡k+12⁢sds+∫dπU⁡s⁢sin⁡k+12⁢sds
876 758 simplrd ⊢χ→∫0dU⁡s⁢sin⁡k+12⁢sds<e2
877 758 simprd ⊢χ→∫dπU⁡s⁢sin⁡k+12⁢sds<e2
878 869 870 874 876 877 lt2halvesd ⊢χ→∫0dU⁡s⁢sin⁡k+12⁢sds+∫dπU⁡s⁢sin⁡k+12⁢sds<e
879 868 871 874 875 878 lelttrd ⊢χ→∫0dU⁡s⁢sin⁡k+12⁢sds+∫dπU⁡s⁢sin⁡k+12⁢sds<e
880 860 879 eqbrtrd ⊢χ→∫0πU⁡s⁢sin⁡k+12⁢sds<e
881 754 880 syl ⊢φ∧e∈ℝ+∧d∈0π∧∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧j∈ℕ∧∀l∈j+∞∫dπU⁡s⁢sin⁡l⁢sds<e2∧k∈ℤ≥j→∫0πU⁡s⁢sin⁡k+12⁢sds<e
882 881 ex ⊢φ∧e∈ℝ+∧d∈0π∧∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧j∈ℕ∧∀l∈j+∞∫dπU⁡s⁢sin⁡l⁢sds<e2→k∈ℤ≥j→∫0πU⁡s⁢sin⁡k+12⁢sds<e
883 709 882 ralrimi ⊢φ∧e∈ℝ+∧d∈0π∧∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧j∈ℕ∧∀l∈j+∞∫dπU⁡s⁢sin⁡l⁢sds<e2→∀k∈ℤ≥j∫0πU⁡s⁢sin⁡k+12⁢sds<e
884 883 ex ⊢φ∧e∈ℝ+∧d∈0π∧∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2∧j∈ℕ→∀l∈j+∞∫dπU⁡s⁢sin⁡l⁢sds<e2→∀k∈ℤ≥j∫0πU⁡s⁢sin⁡k+12⁢sds<e
885 884 reximdva ⊢φ∧e∈ℝ+∧d∈0π∧∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2→∃j∈ℕ∀l∈j+∞∫dπU⁡s⁢sin⁡l⁢sds<e2→∃j∈ℕ∀k∈ℤ≥j∫0πU⁡s⁢sin⁡k+12⁢sds<e
886 702 885 mpd ⊢φ∧e∈ℝ+∧d∈0π∧∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2→∃j∈ℕ∀k∈ℤ≥j∫0πU⁡s⁢sin⁡k+12⁢sds<e
887 pipos ⊢0<π
888 70 766 42 lttri ⊢−π<0∧0<π→−π<π
889 74 887 888 mp2an ⊢−π<π
890 70 42 889 ltleii ⊢−π≤π
891 890 a1i ⊢φ→−π≤π
892 3 fourierdlem2 ⊢M∈ℕ→V∈P⁡M↔V∈ℝ0…M∧V⁡0=-π+X∧V⁡M=π+X∧∀i∈0..^MV⁡i<V⁡i+1
893 4 892 syl ⊢φ→V∈P⁡M↔V∈ℝ0…M∧V⁡0=-π+X∧V⁡M=π+X∧∀i∈0..^MV⁡i<V⁡i+1
894 5 893 mpbid ⊢φ→V∈ℝ0…M∧V⁡0=-π+X∧V⁡M=π+X∧∀i∈0..^MV⁡i<V⁡i+1
895 894 simpld ⊢φ→V∈ℝ0…M
896 elmapi ⊢V∈ℝ0…M→V:0…M⟶ℝ
897 895 896 syl ⊢φ→V:0…M⟶ℝ
898 897 ffvelcdmda ⊢φ∧i∈0…M→V⁡i∈ℝ
899 2 adantr ⊢φ∧i∈0…M→X∈ℝ
900 898 899 resubcld ⊢φ∧i∈0…M→V⁡i−X∈ℝ
901 900 29 fmptd ⊢φ→Q:0…M⟶ℝ
902 29 a1i ⊢φ→Q=i∈0…M⟼V⁡i−X
903 fveq2 ⊢i=0→V⁡i=V⁡0
904 903 oveq1d ⊢i=0→V⁡i−X=V⁡0−X
905 904 adantl ⊢φ∧i=0→V⁡i−X=V⁡0−X
906 4 nnnn0d ⊢φ→M∈ℕ0
907 nn0uz ⊢ℕ0=ℤ≥0
908 906 907 eleqtrdi ⊢φ→M∈ℤ≥0
909 eluzfz1 ⊢M∈ℤ≥0→0∈0…M
910 908 909 syl ⊢φ→0∈0…M
911 897 910 ffvelcdmd ⊢φ→V⁡0∈ℝ
912 911 2 resubcld ⊢φ→V⁡0−X∈ℝ
913 902 905 910 912 fvmptd ⊢φ→Q⁡0=V⁡0−X
914 894 simprd ⊢φ→V⁡0=-π+X∧V⁡M=π+X∧∀i∈0..^MV⁡i<V⁡i+1
915 914 simplld ⊢φ→V⁡0=-π+X
916 915 oveq1d ⊢φ→V⁡0−X=−π+X-X
917 454 recnd ⊢φ→−π∈ℂ
918 2 recnd ⊢φ→X∈ℂ
919 917 918 pncand ⊢φ→−π+X-X=−π
920 913 916 919 3eqtrd ⊢φ→Q⁡0=−π
921 454 456 2 3 840 4 5 29 fourierdlem14 ⊢φ→Q∈m∈ℕ⟼p∈ℝ0…m|p⁡0=−π∧p⁡m=π∧∀i∈0..^mp⁡i<p⁡i+1⁡M
922 840 fourierdlem2 ⊢M∈ℕ→Q∈m∈ℕ⟼p∈ℝ0…m|p⁡0=−π∧p⁡m=π∧∀i∈0..^mp⁡i<p⁡i+1⁡M↔Q∈ℝ0…M∧Q⁡0=−π∧Q⁡M=π∧∀i∈0..^MQ⁡i<Q⁡i+1
923 4 922 syl ⊢φ→Q∈m∈ℕ⟼p∈ℝ0…m|p⁡0=−π∧p⁡m=π∧∀i∈0..^mp⁡i<p⁡i+1⁡M↔Q∈ℝ0…M∧Q⁡0=−π∧Q⁡M=π∧∀i∈0..^MQ⁡i<Q⁡i+1
924 921 923 mpbid ⊢φ→Q∈ℝ0…M∧Q⁡0=−π∧Q⁡M=π∧∀i∈0..^MQ⁡i<Q⁡i+1
925 924 simprd ⊢φ→Q⁡0=−π∧Q⁡M=π∧∀i∈0..^MQ⁡i<Q⁡i+1
926 925 simplrd ⊢φ→Q⁡M=π
927 925 simprd ⊢φ→∀i∈0..^MQ⁡i<Q⁡i+1
928 927 r19.21bi ⊢φ∧i∈0..^M→Q⁡i<Q⁡i+1
929 1 adantr ⊢φ∧i∈0..^M→F:ℝ⟶ℝ
930 840 4 921 fourierdlem15 ⊢φ→Q:0…M⟶−ππ
931 930 adantr ⊢φ∧i∈0..^M→Q:0…M⟶−ππ
932 elfzofz ⊢i∈0..^M→i∈0…M
933 932 adantl ⊢φ∧i∈0..^M→i∈0…M
934 931 933 ffvelcdmd ⊢φ∧i∈0..^M→Q⁡i∈−ππ
935 fzofzp1 ⊢i∈0..^M→i+1∈0…M
936 935 adantl ⊢φ∧i∈0..^M→i+1∈0…M
937 931 936 ffvelcdmd ⊢φ∧i∈0..^M→Q⁡i+1∈−ππ
938 2 adantr ⊢φ∧i∈0..^M→X∈ℝ
939 ffn ⊢V:0…M⟶ℝ→VFn0…M
940 895 896 939 3syl ⊢φ→VFn0…M
941 fvelrnb ⊢VFn0…M→X∈ran⁡V↔∃i∈0…MV⁡i=X
942 940 941 syl ⊢φ→X∈ran⁡V↔∃i∈0…MV⁡i=X
943 6 942 mpbid ⊢φ→∃i∈0…MV⁡i=X
944 oveq1 ⊢V⁡i=X→V⁡i−X=X−X
945 944 adantl ⊢φ∧i∈0…M∧V⁡i=X→V⁡i−X=X−X
946 918 subidd ⊢φ→X−X=0
947 946 ad2antrr ⊢φ∧i∈0…M∧V⁡i=X→X−X=0
948 945 947 eqtr2d ⊢φ∧i∈0…M∧V⁡i=X→0=V⁡i−X
949 948 ex ⊢φ∧i∈0…M→V⁡i=X→0=V⁡i−X
950 949 reximdva ⊢φ→∃i∈0…MV⁡i=X→∃i∈0…M0=V⁡i−X
951 943 950 mpd ⊢φ→∃i∈0…M0=V⁡i−X
952 29 elrnmpt ⊢0∈ℝ→0∈ran⁡Q↔∃i∈0…M0=V⁡i−X
953 766 952 ax-mp ⊢0∈ran⁡Q↔∃i∈0…M0=V⁡i−X
954 951 953 sylibr ⊢φ→0∈ran⁡Q
955 840 4 921 954 fourierdlem12 ⊢φ∧i∈0..^M→¬0∈Q⁡iQ⁡i+1
956 897 adantr ⊢φ∧i∈0..^M→V:0…M⟶ℝ
957 956 933 ffvelcdmd ⊢φ∧i∈0..^M→V⁡i∈ℝ
958 957 938 resubcld ⊢φ∧i∈0..^M→V⁡i−X∈ℝ
959 29 fvmpt2 ⊢i∈0…M∧V⁡i−X∈ℝ→Q⁡i=V⁡i−X
960 933 958 959 syl2anc ⊢φ∧i∈0..^M→Q⁡i=V⁡i−X
961 960 oveq1d ⊢φ∧i∈0..^M→Q⁡i+X=V⁡i-X+X
962 957 recnd ⊢φ∧i∈0..^M→V⁡i∈ℂ
963 918 adantr ⊢φ∧i∈0..^M→X∈ℂ
964 962 963 npcand ⊢φ∧i∈0..^M→V⁡i-X+X=V⁡i
965 961 964 eqtrd ⊢φ∧i∈0..^M→Q⁡i+X=V⁡i
966 fveq2 ⊢j=i→V⁡j=V⁡i
967 966 oveq1d ⊢j=i→V⁡j−X=V⁡i−X
968 967 cbvmptv ⊢j∈0…M⟼V⁡j−X=i∈0…M⟼V⁡i−X
969 29 968 eqtr4i ⊢Q=j∈0…M⟼V⁡j−X
970 969 a1i ⊢φ∧i∈0..^M→Q=j∈0…M⟼V⁡j−X
971 fveq2 ⊢j=i+1→V⁡j=V⁡i+1
972 971 oveq1d ⊢j=i+1→V⁡j−X=V⁡i+1−X
973 972 adantl ⊢φ∧i∈0..^M∧j=i+1→V⁡j−X=V⁡i+1−X
974 956 936 ffvelcdmd ⊢φ∧i∈0..^M→V⁡i+1∈ℝ
975 974 938 resubcld ⊢φ∧i∈0..^M→V⁡i+1−X∈ℝ
976 970 973 936 975 fvmptd ⊢φ∧i∈0..^M→Q⁡i+1=V⁡i+1−X
977 976 oveq1d ⊢φ∧i∈0..^M→Q⁡i+1+X=V⁡i+1-X+X
978 974 recnd ⊢φ∧i∈0..^M→V⁡i+1∈ℂ
979 978 963 npcand ⊢φ∧i∈0..^M→V⁡i+1-X+X=V⁡i+1
980 977 979 eqtrd ⊢φ∧i∈0..^M→Q⁡i+1+X=V⁡i+1
981 965 980 oveq12d ⊢φ∧i∈0..^M→Q⁡i+XQ⁡i+1+X=V⁡iV⁡i+1
982 981 reseq2d ⊢φ∧i∈0..^M→F↾Q⁡i+XQ⁡i+1+X=F↾V⁡iV⁡i+1
983 981 oveq1d ⊢φ∧i∈0..^M→Q⁡i+XQ⁡i+1+X⟶cnℂ=V⁡iV⁡i+1⟶cnℂ
984 7 982 983 3eltr4d ⊢φ∧i∈0..^M→F↾Q⁡i+XQ⁡i+1+X:Q⁡i+XQ⁡i+1+X⟶cnℂ
985 54 adantr ⊢φ∧i∈0..^M→Y∈ℝ
986 64 adantr ⊢φ∧i∈0..^M→W∈ℝ
987 929 934 937 938 955 984 985 986 13 fourierdlem40 ⊢φ∧i∈0..^M→H↾Q⁡iQ⁡i+1:Q⁡iQ⁡i+1⟶cnℂ
988 id ⊢Fℝ′↾V⁡iV⁡i+1:V⁡iV⁡i+1⟶ℝ→Fℝ′↾V⁡iV⁡i+1:V⁡iV⁡i+1⟶ℝ
989 66 a1i ⊢Fℝ′↾V⁡iV⁡i+1:V⁡iV⁡i+1⟶ℝ→ℝ⊆ℂ
990 988 989 fssd ⊢Fℝ′↾V⁡iV⁡i+1:V⁡iV⁡i+1⟶ℝ→Fℝ′↾V⁡iV⁡i+1:V⁡iV⁡i+1⟶ℂ
991 9 600 990 3syl ⊢φ∧i∈0..^M→Fℝ′↾V⁡iV⁡i+1:V⁡iV⁡i+1⟶ℂ
992 eqid ⊢ifV⁡i=XBR−ifV⁡i<XWYQ⁡i=ifV⁡i=XBR−ifV⁡i<XWYQ⁡i
993 2 3 1 6 20 64 13 4 5 11 29 840 841 991 23 992 fourierdlem75 ⊢φ∧i∈0..^M→ifV⁡i=XBR−ifV⁡i<XWYQ⁡i∈H↾Q⁡iQ⁡i+1limℂQ⁡i
994 eqid ⊢ifV⁡i+1=XAL−ifV⁡i+1<XWYQ⁡i+1=ifV⁡i+1=XAL−ifV⁡i+1<XWYQ⁡i+1
995 2 3 1 6 54 21 13 4 5 12 29 840 841 601 22 994 fourierdlem74 ⊢φ∧i∈0..^M→ifV⁡i+1=XAL−ifV⁡i+1<XWYQ⁡i+1∈H↾Q⁡iQ⁡i+1limℂQ⁡i+1
996 fveq2 ⊢j=i→Q⁡j=Q⁡i
997 oveq1 ⊢j=i→j+1=i+1
998 997 fveq2d ⊢j=i→Q⁡j+1=Q⁡i+1
999 996 998 oveq12d ⊢j=i→Q⁡jQ⁡j+1=Q⁡iQ⁡i+1
1000 999 cbvmptv ⊢j∈0..^M⟼Q⁡jQ⁡j+1=i∈0..^M⟼Q⁡iQ⁡i+1
1001 454 456 891 195 4 901 920 926 928 987 993 995 1000 fourierdlem70 ⊢φ→∃x∈ℝ∀s∈−ππH⁡s≤x
1002 eqid ⊢e3y=e3y
1003 fveq2 ⊢t=s→G⁡t=G⁡s
1004 1003 fveq2d ⊢t=s→G⁡t=G⁡s
1005 1004 breq1d ⊢t=s→G⁡t≤y↔G⁡s≤y
1006 1005 cbvralvw ⊢∀t∈−ππG⁡t≤y↔∀s∈−ππG⁡s≤y
1007 1006 ralbii ⊢∀n∈ℕ∀t∈−ππG⁡t≤y↔∀n∈ℕ∀s∈−ππG⁡s≤y
1008 1007 3anbi3i ⊢φ∧e∈ℝ+∧y∈ℝ+∧∀n∈ℕ∀t∈−ππG⁡t≤y↔φ∧e∈ℝ+∧y∈ℝ+∧∀n∈ℕ∀s∈−ππG⁡s≤y
1009 1008 anbi1i ⊢φ∧e∈ℝ+∧y∈ℝ+∧∀n∈ℕ∀t∈−ππG⁡t≤y∧u∈dom⁡vol↔φ∧e∈ℝ+∧y∈ℝ+∧∀n∈ℕ∀s∈−ππG⁡s≤y∧u∈dom⁡vol
1010 1009 anbi1i ⊢φ∧e∈ℝ+∧y∈ℝ+∧∀n∈ℕ∀t∈−ππG⁡t≤y∧u∈dom⁡vol∧u⊆−ππ∧vol⁡u≤e3y↔φ∧e∈ℝ+∧y∈ℝ+∧∀n∈ℕ∀s∈−ππG⁡s≤y∧u∈dom⁡vol∧u⊆−ππ∧vol⁡u≤e3y
1011 1010 anbi1i ⊢φ∧e∈ℝ+∧y∈ℝ+∧∀n∈ℕ∀t∈−ππG⁡t≤y∧u∈dom⁡vol∧u⊆−ππ∧vol⁡u≤e3y∧n∈ℕ↔φ∧e∈ℝ+∧y∈ℝ+∧∀n∈ℕ∀s∈−ππG⁡s≤y∧u∈dom⁡vol∧u⊆−ππ∧vol⁡u≤e3y∧n∈ℕ
1012 1 2 54 64 13 14 15 16 17 1001 845 1002 1011 fourierdlem87 ⊢φ∧e∈ℝ+→∃c∈ℝ+∀u∈dom⁡volu⊆−ππ∧vol⁡u≤c→∀k∈ℕ∫uU⁡s⁢sin⁡k+12⁢sds<e2
1013 iftrue ⊢c≤π2→ifc≤π2cπ2=c
1014 1013 adantl ⊢c∈ℝ+∧c≤π2→ifc≤π2cπ2=c
1015 76 a1i ⊢c∈ℝ+∧c≤π2→0∈ℝ*
1016 77 a1i ⊢c∈ℝ+∧c≤π2→π∈ℝ*
1017 rpre ⊢c∈ℝ+→c∈ℝ
1018 1017 adantr ⊢c∈ℝ+∧c≤π2→c∈ℝ
1019 rpgt0 ⊢c∈ℝ+→0<c
1020 1019 adantr ⊢c∈ℝ+∧c≤π2→0<c
1021 42 rehalfcli ⊢π2∈ℝ
1022 1021 a1i ⊢c∈ℝ+∧c≤π2→π2∈ℝ
1023 42 a1i ⊢c∈ℝ+∧c≤π2→π∈ℝ
1024 simpr ⊢c∈ℝ+∧c≤π2→c≤π2
1025 halfpos ⊢π∈ℝ→0<π↔π2<π
1026 42 1025 ax-mp ⊢0<π↔π2<π
1027 887 1026 mpbi ⊢π2<π
1028 1027 a1i ⊢c∈ℝ+∧c≤π2→π2<π
1029 1018 1022 1023 1024 1028 lelttrd ⊢c∈ℝ+∧c≤π2→c<π
1030 1015 1016 1018 1020 1029 eliood ⊢c∈ℝ+∧c≤π2→c∈0π
1031 1014 1030 eqeltrd ⊢c∈ℝ+∧c≤π2→ifc≤π2cπ2∈0π
1032 iffalse ⊢¬c≤π2→ifc≤π2cπ2=π2
1033 2pos ⊢0<2
1034 42 119 887 1033 divgt0ii ⊢0<π2
1035 elioo2 ⊢0∈ℝ*∧π∈ℝ*→π2∈0π↔π2∈ℝ∧0<π2∧π2<π
1036 76 77 1035 mp2an ⊢π2∈0π↔π2∈ℝ∧0<π2∧π2<π
1037 1021 1034 1027 1036 mpbir3an ⊢π2∈0π
1038 1037 a1i ⊢¬c≤π2→π2∈0π
1039 1032 1038 eqeltrd ⊢¬c≤π2→ifc≤π2cπ2∈0π
1040 1039 adantl ⊢c∈ℝ+∧¬c≤π2→ifc≤π2cπ2∈0π
1041 1031 1040 pm2.61dan ⊢c∈ℝ+→ifc≤π2cπ2∈0π
1042 1041 3ad2ant2 ⊢φ∧e∈ℝ+∧c∈ℝ+∧∀u∈dom⁡volu⊆−ππ∧vol⁡u≤c→∀k∈ℕ∫uU⁡s⁢sin⁡k+12⁢sds<e2→ifc≤π2cπ2∈0π
1043 ioombl ⊢0ifc≤π2cπ2∈dom⁡vol
1044 1043 a1i ⊢c∈ℝ+∧∀u∈dom⁡volu⊆−ππ∧vol⁡u≤c→∀k∈ℕ∫uU⁡s⁢sin⁡k+12⁢sds<e2→0ifc≤π2cπ2∈dom⁡vol
1045 simpr ⊢c∈ℝ+∧∀u∈dom⁡volu⊆−ππ∧vol⁡u≤c→∀k∈ℕ∫uU⁡s⁢sin⁡k+12⁢sds<e2→∀u∈dom⁡volu⊆−ππ∧vol⁡u≤c→∀k∈ℕ∫uU⁡s⁢sin⁡k+12⁢sds<e2
1046 1044 1045 jca ⊢c∈ℝ+∧∀u∈dom⁡volu⊆−ππ∧vol⁡u≤c→∀k∈ℕ∫uU⁡s⁢sin⁡k+12⁢sds<e2→0ifc≤π2cπ2∈dom⁡vol∧∀u∈dom⁡volu⊆−ππ∧vol⁡u≤c→∀k∈ℕ∫uU⁡s⁢sin⁡k+12⁢sds<e2
1047 ioossicc ⊢0ifc≤π2cπ2⊆0ifc≤π2cπ2
1048 70 a1i ⊢c∈ℝ+→−π∈ℝ
1049 42 a1i ⊢c∈ℝ+→π∈ℝ
1050 767 a1i ⊢c∈ℝ+→−π≤0
1051 791 1041 sselid ⊢c∈ℝ+→ifc≤π2cπ2∈ℝ
1052 1021 a1i ⊢c∈ℝ+→π2∈ℝ
1053 min2 ⊢c∈ℝ∧π2∈ℝ→ifc≤π2cπ2≤π2
1054 1017 1021 1053 sylancl ⊢c∈ℝ+→ifc≤π2cπ2≤π2
1055 1027 a1i ⊢c∈ℝ+→π2<π
1056 1051 1052 1049 1054 1055 lelttrd ⊢c∈ℝ+→ifc≤π2cπ2<π
1057 1051 1049 1056 ltled ⊢c∈ℝ+→ifc≤π2cπ2≤π
1058 iccss ⊢−π∈ℝ∧π∈ℝ∧−π≤0∧ifc≤π2cπ2≤π→0ifc≤π2cπ2⊆−ππ
1059 1048 1049 1050 1057 1058 syl22anc ⊢c∈ℝ+→0ifc≤π2cπ2⊆−ππ
1060 1047 1059 sstrid ⊢c∈ℝ+→0ifc≤π2cπ2⊆−ππ
1061 0red ⊢c∈ℝ+→0∈ℝ
1062 1020 1014 breqtrrd ⊢c∈ℝ+∧c≤π2→0<ifc≤π2cπ2
1063 1034 1032 breqtrrid ⊢¬c≤π2→0<ifc≤π2cπ2
1064 1063 adantl ⊢c∈ℝ+∧¬c≤π2→0<ifc≤π2cπ2
1065 1062 1064 pm2.61dan ⊢c∈ℝ+→0<ifc≤π2cπ2
1066 1061 1051 1065 ltled ⊢c∈ℝ+→0≤ifc≤π2cπ2
1067 volioo ⊢0∈ℝ∧ifc≤π2cπ2∈ℝ∧0≤ifc≤π2cπ2→vol⁡0ifc≤π2cπ2=ifc≤π2cπ2−0
1068 1061 1051 1066 1067 syl3anc ⊢c∈ℝ+→vol⁡0ifc≤π2cπ2=ifc≤π2cπ2−0
1069 1051 recnd ⊢c∈ℝ+→ifc≤π2cπ2∈ℂ
1070 1069 subid1d ⊢c∈ℝ+→ifc≤π2cπ2−0=ifc≤π2cπ2
1071 1068 1070 eqtrd ⊢c∈ℝ+→vol⁡0ifc≤π2cπ2=ifc≤π2cπ2
1072 min1 ⊢c∈ℝ∧π2∈ℝ→ifc≤π2cπ2≤c
1073 1017 1021 1072 sylancl ⊢c∈ℝ+→ifc≤π2cπ2≤c
1074 1071 1073 eqbrtrd ⊢c∈ℝ+→vol⁡0ifc≤π2cπ2≤c
1075 1060 1074 jca ⊢c∈ℝ+→0ifc≤π2cπ2⊆−ππ∧vol⁡0ifc≤π2cπ2≤c
1076 1075 adantr ⊢c∈ℝ+∧∀u∈dom⁡volu⊆−ππ∧vol⁡u≤c→∀k∈ℕ∫uU⁡s⁢sin⁡k+12⁢sds<e2→0ifc≤π2cπ2⊆−ππ∧vol⁡0ifc≤π2cπ2≤c
1077 sseq1 ⊢u=0ifc≤π2cπ2→u⊆−ππ↔0ifc≤π2cπ2⊆−ππ
1078 fveq2 ⊢u=0ifc≤π2cπ2→vol⁡u=vol⁡0ifc≤π2cπ2
1079 1078 breq1d ⊢u=0ifc≤π2cπ2→vol⁡u≤c↔vol⁡0ifc≤π2cπ2≤c
1080 1077 1079 anbi12d ⊢u=0ifc≤π2cπ2→u⊆−ππ∧vol⁡u≤c↔0ifc≤π2cπ2⊆−ππ∧vol⁡0ifc≤π2cπ2≤c
1081 itgeq1 ⊢u=0ifc≤π2cπ2→∫uU⁡s⁢sin⁡k+12⁢sds=∫0ifc≤π2cπ2U⁡s⁢sin⁡k+12⁢sds
1082 1081 fveq2d ⊢u=0ifc≤π2cπ2→∫uU⁡s⁢sin⁡k+12⁢sds=∫0ifc≤π2cπ2U⁡s⁢sin⁡k+12⁢sds
1083 1082 breq1d ⊢u=0ifc≤π2cπ2→∫uU⁡s⁢sin⁡k+12⁢sds<e2↔∫0ifc≤π2cπ2U⁡s⁢sin⁡k+12⁢sds<e2
1084 1083 ralbidv ⊢u=0ifc≤π2cπ2→∀k∈ℕ∫uU⁡s⁢sin⁡k+12⁢sds<e2↔∀k∈ℕ∫0ifc≤π2cπ2U⁡s⁢sin⁡k+12⁢sds<e2
1085 1080 1084 imbi12d ⊢u=0ifc≤π2cπ2→u⊆−ππ∧vol⁡u≤c→∀k∈ℕ∫uU⁡s⁢sin⁡k+12⁢sds<e2↔0ifc≤π2cπ2⊆−ππ∧vol⁡0ifc≤π2cπ2≤c→∀k∈ℕ∫0ifc≤π2cπ2U⁡s⁢sin⁡k+12⁢sds<e2
1086 1085 rspcva ⊢0ifc≤π2cπ2∈dom⁡vol∧∀u∈dom⁡volu⊆−ππ∧vol⁡u≤c→∀k∈ℕ∫uU⁡s⁢sin⁡k+12⁢sds<e2→0ifc≤π2cπ2⊆−ππ∧vol⁡0ifc≤π2cπ2≤c→∀k∈ℕ∫0ifc≤π2cπ2U⁡s⁢sin⁡k+12⁢sds<e2
1087 1046 1076 1086 sylc ⊢c∈ℝ+∧∀u∈dom⁡volu⊆−ππ∧vol⁡u≤c→∀k∈ℕ∫uU⁡s⁢sin⁡k+12⁢sds<e2→∀k∈ℕ∫0ifc≤π2cπ2U⁡s⁢sin⁡k+12⁢sds<e2
1088 1087 3adant1 ⊢φ∧e∈ℝ+∧c∈ℝ+∧∀u∈dom⁡volu⊆−ππ∧vol⁡u≤c→∀k∈ℕ∫uU⁡s⁢sin⁡k+12⁢sds<e2→∀k∈ℕ∫0ifc≤π2cπ2U⁡s⁢sin⁡k+12⁢sds<e2
1089 oveq2 ⊢d=ifc≤π2cπ2→0d=0ifc≤π2cπ2
1090 1089 itgeq1d ⊢d=ifc≤π2cπ2→∫0dU⁡s⁢sin⁡k+12⁢sds=∫0ifc≤π2cπ2U⁡s⁢sin⁡k+12⁢sds
1091 1090 fveq2d ⊢d=ifc≤π2cπ2→∫0dU⁡s⁢sin⁡k+12⁢sds=∫0ifc≤π2cπ2U⁡s⁢sin⁡k+12⁢sds
1092 1091 breq1d ⊢d=ifc≤π2cπ2→∫0dU⁡s⁢sin⁡k+12⁢sds<e2↔∫0ifc≤π2cπ2U⁡s⁢sin⁡k+12⁢sds<e2
1093 1092 ralbidv ⊢d=ifc≤π2cπ2→∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2↔∀k∈ℕ∫0ifc≤π2cπ2U⁡s⁢sin⁡k+12⁢sds<e2
1094 1093 rspcev ⊢ifc≤π2cπ2∈0π∧∀k∈ℕ∫0ifc≤π2cπ2U⁡s⁢sin⁡k+12⁢sds<e2→∃d∈0π∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2
1095 1042 1088 1094 syl2anc ⊢φ∧e∈ℝ+∧c∈ℝ+∧∀u∈dom⁡volu⊆−ππ∧vol⁡u≤c→∀k∈ℕ∫uU⁡s⁢sin⁡k+12⁢sds<e2→∃d∈0π∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2
1096 1095 rexlimdv3a ⊢φ∧e∈ℝ+→∃c∈ℝ+∀u∈dom⁡volu⊆−ππ∧vol⁡u≤c→∀k∈ℕ∫uU⁡s⁢sin⁡k+12⁢sds<e2→∃d∈0π∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2
1097 1012 1096 mpd ⊢φ∧e∈ℝ+→∃d∈0π∀k∈ℕ∫0dU⁡s⁢sin⁡k+12⁢sds<e2
1098 886 1097 r19.29a ⊢φ∧e∈ℝ+→∃j∈ℕ∀k∈ℤ≥j∫0πU⁡s⁢sin⁡k+12⁢sds<e
1099 1098 ralrimiva ⊢φ→∀e∈ℝ+∃j∈ℕ∀k∈ℤ≥j∫0πU⁡s⁢sin⁡k+12⁢sds<e
1100 nnex ⊢ℕ∈V
1101 1100 mptex ⊢n∈ℕ⟼∫0πG⁡sds∈V
1102 1101 a1i ⊢φ→n∈ℕ⟼∫0πG⁡sds∈V
1103 eqidd ⊢φ∧k∈ℕ→n∈ℕ⟼∫0πG⁡sds=n∈ℕ⟼∫0πG⁡sds
1104 772 adantl ⊢φ∧k∈ℕ∧n=k∧s∈0π→s∈−ππ
1105 774 ad4ant14 ⊢φ∧k∈ℕ∧n=k∧s∈0π→U⁡s∈ℝ
1106 772 adantl ⊢k∈ℕ∧n=k∧s∈0π→s∈−ππ
1107 simpr ⊢k∈ℕ∧n=k→n=k
1108 simpl ⊢k∈ℕ∧n=k→k∈ℕ
1109 1107 1108 eqeltrd ⊢k∈ℕ∧n=k→n∈ℕ
1110 1109 nnred ⊢k∈ℕ∧n=k→n∈ℝ
1111 726 a1i ⊢k∈ℕ∧n=k→12∈ℝ
1112 1110 1111 readdcld ⊢k∈ℕ∧n=k→n+12∈ℝ
1113 1112 adantr ⊢k∈ℕ∧n=k∧s∈0π→n+12∈ℝ
1114 228 1106 sselid ⊢k∈ℕ∧n=k∧s∈0π→s∈ℝ
1115 1113 1114 remulcld ⊢k∈ℕ∧n=k∧s∈0π→n+12⁢s∈ℝ
1116 1115 resincld ⊢k∈ℕ∧n=k∧s∈0π→sin⁡n+12⁢s∈ℝ
1117 1106 1116 824 syl2anc ⊢k∈ℕ∧n=k∧s∈0π→S⁡s=sin⁡n+12⁢s
1118 1117 adantlll ⊢φ∧k∈ℕ∧n=k∧s∈0π→S⁡s=sin⁡n+12⁢s
1119 1110 adantll ⊢φ∧k∈ℕ∧n=k→n∈ℝ
1120 1119 adantr ⊢φ∧k∈ℕ∧n=k∧s∈0π→n∈ℝ
1121 1red ⊢φ∧k∈ℕ∧n=k∧s∈0π→1∈ℝ
1122 1121 rehalfcld ⊢φ∧k∈ℕ∧n=k∧s∈0π→12∈ℝ
1123 1120 1122 readdcld ⊢φ∧k∈ℕ∧n=k∧s∈0π→n+12∈ℝ
1124 228 1104 sselid ⊢φ∧k∈ℕ∧n=k∧s∈0π→s∈ℝ
1125 1123 1124 remulcld ⊢φ∧k∈ℕ∧n=k∧s∈0π→n+12⁢s∈ℝ
1126 1125 resincld ⊢φ∧k∈ℕ∧n=k∧s∈0π→sin⁡n+12⁢s∈ℝ
1127 1118 1126 eqeltrd ⊢φ∧k∈ℕ∧n=k∧s∈0π→S⁡s∈ℝ
1128 1105 1127 remulcld ⊢φ∧k∈ℕ∧n=k∧s∈0π→U⁡s⁢S⁡s∈ℝ
1129 17 fvmpt2 ⊢s∈−ππ∧U⁡s⁢S⁡s∈ℝ→G⁡s=U⁡s⁢S⁡s
1130 1104 1128 1129 syl2anc ⊢φ∧k∈ℕ∧n=k∧s∈0π→G⁡s=U⁡s⁢S⁡s
1131 oveq1 ⊢n=k→n+12=k+12
1132 1131 oveq1d ⊢n=k→n+12⁢s=k+12⁢s
1133 1132 fveq2d ⊢n=k→sin⁡n+12⁢s=sin⁡k+12⁢s
1134 1133 ad2antlr ⊢φ∧k∈ℕ∧n=k∧s∈0π→sin⁡n+12⁢s=sin⁡k+12⁢s
1135 1118 1134 eqtrd ⊢φ∧k∈ℕ∧n=k∧s∈0π→S⁡s=sin⁡k+12⁢s
1136 1135 oveq2d ⊢φ∧k∈ℕ∧n=k∧s∈0π→U⁡s⁢S⁡s=U⁡s⁢sin⁡k+12⁢s
1137 1130 1136 eqtrd ⊢φ∧k∈ℕ∧n=k∧s∈0π→G⁡s=U⁡s⁢sin⁡k+12⁢s
1138 1137 itgeq2dv ⊢φ∧k∈ℕ∧n=k→∫0πG⁡sds=∫0πU⁡s⁢sin⁡k+12⁢sds
1139 simpr ⊢φ∧k∈ℕ→k∈ℕ
1140 805 itgeq2dv ⊢n=k→∫0πU⁡s⁢sin⁡n+12⁢sds=∫0πU⁡s⁢sin⁡k+12⁢sds
1141 1140 eleq1d ⊢n=k→∫0πU⁡s⁢sin⁡n+12⁢sds∈ℂ↔∫0πU⁡s⁢sin⁡k+12⁢sds∈ℂ
1142 800 1141 imbi12d ⊢n=k→φ∧n∈ℕ→∫0πU⁡s⁢sin⁡n+12⁢sds∈ℂ↔φ∧k∈ℕ→∫0πU⁡s⁢sin⁡k+12⁢sds∈ℂ
1143 774 adantlr ⊢φ∧n∈ℕ∧s∈0π→U⁡s∈ℝ
1144 simpr ⊢φ∧n∈ℕ→n∈ℕ
1145 1144 772 821 syl2an ⊢φ∧n∈ℕ∧s∈0π→sin⁡n+12⁢s∈ℝ
1146 1143 1145 remulcld ⊢φ∧n∈ℕ∧s∈0π→U⁡s⁢sin⁡n+12⁢s∈ℝ
1147 1146 847 itgcl ⊢φ∧n∈ℕ→∫0πU⁡s⁢sin⁡n+12⁢sds∈ℂ
1148 1142 1147 chvarvv ⊢φ∧k∈ℕ→∫0πU⁡s⁢sin⁡k+12⁢sds∈ℂ
1149 1103 1138 1139 1148 fvmptd ⊢φ∧k∈ℕ→n∈ℕ⟼∫0πG⁡sds⁡k=∫0πU⁡s⁢sin⁡k+12⁢sds
1150 39 33 1102 1149 1148 clim0c ⊢φ→n∈ℕ⟼∫0πG⁡sds⇝0↔∀e∈ℝ+∃j∈ℕ∀k∈ℤ≥j∫0πU⁡s⁢sin⁡k+12⁢sds<e
1151 1099 1150 mpbird ⊢φ→n∈ℕ⟼∫0πG⁡sds⇝0
1152 1100 mptex ⊢n∈ℕ⟼∫0πG⁡sdsπ∈V
1153 19 1152 eqeltri ⊢E∈V
1154 1153 a1i ⊢φ→E∈V
1155 1100 mptex ⊢n∈ℕ⟼π∈V
1156 1155 a1i ⊢φ→n∈ℕ⟼π∈V
1157 42 recni ⊢π∈ℂ
1158 1157 a1i ⊢φ→π∈ℂ
1159 eqidd ⊢m∈ℕ→n∈ℕ⟼π=n∈ℕ⟼π
1160 eqidd ⊢m∈ℕ∧n=m→π=π
1161 id ⊢m∈ℕ→m∈ℕ
1162 42 a1i ⊢m∈ℕ→π∈ℝ
1163 1159 1160 1161 1162 fvmptd ⊢m∈ℕ→n∈ℕ⟼π⁡m=π
1164 1163 adantl ⊢φ∧m∈ℕ→n∈ℕ⟼π⁡m=π
1165 39 33 1156 1158 1164 climconst ⊢φ→n∈ℕ⟼π⇝π
1166 766 887 gtneii ⊢π≠0
1167 1166 a1i ⊢φ→π≠0
1168 2 adantr ⊢φ∧n∈ℕ→X∈ℝ
1169 54 adantr ⊢φ∧n∈ℕ→Y∈ℝ
1170 64 adantr ⊢φ∧n∈ℕ→W∈ℝ
1171 830 1168 1169 1170 13 14 15 834 16 17 fourierdlem67 ⊢φ∧n∈ℕ→G:−ππ⟶ℝ
1172 1171 adantr ⊢φ∧n∈ℕ∧s∈0π→G:−ππ⟶ℝ
1173 809 sselda ⊢φ∧n∈ℕ∧s∈0π→s∈−ππ
1174 1172 1173 ffvelcdmd ⊢φ∧n∈ℕ∧s∈0π→G⁡s∈ℝ
1175 1171 ffvelcdmda ⊢φ∧n∈ℕ∧s∈−ππ→G⁡s∈ℝ
1176 1171 feqmptd ⊢φ∧n∈ℕ→G=s∈−ππ⟼G⁡s
1177 1176 845 eqeltrrd ⊢φ∧n∈ℕ→s∈−ππ⟼G⁡s∈𝐿1
1178 809 811 1175 1177 iblss ⊢φ∧n∈ℕ→s∈0π⟼G⁡s∈𝐿1
1179 1174 1178 itgcl ⊢φ∧n∈ℕ→∫0πG⁡sds∈ℂ
1180 eqid ⊢n∈ℕ⟼∫0πG⁡sds=n∈ℕ⟼∫0πG⁡sds
1181 1180 fvmpt2 ⊢n∈ℕ∧∫0πG⁡sds∈ℂ→n∈ℕ⟼∫0πG⁡sds⁡n=∫0πG⁡sds
1182 1144 1179 1181 syl2anc ⊢φ∧n∈ℕ→n∈ℕ⟼∫0πG⁡sds⁡n=∫0πG⁡sds
1183 1182 1179 eqeltrd ⊢φ∧n∈ℕ→n∈ℕ⟼∫0πG⁡sds⁡n∈ℂ
1184 eqid ⊢n∈ℕ⟼π=n∈ℕ⟼π
1185 1184 fvmpt2 ⊢n∈ℕ∧π∈ℝ→n∈ℕ⟼π⁡n=π
1186 42 1185 mpan2 ⊢n∈ℕ→n∈ℕ⟼π⁡n=π
1187 1157 a1i ⊢n∈ℕ→π∈ℂ
1188 1166 a1i ⊢n∈ℕ→π≠0
1189 eldifsn ⊢π∈ℂ∖0↔π∈ℂ∧π≠0
1190 1187 1188 1189 sylanbrc ⊢n∈ℕ→π∈ℂ∖0
1191 1186 1190 eqeltrd ⊢n∈ℕ→n∈ℕ⟼π⁡n∈ℂ∖0
1192 1191 adantl ⊢φ∧n∈ℕ→n∈ℕ⟼π⁡n∈ℂ∖0
1193 1157 a1i ⊢φ∧n∈ℕ→π∈ℂ
1194 1166 a1i ⊢φ∧n∈ℕ→π≠0
1195 1179 1193 1194 divcld ⊢φ∧n∈ℕ→∫0πG⁡sdsπ∈ℂ
1196 19 fvmpt2 ⊢n∈ℕ∧∫0πG⁡sdsπ∈ℂ→E⁡n=∫0πG⁡sdsπ
1197 1144 1195 1196 syl2anc ⊢φ∧n∈ℕ→E⁡n=∫0πG⁡sdsπ
1198 1182 eqcomd ⊢φ∧n∈ℕ→∫0πG⁡sds=n∈ℕ⟼∫0πG⁡sds⁡n
1199 1186 eqcomd ⊢n∈ℕ→π=n∈ℕ⟼π⁡n
1200 1199 adantl ⊢φ∧n∈ℕ→π=n∈ℕ⟼π⁡n
1201 1198 1200 oveq12d ⊢φ∧n∈ℕ→∫0πG⁡sdsπ=n∈ℕ⟼∫0πG⁡sds⁡nn∈ℕ⟼π⁡n
1202 1197 1201 eqtrd ⊢φ∧n∈ℕ→E⁡n=n∈ℕ⟼∫0πG⁡sds⁡nn∈ℕ⟼π⁡n
1203 34 35 36 38 39 33 1151 1154 1165 1167 1183 1192 1202 climdivf ⊢φ→E⇝0π
1204 1157 1166 div0i ⊢0π=0
1205 1204 a1i ⊢φ→0π=0
1206 1203 1205 breqtrd ⊢φ→E⇝0
1207 1100 mptex ⊢m∈ℕ⟼∫0πF⁡X+s⁢D⁡m⁡sds∈V
1208 18 1207 eqeltri ⊢Z∈V
1209 1208 a1i ⊢φ→Z∈V
1210 1100 mptex ⊢m∈ℕ⟼Y2∈V
1211 1210 a1i ⊢φ→m∈ℕ⟼Y2∈V
1212 limccl ⊢F↾X+∞limℂX⊆ℂ
1213 1212 20 sselid ⊢φ→Y∈ℂ
1214 1213 halfcld ⊢φ→Y2∈ℂ
1215 eqidd ⊢φ∧n∈ℤ≥1→m∈ℕ⟼Y2=m∈ℕ⟼Y2
1216 eqidd ⊢φ∧n∈ℤ≥1∧m=n→Y2=Y2
1217 39 eqcomi ⊢ℤ≥1=ℕ
1218 1217 eleq2i ⊢n∈ℤ≥1↔n∈ℕ
1219 1218 biimpi ⊢n∈ℤ≥1→n∈ℕ
1220 1219 adantl ⊢φ∧n∈ℤ≥1→n∈ℕ
1221 1214 adantr ⊢φ∧n∈ℤ≥1→Y2∈ℂ
1222 1215 1216 1220 1221 fvmptd ⊢φ∧n∈ℤ≥1→m∈ℕ⟼Y2⁡n=Y2
1223 32 33 1211 1214 1222 climconst ⊢φ→m∈ℕ⟼Y2⇝Y2
1224 1195 19 fmptd ⊢φ→E:ℕ⟶ℂ
1225 1224 adantr ⊢φ∧n∈ℤ≥1→E:ℕ⟶ℂ
1226 1225 1220 ffvelcdmd ⊢φ∧n∈ℤ≥1→E⁡n∈ℂ
1227 1222 1221 eqeltrd ⊢φ∧n∈ℤ≥1→m∈ℕ⟼Y2⁡n∈ℂ
1228 1222 oveq2d ⊢φ∧n∈ℤ≥1→E⁡n+m∈ℕ⟼Y2⁡n=E⁡n+Y2
1229 810 a1i ⊢φ→0π∈dom⁡vol
1230 0red ⊢s∈0π→0∈ℝ
1231 1230 rexrd ⊢s∈0π→0∈ℝ*
1232 77 a1i ⊢s∈0π→π∈ℝ*
1233 id ⊢s∈0π→s∈0π
1234 ioogtlb ⊢0∈ℝ*∧π∈ℝ*∧s∈0π→0<s
1235 1231 1232 1233 1234 syl3anc ⊢s∈0π→0<s
1236 1235 gt0ne0d ⊢s∈0π→s≠0
1237 1236 neneqd ⊢s∈0π→¬s=0
1238 velsn ⊢s∈0↔s=0
1239 1237 1238 sylnibr ⊢s∈0π→¬s∈0
1240 772 1239 eldifd ⊢s∈0π→s∈−ππ∖0
1241 1240 ssriv ⊢0π⊆−ππ∖0
1242 1241 a1i ⊢φ→0π⊆−ππ∖0
1243 1235 adantl ⊢φ∧s∈0π→0<s
1244 1243 iftrued ⊢φ∧s∈0π→if0<sYW=Y
1245 eqid ⊢D⁡n=D⁡n
1246 0red ⊢φ∧n∈ℕ→0∈ℝ
1247 42 a1i ⊢φ∧n∈ℕ→π∈ℝ
1248 766 42 887 ltleii ⊢0≤π
1249 1248 a1i ⊢φ∧n∈ℕ→0≤π
1250 eqid ⊢s∈0π⟼s2+∑k=1nsin⁡k⁢skπ=s∈0π⟼s2+∑k=1nsin⁡k⁢skπ
1251 24 1144 1245 1246 1247 1249 1250 dirkeritg ⊢φ∧n∈ℕ→∫0πD⁡n⁡sds=s∈0π⟼s2+∑k=1nsin⁡k⁢skπ⁡π−s∈0π⟼s2+∑k=1nsin⁡k⁢skπ⁡0
1252 ubicc2 ⊢0∈ℝ*∧π∈ℝ*∧0≤π→π∈0π
1253 76 77 1248 1252 mp3an ⊢π∈0π
1254 oveq1 ⊢s=π→s2=π2
1255 oveq2 ⊢s=π→k⁢s=k⁢π
1256 1255 fveq2d ⊢s=π→sin⁡k⁢s=sin⁡k⁢π
1257 1256 oveq1d ⊢s=π→sin⁡k⁢sk=sin⁡k⁢πk
1258 elfzelz ⊢k∈1…n→k∈ℤ
1259 1258 zcnd ⊢k∈1…n→k∈ℂ
1260 1157 a1i ⊢k∈1…n→π∈ℂ
1261 1166 a1i ⊢k∈1…n→π≠0
1262 1259 1260 1261 divcan4d ⊢k∈1…n→k⁢ππ=k
1263 1262 1258 eqeltrd ⊢k∈1…n→k⁢ππ∈ℤ
1264 1259 1260 mulcld ⊢k∈1…n→k⁢π∈ℂ
1265 sineq0 ⊢k⁢π∈ℂ→sin⁡k⁢π=0↔k⁢ππ∈ℤ
1266 1264 1265 syl ⊢k∈1…n→sin⁡k⁢π=0↔k⁢ππ∈ℤ
1267 1263 1266 mpbird ⊢k∈1…n→sin⁡k⁢π=0
1268 1267 oveq1d ⊢k∈1…n→sin⁡k⁢πk=0k
1269 0red ⊢k∈1…n→0∈ℝ
1270 1red ⊢k∈1…n→1∈ℝ
1271 1258 zred ⊢k∈1…n→k∈ℝ
1272 117 a1i ⊢k∈1…n→0<1
1273 elfzle1 ⊢k∈1…n→1≤k
1274 1269 1270 1271 1272 1273 ltletrd ⊢k∈1…n→0<k
1275 1274 gt0ne0d ⊢k∈1…n→k≠0
1276 1259 1275 div0d ⊢k∈1…n→0k=0
1277 1268 1276 eqtrd ⊢k∈1…n→sin⁡k⁢πk=0
1278 1257 1277 sylan9eq ⊢s=π∧k∈1…n→sin⁡k⁢sk=0
1279 1278 sumeq2dv ⊢s=π→∑k=1nsin⁡k⁢sk=∑k=1n0
1280 fzfi ⊢1…n∈Fin
1281 1280 olci ⊢1…n⊆ℤ≥∥˙∨1…n∈Fin
1282 sumz ⊢1…n⊆ℤ≥∥˙∨1…n∈Fin→∑k=1n0=0
1283 1281 1282 ax-mp ⊢∑k=1n0=0
1284 1279 1283 eqtrdi ⊢s=π→∑k=1nsin⁡k⁢sk=0
1285 1254 1284 oveq12d ⊢s=π→s2+∑k=1nsin⁡k⁢sk=π2+0
1286 1285 oveq1d ⊢s=π→s2+∑k=1nsin⁡k⁢skπ=π2+0π
1287 ovex ⊢π2+0π∈V
1288 1286 1250 1287 fvmpt ⊢π∈0π→s∈0π⟼s2+∑k=1nsin⁡k⁢skπ⁡π=π2+0π
1289 1253 1288 ax-mp ⊢s∈0π⟼s2+∑k=1nsin⁡k⁢skπ⁡π=π2+0π
1290 lbicc2 ⊢0∈ℝ*∧π∈ℝ*∧0≤π→0∈0π
1291 76 77 1248 1290 mp3an ⊢0∈0π
1292 oveq1 ⊢s=0→s2=02
1293 2cn ⊢2∈ℂ
1294 1293 256 div0i ⊢02=0
1295 1292 1294 eqtrdi ⊢s=0→s2=0
1296 oveq2 ⊢s=0→k⁢s=k⋅0
1297 1259 mul01d ⊢k∈1…n→k⋅0=0
1298 1296 1297 sylan9eq ⊢s=0∧k∈1…n→k⁢s=0
1299 1298 fveq2d ⊢s=0∧k∈1…n→sin⁡k⁢s=sin⁡0
1300 sin0 ⊢sin⁡0=0
1301 1299 1300 eqtrdi ⊢s=0∧k∈1…n→sin⁡k⁢s=0
1302 1301 oveq1d ⊢s=0∧k∈1…n→sin⁡k⁢sk=0k
1303 1276 adantl ⊢s=0∧k∈1…n→0k=0
1304 1302 1303 eqtrd ⊢s=0∧k∈1…n→sin⁡k⁢sk=0
1305 1304 sumeq2dv ⊢s=0→∑k=1nsin⁡k⁢sk=∑k=1n0
1306 1305 1283 eqtrdi ⊢s=0→∑k=1nsin⁡k⁢sk=0
1307 1295 1306 oveq12d ⊢s=0→s2+∑k=1nsin⁡k⁢sk=0+0
1308 00id ⊢0+0=0
1309 1307 1308 eqtrdi ⊢s=0→s2+∑k=1nsin⁡k⁢sk=0
1310 1309 oveq1d ⊢s=0→s2+∑k=1nsin⁡k⁢skπ=0π
1311 1310 1204 eqtrdi ⊢s=0→s2+∑k=1nsin⁡k⁢skπ=0
1312 c0ex ⊢0∈V
1313 1311 1250 1312 fvmpt ⊢0∈0π→s∈0π⟼s2+∑k=1nsin⁡k⁢skπ⁡0=0
1314 1291 1313 ax-mp ⊢s∈0π⟼s2+∑k=1nsin⁡k⁢skπ⁡0=0
1315 1289 1314 oveq12i ⊢s∈0π⟼s2+∑k=1nsin⁡k⁢skπ⁡π−s∈0π⟼s2+∑k=1nsin⁡k⁢skπ⁡0=π2+0π−0
1316 1315 a1i ⊢φ∧n∈ℕ→s∈0π⟼s2+∑k=1nsin⁡k⁢skπ⁡π−s∈0π⟼s2+∑k=1nsin⁡k⁢skπ⁡0=π2+0π−0
1317 1021 recni ⊢π2∈ℂ
1318 1317 addridi ⊢π2+0=π2
1319 1318 oveq1i ⊢π2+0π=π2π
1320 1157 1293 1157 256 1166 divdiv32i ⊢π2π=ππ2
1321 1157 1166 dividi ⊢ππ=1
1322 1321 oveq1i ⊢ππ2=12
1323 1319 1320 1322 3eqtri ⊢π2+0π=12
1324 1323 oveq1i ⊢π2+0π−0=12−0
1325 halfcn ⊢12∈ℂ
1326 1325 subid1i ⊢12−0=12
1327 1324 1326 eqtri ⊢π2+0π−0=12
1328 1327 a1i ⊢φ∧n∈ℕ→π2+0π−0=12
1329 1251 1316 1328 3eqtrd ⊢φ∧n∈ℕ→∫0πD⁡n⁡sds=12
1330 1 2 3 4 5 6 7 11 12 13 14 15 16 17 841 601 22 23 20 21 1229 1242 19 24 54 1244 1329 fourierdlem95 ⊢φ∧n∈ℕ→E⁡n+Y2=∫0πF⁡X+s⁢D⁡n⁡sds
1331 1220 1330 syldan ⊢φ∧n∈ℤ≥1→E⁡n+Y2=∫0πF⁡X+s⁢D⁡n⁡sds
1332 18 a1i ⊢φ∧n∈ℕ→Z=m∈ℕ⟼∫0πF⁡X+s⁢D⁡m⁡sds
1333 fveq2 ⊢m=n→D⁡m=D⁡n
1334 1333 fveq1d ⊢m=n→D⁡m⁡s=D⁡n⁡s
1335 1334 oveq2d ⊢m=n→F⁡X+s⁢D⁡m⁡s=F⁡X+s⁢D⁡n⁡s
1336 1335 adantr ⊢m=n∧s∈0π→F⁡X+s⁢D⁡m⁡s=F⁡X+s⁢D⁡n⁡s
1337 1336 itgeq2dv ⊢m=n→∫0πF⁡X+s⁢D⁡m⁡sds=∫0πF⁡X+s⁢D⁡n⁡sds
1338 1337 adantl ⊢φ∧n∈ℕ∧m=n→∫0πF⁡X+s⁢D⁡m⁡sds=∫0πF⁡X+s⁢D⁡n⁡sds
1339 1 adantr ⊢φ∧s∈0π→F:ℝ⟶ℝ
1340 2 adantr ⊢φ∧s∈0π→X∈ℝ
1341 782 adantl ⊢φ∧s∈0π→s∈ℝ
1342 1340 1341 readdcld ⊢φ∧s∈0π→X+s∈ℝ
1343 1339 1342 ffvelcdmd ⊢φ∧s∈0π→F⁡X+s∈ℝ
1344 1343 adantlr ⊢φ∧n∈ℕ∧s∈0π→F⁡X+s∈ℝ
1345 24 dirkerf ⊢n∈ℕ→D⁡n:ℝ⟶ℝ
1346 1345 ad2antlr ⊢φ∧n∈ℕ∧s∈0π→D⁡n:ℝ⟶ℝ
1347 782 adantl ⊢φ∧n∈ℕ∧s∈0π→s∈ℝ
1348 1346 1347 ffvelcdmd ⊢φ∧n∈ℕ∧s∈0π→D⁡n⁡s∈ℝ
1349 1344 1348 remulcld ⊢φ∧n∈ℕ∧s∈0π→F⁡X+s⁢D⁡n⁡s∈ℝ
1350 1 adantr ⊢φ∧s∈−ππ→F:ℝ⟶ℝ
1351 2 adantr ⊢φ∧s∈−ππ→X∈ℝ
1352 228 sseli ⊢s∈−ππ→s∈ℝ
1353 1352 adantl ⊢φ∧s∈−ππ→s∈ℝ
1354 1351 1353 readdcld ⊢φ∧s∈−ππ→X+s∈ℝ
1355 1350 1354 ffvelcdmd ⊢φ∧s∈−ππ→F⁡X+s∈ℝ
1356 1355 adantlr ⊢φ∧n∈ℕ∧s∈−ππ→F⁡X+s∈ℝ
1357 1345 ad2antlr ⊢φ∧n∈ℕ∧s∈−ππ→D⁡n:ℝ⟶ℝ
1358 1352 adantl ⊢φ∧n∈ℕ∧s∈−ππ→s∈ℝ
1359 1357 1358 ffvelcdmd ⊢φ∧n∈ℕ∧s∈−ππ→D⁡n⁡s∈ℝ
1360 1356 1359 remulcld ⊢φ∧n∈ℕ∧s∈−ππ→F⁡X+s⁢D⁡n⁡s∈ℝ
1361 70 a1i ⊢φ∧n∈ℕ→−π∈ℝ
1362 24 dirkercncf ⊢n∈ℕ→D⁡n:ℝ⟶cnℝ
1363 1362 adantl ⊢φ∧n∈ℕ→D⁡n:ℝ⟶cnℝ
1364 eqid ⊢s∈−ππ⟼F⁡X+s⁢D⁡n⁡s=s∈−ππ⟼F⁡X+s⁢D⁡n⁡s
1365 1361 1247 830 1168 3 835 836 837 838 839 29 840 1363 1364 fourierdlem84 ⊢φ∧n∈ℕ→s∈−ππ⟼F⁡X+s⁢D⁡n⁡s∈𝐿1
1366 809 811 1360 1365 iblss ⊢φ∧n∈ℕ→s∈0π⟼F⁡X+s⁢D⁡n⁡s∈𝐿1
1367 1349 1366 itgrecl ⊢φ∧n∈ℕ→∫0πF⁡X+s⁢D⁡n⁡sds∈ℝ
1368 1332 1338 1144 1367 fvmptd ⊢φ∧n∈ℕ→Z⁡n=∫0πF⁡X+s⁢D⁡n⁡sds
1369 1368 eqcomd ⊢φ∧n∈ℕ→∫0πF⁡X+s⁢D⁡n⁡sds=Z⁡n
1370 1220 1369 syldan ⊢φ∧n∈ℤ≥1→∫0πF⁡X+s⁢D⁡n⁡sds=Z⁡n
1371 1228 1331 1370 3eqtrrd ⊢φ∧n∈ℤ≥1→Z⁡n=E⁡n+m∈ℕ⟼Y2⁡n
1372 32 33 1206 1209 1223 1226 1227 1371 climadd ⊢φ→Z⇝0+Y2
1373 1214 addlidd ⊢φ→0+Y2=Y2
1374 1372 1373 breqtrd ⊢φ→Z⇝Y2