let n, m be Integer; idiv_prg (n,m) = n div m
per cases
( m = 0 or m <> 0 )
;
suppose A2:
m <> 0
;
idiv_prg (n,m) = n div mnow ( ( 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
;
idiv_prg (n,m) = n div mnow ( ( 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 A5:
m < 0
;
idiv_prg (n,m) = n div mnow ( ( (- 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
;
idiv_prg (n,m) = n div mreconsider 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;
verum end; case A8:
(- m) * (idiv1_prg (n,(- m))) <> n
;
idiv_prg (n,m) = n div mreconsider 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;
verum end; end; end; hence
idiv_prg (
n,
m)
= n div m
;
verum end; end; end; hence
idiv_prg (
n,
m)
= n div m
;
verum end; case A10:
n < 0
;
idiv_prg (n,m) = n div mnow ( ( 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 A14:
m > 0
;
idiv_prg (n,m) = n div mnow ( ( 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
;
idiv_prg (n,m) = n div mreconsider 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;
verum end; case A17:
m * (idiv1_prg ((- n),m)) <> - n
;
idiv_prg (n,m) = n div mreconsider 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;
verum end; end; end; hence
idiv_prg (
n,
m)
= n div m
;
verum end; end; end; hence
idiv_prg (
n,
m)
= n div m
;
verum end; end; end; hence
idiv_prg (
n,
m)
= n div m
;
verum end; end;