let k be Element of NAT ; :: thesis: for x being Element of REAL st k is odd & x > 0 & x <= 1 holds
(((- x) rExpSeq) . (k + 1)) + (((- x) rExpSeq) . (k + 2)) >= 0
let x be Element of REAL ; :: thesis: ( k is odd & x > 0 & x <= 1 implies (((- x) rExpSeq) . (k + 1)) + (((- x) rExpSeq) . (k + 2)) >= 0 )
assume that
A1: k is odd and
A2: x > 0 and
A3: x <= 1 ; :: thesis: (((- x) rExpSeq) . (k + 1)) + (((- x) rExpSeq) . (k + 2)) >= 0
consider m being Nat such that
A4: k = (2 * m) + 1 by A1, ABIAN:9;
set q = m + 1;
A5: k + 2 = (2 * (m + 1)) + 1 by A4;
consider m being Nat such that
A6: k = (2 * m) + 1 by A1, ABIAN:9;
A7: for k being Element of NAT st k is even holds
(- x) |^ k > 0
proof
let k be Element of NAT ; :: thesis: ( k is even implies (- x) |^ k > 0 )
assume k is even ; :: thesis: (- x) |^ k > 0
then consider m being Nat such that
A8: k = 2 * m by ABIAN:def 2;
defpred S1[ Nat] means (- x) |^ (2 * $1) > 0 ;
A9: S1[ 0 ] by NEWTON:4;
A10: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A11: S1[k] ; :: thesis: S1[k + 1]
(- x) |^ (2 * (k + 1)) = (- x) |^ ((2 * k) + 2) ;
then A12: (- x) |^ (2 * (k + 1)) = ((- x) |^ (2 * k)) * ((- x) |^ 2) by NEWTON:8;
(- x) * (- x) > 0 by A2;
then (- x) |^ 2 > 0 by NEWTON:81;
hence S1[k + 1] by A11, A12; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A9, A10);
 hence (- x) |^ k > 0 by A8; :: thesis: verum
