let
l
be
Integer
;
:: thesis:
(
l
<>
0
implies
0
#Z
l
=
0
)
assume
A1
:
l
<>
0
;
:: thesis:
0
#Z
l
=
0
per
cases
(
l
>
0
or
l
<
0
)
by
A1
;
suppose
A2
:
l
>
0
;
:: thesis:
0
#Z
l
=
0
then
reconsider
l
=
l
as
Element
of
NAT
by
INT_1:3
;
l
>=
0
+
1
by
A2
,
NAT_1:13
;
then
A3
:
0
^
l
=
0
by
NEWTON:11
;
.
l
.
=
l
by
ABSVALUE:def 1
;
hence
0
#Z
l
=
0
by
A3
,
Def3
;
:: thesis:
verum
end;
suppose
A4
:
l
<
0
;
:: thesis:
0
#Z
l
=
0
then
reconsider
k
=

l
as
Element
of
NAT
by
INT_1:3
;
k
>

0
by
A4
;
then
k
>=
0
+
1
by
NAT_1:13
;
then
A5
:
0
^
k
=
0
by
NEWTON:11
;
.
l
.
=
k
by
A4
,
ABSVALUE:def 1
;
then
(
0
^
.
l
.
)
"
=
0
by
A5
;
hence
0
#Z
l
=
0
by
A4
,
Def3
;
:: thesis:
verum
end;
end;