let a be Real; 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; ( ( ( 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 ) )
; n -root (m -root a) = (n * m) -root a
A2:
now 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 alet a be
Real;
for n, m being Nat st a >= 0 & n >= 1 & m >= 1 holds
n -root (m -root a) = (n * m) -root alet n,
m be
Nat;
( 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
;
n -root (m -root a) = (n * m) -root aA6:
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
;
verum end;
now ( n is odd & m is odd implies n -root (m -root a) = (n * m) -root a )assume
n is
odd
;
( 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
;
n -root (m -root a) = (n * m) -root athen 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 n -root (m -root a) = (n * m) -root aper cases
( a >= 0 or a < 0 )
;
suppose A14:
a < 0
;
n -root (m -root a) = (n * m) -root athen
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
;
verum end; end; end; hence
n -root (m -root a) = (n * m) -root a
;
verum end;
hence
n -root (m -root a) = (n * m) -root a
by A1, A2; verum