let n be Element of NAT ; :: thesis: exp ((((2 * n) + 1) * PI) * <i>) = - 1
exp ((((2 * n) + 1) * PI) * <i>) = (cos (((PI * 2) * n) + PI)) + ((sin ((PI * (2 * n)) + (1 * PI))) * <i>) by SIN_COS:28
.= (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