let z, s be Element of COMPLEX ; 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 ; ( 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
; |.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; verum