A1: cos . 1 >= 1 / 2

proof

A3: ( Partial_Sums (1 P_cos ) is convergent & cos . 1 = Sum (1 P_cos ) ) by Th39, Th40;
lim ((Partial_Sums (1 P_cos )) * bq) = lim (Partial_Sums (1 P_cos )) by A3, SEQ_4:30;
then A5: lim ((Partial_Sums (1 P_cos )) * bq) = cos . 1 by A3, SERIES_1:def 3;
for n being Element of NAT holds ((Partial_Sums (1 P_cos )) * bq) . n >= 1 / 2

proof

let n be Element of NAT ; :: thesis: ((Partial_Sums (1 P_cos )) * bq) . n >= 1 / 2
defpred S₁[ Element of NAT ] means ((Partial_Sums (1 P_cos )) * bq) . $1 >= 1 / 2;
((Partial_Sums (1 P_cos )) * bq) . 0 = (Partial_Sums (1 P_cos )) . (bq . 0 ) by FUNCT_2:21
.= (Partial_Sums (1 P_cos )) . ((2 * 0 ) + 1) by Lm10
.= ((Partial_Sums (1 P_cos )) . 0 ) + ((1 P_cos ) . (0 + 1)) by SERIES_1:def 1
.= ((1 P_cos ) . 0 ) + ((1 P_cos ) . (0 + 1)) by SERIES_1:def 1
.= ((((- 1) |^ 0 ) * (1 |^ (2 * 0 ))) / ((2 * 0 ) ! )) + ((1 P_cos ) . 1) by Def25
.= ((((- 1) |^ 0 ) * (1 |^ (2 * 0 ))) / ((2 * 0 ) ! )) + ((((- 1) |^ 1) * (1 |^ (2 * 1))) / ((2 * 1) ! )) by Def25
.= ((1 * (1 |^ (2 * 0 ))) / ((2 * 0 ) ! )) + ((((- 1) |^ 1) * (1 |^ (2 * 1))) / ((2 * 1) ! )) by Lm11
.= (1 / 1) + ((((- 1) |^ 1) * (1 |^ (2 * 1))) / ((2 * 1) ! )) by NEWTON:9, NEWTON:18
.= 1 + (((- 1) * (1 |^ (2 * 1))) / ((2 * 1) ! )) by NEWTON:10
.= 1 + (((- 1) * 1) / ((2 * 1) ! )) by NEWTON:15
.= 1 + ((- 1) / ((1 ! ) * (1 + 1))) by NEWTON:21
.= 1 + ((- 1) / (((0 ! ) * (0 + 1)) * 2)) by NEWTON:21
.= 1 / 2 by NEWTON:18 ;
then A6: S₁[ 0 ] ;
A7: 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 A8: ((Partial_Sums (1 P_cos )) * bq) . k >= 1 / 2 ; :: thesis: S₁[k + 1]
((Partial_Sums (1 P_cos )) * bq) . (k + 1) = (Partial_Sums (1 P_cos )) . (bq . (k + 1)) by FUNCT_2:21
.= (Partial_Sums (1 P_cos )) . ((2 * (k + 1)) + 1) by Lm10
.= ((Partial_Sums (1 P_cos )) . (((2 * k) + 1) + 1)) + ((1 P_cos ) . ((2 * (k + 1)) + 1)) by SERIES_1:def 1
.= (((Partial_Sums (1 P_cos )) . ((2 * k) + 1)) + ((1 P_cos ) . (((2 * k) + 1) + 1))) + ((1 P_cos ) . ((2 * (k + 1)) + 1)) by SERIES_1:def 1
.= (((Partial_Sums (1 P_cos )) . (bq . k)) + ((1 P_cos ) . (((2 * k) + 1) + 1))) + ((1 P_cos ) . ((2 * (k + 1)) + 1)) by Lm10
.= ((((Partial_Sums (1 P_cos )) * bq) . k) + ((1 P_cos ) . (((2 * k) + 1) + 1))) + ((1 P_cos ) . ((2 * (k + 1)) + 1)) by FUNCT_2:21 ;
then A9: (((Partial_Sums (1 P_cos )) * bq) . (k + 1)) - (((Partial_Sums (1 P_cos )) * bq) . k) = ((1 P_cos ) . (((2 * k) + 1) + 1)) + ((1 P_cos ) . ((2 * (k + 1)) + 1)) ;
A10: (1 P_cos ) . (((2 * k) + 1) + 1) = (((- 1) |^ (2 * (k + 1))) * (1 |^ (2 * (2 * (k + 1))))) / ((2 * (2 * (k + 1))) ! ) by Def25
.= (1 * (1 |^ (2 * (2 * (k + 1))))) / ((2 * (2 * (k + 1))) ! ) by Lm11
.= 1 / ((2 * (2 * (k + 1))) ! ) by NEWTON:15 ;
B11: (1 P_cos ) . ((2 * (k + 1)) + 1) = (((- 1) |^ ((2 * (k + 1)) + 1)) * (1 |^ (2 * ((2 * (k + 1)) + 1)))) / ((2 * ((2 * (k + 1)) + 1)) ! ) by Def25
.= ((- 1) * (1 |^ (2 * ((2 * (k + 1)) + 1)))) / ((2 * ((2 * (k + 1)) + 1)) ! ) by Lm11
.= ((- 1) * 1) / ((2 * ((2 * (k + 1)) + 1)) ! ) by NEWTON:15
.= (- 1) / ((2 * ((2 * (k + 1)) + 1)) ! ) ;
2 * (2 * (k + 1)) < 2 * ((2 * (k + 1)) + 1) by XREAL_1:31, XREAL_1:70;
then A12: (2 * (2 * (k + 1))) ! <= (2 * ((2 * (k + 1)) + 1)) ! by Th42;
1 / ((2 * (2 * (k + 1))) ! ) >= 1 / ((2 * ((2 * (k + 1)) + 1)) ! ) by A12, NEWTON:23, XREAL_1:87;
then (1 / ((2 * (2 * (k + 1))) ! )) - (1 / ((2 * ((2 * (k + 1)) + 1)) ! )) >= 0 by XREAL_1:50;
then ((Partial_Sums (1 P_cos )) * bq) . (k + 1) >= ((Partial_Sums (1 P_cos )) * bq) . k by A9, A10, B11, XREAL_1:51;
hence S₁[k + 1] by A8, XXREAL_0:2; :: thesis: verum

