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
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
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; verum