let i1, i2 be Integer; ( 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 ) )
( ( ( i1 = - 1 & i2 = 1 ) or ( i1 = 1 & i2 = - 1 ) ) implies i1 * i2 = - 1 )proof
assume
i1 * i2 = - 1
;
( ( i1 = - 1 & i2 = 1 ) or ( i1 = 1 & i2 = - 1 ) )
then
(- i1) * i2 = 1
;
then
( (
- (- i1) = - 1 &
i2 = 1 ) or (
- i1 = - 1 &
i2 = - 1 ) )
by Th9;
hence
( (
i1 = - 1 &
i2 = 1 ) or (
i1 = 1 &
i2 = - 1 ) )
;
verum
end;
assume
( ( i1 = - 1 & i2 = 1 ) or ( i1 = 1 & i2 = - 1 ) )
; i1 * i2 = - 1
hence
i1 * i2 = - 1
; verum