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, COMPLEX2:19
.= (|.s.| * ((cos (Arg s)) + ((sin (Arg s)) * <i> ))) |^ n
.= (|.s.| |^ n) * (((cos (Arg s)) + ((sin (Arg s)) * <i> )) |^ n) by NEWTON:12
.= (|.s.| to_power n) * ((cos (n * (Arg s))) + ((sin (n * (Arg s))) * <i> )) by Th53
.= ((|.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 COMPLEX2:19
.= (|.z.| * ((cos (Arg z)) + ((sin (Arg z)) * <i> ))) |^ n
.= (|.z.| |^ n) * (((cos (Arg z)) + ((sin (Arg z)) * <i> )) |^ n) by NEWTON:12
.= (|.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> ) ;
then (|.s.| to_power n) * (cos (n * (Arg s))) = (|.z.| to_power n) * (cos (n * (Arg z))) by COMPLEX1:163;
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:68;
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:32;
then A6: ((|.s.| to_power n) ^2 ) * 1 = (|.z.| to_power n) ^2 by SIN_COS:32;
A7: |.s.| > 0 by A1, COMPLEX1:133;
then |.s.| to_power n > 0 by POWER:39;
then A8: |.s.| to_power n = sqrt ((|.z.| to_power n) ^2 ) by A6, SQUARE_1:89;
A9: |.z.| > 0 by A2, COMPLEX1:133;
then |.z.| to_power n > 0 by POWER:39;
then |.s.| |^ n = |.z.| |^ n by A8, SQUARE_1:89;
then |.s.| = n -root (|.z.| |^ n) by A3, A7, POWER:5;
hence |.s.| = |.z.| by A3, A9, POWER:5; :: thesis: verum