let z be Element of COMPLEX ; :: thesis: exp (z + ((2 * PI ) * <i> )) = exp z
z + ((2 * PI ) * <i> ) = ((Re z) + ((Im z) * <i> )) + (((2 * PI ) + (0 * <i> )) * <i> ) by COMPLEX1:29
.= ((Re z) + 0 ) + (((Im z) + (2 * PI )) * <i> ) ;
then exp (z + ((2 * PI ) * <i> )) = ((exp_R . (Re z)) * (cos . ((Im z) + ((2 * PI ) * 1)))) + (((exp_R . (Re z)) * (sin . ((Im z) + (2 * PI )))) * <i> ) by Th19
.= ((exp_R . (Re z)) * (cos . (Im z))) + (((exp_R . (Re z)) * (sin . ((Im z) + ((2 * PI ) * 1)))) * <i> ) by SIN_COS2:11
.= ((exp_R . (Re z)) * (cos . (Im z))) + (((exp_R . (Re z)) * (sin . (Im z))) * <i> ) by SIN_COS2:10
.= exp ((Re z) + ((Im z) * <i> )) by Th19 ;
hence exp (z + ((2 * PI ) * <i> )) = exp z by COMPLEX1:29; :: thesis: verum