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

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

let a, b be Real; :: thesis: for n being Nat st n >= 1 & a >= 0 & b >= 0 holds
n -root (a * b) = (n -root a) * (n -root b)
let n be Nat; :: thesis: ( n >= 1 & a >= 0 & b >= 0 implies n -root (a * b) = (n -root a) * (n -root b) )
assume that
A3: n >= 1 and
A4: a >= 0 and
A5: b >= 0 ; :: thesis: n -root (a * b) = (n -root a) * (n -root b)
thus n -root (a * b) = n -Root (a * b) by A3, A4, A5, Def1
.= (n -Root a) * (n -Root b) by A3, A4, A5, PREPOWER:22
.= (n -root a) * (n -Root b) by A3, A4, Def1
.= (n -root a) * (n -root b) by A3, A5, Def1 ; :: thesis: verum

end;

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

assume A6: n is odd ; :: thesis: n -root (a * b) = (n -root a) * (n -root b)
then A7: n >= 1 by ABIAN:12;

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

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

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

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

end;

suppose A8: ( a < 0 & b < 0 ) ; :: thesis: n -root (a * b) = (n -root a) * (n -root b)

hence n -root (a * b) = n -Root ((- a) * (- b)) by A7, Def1
.= (- (- (n -Root (- a)))) * (n -Root (- b)) by A7, A8, PREPOWER:22
.= (- (n -root a)) * (- (- (n -Root (- b)))) by A6, A8, Def1
.= (- (n -root a)) * (- (n -root b)) by A6, A8, Def1
.= (n -root a) * (n -root b) ;
:: thesis: verum

end;

suppose A9: ( a >= 0 & b < 0 ) ; :: thesis: n -root (a * b) = (n -root a) * (n -root b)

thus n -root (a * b) = - (n -root (- (a * b))) by A6, Th10
.= - (n -root (a * (- b)))
.= - ((n -root a) * (n -root (- b))) by A2, A7, A9
.= (n -root a) * (- (n -root (- b)))
.= (n -root a) * (n -root b) by A6, Th10 ; :: thesis: verum

end;

suppose A10: ( a < 0 & b >= 0 ) ; :: thesis: n -root (a * b) = (n -root a) * (n -root b)

thus n -root (a * b) = - (n -root (- (a * b))) by A6, Th10
.= - (n -root ((- a) * b))
.= - ((n -root (- a)) * (n -root b)) by A2, A7, A10
.= (- (n -root (- a))) * (n -root b)
.= (n -root a) * (n -root b) by A6, Th10 ; :: thesis: verum

end;

end;

end;

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

end;

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