let a be Real; :: thesis: ( ( a is heavy & a is negative implies a < - 1 ) & ( a < - 1 implies ( a is heavy & a is negative ) ) & ( a is light & a is negative implies ( - 1 < a & a < 0 ) ) & ( - 1 < a & a < 0 implies ( a is light & a is negative ) ) & ( a is light & a is positive implies ( 0 < a & a < 1 ) ) & ( 0 < a & a < 1 implies ( a is light & a is positive ) ) & ( a is heavy & a is positive implies a > 1 ) & ( a > 1 implies ( a is heavy & a is positive ) ) & ( a is weightless & a is positive implies a = 1 ) & ( a = 1 implies ( a is weightless & a is positive ) ) & ( a is weightless & a is negative implies a = - 1 ) & ( a = - 1 implies ( a is weightless & a is negative ) ) )
A1: ( a is heavy & a is negative implies a < - 1 )
proof
assume ( a is heavy & a is negative ) ; :: thesis: a < - 1
then - a > 1 by ABSVALUE:def 1;
then - (- a) < - 1 by XREAL_1:24;
hence a < - 1 ; :: thesis: verum
end;
A1a: ( a < - 1 implies ( a is heavy & a is negative ) )
proof
assume B1: a < - 1 ; :: thesis: ( a is heavy & a is negative )
then - a > - (- 1) by XREAL_1:24;
hence ( a is heavy & a is negative ) by B1, ABSVALUE:def 1; :: thesis: verum
end;
A3: ( a is light & a is negative implies ( - 1 < a & a < 0 ) )
proof
assume B1: ( a is light & a is negative ) ; :: thesis: ( - 1 < a & a < 0 )
then - a < 1 by ABSVALUE:def 1;
then - (- a) > - 1 by XREAL_1:24;
hence ( - 1 < a & a < 0 ) by B1; :: thesis: verum
end;
A3a: ( - 1 < a & a < 0 implies ( a is light & a is negative ) )
proof
assume B1: ( - 1 < a & a < 0 ) ; :: thesis: ( a is light & a is negative )
then - a < - (- 1) by XREAL_1:24;
hence ( a is light & a is negative ) by B1, ABSVALUE:def 1; :: thesis: verum
end;
( not a is weightless or a = 0 or 1 = a or 1 = - a ) by ABSVALUE:1;
hence ( ( a is heavy & a is negative implies a < - 1 ) & ( a < - 1 implies ( a is heavy & a is negative ) ) & ( a is light & a is negative implies ( - 1 < a & a < 0 ) ) & ( - 1 < a & a < 0 implies ( a is light & a is negative ) ) & ( a is light & a is positive implies ( 0 < a & a < 1 ) ) & ( 0 < a & a < 1 implies ( a is light & a is positive ) ) & ( a is heavy & a is positive implies a > 1 ) & ( a > 1 implies ( a is heavy & a is positive ) ) & ( a is weightless & a is positive implies a = 1 ) & ( a = 1 implies ( a is weightless & a is positive ) ) & ( a is weightless & a is negative implies a = - 1 ) & ( a = - 1 implies ( a is weightless & a is negative ) ) ) by A1, A1a, ABSVALUE:def 1, A3, A3a; :: thesis: verum