Theorem itgsinexplem1 29794

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

Hypotheses

Ref	Expression
itgsinexplem1.1	|- F = ( x e. CC |-> ( ( sin ` x ) ^ N ) )
itgsinexplem1.2	|- G = ( x e. CC |-> -u ( cos ` x ) )
itgsinexplem1.3	|- H = ( x e. CC |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) )
itgsinexplem1.4	|- I = ( x e. CC |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) )
itgsinexplem1.5	|- L = ( x e. CC |-> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) )
itgsinexplem1.6	|- M = ( x e. CC |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) )
itgsinexplem1.7	|- ( ph -> N e. NN )

Assertion

Ref	Expression
itgsinexplem1	|- ( ph -> S. ( 0 (,) pi ) ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) _d x = ( N x. S. ( 0 (,) pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) _d x ) )

Distinct variable groups:   x, N   ph, x

Allowed substitution hints:   F( x)   G( x)   H( x)   I( x)   L( x)   M( x)

Proof of Theorem itgsinexplem1

Step	Hyp	Ref	Expression
1		0m0e0 10431	. . . . 5 |- ( 0 - 0 ) = 0
2	1	oveq1i 6101	. . . 4 |- ( ( 0 - 0 ) - S. ( 0 (,) pi ) ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) _d x ) = ( 0 - S. ( 0 (,) pi ) ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) _d x )
3		0re 9386	. . . . . 6 |- 0 e. RR
4	3	a1i 11	. . . . 5 |- ( ph -> 0 e. RR )
5		pire 21921	. . . . . 6 |- pi e. RR
6	5	a1i 11	. . . . 5 |- ( ph -> pi e. RR )
7		pipos 21923	. . . . . . 7 |- 0 < pi
8	3, 5, 7	ltleii 9497	. . . . . 6 |- 0 <_ pi
9	8	a1i 11	. . . . 5 |- ( ph -> 0 <_ pi )
10	3, 5	pm3.2i 455	. . . . . . . . . . . . 13 |- ( 0 e. RR /\ pi e. RR )
11		iccssre 11377	. . . . . . . . . . . . 13 |- ( ( 0 e. RR /\ pi e. RR ) -> ( 0 [,] pi ) C_ RR )
12	10, 11	ax-mp 5	. . . . . . . . . . . 12 |- ( 0 [,] pi ) C_ RR
13		ax-resscn 9339	. . . . . . . . . . . 12 |- RR C_ CC
14	12, 13	sstri 3365	. . . . . . . . . . 11 |- ( 0 [,] pi ) C_ CC
15	14	sseli 3352	. . . . . . . . . 10 |- ( x e. ( 0 [,] pi ) -> x e. CC )
16	15	adantl 466	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> x e. CC )
17	15	sincld 13414	. . . . . . . . . . 11 |- ( x e. ( 0 [,] pi ) -> ( sin ` x ) e. CC )
18	17	adantl 466	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( sin ` x ) e. CC )
19		itgsinexplem1.7	. . . . . . . . . . . 12 |- ( ph -> N e. NN )
20	19	nnnn0d 10636	. . . . . . . . . . 11 |- ( ph -> N e. NN0 )
21	20	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> N e. NN0 )
22	18, 21	expcld 12008	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( sin ` x ) ^ N ) e. CC )
23		itgsinexplem1.1	. . . . . . . . . 10 |- F = ( x e. CC |-> ( ( sin ` x ) ^ N ) )
24	23	fvmpt2 5781	. . . . . . . . 9 |- ( ( x e. CC /\ ( ( sin ` x ) ^ N ) e. CC ) -> ( F ` x ) = ( ( sin ` x ) ^ N ) )
25	16, 22, 24	syl2anc 661	. . . . . . . 8 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( F ` x ) = ( ( sin ` x ) ^ N ) )
26	25	eqcomd 2448	. . . . . . 7 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( sin ` x ) ^ N ) = ( F ` x ) )
27	26	mpteq2dva 4378	. . . . . 6 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( sin ` x ) ^ N ) ) = ( x e. ( 0 [,] pi ) |-> ( F ` x ) ) )
28		nfmpt1 4381	. . . . . . . 8 |- F/_ x ( x e. CC |-> ( ( sin ` x ) ^ N ) )
29	23, 28	nfcxfr 2576	. . . . . . 7 |- F/_ x F
30		nfcv 2579	. . . . . . . . 9 |- F/_ x sin
31		sincn 21909	. . . . . . . . . 10 |- sin e. ( CC -cn-> CC )
32	31	a1i 11	. . . . . . . . 9 |- ( ph -> sin e. ( CC -cn-> CC ) )
33	30, 32, 20	expcnfg 29773	. . . . . . . 8 |- ( ph -> ( x e. CC |-> ( ( sin ` x ) ^ N ) ) e. ( CC -cn-> CC ) )
34	23, 33	syl5eqel 2527	. . . . . . 7 |- ( ph -> F e. ( CC -cn-> CC ) )
35	14	a1i 11	. . . . . . 7 |- ( ph -> ( 0 [,] pi ) C_ CC )
36	29, 34, 35	cncfmptss 29768	. . . . . 6 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( F ` x ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
37	27, 36	eqeltrd 2517	. . . . 5 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( sin ` x ) ^ N ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
38	15	coscld 13415	. . . . . . . . . . 11 |- ( x e. ( 0 [,] pi ) -> ( cos ` x ) e. CC )
39	38	negcld 9706	. . . . . . . . . 10 |- ( x e. ( 0 [,] pi ) -> -u ( cos ` x ) e. CC )
40		itgsinexplem1.2	. . . . . . . . . . 11 |- G = ( x e. CC |-> -u ( cos ` x ) )
41	40	fvmpt2 5781	. . . . . . . . . 10 |- ( ( x e. CC /\ -u ( cos ` x ) e. CC ) -> ( G ` x ) = -u ( cos ` x ) )
42	15, 39, 41	syl2anc 661	. . . . . . . . 9 |- ( x e. ( 0 [,] pi ) -> ( G ` x ) = -u ( cos ` x ) )
43	42	eqcomd 2448	. . . . . . . 8 |- ( x e. ( 0 [,] pi ) -> -u ( cos ` x ) = ( G ` x ) )
44	43	adantl 466	. . . . . . 7 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> -u ( cos ` x ) = ( G ` x ) )
45	44	mpteq2dva 4378	. . . . . 6 |- ( ph -> ( x e. ( 0 [,] pi ) |-> -u ( cos ` x ) ) = ( x e. ( 0 [,] pi ) |-> ( G ` x ) ) )
46		nfmpt1 4381	. . . . . . . 8 |- F/_ x ( x e. CC |-> -u ( cos ` x ) )
47	40, 46	nfcxfr 2576	. . . . . . 7 |- F/_ x G
48		coscn 21910	. . . . . . . . 9 |- cos e. ( CC -cn-> CC )
49	48	a1i 11	. . . . . . . 8 |- ( ph -> cos e. ( CC -cn-> CC ) )
50	40	negfcncf 20495	. . . . . . . 8 |- ( cos e. ( CC -cn-> CC ) -> G e. ( CC -cn-> CC ) )
51	49, 50	syl 16	. . . . . . 7 |- ( ph -> G e. ( CC -cn-> CC ) )
52	47, 51, 35	cncfmptss 29768	. . . . . 6 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( G ` x ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
53	45, 52	eqeltrd 2517	. . . . 5 |- ( ph -> ( x e. ( 0 [,] pi ) |-> -u ( cos ` x ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
54		ioossre 11357	. . . . . . . . . . . 12 |- ( 0 (,) pi ) C_ RR
55	54, 13	sstri 3365	. . . . . . . . . . 11 |- ( 0 (,) pi ) C_ CC
56	55	sseli 3352	. . . . . . . . . 10 |- ( x e. ( 0 (,) pi ) -> x e. CC )
57	56	adantl 466	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> x e. CC )
58	19	nncnd 10338	. . . . . . . . . . . 12 |- ( ph -> N e. CC )
59	58	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> N e. CC )
60	56	sincld 13414	. . . . . . . . . . . . 13 |- ( x e. ( 0 (,) pi ) -> ( sin ` x ) e. CC )
61	60	adantl 466	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( sin ` x ) e. CC )
62		nnm1nn0 10621	. . . . . . . . . . . . . 14 |- ( N e. NN -> ( N - 1 ) e. NN0 )
63	19, 62	syl 16	. . . . . . . . . . . . 13 |- ( ph -> ( N - 1 ) e. NN0 )
64	63	adantr 465	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( N - 1 ) e. NN0 )
65	61, 64	expcld 12008	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( sin ` x ) ^ ( N - 1 ) ) e. CC )
66	59, 65	mulcld 9406	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) e. CC )
67	56	coscld 13415	. . . . . . . . . . 11 |- ( x e. ( 0 (,) pi ) -> ( cos ` x ) e. CC )
68	67	adantl 466	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( cos ` x ) e. CC )
69	66, 68	mulcld 9406	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) e. CC )
70		itgsinexplem1.3	. . . . . . . . . 10 |- H = ( x e. CC |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) )
71	70	fvmpt2 5781	. . . . . . . . 9 |- ( ( x e. CC /\ ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) e. CC ) -> ( H ` x ) = ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) )
72	57, 69, 71	syl2anc 661	. . . . . . . 8 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( H ` x ) = ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) )
73	72	eqcomd 2448	. . . . . . 7 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) = ( H ` x ) )
74	73	mpteq2dva 4378	. . . . . 6 |- ( ph -> ( x e. ( 0 (,) pi ) |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) = ( x e. ( 0 (,) pi ) |-> ( H ` x ) ) )
75		nfmpt1 4381	. . . . . . . 8 |- F/_ x ( x e. CC |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) )
76	70, 75	nfcxfr 2576	. . . . . . 7 |- F/_ x H
77		ssid 3375	. . . . . . . . . . . 12 |- CC C_ CC
78	77	a1i 11	. . . . . . . . . . 11 |- ( ph -> CC C_ CC )
79		cncfmptc 20487	. . . . . . . . . . 11 |- ( ( N e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> N ) e. ( CC -cn-> CC ) )
80	58, 78, 78, 79	syl3anc 1218	. . . . . . . . . 10 |- ( ph -> ( x e. CC |-> N ) e. ( CC -cn-> CC ) )
81	30, 32, 63	expcnfg 29773	. . . . . . . . . 10 |- ( ph -> ( x e. CC |-> ( ( sin ` x ) ^ ( N - 1 ) ) ) e. ( CC -cn-> CC ) )
82	80, 81	mulcncf 20931	. . . . . . . . 9 |- ( ph -> ( x e. CC |-> ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) e. ( CC -cn-> CC ) )
83		cosf 13409	. . . . . . . . . . . 12 |- cos : CC --> CC
84	83	a1i 11	. . . . . . . . . . 11 |- ( ph -> cos : CC --> CC )
85	84	feqmptd 5744	. . . . . . . . . 10 |- ( ph -> cos = ( x e. CC |-> ( cos ` x ) ) )
86	85, 48	syl6eqelr 2532	. . . . . . . . 9 |- ( ph -> ( x e. CC |-> ( cos ` x ) ) e. ( CC -cn-> CC ) )
87	82, 86	mulcncf 20931	. . . . . . . 8 |- ( ph -> ( x e. CC |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) e. ( CC -cn-> CC ) )
88	70, 87	syl5eqel 2527	. . . . . . 7 |- ( ph -> H e. ( CC -cn-> CC ) )
89	55	a1i 11	. . . . . . 7 |- ( ph -> ( 0 (,) pi ) C_ CC )
90	76, 88, 89	cncfmptss 29768	. . . . . 6 |- ( ph -> ( x e. ( 0 (,) pi ) |-> ( H ` x ) ) e. ( ( 0 (,) pi ) -cn-> CC ) )
91	74, 90	eqeltrd 2517	. . . . 5 |- ( ph -> ( x e. ( 0 (,) pi ) |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) e. ( ( 0 (,) pi ) -cn-> CC ) )
92	30, 32, 89	cncfmptss 29768	. . . . 5 |- ( ph -> ( x e. ( 0 (,) pi ) |-> ( sin ` x ) ) e. ( ( 0 (,) pi ) -cn-> CC ) )
93		ioossicc 11381	. . . . . . 7 |- ( 0 (,) pi ) C_ ( 0 [,] pi )
94	93	a1i 11	. . . . . 6 |- ( ph -> ( 0 (,) pi ) C_ ( 0 [,] pi ) )
95		ioombl 21046	. . . . . . 7 |- ( 0 (,) pi ) e. dom vol
96	95	a1i 11	. . . . . 6 |- ( ph -> ( 0 (,) pi ) e. dom vol )
97	22, 18	mulcld 9406	. . . . . 6 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) e. CC )
98		itgsinexplem1.4	. . . . . . . . . . . 12 |- I = ( x e. CC |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) )
99	98	fvmpt2 5781	. . . . . . . . . . 11 |- ( ( x e. CC /\ ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) e. CC ) -> ( I ` x ) = ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) )
100	16, 97, 99	syl2anc 661	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( I ` x ) = ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) )
101	100	eqcomd 2448	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) = ( I ` x ) )
102	101	mpteq2dva 4378	. . . . . . . 8 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) ) = ( x e. ( 0 [,] pi ) |-> ( I ` x ) ) )
103		nfmpt1 4381	. . . . . . . . . 10 |- F/_ x ( x e. CC |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) )
104	98, 103	nfcxfr 2576	. . . . . . . . 9 |- F/_ x I
105		sinf 13408	. . . . . . . . . . . . . 14 |- sin : CC --> CC
106	105	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> sin : CC --> CC )
107	106	feqmptd 5744	. . . . . . . . . . . 12 |- ( ph -> sin = ( x e. CC |-> ( sin ` x ) ) )
108	107, 31	syl6eqelr 2532	. . . . . . . . . . 11 |- ( ph -> ( x e. CC |-> ( sin ` x ) ) e. ( CC -cn-> CC ) )
109	33, 108	mulcncf 20931	. . . . . . . . . 10 |- ( ph -> ( x e. CC |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) ) e. ( CC -cn-> CC ) )
110	98, 109	syl5eqel 2527	. . . . . . . . 9 |- ( ph -> I e. ( CC -cn-> CC ) )
111	104, 110, 35	cncfmptss 29768	. . . . . . . 8 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( I ` x ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
112	102, 111	eqeltrd 2517	. . . . . . 7 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
113		cniccibl 21318	. . . . . . 7 |- ( ( 0 e. RR /\ pi e. RR /\ ( x e. ( 0 [,] pi ) |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) ) e. ( ( 0 [,] pi ) -cn-> CC ) ) -> ( x e. ( 0 [,] pi ) |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) ) e. L^1 )
114	4, 6, 112, 113	syl3anc 1218	. . . . . 6 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) ) e. L^1 )
115	94, 96, 97, 114	iblss 21282	. . . . 5 |- ( ph -> ( x e. ( 0 (,) pi ) |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) ) e. L^1 )
116	58	adantr 465	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> N e. CC )
117	63	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( N - 1 ) e. NN0 )
118	18, 117	expcld 12008	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( sin ` x ) ^ ( N - 1 ) ) e. CC )
119	116, 118	mulcld 9406	. . . . . . . 8 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) e. CC )
120	38	adantl 466	. . . . . . . 8 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( cos ` x ) e. CC )
121	119, 120	mulcld 9406	. . . . . . 7 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) e. CC )
122	39	adantl 466	. . . . . . 7 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> -u ( cos ` x ) e. CC )
123	121, 122	mulcld 9406	. . . . . 6 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) e. CC )
124		itgsinexplem1.5	. . . . . . . . . . . 12 |- L = ( x e. CC |-> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) )
125	124	fvmpt2 5781	. . . . . . . . . . 11 |- ( ( x e. CC /\ ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) e. CC ) -> ( L ` x ) = ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) )
126	16, 123, 125	syl2anc 661	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( L ` x ) = ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) )
127	126	eqcomd 2448	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) = ( L ` x ) )
128	127	mpteq2dva 4378	. . . . . . . 8 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) ) = ( x e. ( 0 [,] pi ) |-> ( L ` x ) ) )
129		nfmpt1 4381	. . . . . . . . . 10 |- F/_ x ( x e. CC |-> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) )
130	124, 129	nfcxfr 2576	. . . . . . . . 9 |- F/_ x L
131		eqid 2443	. . . . . . . . . . . . 13 |- ( x e. CC |-> -u ( cos ` x ) ) = ( x e. CC |-> -u ( cos ` x ) )
132	131	negfcncf 20495	. . . . . . . . . . . 12 |- ( cos e. ( CC -cn-> CC ) -> ( x e. CC |-> -u ( cos ` x ) ) e. ( CC -cn-> CC ) )
133	49, 132	syl 16	. . . . . . . . . . 11 |- ( ph -> ( x e. CC |-> -u ( cos ` x ) ) e. ( CC -cn-> CC ) )
134	87, 133	mulcncf 20931	. . . . . . . . . 10 |- ( ph -> ( x e. CC |-> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) ) e. ( CC -cn-> CC ) )
135	124, 134	syl5eqel 2527	. . . . . . . . 9 |- ( ph -> L e. ( CC -cn-> CC ) )
136	130, 135, 35	cncfmptss 29768	. . . . . . . 8 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( L ` x ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
137	128, 136	eqeltrd 2517	. . . . . . 7 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
138		cniccibl 21318	. . . . . . 7 |- ( ( 0 e. RR /\ pi e. RR /\ ( x e. ( 0 [,] pi ) |-> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) ) e. ( ( 0 [,] pi ) -cn-> CC ) ) -> ( x e. ( 0 [,] pi ) |-> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) ) e. L^1 )
139	4, 6, 137, 138	syl3anc 1218	. . . . . 6 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) ) e. L^1 )
140	94, 96, 123, 139	iblss 21282	. . . . 5 |- ( ph -> ( x e. ( 0 (,) pi ) |-> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) ) e. L^1 )
141		reelprrecn 9374	. . . . . . 7 |- RR e. { RR , CC }
142	141	a1i 11	. . . . . 6 |- ( ph -> RR e. { RR , CC } )
143		recn 9372	. . . . . . . . 9 |- ( x e. RR -> x e. CC )
144	143	sincld 13414	. . . . . . . 8 |- ( x e. RR -> ( sin ` x ) e. CC )
145	144	adantl 466	. . . . . . 7 |- ( ( ph /\ x e. RR ) -> ( sin ` x ) e. CC )
146	20	adantr 465	. . . . . . 7 |- ( ( ph /\ x e. RR ) -> N e. NN0 )
147	145, 146	expcld 12008	. . . . . 6 |- ( ( ph /\ x e. RR ) -> ( ( sin ` x ) ^ N ) e. CC )
148	58	adantr 465	. . . . . . . 8 |- ( ( ph /\ x e. RR ) -> N e. CC )
149	63	adantr 465	. . . . . . . . 9 |- ( ( ph /\ x e. RR ) -> ( N - 1 ) e. NN0 )
150	145, 149	expcld 12008	. . . . . . . 8 |- ( ( ph /\ x e. RR ) -> ( ( sin ` x ) ^ ( N - 1 ) ) e. CC )
151	148, 150	mulcld 9406	. . . . . . 7 |- ( ( ph /\ x e. RR ) -> ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) e. CC )
152	143	coscld 13415	. . . . . . . 8 |- ( x e. RR -> ( cos ` x ) e. CC )
153	152	adantl 466	. . . . . . 7 |- ( ( ph /\ x e. RR ) -> ( cos ` x ) e. CC )
154	151, 153	mulcld 9406	. . . . . 6 |- ( ( ph /\ x e. RR ) -> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) e. CC )
155		sincl 13410	. . . . . . . . . . 11 |- ( x e. CC -> ( sin ` x ) e. CC )
156	155	adantl 466	. . . . . . . . . 10 |- ( ( ph /\ x e. CC ) -> ( sin ` x ) e. CC )
157	20	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ x e. CC ) -> N e. NN0 )
158	156, 157	expcld 12008	. . . . . . . . 9 |- ( ( ph /\ x e. CC ) -> ( ( sin ` x ) ^ N ) e. CC )
159	158, 23	fmptd 5867	. . . . . . . 8 |- ( ph -> F : CC --> CC )
160	143	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> x e. CC )
161		elex 2981	. . . . . . . . . . . . . . 15 |- ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) e. CC -> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) e. _V )
162	154, 161	syl 16	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) e. _V )
163		rabid 2897	. . . . . . . . . . . . . 14 |- ( x e. { x e. CC | ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) e. _V } <-> ( x e. CC /\ ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) e. _V ) )
164	160, 162, 163	sylanbrc 664	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR ) -> x e. { x e. CC | ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) e. _V } )
165	70	dmmpt 5333	. . . . . . . . . . . . 13 |- dom H = { x e. CC | ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) e. _V }
166	164, 165	syl6eleqr 2534	. . . . . . . . . . . 12 |- ( ( ph /\ x e. RR ) -> x e. dom H )
167	166	ex 434	. . . . . . . . . . 11 |- ( ph -> ( x e. RR -> x e. dom H ) )
168	167	alrimiv 1685	. . . . . . . . . 10 |- ( ph -> A. x ( x e. RR -> x e. dom H ) )
169		nfcv 2579	. . . . . . . . . . 11 |- F/_ x RR
170	76	nfdm 5081	. . . . . . . . . . 11 |- F/_ x dom H
171	169, 170	dfss2f 3347	. . . . . . . . . 10 |- ( RR C_ dom H <-> A. x ( x e. RR -> x e. dom H ) )
172	168, 171	sylibr 212	. . . . . . . . 9 |- ( ph -> RR C_ dom H )
173	19	dvsinexp 29787	. . . . . . . . . . 11 |- ( ph -> ( CC _D ( x e. CC |-> ( ( sin ` x ) ^ N ) ) ) = ( x e. CC |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) )
174	23	oveq2i 6102	. . . . . . . . . . 11 |- ( CC _D F ) = ( CC _D ( x e. CC |-> ( ( sin ` x ) ^ N ) ) )
175	173, 174, 70	3eqtr4g 2500	. . . . . . . . . 10 |- ( ph -> ( CC _D F ) = H )
176	175	dmeqd 5042	. . . . . . . . 9 |- ( ph -> dom ( CC _D F ) = dom H )
177	172, 176	sseqtr4d 3393	. . . . . . . 8 |- ( ph -> RR C_ dom ( CC _D F ) )
178		dvres3 21388	. . . . . . . 8 |- ( ( ( RR e. { RR , CC } /\ F : CC --> CC ) /\ ( CC C_ CC /\ RR C_ dom ( CC _D F ) ) ) -> ( RR _D ( F |` RR ) ) = ( ( CC _D F ) |` RR ) )
179	142, 159, 78, 177, 178	syl22anc 1219	. . . . . . 7 |- ( ph -> ( RR _D ( F |` RR ) ) = ( ( CC _D F ) |` RR ) )
180	23	reseq1i 5106	. . . . . . . . . 10 |- ( F |` RR ) = ( ( x e. CC |-> ( ( sin ` x ) ^ N ) ) |` RR )
181		resmpt 5156	. . . . . . . . . . 11 |- ( RR C_ CC -> ( ( x e. CC |-> ( ( sin ` x ) ^ N ) ) |` RR ) = ( x e. RR |-> ( ( sin ` x ) ^ N ) ) )
182	13, 181	ax-mp 5	. . . . . . . . . 10 |- ( ( x e. CC |-> ( ( sin ` x ) ^ N ) ) |` RR ) = ( x e. RR |-> ( ( sin ` x ) ^ N ) )
183	180, 182	eqtri 2463	. . . . . . . . 9 |- ( F |` RR ) = ( x e. RR |-> ( ( sin ` x ) ^ N ) )
184	183	oveq2i 6102	. . . . . . . 8 |- ( RR _D ( F |` RR ) ) = ( RR _D ( x e. RR |-> ( ( sin ` x ) ^ N ) ) )
185	184	a1i 11	. . . . . . 7 |- ( ph -> ( RR _D ( F |` RR ) ) = ( RR _D ( x e. RR |-> ( ( sin ` x ) ^ N ) ) ) )
186	175	reseq1d 5109	. . . . . . . 8 |- ( ph -> ( ( CC _D F ) |` RR ) = ( H |` RR ) )
187	70	reseq1i 5106	. . . . . . . . 9 |- ( H |` RR ) = ( ( x e. CC |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) |` RR )
188		resmpt 5156	. . . . . . . . . 10 |- ( RR C_ CC -> ( ( x e. CC |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) |` RR ) = ( x e. RR |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) )
189	13, 188	ax-mp 5	. . . . . . . . 9 |- ( ( x e. CC |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) |` RR ) = ( x e. RR |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) )
190	187, 189	eqtri 2463	. . . . . . . 8 |- ( H |` RR ) = ( x e. RR |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) )
191	186, 190	syl6eq 2491	. . . . . . 7 |- ( ph -> ( ( CC _D F ) |` RR ) = ( x e. RR |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) )
192	179, 185, 191	3eqtr3d 2483	. . . . . 6 |- ( ph -> ( RR _D ( x e. RR |-> ( ( sin ` x ) ^ N ) ) ) = ( x e. RR |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) )
193	12	a1i 11	. . . . . 6 |- ( ph -> ( 0 [,] pi ) C_ RR )
194		eqid 2443	. . . . . . 7 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
195	194	tgioo2 20380	. . . . . 6 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
196	10	a1i 11	. . . . . . 7 |- ( ph -> ( 0 e. RR /\ pi e. RR ) )
197		iccntr 20398	. . . . . . 7 |- ( ( 0 e. RR /\ pi e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( 0 [,] pi ) ) = ( 0 (,) pi ) )
198	196, 197	syl 16	. . . . . 6 |- ( ph -> ( ( int ` ( topGen ` ran (,) ) ) ` ( 0 [,] pi ) ) = ( 0 (,) pi ) )
199	142, 147, 154, 192, 193, 195, 194, 198	dvmptres2 21436	. . . . 5 |- ( ph -> ( RR _D ( x e. ( 0 [,] pi ) |-> ( ( sin ` x ) ^ N ) ) ) = ( x e. ( 0 (,) pi ) |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) )
200	152	negcld 9706	. . . . . . 7 |- ( x e. RR -> -u ( cos ` x ) e. CC )
201	200	adantl 466	. . . . . 6 |- ( ( ph /\ x e. RR ) -> -u ( cos ` x ) e. CC )
202	144	negcld 9706	. . . . . . . . 9 |- ( x e. RR -> -u ( sin ` x ) e. CC )
203	202	adantl 466	. . . . . . . 8 |- ( ( ph /\ x e. RR ) -> -u ( sin ` x ) e. CC )
204		dvcosre 29788	. . . . . . . . 9 |- ( RR _D ( x e. RR |-> ( cos ` x ) ) ) = ( x e. RR |-> -u ( sin ` x ) )
205	204	a1i 11	. . . . . . . 8 |- ( ph -> ( RR _D ( x e. RR |-> ( cos ` x ) ) ) = ( x e. RR |-> -u ( sin ` x ) ) )
206	142, 153, 203, 205	dvmptneg 21440	. . . . . . 7 |- ( ph -> ( RR _D ( x e. RR |-> -u ( cos ` x ) ) ) = ( x e. RR |-> -u -u ( sin ` x ) ) )
207	144	negnegd 9710	. . . . . . . . 9 |- ( x e. RR -> -u -u ( sin ` x ) = ( sin ` x ) )
208	207	adantl 466	. . . . . . . 8 |- ( ( ph /\ x e. RR ) -> -u -u ( sin ` x ) = ( sin ` x ) )
209	208	mpteq2dva 4378	. . . . . . 7 |- ( ph -> ( x e. RR |-> -u -u ( sin ` x ) ) = ( x e. RR |-> ( sin ` x ) ) )
210	206, 209	eqtrd 2475	. . . . . 6 |- ( ph -> ( RR _D ( x e. RR |-> -u ( cos ` x ) ) ) = ( x e. RR |-> ( sin ` x ) ) )
211	142, 201, 145, 210, 193, 195, 194, 198	dvmptres2 21436	. . . . 5 |- ( ph -> ( RR _D ( x e. ( 0 [,] pi ) |-> -u ( cos ` x ) ) ) = ( x e. ( 0 (,) pi ) |-> ( sin ` x ) ) )
212		fveq2 5691	. . . . . . . . . . 11 |- ( x = 0 -> ( sin ` x ) = ( sin ` 0 ) )
213		sin0 13433	. . . . . . . . . . 11 |- ( sin ` 0 ) = 0
214	212, 213	syl6eq 2491	. . . . . . . . . 10 |- ( x = 0 -> ( sin ` x ) = 0 )
215	214	oveq1d 6106	. . . . . . . . 9 |- ( x = 0 -> ( ( sin ` x ) ^ N ) = ( 0 ^ N ) )
216	215	adantl 466	. . . . . . . 8 |- ( ( ph /\ x = 0 ) -> ( ( sin ` x ) ^ N ) = ( 0 ^ N ) )
217	19	adantr 465	. . . . . . . . 9 |- ( ( ph /\ x = 0 ) -> N e. NN )
218	217	0expd 12024	. . . . . . . 8 |- ( ( ph /\ x = 0 ) -> ( 0 ^ N ) = 0 )
219	216, 218	eqtrd 2475	. . . . . . 7 |- ( ( ph /\ x = 0 ) -> ( ( sin ` x ) ^ N ) = 0 )
220	219	oveq1d 6106	. . . . . 6 |- ( ( ph /\ x = 0 ) -> ( ( ( sin ` x ) ^ N ) x. -u ( cos ` x ) ) = ( 0 x. -u ( cos ` x ) ) )
221		id 22	. . . . . . . . . 10 |- ( x = 0 -> x = 0 )
222		0cn 9378	. . . . . . . . . 10 |- 0 e. CC
223	221, 222	syl6eqel 2531	. . . . . . . . 9 |- ( x = 0 -> x e. CC )
224		coscl 13411	. . . . . . . . . 10 |- ( x e. CC -> ( cos ` x ) e. CC )
225	224	negcld 9706	. . . . . . . . 9 |- ( x e. CC -> -u ( cos ` x ) e. CC )
226	223, 225	syl 16	. . . . . . . 8 |- ( x = 0 -> -u ( cos ` x ) e. CC )
227	226	adantl 466	. . . . . . 7 |- ( ( ph /\ x = 0 ) -> -u ( cos ` x ) e. CC )
228	227	mul02d 9567	. . . . . 6 |- ( ( ph /\ x = 0 ) -> ( 0 x. -u ( cos ` x ) ) = 0 )
229	220, 228	eqtrd 2475	. . . . 5 |- ( ( ph /\ x = 0 ) -> ( ( ( sin ` x ) ^ N ) x. -u ( cos ` x ) ) = 0 )
230		fveq2 5691	. . . . . . . . . . 11 |- ( x = pi -> ( sin ` x ) = ( sin ` pi ) )
231		sinpi 21920	. . . . . . . . . . 11 |- ( sin ` pi ) = 0
232	230, 231	syl6eq 2491	. . . . . . . . . 10 |- ( x = pi -> ( sin ` x ) = 0 )
233	232	oveq1d 6106	. . . . . . . . 9 |- ( x = pi -> ( ( sin ` x ) ^ N ) = ( 0 ^ N ) )
234	233	adantl 466	. . . . . . . 8 |- ( ( ph /\ x = pi ) -> ( ( sin ` x ) ^ N ) = ( 0 ^ N ) )
235	19	adantr 465	. . . . . . . . 9 |- ( ( ph /\ x = pi ) -> N e. NN )
236	235	0expd 12024	. . . . . . . 8 |- ( ( ph /\ x = pi ) -> ( 0 ^ N ) = 0 )
237	234, 236	eqtrd 2475	. . . . . . 7 |- ( ( ph /\ x = pi ) -> ( ( sin ` x ) ^ N ) = 0 )
238	237	oveq1d 6106	. . . . . 6 |- ( ( ph /\ x = pi ) -> ( ( ( sin ` x ) ^ N ) x. -u ( cos ` x ) ) = ( 0 x. -u ( cos ` x ) ) )
239		id 22	. . . . . . . . . . 11 |- ( x = pi -> x = pi )
240	5	recni 9398	. . . . . . . . . . 11 |- pi e. CC
241	239, 240	syl6eqel 2531	. . . . . . . . . 10 |- ( x = pi -> x e. CC )
242	241	coscld 13415	. . . . . . . . 9 |- ( x = pi -> ( cos ` x ) e. CC )
243	242	negcld 9706	. . . . . . . 8 |- ( x = pi -> -u ( cos ` x ) e. CC )
244	243	adantl 466	. . . . . . 7 |- ( ( ph /\ x = pi ) -> -u ( cos ` x ) e. CC )
245	244	mul02d 9567	. . . . . 6 |- ( ( ph /\ x = pi ) -> ( 0 x. -u ( cos ` x ) ) = 0 )
246	238, 245	eqtrd 2475	. . . . 5 |- ( ( ph /\ x = pi ) -> ( ( ( sin ` x ) ^ N ) x. -u ( cos ` x ) ) = 0 )
247	4, 6, 9, 37, 53, 91, 92, 115, 140, 199, 211, 229, 246	itgparts 21519	. . . 4 |- ( ph -> S. ( 0 (,) pi ) ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) _d x = ( ( 0 - 0 ) - S. ( 0 (,) pi ) ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) _d x ) )
248		df-neg 9598	. . . . 5 |- -u S. ( 0 (,) pi ) ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) _d x = ( 0 - S. ( 0 (,) pi ) ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) _d x )
249	248	a1i 11	. . . 4 |- ( ph -> -u S. ( 0 (,) pi ) ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) _d x = ( 0 - S. ( 0 (,) pi ) ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) _d x ) )
250	2, 247, 249	3eqtr4a 2501	. . 3 |- ( ph -> S. ( 0 (,) pi ) ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) _d x = -u S. ( 0 (,) pi ) ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) _d x )
251	66, 68, 68	mulassd 9409	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. ( cos ` x ) ) = ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( ( cos ` x ) x. ( cos ` x ) ) ) )
252		sqval 11925	. . . . . . . . . . . . . 14 |- ( ( cos ` x ) e. CC -> ( ( cos ` x ) ^ 2 ) = ( ( cos ` x ) x. ( cos ` x ) ) )
253	252	eqcomd 2448	. . . . . . . . . . . . 13 |- ( ( cos ` x ) e. CC -> ( ( cos ` x ) x. ( cos ` x ) ) = ( ( cos ` x ) ^ 2 ) )
254	67, 253	syl 16	. . . . . . . . . . . 12 |- ( x e. ( 0 (,) pi ) -> ( ( cos ` x ) x. ( cos ` x ) ) = ( ( cos ` x ) ^ 2 ) )
255	254	adantl 466	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( cos ` x ) x. ( cos ` x ) ) = ( ( cos ` x ) ^ 2 ) )
256	255	oveq2d 6107	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( ( cos ` x ) x. ( cos ` x ) ) ) = ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( ( cos ` x ) ^ 2 ) ) )
257	67	sqcld 12006	. . . . . . . . . . . 12 |- ( x e. ( 0 (,) pi ) -> ( ( cos ` x ) ^ 2 ) e. CC )
258	257	adantl 466	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( cos ` x ) ^ 2 ) e. CC )
259	59, 65, 258	mulassd 9409	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( ( cos ` x ) ^ 2 ) ) = ( N x. ( ( ( sin ` x ) ^ ( N - 1 ) ) x. ( ( cos ` x ) ^ 2 ) ) ) )
260	256, 259	eqtrd 2475	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( ( cos ` x ) x. ( cos ` x ) ) ) = ( N x. ( ( ( sin ` x ) ^ ( N - 1 ) ) x. ( ( cos ` x ) ^ 2 ) ) ) )
261	65, 258	mulcomd 9407	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( ( sin ` x ) ^ ( N - 1 ) ) x. ( ( cos ` x ) ^ 2 ) ) = ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) )
262	261	oveq2d 6107	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( N x. ( ( ( sin ` x ) ^ ( N - 1 ) ) x. ( ( cos ` x ) ^ 2 ) ) ) = ( N x. ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) )
263	251, 260, 262	3eqtrd 2479	. . . . . . . 8 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. ( cos ` x ) ) = ( N x. ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) )
264	263	negeqd 9604	. . . . . . 7 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> -u ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. ( cos ` x ) ) = -u ( N x. ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) )
265	69, 68	mulneg2d 9798	. . . . . . 7 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) = -u ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. ( cos ` x ) ) )
266	258, 65	mulcld 9406	. . . . . . . 8 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) e. CC )
267	59, 266	mulneg1d 9797	. . . . . . 7 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( -u N x. ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) = -u ( N x. ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) )
268	264, 265, 267	3eqtr4d 2485	. . . . . 6 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) = ( -u N x. ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) )
269	268	itgeq2dv 21259	. . . . 5 |- ( ph -> S. ( 0 (,) pi ) ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) _d x = S. ( 0 (,) pi ) ( -u N x. ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) _d x )
270	58	negcld 9706	. . . . . 6 |- ( ph -> -u N e. CC )
271	38	sqcld 12006	. . . . . . . . 9 |- ( x e. ( 0 [,] pi ) -> ( ( cos ` x ) ^ 2 ) e. CC )
272	271	adantl 466	. . . . . . . 8 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( cos ` x ) ^ 2 ) e. CC )
273	272, 118	mulcld 9406	. . . . . . 7 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) e. CC )
274		itgsinexplem1.6	. . . . . . . . . . . . 13 |- M = ( x e. CC |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) )
275	274	fvmpt2 5781	. . . . . . . . . . . 12 |- ( ( x e. CC /\ ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) e. CC ) -> ( M ` x ) = ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) )
276	16, 273, 275	syl2anc 661	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( M ` x ) = ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) )
277	276	eqcomd 2448	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) = ( M ` x ) )
278	277	mpteq2dva 4378	. . . . . . . . 9 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) = ( x e. ( 0 [,] pi ) |-> ( M ` x ) ) )
279		nfmpt1 4381	. . . . . . . . . . 11 |- F/_ x ( x e. CC |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) )
280	274, 279	nfcxfr 2576	. . . . . . . . . 10 |- F/_ x M
281		nfcv 2579	. . . . . . . . . . . . 13 |- F/_ x cos
282		2nn0 10596	. . . . . . . . . . . . . 14 |- 2 e. NN0
283	282	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> 2 e. NN0 )
284	281, 49, 283	expcnfg 29773	. . . . . . . . . . . 12 |- ( ph -> ( x e. CC |-> ( ( cos ` x ) ^ 2 ) ) e. ( CC -cn-> CC ) )
285	284, 81	mulcncf 20931	. . . . . . . . . . 11 |- ( ph -> ( x e. CC |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) e. ( CC -cn-> CC ) )
286	274, 285	syl5eqel 2527	. . . . . . . . . 10 |- ( ph -> M e. ( CC -cn-> CC ) )
287	280, 286, 35	cncfmptss 29768	. . . . . . . . 9 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( M ` x ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
288	278, 287	eqeltrd 2517	. . . . . . . 8 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
289		cniccibl 21318	. . . . . . . 8 |- ( ( 0 e. RR /\ pi e. RR /\ ( x e. ( 0 [,] pi ) |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) e. ( ( 0 [,] pi ) -cn-> CC ) ) -> ( x e. ( 0 [,] pi ) |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) e. L^1 )
290	4, 6, 288, 289	syl3anc 1218	. . . . . . 7 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) e. L^1 )
291	94, 96, 273, 290	iblss 21282	. . . . . 6 |- ( ph -> ( x e. ( 0 (,) pi ) |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) e. L^1 )
292	270, 266, 291	itgmulc2 21311	. . . . 5 |- ( ph -> ( -u N x. S. ( 0 (,) pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) _d x ) = S. ( 0 (,) pi ) ( -u N x. ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) _d x )
293	269, 292	eqtr4d 2478	. . . 4 |- ( ph -> S. ( 0 (,) pi ) ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) _d x = ( -u N x. S. ( 0 (,) pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) _d x ) )
294	293	negeqd 9604	. . 3 |- ( ph -> -u S. ( 0 (,) pi ) ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) _d x = -u ( -u N x. S. ( 0 (,) pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) _d x ) )
295	250, 294	eqtrd 2475	. 2 |- ( ph -> S. ( 0 (,) pi ) ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) _d x = -u ( -u N x. S. ( 0 (,) pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) _d x ) )
296	266, 291	itgcl 21261	. . . 4 |- ( ph -> S. ( 0 (,) pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) _d x e. CC )
297	58, 296	mulneg1d 9797	. . 3 |- ( ph -> ( -u N x. S. ( 0 (,) pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) _d x ) = -u ( N x. S. ( 0 (,) pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) _d x ) )
298	297	negeqd 9604	. 2 |- ( ph -> -u ( -u N x. S. ( 0 (,) pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) _d x ) = -u -u ( N x. S. ( 0 (,) pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) _d x ) )
299	58, 296	mulcld 9406	. . 3 |- ( ph -> ( N x. S. ( 0 (,) pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) _d x ) e. CC )
300	299	negnegd 9710	. 2 |- ( ph -> -u -u ( N x. S. ( 0 (,) pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) _d x ) = ( N x. S. ( 0 (,) pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) _d x ) )
301	295, 298, 300	3eqtrd 2479	1 |- ( ph -> S. ( 0 (,) pi ) ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) _d x = ( N x. S. ( 0 (,) pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) _d x ) )

Syntax hints:   -> wi 4   /\ wa 369   A.wal 1367   = wceq 1369   e. wcel 1756   {crab 2719   _Vcvv 2972   C_ wss 3328   {cpr 3879   class class class wbr 4292   e. cmpt 4350   dom cdm 4840   ran crn 4841   |` cres 4842   -->wf 5414   ` cfv 5418  (class class class)co 6091   CCcc 9280   RRcr 9281   0cc0 9282   1c1 9283   x. cmul 9287   <_ cle 9419   - cmin 9595   -ucneg 9596   NNcn 10322   2c2 10371   NN0cn0 10579   (,)cioo 11300   [,]cicc 11303   ^cexp 11865   sincsin 13349   cosccos 13350   picpi 13352   TopOpenctopn 14360   topGenctg 14376  ℂ_fldccnfld 17818   intcnt 18621   -cn->ccncf 20452   volcvol 20947   L^1cibl 21097   S.citg 21098   _D cdv 21338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4403  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372  ax-inf2 7847  ax-cc 8604  ax-cnex 9338  ax-resscn 9339  ax-1cn 9340  ax-icn 9341  ax-addcl 9342  ax-addrcl 9343  ax-mulcl 9344  ax-mulrcl 9345  ax-mulcom 9346  ax-addass 9347  ax-mulass 9348  ax-distr 9349  ax-i2m1 9350  ax-1ne0 9351  ax-1rid 9352  ax-rnegex 9353  ax-rrecex 9354  ax-cnre 9355  ax-pre-lttri 9356  ax-pre-lttrn 9357  ax-pre-ltadd 9358  ax-pre-mulgt0 9359  ax-pre-sup 9360  ax-addf 9361  ax-mulf 9362

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-nel 2609  df-ral 2720  df-rex 2721  df-reu 2722  df-rmo 2723  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-pss 3344  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-tp 3882  df-op 3884  df-uni 4092  df-int 4129  df-iun 4173  df-iin 4174  df-disj 4263  df-br 4293  df-opab 4351  df-mpt 4352  df-tr 4386  df-eprel 4632  df-id 4636  df-po 4641  df-so 4642  df-fr 4679  df-se 4680  df-we 4681  df-ord 4722  df-on 4723  df-lim 4724  df-suc 4725  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-isom 5427  df-riota 6052  df-ov 6094  df-oprab 6095  df-mpt2 6096  df-of 6320  df-ofr 6321  df-om 6477  df-1st 6577  df-2nd 6578  df-supp 6691  df-recs 6832  df-rdg 6866  df-1o 6920  df-2o 6921  df-oadd 6924  df-omul 6925  df-er 7101  df-map 7216  df-pm 7217  df-ixp 7264  df-en 7311  df-dom 7312  df-sdom 7313  df-fin 7314  df-fsupp 7621  df-fi 7661  df-sup 7691  df-oi 7724  df-card 8109  df-acn 8112  df-cda 8337  df-pnf 9420  df-mnf 9421  df-xr 9422  df-ltxr 9423  df-le 9424  df-sub 9597  df-neg 9598  df-div 9994  df-nn 10323  df-2 10380  df-3 10381  df-4 10382  df-5 10383  df-6 10384  df-7 10385  df-8 10386  df-9 10387  df-10 10388  df-n0 10580  df-z 10647  df-dec 10756  df-uz 10862  df-q 10954  df-rp 10992  df-xneg 11089  df-xadd 11090  df-xmul 11091  df-ioo 11304  df-ioc 11305  df-ico 11306  df-icc 11307  df-fz 11438  df-fzo 11549  df-fl 11642  df-mod 11709  df-seq 11807  df-exp 11866  df-fac 12052  df-bc 12079  df-hash 12104  df-shft 12556  df-cj 12588  df-re 12589  df-im 12590  df-sqr 12724  df-abs 12725  df-limsup 12949  df-clim 12966  df-rlim 12967  df-sum 13164  df-ef 13353  df-sin 13355  df-cos 13356  df-pi 13358  df-struct 14176  df-ndx 14177  df-slot 14178  df-base 14179  df-sets 14180  df-ress 14181  df-plusg 14251  df-mulr 14252  df-starv 14253  df-sca 14254  df-vsca 14255  df-ip 14256  df-tset 14257  df-ple 14258  df-ds 14260  df-unif 14261  df-hom 14262  df-cco 14263  df-rest 14361  df-topn 14362  df-0g 14380  df-gsum 14381  df-topgen 14382  df-pt 14383  df-prds 14386  df-xrs 14440  df-qtop 14445  df-imas 14446  df-xps 14448  df-mre 14524  df-mrc 14525  df-acs 14527  df-mnd 15415  df-submnd 15465  df-mulg 15548  df-cntz 15835  df-cmn 16279  df-psmet 17809  df-xmet 17810  df-met 17811  df-bl 17812  df-mopn 17813  df-fbas 17814  df-fg 17815  df-cnfld 17819  df-top 18503  df-bases 18505  df-topon 18506  df-topsp 18507  df-cld 18623  df-ntr 18624  df-cls 18625  df-nei 18702  df-lp 18740  df-perf 18741  df-cn 18831  df-cnp 18832  df-haus 18919  df-cmp 18990  df-tx 19135  df-hmeo 19328  df-fil 19419  df-fm 19511  df-flim 19512  df-flf 19513  df-xms 19895  df-ms 19896  df-tms 19897  df-cncf 20454  df-ovol 20948  df-vol 20949  df-mbf 21099  df-itg1 21100  df-itg2 21101  df-ibl 21102  df-itg 21103  df-0p 21148  df-limc 21341  df-dv 21342

This theorem is referenced by:  itgsinexp  29795