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:28
.=
(cos (((2 * n) + (1 / 2)) * PI )) + ((sin (- (((2 * n) + (1 / 2)) * PI ))) * <i> )
by SIN_COS:34
.=
(cos (((PI * 2) * n) + ((1 / 2) * PI ))) + ((- (sin ((PI * (2 * n)) + ((1 / 2) * PI )))) * <i> )
by SIN_COS:34
.=
(cos . (((PI * 2) * n) + ((1 / 2) * PI ))) + (- ((sin (((PI * 2) * n) + ((1 / 2) * PI ))) * <i> ))
by SIN_COS:def 23
.=
(cos . (((PI * 2) * n) + ((1 / 2) * PI ))) + (- ((sin . (((PI * 2) * n) + ((1 / 2) * PI ))) * <i> ))
by SIN_COS:def 21
.=
(cos . ((1 / 2) * PI )) + ((- (sin . (((PI * 2) * n) + ((1 / 2) * PI )))) * <i> )
by SIN_COS2:11
.=
(- (sin . (PI / 2))) * <i>
by SIN_COS:81, SIN_COS2:10
;
hence
exp ((- (((2 * n) + (1 / 2)) * PI )) * <i> ) = - (1 * <i> )
by SIN_COS:81; verum