let a, b be natural number ; :: thesis: ( b <> 0 implies ex k being Element of NAT st
( k * b <= a & a < (k + 1) * b ) )
assume A1: b <> 0 ; :: thesis: ex k being Element of NAT st
( k * b <= a & a < (k + 1) * b )
set k' = a div b;
consider t being Nat such that
A2: ( a = (b * (a div b)) + t & t < b ) by A1, NAT_D:def 1;
((a div b) + 1) * b = ((a div b) * b) + b ;
then ((a div b) + 1) * b > a by A2, XREAL_1:8;
hence ex k being Element of NAT st
( k * b <= a & a < (k + 1) * b ) by A2, NAT_1:11; :: thesis: verum