Theorem itgsinexplem1 31299

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 10645	. . . . 5 |- ( 0 - 0 ) = 0
2	1	oveq1i 6294	. . . 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 9596	. . . . . 6 |- 0 e. RR
4	3	a1i 11	. . . . 5 |- ( ph -> 0 e. RR )
5		pire 22613	. . . . . 6 |- pi e. RR
6	5	a1i 11	. . . . 5 |- ( ph -> pi e. RR )
7		pipos 22615	. . . . . . 7 |- 0 < pi
8	3, 5, 7	ltleii 9707	. . . . . 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 11606	. . . . . . . . . . . . 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 9549	. . . . . . . . . . . 12 |- RR C_ CC
14	12, 13	sstri 3513	. . . . . . . . . . 11 |- ( 0 [,] pi ) C_ CC
15	14	sseli 3500	. . . . . . . . . 10 |- ( x e. ( 0 [,] pi ) -> x e. CC )
16	15	adantl 466	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> x e. CC )
17	15	sincld 13726	. . . . . . . . . . 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 10852	. . . . . . . . . . 11 |- ( ph -> N e. NN0 )
21	20	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> N e. NN0 )
22	18, 21	expcld 12278	. . . . . . . . 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 5957	. . . . . . . . 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 2475	. . . . . . 7 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( sin ` x ) ^ N ) = ( F ` x ) )
27	26	mpteq2dva 4533	. . . . . 6 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( sin ` x ) ^ N ) ) = ( x e. ( 0 [,] pi ) |-> ( F ` x ) ) )
28		nfmpt1 4536	. . . . . . . 8 |- F/_ x ( x e. CC |-> ( ( sin ` x ) ^ N ) )
29	23, 28	nfcxfr 2627	. . . . . . 7 |- F/_ x F
30		nfcv 2629	. . . . . . . . 9 |- F/_ x sin
31		sincn 22601	. . . . . . . . . 10 |- sin e. ( CC -cn-> CC )
32	31	a1i 11	. . . . . . . . 9 |- ( ph -> sin e. ( CC -cn-> CC ) )
33	30, 32, 20	expcnfg 31170	. . . . . . . 8 |- ( ph -> ( x e. CC |-> ( ( sin ` x ) ^ N ) ) e. ( CC -cn-> CC ) )
34	23, 33	syl5eqel 2559	. . . . . . 7 |- ( ph -> F e. ( CC -cn-> CC ) )
35	14	a1i 11	. . . . . . 7 |- ( ph -> ( 0 [,] pi ) C_ CC )
36	29, 34, 35	cncfmptss 31165	. . . . . 6 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( F ` x ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
37	27, 36	eqeltrd 2555	. . . . 5 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( sin ` x ) ^ N ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
38	15	coscld 13727	. . . . . . . . . . 11 |- ( x e. ( 0 [,] pi ) -> ( cos ` x ) e. CC )
39	38	negcld 9917	. . . . . . . . . 10 |- ( x e. ( 0 [,] pi ) -> -u ( cos ` x ) e. CC )
40		itgsinexplem1.2	. . . . . . . . . . 11 |- G = ( x e. CC |-> -u ( cos ` x ) )
41	40	fvmpt2 5957	. . . . . . . . . 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 2475	. . . . . . . 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 4533	. . . . . 6 |- ( ph -> ( x e. ( 0 [,] pi ) |-> -u ( cos ` x ) ) = ( x e. ( 0 [,] pi ) |-> ( G ` x ) ) )
46		nfmpt1 4536	. . . . . . . 8 |- F/_ x ( x e. CC |-> -u ( cos ` x ) )
47	40, 46	nfcxfr 2627	. . . . . . 7 |- F/_ x G
48		coscn 22602	. . . . . . . . 9 |- cos e. ( CC -cn-> CC )
49	48	a1i 11	. . . . . . . 8 |- ( ph -> cos e. ( CC -cn-> CC ) )
50	40	negfcncf 21186	. . . . . . . 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 31165	. . . . . 6 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( G ` x ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
53	45, 52	eqeltrd 2555	. . . . 5 |- ( ph -> ( x e. ( 0 [,] pi ) |-> -u ( cos ` x ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
54		ioossre 11586	. . . . . . . . . . . 12 |- ( 0 (,) pi ) C_ RR
55	54, 13	sstri 3513	. . . . . . . . . . 11 |- ( 0 (,) pi ) C_ CC
56	55	sseli 3500	. . . . . . . . . 10 |- ( x e. ( 0 (,) pi ) -> x e. CC )
57	56	adantl 466	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> x e. CC )
58	19	nncnd 10552	. . . . . . . . . . . 12 |- ( ph -> N e. CC )
59	58	adantr 465	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> N e. CC )
60	56	sincld 13726	. . . . . . . . . . . . 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 10837	. . . . . . . . . . . . . 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 12278	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( sin ` x ) ^ ( N - 1 ) ) e. CC )
66	59, 65	mulcld 9616	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) e. CC )
67	56	coscld 13727	. . . . . . . . . . 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 9616	. . . . . . . . 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 5957	. . . . . . . . 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 2475	. . . . . . 7 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) = ( H ` x ) )
74	73	mpteq2dva 4533	. . . . . 6 |- ( ph -> ( x e. ( 0 (,) pi ) |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) = ( x e. ( 0 (,) pi ) |-> ( H ` x ) ) )
75		nfmpt1 4536	. . . . . . . 8 |- F/_ x ( x e. CC |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) )
76	70, 75	nfcxfr 2627	. . . . . . 7 |- F/_ x H
77		ssid 3523	. . . . . . . . . . . 12 |- CC C_ CC
78	77	a1i 11	. . . . . . . . . . 11 |- ( ph -> CC C_ CC )
79		cncfmptc 21178	. . . . . . . . . . 11 |- ( ( N e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> N ) e. ( CC -cn-> CC ) )
80	58, 78, 78, 79	syl3anc 1228	. . . . . . . . . 10 |- ( ph -> ( x e. CC |-> N ) e. ( CC -cn-> CC ) )
81	30, 32, 63	expcnfg 31170	. . . . . . . . . 10 |- ( ph -> ( x e. CC |-> ( ( sin ` x ) ^ ( N - 1 ) ) ) e. ( CC -cn-> CC ) )
82	80, 81	mulcncf 21622	. . . . . . . . 9 |- ( ph -> ( x e. CC |-> ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) e. ( CC -cn-> CC ) )
83		cosf 13721	. . . . . . . . . . . 12 |- cos : CC --> CC
84	83	a1i 11	. . . . . . . . . . 11 |- ( ph -> cos : CC --> CC )
85	84	feqmptd 5920	. . . . . . . . . 10 |- ( ph -> cos = ( x e. CC |-> ( cos ` x ) ) )
86	85, 48	syl6eqelr 2564	. . . . . . . . 9 |- ( ph -> ( x e. CC |-> ( cos ` x ) ) e. ( CC -cn-> CC ) )
87	82, 86	mulcncf 21622	. . . . . . . 8 |- ( ph -> ( x e. CC |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) e. ( CC -cn-> CC ) )
88	70, 87	syl5eqel 2559	. . . . . . 7 |- ( ph -> H e. ( CC -cn-> CC ) )
89	55	a1i 11	. . . . . . 7 |- ( ph -> ( 0 (,) pi ) C_ CC )
90	76, 88, 89	cncfmptss 31165	. . . . . 6 |- ( ph -> ( x e. ( 0 (,) pi ) |-> ( H ` x ) ) e. ( ( 0 (,) pi ) -cn-> CC ) )
91	74, 90	eqeltrd 2555	. . . . 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 31165	. . . . 5 |- ( ph -> ( x e. ( 0 (,) pi ) |-> ( sin ` x ) ) e. ( ( 0 (,) pi ) -cn-> CC ) )
93		ioossicc 11610	. . . . . . 7 |- ( 0 (,) pi ) C_ ( 0 [,] pi )
94	93	a1i 11	. . . . . 6 |- ( ph -> ( 0 (,) pi ) C_ ( 0 [,] pi ) )
95		ioombl 21738	. . . . . . 7 |- ( 0 (,) pi ) e. dom vol
96	95	a1i 11	. . . . . 6 |- ( ph -> ( 0 (,) pi ) e. dom vol )
97	22, 18	mulcld 9616	. . . . . 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 5957	. . . . . . . . . . 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 2475	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) = ( I ` x ) )
102	101	mpteq2dva 4533	. . . . . . . 8 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) ) = ( x e. ( 0 [,] pi ) |-> ( I ` x ) ) )
103		nfmpt1 4536	. . . . . . . . . 10 |- F/_ x ( x e. CC |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) )
104	98, 103	nfcxfr 2627	. . . . . . . . 9 |- F/_ x I
105		sinf 13720	. . . . . . . . . . . . . 14 |- sin : CC --> CC
106	105	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> sin : CC --> CC )
107	106	feqmptd 5920	. . . . . . . . . . . 12 |- ( ph -> sin = ( x e. CC |-> ( sin ` x ) ) )
108	107, 31	syl6eqelr 2564	. . . . . . . . . . 11 |- ( ph -> ( x e. CC |-> ( sin ` x ) ) e. ( CC -cn-> CC ) )
109	33, 108	mulcncf 21622	. . . . . . . . . 10 |- ( ph -> ( x e. CC |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) ) e. ( CC -cn-> CC ) )
110	98, 109	syl5eqel 2559	. . . . . . . . 9 |- ( ph -> I e. ( CC -cn-> CC ) )
111	104, 110, 35	cncfmptss 31165	. . . . . . . 8 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( I ` x ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
112	102, 111	eqeltrd 2555	. . . . . . 7 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
113		cniccibl 22010	. . . . . . 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 1228	. . . . . 6 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) ) e. L^1 )
115	94, 96, 97, 114	iblss 21974	. . . . 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 12278	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( sin ` x ) ^ ( N - 1 ) ) e. CC )
119	116, 118	mulcld 9616	. . . . . . . 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 9616	. . . . . . 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 9616	. . . . . 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 5957	. . . . . . . . . . 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 2475	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) = ( L ` x ) )
128	127	mpteq2dva 4533	. . . . . . . 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 4536	. . . . . . . . . 10 |- F/_ x ( x e. CC |-> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) )
130	124, 129	nfcxfr 2627	. . . . . . . . 9 |- F/_ x L
131		eqid 2467	. . . . . . . . . . . . 13 |- ( x e. CC |-> -u ( cos ` x ) ) = ( x e. CC |-> -u ( cos ` x ) )
132	131	negfcncf 21186	. . . . . . . . . . . 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 21622	. . . . . . . . . 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 2559	. . . . . . . . 9 |- ( ph -> L e. ( CC -cn-> CC ) )
136	130, 135, 35	cncfmptss 31165	. . . . . . . 8 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( L ` x ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
137	128, 136	eqeltrd 2555	. . . . . . 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 22010	. . . . . . 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 1228	. . . . . 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 21974	. . . . 5 |- ( ph -> ( x e. ( 0 (,) pi ) |-> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) ) e. L^1 )
141		reelprrecn 9584	. . . . . . 7 |- RR e. { RR , CC }
142	141	a1i 11	. . . . . 6 |- ( ph -> RR e. { RR , CC } )
143		recn 9582	. . . . . . . . 9 |- ( x e. RR -> x e. CC )
144	143	sincld 13726	. . . . . . . 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 12278	. . . . . 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 12278	. . . . . . . 8 |- ( ( ph /\ x e. RR ) -> ( ( sin ` x ) ^ ( N - 1 ) ) e. CC )
151	148, 150	mulcld 9616	. . . . . . 7 |- ( ( ph /\ x e. RR ) -> ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) e. CC )
152	143	coscld 13727	. . . . . . . 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 9616	. . . . . 6 |- ( ( ph /\ x e. RR ) -> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) e. CC )
155		sincl 13722	. . . . . . . . . . 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 12278	. . . . . . . . 9 |- ( ( ph /\ x e. CC ) -> ( ( sin ` x ) ^ N ) e. CC )
159	158, 23	fmptd 6045	. . . . . . . 8 |- ( ph -> F : CC --> CC )
160	143	adantl 466	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> x e. CC )
161		elex 3122	. . . . . . . . . . . . . . 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 3038	. . . . . . . . . . . . . 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 5502	. . . . . . . . . . . . 13 |- dom H = { x e. CC | ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) e. _V }
166	164, 165	syl6eleqr 2566	. . . . . . . . . . . 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 1695	. . . . . . . . . 10 |- ( ph -> A. x ( x e. RR -> x e. dom H ) )
169		nfcv 2629	. . . . . . . . . . 11 |- F/_ x RR
170	76	nfdm 5244	. . . . . . . . . . 11 |- F/_ x dom H
171	169, 170	dfss2f 3495	. . . . . . . . . 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 31266	. . . . . . . . . . 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 6295	. . . . . . . . . . 11 |- ( CC _D F ) = ( CC _D ( x e. CC |-> ( ( sin ` x ) ^ N ) ) )
175	173, 174, 70	3eqtr4g 2533	. . . . . . . . . 10 |- ( ph -> ( CC _D F ) = H )
176	175	dmeqd 5205	. . . . . . . . 9 |- ( ph -> dom ( CC _D F ) = dom H )
177	172, 176	sseqtr4d 3541	. . . . . . . 8 |- ( ph -> RR C_ dom ( CC _D F ) )
178		dvres3 22080	. . . . . . . 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 1229	. . . . . . 7 |- ( ph -> ( RR _D ( F |` RR ) ) = ( ( CC _D F ) |` RR ) )
180	23	reseq1i 5269	. . . . . . . . . 10 |- ( F |` RR ) = ( ( x e. CC |-> ( ( sin ` x ) ^ N ) ) |` RR )
181		resmpt 5323	. . . . . . . . . . 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 2496	. . . . . . . . 9 |- ( F |` RR ) = ( x e. RR |-> ( ( sin ` x ) ^ N ) )
184	183	oveq2i 6295	. . . . . . . 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 5272	. . . . . . . 8 |- ( ph -> ( ( CC _D F ) |` RR ) = ( H |` RR ) )
187	70	reseq1i 5269	. . . . . . . . 9 |- ( H |` RR ) = ( ( x e. CC |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) |` RR )
188		resmpt 5323	. . . . . . . . . 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 2496	. . . . . . . 8 |- ( H |` RR ) = ( x e. RR |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) )
191	186, 190	syl6eq 2524	. . . . . . 7 |- ( ph -> ( ( CC _D F ) |` RR ) = ( x e. RR |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) )
192	179, 185, 191	3eqtr3d 2516	. . . . . 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 2467	. . . . . . 7 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
195	194	tgioo2 21071	. . . . . 6 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
196	10	a1i 11	. . . . . . 7 |- ( ph -> ( 0 e. RR /\ pi e. RR ) )
197		iccntr 21089	. . . . . . 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 22128	. . . . 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 9917	. . . . . . 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 9917	. . . . . . . . 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 31267	. . . . . . . . 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 22132	. . . . . . 7 |- ( ph -> ( RR _D ( x e. RR |-> -u ( cos ` x ) ) ) = ( x e. RR |-> -u -u ( sin ` x ) ) )
207	144	negnegd 9921	. . . . . . . . 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 4533	. . . . . . 7 |- ( ph -> ( x e. RR |-> -u -u ( sin ` x ) ) = ( x e. RR |-> ( sin ` x ) ) )
210	206, 209	eqtrd 2508	. . . . . 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 22128	. . . . 5 |- ( ph -> ( RR _D ( x e. ( 0 [,] pi ) |-> -u ( cos ` x ) ) ) = ( x e. ( 0 (,) pi ) |-> ( sin ` x ) ) )
212		fveq2 5866	. . . . . . . . . . 11 |- ( x = 0 -> ( sin ` x ) = ( sin ` 0 ) )
213		sin0 13745	. . . . . . . . . . 11 |- ( sin ` 0 ) = 0
214	212, 213	syl6eq 2524	. . . . . . . . . 10 |- ( x = 0 -> ( sin ` x ) = 0 )
215	214	oveq1d 6299	. . . . . . . . 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 12294	. . . . . . . 8 |- ( ( ph /\ x = 0 ) -> ( 0 ^ N ) = 0 )
219	216, 218	eqtrd 2508	. . . . . . 7 |- ( ( ph /\ x = 0 ) -> ( ( sin ` x ) ^ N ) = 0 )
220	219	oveq1d 6299	. . . . . 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 9588	. . . . . . . . . 10 |- 0 e. CC
223	221, 222	syl6eqel 2563	. . . . . . . . 9 |- ( x = 0 -> x e. CC )
224		coscl 13723	. . . . . . . . . 10 |- ( x e. CC -> ( cos ` x ) e. CC )
225	224	negcld 9917	. . . . . . . . 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 9777	. . . . . 6 |- ( ( ph /\ x = 0 ) -> ( 0 x. -u ( cos ` x ) ) = 0 )
229	220, 228	eqtrd 2508	. . . . 5 |- ( ( ph /\ x = 0 ) -> ( ( ( sin ` x ) ^ N ) x. -u ( cos ` x ) ) = 0 )
230		fveq2 5866	. . . . . . . . . . 11 |- ( x = pi -> ( sin ` x ) = ( sin ` pi ) )
231		sinpi 22612	. . . . . . . . . . 11 |- ( sin ` pi ) = 0
232	230, 231	syl6eq 2524	. . . . . . . . . 10 |- ( x = pi -> ( sin ` x ) = 0 )
233	232	oveq1d 6299	. . . . . . . . 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 12294	. . . . . . . 8 |- ( ( ph /\ x = pi ) -> ( 0 ^ N ) = 0 )
237	234, 236	eqtrd 2508	. . . . . . 7 |- ( ( ph /\ x = pi ) -> ( ( sin ` x ) ^ N ) = 0 )
238	237	oveq1d 6299	. . . . . 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 9608	. . . . . . . . . . 11 |- pi e. CC
241	239, 240	syl6eqel 2563	. . . . . . . . . 10 |- ( x = pi -> x e. CC )
242	241	coscld 13727	. . . . . . . . 9 |- ( x = pi -> ( cos ` x ) e. CC )
243	242	negcld 9917	. . . . . . . 8 |- ( x = pi -> -u ( cos ` x ) e. CC )
244	243	adantl 466	. . . . . . 7 |- ( ( ph /\ x = pi ) -> -u ( cos ` x ) e. CC )
245	244	mul02d 9777	. . . . . 6 |- ( ( ph /\ x = pi ) -> ( 0 x. -u ( cos ` x ) ) = 0 )
246	238, 245	eqtrd 2508	. . . . 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 22211	. . . 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 9808	. . . . 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 2534	. . 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 9619	. . . . . . . . 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 12195	. . . . . . . . . . . . . 14 |- ( ( cos ` x ) e. CC -> ( ( cos ` x ) ^ 2 ) = ( ( cos ` x ) x. ( cos ` x ) ) )
253	252	eqcomd 2475	. . . . . . . . . . . . 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 6300	. . . . . . . . . 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 12276	. . . . . . . . . . . 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 9619	. . . . . . . . . 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 2508	. . . . . . . . 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 9617	. . . . . . . . . 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 6300	. . . . . . . . 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 2512	. . . . . . . 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 9814	. . . . . . 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 10010	. . . . . . 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 9616	. . . . . . . 8 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) e. CC )
267	59, 266	mulneg1d 10009	. . . . . . 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 2518	. . . . . 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 21951	. . . . 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 9917	. . . . . 6 |- ( ph -> -u N e. CC )
271	38	sqcld 12276	. . . . . . . . 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 9616	. . . . . . 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 5957	. . . . . . . . . . . 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 2475	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) = ( M ` x ) )
278	277	mpteq2dva 4533	. . . . . . . . 9 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) = ( x e. ( 0 [,] pi ) |-> ( M ` x ) ) )
279		nfmpt1 4536	. . . . . . . . . . 11 |- F/_ x ( x e. CC |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) )
280	274, 279	nfcxfr 2627	. . . . . . . . . 10 |- F/_ x M
281		nfcv 2629	. . . . . . . . . . . . 13 |- F/_ x cos
282		2nn0 10812	. . . . . . . . . . . . . 14 |- 2 e. NN0
283	282	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> 2 e. NN0 )
284	281, 49, 283	expcnfg 31170	. . . . . . . . . . . 12 |- ( ph -> ( x e. CC |-> ( ( cos ` x ) ^ 2 ) ) e. ( CC -cn-> CC ) )
285	284, 81	mulcncf 21622	. . . . . . . . . . 11 |- ( ph -> ( x e. CC |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) e. ( CC -cn-> CC ) )
286	274, 285	syl5eqel 2559	. . . . . . . . . 10 |- ( ph -> M e. ( CC -cn-> CC ) )
287	280, 286, 35	cncfmptss 31165	. . . . . . . . 9 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( M ` x ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
288	278, 287	eqeltrd 2555	. . . . . . . 8 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
289		cniccibl 22010	. . . . . . . 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 1228	. . . . . . 7 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) e. L^1 )
291	94, 96, 273, 290	iblss 21974	. . . . . 6 |- ( ph -> ( x e. ( 0 (,) pi ) |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) e. L^1 )
292	270, 266, 291	itgmulc2 22003	. . . . 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 2511	. . . 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 9814	. . 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 2508	. 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 21953	. . . 4 |- ( ph -> S. ( 0 (,) pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) _d x e. CC )
297	58, 296	mulneg1d 10009	. . 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 9814	. 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 9616	. . 3 |- ( ph -> ( N x. S. ( 0 (,) pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) _d x ) e. CC )
300	299	negnegd 9921	. 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 2512	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 1377   = wceq 1379   e. wcel 1767   {crab 2818   _Vcvv 3113   C_ wss 3476   {cpr 4029   class class class wbr 4447   |-> cmpt 4505   dom cdm 4999   ran crn 5000   |` cres 5001   -->wf 5584   ` cfv 5588  (class class class)co 6284   CCcc 9490   RRcr 9491   0cc0 9492   1c1 9493   x. cmul 9497   <_ cle 9629   - cmin 9805   -ucneg 9806   NNcn 10536   2c2 10585   NN0cn0 10795   (,)cioo 11529   [,]cicc 11532   ^cexp 12134   sincsin 13661   cosccos 13662   picpi 13664   TopOpenctopn 14677   topGenctg 14693  ℂ_fldccnfld 18219   intcnt 19312   -cn->ccncf 21143   volcvol 21638   L^1cibl 21789   S.citg 21790   _D cdv 22030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6576  ax-inf2 8058  ax-cc 8815  ax-cnex 9548  ax-resscn 9549  ax-1cn 9550  ax-icn 9551  ax-addcl 9552  ax-addrcl 9553  ax-mulcl 9554  ax-mulrcl 9555  ax-mulcom 9556  ax-addass 9557  ax-mulass 9558  ax-distr 9559  ax-i2m1 9560  ax-1ne0 9561  ax-1rid 9562  ax-rnegex 9563  ax-rrecex 9564  ax-cnre 9565  ax-pre-lttri 9566  ax-pre-lttrn 9567  ax-pre-ltadd 9568  ax-pre-mulgt0 9569  ax-pre-sup 9570  ax-addf 9571  ax-mulf 9572

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-iin 4328  df-disj 4418  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-f1 5593  df-fo 5594  df-f1o 5595  df-fv 5596  df-isom 5597  df-riota 6245  df-ov 6287  df-oprab 6288  df-mpt2 6289  df-of 6524  df-ofr 6525  df-om 6685  df-1st 6784  df-2nd 6785  df-supp 6902  df-recs 7042  df-rdg 7076  df-1o 7130  df-2o 7131  df-oadd 7134  df-omul 7135  df-er 7311  df-map 7422  df-pm 7423  df-ixp 7470  df-en 7517  df-dom 7518  df-sdom 7519  df-fin 7520  df-fsupp 7830  df-fi 7871  df-sup 7901  df-oi 7935  df-card 8320  df-acn 8323  df-cda 8548  df-pnf 9630  df-mnf 9631  df-xr 9632  df-ltxr 9633  df-le 9634  df-sub 9807  df-neg 9808  df-div 10207  df-nn 10537  df-2 10594  df-3 10595  df-4 10596  df-5 10597  df-6 10598  df-7 10599  df-8 10600  df-9 10601  df-10 10602  df-n0 10796  df-z 10865  df-dec 10977  df-uz 11083  df-q 11183  df-rp 11221  df-xneg 11318  df-xadd 11319  df-xmul 11320  df-ioo 11533  df-ioc 11534  df-ico 11535  df-icc 11536  df-fz 11673  df-fzo 11793  df-fl 11897  df-mod 11965  df-seq 12076  df-exp 12135  df-fac 12322  df-bc 12349  df-hash 12374  df-shft 12863  df-cj 12895  df-re 12896  df-im 12897  df-sqrt 13031  df-abs 13032  df-limsup 13257  df-clim 13274  df-rlim 13275  df-sum 13472  df-ef 13665  df-sin 13667  df-cos 13668  df-pi 13670  df-struct 14492  df-ndx 14493  df-slot 14494  df-base 14495  df-sets 14496  df-ress 14497  df-plusg 14568  df-mulr 14569  df-starv 14570  df-sca 14571  df-vsca 14572  df-ip 14573  df-tset 14574  df-ple 14575  df-ds 14577  df-unif 14578  df-hom 14579  df-cco 14580  df-rest 14678  df-topn 14679  df-0g 14697  df-gsum 14698  df-topgen 14699  df-pt 14700  df-prds 14703  df-xrs 14757  df-qtop 14762  df-imas 14763  df-xps 14765  df-mre 14841  df-mrc 14842  df-acs 14844  df-mnd 15732  df-submnd 15787  df-mulg 15870  df-cntz 16160  df-cmn 16606  df-psmet 18210  df-xmet 18211  df-met 18212  df-bl 18213  df-mopn 18214  df-fbas 18215  df-fg 18216  df-cnfld 18220  df-top 19194  df-bases 19196  df-topon 19197  df-topsp 19198  df-cld 19314  df-ntr 19315  df-cls 19316  df-nei 19393  df-lp 19431  df-perf 19432  df-cn 19522  df-cnp 19523  df-haus 19610  df-cmp 19681  df-tx 19826  df-hmeo 20019  df-fil 20110  df-fm 20202  df-flim 20203  df-flf 20204  df-xms 20586  df-ms 20587  df-tms 20588  df-cncf 21145  df-ovol 21639  df-vol 21640  df-mbf 21791  df-itg1 21792  df-itg2 21793  df-ibl 21794  df-itg 21795  df-0p 21840  df-limc 22033  df-dv 22034

This theorem is referenced by:  itgsinexp  31300