let
a
be
Real
;
:: thesis:
for
k
being
Integer
st
a
>
0
holds
a
#Z
k
>
0
let
k
be
Integer
;
:: thesis:
(
a
>
0
implies
a
#Z
k
>
0
)
assume
A1
:
a
>
0
;
:: thesis:
a
#Z
k
>
0
per
cases
(
k
>=
0
or
k
<
0
)
;
suppose
k
>=
0
;
:: thesis:
a
#Z
k
>
0
then
a
#Z
k
=
a
|^
|.
k
.|
by
Def3
;
hence
a
#Z
k
>
0
by
A1
,
Th6
;
:: thesis:
verum
end;
suppose
A2
:
k
<
0
;
:: thesis:
a
#Z
k
>
0
A3
:
a
|^
|.
k
.|
>
0
by
A1
,
Th6
;
a
#Z
k
=
(
a
|^
|.
k
.|
)
"
by
A2
,
Def3
;
hence
a
#Z
k
>
0
by
A3
;
:: thesis:
verum
end;
end;