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;