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, INT_1:75; :: thesis: verum

end;

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

now

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

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

now

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

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

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

end;

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

A10: - m > 0 by A5, XREAL_1:60;
then reconsider m2 = - m, n2 = n as Element of NAT by A3, INT_1:16;
A11: idiv_prg n,m = (- (idiv1_prg n,(- m))) - 1 by A3, A5, A9, Def2;
idiv1_prg n,(- m) = n2 div m2 by A10, Th9;
hence idiv_prg n,m = n div m by A5, A9, A11, 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 A12: n < 0 ; :: thesis: idiv_prg n,m = n div m

then A13: - n > 0 by XREAL_1:60;

now

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

case A14: m < 0 ; :: thesis: idiv_prg n,m = n div m

then A15: - m > 0 by XREAL_1:60;
A16: idiv_prg n,m = idiv1_prg (- n),(- m) by A12, A14, Def2
.= (- n) div (- m) by A13, A15, Th10 ;
n div m = [\(n / m)/] by INT_1:def 7
.= [\((- n) / (- m))/] by XCMPLX_1:192
.= (- n) div (- m) by INT_1:def 7 ;
hence idiv_prg n,m = n div m by A16; :: thesis: verum

end;

case A17: m > 0 ; :: thesis: idiv_prg n,m = n div m

now

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

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

reconsider m2 = m, n2 = - n as Element of NAT by A13, A17, INT_1:16;
A19: idiv_prg n,m = - (idiv1_prg (- n),m) by A12, A17, A18, Def2;
idiv1_prg (- n),m = n2 div m2 by A17, Th9;
hence idiv_prg n,m = n div m by A12, A17, A18, A19, Th11; :: thesis: verum

end;

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

reconsider m2 = m, n2 = - n as Element of NAT by A13, A17, INT_1:16;
A21: idiv_prg n,m = (- (idiv1_prg (- n),m)) - 1 by A12, A17, A20, Def2;
idiv1_prg (- n),m = n2 div m2 by A17, Th9;
hence idiv_prg n,m = n div m by A12, A17, A20, A21, 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;