defpred S₁[ Integer] means ( ( m = 0 implies n div m = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies n div m = idiv1_prg n,m ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( $1 = idiv1_prg n,(- m) & ( (- m) * $1 = n implies n div m = - $1 ) & ( (- m) * $1 <> n implies n div m = (- $1) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( $1 = idiv1_prg (- n),m & ( m * $1 = - n implies n div m = - $1 ) & ( m * $1 <> - n implies n div m = (- $1) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies n div m = idiv1_prg (- n),(- m) ) ) ) ) ) ) ) );

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

suppose m = 0 ; :: thesis: ex b₁, i being Integer st
( ( m = 0 implies b₁ = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies b₁ = idiv1_prg n,m ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( i = idiv1_prg n,(- m) & ( (- m) * i = n implies b₁ = - i ) & ( (- m) * i <> n implies b₁ = (- i) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( i = idiv1_prg (- n),m & ( m * i = - n implies b₁ = - i ) & ( m * i <> - n implies b₁ = (- i) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies b₁ = idiv1_prg (- n),(- m) ) ) ) ) ) ) ) )

hence ex b₁, i being Integer st
( ( m = 0 implies b₁ = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies b₁ = idiv1_prg n,m ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( i = idiv1_prg n,(- m) & ( (- m) * i = n implies b₁ = - i ) & ( (- m) * i <> n implies b₁ = (- i) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( i = idiv1_prg (- n),m & ( m * i = - n implies b₁ = - i ) & ( m * i <> - n implies b₁ = (- i) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies b₁ = idiv1_prg (- n),(- m) ) ) ) ) ) ) ) ) ; :: thesis: verum

end;

suppose A1: m <> 0 ; :: thesis: ex b₁, i being Integer st
( ( m = 0 implies b₁ = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies b₁ = idiv1_prg n,m ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( i = idiv1_prg n,(- m) & ( (- m) * i = n implies b₁ = - i ) & ( (- m) * i <> n implies b₁ = (- i) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( i = idiv1_prg (- n),m & ( m * i = - n implies b₁ = - i ) & ( m * i <> - n implies b₁ = (- i) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies b₁ = idiv1_prg (- n),(- m) ) ) ) ) ) ) ) )

now

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

case A2: n >= 0 ; :: thesis: ex i being Integer st S₁[i]

now

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

case m > 0 ; :: thesis: ex i being Integer st S₁[i]

then S₁[ idiv1_prg n,m] by A2, Th10;
hence ex i being Integer st S₁[i] ; :: thesis: verum

end;

case A3: m < 0 ; :: thesis: ex i being Integer st S₁[i]

then A4: - m > 0 by XREAL_1:60;
then reconsider n2 = n, m2 = - m as Element of NAT by A2, INT_1:16;

now

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

case A5: (- m) * (idiv1_prg n,(- m)) = n ; :: thesis: ex i being Integer st S₁[i]

A6: idiv1_prg n,(- m) = n div (- m) by A2, A4, Th10;
then n div m = - (n2 div m2) by A3, A5, Th11;
hence ex i being Integer st S₁[i] by A3, A5, A6; :: thesis: verum

end;

case A7: (- m) * (idiv1_prg n,(- m)) <> n ; :: thesis: ex i being Integer st S₁[i]

A8: idiv1_prg n,(- m) = n div (- m) by A2, A4, Th10;
then n div m = (- (n2 div m2)) - 1 by A3, A7, Th11;
hence ex i being Integer st S₁[i] by A3, A7, A8; :: thesis: verum

end;

end;

end;

hence ex i being Integer st S₁[i] ; :: thesis: verum

end;

end;

end;

hence ex i being Integer st S₁[i] ; :: thesis: verum

end;

case A9: n < 0 ; :: thesis: ex i being Integer st S₁[i]

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

now

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

case m < 0 ; :: thesis: ex i being Integer st S₁[i]

then A12: - m > 0 by XREAL_1:60;
n div m = [\(n / m)/] by INT_1:def 7
.= [\((- n) / (- m))/] by XCMPLX_1:192
.= (- n) div (- m) by INT_1:def 7 ;
then S₁[ idiv1_prg (- n),(- m)] by A9, A12, Th10;
hence ex i being Integer st S₁[i] ; :: thesis: verum

end;

case A13: m > 0 ; :: thesis: ex i being Integer st S₁[i]

then reconsider n2 = - n, m2 = m as Element of NAT by A10, INT_1:16;

now

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

case A14: m * (idiv1_prg (- n),m) = - n ; :: thesis: ex i being Integer st S₁[i]

A15: idiv1_prg (- n),m = (- n) div m by A10, A13, Th10;
then n div m = - (n2 div m2) by A9, A13, A14, Th11;
hence ex i being Integer st S₁[i] by A9, A13, A14, A15; :: thesis: verum

end;

case A16: m * (idiv1_prg (- n),m) <> - n ; :: thesis: ex i being Integer st S₁[i]

A17: idiv1_prg (- n),m = (- n) div m by A10, A13, Th10;
then n div m = (- (n2 div m2)) - 1 by A9, A13, A16, Th11;
hence ex i being Integer st S₁[i] by A9, A13, A16, A17; :: thesis: verum

end;

end;

end;

hence ex i being Integer st S₁[i] ; :: thesis: verum

end;

end;

end;

hence ex i being Integer st S₁[i] ; :: thesis: verum

end;

end;

end;

hence ex b₁, i being Integer st
( ( m = 0 implies b₁ = 0 ) & ( not m = 0 implies ( ( n >= 0 & m > 0 implies b₁ = idiv1_prg n,m ) & ( ( not n >= 0 or not m > 0 ) implies ( ( n >= 0 & m < 0 implies ( i = idiv1_prg n,(- m) & ( (- m) * i = n implies b₁ = - i ) & ( (- m) * i <> n implies b₁ = (- i) - 1 ) ) ) & ( ( not n >= 0 or not m < 0 ) implies ( ( n < 0 & m > 0 implies ( i = idiv1_prg (- n),m & ( m * i = - n implies b₁ = - i ) & ( m * i <> - n implies b₁ = (- i) - 1 ) ) ) & ( ( not n < 0 or not m > 0 ) implies b₁ = idiv1_prg (- n),(- m) ) ) ) ) ) ) ) ) ; :: thesis: verum

end;

end;