:: deftheorem Def2 defines idiv_prg PRGCOR_1:def 2 :
for n, m, b₃ being Integer holds
( b₃ = idiv_prg (n,m) iff ex 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)) ) ) ) ) ) ) ) ) );