let th be Real; :: thesis: ( th in [.0,1.] implies ( 0 < cos . th & cos . th >= 1 / 2 ) )
assume th in [.0,1.] ; :: thesis: ( 0 < cos . th & cos . th >= 1 / 2 )
then A1: ( 0 <= th & th <= 1 ) by XXREAL_1:1;
A2: Partial_Sums (th P_cos) is convergent by Th35;
A3: cos . th = Sum (th P_cos) by Th36;
lim ((Partial_Sums (th P_cos)) * bq) = lim (Partial_Sums (th P_cos)) by A2, SEQ_4:17;
then A4: lim ((Partial_Sums (th P_cos)) * bq) = cos . th by A3, SERIES_1:def 3;
for n being Nat holds ((Partial_Sums (th P_cos)) * bq) . n >= 1 / 2

proof

let n be Nat; :: thesis: ((Partial_Sums (th P_cos)) * bq) . n >= 1 / 2
A5: ((Partial_Sums (th P_cos)) * bq) . 0 = (Partial_Sums (th P_cos)) . (bq . 0) by FUNCT_2:15
.= (Partial_Sums (th P_cos)) . ((2 * 0) + 1) by Lm6
.= ((Partial_Sums (th P_cos)) . 0) + ((th P_cos) . (0 + 1)) by SERIES_1:def 1
.= ((th P_cos) . 0) + ((th P_cos) . (0 + 1)) by SERIES_1:def 1
.= ((((- 1) |^ 0) * (th |^ (2 * 0))) / ((2 * 0) !)) + ((th P_cos) . 1) by Def21
.= ((((- 1) |^ 0) * (th |^ (2 * 0))) / ((2 * 0) !)) + ((((- 1) |^ 1) * (th |^ (2 * 1))) / ((2 * 1) !)) by Def21
.= ((1 * (th |^ (2 * 0))) / ((2 * 0) !)) + ((((- 1) |^ 1) * (th |^ (2 * 1))) / ((2 * 1) !)) by Lm7
.= (1 / 1) + ((((- 1) |^ 1) * (th |^ (2 * 1))) / ((2 * 1) !)) by NEWTON:4, NEWTON:12
.= 1 + (((- 1) * (th |^ (2 * 1))) / ((2 * 1) !))
.= 1 + (((- 1) * (th * th)) / ((2 * 1) !)) by NEWTON:81
.= 1 - ((th ^2) / 2) by NEWTON:14 ;
defpred S₁[ Nat] means ((Partial_Sums (th P_cos)) * bq) . $1 >= 1 / 2;
th ^2 <= 1 ^2 by A1, SQUARE_1:15;
then ( 1 - (1 / 2) = 1 / 2 & (th ^2) / 2 <= 1 / 2 ) by XREAL_1:72;
then A6: S₁[ 0 ] by A5, XREAL_1:10;
A7: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A8: k in NAT by ORDINAL1:def 12;
assume A9: ((Partial_Sums (th P_cos)) * bq) . k >= 1 / 2 ; :: thesis: S₁[k + 1]
((Partial_Sums (th P_cos)) * bq) . (k + 1) = (Partial_Sums (th P_cos)) . (bq . (k + 1)) by FUNCT_2:15
.= (Partial_Sums (th P_cos)) . ((2 * (k + 1)) + 1) by Lm6
.= ((Partial_Sums (th P_cos)) . (((2 * k) + 1) + 1)) + ((th P_cos) . ((2 * (k + 1)) + 1)) by SERIES_1:def 1
.= (((Partial_Sums (th P_cos)) . ((2 * k) + 1)) + ((th P_cos) . (((2 * k) + 1) + 1))) + ((th P_cos) . ((2 * (k + 1)) + 1)) by SERIES_1:def 1
.= (((Partial_Sums (th P_cos)) . (bq . k)) + ((th P_cos) . (((2 * k) + 1) + 1))) + ((th P_cos) . ((2 * (k + 1)) + 1)) by Lm6
.= ((((Partial_Sums (th P_cos)) * bq) . k) + ((th P_cos) . (((2 * k) + 1) + 1))) + ((th P_cos) . ((2 * (k + 1)) + 1)) by FUNCT_2:15, A8 ;
then A10: (((Partial_Sums (th P_cos)) * bq) . (k + 1)) - (((Partial_Sums (th P_cos)) * bq) . k) = ((th P_cos) . (((2 * k) + 1) + 1)) + ((th P_cos) . ((2 * (k + 1)) + 1)) ;
A11: (th P_cos) . (((2 * k) + 1) + 1) = (((- 1) |^ (2 * (k + 1))) * (th |^ (2 * (2 * (k + 1))))) / ((2 * (2 * (k + 1))) !) by Def21
.= (1 * (th |^ (2 * (2 * (k + 1))))) / ((2 * (2 * (k + 1))) !) by Lm7
.= (th |^ (2 * (2 * (k + 1)))) / ((2 * (2 * (k + 1))) !) ;
A12: (th P_cos) . ((2 * (k + 1)) + 1) = (((- 1) |^ ((2 * (k + 1)) + 1)) * (th |^ (2 * ((2 * (k + 1)) + 1)))) / ((2 * ((2 * (k + 1)) + 1)) !) by Def21
.= ((- 1) * (th |^ (2 * ((2 * (k + 1)) + 1)))) / ((2 * ((2 * (k + 1)) + 1)) !) by Lm7 ;
A13: 2 * (2 * (k + 1)) < 2 * ((2 * (k + 1)) + 1) by XREAL_1:29, XREAL_1:68;
then A14: (2 * (2 * (k + 1))) ! <= (2 * ((2 * (k + 1)) + 1)) ! by Th38;
A15: th |^ (2 * ((2 * (k + 1)) + 1)) <= th |^ (2 * (2 * (k + 1))) by A1, A13, Th39;
A16: ( 0 <= th |^ (2 * ((2 * (k + 1)) + 1)) & (2 * ((2 * (k + 1)) + 1)) ! > 0 ) by POWER:3;
1 / ((2 * ((2 * (k + 1)) + 1)) !) <= 1 / ((2 * (2 * (k + 1))) !) by A14, XREAL_1:85;
then (th |^ (2 * ((2 * (k + 1)) + 1))) * (1 / ((2 * ((2 * (k + 1)) + 1)) !)) <= (th |^ (2 * (2 * (k + 1)))) * (1 / ((2 * (2 * (k + 1))) !)) by A15, A16, XREAL_1:66;
then (((th |^ (2 * (2 * (k + 1)))) * 1) / ((2 * (2 * (k + 1))) !)) - (((th |^ (2 * ((2 * (k + 1)) + 1))) * 1) / ((2 * ((2 * (k + 1)) + 1)) !)) >= 0 by XREAL_1:48;
then ((Partial_Sums (th P_cos)) * bq) . (k + 1) >= ((Partial_Sums (th P_cos)) * bq) . k by A10, A11, A12, XREAL_1:49;
hence S₁[k + 1] by A9, XXREAL_0:2; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A7);
hence ((Partial_Sums (th P_cos)) * bq) . n >= 1 / 2 ; :: thesis: verum

end;

hence ( 0 < cos . th & cos . th >= 1 / 2 ) by A2, A4, PREPOWER:1, SEQ_4:16; :: thesis: verum