A1:
Partial_Sums (1 P_cos ) is convergent
by Th39;
A2:
cos . 1 = Sum (1 P_cos )
by Th40;
A3:
lim ((Partial_Sums (1 P_cos )) * bq) = lim (Partial_Sums (1 P_cos ))
by A1, SEQ_4:30;
A4:
lim ((Partial_Sums (1 P_cos )) * bq) = cos . 1
by A2, A3, SERIES_1:def 3;
A5:
for n being Element of NAT holds ((Partial_Sums (1 P_cos )) * bq) . n >= 1 / 2
proof
let n be
Element of
NAT ;
((Partial_Sums (1 P_cos )) * bq) . n >= 1 / 2
defpred S1[
Element of
NAT ]
means ((Partial_Sums (1 P_cos )) * bq) . $1
>= 1
/ 2;
A6:
((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 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 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 Lm8
.=
(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
;
A7:
S1[
0 ]
by A6;
A8:
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
proof
let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )
assume A9:
((Partial_Sums (1 P_cos )) * bq) . k >= 1
/ 2
;
S1[k + 1]
A10:
((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 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:21
;
A11:
(((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))
by A10;
A12:
(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 Lm8
.=
1
/ ((2 * (2 * (k + 1))) ! )
by NEWTON:15
;
A13:
(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 Lm8
.=
((- 1) * 1) / ((2 * ((2 * (k + 1)) + 1)) ! )
by NEWTON:15
.=
(- 1) / ((2 * ((2 * (k + 1)) + 1)) ! )
;
A14:
2
* (2 * (k + 1)) < 2
* ((2 * (k + 1)) + 1)
by XREAL_1:31, XREAL_1:70;
A15:
(2 * (2 * (k + 1))) ! <= (2 * ((2 * (k + 1)) + 1)) !
by A14, Th42;
A16:
1
/ ((2 * (2 * (k + 1))) ! ) >= 1
/ ((2 * ((2 * (k + 1)) + 1)) ! )
by A15, NEWTON:23, XREAL_1:87;
A17:
(1 / ((2 * (2 * (k + 1))) ! )) - (1 / ((2 * ((2 * (k + 1)) + 1)) ! )) >= 0
by A16, XREAL_1:50;
A18:
((Partial_Sums (1 P_cos )) * bq) . (k + 1) >= ((Partial_Sums (1 P_cos )) * bq) . k
by A11, A12, A13, A17, XREAL_1:51;
thus
S1[
k + 1]
by A9, A18, XXREAL_0:2;
verum
end;
A19:
for
n being
Element of
NAT holds
S1[
n]
from NAT_1:sch 1(A7, A8);
thus
((Partial_Sums (1 P_cos )) * bq) . n >= 1
/ 2
by A19;
verum
end;
A20:
cos . 1 >= 1 / 2
by A1, A4, A5, PREPOWER:2, SEQ_4:29;
A21:
Partial_Sums (1 P_sin ) is convergent
by Th39;
A22:
sin . 1 = Sum (1 P_sin )
by Th40;
A23:
lim ((Partial_Sums (1 P_sin )) * bq) = lim (Partial_Sums (1 P_sin ))
by A21, SEQ_4:30;
A24:
lim ((Partial_Sums (1 P_sin )) * bq) = sin . 1
by A22, A23, SERIES_1:def 3;
A25:
for n being Element of NAT holds ((Partial_Sums (1 P_sin )) * bq) . n >= 5 / 6
proof
let n be
Element of
NAT ;
((Partial_Sums (1 P_sin )) * bq) . n >= 5 / 6
defpred S1[
Element of
NAT ]
means ((Partial_Sums (1 P_sin )) * bq) . $1
>= 5
/ 6;
A26:
((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 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 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 Lm8
.=
(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
;
A27:
S1[
0 ]
by A26;
A28:
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
proof
let k be
Element of
NAT ;
( S1[k] implies S1[k + 1] )
assume A29:
((Partial_Sums (1 P_sin )) * bq) . k >= 5
/ 6
;
S1[k + 1]
A30:
((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 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:21
;
A31:
(((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))
by A30;
A32:
(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 Lm8
.=
1
/ (((2 * (2 * (k + 1))) + 1) ! )
by NEWTON:15
;
A33:
(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 Lm8
.=
((- 1) * 1) / (((2 * ((2 * (k + 1)) + 1)) + 1) ! )
by NEWTON:15
.=
(- 1) / (((2 * ((2 * (k + 1)) + 1)) + 1) ! )
;
A34:
2
* (2 * (k + 1)) < 2
* ((2 * (k + 1)) + 1)
by XREAL_1:31, XREAL_1:70;
A35:
(2 * (2 * (k + 1))) + 1
< (2 * ((2 * (k + 1)) + 1)) + 1
by A34, XREAL_1:8;
A36:
((2 * (2 * (k + 1))) + 1) ! <= ((2 * ((2 * (k + 1)) + 1)) + 1) !
by A35, Th42;
A37:
1
/ (((2 * (2 * (k + 1))) + 1) ! ) >= 1
/ (((2 * ((2 * (k + 1)) + 1)) + 1) ! )
by A36, NEWTON:23, XREAL_1:87;
A38:
(1 / (((2 * (2 * (k + 1))) + 1) ! )) - (1 / (((2 * ((2 * (k + 1)) + 1)) + 1) ! )) >= 0
by A37, XREAL_1:50;
A39:
((Partial_Sums (1 P_sin )) * bq) . (k + 1) >= ((Partial_Sums (1 P_sin )) * bq) . k
by A31, A32, A33, A38, XREAL_1:51;
thus
S1[
k + 1]
by A29, A39, XXREAL_0:2;
verum
end;
A40:
for
n being
Element of
NAT holds
S1[
n]
from NAT_1:sch 1(A27, A28);
thus
((Partial_Sums (1 P_sin )) * bq) . n >= 5
/ 6
by A40;
verum
end;
A41:
sin . 1 >= 5 / 6
by A21, A24, A25, PREPOWER:2, SEQ_4:29;
A42:
((cos . 1) ^2 ) + ((sin . 1) ^2 ) = 1
by Th31;
A43:
(sin . 1) ^2 >= (5 / 6) ^2
by A41, SQUARE_1:77;
A44:
1 - (1 - ((cos . 1) ^2 )) <= 1 - (25 / 36)
by A42, A43, XREAL_1:12;
A45:
(cos . 1) ^2 < 25 / 36
by A44, XXREAL_0:2;
A46:
(sin . 1) ^2 > (cos . 1) ^2
by A43, A45, XXREAL_0:2;
A47:
sqrt ((cos . 1) ^2 ) < sqrt ((sin . 1) ^2 )
by A46, SQUARE_1:95, XREAL_1:65;
A48:
sqrt ((cos . 1) ^2 ) = cos . 1
by A20, SQUARE_1:89;
thus
( cos . 1 > 0 & sin . 1 > 0 & cos . 1 < sin . 1 )
by A20, A41, A47, A48, SQUARE_1:89; verum