Metamath Proof Explorer

Theorem itgsinexp

Description: A recursive formula for the integral of sin^N on the interval (0,π) . (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses itgsinexp.1 
|- I = ( n e. NN0 |-> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ n ) _d x )
itgsinexp.2 
|- ( ph -> N e. ( ZZ>= ` 2 ) )
Assertion itgsinexp 
|- ( ph -> ( I ` N ) = ( ( ( N - 1 ) / N ) x. ( I ` ( N - 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 itgsinexp.1 
 |-  I = ( n e. NN0 |-> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ n ) _d x )
2 itgsinexp.2 
 |-  ( ph -> N e. ( ZZ>= ` 2 ) )
3 eluzelz 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. ZZ )
4 zcn 
 |-  ( N e. ZZ -> N e. CC )
5 2 3 4 3syl 
 |-  ( ph -> N e. CC )
6 1cnd 
 |-  ( ph -> 1 e. CC )
7 5 6 npcand 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
8 7 eqcomd 
 |-  ( ph -> N = ( ( N - 1 ) + 1 ) )
9 8 oveq1d 
 |-  ( ph -> ( N x. ( I ` N ) ) = ( ( ( N - 1 ) + 1 ) x. ( I ` N ) ) )
10 uz2m1nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) e. NN )
11 2 10 syl 
 |-  ( ph -> ( N - 1 ) e. NN )
12 11 nncnd 
 |-  ( ph -> ( N - 1 ) e. CC )
13 1 a1i 
 |-  ( ph -> I = ( n e. NN0 |-> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ n ) _d x ) )
14 oveq2 
 |-  ( n = N -> ( ( sin ` x ) ^ n ) = ( ( sin ` x ) ^ N ) )
15 14 ad2antlr 
 |-  ( ( ( ph /\ n = N ) /\ x e. ( 0 (,) _pi ) ) -> ( ( sin ` x ) ^ n ) = ( ( sin ` x ) ^ N ) )
16 15 itgeq2dv 
 |-  ( ( ph /\ n = N ) -> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ n ) _d x = S. ( 0 (,) _pi ) ( ( sin ` x ) ^ N ) _d x )
17 2cnd 
 |-  ( ph -> 2 e. CC )
18 npcan 
 |-  ( ( N e. CC /\ 2 e. CC ) -> ( ( N - 2 ) + 2 ) = N )
19 18 eqcomd 
 |-  ( ( N e. CC /\ 2 e. CC ) -> N = ( ( N - 2 ) + 2 ) )
20 5 17 19 syl2anc 
 |-  ( ph -> N = ( ( N - 2 ) + 2 ) )
21 uznn0sub 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 2 ) e. NN0 )
22 2 21 syl 
 |-  ( ph -> ( N - 2 ) e. NN0 )
23 2nn0 
 |-  2 e. NN0
24 23 a1i 
 |-  ( ph -> 2 e. NN0 )
25 22 24 nn0addcld 
 |-  ( ph -> ( ( N - 2 ) + 2 ) e. NN0 )
26 20 25 eqeltrd 
 |-  ( ph -> N e. NN0 )
27 itgex 
 |-  S. ( 0 (,) _pi ) ( ( sin ` x ) ^ N ) _d x e. _V
28 27 a1i 
 |-  ( ph -> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ N ) _d x e. _V )
29 13 16 26 28 fvmptd 
 |-  ( ph -> ( I ` N ) = S. ( 0 (,) _pi ) ( ( sin ` x ) ^ N ) _d x )
30 ioosscn 
 |-  ( 0 (,) _pi ) C_ CC
31 30 sseli 
 |-  ( x e. ( 0 (,) _pi ) -> x e. CC )
