A1: Partial_Sums (1 P_cos) is convergent by Th35;
A2: cos . 1 = Sum (1 P_cos) by Th36;
lim ((Partial_Sums (1 P_cos)) * bq) = lim (Partial_Sums (1 P_cos)) by A1, SEQ_4:17;
then A3: lim ((Partial_Sums (1 P_cos)) * bq) = cos . 1 by A2, SERIES_1:def 3;
for n being Nat holds ((Partial_Sums (1 P_cos)) * bq) . n >= 1 / 2

proof

let n be Nat; :: thesis: ((Partial_Sums (1 P_cos)) * bq) . n >= 1 / 2
defpred S₁[ 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:15
.= (Partial_Sums (1 P_cos)) . ((2 * 0) + 1) by Lm6
.= ((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 Def21
.= ((((- 1) |^ 0) * (1 |^ (2 * 0))) / ((2 * 0) !)) + ((((- 1) |^ 1) * (1 |^ (2 * 1))) / ((2 * 1) !)) by Def21
.= ((1 * (1 |^ (2 * 0))) / ((2 * 0) !)) + ((((- 1) |^ 1) * (1 |^ (2 * 1))) / ((2 * 1) !)) by Lm7
.= (1 / 1) + ((((- 1) |^ 1) * (1 |^ (2 * 1))) / ((2 * 1) !)) by NEWTON:12
.= 1 + (((- 1) * (1 |^ (2 * 1))) / ((2 * 1) !))
.= 1 + (((- 1) * 1) / ((2 * 1) !))
.= 1 + ((- 1) / ((1 !) * (1 + 1))) by NEWTON:15
.= 1 + ((- 1) / (((0 !) * (0 + 1)) * 2)) by NEWTON:15
.= 1 / 2 by NEWTON:12 ;
then A4: S₁[ 0 ] ;
A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A6: k in NAT by ORDINAL1:def 12;
assume A7: ((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:15
.= (Partial_Sums (1 P_cos)) . ((2 * (k + 1)) + 1) by Lm6
.= ((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 Lm6
.= ((((Partial_Sums (1 P_cos)) * bq) . k) + ((1 P_cos) . (((2 * k) + 1) + 1))) + ((1 P_cos) . ((2 * (k + 1)) + 1)) by FUNCT_2:15, A6 ;
then A8: (((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)) ;
A9: (1 P_cos) . (((2 * k) + 1) + 1) = (((- 1) |^ (2 * (k + 1))) * (1 |^ (2 * (2 * (k + 1))))) / ((2 * (2 * (k + 1))) !) by Def21
.= (1 * (1 |^ (2 * (2 * (k + 1))))) / ((2 * (2 * (k + 1))) !) by Lm7
.= 1 / ((2 * (2 * (k + 1))) !) ;
A10: (1 P_cos) . ((2 * (k + 1)) + 1) = (((- 1) |^ ((2 * (k + 1)) + 1)) * (1 |^ (2 * ((2 * (k + 1)) + 1)))) / ((2 * ((2 * (k + 1)) + 1)) !) by Def21
.= ((- 1) * (1 |^ (2 * ((2 * (k + 1)) + 1)))) / ((2 * ((2 * (k + 1)) + 1)) !) by Lm7
.= ((- 1) * 1) / ((2 * ((2 * (k + 1)) + 1)) !)
.= (- 1) / ((2 * ((2 * (k + 1)) + 1)) !) ;
2 * (2 * (k + 1)) < 2 * ((2 * (k + 1)) + 1) by XREAL_1:29, XREAL_1:68;
then (2 * (2 * (k + 1))) ! <= (2 * ((2 * (k + 1)) + 1)) ! by Th38;
then 1 / ((2 * (2 * (k + 1))) !) >= 1 / ((2 * ((2 * (k + 1)) + 1)) !) by XREAL_1:85;
then (1 / ((2 * (2 * (k + 1))) !)) - (1 / ((2 * ((2 * (k + 1)) + 1)) !)) >= 0 by XREAL_1:48;
then ((Partial_Sums (1 P_cos)) * bq) . (k + 1) >= ((Partial_Sums (1 P_cos)) * bq) . k by A8, A9, A10, XREAL_1:49;
hence S₁[k + 1] by A7, XXREAL_0:2; :: thesis: verum

end;

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

end;

then A11: cos . 1 >= 1 / 2 by A1, A3, PREPOWER:1, SEQ_4:16;
A12: Partial_Sums (1 P_sin) is convergent by Th35;
A13: sin . 1 = Sum (1 P_sin) by Th36;
lim ((Partial_Sums (1 P_sin)) * bq) = lim (Partial_Sums (1 P_sin)) by A12, SEQ_4:17;
then A14: lim ((Partial_Sums (1 P_sin)) * bq) = sin . 1 by A13, SERIES_1:def 3;
for n being Nat holds ((Partial_Sums (1 P_sin)) * bq) . n >= 5 / 6

proof

let n be Nat; :: thesis: ((Partial_Sums (1 P_sin)) * bq) . n >= 5 / 6
defpred S₁[ 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:15
.= (Partial_Sums (1 P_sin)) . ((2 * 0) + 1) by Lm6
.= ((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 Def20
.= ((((- 1) |^ 0) * (1 |^ ((2 * 0) + 1))) / (((2 * 0) + 1) !)) + ((((- 1) |^ 1) * (1 |^ ((2 * 1) + 1))) / (((2 * 1) + 1) !)) by Def20
.= ((1 * (1 |^ ((2 * 0) + 1))) / (((2 * 0) + 1) !)) + ((((- 1) |^ 1) * (1 |^ ((2 * 1) + 1))) / (((2 * 1) + 1) !)) by Lm7
.= (1 / ((0 + 1) !)) + ((((- 1) |^ 1) * (1 |^ ((2 * 1) + 1))) / (((2 * 1) + 1) !))
.= (1 / ((0 !) * 1)) + ((((- 1) |^ 1) * (1 |^ ((2 * 1) + 1))) / (((2 * 1) + 1) !)) by NEWTON:15
.= 1 + (((- 1) * (1 |^ ((2 * 1) + 1))) / (((2 * 1) + 1) !)) by NEWTON:12
.= 1 + (((- 1) * 1) / (((2 * 1) + 1) !))
.= 1 + ((- 1) / (((2 * 1) !) * ((2 * 1) + 1))) by NEWTON:15
.= 1 + ((- 1) / (((1 !) * (1 + 1)) * 3)) by NEWTON:15
.= 1 + ((- 1) / (((0 + 1) !) * (2 * 3)))
.= 1 + ((- 1) / ((1 * 1) * 6)) by NEWTON:12, NEWTON:15
.= 5 / 6 ;
then A15: S₁[ 0 ] ;
A16: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A17: k in NAT by ORDINAL1:def 12;
assume A18: ((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:15
.= (Partial_Sums (1 P_sin)) . ((2 * (k + 1)) + 1) by Lm6
.= ((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 Lm6
.= ((((Partial_Sums (1 P_sin)) * bq) . k) + ((1 P_sin) . (((2 * k) + 1) + 1))) + ((1 P_sin) . ((2 * (k + 1)) + 1)) by FUNCT_2:15, A17 ;
then A19: (((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)) ;
A20: (1 P_sin) . (((2 * k) + 1) + 1) = (((- 1) |^ (2 * (k + 1))) * (1 |^ ((2 * (2 * (k + 1))) + 1))) / (((2 * (2 * (k + 1))) + 1) !) by Def20
.= (1 * (1 |^ ((2 * (2 * (k + 1))) + 1))) / (((2 * (2 * (k + 1))) + 1) !) by Lm7
.= 1 / (((2 * (2 * (k + 1))) + 1) !) ;
A21: (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 Def20
.= ((- 1) * (1 |^ ((2 * ((2 * (k + 1)) + 1)) + 1))) / (((2 * ((2 * (k + 1)) + 1)) + 1) !) by Lm7
.= ((- 1) * 1) / (((2 * ((2 * (k + 1)) + 1)) + 1) !)
.= (- 1) / (((2 * ((2 * (k + 1)) + 1)) + 1) !) ;
2 * (2 * (k + 1)) < 2 * ((2 * (k + 1)) + 1) by XREAL_1:29, XREAL_1:68;
then (2 * (2 * (k + 1))) + 1 < (2 * ((2 * (k + 1)) + 1)) + 1 by XREAL_1:6;
then ((2 * (2 * (k + 1))) + 1) ! <= ((2 * ((2 * (k + 1)) + 1)) + 1) ! by Th38;
then 1 / (((2 * (2 * (k + 1))) + 1) !) >= 1 / (((2 * ((2 * (k + 1)) + 1)) + 1) !) by XREAL_1:85;
then (1 / (((2 * (2 * (k + 1))) + 1) !)) - (1 / (((2 * ((2 * (k + 1)) + 1)) + 1) !)) >= 0 by XREAL_1:48;
then ((Partial_Sums (1 P_sin)) * bq) . (k + 1) >= ((Partial_Sums (1 P_sin)) * bq) . k by A19, A20, A21, XREAL_1:49;
hence S₁[k + 1] by A18, XXREAL_0:2; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A15, A16);
hence ((Partial_Sums (1 P_sin)) * bq) . n >= 5 / 6 ; :: thesis: verum

end;

then A22: sin . 1 >= 5 / 6 by A12, A14, PREPOWER:1, SEQ_4:16;
A23: ((cos . 1) ^2) + ((sin . 1) ^2) = 1 by Th28;
A24: (sin . 1) ^2 >= (5 / 6) ^2 by A22, SQUARE_1:15;
then 1 - (1 - ((cos . 1) ^2)) <= 1 - (25 / 36) by A23, XREAL_1:10;
then (cos . 1) ^2 < 25 / 36 by XXREAL_0:2;
then (sin . 1) ^2 > (cos . 1) ^2 by A24, XXREAL_0:2;
then A25: sqrt ((cos . 1) ^2) < sqrt ((sin . 1) ^2) by SQUARE_1:27, XREAL_1:63;
sqrt ((cos . 1) ^2) = cos . 1 by A11, SQUARE_1:22;
hence ( cos . 1 > 0 & sin . 1 > 0 & cos . 1 < sin . 1 ) by A11, A22, A25, SQUARE_1:22; :: thesis: verum