This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ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 )