let n be Nat; :: thesis: ( n >= 2 implies ((n -' 1) / n) * ('I' . (n -' 2)) = 'I' . n )
assume A1: n >= 2 ; :: thesis: ((n -' 1) / n) * ('I' . (n -' 2)) = 'I' . n
then A2: 1 < n by XXREAL_0:2;
reconsider n0 = n as Element of NAT by ORDINAL1:def 12;
reconsider n1 = n -' 1 as Nat ;
A3: n1 = n - 1 by A1, XXREAL_0:2, XREAL_1:233;
then A4: @ ((@ sin) |^ n) = (@ sin) |^ (n1 + 1)
.= ((@ sin) |^ n1) * (@ sin) by Th20
.= (@ ((@ sin) |^ (n -' 1))) (#) (@ (@ sin)) by Th13 ;
A5: n1 > 0 by XREAL_1:50, A2, A3;
reconsider n1 = n1 as non zero Nat by A1, A3;
reconsider g = ((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))) (#) (@ (@ cos)) as Function of REAL,REAL ;
reconsider G = @ ((@ sin) |^ (n -' 1)) as Function of REAL,REAL ;
reconsider f = @ (@ sin) as Function of REAL,REAL ;
reconsider F = @ (@ (- cos)) as Function of REAL,REAL ;
A6: REAL c= dom sin by FUNCT_2:def 1;
A7: sin | REAL is continuous ;
A9: dom g = REAL by FUNCT_2:def 1;
(@ ((@ sin) |^ (n -' 2))) | REAL is continuous by Th21;
then A10: g | REAL is continuous ;
A11: G is_integral_of g, REAL by A1, Th31;
[.0,(PI / 2).] c= REAL ;
then A13: ((F . (PI / 2)) * (G . (PI / 2))) - ((F . 0) * (G . 0)) = (integral ((f (#) G),0,(PI / 2))) + (integral ((F (#) g),0,(PI / 2))) by INTEGRA7:22, INTEGRA7:25, COMPTRIG:5, A9, A6, A10, A7, A11;
A14: (@ (@ (- cos))) . (PI / 2) = - 0 by SIN_COS:76, VALUED_1:8;
A15: - (@ ((@ cos) |^ 2)) = (- cos) (#) cos by RFUNCT_1:12, Th35;
A16: (@ sin) |^ 2 = (1. (RAlgebra REAL)) - ((@ cos) |^ 2) by Th35, VECTSP_2:2;
reconsider f = (@ cos) |^ 2 as Element of (RAlgebra REAL) ;
A17: (@ ((@ sin) |^ 2)) - (@ (1. (RAlgebra REAL))) = ((@ sin) |^ 2) - (1. (RAlgebra REAL)) by Th19
.= - ((@ cos) |^ 2) by A16, VECTSP_2:2
.= @ ((- 1) * ((@ cos) |^ 2)) by RLVECT_1:16
.= - (@ ((@ cos) |^ 2)) by Th17 ;
set e1 = 1. (RAlgebra REAL);
set s1 = (n -' 1) (#) (@ ((@ sin) |^ (n -' 2)));
A18: (@ ((@ sin) |^ 2)) (#) ((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))) = (n -' 1) (#) ((@ ((@ sin) |^ 2)) (#) (@ ((@ sin) |^ (n -' 2)))) by RFUNCT_1:13
.= (n -' 1) (#) (@ (((@ sin) |^ 2) * ((@ sin) |^ (n -' 2)))) by Th13
.= (n -' 1) (#) (@ ((@ sin) |^ ((n -' 2) + 2))) by BINOM:10
.= (n -' 1) (#) (@ ((@ sin) |^ n)) by A1, XREAL_1:235 ;
(@ (1. (RAlgebra REAL))) (#) (@ ((@ sin) |^ (n -' 2))) = (1. (RAlgebra REAL)) * ((@ sin) |^ (n -' 2)) by Th13
.= @ ((@ sin) |^ (n -' 2)) ;
then (@ (1. (RAlgebra REAL))) (#) ((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))) = (n -' 1) (#) (@ ((@ sin) |^ (n -' 2))) by RFUNCT_1:13;
then A21: ((@ ((@ sin) |^ 2)) - (@ (1. (RAlgebra REAL)))) (#) ((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))) = ((n -' 1) (#) (@ ((@ sin) |^ n))) - ((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))) by A18, RFUNCT_1:14;
set I1 = @ ((@ sin) |^ n);
set I2 = @ ((@ sin) |^ (n -' 2));
A22: F (#) g = ((n -' 1) (#) (@ ((@ sin) |^ n))) - ((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))) by A21, A17, A15, RFUNCT_1:9;
A23: ( ((n -' 1) (#) (@ ((@ sin) |^ n))) | ['0,(PI / 2)'] is continuous & (n -' 1) (#) (@ ((@ sin) |^ n)) is_integrable_on ['0,(PI / 2)'] & ((n -' 1) (#) (@ ((@ sin) |^ n))) | ['0,(PI / 2)'] is bounded ) by Th26;
A24: ( ((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))) | ['0,(PI / 2)'] is continuous & (n -' 1) (#) (@ ((@ sin) |^ (n -' 2))) is_integrable_on ['0,(PI / 2)'] & ((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))) | ['0,(PI / 2)'] is bounded ) by Th26;
A25: ( (@ ((@ sin) |^ n)) | ['0,(PI / 2)'] is continuous & @ ((@ sin) |^ n) is_integrable_on ['0,(PI / 2)'] & (@ ((@ sin) |^ n)) | ['0,(PI / 2)'] is bounded ) by Th25;
A26: ( (@ ((@ sin) |^ (n -' 2))) | ['0,(PI / 2)'] is continuous & @ ((@ sin) |^ (n -' 2)) is_integrable_on ['0,(PI / 2)'] & (@ ((@ sin) |^ (n -' 2))) | ['0,(PI / 2)'] is bounded ) by Th25;
['0,(PI / 2)'] = [.0,(PI / 2).] by COMPTRIG:5, INTEGRA5:def 3;
then A28: ( 0 in ['0,(PI / 2)'] & PI / 2 in ['0,(PI / 2)'] ) by COMPTRIG:5, XXREAL_1:1;
A30: ( dom (@ ((@ sin) |^ n)) = REAL & dom (@ ((@ sin) |^ (n -' 2))) = REAL ) by FUNCT_2:def 1;
( dom ((n -' 1) (#) (@ ((@ sin) |^ n))) = REAL & dom ((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))) = REAL ) by FUNCT_2:def 1;
then A31: integral ((F (#) g),0,(PI / 2)) = (integral (((n -' 1) (#) (@ ((@ sin) |^ n))),0,(PI / 2))) - (integral (((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))),0,(PI / 2))) by COMPTRIG:5, A22, A28, A23, A24, INTEGRA6:24;
A32: integral (((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))),0,(PI / 2)) = (n -' 1) * (integral ((@ ((@ sin) |^ (n -' 2))),0,(PI / 2))) by A26, COMPTRIG:5, A30, INTEGRA6:10;
A33: ((F . (PI / 2)) * (G . (PI / 2))) - ((F . 0) * (G . 0)) = (0 * (G . (PI / 2))) - ((F . 0) * 0) by A14, A5, Th27
.= 0 ;
integral ((@ ((@ sin) |^ n)),0,(PI / 2)) = (- (integral (((n -' 1) (#) (@ ((@ sin) |^ n))),0,(PI / 2)))) + (integral (((n -' 1) (#) (@ ((@ sin) |^ (n -' 2)))),0,(PI / 2))) by A31, A33, A13, A4
.= (- ((n -' 1) * (integral ((@ ((@ sin) |^ n)),0,(PI / 2))))) + ((n -' 1) * (integral ((@ ((@ sin) |^ (n -' 2))),0,(PI / 2)))) by A25, COMPTRIG:5, A30, INTEGRA6:10, A32 ;
then A34: (n -' 1) * (integral ((@ ((@ sin) |^ (n -' 2))),0,(PI / 2))) = ((n -' 1) + 1) * (integral ((@ ((@ sin) |^ n)),0,(PI / 2)))
.= n * (integral ((@ ((@ sin) |^ n)),0,(PI / 2))) by A1, XXREAL_0:2, XREAL_1:235
.= n * ('I' . n0) by Def6 ;
((n -' 1) * ('I' . (n -' 2))) / n = (n * ('I' . n)) / n by A34, Def6
.= 'I' . n by A1, XCMPLX_1:89 ;
hence ((n -' 1) / n) * ('I' . (n -' 2)) = 'I' . n ; :: thesis: verum