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