32 31 sincld 
 |-  ( x e. ( 0 (,) _pi ) -> ( sin ` x ) e. CC )
33 32 adantl 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( sin ` x ) e. CC )
34 26 adantr 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> N e. NN0 )
35 33 34 expcld 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( sin ` x ) ^ N ) e. CC )
36 ioossicc 
 |-  ( 0 (,) _pi ) C_ ( 0 [,] _pi )
37 36 a1i 
 |-  ( ph -> ( 0 (,) _pi ) C_ ( 0 [,] _pi ) )
38 ioombl 
 |-  ( 0 (,) _pi ) e. dom vol
39 38 a1i 
 |-  ( ph -> ( 0 (,) _pi ) e. dom vol )
40 0re 
 |-  0 e. RR
41 pire 
 |-  _pi e. RR
42 iccssre 
 |-  ( ( 0 e. RR /\ _pi e. RR ) -> ( 0 [,] _pi ) C_ RR )
43 40 41 42 mp2an 
 |-  ( 0 [,] _pi ) C_ RR
44 ax-resscn 
 |-  RR C_ CC
45 43 44 sstri 
 |-  ( 0 [,] _pi ) C_ CC
46 45 sseli 
 |-  ( x e. ( 0 [,] _pi ) -> x e. CC )
47 46 sincld 
 |-  ( x e. ( 0 [,] _pi ) -> ( sin ` x ) e. CC )
48 47 adantl 
 |-  ( ( ph /\ x e. ( 0 [,] _pi ) ) -> ( sin ` x ) e. CC )
49 26 adantr 
 |-  ( ( ph /\ x e. ( 0 [,] _pi ) ) -> N e. NN0 )
50 48 49 expcld 
 |-  ( ( ph /\ x e. ( 0 [,] _pi ) ) -> ( ( sin ` x ) ^ N ) e. CC )
51 40 a1i 
 |-  ( ph -> 0 e. RR )
52 41 a1i 
 |-  ( ph -> _pi e. RR )
53 46 adantl 
 |-  ( ( ph /\ x e. ( 0 [,] _pi ) ) -> x e. CC )
54 eqid 
 |-  ( x e. CC |-> ( ( sin ` x ) ^ N ) ) = ( x e. CC |-> ( ( sin ` x ) ^ N ) )
55 54 fvmpt2 
 |-  ( ( x e. CC /\ ( ( sin ` x ) ^ N ) e. CC ) -> ( ( x e. CC |-> ( ( sin ` x ) ^ N ) ) ` x ) = ( ( sin ` x ) ^ N ) )
56 53 50 55 syl2anc 
 |-  ( ( ph /\ x e. ( 0 [,] _pi ) ) -> ( ( x e. CC |-> ( ( sin ` x ) ^ N ) ) ` x ) = ( ( sin ` x ) ^ N ) )
57 56 eqcomd 
 |-  ( ( ph /\ x e. ( 0 [,] _pi ) ) -> ( ( sin ` x ) ^ N ) = ( ( x e. CC |-> ( ( sin ` x ) ^ N ) ) ` x ) )
58 57 mpteq2dva 
 |-  ( ph -> ( x e. ( 0 [,] _pi ) |-> ( ( sin ` x ) ^ N ) ) = ( x e. ( 0 [,] _pi ) |-> ( ( x e. CC |-> ( ( sin ` x ) ^ N ) ) ` x ) ) )
59 nfmpt1 
 |-  F/_ x ( x e. CC |-> ( ( sin ` x ) ^ N ) )
60 nfcv 
 |-  F/_ x sin
61 sincn 
 |-  sin e. ( CC -cn-> CC )
62 61 a1i 
 |-  ( ph -> sin e. ( CC -cn-> CC ) )
63 60 62 26 expcnfg 
 |-  ( ph -> ( x e. CC |-> ( ( sin ` x ) ^ N ) ) e. ( CC -cn-> CC ) )
64 45 a1i 
 |-  ( ph -> ( 0 [,] _pi ) C_ CC )
65 59 63 64 cncfmptss 
 |-  ( ph -> ( x e. ( 0 [,] _pi ) |-> ( ( x e. CC |-> ( ( sin ` x ) ^ N ) ) ` x ) ) e. ( ( 0 [,] _pi ) -cn-> CC ) )
66 58 65 eqeltrd 
 |-  ( ph -> ( x e. ( 0 [,] _pi ) |-> ( ( sin ` x ) ^ N ) ) e. ( ( 0 [,] _pi ) -cn-> CC ) )
67 cniccibl 
 |-  ( ( 0 e. RR /\ _pi e. RR /\ ( x e. ( 0 [,] _pi ) |-> ( ( sin ` x ) ^ N ) ) e. ( ( 0 [,] _pi ) -cn-> CC ) ) -> ( x e. ( 0 [,] _pi ) |-> ( ( sin ` x ) ^ N ) ) e. L^1 )
68 51 52 66 67 syl3anc 
 |-  ( ph -> ( x e. ( 0 [,] _pi ) |-> ( ( sin ` x ) ^ N ) ) e. L^1 )
69 37 39 50 68 iblss 
 |-  ( ph -> ( x e. ( 0 (,) _pi ) |-> ( ( sin ` x ) ^ N ) ) e. L^1 )
70 35 69 itgcl 
 |-  ( ph -> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ N ) _d x e. CC )
71 29 70 eqeltrd 
 |-  ( ph -> ( I ` N ) e. CC )
72 12 71 adddirp1d 
 |-  ( ph -> ( ( ( N - 1 ) + 1 ) x. ( I ` N ) ) = ( ( ( N - 1 ) x. ( I ` N ) ) + ( I ` N ) ) )
73 eluz2b2 
 |-  ( N e. ( ZZ>= ` 2 ) <-> ( N e. NN /\ 1 < N ) )
74 2 73 sylib 
 |-  ( ph -> ( N e. NN /\ 1 < N ) )
75 74 simpld 
 |-  ( ph -> N e. NN )
76 expm1t 
 |-  ( ( ( sin ` x ) e. CC /\ N e. NN ) -> ( ( sin ` x ) ^ N ) = ( ( ( sin ` x ) ^ ( N - 1 ) ) x. ( sin ` x ) ) )
77 32 75 76 syl2anr 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( sin ` x ) ^ N ) = ( ( ( sin ` x ) ^ ( N - 1 ) ) x. ( sin ` x ) ) )
78 77 itgeq2dv 
 |-  ( ph -> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ N ) _d x = S. ( 0 (,) _pi ) ( ( ( sin ` x ) ^ ( N - 1 ) ) x. ( sin ` x ) ) _d x )
