let n, m be Integer; :: thesis: idiv_prg (n,m) = n div m

per cases ( m = 0 or m <> 0 ) ;

suppose A1: m = 0 ; :: thesis: idiv_prg (n,m) = n div m

then idiv_prg (n,m) = 0 by Def2;
hence idiv_prg (n,m) = n div m by A1; :: thesis: verum

end;

suppose A2: m <> 0 ; :: thesis: idiv_prg (n,m) = n div m

now :: thesis: ( ( n >= 0 & idiv_prg (n,m) = n div m ) or ( n < 0 & idiv_prg (n,m) = n div m ) )

per cases ( n >= 0 or n < 0 ) ;

case A3: n >= 0 ; :: thesis: idiv_prg (n,m) = n div m

now :: thesis: ( ( m > 0 & idiv_prg (n,m) = n div m ) or ( m < 0 & idiv_prg (n,m) = n div m ) )

per cases ( m > 0 or m < 0 ) by A2;

case A4: m > 0 ; :: thesis: idiv_prg (n,m) = n div m

hence idiv_prg (n,m) = idiv1_prg (n,m) by A3, Def2
.= n div m by A3, A4, Th10 ;
:: thesis: verum

end;

case A5: m < 0 ; :: thesis: idiv_prg (n,m) = n div m

now :: thesis: ( ( (- m) * (idiv1_prg (n,(- m))) = n & idiv_prg (n,m) = n div m ) or ( (- m) * (idiv1_prg (n,(- m))) <> n & idiv_prg (n,m) = n div m ) )

per cases ( (- m) * (idiv1_prg (n,(- m))) = n or (- m) * (idiv1_prg (n,(- m))) <> n ) ;

case A6: (- m) * (idiv1_prg (n,(- m))) = n ; :: thesis: idiv_prg (n,m) = n div m

reconsider m2 = - m, n2 = n as Element of NAT by A3, A5, INT_1:3;
- m > 0 by A5, XREAL_1:58;
then A7: idiv1_prg (n,(- m)) = n2 div m2 by Th9;
idiv_prg (n,m) = - (idiv1_prg (n,(- m))) by A3, A5, A6, Def2;
hence idiv_prg (n,m) = n div m by A5, A6, A7, Th11; :: thesis: verum

end;

case A8: (- m) * (idiv1_prg (n,(- m))) <> n ; :: thesis: idiv_prg (n,m) = n div m

reconsider m2 = - m, n2 = n as Element of NAT by A3, A5, INT_1:3;
- m > 0 by A5, XREAL_1:58;
then A9: idiv1_prg (n,(- m)) = n2 div m2 by Th9;
idiv_prg (n,m) = (- (idiv1_prg (n,(- m)))) - 1 by A3, A5, A8, Def2;
hence idiv_prg (n,m) = n div m by A5, A8, A9, Th11; :: thesis: verum

end;

end;

end;

hence idiv_prg (n,m) = n div m ; :: thesis: verum

end;

end;

end;

hence idiv_prg (n,m) = n div m ; :: thesis: verum

end;

case A10: n < 0 ; :: thesis: idiv_prg (n,m) = n div m

now :: thesis: ( ( m < 0 & idiv_prg (n,m) = n div m ) or ( m > 0 & idiv_prg (n,m) = n div m ) )

per cases ( m < 0 or m > 0 ) by A2;

case A11: m < 0 ; :: thesis: idiv_prg (n,m) = n div m

then A12: - m > 0 by XREAL_1:58;
A13: n div m = [\(n / m)/] by INT_1:def 9
.= [\((- n) / (- m))/] by XCMPLX_1:191
.= (- n) div (- m) by INT_1:def 9 ;
idiv_prg (n,m) = idiv1_prg ((- n),(- m)) by A10, A11, Def2
.= (- n) div (- m) by A10, A12, Th10 ;
hence idiv_prg (n,m) = n div m by A13; :: thesis: verum

end;

case A14: m > 0 ; :: thesis: idiv_prg (n,m) = n div m

now :: thesis: ( ( m * (idiv1_prg ((- n),m)) = - n & idiv_prg (n,m) = n div m ) or ( m * (idiv1_prg ((- n),m)) <> - n & idiv_prg (n,m) = n div m ) )

per cases ( m * (idiv1_prg ((- n),m)) = - n or m * (idiv1_prg ((- n),m)) <> - n ) ;

case A15: m * (idiv1_prg ((- n),m)) = - n ; :: thesis: idiv_prg (n,m) = n div m

reconsider m2 = m, n2 = - n as Element of NAT by A10, A14, INT_1:3;
A16: idiv1_prg ((- n),m) = n2 div m2 by A14, Th9;
idiv_prg (n,m) = - (idiv1_prg ((- n),m)) by A10, A14, A15, Def2;
hence idiv_prg (n,m) = n div m by A10, A14, A15, A16, Th11; :: thesis: verum

end;

case A17: m * (idiv1_prg ((- n),m)) <> - n ; :: thesis: idiv_prg (n,m) = n div m

reconsider m2 = m, n2 = - n as Element of NAT by A10, A14, INT_1:3;
A18: idiv1_prg ((- n),m) = n2 div m2 by A14, Th9;
idiv_prg (n,m) = (- (idiv1_prg ((- n),m))) - 1 by A10, A14, A17, Def2;
hence idiv_prg (n,m) = n div m by A10, A14, A17, A18, Th11; :: thesis: verum

end;

end;

end;

hence idiv_prg (n,m) = n div m ; :: thesis: verum

end;

end;

end;

hence idiv_prg (n,m) = n div m ; :: thesis: verum

end;

end;

end;

hence idiv_prg (n,m) = n div m ; :: thesis: verum

end;

end;