let a, b be Real; 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; ( ( ( 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 )
; n -root (a * b) = (n -root a) * (n -root b)
A2:
now 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;
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;
( 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
;
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
;
verum end;
hence
n -root (a * b) = (n -root a) * (n -root b)
by A1, A2; verum