This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itgsinexplem1

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

Ref Expression
Hypotheses itgsinexplem1.1 
|- F = ( x 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 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 ) )

Proof

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