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>)
z |^ n = (((|.z.| * (cos (Arg z))) - (0 * (sin (Arg z)))) + (((|.z.| * (sin (Arg z))) + ((cos (Arg z)) * 0)) * <i>)) |^ n by COMPTRIG:62
.= (|.z.| * ((cos (Arg z)) + ((sin (Arg z)) * <i>))) |^ n
.= (|.z.| |^ n) * (((cos (Arg z)) + ((sin (Arg z)) * <i>)) |^ n) by NEWTON:7 ;
hence z |^ n = (|.z.| to_power n) * ((cos (n * (Arg z))) + ((sin (n * (Arg z))) * <i>)) by Th31
.= ((|.z.| to_power n) * (cos (n * (Arg z)))) + (((|.z.| to_power n) * (sin (n * (Arg z)))) * <i>) ;
:: thesis: verum