let a be real number ; :: thesis: for n, m being Element of NAT st ( ( a >= 0 & n >= 1 & m >= 1 ) or ( not n is even & not m is even ) ) holds
n -root (m -root a) = (n * m) -root a
let n, m be Element of NAT ; :: thesis: ( ( ( a >= 0 & n >= 1 & m >= 1 ) or ( not n is even & not m is even ) ) implies n -root (m -root a) = (n * m) -root a )
assume A1: ( ( a >= 0 & n >= 1 & m >= 1 ) or ( not n is even & not m is even ) ) ; :: thesis: n -root (m -root a) = (n * m) -root a

A2: now

let a be real number ; :: thesis: for n, m being Element of NAT st a >= 0 & n >= 1 & m >= 1 holds
n -root (m -root a) = (n * m) -root a
let n, m be Element of NAT ; :: thesis: ( a >= 0 & n >= 1 & m >= 1 implies n -root (m -root a) = (n * m) -root a )
assume that
A3: a >= 0 and
A4: n >= 1 and
A5: m >= 1 ; :: thesis: n -root (m -root a) = (n * m) -root a
A6: n * m >= 1 by A4, A5, XREAL_1:161;
m -root a >= 0 by A3, A5, Th8;
then A8: m -Root a >= 0 by A3, A5, Def1;
thus n -root (m -root a) = n -root (m -Root a) by A3, A5, Def1
.= n -Root (m -Root a) by A4, A8, Def1
.= (n * m) -Root a by A3, A4, A5, PREPOWER:34
.= (n * m) -root a by A3, A6, Def1 ; :: thesis: verum

end;

now

assume not n is even ; :: thesis: ( not m is even implies n -root (m -root a) = (n * m) -root a )
then consider m1 being Element of NAT such that
A10: n = (2 * m1) + 1 by ABIAN:9;
assume not m is even ; :: thesis: n -root (m -root a) = (n * m) -root a
then consider m2 being Element of NAT such that
A11: m = (2 * m2) + 1 by ABIAN:9;
A12: n >= 0 + 1 by A10, XREAL_1:8;
A13: m >= 0 + 1 by A11, XREAL_1:8;
then A14: n * m >= 1 by A12, XREAL_1:161;
A15: n * m = (2 * (((m1 * (2 * m2)) + m1) + m2)) + 1 by A10, A11;

now

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

suppose a >= 0 ; :: thesis: n -root (m -root a) = (n * m) -root a

hence n -root (m -root a) = (n * m) -root a by A2, A12, A13; :: thesis: verum

end;

suppose A18: a < 0 ; :: thesis: n -root (m -root a) = (n * m) -root a

then m -root (- a) >= 0 by A13, Th8;
then A20: m -Root (- a) >= 0 by A13, A18, Def1;
thus n -root (m -root a) = n -root (- (m -Root (- a))) by A11, A18, Def1
.= - (n -root (- (- (m -Root (- a))))) by A10, Th11
.= - (n -Root (m -Root (- a))) by A12, A20, Def1
.= - ((n * m) -Root (- a)) by A12, A13, A18, PREPOWER:34
.= - ((n * m) -root (- a)) by A14, A18, Def1
.= (n * m) -root a by A15, Th11 ; :: thesis: verum

end;

end;

end;

hence n -root (m -root a) = (n * m) -root a ; :: thesis: verum

end;

hence n -root (m -root a) = (n * m) -root a by A1, A2; :: thesis: verum