per cases ( r > 0 or r < 0 ) ;

suppose r > 0 ; :: thesis: r |^ n is positive

then r |^ n > 0 by PREPOWER:6;
hence r |^ n is positive ; :: thesis: verum

end;

suppose r < 0 ; :: thesis: r |^ n is positive

then A1: ( |.r.| = - r & - r > 0 ) by ABSVALUE:def 1;
then r |^ n = ((- 1) * |.r.|) |^ n
.= ((- 1) ^ n) * (|.r.| |^ n) by NEWTON:7
.= (1 * |.r.|) ^ n ;
hence r |^ n is positive by A1, PREPOWER:6; :: thesis: verum

end;

end;