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 ) ) by INT_1:75; :: 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 A1: ( n >= 0 & m < 0 & n2 = n & 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 A2: m2 * (n2 div m2) = n2 ; :: thesis: n div m = - (n2 div m2)
A3: m2 > 0 by A1, XREAL_1:60;
then A4: n2 = (m2 * (n2 div m2)) + (n2 mod m2) by NAT_D:2;
thus n div m = [\(n / m)/] by INT_1:def 7
.= [\((- n) / (- m))/] by XCMPLX_1:192
.= (- n2) div m2 by A1, INT_1:def 7
.= - (n2 div m2) by A2, A3, A4, WSIERP_1:50 ; :: thesis: verum

end;

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

proof

assume A5: m2 * (n2 div m2) <> n2 ; :: thesis: n div m = (- (n2 div m2)) - 1
A6: m2 > 0 by A1, XREAL_1:60;
then n2 = (m2 * (n2 div m2)) + (n2 mod m2) by NAT_D:2;
then A7: not n2 mod m2 = 0 by A5;
A8: n div m = [\(n / m)/] by INT_1:def 7
.= [\((- n) / (- m))/] by XCMPLX_1:192
.= (- n2) div m2 by A1, INT_1:def 7 ;
((- n2) div m2) + 1 = - (n2 div m2) by A6, A7, WSIERP_1:49;
hence n div m = (- (n2 div m2)) - 1 by A8; :: 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 A9: ( n < 0 & m > 0 & n2 = - n & 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 A10: m2 * (n2 div m2) = n2 ; :: thesis: n div m = - (n2 div m2)
A11: n2 = (m2 * (n2 div m2)) + (n2 mod m2) by A9, NAT_D:2;
n div m = (- n2) div m by A9
.= - (n2 div m2) by A9, A10, A11, WSIERP_1:50 ;
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 A12: m2 * (n2 div m2) <> n2 ; :: thesis: n div m = (- (n2 div m2)) - 1
n2 = (m2 * (n2 div m2)) + (n2 mod m2) by A9, NAT_D:2;
then not n2 mod m2 = 0 by A12;
then ((- n2) div m2) + 1 = - (n2 div m2) by A9, WSIERP_1:49;
hence n div m = (- (n2 div m2)) - 1 by A9; :: thesis: verum

end;

end;

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

proof

assume A13: ( n < 0 & m < 0 & n2 = - n & m2 = - m ) ; :: thesis: n div m = n2 div m2
thus n div m = [\(n / m)/] by INT_1:def 7
.= [\((- n) / (- m))/] by XCMPLX_1:192
.= n2 div m2 by A13, INT_1:def 7 ; :: thesis: verum

end;