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 
|- ( ( A e. RR /\ B e. RR /\ N e. NN0 ) -> ( x e. ( A (,) B ) |-> ( ( sin ` x ) ^ N ) ) e. L^1 )

Proof

Step Hyp Ref Expression
1 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
2 1 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ N e. NN0 ) -> ( A (,) B ) C_ ( A [,] B ) )
3 ioombl 
 |-  ( A (,) B ) e. dom vol
4 3 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ N e. NN0 ) -> ( A (,) B ) e. dom vol )
5 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
6 ax-resscn 
 |-  RR C_ CC
7 5 6 sstrdi 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ CC )
8 7 sselda 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ x e. ( A [,] B ) ) -> x e. CC )
9 8 3adantl3 
 |-  ( ( ( A e. RR /\ B e. RR /\ N e. NN0 ) /\ x e. ( A [,] B ) ) -> x e. CC )
10 9 sincld 
 |-  ( ( ( A e. RR /\ B e. RR /\ N e. NN0 ) /\ x e. ( A [,] B ) ) -> ( sin ` x ) e. CC )
11 simpl3 
 |-  ( ( ( A e. RR /\ B e. RR /\ N e. NN0 ) /\ x e. ( A [,] B ) ) -> N e. NN0 )
12 10 11 expcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ N e. NN0 ) /\ x e. ( A [,] B ) ) -> ( ( sin ` x ) ^ N ) e. CC )
13 ibliccsinexp 
 |-  ( ( A e. RR /\ B e. RR /\ N e. NN0 ) -> ( x e. ( A [,] B ) |-> ( ( sin ` x ) ^ N ) ) e. L^1 )
14 2 4 12 13 iblss 
 |-  ( ( A e. RR /\ B e. RR /\ N e. NN0 ) -> ( x e. ( A (,) B ) |-> ( ( sin ` x ) ^ N ) ) e. L^1 )