let z be Element of COMPLEX ; :: thesis: for n being Nat st ( z <> 0 or n <> 0 ) holds
z |^ n = ((|.z.| |^ n) * (cos (n * (Arg z)))) + (((|.z.| |^ n) * (sin (n * (Arg z)))) * <i> )
let n be Nat; :: thesis: ( ( z <> 0 or n <> 0 ) implies z |^ n = ((|.z.| |^ n) * (cos (n * (Arg z)))) + (((|.z.| |^ n) * (sin (n * (Arg z)))) * <i> ) )
assume A1: ( z <> 0 or n <> 0 ) ; :: thesis: z |^ n = ((|.z.| |^ n) * (cos (n * (Arg z)))) + (((|.z.| |^ n) * (sin (n * (Arg z)))) * <i> )

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

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

hence z |^ n = ((|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * <i> )) |^ n by Def1
.= ((|.z.| + (0 * <i> )) * ((cos (Arg z)) + ((sin (Arg z)) * <i> ))) |^ n
.= ((|.z.| + (0 * <i> )) |^ n) * (((cos (Arg z)) + ((sin (Arg z)) * <i> )) |^ n) by NEWTON:12
.= ((|.z.| |^ n) + (0 * <i> )) * ((cos (n * (Arg z))) + ((sin (n * (Arg z))) * <i> )) by Th71
.= ((|.z.| |^ n) * (cos (n * (Arg z)))) + (((|.z.| |^ n) * (sin (n * (Arg z)))) * <i> ) ;
:: thesis: verum

end;

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

then A3: n >= 1 + 0 by NAT_1:13;
hence z |^ n = (0 * (cos (n * (Arg z)))) + ((0 * (sin (n * (Arg z)))) * <i> ) by A2, NEWTON:16
.= (0 * (cos (n * (Arg z)))) + (((|.z.| |^ n) * (sin (n * (Arg z)))) * <i> ) by A2, A3, COMPLEX1:130, NEWTON:16
.= ((|.z.| |^ n) * (cos (n * (Arg z)))) + (((|.z.| |^ n) * (sin (n * (Arg z)))) * <i> ) by A2, A3, COMPLEX1:130, NEWTON:16 ;
:: thesis: verum

end;

end;