79 eqid 
 |-  ( x e. CC |-> ( ( sin ` x ) ^ ( N - 1 ) ) ) = ( x e. CC |-> ( ( sin ` x ) ^ ( N - 1 ) ) )
80 eqid 
 |-  ( x e. CC |-> -u ( cos ` x ) ) = ( x e. CC |-> -u ( cos ` x ) )
81 eqid 
 |-  ( x e. CC |-> ( ( ( N - 1 ) x. ( ( sin ` x ) ^ ( ( N - 1 ) - 1 ) ) ) x. ( cos ` x ) ) ) = ( x e. CC |-> ( ( ( N - 1 ) x. ( ( sin ` x ) ^ ( ( N - 1 ) - 1 ) ) ) x. ( cos ` x ) ) )
82 eqid 
 |-  ( x e. CC |-> ( ( ( sin ` x ) ^ ( N - 1 ) ) x. ( sin ` x ) ) ) = ( x e. CC |-> ( ( ( sin ` x ) ^ ( N - 1 ) ) x. ( sin ` x ) ) )
83 eqid 
 |-  ( x e. CC |-> ( ( ( ( N - 1 ) x. ( ( sin ` x ) ^ ( ( N - 1 ) - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) ) = ( x e. CC |-> ( ( ( ( N - 1 ) x. ( ( sin ` x ) ^ ( ( N - 1 ) - 1 ) ) ) x. ( cos ` x ) ) x. -u ( cos ` x ) ) )
84 eqid 
 |-  ( x e. CC |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( ( N - 1 ) - 1 ) ) ) ) = ( x e. CC |-> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( ( N - 1 ) - 1 ) ) ) )
85 79 80 81 82 83 84 11 itgsinexplem1 
 |-  ( ph -> S. ( 0 (,) _pi ) ( ( ( sin ` x ) ^ ( N - 1 ) ) x. ( sin ` x ) ) _d x = ( ( N - 1 ) x. S. ( 0 (,) _pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( ( N - 1 ) - 1 ) ) ) _d x ) )
86 5 6 6 subsub4d 
 |-  ( ph -> ( ( N - 1 ) - 1 ) = ( N - ( 1 + 1 ) ) )
87 1p1e2 
 |-  ( 1 + 1 ) = 2
88 87 a1i 
 |-  ( ph -> ( 1 + 1 ) = 2 )
89 88 oveq2d 
 |-  ( ph -> ( N - ( 1 + 1 ) ) = ( N - 2 ) )
90 86 89 eqtrd 
 |-  ( ph -> ( ( N - 1 ) - 1 ) = ( N - 2 ) )
91 90 adantr 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( N - 1 ) - 1 ) = ( N - 2 ) )
92 91 oveq2d 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( sin ` x ) ^ ( ( N - 1 ) - 1 ) ) = ( ( sin ` x ) ^ ( N - 2 ) ) )
93 92 oveq2d 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( ( N - 1 ) - 1 ) ) ) = ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 2 ) ) ) )
94 93 itgeq2dv 
 |-  ( ph -> S. ( 0 (,) _pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( ( N - 1 ) - 1 ) ) ) _d x = S. ( 0 (,) _pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 2 ) ) ) _d x )
