let z be Complex; :: thesis: for n0 being non zero Nat
for r being Real st r > 0 holds
n0 -root (z / r) = (n0 -root z) / (n0 -root r)
let n0 be non zero Nat; :: thesis: for r being Real st r > 0 holds
n0 -root (z / r) = (n0 -root z) / (n0 -root r)
let r be Real; :: thesis: ( r > 0 implies n0 -root (z / r) = (n0 -root z) / (n0 -root r) )
reconsider r9 = 1 / r as Real ;
reconsider n = n0 as Element of NAT by ORDINAL1:def 12;
A1: n >= 0 + 1 by NAT_1:13;
assume A2: r > 0 ; :: thesis: n0 -root (z / r) = (n0 -root z) / (n0 -root r)
then A3: |.r.| > 0 by COMPLEX1:47;
( z / r = z * (1 / r) & Arg (z * r9) = Arg z ) by A2, COMPLEX2:27, XCMPLX_1:99;
hence n0 -root (z / r) = (n -real-root (|.z.| / |.r.|)) * ((cos ((Arg z) / n)) + ((sin ((Arg z) / n)) * <i>)) by COMPLEX1:67
.= ((n -real-root |.z.|) / (n -real-root |.r.|)) * ((cos ((Arg z) / n)) + ((sin ((Arg z) / n)) * <i>)) by A3, A1, COMPLEX1:46, POWER:13
.= ((cos ((Arg z) / n)) + ((sin ((Arg z) / n)) * <i>)) / ((n -real-root |.r.|) / (n -real-root |.z.|)) by XCMPLX_1:79
.= ((n -real-root |.z.|) * ((cos ((Arg z) / n)) + ((sin ((Arg z) / n)) * <i>))) / (n -real-root |.r.|) by XCMPLX_1:77
.= (n0 -root z) / (n -real-root r) by A2, COMPLEX1:43
.= (n0 -root z) / (n0 -root r) by A2, Th8 ;
:: thesis: verum