Metamath Proof Explorer

Theorem ibliccsinexp

Description: sin^n on a closed interval is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Assertion ibliccsinexp 
|- ( ( 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 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
2 ax-resscn 
 |-  RR C_ CC
3 1 2 sstrdi 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ CC )
4 3 sselda 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ x e. ( A [,] B ) ) -> x e. CC )
5 4 3adantl3 
 |-  ( ( ( A e. RR /\ B e. RR /\ N e. NN0 ) /\ x e. ( A [,] B ) ) -> x e. CC )
6 5 sincld 
 |-  ( ( ( A e. RR /\ B e. RR /\ N e. NN0 ) /\ x e. ( A [,] B ) ) -> ( sin ` x ) e. CC )
7 simpl3 
 |-  ( ( ( A e. RR /\ B e. RR /\ N e. NN0 ) /\ x e. ( A [,] B ) ) -> N e. NN0 )
8 6 7 expcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ N e. NN0 ) /\ x e. ( A [,] B ) ) -> ( ( sin ` x ) ^ N ) e. CC )
9 eqid 
 |-  ( x e. CC |-> ( ( sin ` x ) ^ N ) ) = ( x e. CC |-> ( ( sin ` x ) ^ N ) )
10 9 fvmpt2 
 |-  ( ( x e. CC /\ ( ( sin ` x ) ^ N ) e. CC ) -> ( ( x e. CC |-> ( ( sin ` x ) ^ N ) ) ` x ) = ( ( sin ` x ) ^ N ) )
11 5 8 10 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ N e. NN0 ) /\ x e. ( A [,] B ) ) -> ( ( x e. CC |-> ( ( sin ` x ) ^ N ) ) ` x ) = ( ( sin ` x ) ^ N ) )
12 11 eqcomd 
 |-  ( ( ( A e. RR /\ B e. RR /\ N e. NN0 ) /\ x e. ( A [,] B ) ) -> ( ( sin ` x ) ^ N ) = ( ( x e. CC |-> ( ( sin ` x ) ^ N ) ) ` x ) )
13 12 mpteq2dva 
 |-  ( ( A e. RR /\ B e. RR /\ N e. NN0 ) -> ( x e. ( A [,] B ) |-> ( ( sin ` x ) ^ N ) ) = ( x e. ( A [,] B ) |-> ( ( x e. CC |-> ( ( sin ` x ) ^ N ) ) ` x ) ) )
14 nfmpt1 
 |-  F/_ x ( x e. CC |-> ( ( sin ` x ) ^ N ) )
15 nfcv 
 |-  F/_ x sin
16 sincn 
 |-  sin e. ( CC -cn-> CC )
17 16 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ N e. NN0 ) -> sin e. ( CC -cn-> CC ) )
18 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ N e. NN0 ) -> N e. NN0 )
19 15 17 18 expcnfg 
 |-  ( ( A e. RR /\ B e. RR /\ N e. NN0 ) -> ( x e. CC |-> ( ( sin ` x ) ^ N ) ) e. ( CC -cn-> CC ) )
20 3 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ N e. NN0 ) -> ( A [,] B ) C_ CC )
21 14 19 20 cncfmptss 
 |-  ( ( A e. RR /\ B e. RR /\ N e. NN0 ) -> ( x e. ( A [,] B ) |-> ( ( x e. CC |-> ( ( sin ` x ) ^ N ) ) ` x ) ) e. ( ( A [,] B ) -cn-> CC ) )
22 13 21 eqeltrd 
 |-  ( ( A e. RR /\ B e. RR /\ N e. NN0 ) -> ( x e. ( A [,] B ) |-> ( ( sin ` x ) ^ N ) ) e. ( ( A [,] B ) -cn-> CC ) )
23 cniccibl 
 |-  ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> ( ( sin ` x ) ^ N ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( x e. ( A [,] B ) |-> ( ( sin ` x ) ^ N ) ) e. L^1 )
24 22 23 syld3an3 
 |-  ( ( A e. RR /\ B e. RR /\ N e. NN0 ) -> ( x e. ( A [,] B ) |-> ( ( sin ` x ) ^ N ) ) e. L^1 )