95 94 oveq2d 
 |-  ( ph -> ( ( N - 1 ) x. S. ( 0 (,) _pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( ( N - 1 ) - 1 ) ) ) _d x ) = ( ( N - 1 ) x. S. ( 0 (,) _pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 2 ) ) ) _d x ) )
96 sincossq 
 |-  ( x e. CC -> ( ( ( sin ` x ) ^ 2 ) + ( ( cos ` x ) ^ 2 ) ) = 1 )
97 1cnd 
 |-  ( x e. CC -> 1 e. CC )
98 sincl 
 |-  ( x e. CC -> ( sin ` x ) e. CC )
99 98 sqcld 
 |-  ( x e. CC -> ( ( sin ` x ) ^ 2 ) e. CC )
100 coscl 
 |-  ( x e. CC -> ( cos ` x ) e. CC )
101 100 sqcld 
 |-  ( x e. CC -> ( ( cos ` x ) ^ 2 ) e. CC )
102 97 99 101 subaddd 
 |-  ( x e. CC -> ( ( 1 - ( ( sin ` x ) ^ 2 ) ) = ( ( cos ` x ) ^ 2 ) <-> ( ( ( sin ` x ) ^ 2 ) + ( ( cos ` x ) ^ 2 ) ) = 1 ) )
103 96 102 mpbird 
 |-  ( x e. CC -> ( 1 - ( ( sin ` x ) ^ 2 ) ) = ( ( cos ` x ) ^ 2 ) )
104 103 eqcomd 
 |-  ( x e. CC -> ( ( cos ` x ) ^ 2 ) = ( 1 - ( ( sin ` x ) ^ 2 ) ) )
105 31 104 syl 
 |-  ( x e. ( 0 (,) _pi ) -> ( ( cos ` x ) ^ 2 ) = ( 1 - ( ( sin ` x ) ^ 2 ) ) )
106 105 oveq1d 
 |-  ( x e. ( 0 (,) _pi ) -> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 2 ) ) ) = ( ( 1 - ( ( sin ` x ) ^ 2 ) ) x. ( ( sin ` x ) ^ ( N - 2 ) ) ) )
107 106 adantl 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 2 ) ) ) = ( ( 1 - ( ( sin ` x ) ^ 2 ) ) x. ( ( sin ` x ) ^ ( N - 2 ) ) ) )
108 107 itgeq2dv 
 |-  ( ph -> S. ( 0 (,) _pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 2 ) ) ) _d x = S. ( 0 (,) _pi ) ( ( 1 - ( ( sin ` x ) ^ 2 ) ) x. ( ( sin ` x ) ^ ( N - 2 ) ) ) _d x )
109 1cnd 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> 1 e. CC )
110 32 sqcld 
 |-  ( x e. ( 0 (,) _pi ) -> ( ( sin ` x ) ^ 2 ) e. CC )
111 110 adantl 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( sin ` x ) ^ 2 ) e. CC )
112 90 eqcomd 
 |-  ( ph -> ( N - 2 ) = ( ( N - 1 ) - 1 ) )
113 nnm1nn0 
 |-  ( ( N - 1 ) e. NN -> ( ( N - 1 ) - 1 ) e. NN0 )
114 11 113 syl 
 |-  ( ph -> ( ( N - 1 ) - 1 ) e. NN0 )
115 112 114 eqeltrd 
 |-  ( ph -> ( N - 2 ) e. NN0 )
