let
a
be
Integer
;
:: thesis:
(
a
=
0
or
absreal
.
a
>=
1 )
assume
A1
:
a
<>
0
;
:: thesis:
absreal
.
a
>=
1
per
cases
(
0
<=
a
or
a
<
0
)
;
suppose
0
<=
a
;
:: thesis:
absreal
.
a
>=
1
then
reconsider
a
=
a
as
Element
of
NAT
by
INT_1:3
;
A2
:
absreal
.
a
=
.
a
.
by
EUCLID:def 2
.=
a
by
ABSVALUE:def 1
;
0
+
1
<
a
+
1
by
A1
,
XREAL_1:6
;
hence
absreal
.
a
>=
1
by
A2
,
NAT_1:13
;
:: thesis:
verum
end;
suppose
A3
:
a
<
0
;
:: thesis:
absreal
.
a
>=
1
then
a
<=

1
by
INT_1:8
;
then
A4
:

(

1
)
<=

a
by
XREAL_1:24
;
absreal
.
a
=
.
a
.
by
EUCLID:def 2
.=

a
by
A3
,
ABSVALUE:def 1
;
hence
absreal
.
a
>=
1
by
A4
;
:: thesis:
verum
end;
end;