let a, b be Real; :: thesis: for n being Nat st a >= 0 & b >= 0 & n >= 1 holds
n -Root (a * b) = (n -Root a) * (n -Root b)

let n be Nat; :: thesis: ( a >= 0 & b >= 0 & n >= 1 implies n -Root (a * b) = (n -Root a) * (n -Root b) )
assume that
A1: a >= 0 and
A2: b >= 0 and
A3: n >= 1 and
A4: n -Root (a * b) <> (n -Root a) * (n -Root b) ; :: thesis: contradiction
A5: ((n -Root a) * (n -Root b)) |^ n = ((n -Root a) |^ n) * ((n -Root b) |^ n) by NEWTON:7
.= a * ((n -Root b) |^ n) by A1, A3, Th19
.= a * b by A2, A3, Th19 ;
per cases ( ( a > 0 & b > 0 ) or ( a = 0 & b > 0 ) or ( a > 0 & b = 0 ) or ( a = 0 & b = 0 ) ) by A1, A2;
suppose A6: ( a > 0 & b > 0 ) ; :: thesis: contradiction
then A7: n -Root b > 0 by ;
A8: n -Root a > 0 by A3, A6, Def2;
a * b > 0 by A6;
then A9: n -Root (a * b) > 0 by ;
per cases ( n -Root (a * b) < (n -Root a) * (n -Root b) or n -Root (a * b) > (n -Root a) * (n -Root b) ) by ;
suppose n -Root (a * b) < (n -Root a) * (n -Root b) ; :: thesis: contradiction
end;
suppose n -Root (a * b) > (n -Root a) * (n -Root b) ; :: thesis: contradiction
end;
end;
end;
suppose A10: ( a = 0 & b > 0 ) ; :: thesis: contradiction
end;
suppose A11: ( a > 0 & b = 0 ) ; :: thesis: contradiction
end;
suppose A12: ( a = 0 & b = 0 ) ; :: thesis: contradiction
end;
end;
{"found_math": false, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0}