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 ;
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 ;
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 ; :: 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 A14: x |^ (k + 2) = (x |^ (k + 1)) * x by NEWTON:6;
x |^ (k + 2) = x * ((- x) |^ (k + 1)) by ;
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
A16: 0 < (- x) |^ (k + 1) by A6, A7;
A17: 1 <= ((- x) |^ (k + 1)) / ((- x) |^ (k + 1)) by ;
A18: ((- x) |^ (k + 1)) / ((- x) |^ (k + 1)) <= 1 by ;
((- x) |^ (k + 1)) / ((- x) |^ (k + 1)) = 1 by ;
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;
A22: ((k + 1) !) / ((k + 1) !) <= 1 by XREAL_1:183;
((k + 1) !) / ((k + 1) !) = 1 by ;
then ((k + 2) !) * (((k + 1) !) ") = ((k + 1) + 1) * 1 by ;
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 A23: (x |^ (k + 2)) / ((- x) |^ (k + 1)) <= ((k + 2) !) / ((k + 1) !) ; :: thesis: (((- x) rExpSeq) . (k + 1)) + (((- x) rExpSeq) . (k + 2)) >= 0
(x |^ (k + 2)) * (((- x) |^ (k + 1)) ") <= ((k + 2) !) / ((k + 1) !) by ;
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 ;
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 ;
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 ;
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 & - ((() . (k + 2)) - (((- x) rExpSeq) . (k + 1))) >= 0 ) ;
- (() . (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 consider m being Element of NAT such that
A34: k + 2 = (2 * m) + 1 by A5;
A35: - (x |^ (k + 2)) = (- x) |^ (k + 2) by ;
- (() . (k + 2)) = - ((x |^ (k + 2)) / ((k + 2) !)) by SIN_COS:def 5;
then - (() . (k + 2)) = - ((x |^ (k + 2)) * (((k + 2) !) ")) by XCMPLX_0:def 9;
then - (() . (k + 2)) = (- (x |^ (k + 2))) * (((k + 2) !) ") ;
then - (() . (k + 2)) = (- (x |^ (k + 2))) / ((k + 2) !) by XCMPLX_0:def 9;
hence - (() . (k + 2)) = ((- x) rExpSeq) . (k + 2) by ; :: 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 ; :: thesis: verum