116 115 adantr 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( N - 2 ) e. NN0 )
117 33 116 expcld 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( sin ` x ) ^ ( N - 2 ) ) e. CC )
118 109 111 117 subdird 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( 1 - ( ( sin ` x ) ^ 2 ) ) x. ( ( sin ` x ) ^ ( N - 2 ) ) ) = ( ( 1 x. ( ( sin ` x ) ^ ( N - 2 ) ) ) - ( ( ( sin ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 2 ) ) ) ) )
119 117 mullidd 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( 1 x. ( ( sin ` x ) ^ ( N - 2 ) ) ) = ( ( sin ` x ) ^ ( N - 2 ) ) )
120 23 a1i 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> 2 e. NN0 )
121 33 116 120 expaddd 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( sin ` x ) ^ ( 2 + ( N - 2 ) ) ) = ( ( ( sin ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 2 ) ) ) )
122 17 5 pncan3d 
 |-  ( ph -> ( 2 + ( N - 2 ) ) = N )
123 122 oveq2d 
 |-  ( ph -> ( ( sin ` x ) ^ ( 2 + ( N - 2 ) ) ) = ( ( sin ` x ) ^ N ) )
124 123 adantr 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( sin ` x ) ^ ( 2 + ( N - 2 ) ) ) = ( ( sin ` x ) ^ N ) )
125 121 124 eqtr3d 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( ( sin ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 2 ) ) ) = ( ( sin ` x ) ^ N ) )
126 119 125 oveq12d 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( 1 x. ( ( sin ` x ) ^ ( N - 2 ) ) ) - ( ( ( sin ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 2 ) ) ) ) = ( ( ( sin ` x ) ^ ( N - 2 ) ) - ( ( sin ` x ) ^ N ) ) )
127 118 126 eqtrd 
 |-  ( ( ph /\ x e. ( 0 (,) _pi ) ) -> ( ( 1 - ( ( sin ` x ) ^ 2 ) ) x. ( ( sin ` x ) ^ ( N - 2 ) ) ) = ( ( ( sin ` x ) ^ ( N - 2 ) ) - ( ( sin ` x ) ^ N ) ) )
128 127 itgeq2dv 
 |-  ( ph -> S. ( 0 (,) _pi ) ( ( 1 - ( ( sin ` x ) ^ 2 ) ) x. ( ( sin ` x ) ^ ( N - 2 ) ) ) _d x = S. ( 0 (,) _pi ) ( ( ( sin ` x ) ^ ( N - 2 ) ) - ( ( sin ` x ) ^ N ) ) _d x )
129 115 adantr 
 |-  ( ( ph /\ x e. ( 0 [,] _pi ) ) -> ( N - 2 ) e. NN0 )
130 48 129 expcld 
 |-  ( ( ph /\ x e. ( 0 [,] _pi ) ) -> ( ( sin ` x ) ^ ( N - 2 ) ) e. CC )
131 eqid 
 |-  ( x e. CC |-> ( ( sin ` x ) ^ ( N - 2 ) ) ) = ( x e. CC |-> ( ( sin ` x ) ^ ( N - 2 ) ) )
132 131 fvmpt2 
 |-  ( ( x e. CC /\ ( ( sin ` x ) ^ ( N - 2 ) ) e. CC ) -> ( ( x e. CC |-> ( ( sin ` x ) ^ ( N - 2 ) ) ) ` x ) = ( ( sin ` x ) ^ ( N - 2 ) ) )