end;

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

end;

hence cos . 1 >= 1 / 2 by A3, A5, PREPOWER:2, SEQ_4:29; :: thesis: verum

end;

A13: sin . 1 >= 5 / 6

proof

A15: ( Partial_Sums (1 P_sin ) is convergent & sin . 1 = Sum (1 P_sin ) ) by Th39, Th40;
lim ((Partial_Sums (1 P_sin )) * bq) = lim (Partial_Sums (1 P_sin )) by A15, SEQ_4:30;
then A17: lim ((Partial_Sums (1 P_sin )) * bq) = sin . 1 by A15, SERIES_1:def 3;
for n being Element of NAT holds ((Partial_Sums (1 P_sin )) * bq) . n >= 5 / 6

proof

let n be Element of NAT ; :: thesis: ((Partial_Sums (1 P_sin )) * bq) . n >= 5 / 6
defpred S₁[ Element of NAT ] means ((Partial_Sums (1 P_sin )) * bq) . $1 >= 5 / 6;
((Partial_Sums (1 P_sin )) * bq) . 0 = (Partial_Sums (1 P_sin )) . (bq . 0 ) by FUNCT_2:21
.= (Partial_Sums (1 P_sin )) . ((2 * 0 ) + 1) by Lm10
.= ((Partial_Sums (1 P_sin )) . 0 ) + ((1 P_sin ) . (0 + 1)) by SERIES_1:def 1
.= ((1 P_sin ) . 0 ) + ((1 P_sin ) . (0 + 1)) by SERIES_1:def 1
.= ((((- 1) |^ 0 ) * (1 |^ ((2 * 0 ) + 1))) / (((2 * 0 ) + 1) ! )) + ((1 P_sin ) . 1) by Def24
.= ((((- 1) |^ 0 ) * (1 |^ ((2 * 0 ) + 1))) / (((2 * 0 ) + 1) ! )) + ((((- 1) |^ 1) * (1 |^ ((2 * 1) + 1))) / (((2 * 1) + 1) ! )) by Def24
.= ((1 * (1 |^ ((2 * 0 ) + 1))) / (((2 * 0 ) + 1) ! )) + ((((- 1) |^ 1) * (1 |^ ((2 * 1) + 1))) / (((2 * 1) + 1) ! )) by Lm11
.= (1 / ((0 + 1) ! )) + ((((- 1) |^ 1) * (1 |^ ((2 * 1) + 1))) / (((2 * 1) + 1) ! )) by NEWTON:10
.= (1 / ((0 ! ) * 1)) + ((((- 1) |^ 1) * (1 |^ ((2 * 1) + 1))) / (((2 * 1) + 1) ! )) by NEWTON:21
.= 1 + (((- 1) * (1 |^ ((2 * 1) + 1))) / (((2 * 1) + 1) ! )) by NEWTON:10, NEWTON:18
.= 1 + (((- 1) * 1) / (((2 * 1) + 1) ! )) by NEWTON:15
.= 1 + ((- 1) / (((2 * 1) ! ) * ((2 * 1) + 1))) by NEWTON:21
.= 1 + ((- 1) / (((1 ! ) * (1 + 1)) * 3)) by NEWTON:21
.= 1 + ((- 1) / (((0 + 1) ! ) * (2 * 3)))
.= 1 + ((- 1) / ((1 * 1) * 6)) by NEWTON:18, NEWTON:21
.= 5 / 6 ;
then A18: S₁[ 0 ] ;
A19: 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 A20: ((Partial_Sums (1 P_sin )) * bq) . k >= 5 / 6 ; :: thesis: S₁[k + 1]
((Partial_Sums (1 P_sin )) * bq) . (k + 1) = (Partial_Sums (1 P_sin )) . (bq . (k + 1)) by FUNCT_2:21
.= (Partial_Sums (1 P_sin )) . ((2 * (k + 1)) + 1) by Lm10
.= ((Partial_Sums (1 P_sin )) . (((2 * k) + 1) + 1)) + ((1 P_sin ) . ((2 * (k + 1)) + 1)) by SERIES_1:def 1
.= (((Partial_Sums (1 P_sin )) . ((2 * k) + 1)) + ((1 P_sin ) . (((2 * k) + 1) + 1))) + ((1 P_sin ) . ((2 * (k + 1)) + 1)) by SERIES_1:def 1
.= (((Partial_Sums (1 P_sin )) . (bq . k)) + ((1 P_sin ) . (((2 * k) + 1) + 1))) + ((1 P_sin ) . ((2 * (k + 1)) + 1)) by Lm10
.= ((((Partial_Sums (1 P_sin )) * bq) . k) + ((1 P_sin ) . (((2 * k) + 1) + 1))) + ((1 P_sin ) . ((2 * (k + 1)) + 1)) by FUNCT_2:21 ;
then A21: (((Partial_Sums (1 P_sin )) * bq) . (k + 1)) - (((Partial_Sums (1 P_sin )) * bq) . k) = ((1 P_sin ) . (((2 * k) + 1) + 1)) + ((1 P_sin ) . ((2 * (k + 1)) + 1)) ;
A22: (1 P_sin ) . (((2 * k) + 1) + 1) = (((- 1) |^ (2 * (k + 1))) * (1 |^ ((2 * (2 * (k + 1))) + 1))) / (((2 * (2 * (k + 1))) + 1) ! ) by Def24
.= (1 * (1 |^ ((2 * (2 * (k + 1))) + 1))) / (((2 * (2 * (k + 1))) + 1) ! ) by Lm11
.= 1 / (((2 * (2 * (k + 1))) + 1) ! ) by NEWTON:15 ;
B23: (1 P_sin ) . ((2 * (k + 1)) + 1) = (((- 1) |^ ((2 * (k + 1)) + 1)) * (1 |^ ((2 * ((2 * (k + 1)) + 1)) + 1))) / (((2 * ((2 * (k + 1)) + 1)) + 1) ! ) by Def24
.= ((- 1) * (1 |^ ((2 * ((2 * (k + 1)) + 1)) + 1))) / (((2 * ((2 * (k + 1)) + 1)) + 1) ! ) by Lm11
.= ((- 1) * 1) / (((2 * ((2 * (k + 1)) + 1)) + 1) ! ) by NEWTON:15
.= (- 1) / (((2 * ((2 * (k + 1)) + 1)) + 1) ! ) ;
2 * (2 * (k + 1)) < 2 * ((2 * (k + 1)) + 1) by XREAL_1:31, XREAL_1:70;
then (2 * (2 * (k + 1))) + 1 < (2 * ((2 * (k + 1)) + 1)) + 1 by XREAL_1:8;
then A24: ((2 * (2 * (k + 1))) + 1) ! <= ((2 * ((2 * (k + 1)) + 1)) + 1) ! by Th42;
1 / (((2 * (2 * (k + 1))) + 1) ! ) >= 1 / (((2 * ((2 * (k + 1)) + 1)) + 1) ! ) by A24, NEWTON:23, XREAL_1:87;
then (1 / (((2 * (2 * (k + 1))) + 1) ! )) - (1 / (((2 * ((2 * (k + 1)) + 1)) + 1) ! )) >= 0 by XREAL_1:50;
then ((Partial_Sums (1 P_sin )) * bq) . (k + 1) >= ((Partial_Sums (1 P_sin )) * bq) . k by A21, A22, B23, XREAL_1:51;
hence S₁[k + 1] by A20, XXREAL_0:2; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A18, A19);
hence ((Partial_Sums (1 P_sin )) * bq) . n >= 5 / 6 ; :: thesis: verum

end;

hence sin . 1 >= 5 / 6 by A15, A17, PREPOWER:2, SEQ_4:29; :: thesis: verum

end;

sin . 1 > cos . 1

proof

A25: ((cos . 1) ^2 ) + ((sin . 1) ^2 ) = 1 by Th31;
A26: (sin . 1) ^2 >= (5 / 6) ^2 by A13, SQUARE_1:77;
then 1 - (1 - ((cos . 1) ^2 )) <= 1 - (25 / 36) by A25, XREAL_1:12;
then (cos . 1) ^2 < 25 / 36 by XXREAL_0:2;
then (sin . 1) ^2 > (cos . 1) ^2 by A26, XXREAL_0:2;
then A27: sqrt ((cos . 1) ^2 ) < sqrt ((sin . 1) ^2 ) by SQUARE_1:95, XREAL_1:65;
sqrt ((cos . 1) ^2 ) = cos . 1 by A1, SQUARE_1:89;
hence sin . 1 > cos . 1 by A13, A27, SQUARE_1:89; :: thesis: verum

end;

hence ( cos . 1 > 0 & sin . 1 > 0 & cos . 1 < sin . 1 ) by A1; :: thesis: verum