iblioosinexp

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

		Ref	Expression
	Assertion	iblioosinexp	$⊢ (A \in ℝ \land B \in ℝ \land N \in ℕ_{0}) \to (x \in (A, B) ⟼ {\sin x}^{N}) \in 𝐿^{1}$

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

Metamath Proof Explorer