let a be Real; :: thesis: for m, n being Nat st ( ( a >= 0 & n >= 1 & m >= 1 ) or ( n is odd & m is odd ) ) holds
n -root (m -root a) = (n * m) -root a
let m, n be Nat; :: thesis: ( ( ( a >= 0 & n >= 1 & m >= 1 ) or ( n is odd & m is odd ) ) implies n -root (m -root a) = (n * m) -root a )
assume A1: ( ( a >= 0 & n >= 1 & m >= 1 ) or ( n is odd & m is odd ) ) ; :: thesis: n -root (m -root a) = (n * m) -root a

A2: now :: thesis: for a being Real
for n, m being Nat st a >= 0 & n >= 1 & m >= 1 holds
n -root (m -root a) = (n * m) -root a

let a be Real; :: thesis: for n, m being Nat st a >= 0 & n >= 1 & m >= 1 holds
n -root (m -root a) = (n * m) -root a
let n, m be 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:159;
m -root a >= 0 by A3, A5, Th7;
then A7: 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, A7, Def1
.= (n * m) -Root a by A3, A4, A5, PREPOWER:25
.= (n * m) -root a by A3, A6, Def1 ; :: thesis: verum

end;

now :: thesis: ( n is odd & m is odd implies n -root (m -root a) = (n * m) -root a )

assume n is odd ; :: thesis: ( m is odd implies n -root (m -root a) = (n * m) -root a )
then consider m1 being Nat such that
A8: n = (2 * m1) + 1 by ABIAN:9;
assume m is odd ; :: thesis: n -root (m -root a) = (n * m) -root a
then consider m2 being Nat such that
A9: m = (2 * m2) + 1 by ABIAN:9;
A10: n >= 0 + 1 by A8, XREAL_1:6;
A11: m >= 0 + 1 by A9, XREAL_1:6;
then A12: n * m >= 1 by A10, XREAL_1:159;
A13: n * m = (2 * (((m1 * (2 * m2)) + m1) + m2)) + 1 by A8, A9;

now :: thesis: n -root (m -root a) = (n * m) -root a

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, A10, A11; :: thesis: verum

end;

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

then m -root (- a) >= 0 by A11, Th7;
then A15: m -Root (- a) >= 0 by A11, A14, Def1;
thus n -root (m -root a) = n -root (- (m -Root (- a))) by A9, A14, Def1
.= - (n -root (- (- (m -Root (- a))))) by A8, Th10
.= - (n -Root (m -Root (- a))) by A10, A15, Def1
.= - ((n * m) -Root (- a)) by A10, A11, A14, PREPOWER:25
.= - ((n * m) -root (- a)) by A12, A14, Def1
.= (n * m) -root a by A13, Th10 ; :: 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