let b be Integer; :: thesis: ( b > 0 implies for a being Integer ex q, r being Integer st

( a = (b * q) + r & r >= 0 & r < b ) )

assume A1: b > 0 ; :: thesis: for a being Integer ex q, r being Integer st

( a = (b * q) + r & r >= 0 & r < b )

let a be Integer; :: thesis: ex q, r being Integer st

( a = (b * q) + r & r >= 0 & r < b )

( a = (b * q) + r & r >= 0 & r < b ) )

assume A1: b > 0 ; :: thesis: for a being Integer ex q, r being Integer st

( a = (b * q) + r & r >= 0 & r < b )

let a be Integer; :: thesis: ex q, r being Integer st

( a = (b * q) + r & r >= 0 & r < b )

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

end;

suppose A2:
a >= 0
; :: thesis: ex q, r being Integer st

( a = (b * q) + r & r >= 0 & r < b )

( a = (b * q) + r & r >= 0 & r < b )

A3:
b in NAT
by A1, INT_1:3;

a in NAT by A2, INT_1:3;

then consider k, t being Nat such that

A4: ( a = (b * k) + t & t < b ) by A1, A3, NAT_1:17;

take k ; :: thesis: ex r being Integer st

( a = (b * k) + r & r >= 0 & r < b )

take t ; :: thesis: ( a = (b * k) + t & t >= 0 & t < b )

thus ( a = (b * k) + t & t >= 0 & t < b ) by A4; :: thesis: verum

end;a in NAT by A2, INT_1:3;

then consider k, t being Nat such that

A4: ( a = (b * k) + t & t < b ) by A1, A3, NAT_1:17;

take k ; :: thesis: ex r being Integer st

( a = (b * k) + r & r >= 0 & r < b )

take t ; :: thesis: ( a = (b * k) + t & t >= 0 & t < b )

thus ( a = (b * k) + t & t >= 0 & t < b ) by A4; :: thesis: verum

suppose A5:
a < 0
; :: thesis: ex q, r being Integer st

( a = (b * q) + r & r >= 0 & r < b )

( a = (b * q) + r & r >= 0 & r < b )

A6:
b in NAT
by A1, INT_1:3;

- a in NAT by A5, INT_1:3;

then consider k, t being Nat such that

A7: - a = (b * k) + t and

A8: t < b by A1, A6, NAT_1:17;

end;- a in NAT by A5, INT_1:3;

then consider k, t being Nat such that

A7: - a = (b * k) + t and

A8: t < b by A1, A6, NAT_1:17;

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

end;

suppose A9:
t = 0
; :: thesis: ex q, r being Integer st

( a = (b * q) + r & r >= 0 & r < b )

( a = (b * q) + r & r >= 0 & r < b )

take q = - k; :: thesis: ex r being Integer st

( a = (b * q) + r & r >= 0 & r < b )

take r = 0 ; :: thesis: ( a = (b * q) + r & r >= 0 & r < b )

a = b * (- k) by A7, A9;

hence a = (b * q) + r ; :: thesis: ( r >= 0 & r < b )

thus ( r >= 0 & r < b ) by A1; :: thesis: verum

end;( a = (b * q) + r & r >= 0 & r < b )

take r = 0 ; :: thesis: ( a = (b * q) + r & r >= 0 & r < b )

a = b * (- k) by A7, A9;

hence a = (b * q) + r ; :: thesis: ( r >= 0 & r < b )

thus ( r >= 0 & r < b ) by A1; :: thesis: verum

suppose A10:
t <> 0
; :: thesis: ex q, r being Integer st

( a = (b * q) + r & r >= 0 & r < b )

( a = (b * q) + r & r >= 0 & r < b )

take q = (- k) - 1; :: thesis: ex r being Integer st

( a = (b * q) + r & r >= 0 & r < b )

take r = b - t; :: thesis: ( a = (b * q) + r & r >= 0 & r < b )

a = (b * ((- k) - 1)) + (b - t) by A7;

hence a = (b * q) + r ; :: thesis: ( r >= 0 & r < b )

thus ( r >= 0 & r < b ) by A8, A10, XREAL_1:44, XREAL_1:50; :: thesis: verum

end;( a = (b * q) + r & r >= 0 & r < b )

take r = b - t; :: thesis: ( a = (b * q) + r & r >= 0 & r < b )

a = (b * ((- k) - 1)) + (b - t) by A7;

hence a = (b * q) + r ; :: thesis: ( r >= 0 & r < b )

thus ( r >= 0 & r < b ) by A8, A10, XREAL_1:44, XREAL_1:50; :: thesis: verum