let a be real number ; :: thesis: for n being Element of NAT st ( ( a > 0 & n >= 1 ) or ( a <> 0 & not n is even ) ) holds
n -root (1 / a) = 1 / (n -root a)
let n be Element of NAT ; :: thesis: ( ( ( a > 0 & n >= 1 ) or ( a <> 0 & not n is even ) ) implies n -root (1 / a) = 1 / (n -root a) )
assume A1: ( ( a > 0 & n >= 1 ) or ( a <> 0 & not n is even ) ) ; :: thesis: n -root (1 / a) = 1 / (n -root a)

A2: now

let a be real number ; :: thesis: for n being Element of NAT st a > 0 & n >= 1 holds
n -root (1 / a) = 1 / (n -root a)
let n be Element of 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:32
.= 1 / (n -root a) by A3, Def1 ;
:: thesis: verum

end;

now

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

now

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

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

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

end;

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

then A11: - a > 0 by XREAL_1:60;
thus 1 / (n -root a) = 1 / (- (n -root (- a))) by A6, Th11
.= - (1 / (n -root (- a))) by XCMPLX_1:189
.= - (n -root (1 / (- a))) by A2, A7, A11
.= - (n -root (- (1 / a))) by XCMPLX_1:189
.= n -root (1 / a) by A6, Th11 ; :: 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