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:7
.= ((|.z.| |^ n) + (0 * <i>)) * ((cos (n * (Arg z))) + ((sin (n * (Arg z))) * <i>)) by Th53
.= ((|.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:11
.= (0 * (cos (n * (Arg z)))) + (((|.z.| |^ n) * (sin (n * (Arg z)))) * <i>) by A2, A3, COMPLEX1:44, NEWTON:11
.= ((|.z.| |^ n) * (cos (n * (Arg z)))) + (((|.z.| |^ n) * (sin (n * (Arg z)))) * <i>) by A2, A3, COMPLEX1:44, NEWTON:11 ;
:: thesis: verum
end;
end;