let n be Element of NAT ; :: thesis: ( ex m being Element of NAT st n = (2 * m) + 1 implies n -root (- 1) = - 1 )
assume A1: ex m being Element of NAT st n = (2 * m) + 1 ; :: thesis: n -root (- 1) = - 1
A2: n >= 0 + 1 by A1, XREAL_1:8;
thus n -root (- 1) = - (n -Root (- (- 1))) by A1, Def1
.= - 1 by A2, PREPOWER:29 ; :: thesis: verum