let a be real number ; :: thesis: for n being Element of NAT
for k being Integer st a > 0 & n >= 1 holds
(n -Root a) #Z k = n -Root (a #Z k)
let n be Element of 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 A1:
( a > 0 & n >= 1 )
; :: thesis: (n -Root a) #Z k = n -Root (a #Z k)
then A2:
n -Root a > 0
by Def3;
A3:
for m being Element of NAT st m >= 1 holds
(n -Root a) |^ m = n -Root (a |^ m)
proof
let m be
Element of
NAT ;
:: thesis: ( m >= 1 implies (n -Root a) |^ m = n -Root (a |^ m) )
assume that A4:
m >= 1
and A5:
(n -Root a) |^ m <> n -Root (a |^ m)
;
:: thesis: contradiction
A6:
a |^ m > 0
by A1, Th13;
then A7:
m -Root (n -Root (a |^ m)) =
(n * m) -Root (a |^ m)
by A1, A4, Th34
.=
n -Root (m -Root (a |^ m))
by A1, A4, A6, Th34
.=
n -Root a
by A1, A4, Lm2
;
A8:
m -Root ((n -Root a) |^ m) = n -Root a
by A2, A4, Lm2;
A9:
(n -Root a) |^ m >= 0
by A2, Th13;
A10:
n -Root (a |^ m) >= 0
by A1, A6, Def3;
end;