let z, s be Element of COMPLEX ; :: thesis: for n being Element of NAT st s <> 0 & z <> 0 & n >= 1 & s |^ n = z |^ n holds
|.s.| = |.z.|
let n be Element of NAT ; :: thesis: ( s <> 0 & z <> 0 & n >= 1 & s |^ n = z |^ n implies |.s.| = |.z.| )
assume that
A1: s <> 0 and
A2: z <> 0 and
A3: n >= 1 and
A4: s |^ n = z |^ n ; :: thesis: |.s.| = |.z.|
z |^ n = ((|.s.| * (cos (Arg s))) + ((|.s.| * (sin (Arg s))) * <i>)) |^ n by A4, COMPTRIG:62
.= (|.s.| * ((cos (Arg s)) + ((sin (Arg s)) * <i>))) |^ n
.= (|.s.| |^ n) * (((cos (Arg s)) + ((sin (Arg s)) * <i>)) |^ n) by NEWTON:7
.= (|.s.| to_power n) * ((cos (n * (Arg s))) + ((sin (n * (Arg s))) * <i>)) by Th31
.= ((|.s.| to_power n) * (cos (n * (Arg s)))) + (((|.s.| to_power n) * (sin (n * (Arg s)))) * <i>) ;
then A5: ((|.s.| to_power n) * (cos (n * (Arg s)))) + (((|.s.| to_power n) * (sin (n * (Arg s)))) * <i>) = ((|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * <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
.= (|.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>) ;
then (|.s.| to_power n) * (cos (n * (Arg s))) = (|.z.| to_power n) * (cos (n * (Arg z))) by COMPLEX1:77;
then (((|.s.| to_power n) ^2) * ((cos (n * (Arg s))) ^2)) + (((|.s.| to_power n) * (sin (n * (Arg s)))) ^2) = (((|.z.| to_power n) * (cos (n * (Arg z)))) ^2) + (((|.z.| to_power n) * (sin (n * (Arg z)))) ^2) by A5, SQUARE_1:9;
then ((|.s.| to_power n) ^2) * (((cos (n * (Arg s))) ^2) + ((sin (n * (Arg s))) ^2)) = ((|.z.| to_power n) ^2) * (((cos (n * (Arg z))) ^2) + ((sin (n * (Arg z))) ^2)) ;
then ((|.s.| to_power n) ^2) * (((cos (n * (Arg s))) ^2) + ((sin (n * (Arg s))) ^2)) = ((|.z.| to_power n) ^2) * 1 by SIN_COS:29;
then A6: ((|.s.| to_power n) ^2) * 1 = (|.z.| to_power n) ^2 by SIN_COS:29;
A7: |.s.| > 0 by A1, COMPLEX1:47;
then |.s.| to_power n > 0 by POWER:34;
then A8: |.s.| to_power n = sqrt ((|.z.| to_power n) ^2) by A6, SQUARE_1:22;
A9: |.z.| > 0 by A2, COMPLEX1:47;
then |.z.| to_power n > 0 by POWER:34;
then |.s.| |^ n = |.z.| |^ n by A8, SQUARE_1:22;
then |.s.| = n -root (|.z.| |^ n) by A3, A7, POWER:4;
hence |.s.| = |.z.| by A3, A9, POWER:4; :: thesis: verum