let r be Real; :: thesis: ( 0 < r implies ex m being Nat st

( not m is zero & 1 / m < r ) )

assume A1: 0 < r ; :: thesis: ex m being Nat st

( not m is zero & 1 / m < r )

consider m being Nat such that

A2: 1 / r < m by SEQ_4:3;

A3: 0 < m by A1, A2;

take m ; :: thesis: ( not m is zero & 1 / m < r )

thus not m is zero by A1, A2; :: thesis: 1 / m < r

(1 / r) * r < m * r by A2, A1, XREAL_1:68;

then 1 < m * r by A1, XCMPLX_1:106;

then 1 / m < (m * r) / m by A3, XREAL_1:74;

then 1 / m < r * (m / m) by XCMPLX_1:74;

hence 1 / m < r by A3, XCMPLX_1:88; :: thesis: verum

( not m is zero & 1 / m < r ) )

assume A1: 0 < r ; :: thesis: ex m being Nat st

( not m is zero & 1 / m < r )

consider m being Nat such that

A2: 1 / r < m by SEQ_4:3;

A3: 0 < m by A1, A2;

take m ; :: thesis: ( not m is zero & 1 / m < r )

thus not m is zero by A1, A2; :: thesis: 1 / m < r

(1 / r) * r < m * r by A2, A1, XREAL_1:68;

then 1 < m * r by A1, XCMPLX_1:106;

then 1 / m < (m * r) / m by A3, XREAL_1:74;

then 1 / m < r * (m / m) by XCMPLX_1:74;

hence 1 / m < r by A3, XCMPLX_1:88; :: thesis: verum