# 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 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {N}\in {ℕ}_{0}\right)\to \left({x}\in \left({A},{B}\right)⟼{\mathrm{sin}{x}}^{{N}}\right)\in {𝐿}^{1}$

### Proof

Step Hyp Ref Expression
1 ioossicc ${⊢}\left({A},{B}\right)\subseteq \left[{A},{B}\right]$
2 1 a1i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {N}\in {ℕ}_{0}\right)\to \left({A},{B}\right)\subseteq \left[{A},{B}\right]$
3 ioombl ${⊢}\left({A},{B}\right)\in \mathrm{dom}vol$
4 3 a1i ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {N}\in {ℕ}_{0}\right)\to \left({A},{B}\right)\in \mathrm{dom}vol$
5 iccssre ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left[{A},{B}\right]\subseteq ℝ$
6 ax-resscn ${⊢}ℝ\subseteq ℂ$
7 5 6 sstrdi ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left[{A},{B}\right]\subseteq ℂ$
8 7 sselda ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {x}\in \left[{A},{B}\right]\right)\to {x}\in ℂ$
9 8 3adantl3 ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {N}\in {ℕ}_{0}\right)\wedge {x}\in \left[{A},{B}\right]\right)\to {x}\in ℂ$
10 9 sincld ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {N}\in {ℕ}_{0}\right)\wedge {x}\in \left[{A},{B}\right]\right)\to \mathrm{sin}{x}\in ℂ$
11 simpl3 ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {N}\in {ℕ}_{0}\right)\wedge {x}\in \left[{A},{B}\right]\right)\to {N}\in {ℕ}_{0}$
12 10 11 expcld ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\wedge {N}\in {ℕ}_{0}\right)\wedge {x}\in \left[{A},{B}\right]\right)\to {\mathrm{sin}{x}}^{{N}}\in ℂ$
13 ibliccsinexp ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {N}\in {ℕ}_{0}\right)\to \left({x}\in \left[{A},{B}\right]⟼{\mathrm{sin}{x}}^{{N}}\right)\in {𝐿}^{1}$
14 2 4 12 13 iblss ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {N}\in {ℕ}_{0}\right)\to \left({x}\in \left({A},{B}\right)⟼{\mathrm{sin}{x}}^{{N}}\right)\in {𝐿}^{1}$