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 :: thesis: ( ( n >= 0 & ex i being Integer st S₁[i] ) or ( n < 0 & ex i being Integer st S₁[i] ) )

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

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

now :: thesis: ( ( m > 0 & ex i being Integer st S₁[i] ) or ( m < 0 & ex i being Integer st S₁[i] ) )

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 reconsider n2 = n, m2 = - m as Element of NAT by A2, INT_1:3;
A4: - m > 0 by A3, XREAL_1:58;

now :: thesis: ( ( (- m) * (idiv1_prg (n,(- m))) = n & ex i being Integer st S₁[i] ) or ( (- m) * (idiv1_prg (n,(- m))) <> n & ex i being Integer st S₁[i] ) )

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]

now :: thesis: ( ( m < 0 & ex i being Integer st S₁[i] ) or ( m > 0 & ex i being Integer st S₁[i] ) )

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

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

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

end;

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

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

now :: thesis: ( ( m * (idiv1_prg ((- n),m)) = - n & ex i being Integer st S₁[i] ) or ( m * (idiv1_prg ((- n),m)) <> - n & ex i being Integer st S₁[i] ) )

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

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

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

end;

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

A16: idiv1_prg ((- n),m) = (- n) div m by A9, A12, Th10;
then n div m = (- (n2 div m2)) - 1 by A9, A12, A15, Th11;
hence ex i being Integer st S₁[i] by A9, A12, A15, A16; :: 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;