let a be Integer; :: thesis: for b being non zero Integer st [\(a / b)/] = - [\(- (a / b))/] holds
b divides a
let b be non zero Integer; :: thesis: ( [\(a / b)/] = - [\(- (a / b))/] implies b divides a )
assume A1: [\(a / b)/] = - [\(- (a / b))/] ; :: thesis: b divides a
0 = ([\(a / b)/] + [\(- (a / b))/]) + (sgn (frac (a / b))) by FL
.= sgn (frac (a / b)) by A1 ;
then reconsider x = a / b as Integer ;
a = x * b by XCMPLX_1:87;
hence b divides a ; :: thesis: verum