let n be Element of NAT ; exp ((- (((2 * n) + (1 / 2)) * PI)) * <i>) = - (1 * <i>)
exp ((- (((2 * n) + (1 / 2)) * PI)) * <i>) =
(cos (- (((2 * n) + (1 / 2)) * PI))) + ((sin (- (((2 * n) + (1 / 2)) * PI))) * <i>)
by SIN_COS:25
.=
(cos (((2 * n) + (1 / 2)) * PI)) + ((sin (- (((2 * n) + (1 / 2)) * PI))) * <i>)
by SIN_COS:31
.=
(cos (((PI * 2) * n) + ((1 / 2) * PI))) + ((- (sin ((PI * (2 * n)) + ((1 / 2) * PI)))) * <i>)
by SIN_COS:31
.=
(cos . (((PI * 2) * n) + ((1 / 2) * PI))) + (- ((sin (((PI * 2) * n) + ((1 / 2) * PI))) * <i>))
by SIN_COS:def 19
.=
(cos . (((PI * 2) * n) + ((1 / 2) * PI))) + (- ((sin . (((PI * 2) * n) + ((1 / 2) * PI))) * <i>))
by SIN_COS:def 17
.=
(cos . ((1 / 2) * PI)) + ((- (sin . (((PI * 2) * n) + ((1 / 2) * PI)))) * <i>)
by SIN_COS2:11
.=
(- (sin . (PI / 2))) * <i>
by SIN_COS:76, SIN_COS2:10
;
hence
exp ((- (((2 * n) + (1 / 2)) * PI)) * <i>) = - (1 * <i>)
by SIN_COS:76; verum