let th be real number ; :: 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 A2: ( 0 <= th & th <= 1 ) by XXREAL_1:1;
th is Real by XREAL_0:def 1;
then A4: Partial_Sums (th P_cos ) is convergent by Th39;
A5: cos . th = Sum (th P_cos ) by Th40;
lim ((Partial_Sums (th P_cos )) * bq) = lim (Partial_Sums (th P_cos )) by A4, SEQ_4:30;
then A7: lim ((Partial_Sums (th P_cos )) * bq) = cos . th by A5, SERIES_1:def 3;
for n being Element of NAT holds ((Partial_Sums (th P_cos )) * bq) . n >= 1 / 2

proof

let n be Element of NAT ; :: thesis: ((Partial_Sums (th P_cos )) * bq) . n >= 1 / 2
A9: ((Partial_Sums (th P_cos )) * bq) . 0 = (Partial_Sums (th P_cos )) . (bq . 0 ) by FUNCT_2:21
.= (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 Def25
.= ((((- 1) |^ 0 ) * (th |^ (2 * 0 ))) / ((2 * 0 ) ! )) + ((((- 1) |^ 1) * (th |^ (2 * 1))) / ((2 * 1) ! )) by Def25
.= ((1 * (th |^ (2 * 0 ))) / ((2 * 0 ) ! )) + ((((- 1) |^ 1) * (th |^ (2 * 1))) / ((2 * 1) ! )) by Lm8
.= (1 / 1) + ((((- 1) |^ 1) * (th |^ (2 * 1))) / ((2 * 1) ! )) by NEWTON:9, NEWTON:18
.= 1 + (((- 1) * (th |^ (2 * 1))) / ((2 * 1) ! )) by NEWTON:10
.= 1 + (((- 1) * (th * th)) / ((2 * 1) ! )) by NEWTON:100
.= 1 - ((th ^2 ) / 2) by NEWTON:20 ;
defpred S₁[ Element of NAT ] means ((Partial_Sums (th P_cos )) * bq) . $1 >= 1 / 2;
th ^2 <= 1 ^2 by A2, SQUARE_1:77;
then ( 1 - (1 / 2) = 1 / 2 & (th ^2 ) / 2 <= 1 / 2 ) by XREAL_1:74;
then A12: S₁[ 0 ] by A9, XREAL_1:12;
A13: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A14: ((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:21
.= (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:21 ;
then A16: (((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)) ;
A17: (th P_cos ) . (((2 * k) + 1) + 1) = (((- 1) |^ (2 * (k + 1))) * (th |^ (2 * (2 * (k + 1))))) / ((2 * (2 * (k + 1))) ! ) by Def25
.= (1 * (th |^ (2 * (2 * (k + 1))))) / ((2 * (2 * (k + 1))) ! ) by Lm8
.= (th |^ (2 * (2 * (k + 1)))) / ((2 * (2 * (k + 1))) ! ) ;
A18: (th P_cos ) . ((2 * (k + 1)) + 1) = (((- 1) |^ ((2 * (k + 1)) + 1)) * (th |^ (2 * ((2 * (k + 1)) + 1)))) / ((2 * ((2 * (k + 1)) + 1)) ! ) by Def25
.= ((- 1) * (th |^ (2 * ((2 * (k + 1)) + 1)))) / ((2 * ((2 * (k + 1)) + 1)) ! ) by Lm8 ;
A19: 2 * (2 * (k + 1)) < 2 * ((2 * (k + 1)) + 1) by XREAL_1:31, XREAL_1:70;
then A20: (2 * (2 * (k + 1))) ! <= (2 * ((2 * (k + 1)) + 1)) ! by Th42;
A21: th |^ (2 * ((2 * (k + 1)) + 1)) <= th |^ (2 * (2 * (k + 1))) by A2, A19, Th43;
A22: ( 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 A20, XREAL_1:87;
then (th |^ (2 * ((2 * (k + 1)) + 1))) * (1 / ((2 * ((2 * (k + 1)) + 1)) ! )) <= (th |^ (2 * (2 * (k + 1)))) * (1 / ((2 * (2 * (k + 1))) ! )) by A21, A22, XREAL_1:68;
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:50;
then ((Partial_Sums (th P_cos )) * bq) . (k + 1) >= ((Partial_Sums (th P_cos )) * bq) . k by A16, A17, A18, XREAL_1:51;
hence S₁[k + 1] by A14, XXREAL_0:2; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A12, A13);
hence ((Partial_Sums (th P_cos )) * bq) . n >= 1 / 2 ; :: thesis: verum

end;

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