A1:
cos . (- (PI / 4)) = 1 / (sqrt 2)
by Th29, SIN_COS:33;
A2: cos . ((3 / 4) * PI ) =
cos . (PI + (- (PI / 4)))
.=
- (1 / (sqrt 2))
by A1, SIN_COS:83
;
A3:
sin . (- (PI / 4)) = - (1 / (sqrt 2))
by Th29, SIN_COS:33;
sin . ((3 / 4) * PI ) =
sin . (PI + (- (PI / 4)))
.=
- (- (1 / (sqrt 2)))
by A3, SIN_COS:83
.=
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:33; verum