let a be Real; 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; for k being Integer st a > 0 & n >= 1 holds
(n -Root a) #Z k = n -Root (a #Z k)
let k be Integer; ( a > 0 & n >= 1 implies (n -Root a) #Z k = n -Root (a #Z k) )
assume that
A1:
a > 0
and
A2:
n >= 1
; (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;
( 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)
;
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;