Theorem iblioosinexp

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

	Ref	Expression
Assertion	iblioosinexp	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ) ∈ 𝐿1 )

Proof

Step	Hyp	Ref	Expression
1		ioossicc	⊢ ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 )
2	1	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 (,) 𝐵 ) ⊆ ( 𝐴 [,] 𝐵 ) )
3		ioombl	⊢ ( 𝐴 (,) 𝐵 ) ∈ dom vol
4	3	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 (,) 𝐵 ) ∈ dom vol )
5		iccssre	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
6		ax-resscn	⊢ ℝ ⊆ ℂ
7	5 6	sstrdi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
8	7	sselda	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℂ )
9	8	3adantl3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℂ )
10	9	sincld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( sin ‘ 𝑥 ) ∈ ℂ )
11		simpl3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑁 ∈ ℕ0 )
12	10 11	expcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ∈ ℂ )
13		ibliccsinexp	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ) ∈ 𝐿1 )
14	2 4 12 13	iblss	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ) ∈ 𝐿1 )