end;
A13: (x |^ (k + 2)) / ((- x) |^ (k + 1)) = x
proof
x |^ (k + 2) = x |^ ((k + 1) + 1) ;
then x |^ (k + 2) = (x |^ (k + 1)) * x by NEWTON:6;
then x |^ (k + 2) = x * ((- x) |^ (k + 1)) by A6, POWER:1;
then (x |^ (k + 2)) / ((- x) |^ (k + 1)) = (x * ((- x) |^ (k + 1))) * (((- x) |^ (k + 1)) ") by XCMPLX_0:def 9;
then A15: (x |^ (k + 2)) / ((- x) |^ (k + 1)) = x * (((- x) |^ (k + 1)) * (((- x) |^ (k + 1)) ")) ;
((- x) |^ (k + 1)) * (((- x) |^ (k + 1)) ") = 1
proof
A17: 1 <= ((- x) |^ (k + 1)) / ((- x) |^ (k + 1)) by A6, A7, XREAL_1:181;
0 < (- x) |^ (k + 1) by A6, A7;
then A18: ((- x) |^ (k + 1)) / ((- x) |^ (k + 1)) <= 1 by XREAL_1:185;
((- x) |^ (k + 1)) / ((- x) |^ (k + 1)) = 1 by A17, A18, XXREAL_0:1;
hence ((- x) |^ (k + 1)) * (((- x) |^ (k + 1)) ") = 1 by XCMPLX_0:def 9; :: thesis: verum
end;
hence (x |^ (k + 2)) / ((- x) |^ (k + 1)) = x by A15; :: thesis: verum
end;
A19: 1 <= ((k + 2) !) / ((k + 1) !)
proof
(k + 2) ! = ((k + 1) + 1) * ((k + 1) !) by NEWTON:15;
then A20: ((k + 2) !) * (((k + 1) !) ") = ((k + 1) + 1) * (((k + 1) !) * (((k + 1) !) ")) ;
A21: 1 <= ((k + 1) !) / ((k + 1) !) by XREAL_1:181;
((k + 1) !) / ((k + 1) !) <= 1 by XREAL_1:183;
then ((k + 1) !) / ((k + 1) !) = 1 by A21, XXREAL_0:1;
then ((k + 2) !) * (((k + 1) !) ") = ((k + 1) + 1) * 1 by A20, XCMPLX_0:def 9;
then ((k + 2) !) * (((k + 1) !) ") >= 1 by NAT_1:11;
hence 1 <= ((k + 2) !) / ((k + 1) !) by XCMPLX_0:def 9; :: thesis: verum
end;
( (x |^ (k + 2)) / ((- x) |^ (k + 1)) <= ((k + 2) !) / ((k + 1) !) implies (((- x) rExpSeq) . (k + 1)) + (((- x) rExpSeq) . (k + 2)) >= 0 )
proof
assume (x |^ (k + 2)) / ((- x) |^ (k + 1)) <= ((k + 2) !) / ((k + 1) !) ; :: thesis: (((- x) rExpSeq) . (k + 1)) + (((- x) rExpSeq) . (k + 2)) >= 0
then (x |^ (k + 2)) * (((- x) |^ (k + 1)) ") <= ((k + 2) !) / ((k + 1) !) by XCMPLX_0:def 9;
then A24: (x |^ (k + 2)) * (((- x) |^ (k + 1)) ") <= (((k + 1) !) ") * ((k + 2) !) by XCMPLX_0:def 9;
(- x) |^ (k + 1) > 0 by A6, A7;
then A25: (x |^ (k + 2)) / ((k + 2) !) <= (((k + 1) !) ") / (((- x) |^ (k + 1)) ") by A24, XREAL_1:102;
A26: (((k + 1) !) ") * 1 = 1 / ((k + 1) !) by XCMPLX_0:def 9;
( (((k + 1) !) ") / (((- x) |^ (k + 1)) ") = (1 / ((k + 1) !)) * ((((- x) |^ (k + 1)) ") ") & 1 * (((k + 1) !) ") = 1 / ((k + 1) !) ) by A26, XCMPLX_0:def 9;
then A27: (((k + 1) !) ") / (((- x) |^ (k + 1)) ") = ((- x) |^ (k + 1)) / ((k + 1) !) by XCMPLX_0:def 9;
(x rExpSeq) . (k + 2) <= ((- x) |^ (k + 1)) / ((k + 1) !) by A25, A27, SIN_COS:def 5;
then (x rExpSeq) . (k + 2) <= ((- x) rExpSeq) . (k + 1) by SIN_COS:def 5;
then ((x rExpSeq) . (k + 2)) - (((- x) rExpSeq) . (k + 1)) <= (((- x) rExpSeq) . (k + 1)) - (((- x) rExpSeq) . (k + 1)) by XREAL_1:9;
then A28: ( ((x rExpSeq) . (k + 2)) - (((- x) rExpSeq) . (k + 1)) <= 0 & - (((x rExpSeq) . (k + 2)) - (((- x) rExpSeq) . (k + 1))) >= 0 ) ;
- ((x rExpSeq) . (k + 2)) = ((- x) rExpSeq) . (k + 2)
proof
defpred S1[ Nat] means - (x |^ ((2 * $1) + 1)) = (- x) |^ ((2 * $1) + 1);
A30: S1[ 0 ] ;
A31: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A32: S1[k] ; :: thesis: S1[k + 1]
- (x |^ ((2 * (k + 1)) + 1)) = - ((x |^ (((2 * k) + 1) + 1)) * x) by NEWTON:6;
then - (x |^ ((2 * (k + 1)) + 1)) = - (((x |^ ((2 * k) + 1)) * x) * x) by NEWTON:6;
then - (x |^ ((2 * (k + 1)) + 1)) = (((- x) |^ ((2 * k) + 1)) * (- x)) * (- x) by A32;
then - (x |^ ((2 * (k + 1)) + 1)) = ((- x) |^ (((2 * k) + 1) + 1)) * (- x) by NEWTON:6;
hence S1[k + 1] by NEWTON:6; :: thesis: verum
end;
A33: for k being Nat holds S1[k] from NAT_1:sch 2(A30, A31);
 consider m being Element of NAT such that
A34: k + 2 = (2 * m) + 1 by A5;
A35: - (x |^ (k + 2)) = (- x) |^ (k + 2) by A33, A34;
- ((x rExpSeq) . (k + 2)) = - ((x |^ (k + 2)) / ((k + 2) !)) by SIN_COS:def 5;
then - ((x rExpSeq) . (k + 2)) = - ((x |^ (k + 2)) * (((k + 2) !) ")) by XCMPLX_0:def 9;
then - ((x rExpSeq) . (k + 2)) = (- (x |^ (k + 2))) * (((k + 2) !) ") ;
then - ((x rExpSeq) . (k + 2)) = (- (x |^ (k + 2))) / ((k + 2) !) by XCMPLX_0:def 9;
hence - ((x rExpSeq) . (k + 2)) = ((- x) rExpSeq) . (k + 2) by A35, SIN_COS:def 5; :: thesis: verum
end;
hence (((- x) rExpSeq) . (k + 1)) + (((- x) rExpSeq) . (k + 2)) >= 0 by A28; :: thesis: verum
end;
hence (((- x) rExpSeq) . (k + 1)) + (((- x) rExpSeq) . (k + 2)) >= 0 by A3, A19, A13, XXREAL_0:2; :: thesis: verum