Metamath Proof Explorer


Theorem itgsinexplem1

Description: Integration by parts is applied to integrate sin^(N+1). (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses itgsinexplem1.1 F = x sin x N
itgsinexplem1.2 G = x cos x
itgsinexplem1.3 H = x N sin x N 1 cos x
itgsinexplem1.4 I = x sin x N sin x
itgsinexplem1.5 L = x N sin x N 1 cos x cos x
itgsinexplem1.6 M = x cos x 2 sin x N 1
itgsinexplem1.7 φ N
Assertion itgsinexplem1 φ 0 π sin x N sin x dx = N 0 π cos x 2 sin x N 1 dx

Proof

Step Hyp Ref Expression
1 itgsinexplem1.1 F = x sin x N
2 itgsinexplem1.2 G = x cos x
3 itgsinexplem1.3 H = x N sin x N 1 cos x
4 itgsinexplem1.4 I = x sin x N sin x
5 itgsinexplem1.5 L = x N sin x N 1 cos x cos x
6 itgsinexplem1.6 M = x cos x 2 sin x N 1
7 itgsinexplem1.7 φ N
8 0m0e0 0 0 = 0
9 8 oveq1i 0 - 0 - 0 π N sin x N 1 cos x cos x dx = 0 0 π N sin x N 1 cos x cos x dx
10 0re 0
11 10 a1i φ 0
12 pire π
13 12 a1i φ π
14 pipos 0 < π
15 10 12 14 ltleii 0 π
16 15 a1i φ 0 π
17 10 12 pm3.2i 0 π
18 iccssre 0 π 0 π
19 17 18 ax-mp 0 π
20 ax-resscn
21 19 20 sstri 0 π
22 21 sseli x 0 π x
23 22 adantl φ x 0 π x
24 22 sincld x 0 π sin x
25 24 adantl φ x 0 π sin x
26 7 nnnn0d φ N 0
27 26 adantr φ x 0 π N 0
28 25 27 expcld φ x 0 π sin x N
29 1 fvmpt2 x sin x N F x = sin x N
30 23 28 29 syl2anc φ x 0 π F x = sin x N
31 30 eqcomd φ x 0 π sin x N = F x
32 31 mpteq2dva φ x 0 π sin x N = x 0 π F x
33 nfmpt1 _ x x sin x N
34 1 33 nfcxfr _ x F
35 nfcv _ x sin
36 sincn sin : cn
37 36 a1i φ sin : cn
38 35 37 26 expcnfg φ x sin x N : cn
39 1 38 eqeltrid φ F : cn
40 21 a1i φ 0 π
41 34 39 40 cncfmptss φ x 0 π F x : 0 π cn
42 32 41 eqeltrd φ x 0 π sin x N : 0 π cn
43 22 coscld x 0 π cos x
44 43 negcld x 0 π cos x
45 2 fvmpt2 x cos x G x = cos x
46 22 44 45 syl2anc x 0 π G x = cos x
47 46 eqcomd x 0 π cos x = G x
48 47 adantl φ x 0 π cos x = G x
49 48 mpteq2dva φ x 0 π cos x = x 0 π G x
50 nfmpt1 _ x x cos x
51 2 50 nfcxfr _ x G
52 coscn cos : cn
53 52 a1i φ cos : cn
54 2 negfcncf cos : cn G : cn
55 53 54 syl φ G : cn
56 51 55 40 cncfmptss φ x 0 π G x : 0 π cn
57 49 56 eqeltrd φ x 0 π cos x : 0 π cn
58 ssidd φ
59 7 nncnd φ N
60 58 59 58 constcncfg φ x N : cn
61 nnm1nn0 N N 1 0
62 7 61 syl φ N 1 0
63 35 37 62 expcnfg φ x sin x N 1 : cn
64 60 63 mulcncf φ x N sin x N 1 : cn
65 cosf cos :
66 65 a1i φ cos :
67 66 feqmptd φ cos = x cos x
68 67 52 eqeltrrdi φ x cos x : cn
69 64 68 mulcncf φ x N sin x N 1 cos x : cn
70 3 69 eqeltrid φ H : cn
71 ioosscn 0 π
72 71 a1i φ 0 π
73 59 adantr φ x 0 π N
74 71 sseli x 0 π x
75 74 sincld x 0 π sin x
76 75 adantl φ x 0 π sin x
77 62 adantr φ x 0 π N 1 0
78 76 77 expcld φ x 0 π sin x N 1
79 73 78 mulcld φ x 0 π N sin x N 1
80 74 coscld x 0 π cos x
81 80 adantl φ x 0 π cos x
82 79 81 mulcld φ x 0 π N sin x N 1 cos x
83 3 70 72 58 82 cncfmptssg φ x 0 π N sin x N 1 cos x : 0 π cn
84 35 37 72 cncfmptss φ x 0 π sin x : 0 π cn
85 ioossicc 0 π 0 π
86 85 a1i φ 0 π 0 π
87 ioombl 0 π dom vol
88 87 a1i φ 0 π dom vol
89 28 25 mulcld φ x 0 π sin x N sin x
90 4 fvmpt2 x sin x N sin x I x = sin x N sin x
91 23 89 90 syl2anc φ x 0 π I x = sin x N sin x
92 91 eqcomd φ x 0 π sin x N sin x = I x
93 92 mpteq2dva φ x 0 π sin x N sin x = x 0 π I x
94 nfmpt1 _ x x sin x N sin x
95 4 94 nfcxfr _ x I
96 sinf sin :
97 96 a1i φ sin :
98 97 feqmptd φ sin = x sin x
99 98 36 eqeltrrdi φ x sin x : cn
100 38 99 mulcncf φ x sin x N sin x : cn
101 4 100 eqeltrid φ I : cn
102 95 101 40 cncfmptss φ x 0 π I x : 0 π cn
103 93 102 eqeltrd φ x 0 π sin x N sin x : 0 π cn
104 cniccibl 0 π x 0 π sin x N sin x : 0 π cn x 0 π sin x N sin x 𝐿 1
105 11 13 103 104 syl3anc φ x 0 π sin x N sin x 𝐿 1
106 86 88 89 105 iblss φ x 0 π sin x N sin x 𝐿 1
107 59 adantr φ x 0 π N
108 62 adantr φ x 0 π N 1 0
109 25 108 expcld φ x 0 π sin x N 1
110 107 109 mulcld φ x 0 π N sin x N 1
111 43 adantl φ x 0 π cos x
112 110 111 mulcld φ x 0 π N sin x N 1 cos x
113 44 adantl φ x 0 π cos x
114 112 113 mulcld φ x 0 π N sin x N 1 cos x cos x
115 eqid x cos x = x cos x
116 115 negfcncf cos : cn x cos x : cn
117 53 116 syl φ x cos x : cn
118 69 117 mulcncf φ x N sin x N 1 cos x cos x : cn
119 5 118 eqeltrid φ L : cn
120 5 119 40 58 114 cncfmptssg φ x 0 π N sin x N 1 cos x cos x : 0 π cn
121 cniccibl 0 π x 0 π N sin x N 1 cos x cos x : 0 π cn x 0 π N sin x N 1 cos x cos x 𝐿 1
122 11 13 120 121 syl3anc φ x 0 π N sin x N 1 cos x cos x 𝐿 1
123 86 88 114 122 iblss φ x 0 π N sin x N 1 cos x cos x 𝐿 1
124 reelprrecn
125 124 a1i φ
126 recn x x
127 126 sincld x sin x
128 127 adantl φ x sin x
129 26 adantr φ x N 0
130 128 129 expcld φ x sin x N
131 59 adantr φ x N
132 62 adantr φ x N 1 0
133 128 132 expcld φ x sin x N 1
134 131 133 mulcld φ x N sin x N 1
135 126 coscld x cos x
136 135 adantl φ x cos x
137 134 136 mulcld φ x N sin x N 1 cos x
138 sincl x sin x
139 138 adantl φ x sin x
140 26 adantr φ x N 0
141 139 140 expcld φ x sin x N
142 141 1 fmptd φ F :
143 126 adantl φ x x
144 elex N sin x N 1 cos x N sin x N 1 cos x V
145 137 144 syl φ x N sin x N 1 cos x V
146 rabid x x | N sin x N 1 cos x V x N sin x N 1 cos x V
147 143 145 146 sylanbrc φ x x x | N sin x N 1 cos x V
148 3 dmmpt dom H = x | N sin x N 1 cos x V
149 147 148 eleqtrrdi φ x x dom H
150 149 ex φ x x dom H
151 150 alrimiv φ x x x dom H
152 nfcv _ x
153 nfmpt1 _ x x N sin x N 1 cos x
154 3 153 nfcxfr _ x H
155 154 nfdm _ x dom H
156 152 155 dfss2f dom H x x x dom H
157 151 156 sylibr φ dom H
158 7 dvsinexp φ dx sin x N d x = x N sin x N 1 cos x
159 1 oveq2i D F = dx sin x N d x
160 158 159 3 3eqtr4g φ D F = H
161 160 dmeqd φ dom F = dom H
162 157 161 sseqtrrd φ dom F
163 dvres3 F : dom F D F = F
164 125 142 58 162 163 syl22anc φ D F = F
165 1 reseq1i F = x sin x N
166 resmpt x sin x N = x sin x N
167 20 166 ax-mp x sin x N = x sin x N
168 165 167 eqtri F = x sin x N
169 168 oveq2i D F = dx sin x N d x
170 169 a1i φ D F = dx sin x N d x
171 160 reseq1d φ F = H
172 3 reseq1i H = x N sin x N 1 cos x
173 resmpt x N sin x N 1 cos x = x N sin x N 1 cos x
174 20 173 ax-mp x N sin x N 1 cos x = x N sin x N 1 cos x
175 172 174 eqtri H = x N sin x N 1 cos x
176 171 175 eqtrdi φ F = x N sin x N 1 cos x
177 164 170 176 3eqtr3d φ dx sin x N d x = x N sin x N 1 cos x
178 19 a1i φ 0 π
179 eqid TopOpen fld = TopOpen fld
180 179 tgioo2 topGen ran . = TopOpen fld 𝑡
181 17 a1i φ 0 π
182 iccntr 0 π int topGen ran . 0 π = 0 π
183 181 182 syl φ int topGen ran . 0 π = 0 π
184 125 130 137 177 178 180 179 183 dvmptres2 φ dx 0 π sin x N d x = x 0 π N sin x N 1 cos x
185 135 negcld x cos x
186 185 adantl φ x cos x
187 127 negcld x sin x
188 187 adantl φ x sin x
189 dvcosre dx cos x d x = x sin x
190 189 a1i φ dx cos x d x = x sin x
191 125 136 188 190 dvmptneg φ dx cos x d x = x sin x
192 127 negnegd x sin x = sin x
193 192 adantl φ x sin x = sin x
194 193 mpteq2dva φ x sin x = x sin x
195 191 194 eqtrd φ dx cos x d x = x sin x
196 125 186 128 195 178 180 179 183 dvmptres2 φ dx 0 π cos x d x = x 0 π sin x
197 fveq2 x = 0 sin x = sin 0
198 sin0 sin 0 = 0
199 197 198 eqtrdi x = 0 sin x = 0
200 199 oveq1d x = 0 sin x N = 0 N
201 200 adantl φ x = 0 sin x N = 0 N
202 7 adantr φ x = 0 N
203 202 0expd φ x = 0 0 N = 0
204 201 203 eqtrd φ x = 0 sin x N = 0
205 204 oveq1d φ x = 0 sin x N cos x = 0 cos x
206 id x = 0 x = 0
207 0cn 0
208 206 207 eqeltrdi x = 0 x
209 coscl x cos x
210 209 negcld x cos x
211 208 210 syl x = 0 cos x
212 211 adantl φ x = 0 cos x
213 212 mul02d φ x = 0 0 cos x = 0
214 205 213 eqtrd φ x = 0 sin x N cos x = 0
215 fveq2 x = π sin x = sin π
216 sinpi sin π = 0
217 215 216 eqtrdi x = π sin x = 0
218 217 oveq1d x = π sin x N = 0 N
219 218 adantl φ x = π sin x N = 0 N
220 7 adantr φ x = π N
221 220 0expd φ x = π 0 N = 0
222 219 221 eqtrd φ x = π sin x N = 0
223 222 oveq1d φ x = π sin x N cos x = 0 cos x
224 id x = π x = π
225 picn π
226 224 225 eqeltrdi x = π x
227 226 coscld x = π cos x
228 227 negcld x = π cos x
229 228 adantl φ x = π cos x
230 229 mul02d φ x = π 0 cos x = 0
231 223 230 eqtrd φ x = π sin x N cos x = 0
232 11 13 16 42 57 83 84 106 123 184 196 214 231 itgparts φ 0 π sin x N sin x dx = 0 - 0 - 0 π N sin x N 1 cos x cos x dx
233 df-neg 0 π N sin x N 1 cos x cos x dx = 0 0 π N sin x N 1 cos x cos x dx
234 233 a1i φ 0 π N sin x N 1 cos x cos x dx = 0 0 π N sin x N 1 cos x cos x dx
235 9 232 234 3eqtr4a φ 0 π sin x N sin x dx = 0 π N sin x N 1 cos x cos x dx
236 79 81 81 mulassd φ x 0 π N sin x N 1 cos x cos x = N sin x N 1 cos x cos x
237 sqval cos x cos x 2 = cos x cos x
238 237 eqcomd cos x cos x cos x = cos x 2
239 80 238 syl x 0 π cos x cos x = cos x 2
240 239 adantl φ x 0 π cos x cos x = cos x 2
241 240 oveq2d φ x 0 π N sin x N 1 cos x cos x = N sin x N 1 cos x 2
242 80 sqcld x 0 π cos x 2
243 242 adantl φ x 0 π cos x 2
244 73 78 243 mulassd φ x 0 π N sin x N 1 cos x 2 = N sin x N 1 cos x 2
245 241 244 eqtrd φ x 0 π N sin x N 1 cos x cos x = N sin x N 1 cos x 2
246 78 243 mulcomd φ x 0 π sin x N 1 cos x 2 = cos x 2 sin x N 1
247 246 oveq2d φ x 0 π N sin x N 1 cos x 2 = N cos x 2 sin x N 1
248 236 245 247 3eqtrd φ x 0 π N sin x N 1 cos x cos x = N cos x 2 sin x N 1
249 248 negeqd φ x 0 π N sin x N 1 cos x cos x = N cos x 2 sin x N 1
250 82 81 mulneg2d φ x 0 π N sin x N 1 cos x cos x = N sin x N 1 cos x cos x
251 243 78 mulcld φ x 0 π cos x 2 sin x N 1
252 73 251 mulneg1d φ x 0 π -N cos x 2 sin x N 1 = N cos x 2 sin x N 1
253 249 250 252 3eqtr4d φ x 0 π N sin x N 1 cos x cos x = -N cos x 2 sin x N 1
254 253 itgeq2dv φ 0 π N sin x N 1 cos x cos x dx = 0 π -N cos x 2 sin x N 1 dx
255 59 negcld φ N
256 43 sqcld x 0 π cos x 2
257 256 adantl φ x 0 π cos x 2
258 257 109 mulcld φ x 0 π cos x 2 sin x N 1
259 6 fvmpt2 x cos x 2 sin x N 1 M x = cos x 2 sin x N 1
260 23 258 259 syl2anc φ x 0 π M x = cos x 2 sin x N 1
261 260 eqcomd φ x 0 π cos x 2 sin x N 1 = M x
262 261 mpteq2dva φ x 0 π cos x 2 sin x N 1 = x 0 π M x
263 nfmpt1 _ x x cos x 2 sin x N 1
264 6 263 nfcxfr _ x M
265 nfcv _ x cos
266 2nn0 2 0
267 266 a1i φ 2 0
268 265 53 267 expcnfg φ x cos x 2 : cn
269 268 63 mulcncf φ x cos x 2 sin x N 1 : cn
270 6 269 eqeltrid φ M : cn
271 264 270 40 cncfmptss φ x 0 π M x : 0 π cn
272 262 271 eqeltrd φ x 0 π cos x 2 sin x N 1 : 0 π cn
273 cniccibl 0 π x 0 π cos x 2 sin x N 1 : 0 π cn x 0 π cos x 2 sin x N 1 𝐿 1
274 11 13 272 273 syl3anc φ x 0 π cos x 2 sin x N 1 𝐿 1
275 86 88 258 274 iblss φ x 0 π cos x 2 sin x N 1 𝐿 1
276 255 251 275 itgmulc2 φ -N 0 π cos x 2 sin x N 1 dx = 0 π -N cos x 2 sin x N 1 dx
277 254 276 eqtr4d φ 0 π N sin x N 1 cos x cos x dx = -N 0 π cos x 2 sin x N 1 dx
278 277 negeqd φ 0 π N sin x N 1 cos x cos x dx = -N 0 π cos x 2 sin x N 1 dx
279 235 278 eqtrd φ 0 π sin x N sin x dx = -N 0 π cos x 2 sin x N 1 dx
280 251 275 itgcl φ 0 π cos x 2 sin x N 1 dx
281 59 280 mulneg1d φ -N 0 π cos x 2 sin x N 1 dx = N 0 π cos x 2 sin x N 1 dx
282 281 negeqd φ -N 0 π cos x 2 sin x N 1 dx = N 0 π cos x 2 sin x N 1 dx
283 59 280 mulcld φ N 0 π cos x 2 sin x N 1 dx
284 283 negnegd φ N 0 π cos x 2 sin x N 1 dx = N 0 π cos x 2 sin x N 1 dx
285 279 282 284 3eqtrd φ 0 π sin x N sin x dx = N 0 π cos x 2 sin x N 1 dx