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