A1:
sin . (PI / 4) <> 0
by Lm9, COMPTRIG:7;
A2: cot . ((3 / 4) * PI) =
(cos . ((3 / 4) * PI)) * ((sin . ((3 / 4) * PI)) ")
by Lm10, Th2, RFUNCT_1:def 1
.=
(- (sin . (PI / 4))) / (sin . ((PI / 2) + (PI / 4)))
by SIN_COS:78
.=
(- (sin . (PI / 4))) / (cos . (PI / 4))
by SIN_COS:78
.=
- ((sin . (PI / 4)) / (cos . (PI / 4)))
.=
- 1
by A1, SIN_COS:73, XCMPLX_1:60
;
cot . (PI / 4) =
(cos . (PI / 4)) / (sin . (PI / 4))
by Lm9, Th2, RFUNCT_1:def 1
.=
1
by A1, SIN_COS:73, XCMPLX_1:60
;
hence
( cot . (PI / 4) = 1 & cot (PI / 4) = 1 & cot . ((3 / 4) * PI) = - 1 & cot ((3 / 4) * PI) = - 1 )
by A2, Lm9, Lm10, Th14; verum