let i, j be Integer; :: thesis: ( 0 < i & 1 < j implies i div j < i )
assume that
A1: 0 < i and
A2: 1 < j ; :: thesis: i div j < i
assume A3: i <= i div j ; :: thesis: contradiction
i div j <= i / j by Def6;
then j * (i div j) <= j * (i / j) by A2, XREAL_1:64;
then j * (i div j) <= i by A2, XCMPLX_1:87;
then j * (i div j) <= i div j by A3, XXREAL_0:2;
then (j * (i div j)) * ((i div j) ") <= (i div j) * ((i div j) ") by A1, A3, XREAL_1:64;
then j * ((i div j) * ((i div j) ")) <= (i div j) * ((i div j) ") ;
then j * 1 <= (i div j) * ((i div j) ") by A1, A3, XCMPLX_0:def 7;
hence contradiction by A1, A2, A3, XCMPLX_0:def 7; :: thesis: verum