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;