let n be Element of NAT ; 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:25
.=
(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; verum