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 A1:
( 0 <= th & th <= 1 )
by XXREAL_1:1;
th is Real
by XREAL_0:def 1;
then A3:
( Partial_Sums (th P_cos ) is convergent & cos . th = Sum (th P_cos ) )
by Th39, Th40;
lim ((Partial_Sums (th P_cos )) * bq) = lim (Partial_Sums (th P_cos ))
by A3, SEQ_4:30;
then A5:
lim ((Partial_Sums (th P_cos )) * bq) = cos . th
by A3, 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
A6:
((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 Lm10
.=
((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 Lm11
.=
(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
;
A7:
1
- (1 / 2) = 1
/ 2
;
defpred S1[
Element of
NAT ]
means ((Partial_Sums (th P_cos )) * bq) . $1
>= 1
/ 2;
th ^2 <= 1
^2
by A1, SQUARE_1:77;
then
(th ^2 ) / 2
<= 1
/ 2
by XREAL_1:74;
then A8:
S1[
0 ]
by A6, A7, XREAL_1:12;
A9:
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A10:
((Partial_Sums (th P_cos )) * bq) . k >= 1
/ 2
;
:: thesis: S1[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 Lm10
.=
((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 Lm10
.=
((((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 A11:
(((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))
;
A12:
(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 Lm11
.=
(th |^ (2 * (2 * (k + 1)))) / ((2 * (2 * (k + 1))) ! )
;
B13:
(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 Lm11
;
A14:
2
* (2 * (k + 1)) < 2
* ((2 * (k + 1)) + 1)
by XREAL_1:31, XREAL_1:70;
then A15:
(2 * (2 * (k + 1))) ! <= (2 * ((2 * (k + 1)) + 1)) !
by Th42;
A16:
th |^ (2 * ((2 * (k + 1)) + 1)) <= th |^ (2 * (2 * (k + 1)))
by A1, A14, Th43;
A17:
0 <= th |^ (2 * ((2 * (k + 1)) + 1))
by POWER:3;
A18:
(
(2 * (2 * (k + 1))) ! > 0 &
(2 * ((2 * (k + 1)) + 1)) ! > 0 )
by NEWTON:23;
A19:
1
/ ((2 * ((2 * (k + 1)) + 1)) ! ) <= 1
/ ((2 * (2 * (k + 1))) ! )
by A15, NEWTON:23, XREAL_1:87;
A20:
(th |^ (2 * ((2 * (k + 1)) + 1))) * (1 / ((2 * ((2 * (k + 1)) + 1)) ! )) <= (th |^ (2 * (2 * (k + 1)))) * (1 / ((2 * (2 * (k + 1))) ! ))
by A16, A17, A19, A18, XREAL_1:68;
(((th |^ (2 * (2 * (k + 1)))) * 1) / ((2 * (2 * (k + 1))) ! )) - (((th |^ (2 * ((2 * (k + 1)) + 1))) * 1) / ((2 * ((2 * (k + 1)) + 1)) ! )) >= 0
by A20, XREAL_1:50;
then
((Partial_Sums (th P_cos )) * bq) . (k + 1) >= ((Partial_Sums (th P_cos )) * bq) . k
by A11, A12, B13, XREAL_1:51;
hence
S1[
k + 1]
by A10, XXREAL_0:2;
:: thesis: verum
end;
for
n being
Element of
NAT holds
S1[
n]
from NAT_1:sch 1(A8, A9);
hence
((Partial_Sums (th P_cos )) * bq) . n >= 1
/ 2
;
:: thesis: verum
end;
hence
( 0 < cos . th & cos . th >= 1 / 2 )
by A3, A5, PREPOWER:2, SEQ_4:29; :: thesis: verum