itgsinexplem1

Description: Integration by parts is applied to integrate sin^(N+1). (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	itgsinexplem1.1	$⊢ F = (x \in ℂ ⟼ {\sin x}^{N})$
	itgsinexplem1.2	$⊢ G = (x \in ℂ ⟼ - \cos x)$
	itgsinexplem1.3	$⊢ H = (x \in ℂ ⟼ N {\sin x}^{N - 1} \cos x)$
	itgsinexplem1.4	$⊢ I = (x \in ℂ ⟼ {\sin x}^{N} \sin x)$
	itgsinexplem1.5	$⊢ L = (x \in ℂ ⟼ N {\sin x}^{N - 1} \cos x (- \cos x))$
	itgsinexplem1.6	$⊢ M = (x \in ℂ ⟼ {\cos x}^{2} {\sin x}^{N - 1})$
	itgsinexplem1.7	$⊢ φ \to N \in ℕ$
Assertion	itgsinexplem1	$⊢ φ \to \int_{(0, π)} {\sin x}^{N} \sin x d x = N \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 1} d x$

Proof

Step	Hyp	Ref	Expression
1		itgsinexplem1.1	$⊢ F = (x \in ℂ ⟼ {\sin x}^{N})$
2		itgsinexplem1.2	$⊢ G = (x \in ℂ ⟼ - \cos x)$
3		itgsinexplem1.3	$⊢ H = (x \in ℂ ⟼ N {\sin x}^{N - 1} \cos x)$
4		itgsinexplem1.4	$⊢ I = (x \in ℂ ⟼ {\sin x}^{N} \sin x)$
5		itgsinexplem1.5	$⊢ L = (x \in ℂ ⟼ N {\sin x}^{N - 1} \cos x (- \cos x))$
6		itgsinexplem1.6	$⊢ M = (x \in ℂ ⟼ {\cos x}^{2} {\sin x}^{N - 1})$
7		itgsinexplem1.7	$⊢ φ \to N \in ℕ$
8		0m0e0	$⊢ 0 - 0 = 0$
9	8	oveq1i	$⊢ 0 - 0 - \int_{(0, π)} N {\sin x}^{N - 1} \cos x (- \cos x) d x = 0 - \int_{(0, π)} N {\sin x}^{N - 1} \cos x (- \cos x) d x$
10		0re	$⊢ 0 \in ℝ$
11	10	a1i	$⊢ φ \to 0 \in ℝ$
12		pire	$⊢ π \in ℝ$
13	12	a1i	$⊢ φ \to π \in ℝ$
14		pipos	$⊢ 0 < π$
15	10 12 14	ltleii	$⊢ 0 \leq π$
16	15	a1i	$⊢ φ \to 0 \leq π$
17	10 12	pm3.2i	$⊢ (0 \in ℝ \land π \in ℝ)$
18		iccssre	$⊢ (0 \in ℝ \land π \in ℝ) \to [0, π] \subseteq ℝ$
19	17 18	ax-mp	$⊢ [0, π] \subseteq ℝ$
20		ax-resscn	$⊢ ℝ \subseteq ℂ$
21	19 20	sstri	$⊢ [0, π] \subseteq ℂ$
22	21	sseli	$⊢ x \in [0, π] \to x \in ℂ$
23	22	adantl	$⊢ (φ \land x \in [0, π]) \to x \in ℂ$
24	22	sincld	$⊢ x \in [0, π] \to \sin x \in ℂ$
25	24	adantl	$⊢ (φ \land x \in [0, π]) \to \sin x \in ℂ$
26	7	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
27	26	adantr	$⊢ (φ \land x \in [0, π]) \to N \in ℕ_{0}$
28	25 27	expcld	$⊢ (φ \land x \in [0, π]) \to {\sin x}^{N} \in ℂ$
29	1	fvmpt2	$⊢ (x \in ℂ \land {\sin x}^{N} \in ℂ) \to F (x) = {\sin x}^{N}$
30	23 28 29	syl2anc	$⊢ (φ \land x \in [0, π]) \to F (x) = {\sin x}^{N}$
31	30	eqcomd	$⊢ (φ \land x \in [0, π]) \to {\sin x}^{N} = F (x)$
32	31	mpteq2dva	$⊢ φ \to (x \in [0, π] ⟼ {\sin x}^{N}) = (x \in [0, π] ⟼ F (x))$
33		nfmpt1	$⊢ \underline{Ⅎ} x (x \in ℂ ⟼ {\sin x}^{N})$
34	1 33	nfcxfr	$⊢ \underline{Ⅎ} x F$
35		nfcv	$⊢ \underline{Ⅎ} x \sin$
36		sincn	$⊢ \sin : ℂ \underset{cn}{⟶} ℂ$
37	36	a1i	$⊢ φ \to \sin : ℂ \underset{cn}{⟶} ℂ$
38	35 37 26	expcnfg	$⊢ φ \to (x \in ℂ ⟼ {\sin x}^{N}) : ℂ \underset{cn}{⟶} ℂ$
39	1 38	eqeltrid	$⊢ φ \to F : ℂ \underset{cn}{⟶} ℂ$
40	21	a1i	$⊢ φ \to [0, π] \subseteq ℂ$
41	34 39 40	cncfmptss	$⊢ φ \to (x \in [0, π] ⟼ F (x)) : [0, π] \underset{cn}{⟶} ℂ$
42	32 41	eqeltrd	$⊢ φ \to (x \in [0, π] ⟼ {\sin x}^{N}) : [0, π] \underset{cn}{⟶} ℂ$
43	22	coscld	$⊢ x \in [0, π] \to \cos x \in ℂ$
44	43	negcld	$⊢ x \in [0, π] \to - \cos x \in ℂ$
45	2	fvmpt2	$⊢ (x \in ℂ \land - \cos x \in ℂ) \to G (x) = - \cos x$
46	22 44 45	syl2anc	$⊢ x \in [0, π] \to G (x) = - \cos x$
47	46	eqcomd	$⊢ x \in [0, π] \to - \cos x = G (x)$
48	47	adantl	$⊢ (φ \land x \in [0, π]) \to - \cos x = G (x)$
49	48	mpteq2dva	$⊢ φ \to (x \in [0, π] ⟼ - \cos x) = (x \in [0, π] ⟼ G (x))$
50		nfmpt1	$⊢ \underline{Ⅎ} x (x \in ℂ ⟼ - \cos x)$
51	2 50	nfcxfr	$⊢ \underline{Ⅎ} x G$
52		coscn	$⊢ \cos : ℂ \underset{cn}{⟶} ℂ$
53	52	a1i	$⊢ φ \to \cos : ℂ \underset{cn}{⟶} ℂ$
54	2	negfcncf	$⊢ \cos : ℂ \underset{cn}{⟶} ℂ \to G : ℂ \underset{cn}{⟶} ℂ$
55	53 54	syl	$⊢ φ \to G : ℂ \underset{cn}{⟶} ℂ$
56	51 55 40	cncfmptss	$⊢ φ \to (x \in [0, π] ⟼ G (x)) : [0, π] \underset{cn}{⟶} ℂ$
57	49 56	eqeltrd	$⊢ φ \to (x \in [0, π] ⟼ - \cos x) : [0, π] \underset{cn}{⟶} ℂ$
58		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
59	7	nncnd	$⊢ φ \to N \in ℂ$
60	58 59 58	constcncfg	$⊢ φ \to (x \in ℂ ⟼ N) : ℂ \underset{cn}{⟶} ℂ$
61		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
62	7 61	syl	$⊢ φ \to N - 1 \in ℕ_{0}$
63	35 37 62	expcnfg	$⊢ φ \to (x \in ℂ ⟼ {\sin x}^{N - 1}) : ℂ \underset{cn}{⟶} ℂ$
64	60 63	mulcncf	$⊢ φ \to (x \in ℂ ⟼ N {\sin x}^{N - 1}) : ℂ \underset{cn}{⟶} ℂ$
65		cosf	$⊢ \cos : ℂ ⟶ ℂ$
66	65	a1i	$⊢ φ \to \cos : ℂ ⟶ ℂ$
67	66	feqmptd	$⊢ φ \to \cos = (x \in ℂ ⟼ \cos x)$
68	67 52	eqeltrrdi	$⊢ φ \to (x \in ℂ ⟼ \cos x) : ℂ \underset{cn}{⟶} ℂ$
69	64 68	mulcncf	$⊢ φ \to (x \in ℂ ⟼ N {\sin x}^{N - 1} \cos x) : ℂ \underset{cn}{⟶} ℂ$
70	3 69	eqeltrid	$⊢ φ \to H : ℂ \underset{cn}{⟶} ℂ$
71		ioosscn	$⊢ (0, π) \subseteq ℂ$
72	71	a1i	$⊢ φ \to (0, π) \subseteq ℂ$
73	59	adantr	$⊢ (φ \land x \in (0, π)) \to N \in ℂ$
74	71	sseli	$⊢ x \in (0, π) \to x \in ℂ$
75	74	sincld	$⊢ x \in (0, π) \to \sin x \in ℂ$
76	75	adantl	$⊢ (φ \land x \in (0, π)) \to \sin x \in ℂ$
77	62	adantr	$⊢ (φ \land x \in (0, π)) \to N - 1 \in ℕ_{0}$
78	76 77	expcld	$⊢ (φ \land x \in (0, π)) \to {\sin x}^{N - 1} \in ℂ$
79	73 78	mulcld	$⊢ (φ \land x \in (0, π)) \to N {\sin x}^{N - 1} \in ℂ$
80	74	coscld	$⊢ x \in (0, π) \to \cos x \in ℂ$
81	80	adantl	$⊢ (φ \land x \in (0, π)) \to \cos x \in ℂ$
82	79 81	mulcld	$⊢ (φ \land x \in (0, π)) \to N {\sin x}^{N - 1} \cos x \in ℂ$
83	3 70 72 58 82	cncfmptssg	$⊢ φ \to (x \in (0, π) ⟼ N {\sin x}^{N - 1} \cos x) : (0, π) \underset{cn}{⟶} ℂ$
84	35 37 72	cncfmptss	$⊢ φ \to (x \in (0, π) ⟼ \sin x) : (0, π) \underset{cn}{⟶} ℂ$
85		ioossicc	$⊢ (0, π) \subseteq [0, π]$
86	85	a1i	$⊢ φ \to (0, π) \subseteq [0, π]$
87		ioombl	$⊢ (0, π) \in dom vol$
88	87	a1i	$⊢ φ \to (0, π) \in dom vol$
89	28 25	mulcld	$⊢ (φ \land x \in [0, π]) \to {\sin x}^{N} \sin x \in ℂ$
90	4	fvmpt2	$⊢ (x \in ℂ \land {\sin x}^{N} \sin x \in ℂ) \to I (x) = {\sin x}^{N} \sin x$
91	23 89 90	syl2anc	$⊢ (φ \land x \in [0, π]) \to I (x) = {\sin x}^{N} \sin x$
92	91	eqcomd	$⊢ (φ \land x \in [0, π]) \to {\sin x}^{N} \sin x = I (x)$
93	92	mpteq2dva	$⊢ φ \to (x \in [0, π] ⟼ {\sin x}^{N} \sin x) = (x \in [0, π] ⟼ I (x))$
94		nfmpt1	$⊢ \underline{Ⅎ} x (x \in ℂ ⟼ {\sin x}^{N} \sin x)$
95	4 94	nfcxfr	$⊢ \underline{Ⅎ} x I$
96		sinf	$⊢ \sin : ℂ ⟶ ℂ$
97	96	a1i	$⊢ φ \to \sin : ℂ ⟶ ℂ$
98	97	feqmptd	$⊢ φ \to \sin = (x \in ℂ ⟼ \sin x)$
99	98 36	eqeltrrdi	$⊢ φ \to (x \in ℂ ⟼ \sin x) : ℂ \underset{cn}{⟶} ℂ$
100	38 99	mulcncf	$⊢ φ \to (x \in ℂ ⟼ {\sin x}^{N} \sin x) : ℂ \underset{cn}{⟶} ℂ$
101	4 100	eqeltrid	$⊢ φ \to I : ℂ \underset{cn}{⟶} ℂ$
102	95 101 40	cncfmptss	$⊢ φ \to (x \in [0, π] ⟼ I (x)) : [0, π] \underset{cn}{⟶} ℂ$
103	93 102	eqeltrd	$⊢ φ \to (x \in [0, π] ⟼ {\sin x}^{N} \sin x) : [0, π] \underset{cn}{⟶} ℂ$
104		cniccibl	$⊢ (0 \in ℝ \land π \in ℝ \land (x \in [0, π] ⟼ {\sin x}^{N} \sin x) : [0, π] \underset{cn}{⟶} ℂ) \to (x \in [0, π] ⟼ {\sin x}^{N} \sin x) \in 𝐿^{1}$
105	11 13 103 104	syl3anc	$⊢ φ \to (x \in [0, π] ⟼ {\sin x}^{N} \sin x) \in 𝐿^{1}$
106	86 88 89 105	iblss	$⊢ φ \to (x \in (0, π) ⟼ {\sin x}^{N} \sin x) \in 𝐿^{1}$
107	59	adantr	$⊢ (φ \land x \in [0, π]) \to N \in ℂ$
108	62	adantr	$⊢ (φ \land x \in [0, π]) \to N - 1 \in ℕ_{0}$
109	25 108	expcld	$⊢ (φ \land x \in [0, π]) \to {\sin x}^{N - 1} \in ℂ$
110	107 109	mulcld	$⊢ (φ \land x \in [0, π]) \to N {\sin x}^{N - 1} \in ℂ$
111	43	adantl	$⊢ (φ \land x \in [0, π]) \to \cos x \in ℂ$
112	110 111	mulcld	$⊢ (φ \land x \in [0, π]) \to N {\sin x}^{N - 1} \cos x \in ℂ$
113	44	adantl	$⊢ (φ \land x \in [0, π]) \to - \cos x \in ℂ$
114	112 113	mulcld	$⊢ (φ \land x \in [0, π]) \to N {\sin x}^{N - 1} \cos x (- \cos x) \in ℂ$
115		eqid	$⊢ (x \in ℂ ⟼ - \cos x) = (x \in ℂ ⟼ - \cos x)$
116	115	negfcncf	$⊢ \cos : ℂ \underset{cn}{⟶} ℂ \to (x \in ℂ ⟼ - \cos x) : ℂ \underset{cn}{⟶} ℂ$
117	53 116	syl	$⊢ φ \to (x \in ℂ ⟼ - \cos x) : ℂ \underset{cn}{⟶} ℂ$
118	69 117	mulcncf	$⊢ φ \to (x \in ℂ ⟼ N {\sin x}^{N - 1} \cos x (- \cos x)) : ℂ \underset{cn}{⟶} ℂ$
119	5 118	eqeltrid	$⊢ φ \to L : ℂ \underset{cn}{⟶} ℂ$
120	5 119 40 58 114	cncfmptssg	$⊢ φ \to (x \in [0, π] ⟼ N {\sin x}^{N - 1} \cos x (- \cos x)) : [0, π] \underset{cn}{⟶} ℂ$
121		cniccibl	$⊢ (0 \in ℝ \land π \in ℝ \land (x \in [0, π] ⟼ N {\sin x}^{N - 1} \cos x (- \cos x)) : [0, π] \underset{cn}{⟶} ℂ) \to (x \in [0, π] ⟼ N {\sin x}^{N - 1} \cos x (- \cos x)) \in 𝐿^{1}$
122	11 13 120 121	syl3anc	$⊢ φ \to (x \in [0, π] ⟼ N {\sin x}^{N - 1} \cos x (- \cos x)) \in 𝐿^{1}$
123	86 88 114 122	iblss	$⊢ φ \to (x \in (0, π) ⟼ N {\sin x}^{N - 1} \cos x (- \cos x)) \in 𝐿^{1}$
124		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
125	124	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
126		recn	$⊢ x \in ℝ \to x \in ℂ$
127	126	sincld	$⊢ x \in ℝ \to \sin x \in ℂ$
128	127	adantl	$⊢ (φ \land x \in ℝ) \to \sin x \in ℂ$
129	26	adantr	$⊢ (φ \land x \in ℝ) \to N \in ℕ_{0}$
130	128 129	expcld	$⊢ (φ \land x \in ℝ) \to {\sin x}^{N} \in ℂ$
131	59	adantr	$⊢ (φ \land x \in ℝ) \to N \in ℂ$
132	62	adantr	$⊢ (φ \land x \in ℝ) \to N - 1 \in ℕ_{0}$
133	128 132	expcld	$⊢ (φ \land x \in ℝ) \to {\sin x}^{N - 1} \in ℂ$
134	131 133	mulcld	$⊢ (φ \land x \in ℝ) \to N {\sin x}^{N - 1} \in ℂ$
135	126	coscld	$⊢ x \in ℝ \to \cos x \in ℂ$
136	135	adantl	$⊢ (φ \land x \in ℝ) \to \cos x \in ℂ$
137	134 136	mulcld	$⊢ (φ \land x \in ℝ) \to N {\sin x}^{N - 1} \cos x \in ℂ$
138		sincl	$⊢ x \in ℂ \to \sin x \in ℂ$
139	138	adantl	$⊢ (φ \land x \in ℂ) \to \sin x \in ℂ$
140	26	adantr	$⊢ (φ \land x \in ℂ) \to N \in ℕ_{0}$
141	139 140	expcld	$⊢ (φ \land x \in ℂ) \to {\sin x}^{N} \in ℂ$
142	141 1	fmptd	$⊢ φ \to F : ℂ ⟶ ℂ$
143	126	adantl	$⊢ (φ \land x \in ℝ) \to x \in ℂ$
144		elex	$⊢ N {\sin x}^{N - 1} \cos x \in ℂ \to N {\sin x}^{N - 1} \cos x \in V$
145	137 144	syl	$⊢ (φ \land x \in ℝ) \to N {\sin x}^{N - 1} \cos x \in V$
146		rabid	$⊢ x \in \{x \in ℂ \| N {\sin x}^{N - 1} \cos x \in V\} \leftrightarrow (x \in ℂ \land N {\sin x}^{N - 1} \cos x \in V)$
147	143 145 146	sylanbrc	$⊢ (φ \land x \in ℝ) \to x \in \{x \in ℂ \| N {\sin x}^{N - 1} \cos x \in V\}$
148	3	dmmpt	$⊢ dom H = \{x \in ℂ \| N {\sin x}^{N - 1} \cos x \in V\}$
149	147 148	eleqtrrdi	$⊢ (φ \land x \in ℝ) \to x \in dom H$
150	149	ex	$⊢ φ \to (x \in ℝ \to x \in dom H)$
151	150	alrimiv	$⊢ φ \to \forall x (x \in ℝ \to x \in dom H)$
152		nfcv	$⊢ \underline{Ⅎ} x ℝ$
153		nfmpt1	$⊢ \underline{Ⅎ} x (x \in ℂ ⟼ N {\sin x}^{N - 1} \cos x)$
154	3 153	nfcxfr	$⊢ \underline{Ⅎ} x H$
155	154	nfdm	$⊢ \underline{Ⅎ} x dom H$
156	152 155	dfss2f	$⊢ ℝ \subseteq dom H \leftrightarrow \forall x (x \in ℝ \to x \in dom H)$
157	151 156	sylibr	$⊢ φ \to ℝ \subseteq dom H$
158	7	dvsinexp	$⊢ φ \to \frac{d (x \in ℂ⟼ {\sin x}^{N})}{d_{ℂ} x} = (x \in ℂ ⟼ N {\sin x}^{N - 1} \cos x)$
159	1	oveq2i	$⊢ ℂ D F = \frac{d (x \in ℂ⟼ {\sin x}^{N})}{d_{ℂ} x}$
160	158 159 3	3eqtr4g	$⊢ φ \to ℂ D F = H$
161	160	dmeqd	$⊢ φ \to dom F_{ℂ}^{'} = dom H$
162	157 161	sseqtrrd	$⊢ φ \to ℝ \subseteq dom F_{ℂ}^{'}$
163		dvres3	$⊢ ((ℝ \in \{ℝ, ℂ\} \land F : ℂ ⟶ ℂ) \land (ℂ \subseteq ℂ \land ℝ \subseteq dom F_{ℂ}^{'})) \to ℝ D ({F ↾}_{ℝ}) = {F_{ℂ}^{'} ↾}_{ℝ}$
164	125 142 58 162 163	syl22anc	$⊢ φ \to ℝ D ({F ↾}_{ℝ}) = {F_{ℂ}^{'} ↾}_{ℝ}$
165	1	reseq1i	$⊢ {F ↾}_{ℝ} = {(x \in ℂ ⟼ {\sin x}^{N}) ↾}_{ℝ}$
166		resmpt	$⊢ ℝ \subseteq ℂ \to {(x \in ℂ ⟼ {\sin x}^{N}) ↾}_{ℝ} = (x \in ℝ ⟼ {\sin x}^{N})$
167	20 166	ax-mp	$⊢ {(x \in ℂ ⟼ {\sin x}^{N}) ↾}_{ℝ} = (x \in ℝ ⟼ {\sin x}^{N})$
168	165 167	eqtri	$⊢ {F ↾}_{ℝ} = (x \in ℝ ⟼ {\sin x}^{N})$
169	168	oveq2i	$⊢ ℝ D ({F ↾}_{ℝ}) = \frac{d (x \in ℝ⟼ {\sin x}^{N})}{d_{ℝ} x}$
170	169	a1i	$⊢ φ \to ℝ D ({F ↾}_{ℝ}) = \frac{d (x \in ℝ⟼ {\sin x}^{N})}{d_{ℝ} x}$
171	160	reseq1d	$⊢ φ \to {F_{ℂ}^{'} ↾}_{ℝ} = {H ↾}_{ℝ}$
172	3	reseq1i	$⊢ {H ↾}_{ℝ} = {(x \in ℂ ⟼ N {\sin x}^{N - 1} \cos x) ↾}_{ℝ}$
173		resmpt	$⊢ ℝ \subseteq ℂ \to {(x \in ℂ ⟼ N {\sin x}^{N - 1} \cos x) ↾}_{ℝ} = (x \in ℝ ⟼ N {\sin x}^{N - 1} \cos x)$
174	20 173	ax-mp	$⊢ {(x \in ℂ ⟼ N {\sin x}^{N - 1} \cos x) ↾}_{ℝ} = (x \in ℝ ⟼ N {\sin x}^{N - 1} \cos x)$
175	172 174	eqtri	$⊢ {H ↾}_{ℝ} = (x \in ℝ ⟼ N {\sin x}^{N - 1} \cos x)$
176	171 175	eqtrdi	$⊢ φ \to {F_{ℂ}^{'} ↾}_{ℝ} = (x \in ℝ ⟼ N {\sin x}^{N - 1} \cos x)$
177	164 170 176	3eqtr3d	$⊢ φ \to \frac{d (x \in ℝ⟼ {\sin x}^{N})}{d_{ℝ} x} = (x \in ℝ ⟼ N {\sin x}^{N - 1} \cos x)$
178	19	a1i	$⊢ φ \to [0, π] \subseteq ℝ$
179		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
180	179	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
181	17	a1i	$⊢ φ \to (0 \in ℝ \land π \in ℝ)$
182		iccntr	$⊢ (0 \in ℝ \land π \in ℝ) \to int (topGen (ran (.))) ([0, π]) = (0, π)$
183	181 182	syl	$⊢ φ \to int (topGen (ran (.))) ([0, π]) = (0, π)$
184	125 130 137 177 178 180 179 183	dvmptres2	$⊢ φ \to \frac{d (x \in [0, π]⟼ {\sin x}^{N})}{d_{ℝ} x} = (x \in (0, π) ⟼ N {\sin x}^{N - 1} \cos x)$
185	135	negcld	$⊢ x \in ℝ \to - \cos x \in ℂ$
186	185	adantl	$⊢ (φ \land x \in ℝ) \to - \cos x \in ℂ$
187	127	negcld	$⊢ x \in ℝ \to - \sin x \in ℂ$
188	187	adantl	$⊢ (φ \land x \in ℝ) \to - \sin x \in ℂ$
189		dvcosre	$⊢ \frac{d (x \in ℝ⟼ \cos x)}{d_{ℝ} x} = (x \in ℝ ⟼ - \sin x)$
190	189	a1i	$⊢ φ \to \frac{d (x \in ℝ⟼ \cos x)}{d_{ℝ} x} = (x \in ℝ ⟼ - \sin x)$
191	125 136 188 190	dvmptneg	$⊢ φ \to \frac{d (x \in ℝ⟼ - \cos x)}{d_{ℝ} x} = (x \in ℝ ⟼ - (- \sin x))$
192	127	negnegd	$⊢ x \in ℝ \to - (- \sin x) = \sin x$
193	192	adantl	$⊢ (φ \land x \in ℝ) \to - (- \sin x) = \sin x$
194	193	mpteq2dva	$⊢ φ \to (x \in ℝ ⟼ - (- \sin x)) = (x \in ℝ ⟼ \sin x)$
195	191 194	eqtrd	$⊢ φ \to \frac{d (x \in ℝ⟼ - \cos x)}{d_{ℝ} x} = (x \in ℝ ⟼ \sin x)$
196	125 186 128 195 178 180 179 183	dvmptres2	$⊢ φ \to \frac{d (x \in [0, π]⟼ - \cos x)}{d_{ℝ} x} = (x \in (0, π) ⟼ \sin x)$
197		fveq2	$⊢ x = 0 \to \sin x = \sin 0$
198		sin0	$⊢ \sin 0 = 0$
199	197 198	eqtrdi	$⊢ x = 0 \to \sin x = 0$
200	199	oveq1d	$⊢ x = 0 \to {\sin x}^{N} = 0^{N}$
201	200	adantl	$⊢ (φ \land x = 0) \to {\sin x}^{N} = 0^{N}$
202	7	adantr	$⊢ (φ \land x = 0) \to N \in ℕ$
203	202	0expd	$⊢ (φ \land x = 0) \to 0^{N} = 0$
204	201 203	eqtrd	$⊢ (φ \land x = 0) \to {\sin x}^{N} = 0$
205	204	oveq1d	$⊢ (φ \land x = 0) \to {\sin x}^{N} (- \cos x) = 0 \cdot (- \cos x)$
206		id	$⊢ x = 0 \to x = 0$
207		0cn	$⊢ 0 \in ℂ$
208	206 207	eqeltrdi	$⊢ x = 0 \to x \in ℂ$
209		coscl	$⊢ x \in ℂ \to \cos x \in ℂ$
210	209	negcld	$⊢ x \in ℂ \to - \cos x \in ℂ$
211	208 210	syl	$⊢ x = 0 \to - \cos x \in ℂ$
212	211	adantl	$⊢ (φ \land x = 0) \to - \cos x \in ℂ$
213	212	mul02d	$⊢ (φ \land x = 0) \to 0 \cdot (- \cos x) = 0$
214	205 213	eqtrd	$⊢ (φ \land x = 0) \to {\sin x}^{N} (- \cos x) = 0$
215		fveq2	$⊢ x = π \to \sin x = \sin π$
216		sinpi	$⊢ \sin π = 0$
217	215 216	eqtrdi	$⊢ x = π \to \sin x = 0$
218	217	oveq1d	$⊢ x = π \to {\sin x}^{N} = 0^{N}$
219	218	adantl	$⊢ (φ \land x = π) \to {\sin x}^{N} = 0^{N}$
220	7	adantr	$⊢ (φ \land x = π) \to N \in ℕ$
221	220	0expd	$⊢ (φ \land x = π) \to 0^{N} = 0$
222	219 221	eqtrd	$⊢ (φ \land x = π) \to {\sin x}^{N} = 0$
223	222	oveq1d	$⊢ (φ \land x = π) \to {\sin x}^{N} (- \cos x) = 0 \cdot (- \cos x)$
224		id	$⊢ x = π \to x = π$
225		picn	$⊢ π \in ℂ$
226	224 225	eqeltrdi	$⊢ x = π \to x \in ℂ$
227	226	coscld	$⊢ x = π \to \cos x \in ℂ$
228	227	negcld	$⊢ x = π \to - \cos x \in ℂ$
229	228	adantl	$⊢ (φ \land x = π) \to - \cos x \in ℂ$
230	229	mul02d	$⊢ (φ \land x = π) \to 0 \cdot (- \cos x) = 0$
231	223 230	eqtrd	$⊢ (φ \land x = π) \to {\sin x}^{N} (- \cos x) = 0$
232	11 13 16 42 57 83 84 106 123 184 196 214 231	itgparts	$⊢ φ \to \int_{(0, π)} {\sin x}^{N} \sin x d x = 0 - 0 - \int_{(0, π)} N {\sin x}^{N - 1} \cos x (- \cos x) d x$
233		df-neg	$⊢ - \int_{(0, π)} N {\sin x}^{N - 1} \cos x (- \cos x) d x = 0 - \int_{(0, π)} N {\sin x}^{N - 1} \cos x (- \cos x) d x$
234	233	a1i	$⊢ φ \to - \int_{(0, π)} N {\sin x}^{N - 1} \cos x (- \cos x) d x = 0 - \int_{(0, π)} N {\sin x}^{N - 1} \cos x (- \cos x) d x$
235	9 232 234	3eqtr4a	$⊢ φ \to \int_{(0, π)} {\sin x}^{N} \sin x d x = - \int_{(0, π)} N {\sin x}^{N - 1} \cos x (- \cos x) d x$
236	79 81 81	mulassd	$⊢ (φ \land x \in (0, π)) \to N {\sin x}^{N - 1} \cos x \cos x = N {\sin x}^{N - 1} \cos x \cos x$
237		sqval	$⊢ \cos x \in ℂ \to {\cos x}^{2} = \cos x \cos x$
238	237	eqcomd	$⊢ \cos x \in ℂ \to \cos x \cos x = {\cos x}^{2}$
239	80 238	syl	$⊢ x \in (0, π) \to \cos x \cos x = {\cos x}^{2}$
240	239	adantl	$⊢ (φ \land x \in (0, π)) \to \cos x \cos x = {\cos x}^{2}$
241	240	oveq2d	$⊢ (φ \land x \in (0, π)) \to N {\sin x}^{N - 1} \cos x \cos x = N {\sin x}^{N - 1} {\cos x}^{2}$
242	80	sqcld	$⊢ x \in (0, π) \to {\cos x}^{2} \in ℂ$
243	242	adantl	$⊢ (φ \land x \in (0, π)) \to {\cos x}^{2} \in ℂ$
244	73 78 243	mulassd	$⊢ (φ \land x \in (0, π)) \to N {\sin x}^{N - 1} {\cos x}^{2} = N {\sin x}^{N - 1} {\cos x}^{2}$
245	241 244	eqtrd	$⊢ (φ \land x \in (0, π)) \to N {\sin x}^{N - 1} \cos x \cos x = N {\sin x}^{N - 1} {\cos x}^{2}$
246	78 243	mulcomd	$⊢ (φ \land x \in (0, π)) \to {\sin x}^{N - 1} {\cos x}^{2} = {\cos x}^{2} {\sin x}^{N - 1}$
247	246	oveq2d	$⊢ (φ \land x \in (0, π)) \to N {\sin x}^{N - 1} {\cos x}^{2} = N {\cos x}^{2} {\sin x}^{N - 1}$
248	236 245 247	3eqtrd	$⊢ (φ \land x \in (0, π)) \to N {\sin x}^{N - 1} \cos x \cos x = N {\cos x}^{2} {\sin x}^{N - 1}$
249	248	negeqd	$⊢ (φ \land x \in (0, π)) \to - N {\sin x}^{N - 1} \cos x \cos x = - N {\cos x}^{2} {\sin x}^{N - 1}$
250	82 81	mulneg2d	$⊢ (φ \land x \in (0, π)) \to N {\sin x}^{N - 1} \cos x (- \cos x) = - N {\sin x}^{N - 1} \cos x \cos x$
251	243 78	mulcld	$⊢ (φ \land x \in (0, π)) \to {\cos x}^{2} {\sin x}^{N - 1} \in ℂ$
252	73 251	mulneg1d	$⊢ (φ \land x \in (0, π)) \to -N {\cos x}^{2} {\sin x}^{N - 1} = - N {\cos x}^{2} {\sin x}^{N - 1}$
253	249 250 252	3eqtr4d	$⊢ (φ \land x \in (0, π)) \to N {\sin x}^{N - 1} \cos x (- \cos x) = -N {\cos x}^{2} {\sin x}^{N - 1}$
254	253	itgeq2dv	$⊢ φ \to \int_{(0, π)} N {\sin x}^{N - 1} \cos x (- \cos x) d x = \int_{(0, π)} -N {\cos x}^{2} {\sin x}^{N - 1} d x$
255	59	negcld	$⊢ φ \to - N \in ℂ$
256	43	sqcld	$⊢ x \in [0, π] \to {\cos x}^{2} \in ℂ$
257	256	adantl	$⊢ (φ \land x \in [0, π]) \to {\cos x}^{2} \in ℂ$
258	257 109	mulcld	$⊢ (φ \land x \in [0, π]) \to {\cos x}^{2} {\sin x}^{N - 1} \in ℂ$
259	6	fvmpt2	$⊢ (x \in ℂ \land {\cos x}^{2} {\sin x}^{N - 1} \in ℂ) \to M (x) = {\cos x}^{2} {\sin x}^{N - 1}$
260	23 258 259	syl2anc	$⊢ (φ \land x \in [0, π]) \to M (x) = {\cos x}^{2} {\sin x}^{N - 1}$
261	260	eqcomd	$⊢ (φ \land x \in [0, π]) \to {\cos x}^{2} {\sin x}^{N - 1} = M (x)$
262	261	mpteq2dva	$⊢ φ \to (x \in [0, π] ⟼ {\cos x}^{2} {\sin x}^{N - 1}) = (x \in [0, π] ⟼ M (x))$
263		nfmpt1	$⊢ \underline{Ⅎ} x (x \in ℂ ⟼ {\cos x}^{2} {\sin x}^{N - 1})$
264	6 263	nfcxfr	$⊢ \underline{Ⅎ} x M$
265		nfcv	$⊢ \underline{Ⅎ} x \cos$
266		2nn0	$⊢ 2 \in ℕ_{0}$
267	266	a1i	$⊢ φ \to 2 \in ℕ_{0}$
268	265 53 267	expcnfg	$⊢ φ \to (x \in ℂ ⟼ {\cos x}^{2}) : ℂ \underset{cn}{⟶} ℂ$
269	268 63	mulcncf	$⊢ φ \to (x \in ℂ ⟼ {\cos x}^{2} {\sin x}^{N - 1}) : ℂ \underset{cn}{⟶} ℂ$
270	6 269	eqeltrid	$⊢ φ \to M : ℂ \underset{cn}{⟶} ℂ$
271	264 270 40	cncfmptss	$⊢ φ \to (x \in [0, π] ⟼ M (x)) : [0, π] \underset{cn}{⟶} ℂ$
272	262 271	eqeltrd	$⊢ φ \to (x \in [0, π] ⟼ {\cos x}^{2} {\sin x}^{N - 1}) : [0, π] \underset{cn}{⟶} ℂ$
273		cniccibl	$⊢ (0 \in ℝ \land π \in ℝ \land (x \in [0, π] ⟼ {\cos x}^{2} {\sin x}^{N - 1}) : [0, π] \underset{cn}{⟶} ℂ) \to (x \in [0, π] ⟼ {\cos x}^{2} {\sin x}^{N - 1}) \in 𝐿^{1}$
274	11 13 272 273	syl3anc	$⊢ φ \to (x \in [0, π] ⟼ {\cos x}^{2} {\sin x}^{N - 1}) \in 𝐿^{1}$
275	86 88 258 274	iblss	$⊢ φ \to (x \in (0, π) ⟼ {\cos x}^{2} {\sin x}^{N - 1}) \in 𝐿^{1}$
276	255 251 275	itgmulc2	$⊢ φ \to -N \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 1} d x = \int_{(0, π)} -N {\cos x}^{2} {\sin x}^{N - 1} d x$
277	254 276	eqtr4d	$⊢ φ \to \int_{(0, π)} N {\sin x}^{N - 1} \cos x (- \cos x) d x = -N \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 1} d x$
278	277	negeqd	$⊢ φ \to - \int_{(0, π)} N {\sin x}^{N - 1} \cos x (- \cos x) d x = - -N \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 1} d x$
279	235 278	eqtrd	$⊢ φ \to \int_{(0, π)} {\sin x}^{N} \sin x d x = - -N \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 1} d x$
280	251 275	itgcl	$⊢ φ \to \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 1} d x \in ℂ$
281	59 280	mulneg1d	$⊢ φ \to -N \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 1} d x = - N \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 1} d x$
282	281	negeqd	$⊢ φ \to - -N \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 1} d x = - (- N \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 1} d x)$
283	59 280	mulcld	$⊢ φ \to N \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 1} d x \in ℂ$
284	283	negnegd	$⊢ φ \to - (- N \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 1} d x) = N \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 1} d x$
285	279 282 284	3eqtrd	$⊢ φ \to \int_{(0, π)} {\sin x}^{N} \sin x d x = N \int_{(0, π)} {\cos x}^{2} {\sin x}^{N - 1} d x$

Metamath Proof Explorer

Theorem itgsinexplem1

Proof