let k be Nat; :: thesis: for j being Integer st k <> 0 & [\(j / k)/] + 1 >= j / k holds
k >= j - ([\(j / k)/] * k)
let j be Integer; :: thesis: ( k <> 0 & [\(j / k)/] + 1 >= j / k implies k >= j - ([\(j / k)/] * k) )
assume that
A1: k <> 0 and
A2: [\(j / k)/] + 1 >= j / k ; :: thesis: k >= j - ([\(j / k)/] * k)
([\(j / k)/] + 1) + (- 1) >= (j / k) + (- 1) by A2, XREAL_1:6;
then [\(j / k)/] * k >= ((j / k) - 1) * k by XREAL_1:64;
then - (((j / k) - 1) * k) >= - ([\(j / k)/] * k) by XREAL_1:24;
then j + (- (((j / k) - 1) * k)) >= j + (- ([\(j / k)/] * k)) by XREAL_1:6;
then j - (((j / k) * k) - (1 * k)) >= j - ([\(j / k)/] * k) ;
then j - (j - k) >= j - ([\(j / k)/] * k) by A1, XCMPLX_1:87;
hence k >= j - ([\(j / k)/] * k) ; :: thesis: verum