let n, m be Integer; :: thesis: for n2, m2 being Element of NAT holds
( ( m = 0 & n2 = n & m2 = m implies ( n div m = 0 & n2 div m2 = 0 ) ) & ( n >= 0 & m > 0 & n2 = n & m2 = m implies n div m = n2 div m2 ) & ( n >= 0 & m < 0 & n2 = n & m2 = - m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m > 0 & n2 = - n & m2 = m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m < 0 & n2 = - n & m2 = - m implies n div m = n2 div m2 ) )
let n2, m2 be Element of NAT ; :: thesis: ( ( m = 0 & n2 = n & m2 = m implies ( n div m = 0 & n2 div m2 = 0 ) ) & ( n >= 0 & m > 0 & n2 = n & m2 = m implies n div m = n2 div m2 ) & ( n >= 0 & m < 0 & n2 = n & m2 = - m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m > 0 & n2 = - n & m2 = m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m < 0 & n2 = - n & m2 = - m implies n div m = n2 div m2 ) )
thus ( m = 0 & n2 = n & m2 = m implies ( n div m = 0 & n2 div m2 = 0 ) ) ; :: thesis: ( ( n >= 0 & m > 0 & n2 = n & m2 = m implies n div m = n2 div m2 ) & ( n >= 0 & m < 0 & n2 = n & m2 = - m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m > 0 & n2 = - n & m2 = m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m < 0 & n2 = - n & m2 = - m implies n div m = n2 div m2 ) )
thus ( n >= 0 & m > 0 & n2 = n & m2 = m implies n div m = n2 div m2 ) ; :: thesis: ( ( n >= 0 & m < 0 & n2 = n & m2 = - m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m > 0 & n2 = - n & m2 = m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m < 0 & n2 = - n & m2 = - m implies n div m = n2 div m2 ) )
thus ( n >= 0 & m < 0 & n2 = n & m2 = - m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) :: thesis: ( ( n < 0 & m > 0 & n2 = - n & m2 = m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) & ( n < 0 & m < 0 & n2 = - n & m2 = - m implies n div m = n2 div m2 ) )

proof

assume that
n >= 0 and
A1: m < 0 and
A2: n2 = n and
A3: m2 = - m ; :: thesis: ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) )
thus ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) :: thesis: ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 )

proof

assume A4: m2 * (n2 div m2) = n2 ; :: thesis: n div m = - (n2 div m2)
m2 > 0 by A1, A3, XREAL_1:58;
then A6: n2 = (m2 * (n2 div m2)) + (n2 mod m2) by NAT_D:2;
thus n div m = [\(n / m)/] by INT_1:def 9
.= [\((- n) / (- m))/] by XCMPLX_1:191
.= (- n2) div m2 by A2, A3, INT_1:def 9
.= - (n2 div m2) by A4, A6, WSIERP_1:42 ; :: thesis: verum

end;

thus ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) :: thesis: verum

proof

assume A7: m2 * (n2 div m2) <> n2 ; :: thesis: n div m = (- (n2 div m2)) - 1
A8: m2 > 0 by A1, A3, XREAL_1:58;
then n2 = (m2 * (n2 div m2)) + (n2 mod m2) by NAT_D:2;
then not n2 mod m2 = 0 by A7;
then A9: ((- n2) div m2) + 1 = - (n2 div m2) by A8, WSIERP_1:41;
n div m = [\(n / m)/] by INT_1:def 9
.= [\((- n) / (- m))/] by XCMPLX_1:191
.= (- n2) div m2 by A2, A3, INT_1:def 9 ;
hence n div m = (- (n2 div m2)) - 1 by A9; :: thesis: verum

end;

end;

thus ( n < 0 & m > 0 & n2 = - n & m2 = m implies ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) ) ) :: thesis: ( n < 0 & m < 0 & n2 = - n & m2 = - m implies n div m = n2 div m2 )

proof

assume that
n < 0 and
A10: m > 0 and
A11: n2 = - n and
A12: m2 = m ; :: thesis: ( ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) & ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) )
thus ( m2 * (n2 div m2) = n2 implies n div m = - (n2 div m2) ) :: thesis: ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 )

proof

A13: n2 = (m2 * (n2 div m2)) + (n2 mod m2) by A10, A12, NAT_D:2;
assume A14: m2 * (n2 div m2) = n2 ; :: thesis: n div m = - (n2 div m2)
n div m = (- n2) div m by A11
.= - (n2 div m2) by A12, A14, A13, WSIERP_1:42 ;
hence n div m = - (n2 div m2) ; :: thesis: verum

end;

thus ( m2 * (n2 div m2) <> n2 implies n div m = (- (n2 div m2)) - 1 ) :: thesis: verum

proof

assume A15: m2 * (n2 div m2) <> n2 ; :: thesis: n div m = (- (n2 div m2)) - 1
n2 = (m2 * (n2 div m2)) + (n2 mod m2) by A10, A12, NAT_D:2;
then not n2 mod m2 = 0 by A15;
then ((- n2) div m2) + 1 = - (n2 div m2) by A10, A12, WSIERP_1:41;
hence n div m = (- (n2 div m2)) - 1 by A11, A12; :: thesis: verum

end;

end;

thus ( n < 0 & m < 0 & n2 = - n & m2 = - m implies n div m = n2 div m2 ) :: thesis: verum

proof

assume that
n < 0 and
m < 0 and
A16: ( n2 = - n & m2 = - m ) ; :: thesis: n div m = n2 div m2
thus n div m = [\(n / m)/] by INT_1:def 9
.= [\((- n) / (- m))/] by XCMPLX_1:191
.= n2 div m2 by A16, INT_1:def 9 ; :: thesis: verum

end;