let z be Element of COMPLEX ; :: thesis: for n being Element of NAT st ( z <> 0 or n > 0 ) 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 <> 0 or n > 0 ) implies z |^ n = ((|.z.| to_power n) * (cos (n * (Arg z)))) + (((|.z.| to_power n) * (sin (n * (Arg z)))) * <i> ) )
assume A1: ( z <> 0 or n > 0 ) ; :: thesis: z |^ n = ((|.z.| to_power n) * (cos (n * (Arg z)))) + (((|.z.| to_power n) * (sin (n * (Arg z)))) * <i> )

per cases ( z <> 0 or ( z = 0 & n > 0 ) ) by A1;

suppose z <> 0 ; :: 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

end;

suppose A5: ( z = 0 & n > 0 ) ; :: thesis: z |^ n = ((|.z.| to_power n) * (cos (n * (Arg z)))) + (((|.z.| to_power n) * (sin (n * (Arg z)))) * <i> )

then 0 = |.z.| to_power n by COMPLEX1:130, POWER:def 2;
hence z |^ n = ((|.z.| to_power n) * (cos (n * (Arg z)))) + (((|.z.| to_power n) * (sin (n * (Arg z)))) * <i> ) by A5, Th50; :: thesis: verum

end;

end;