A1:
cos . (- (PI / 4)) = 1 / (sqrt 2)
by Th29, SIN_COS:30;
A2: cos . ((3 / 4) * PI) =
cos . (PI + (- (PI / 4)))
.=
- (1 / (sqrt 2))
by A1, SIN_COS:78
;
A3:
sin . (- (PI / 4)) = - (1 / (sqrt 2))
by Th29, SIN_COS:30;
sin . ((3 / 4) * PI) =
sin . (PI + (- (PI / 4)))
.=
- (- (1 / (sqrt 2)))
by A3, SIN_COS:78
.=
1 / (sqrt 2)
;
hence
( sin . (- (PI / 4)) = - (1 / (sqrt 2)) & cos . (- (PI / 4)) = 1 / (sqrt 2) & sin . ((3 / 4) * PI) = 1 / (sqrt 2) & cos . ((3 / 4) * PI) = - (1 / (sqrt 2)) )
by A2, Th29, SIN_COS:30; verum