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
,
Th5
;
:: thesis:
verum
end;
suppose
k
<
0
;
:: thesis:
a
#Z
k
<>
0
then
a
#Z
k
=
(
a
|^
|.
k
.|
)
"
by
Def3
;
hence
a
#Z
k
<>
0
by
A1
,
Th5
,
XCMPLX_1:202
;
:: thesis:
verum
end;
end;