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 )
per cases ( a >= 0 or a < 0 ) ;
suppose A2: a >= 0 ; :: thesis: ex q, r being Integer st
( 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;
suppose A5: a < 0 ; :: thesis: ex q, r being Integer st
( 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;
per cases ( t = 0 or t <> 0 ) ;
suppose A9: t = 0 ; :: thesis: ex q, r being Integer st
( 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;
suppose A10: t <> 0 ; :: thesis: ex q, r being Integer st
( 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;
end;
end;
end;