133 53 130 132 syl2anc 
 |-  ( ( ph /\ x e. ( 0 [,] _pi ) ) -> ( ( x e. CC |-> ( ( sin ` x ) ^ ( N - 2 ) ) ) ` x ) = ( ( sin ` x ) ^ ( N - 2 ) ) )
134 133 eqcomd 
 |-  ( ( ph /\ x e. ( 0 [,] _pi ) ) -> ( ( sin ` x ) ^ ( N - 2 ) ) = ( ( x e. CC |-> ( ( sin ` x ) ^ ( N - 2 ) ) ) ` x ) )
135 134 mpteq2dva 
 |-  ( ph -> ( x e. ( 0 [,] _pi ) |-> ( ( sin ` x ) ^ ( N - 2 ) ) ) = ( x e. ( 0 [,] _pi ) |-> ( ( x e. CC |-> ( ( sin ` x ) ^ ( N - 2 ) ) ) ` x ) ) )
136 nfmpt1 
 |-  F/_ x ( x e. CC |-> ( ( sin ` x ) ^ ( N - 2 ) ) )
137 60 62 115 expcnfg 
 |-  ( ph -> ( x e. CC |-> ( ( sin ` x ) ^ ( N - 2 ) ) ) e. ( CC -cn-> CC ) )
138 136 137 64 cncfmptss 
 |-  ( ph -> ( x e. ( 0 [,] _pi ) |-> ( ( x e. CC |-> ( ( sin ` x ) ^ ( N - 2 ) ) ) ` x ) ) e. ( ( 0 [,] _pi ) -cn-> CC ) )
139 135 138 eqeltrd 
 |-  ( ph -> ( x e. ( 0 [,] _pi ) |-> ( ( sin ` x ) ^ ( N - 2 ) ) ) e. ( ( 0 [,] _pi ) -cn-> CC ) )
140 cniccibl 
 |-  ( ( 0 e. RR /\ _pi e. RR /\ ( x e. ( 0 [,] _pi ) |-> ( ( sin ` x ) ^ ( N - 2 ) ) ) e. ( ( 0 [,] _pi ) -cn-> CC ) ) -> ( x e. ( 0 [,] _pi ) |-> ( ( sin ` x ) ^ ( N - 2 ) ) ) e. L^1 )
141 51 52 139 140 syl3anc 
 |-  ( ph -> ( x e. ( 0 [,] _pi ) |-> ( ( sin ` x ) ^ ( N - 2 ) ) ) e. L^1 )
142 37 39 130 141 iblss 
 |-  ( ph -> ( x e. ( 0 (,) _pi ) |-> ( ( sin ` x ) ^ ( N - 2 ) ) ) e. L^1 )
143 117 142 35 69 itgsub 
 |-  ( ph -> S. ( 0 (,) _pi ) ( ( ( sin ` x ) ^ ( N - 2 ) ) - ( ( sin ` x ) ^ N ) ) _d x = ( S. ( 0 (,) _pi ) ( ( sin ` x ) ^ ( N - 2 ) ) _d x - S. ( 0 (,) _pi ) ( ( sin ` x ) ^ N ) _d x ) )
144 108 128 143 3eqtrd 
 |-  ( ph -> S. ( 0 (,) _pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 2 ) ) ) _d x = ( S. ( 0 (,) _pi ) ( ( sin ` x ) ^ ( N - 2 ) ) _d x - S. ( 0 (,) _pi ) ( ( sin ` x ) ^ N ) _d x ) )
145 144 oveq2d 
 |-  ( ph -> ( ( N - 1 ) x. S. ( 0 (,) _pi ) ( ( ( cos ` x ) ^ 2 ) x. ( ( sin ` x ) ^ ( N - 2 ) ) ) _d x ) = ( ( N - 1 ) x. ( S. ( 0 (,) _pi ) ( ( sin ` x ) ^ ( N - 2 ) ) _d x - S. ( 0 (,) _pi ) ( ( sin ` x ) ^ N ) _d x ) ) )
146 85 95 145 3eqtrd 
 |-  ( ph -> S. ( 0 (,) _pi ) ( ( ( sin ` x ) ^ ( N - 1 ) ) x. ( sin ` x ) ) _d x = ( ( N - 1 ) x. ( S. ( 0 (,) _pi ) ( ( sin ` x ) ^ ( N - 2 ) ) _d x - S. ( 0 (,) _pi ) ( ( sin ` x ) ^ N ) _d x ) ) )
147 29 78 146 3eqtrd 
 |-  ( ph -> ( I ` N ) = ( ( N - 1 ) x. ( S. ( 0 (,) _pi ) ( ( sin ` x ) ^ ( N - 2 ) ) _d x - S. ( 0 (,) _pi ) ( ( sin ` x ) ^ N ) _d x ) ) )
148 oveq2 
 |-  ( n = ( N - 2 ) -> ( ( sin ` x ) ^ n ) = ( ( sin ` x ) ^ ( N - 2 ) ) )
149 148 adantr 
 |-  ( ( n = ( N - 2 ) /\ x e. ( 0 (,) _pi ) ) -> ( ( sin ` x ) ^ n ) = ( ( sin ` x ) ^ ( N - 2 ) ) )
150 149 itgeq2dv 
 |-  ( n = ( N - 2 ) -> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ n ) _d x = S. ( 0 (,) _pi ) ( ( sin ` x ) ^ ( N - 2 ) ) _d x )
