let a be Real; :: thesis: for n being Nat
for k being Integer st a > 0 & n >= 1 holds
(n -Root a) #Z k = n -Root (a #Z k)

let n be Nat; :: thesis: for k being Integer st a > 0 & n >= 1 holds
(n -Root a) #Z k = n -Root (a #Z k)

let k be Integer; :: thesis: ( a > 0 & n >= 1 implies (n -Root a) #Z k = n -Root (a #Z k) )
assume that
A1: a > 0 and
A2: n >= 1 ; :: thesis: (n -Root a) #Z k = n -Root (a #Z k)
A3: n -Root a > 0 by A1, A2, Def2;
A4: for m being Nat st m >= 1 holds
(n -Root a) |^ m = n -Root (a |^ m)
proof
let m be Nat; :: thesis: ( m >= 1 implies (n -Root a) |^ m = n -Root (a |^ m) )
assume that
A5: m >= 1 and
A6: (n -Root a) |^ m <> n -Root (a |^ m) ; :: thesis: contradiction
A7: a |^ m > 0 by ;
then A8: n -Root (a |^ m) >= 0 by ;
A9: m -Root (n -Root (a |^ m)) = (n * m) -Root (a |^ m) by A2, A5, A7, Th25
.= n -Root (m -Root (a |^ m)) by A2, A5, A7, Th25
.= n -Root a by A1, A5, Lm2 ;
A10: m -Root ((n -Root a) |^ m) = n -Root a by A3, A5, Lm2;
A11: (n -Root a) |^ m >= 0 by ;
per cases ) |^ m < n -Root (a |^ m) or (n -Root a) |^ m > n -Root (a |^ m) ) by ;
suppose (n -Root a) |^ m < n -Root (a |^ m) ; :: thesis: contradiction
end;
suppose (n -Root a) |^ m > n -Root (a |^ m) ; :: thesis: contradiction
end;
end;
end;
per cases ( k > 0 or k < 0 or k = 0 ) ;
suppose A12: k > 0 ; :: thesis: (n -Root a) #Z k = n -Root (a #Z k)
then |.k.| > 0 by ABSVALUE:def 1;
then A13: |.k.| >= 0 + 1 by NAT_1:13;
thus (n -Root a) #Z k = (n -Root a) |^ |.k.| by
.= n -Root (a |^ |.k.|) by
.= n -Root (a #Z k) by ; :: thesis: verum
end;
suppose A14: k < 0 ; :: thesis: (n -Root a) #Z k = n -Root (a #Z k)
then |.k.| > 0 by COMPLEX1:47;
then A15: |.k.| >= 0 + 1 by NAT_1:13;
A16: a |^ |.k.| > 0 by ;
thus (n -Root a) #Z k = ((n -Root a) |^ |.k.|) " by
.= (n -Root (a |^ |.k.|)) " by
.= 1 / (n -Root (a |^ |.k.|))
.= n -Root (1 / (a |^ |.k.|)) by
.= n -Root ((a |^ |.k.|) ")
.= n -Root (a #Z k) by ; :: thesis: verum
end;
suppose A17: k = 0 ; :: thesis: (n -Root a) #Z k = n -Root (a #Z k)
then n -Root (a #Z k) = n -Root 1 by Th34
.= 1 by ;
hence (n -Root a) #Z k = n -Root (a #Z k) by ; :: thesis: verum
end;
end;