let z be complex number ; :: thesis: for n0 being non zero natural number
for r being real number st r > 0 holds
n0 -root (z / r) = (n0 -root z) / (n0 -root r)
let n0 be non zero natural number ; :: thesis: for r being real number st r > 0 holds
n0 -root (z / r) = (n0 -root z) / (n0 -root r)
let r be real number ; :: thesis: ( r > 0 implies n0 -root (z / r) = (n0 -root z) / (n0 -root r) )
assume A1: r > 0 ; :: thesis: n0 -root (z / r) = (n0 -root z) / (n0 -root r)
reconsider r' = 1 / r as Real by XREAL_0:def 1;
reconsider n = n0 as Element of NAT by ORDINAL1:def 13;
A2: z / r = z * (1 / r) by XCMPLX_1:100;
A3: Arg (z * r') = Arg z by A1, COMPLEX2:40;
A4: |.r.| > 0 by A1, COMPLEX1:133;
A5: n >= 0 + 1 by NAT_1:13;
thus n0 -root (z / r) = (n -real-root (|.z.| / |.r.|)) * ((cos ((Arg z) / n)) + ((sin ((Arg z) / n)) * <i> )) by A2, A3, COMPLEX1:153
.= ((n -real-root |.z.|) / (n -real-root |.r.|)) * ((cos ((Arg z) / n)) + ((sin ((Arg z) / n)) * <i> )) by A5, COMPLEX1:132, A4, POWER:14
.= ((cos ((Arg z) / n)) + ((sin ((Arg z) / n)) * <i> )) / ((n -real-root |.r.|) / (n -real-root |.z.|)) by XCMPLX_1:80
.= ((n -real-root |.z.|) * ((cos ((Arg z) / n)) + ((sin ((Arg z) / n)) * <i> ))) / (n -real-root |.r.|) by XCMPLX_1:78
.= (n0 -root z) / (n -real-root r) by A1, COMPLEX1:129
.= (n0 -root z) / (n0 -root r) by A1, Th9 ; :: thesis: verum