151 itgex 
 |-  S. ( 0 (,) _pi ) ( ( sin ` x ) ^ ( N - 2 ) ) _d x e. _V
152 151 a1i 
 |-  ( ph -> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ ( N - 2 ) ) _d x e. _V )
153 1 150 115 152 fvmptd3 
 |-  ( ph -> ( I ` ( N - 2 ) ) = S. ( 0 (,) _pi ) ( ( sin ` x ) ^ ( N - 2 ) ) _d x )
154 153 29 oveq12d 
 |-  ( ph -> ( ( I ` ( N - 2 ) ) - ( I ` N ) ) = ( S. ( 0 (,) _pi ) ( ( sin ` x ) ^ ( N - 2 ) ) _d x - S. ( 0 (,) _pi ) ( ( sin ` x ) ^ N ) _d x ) )
155 154 oveq2d 
 |-  ( ph -> ( ( N - 1 ) x. ( ( I ` ( N - 2 ) ) - ( I ` N ) ) ) = ( ( N - 1 ) x. ( S. ( 0 (,) _pi ) ( ( sin ` x ) ^ ( N - 2 ) ) _d x - S. ( 0 (,) _pi ) ( ( sin ` x ) ^ N ) _d x ) ) )
156 117 142 itgcl 
 |-  ( ph -> S. ( 0 (,) _pi ) ( ( sin ` x ) ^ ( N - 2 ) ) _d x e. CC )
157 153 156 eqeltrd 
 |-  ( ph -> ( I ` ( N - 2 ) ) e. CC )
158 12 157 71 subdid 
 |-  ( ph -> ( ( N - 1 ) x. ( ( I ` ( N - 2 ) ) - ( I ` N ) ) ) = ( ( ( N - 1 ) x. ( I ` ( N - 2 ) ) ) - ( ( N - 1 ) x. ( I ` N ) ) ) )
159 147 155 158 3eqtr2d 
 |-  ( ph -> ( I ` N ) = ( ( ( N - 1 ) x. ( I ` ( N - 2 ) ) ) - ( ( N - 1 ) x. ( I ` N ) ) ) )
160 159 eqcomd 
 |-  ( ph -> ( ( ( N - 1 ) x. ( I ` ( N - 2 ) ) ) - ( ( N - 1 ) x. ( I ` N ) ) ) = ( I ` N ) )
161 12 157 mulcld 
 |-  ( ph -> ( ( N - 1 ) x. ( I ` ( N - 2 ) ) ) e. CC )
162 12 71 mulcld 
 |-  ( ph -> ( ( N - 1 ) x. ( I ` N ) ) e. CC )
163 161 162 71 subaddd 
 |-  ( ph -> ( ( ( ( N - 1 ) x. ( I ` ( N - 2 ) ) ) - ( ( N - 1 ) x. ( I ` N ) ) ) = ( I ` N ) <-> ( ( ( N - 1 ) x. ( I ` N ) ) + ( I ` N ) ) = ( ( N - 1 ) x. ( I ` ( N - 2 ) ) ) ) )
164 160 163 mpbid 
 |-  ( ph -> ( ( ( N - 1 ) x. ( I ` N ) ) + ( I ` N ) ) = ( ( N - 1 ) x. ( I ` ( N - 2 ) ) ) )
165 9 72 164 3eqtrd 
 |-  ( ph -> ( N x. ( I ` N ) ) = ( ( N - 1 ) x. ( I ` ( N - 2 ) ) ) )
166 165 oveq1d 
 |-  ( ph -> ( ( N x. ( I ` N ) ) / N ) = ( ( ( N - 1 ) x. ( I ` ( N - 2 ) ) ) / N ) )
167 75 nnne0d 
 |-  ( ph -> N =/= 0 )
168 71 5 167 divcan3d 
 |-  ( ph -> ( ( N x. ( I ` N ) ) / N ) = ( I ` N ) )
169 12 157 5 167 div23d 
 |-  ( ph -> ( ( ( N - 1 ) x. ( I ` ( N - 2 ) ) ) / N ) = ( ( ( N - 1 ) / N ) x. ( I ` ( N - 2 ) ) ) )
170 166 168 169 3eqtr3d 
 |-  ( ph -> ( I ` N ) = ( ( ( N - 1 ) / N ) x. ( I ` ( N - 2 ) ) ) )