Theorem itgsinexplem1 29644

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 10423	. . . . 5 |- ( 0 - 0 ) = 0
2	1	oveq1i 6094	. . . 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 9378	. . . . . 6 |- 0 e. RR
4	3	a1i 11	. . . . 5 |- ( ph -> 0 e. RR )
5		pire 21810	. . . . . 6 |- pi e. RR
6	5	a1i 11	. . . . 5 |- ( ph -> pi e. RR )
7		pipos 21812	. . . . . . 7 |- 0 < pi
8	3, 5, 7	ltleii 9489	. . . . . 6 |- 0 <_ pi
9	8	a1i 11	. . . . 5 |- ( ph -> 0 <_ pi )
10	3, 5	pm3.2i 452	. . . . . . . . . . . . 13 |- ( 0 e. RR /\ pi e. RR )
11		iccssre 11369	. . . . . . . . . . . . 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 9331	. . . . . . . . . . . 12 |- RR C_ CC
14	12, 13	sstri 3357	. . . . . . . . . . 11 |- ( 0 [,] pi ) C_ CC
15	14	sseli 3344	. . . . . . . . . 10 |- ( x e. ( 0 [,] pi ) -> x e. CC )
16	15	adantl 463	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> x e. CC )
17	15	sincld 13401	. . . . . . . . . . 11 |- ( x e. ( 0 [,] pi ) -> ( sin ` x ) e. CC )
18	17	adantl 463	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( sin ` x ) e. CC )
19		itgsinexplem1.7	. . . . . . . . . . . 12 |- ( ph -> N e. NN )
20	19	nnnn0d 10628	. . . . . . . . . . 11 |- ( ph -> N e. NN0 )
21	20	adantr 462	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> N e. NN0 )
22	18, 21	expcld 11996	. . . . . . . . 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 5773	. . . . . . . . 9 |- ( ( x e. CC /\ ( ( sin ` x ) ^ N ) e. CC ) -> ( F ` x ) = ( ( sin ` x ) ^ N ) )
25	16, 22, 24	syl2anc 656	. . . . . . . 8 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( F ` x ) = ( ( sin ` x ) ^ N ) )
26	25	eqcomd 2442	. . . . . . 7 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( sin ` x ) ^ N ) = ( F ` x ) )
27	26	mpteq2dva 4370	. . . . . 6 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( sin ` x ) ^ N ) ) = ( x e. ( 0 [,] pi ) |-> ( F ` x ) ) )
28		nfmpt1 4373	. . . . . . . 8 |- F/_ x ( x e. CC |-> ( ( sin ` x ) ^ N ) )
29	23, 28	nfcxfr 2570	. . . . . . 7 |- F/_ x F
30		nfcv 2573	. . . . . . . . 9 |- F/_ x sin
31		sincn 21798	. . . . . . . . . 10 |- sin e. ( CC -cn-> CC )
32	31	a1i 11	. . . . . . . . 9 |- ( ph -> sin e. ( CC -cn-> CC ) )
33	30, 32, 20	expcnfg 29623	. . . . . . . 8 |- ( ph -> ( x e. CC |-> ( ( sin ` x ) ^ N ) ) e. ( CC -cn-> CC ) )
34	23, 33	syl5eqel 2521	. . . . . . 7 |- ( ph -> F e. ( CC -cn-> CC ) )
35	14	a1i 11	. . . . . . 7 |- ( ph -> ( 0 [,] pi ) C_ CC )
36	29, 34, 35	cncfmptss 29617	. . . . . 6 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( F ` x ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
37	27, 36	eqeltrd 2511	. . . . 5 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( sin ` x ) ^ N ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
38	15	coscld 13402	. . . . . . . . . . 11 |- ( x e. ( 0 [,] pi ) -> ( cos ` x ) e. CC )
39	38	negcld 9698	. . . . . . . . . 10 |- ( x e. ( 0 [,] pi ) -> -u ( cos ` x ) e. CC )
40		itgsinexplem1.2	. . . . . . . . . . 11 |- G = ( x e. CC |-> -u ( cos ` x ) )
41	40	fvmpt2 5773	. . . . . . . . . 10 |- ( ( x e. CC /\ -u ( cos ` x ) e. CC ) -> ( G ` x ) = -u ( cos ` x ) )
42	15, 39, 41	syl2anc 656	. . . . . . . . 9 |- ( x e. ( 0 [,] pi ) -> ( G ` x ) = -u ( cos ` x ) )
43	42	eqcomd 2442	. . . . . . . 8 |- ( x e. ( 0 [,] pi ) -> -u ( cos ` x ) = ( G ` x ) )
44	43	adantl 463	. . . . . . 7 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> -u ( cos ` x ) = ( G ` x ) )
45	44	mpteq2dva 4370	. . . . . 6 |- ( ph -> ( x e. ( 0 [,] pi ) |-> -u ( cos ` x ) ) = ( x e. ( 0 [,] pi ) |-> ( G ` x ) ) )
46		nfmpt1 4373	. . . . . . . 8 |- F/_ x ( x e. CC |-> -u ( cos ` x ) )
47	40, 46	nfcxfr 2570	. . . . . . 7 |- F/_ x G
48		coscn 21799	. . . . . . . . 9 |- cos e. ( CC -cn-> CC )
49	48	a1i 11	. . . . . . . 8 |- ( ph -> cos e. ( CC -cn-> CC ) )
50	40	negfcncf 20341	. . . . . . . 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 29617	. . . . . 6 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( G ` x ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
53	45, 52	eqeltrd 2511	. . . . 5 |- ( ph -> ( x e. ( 0 [,] pi ) |-> -u ( cos ` x ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
54		ioossre 11349	. . . . . . . . . . . 12 |- ( 0 (,) pi ) C_ RR
55	54, 13	sstri 3357	. . . . . . . . . . 11 |- ( 0 (,) pi ) C_ CC
56	55	sseli 3344	. . . . . . . . . 10 |- ( x e. ( 0 (,) pi ) -> x e. CC )
57	56	adantl 463	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> x e. CC )
58	19	nncnd 10330	. . . . . . . . . . . 12 |- ( ph -> N e. CC )
59	58	adantr 462	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> N e. CC )
60	56	sincld 13401	. . . . . . . . . . . . 13 |- ( x e. ( 0 (,) pi ) -> ( sin ` x ) e. CC )
61	60	adantl 463	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( sin ` x ) e. CC )
62		nnm1nn0 10613	. . . . . . . . . . . . . 14 |- ( N e. NN -> ( N - 1 ) e. NN0 )
63	19, 62	syl 16	. . . . . . . . . . . . 13 |- ( ph -> ( N - 1 ) e. NN0 )
64	63	adantr 462	. . . . . . . . . . . 12 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( N - 1 ) e. NN0 )
65	61, 64	expcld 11996	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( sin ` x ) ^ ( N - 1 ) ) e. CC )
66	59, 65	mulcld 9398	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) e. CC )
67	56	coscld 13402	. . . . . . . . . . 11 |- ( x e. ( 0 (,) pi ) -> ( cos ` x ) e. CC )
68	67	adantl 463	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( cos ` x ) e. CC )
69	66, 68	mulcld 9398	. . . . . . . . 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 5773	. . . . . . . . 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 656	. . . . . . . 8 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( H ` x ) = ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) )
73	72	eqcomd 2442	. . . . . . 7 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) = ( H ` x ) )
74	73	mpteq2dva 4370	. . . . . 6 |- ( ph -> ( x e. ( 0 (,) pi ) |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) = ( x e. ( 0 (,) pi ) |-> ( H ` x ) ) )
75		nfmpt1 4373	. . . . . . . 8 |- F/_ x ( x e. CC |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) )
76	70, 75	nfcxfr 2570	. . . . . . 7 |- F/_ x H
77		ssid 3367	. . . . . . . . . . . 12 |- CC C_ CC
78	77	a1i 11	. . . . . . . . . . 11 |- ( ph -> CC C_ CC )
79		cncfmptc 20333	. . . . . . . . . . 11 |- ( ( N e. CC /\ CC C_ CC /\ CC C_ CC ) -> ( x e. CC |-> N ) e. ( CC -cn-> CC ) )
80	58, 78, 78, 79	syl3anc 1213	. . . . . . . . . 10 |- ( ph -> ( x e. CC |-> N ) e. ( CC -cn-> CC ) )
81	30, 32, 63	expcnfg 29623	. . . . . . . . . 10 |- ( ph -> ( x e. CC |-> ( ( sin ` x ) ^ ( N - 1 ) ) ) e. ( CC -cn-> CC ) )
82	80, 81	mulcncf 20777	. . . . . . . . 9 |- ( ph -> ( x e. CC |-> ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) e. ( CC -cn-> CC ) )
83		cosf 13396	. . . . . . . . . . . 12 |- cos : CC --> CC
84	83	a1i 11	. . . . . . . . . . 11 |- ( ph -> cos : CC --> CC )
85	84	feqmptd 5736	. . . . . . . . . 10 |- ( ph -> cos = ( x e. CC |-> ( cos ` x ) ) )
86	85, 48	syl6eqelr 2526	. . . . . . . . 9 |- ( ph -> ( x e. CC |-> ( cos ` x ) ) e. ( CC -cn-> CC ) )
87	82, 86	mulcncf 20777	. . . . . . . 8 |- ( ph -> ( x e. CC |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) e. ( CC -cn-> CC ) )
88	70, 87	syl5eqel 2521	. . . . . . 7 |- ( ph -> H e. ( CC -cn-> CC ) )
89	55	a1i 11	. . . . . . 7 |- ( ph -> ( 0 (,) pi ) C_ CC )
90	76, 88, 89	cncfmptss 29617	. . . . . 6 |- ( ph -> ( x e. ( 0 (,) pi ) |-> ( H ` x ) ) e. ( ( 0 (,) pi ) -cn-> CC ) )
91	74, 90	eqeltrd 2511	. . . . 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 29617	. . . . 5 |- ( ph -> ( x e. ( 0 (,) pi ) |-> ( sin ` x ) ) e. ( ( 0 (,) pi ) -cn-> CC ) )
93		ioossicc 11373	. . . . . . 7 |- ( 0 (,) pi ) C_ ( 0 [,] pi )
94	93	a1i 11	. . . . . 6 |- ( ph -> ( 0 (,) pi ) C_ ( 0 [,] pi ) )
95		ioombl 20892	. . . . . . 7 |- ( 0 (,) pi ) e. dom vol
96	95	a1i 11	. . . . . 6 |- ( ph -> ( 0 (,) pi ) e. dom vol )
97	22, 18	mulcld 9398	. . . . . 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 5773	. . . . . . . . . . 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 656	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( I ` x ) = ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) )
101	100	eqcomd 2442	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) = ( I ` x ) )
102	101	mpteq2dva 4370	. . . . . . . 8 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) ) = ( x e. ( 0 [,] pi ) |-> ( I ` x ) ) )
103		nfmpt1 4373	. . . . . . . . . 10 |- F/_ x ( x e. CC |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) )
104	98, 103	nfcxfr 2570	. . . . . . . . 9 |- F/_ x I
105		sinf 13395	. . . . . . . . . . . . . 14 |- sin : CC --> CC
106	105	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> sin : CC --> CC )
107	106	feqmptd 5736	. . . . . . . . . . . 12 |- ( ph -> sin = ( x e. CC |-> ( sin ` x ) ) )
108	107, 31	syl6eqelr 2526	. . . . . . . . . . 11 |- ( ph -> ( x e. CC |-> ( sin ` x ) ) e. ( CC -cn-> CC ) )
109	33, 108	mulcncf 20777	. . . . . . . . . 10 |- ( ph -> ( x e. CC |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) ) e. ( CC -cn-> CC ) )
110	98, 109	syl5eqel 2521	. . . . . . . . 9 |- ( ph -> I e. ( CC -cn-> CC ) )
111	104, 110, 35	cncfmptss 29617	. . . . . . . 8 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( I ` x ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
112	102, 111	eqeltrd 2511	. . . . . . 7 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
113		cniccibl 21164	. . . . . . 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 1213	. . . . . 6 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) ) e. L^1 )
115	94, 96, 97, 114	iblss 21128	. . . . 5 |- ( ph -> ( x e. ( 0 (,) pi ) |-> ( ( ( sin ` x ) ^ N ) x. ( sin ` x ) ) ) e. L^1 )
116	58	adantr 462	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> N e. CC )
117	63	adantr 462	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( N - 1 ) e. NN0 )
118	18, 117	expcld 11996	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( sin ` x ) ^ ( N - 1 ) ) e. CC )
119	116, 118	mulcld 9398	. . . . . . . 8 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) e. CC )
120	38	adantl 463	. . . . . . . 8 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( cos ` x ) e. CC )
121	119, 120	mulcld 9398	. . . . . . 7 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) e. CC )
122	39	adantl 463	. . . . . . 7 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> -u ( cos ` x ) e. CC )
123	121, 122	mulcld 9398	. . . . . 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 5773	. . . . . . . . . . 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 656	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( L ` x ) = ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) )
127	126	eqcomd 2442	. . . . . . . . 9 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) = ( L ` x ) )
128	127	mpteq2dva 4370	. . . . . . . 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 4373	. . . . . . . . . 10 |- F/_ x ( x e. CC |-> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) )
130	124, 129	nfcxfr 2570	. . . . . . . . 9 |- F/_ x L
131		eqid 2437	. . . . . . . . . . . . 13 |- ( x e. CC |-> -u ( cos ` x ) ) = ( x e. CC |-> -u ( cos ` x ) )
132	131	negfcncf 20341	. . . . . . . . . . . 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 20777	. . . . . . . . . 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 2521	. . . . . . . . 9 |- ( ph -> L e. ( CC -cn-> CC ) )
136	130, 135, 35	cncfmptss 29617	. . . . . . . 8 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( L ` x ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
137	128, 136	eqeltrd 2511	. . . . . . 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 21164	. . . . . . 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 1213	. . . . . 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 21128	. . . . 5 |- ( ph -> ( x e. ( 0 (,) pi ) |-> ( ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) ) e. L^1 )
141		reelprrecn 9366	. . . . . . 7 |- RR e. { RR , CC }
142	141	a1i 11	. . . . . 6 |- ( ph -> RR e. { RR , CC } )
143		recn 9364	. . . . . . . . 9 |- ( x e. RR -> x e. CC )
144	143	sincld 13401	. . . . . . . 8 |- ( x e. RR -> ( sin ` x ) e. CC )
145	144	adantl 463	. . . . . . 7 |- ( ( ph /\ x e. RR ) -> ( sin ` x ) e. CC )
146	20	adantr 462	. . . . . . 7 |- ( ( ph /\ x e. RR ) -> N e. NN0 )
147	145, 146	expcld 11996	. . . . . 6 |- ( ( ph /\ x e. RR ) -> ( ( sin ` x ) ^ N ) e. CC )
148	58	adantr 462	. . . . . . . 8 |- ( ( ph /\ x e. RR ) -> N e. CC )
149	63	adantr 462	. . . . . . . . 9 |- ( ( ph /\ x e. RR ) -> ( N - 1 ) e. NN0 )
150	145, 149	expcld 11996	. . . . . . . 8 |- ( ( ph /\ x e. RR ) -> ( ( sin ` x ) ^ ( N - 1 ) ) e. CC )
151	148, 150	mulcld 9398	. . . . . . 7 |- ( ( ph /\ x e. RR ) -> ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) e. CC )
152	143	coscld 13402	. . . . . . . 8 |- ( x e. RR -> ( cos ` x ) e. CC )
153	152	adantl 463	. . . . . . 7 |- ( ( ph /\ x e. RR ) -> ( cos ` x ) e. CC )
154	151, 153	mulcld 9398	. . . . . 6 |- ( ( ph /\ x e. RR ) -> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) e. CC )
155		sincl 13397	. . . . . . . . . . 11 |- ( x e. CC -> ( sin ` x ) e. CC )
156	155	adantl 463	. . . . . . . . . 10 |- ( ( ph /\ x e. CC ) -> ( sin ` x ) e. CC )
157	20	adantr 462	. . . . . . . . . 10 |- ( ( ph /\ x e. CC ) -> N e. NN0 )
158	156, 157	expcld 11996	. . . . . . . . 9 |- ( ( ph /\ x e. CC ) -> ( ( sin ` x ) ^ N ) e. CC )
159	158, 23	fmptd 5859	. . . . . . . 8 |- ( ph -> F : CC --> CC )
160	143	adantl 463	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. RR ) -> x e. CC )
161		elex 2975	. . . . . . . . . . . . . . 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 2891	. . . . . . . . . . . . . 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 659	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. RR ) -> x e. { x e. CC | ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) e. _V } )
165	70	dmmpt 5325	. . . . . . . . . . . . 13 |- dom H = { x e. CC | ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) e. _V }
166	164, 165	syl6eleqr 2528	. . . . . . . . . . . 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 1686	. . . . . . . . . 10 |- ( ph -> A. x ( x e. RR -> x e. dom H ) )
169		nfcv 2573	. . . . . . . . . . 11 |- F/_ x RR
170	76	nfdm 5072	. . . . . . . . . . 11 |- F/_ x dom H
171	169, 170	dfss2f 3339	. . . . . . . . . 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 29637	. . . . . . . . . . 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 6095	. . . . . . . . . . 11 |- ( CC _D F ) = ( CC _D ( x e. CC |-> ( ( sin ` x ) ^ N ) ) )
175	173, 174, 70	3eqtr4g 2494	. . . . . . . . . 10 |- ( ph -> ( CC _D F ) = H )
176	175	dmeqd 5033	. . . . . . . . 9 |- ( ph -> dom ( CC _D F ) = dom H )
177	172, 176	sseqtr4d 3385	. . . . . . . 8 |- ( ph -> RR C_ dom ( CC _D F ) )
178		dvres3 21234	. . . . . . . 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 1214	. . . . . . 7 |- ( ph -> ( RR _D ( F |` RR ) ) = ( ( CC _D F ) |` RR ) )
180	23	reseq1i 5097	. . . . . . . . . 10 |- ( F |` RR ) = ( ( x e. CC |-> ( ( sin ` x ) ^ N ) ) |` RR )
181		resmpt 5148	. . . . . . . . . . 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 2457	. . . . . . . . 9 |- ( F |` RR ) = ( x e. RR |-> ( ( sin ` x ) ^ N ) )
184	183	oveq2i 6095	. . . . . . . 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 5100	. . . . . . . 8 |- ( ph -> ( ( CC _D F ) |` RR ) = ( H |` RR ) )
187	70	reseq1i 5097	. . . . . . . . 9 |- ( H |` RR ) = ( ( x e. CC |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) |` RR )
188		resmpt 5148	. . . . . . . . . 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 2457	. . . . . . . 8 |- ( H |` RR ) = ( x e. RR |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) )
191	186, 190	syl6eq 2485	. . . . . . 7 |- ( ph -> ( ( CC _D F ) |` RR ) = ( x e. RR |-> ( ( N x. ( ( sin ` x ) ^ ( N - 1 ) ) ) x. ( cos ` x ) ) ) )
192	179, 185, 191	3eqtr3d 2477	. . . . . 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 2437	. . . . . . 7 |- ( TopOpen ` ℂfld ) = ( TopOpen ` ℂfld )
195	194	tgioo2 20226	. . . . . 6 |- ( topGen ` ran (,) ) = ( ( TopOpen ` ℂfld ) ↾t RR )
196	10	a1i 11	. . . . . . 7 |- ( ph -> ( 0 e. RR /\ pi e. RR ) )
197		iccntr 20244	. . . . . . 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 21282	. . . . 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 9698	. . . . . . 7 |- ( x e. RR -> -u ( cos ` x ) e. CC )
201	200	adantl 463	. . . . . 6 |- ( ( ph /\ x e. RR ) -> -u ( cos ` x ) e. CC )
202	144	negcld 9698	. . . . . . . . 9 |- ( x e. RR -> -u ( sin ` x ) e. CC )
203	202	adantl 463	. . . . . . . 8 |- ( ( ph /\ x e. RR ) -> -u ( sin ` x ) e. CC )
204		dvcosre 29638	. . . . . . . . 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 21286	. . . . . . 7 |- ( ph -> ( RR _D ( x e. RR |-> -u ( cos ` x ) ) ) = ( x e. RR |-> -u -u ( sin ` x ) ) )
207	144	negnegd 9702	. . . . . . . . 9 |- ( x e. RR -> -u -u ( sin ` x ) = ( sin ` x ) )
208	207	adantl 463	. . . . . . . 8 |- ( ( ph /\ x e. RR ) -> -u -u ( sin ` x ) = ( sin ` x ) )
209	208	mpteq2dva 4370	. . . . . . 7 |- ( ph -> ( x e. RR |-> -u -u ( sin ` x ) ) = ( x e. RR |-> ( sin ` x ) ) )
210	206, 209	eqtrd 2469	. . . . . 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 21282	. . . . 5 |- ( ph -> ( RR _D ( x e. ( 0 [,] pi ) |-> -u ( cos ` x ) ) ) = ( x e. ( 0 (,) pi ) |-> ( sin ` x ) ) )
212		fveq2 5683	. . . . . . . . . . 11 |- ( x = 0 -> ( sin ` x ) = ( sin ` 0 ) )
213		sin0 13420	. . . . . . . . . . 11 |- ( sin ` 0 ) = 0
214	212, 213	syl6eq 2485	. . . . . . . . . 10 |- ( x = 0 -> ( sin ` x ) = 0 )
215	214	oveq1d 6099	. . . . . . . . 9 |- ( x = 0 -> ( ( sin ` x ) ^ N ) = ( 0 ^ N ) )
216	215	adantl 463	. . . . . . . 8 |- ( ( ph /\ x = 0 ) -> ( ( sin ` x ) ^ N ) = ( 0 ^ N ) )
217	19	adantr 462	. . . . . . . . 9 |- ( ( ph /\ x = 0 ) -> N e. NN )
218	217	0expd 12012	. . . . . . . 8 |- ( ( ph /\ x = 0 ) -> ( 0 ^ N ) = 0 )
219	216, 218	eqtrd 2469	. . . . . . 7 |- ( ( ph /\ x = 0 ) -> ( ( sin ` x ) ^ N ) = 0 )
220	219	oveq1d 6099	. . . . . 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 9370	. . . . . . . . . 10 |- 0 e. CC
223	221, 222	syl6eqel 2525	. . . . . . . . 9 |- ( x = 0 -> x e. CC )
224		coscl 13398	. . . . . . . . . 10 |- ( x e. CC -> ( cos ` x ) e. CC )
225	224	negcld 9698	. . . . . . . . 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 463	. . . . . . 7 |- ( ( ph /\ x = 0 ) -> -u ( cos ` x ) e. CC )
228	227	mul02d 9559	. . . . . 6 |- ( ( ph /\ x = 0 ) -> ( 0 x. -u ( cos ` x ) ) = 0 )
229	220, 228	eqtrd 2469	. . . . 5 |- ( ( ph /\ x = 0 ) -> ( ( ( sin ` x ) ^ N ) x. -u ( cos ` x ) ) = 0 )
230		fveq2 5683	. . . . . . . . . . 11 |- ( x = pi -> ( sin ` x ) = ( sin ` pi ) )
231		sinpi 21809	. . . . . . . . . . 11 |- ( sin ` pi ) = 0
232	230, 231	syl6eq 2485	. . . . . . . . . 10 |- ( x = pi -> ( sin ` x ) = 0 )
233	232	oveq1d 6099	. . . . . . . . 9 |- ( x = pi -> ( ( sin ` x ) ^ N ) = ( 0 ^ N ) )
234	233	adantl 463	. . . . . . . 8 |- ( ( ph /\ x = pi ) -> ( ( sin ` x ) ^ N ) = ( 0 ^ N ) )
235	19	adantr 462	. . . . . . . . 9 |- ( ( ph /\ x = pi ) -> N e. NN )
236	235	0expd 12012	. . . . . . . 8 |- ( ( ph /\ x = pi ) -> ( 0 ^ N ) = 0 )
237	234, 236	eqtrd 2469	. . . . . . 7 |- ( ( ph /\ x = pi ) -> ( ( sin ` x ) ^ N ) = 0 )
238	237	oveq1d 6099	. . . . . 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 9390	. . . . . . . . . . 11 |- pi e. CC
241	239, 240	syl6eqel 2525	. . . . . . . . . 10 |- ( x = pi -> x e. CC )
242	241	coscld 13402	. . . . . . . . 9 |- ( x = pi -> ( cos ` x ) e. CC )
243	242	negcld 9698	. . . . . . . 8 |- ( x = pi -> -u ( cos ` x ) e. CC )
244	243	adantl 463	. . . . . . 7 |- ( ( ph /\ x = pi ) -> -u ( cos ` x ) e. CC )
245	244	mul02d 9559	. . . . . 6 |- ( ( ph /\ x = pi ) -> ( 0 x. -u ( cos ` x ) ) = 0 )
246	238, 245	eqtrd 2469	. . . . 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 21365	. . . 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 9590	. . . . 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 2495	. . 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 9401	. . . . . . . . 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 11913	. . . . . . . . . . . . . 14 |- ( ( cos ` x ) e. CC -> ( ( cos ` x ) ^ 2 ) = ( ( cos ` x ) x. ( cos ` x ) ) )
253	252	eqcomd 2442	. . . . . . . . . . . . 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 463	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( cos ` x ) x. ( cos ` x ) ) = ( ( cos ` x ) ^ 2 ) )
256	255	oveq2d 6100	. . . . . . . . . 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 11994	. . . . . . . . . . . 12 |- ( x e. ( 0 (,) pi ) -> ( ( cos ` x ) ^ 2 ) e. CC )
258	257	adantl 463	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( cos ` x ) ^ 2 ) e. CC )
259	59, 65, 258	mulassd 9401	. . . . . . . . . 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 2469	. . . . . . . . 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 9399	. . . . . . . . . 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 6100	. . . . . . . . 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 2473	. . . . . . . 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 9596	. . . . . . 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 9790	. . . . . . 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 9398	. . . . . . . 8 |- ( ( ph /\ x e. ( 0 (,) pi ) ) -> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) e. CC )
267	59, 266	mulneg1d 9789	. . . . . . 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 2479	. . . . . 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 21105	. . . . 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 9698	. . . . . 6 |- ( ph -> -u N e. CC )
271	38	sqcld 11994	. . . . . . . . 9 |- ( x e. ( 0 [,] pi ) -> ( ( cos ` x ) ^ 2 ) e. CC )
272	271	adantl 463	. . . . . . . 8 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( cos ` x ) ^ 2 ) e. CC )
273	272, 118	mulcld 9398	. . . . . . 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 5773	. . . . . . . . . . . 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 656	. . . . . . . . . . 11 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( M ` x ) = ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) )
277	276	eqcomd 2442	. . . . . . . . . 10 |- ( ( ph /\ x e. ( 0 [,] pi ) ) -> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) = ( M ` x ) )
278	277	mpteq2dva 4370	. . . . . . . . 9 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) = ( x e. ( 0 [,] pi ) |-> ( M ` x ) ) )
279		nfmpt1 4373	. . . . . . . . . . 11 |- F/_ x ( x e. CC |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) )
280	274, 279	nfcxfr 2570	. . . . . . . . . 10 |- F/_ x M
281		nfcv 2573	. . . . . . . . . . . . 13 |- F/_ x cos
282		2nn0 10588	. . . . . . . . . . . . . 14 |- 2 e. NN0
283	282	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> 2 e. NN0 )
284	281, 49, 283	expcnfg 29623	. . . . . . . . . . . 12 |- ( ph -> ( x e. CC |-> ( ( cos ` x ) ^ 2 ) ) e. ( CC -cn-> CC ) )
285	284, 81	mulcncf 20777	. . . . . . . . . . 11 |- ( ph -> ( x e. CC |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) e. ( CC -cn-> CC ) )
286	274, 285	syl5eqel 2521	. . . . . . . . . 10 |- ( ph -> M e. ( CC -cn-> CC ) )
287	280, 286, 35	cncfmptss 29617	. . . . . . . . 9 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( M ` x ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
288	278, 287	eqeltrd 2511	. . . . . . . 8 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) e. ( ( 0 [,] pi ) -cn-> CC ) )
289		cniccibl 21164	. . . . . . . 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 1213	. . . . . . 7 |- ( ph -> ( x e. ( 0 [,] pi ) |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) e. L^1 )
291	94, 96, 273, 290	iblss 21128	. . . . . 6 |- ( ph -> ( x e. ( 0 (,) pi ) |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) ) e. L^1 )
292	270, 266, 291	itgmulc2 21157	. . . . 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 2472	. . . 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 9596	. . 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 2469	. 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 21107	. . . 4 |- ( ph -> S. ( 0 (,) pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) _d x e. CC )
297	58, 296	mulneg1d 9789	. . 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 9596	. 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 9398	. . 3 |- ( ph -> ( N x. S. ( 0 (,) pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 1 ) ) ) _d x ) e. CC )
300	299	negnegd 9702	. 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 2473	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 1362   = wceq 1364   e. wcel 1757   {crab 2713   _Vcvv 2966   C_ wss 3320   {cpr 3871   class class class wbr 4284   e. cmpt 4342   dom cdm 4831   ran crn 4832   |` cres 4833   -->wf 5406   ` cfv 5410  (class class class)co 6084   CCcc 9272   RRcr 9273   0cc0 9274   1c1 9275   x. cmul 9279   <_ cle 9411   - cmin 9587   -ucneg 9588   NNcn 10314   2c2 10363   NN0cn0 10571   (,)cioo 11292   [,]cicc 11295   ^cexp 11853   sincsin 13336   cosccos 13337   picpi 13339   TopOpenctopn 14347   topGenctg 14363  ℂ_fldccnfld 17666   intcnt 18467   -cn->ccncf 20298   volcvol 20793   L^1cibl 20943   S.citg 20944   _D cdv 21184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2418  ax-rep 4395  ax-sep 4405  ax-nul 4413  ax-pow 4462  ax-pr 4523  ax-un 6365  ax-inf2 7839  ax-cc 8596  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351  ax-pre-sup 9352  ax-addf 9353  ax-mulf 9354

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-fal 1370  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2714  df-rex 2715  df-reu 2716  df-rmo 2717  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3281  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-pss 3336  df-nul 3630  df-if 3784  df-pw 3854  df-sn 3870  df-pr 3872  df-tp 3874  df-op 3876  df-uni 4084  df-int 4121  df-iun 4165  df-iin 4166  df-disj 4255  df-br 4285  df-opab 4343  df-mpt 4344  df-tr 4378  df-eprel 4623  df-id 4627  df-po 4632  df-so 4633  df-fr 4670  df-se 4671  df-we 4672  df-ord 4713  df-on 4714  df-lim 4715  df-suc 4716  df-xp 4837  df-rel 4838  df-cnv 4839  df-co 4840  df-dm 4841  df-rn 4842  df-res 4843  df-ima 4844  df-iota 5373  df-fun 5412  df-fn 5413  df-f 5414  df-f1 5415  df-fo 5416  df-f1o 5417  df-fv 5418  df-isom 5419  df-riota 6043  df-ov 6087  df-oprab 6088  df-mpt2 6089  df-of 6313  df-ofr 6314  df-om 6470  df-1st 6570  df-2nd 6571  df-supp 6684  df-recs 6822  df-rdg 6856  df-1o 6912  df-2o 6913  df-oadd 6916  df-omul 6917  df-er 7093  df-map 7208  df-pm 7209  df-ixp 7256  df-en 7303  df-dom 7304  df-sdom 7305  df-fin 7306  df-fsupp 7613  df-fi 7653  df-sup 7683  df-oi 7716  df-card 8101  df-acn 8104  df-cda 8329  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-div 9986  df-nn 10315  df-2 10372  df-3 10373  df-4 10374  df-5 10375  df-6 10376  df-7 10377  df-8 10378  df-9 10379  df-10 10380  df-n0 10572  df-z 10639  df-dec 10748  df-uz 10854  df-q 10946  df-rp 10984  df-xneg 11081  df-xadd 11082  df-xmul 11083  df-ioo 11296  df-ioc 11297  df-ico 11298  df-icc 11299  df-fz 11429  df-fzo 11537  df-fl 11630  df-mod 11697  df-seq 11795  df-exp 11854  df-fac 12040  df-bc 12067  df-hash 12092  df-shft 12544  df-cj 12576  df-re 12577  df-im 12578  df-sqr 12712  df-abs 12713  df-limsup 12937  df-clim 12954  df-rlim 12955  df-sum 13152  df-ef 13340  df-sin 13342  df-cos 13343  df-pi 13345  df-struct 14163  df-ndx 14164  df-slot 14165  df-base 14166  df-sets 14167  df-ress 14168  df-plusg 14238  df-mulr 14239  df-starv 14240  df-sca 14241  df-vsca 14242  df-ip 14243  df-tset 14244  df-ple 14245  df-ds 14247  df-unif 14248  df-hom 14249  df-cco 14250  df-rest 14348  df-topn 14349  df-0g 14367  df-gsum 14368  df-topgen 14369  df-pt 14370  df-prds 14373  df-xrs 14427  df-qtop 14432  df-imas 14433  df-xps 14435  df-mre 14511  df-mrc 14512  df-acs 14514  df-mnd 15402  df-submnd 15452  df-mulg 15532  df-cntz 15819  df-cmn 16263  df-psmet 17657  df-xmet 17658  df-met 17659  df-bl 17660  df-mopn 17661  df-fbas 17662  df-fg 17663  df-cnfld 17667  df-top 18349  df-bases 18351  df-topon 18352  df-topsp 18353  df-cld 18469  df-ntr 18470  df-cls 18471  df-nei 18548  df-lp 18586  df-perf 18587  df-cn 18677  df-cnp 18678  df-haus 18765  df-cmp 18836  df-tx 18981  df-hmeo 19174  df-fil 19265  df-fm 19357  df-flim 19358  df-flf 19359  df-xms 19741  df-ms 19742  df-tms 19743  df-cncf 20300  df-ovol 20794  df-vol 20795  df-mbf 20945  df-itg1 20946  df-itg2 20947  df-ibl 20948  df-itg 20949  df-0p 20994  df-limc 21187  df-dv 21188

This theorem is referenced by:  itgsinexp  29645