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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ) ∈ 𝐿1 )

Proof

Step Hyp Ref Expression
1 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
2 ax-resscn ⊢ ℝ ⊆ ℂ
3 1 2 sstrdi ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
4 3 sselda ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℂ )
5 4 3adantl3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥 ∈ ℂ )
6 5 sincld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( sin ‘ 𝑥 ) ∈ ℂ )
7 simpl3 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑁 ∈ ℕ0 )
8 6 7 expcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ∈ ℂ )
9 eqid ⊢ ( 𝑥 ∈ ℂ ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ) = ( 𝑥 ∈ ℂ ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) )
10 9 fvmpt2 ⊢ ( ( 𝑥 ∈ ℂ ∧ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ∈ ℂ ) → ( ( 𝑥 ∈ ℂ ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ) ‘ 𝑥 ) = ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) )
11 5 8 10 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( 𝑥 ∈ ℂ ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ) ‘ 𝑥 ) = ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) )
12 11 eqcomd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) = ( ( 𝑥 ∈ ℂ ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ) ‘ 𝑥 ) )
13 12 mpteq2dva ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝑥 ∈ ℂ ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ) ‘ 𝑥 ) ) )
14 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ℂ ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) )
15 nfcv ⊢ Ⅎ 𝑥 sin
16 sincn ⊢ sin ∈ ( ℂ –cn→ ℂ )
17 16 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → sin ∈ ( ℂ –cn→ ℂ ) )
18 simp3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → 𝑁 ∈ ℕ0 )
19 15 17 18 expcnfg ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ ℂ ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ) ∈ ( ℂ –cn→ ℂ ) )
20 3 3adant3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
21 14 19 20 cncfmptss ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( 𝑥 ∈ ℂ ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ) ‘ 𝑥 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
22 13 21 eqeltrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
23 cniccibl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ) ∈ 𝐿1 )
24 22 23 syld3an3 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ) ∈ 𝐿1 )