Metamath Proof Explorer


Theorem iblioosinexp

Description: sin^n on an open integral is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Assertion iblioosinexp ABN0xABsinxN𝐿1

Proof

Step Hyp Ref Expression
1 ioossicc ABAB
2 1 a1i ABN0ABAB
3 ioombl ABdomvol
4 3 a1i ABN0ABdomvol
5 iccssre ABAB
6 ax-resscn
7 5 6 sstrdi ABAB
8 7 sselda ABxABx
9 8 3adantl3 ABN0xABx
10 9 sincld ABN0xABsinx
11 simpl3 ABN0xABN0
12 10 11 expcld ABN0xABsinxN
13 ibliccsinexp ABN0xABsinxN𝐿1
14 2 4 12 13 iblss ABN0xABsinxN𝐿1