ibliccsinexp

Description: sin^n on a closed interval is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017)

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

Proof

Step	Hyp	Ref	Expression
1		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
2		ax-resscn	$⊢ ℝ \subseteq ℂ$
3	1 2	sstrdi	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℂ$
4	3	sselda	$⊢ ((A \in ℝ \land B \in ℝ) \land x \in [A, B]) \to x \in ℂ$
5	4	3adantl3	$⊢ ((A \in ℝ \land B \in ℝ \land N \in ℕ_{0}) \land x \in [A, B]) \to x \in ℂ$
6	5	sincld	$⊢ ((A \in ℝ \land B \in ℝ \land N \in ℕ_{0}) \land x \in [A, B]) \to \sin x \in ℂ$
7		simpl3	$⊢ ((A \in ℝ \land B \in ℝ \land N \in ℕ_{0}) \land x \in [A, B]) \to N \in ℕ_{0}$
8	6 7	expcld	$⊢ ((A \in ℝ \land B \in ℝ \land N \in ℕ_{0}) \land x \in [A, B]) \to {\sin x}^{N} \in ℂ$
9		eqid	$⊢ (x \in ℂ ⟼ {\sin x}^{N}) = (x \in ℂ ⟼ {\sin x}^{N})$
10	9	fvmpt2	$⊢ (x \in ℂ \land {\sin x}^{N} \in ℂ) \to (x \in ℂ ⟼ {\sin x}^{N}) (x) = {\sin x}^{N}$
11	5 8 10	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ \land N \in ℕ_{0}) \land x \in [A, B]) \to (x \in ℂ ⟼ {\sin x}^{N}) (x) = {\sin x}^{N}$
12	11	eqcomd	$⊢ ((A \in ℝ \land B \in ℝ \land N \in ℕ_{0}) \land x \in [A, B]) \to {\sin x}^{N} = (x \in ℂ ⟼ {\sin x}^{N}) (x)$
13	12	mpteq2dva	$⊢ (A \in ℝ \land B \in ℝ \land N \in ℕ_{0}) \to (x \in [A, B] ⟼ {\sin x}^{N}) = (x \in [A, B] ⟼ (x \in ℂ ⟼ {\sin x}^{N}) (x))$
14		nfmpt1	$⊢ \underline{Ⅎ} x (x \in ℂ ⟼ {\sin x}^{N})$
15		nfcv	$⊢ \underline{Ⅎ} x \sin$
16		sincn	$⊢ \sin : ℂ \underset{cn}{⟶} ℂ$
17	16	a1i	$⊢ (A \in ℝ \land B \in ℝ \land N \in ℕ_{0}) \to \sin : ℂ \underset{cn}{⟶} ℂ$
18		simp3	$⊢ (A \in ℝ \land B \in ℝ \land N \in ℕ_{0}) \to N \in ℕ_{0}$
19	15 17 18	expcnfg	$⊢ (A \in ℝ \land B \in ℝ \land N \in ℕ_{0}) \to (x \in ℂ ⟼ {\sin x}^{N}) : ℂ \underset{cn}{⟶} ℂ$
20	3	3adant3	$⊢ (A \in ℝ \land B \in ℝ \land N \in ℕ_{0}) \to [A, B] \subseteq ℂ$
21	14 19 20	cncfmptss	$⊢ (A \in ℝ \land B \in ℝ \land N \in ℕ_{0}) \to (x \in [A, B] ⟼ (x \in ℂ ⟼ {\sin x}^{N}) (x)) : [A, B] \underset{cn}{⟶} ℂ$
22	13 21	eqeltrd	$⊢ (A \in ℝ \land B \in ℝ \land N \in ℕ_{0}) \to (x \in [A, B] ⟼ {\sin x}^{N}) : [A, B] \underset{cn}{⟶} ℂ$
23		cniccibl	$⊢ (A \in ℝ \land B \in ℝ \land (x \in [A, B] ⟼ {\sin x}^{N}) : [A, B] \underset{cn}{⟶} ℂ) \to (x \in [A, B] ⟼ {\sin x}^{N}) \in 𝐿^{1}$
24	22 23	syld3an3	$⊢ (A \in ℝ \land B \in ℝ \land N \in ℕ_{0}) \to (x \in [A, B] ⟼ {\sin x}^{N}) \in 𝐿^{1}$

Metamath Proof Explorer

Theorem ibliccsinexp

Proof