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)

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 A1, Th6;

then A8: n -Root (a |^ m) >= 0 by A2, Def2;

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 A3, Th6;

end;assume that

A5: m >= 1 and

A6: (n -Root a) |^ m <> n -Root (a |^ m) ; :: thesis: contradiction

A7: a |^ m > 0 by A1, Th6;

then A8: n -Root (a |^ m) >= 0 by A2, Def2;

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 A3, Th6;

per cases
( k > 0 or k < 0 or k = 0 )
;

end;

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 A12, Def3

.= n -Root (a |^ |.k.|) by A4, A13

.= n -Root (a #Z k) by A12, Def3 ; :: thesis: verum

end;then A13: |.k.| >= 0 + 1 by NAT_1:13;

thus (n -Root a) #Z k = (n -Root a) |^ |.k.| by A12, Def3

.= n -Root (a |^ |.k.|) by A4, A13

.= n -Root (a #Z k) by A12, Def3 ; :: thesis: verum

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 A1, Th6;

thus (n -Root a) #Z k = ((n -Root a) |^ |.k.|) " by A14, Def3

.= (n -Root (a |^ |.k.|)) " by A4, A15

.= 1 / (n -Root (a |^ |.k.|))

.= n -Root (1 / (a |^ |.k.|)) by A2, A16, Th23

.= n -Root ((a |^ |.k.|) ")

.= n -Root (a #Z k) by A14, Def3 ; :: thesis: verum

end;then A15: |.k.| >= 0 + 1 by NAT_1:13;

A16: a |^ |.k.| > 0 by A1, Th6;

thus (n -Root a) #Z k = ((n -Root a) |^ |.k.|) " by A14, Def3

.= (n -Root (a |^ |.k.|)) " by A4, A15

.= 1 / (n -Root (a |^ |.k.|))

.= n -Root (1 / (a |^ |.k.|)) by A2, A16, Th23

.= n -Root ((a |^ |.k.|) ")

.= n -Root (a #Z k) by A14, Def3 ; :: thesis: verum