let z be Element of COMPLEX ; :: thesis: for n being Element of NAT holds z |^ n = ((|.z.| to_power n) * (cos (n * (Arg z)))) + (((|.z.| to_power n) * (sin (n * (Arg z)))) * <i> )
let n be Element of NAT ; :: thesis: z |^ n = ((|.z.| to_power n) * (cos (n * (Arg z)))) + (((|.z.| to_power n) * (sin (n * (Arg z)))) * <i> )
set x = Arg z;
z |^ n = (((|.z.| * (cos (Arg z))) - (0 * (sin (Arg z)))) + (((|.z.| * (sin (Arg z))) + ((cos (Arg z)) * 0 )) * <i> )) |^ n by COMPLEX2:19
.= (|.z.| * ((cos (Arg z)) + ((sin (Arg z)) * <i> ))) |^ n
.= (|.z.| |^ n) * (((cos (Arg z)) + ((sin (Arg z)) * <i> )) |^ n) by NEWTON:12 ;
hence z |^ n = (|.z.| to_power n) * ((cos (n * (Arg z))) + ((sin (n * (Arg z))) * <i> )) by Th53
.= ((|.z.| to_power n) * (cos (n * (Arg z)))) + (((|.z.| to_power n) * (sin (n * (Arg z)))) * <i> ) ;
:: thesis: verum