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