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 a) * (m -root a) = (n * m) -root (a |^ (n + m))
let m, n be Nat; :: thesis: ( ( ( a >= 0 & n >= 1 & m >= 1 ) or ( n is odd & m is odd ) ) implies (n -root a) * (m -root a) = (n * m) -root (a |^ (n + m)) )
assume A1: ( ( a >= 0 & n >= 1 & m >= 1 ) or ( n is odd & m is odd ) ) ; :: thesis: (n -root a) * (m -root a) = (n * m) -root (a |^ (n + m))

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

let a be Real; :: thesis: for n, m being Nat st a >= 0 & n >= 1 & m >= 1 holds
(n -root a) * (m -root a) = (n * m) -root (a |^ (n + m))
let n, m be Nat; :: thesis: ( a >= 0 & n >= 1 & m >= 1 implies (n -root a) * (m -root a) = (n * m) -root (a |^ (n + m)) )
assume that
A3: a >= 0 and
A4: n >= 1 and
A5: m >= 1 ; :: thesis: (n -root a) * (m -root a) = (n * m) -root (a |^ (n + m))
A6: ( n * m >= 1 & a |^ (n + m) >= 0 ) by A3, A4, A5, Th3, XREAL_1:159;
thus (n -root a) * (m -root a) = (n -root a) * (m -Root a) by A3, A5, Def1
.= (n -Root a) * (m -Root a) by A3, A4, Def1
.= (n * m) -Root (a |^ (n + m)) by A3, A4, A5, PREPOWER:26
.= (n * m) -root (a |^ (n + m)) by A6, Def1 ; :: thesis: verum

end;

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

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

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

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

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

hence (n -root a) * (m -root a) = (n * m) -root (a |^ (n + m)) by A2, A9; :: thesis: verum

end;

suppose A12: a < 0 ; :: thesis: (n -root a) * (m -root a) = (n * m) -root (a |^ (n + m))

A13: a |^ (n + m) >= 0 by A11, Th3;
thus (n -root a) * (m -root a) = (n -root a) * (- (m -Root (- a))) by A8, A12, Def1
.= (- (n -Root (- a))) * (- (m -Root (- a))) by A7, A12, Def1
.= (n -Root (- a)) * (m -Root (- a))
.= (n * m) -Root ((- a) |^ (n + m)) by A9, A12, PREPOWER:26
.= (n * m) -Root (a |^ (n + m)) by A11, Th1
.= (n * m) -root (a |^ (n + m)) by A10, A13, Def1 ; :: thesis: verum

end;

end;

end;

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

end;

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