let i1, i2 be Integer; :: thesis: ( i1 * i2 = 1 iff ( ( i1 = 1 & i2 = 1 ) or ( i1 = - 1 & i2 = - 1 ) ) )
thus ( not i1 * i2 = 1 or ( i1 = 1 & i2 = 1 ) or ( i1 = - 1 & i2 = - 1 ) ) :: thesis: ( ( ( i1 = 1 & i2 = 1 ) or ( i1 = - 1 & i2 = - 1 ) ) implies i1 * i2 = 1 )
proof
assume A1: i1 * i2 = 1 ; :: thesis: ( ( i1 = 1 & i2 = 1 ) or ( i1 = - 1 & i2 = - 1 ) )
then A2: not i2 = 0 ;
A3: now :: thesis: ( i1 < 0 & i2 < 0 implies ( i1 = - 1 & i2 = - 1 ) )
A4: (- i1) * (- i2) = i1 * i2 ;
assume that
A5: i1 < 0 and
A6: i2 < 0 ; :: thesis: ( i1 = - 1 & i2 = - 1 )
A7: - i2 is Element of NAT by A6, Th3;
- i1 is Element of NAT by A5, Th3;
then - (- i1) = - 1 by A1, A7, A4, NAT_1:15;
hence ( i1 = - 1 & i2 = - 1 ) by A1; :: thesis: verum
end;
A8: now :: thesis: ( 0 < i1 & 0 < i2 implies ( i1 = 1 & i2 = 1 ) )
assume that
A9: 0 < i1 and
A10: 0 < i2 ; :: thesis: ( i1 = 1 & i2 = 1 )
A11: i2 is Element of NAT by A10, Th3;
i1 is Element of NAT by A9, Th3;
hence ( i1 = 1 & i2 = 1 ) by A1, A11, NAT_1:15; :: thesis: verum
end;
not i1 = 0 by A1;
hence ( ( i1 = 1 & i2 = 1 ) or ( i1 = - 1 & i2 = - 1 ) ) by A1, A2, A8, A3; :: thesis: verum
end;
thus ( ( ( i1 = 1 & i2 = 1 ) or ( i1 = - 1 & i2 = - 1 ) ) implies i1 * i2 = 1 ) ; :: thesis: verum