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

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

let a be Real; :: thesis: for n being Nat st a > 0 & n >= 1 holds
n -root (1 / a) = 1 / (n -root a)
let n be Nat; :: thesis: ( a > 0 & n >= 1 implies n -root (1 / a) = 1 / (n -root a) )
assume A3: ( a > 0 & n >= 1 ) ; :: thesis: n -root (1 / a) = 1 / (n -root a)
hence n -root (1 / a) = n -Root (1 / a) by Def1
.= 1 / (n -Root a) by A3, PREPOWER:23
.= 1 / (n -root a) by A3, Def1 ;
:: thesis: verum

end;

now :: thesis: ( a <> 0 & n is odd implies n -root (1 / a) = 1 / (n -root a) )

assume that
A4: a <> 0 and
A5: n is odd ; :: thesis: n -root (1 / a) = 1 / (n -root a)
A6: n >= 1 by A5, ABIAN:12;

now :: thesis: n -root (1 / a) = 1 / (n -root a)

per cases ( a > 0 or a < 0 ) by A4;

suppose a > 0 ; :: thesis: n -root (1 / a) = 1 / (n -root a)

hence n -root (1 / a) = 1 / (n -root a) by A2, A6; :: thesis: verum

end;

suppose a < 0 ; :: thesis: 1 / (n -root a) = n -root (1 / a)

then A7: - a > 0 by XREAL_1:58;
thus 1 / (n -root a) = 1 / (- (n -root (- a))) by A5, Th10
.= - (1 / (n -root (- a))) by XCMPLX_1:188
.= - (n -root (1 / (- a))) by A2, A6, A7
.= - (n -root (- (1 / a))) by XCMPLX_1:188
.= n -root (1 / a) by A5, Th10 ; :: thesis: verum

end;

end;

end;

hence n -root (1 / a) = 1 / (n -root a) ; :: thesis: verum

end;

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