let p be real number ; :: thesis: for m being Element of NAT st p > 0 holds
ex i being Element of NAT st
( 1 / (i + 1) < p & i >= m )
let m be Element of NAT ; :: thesis: ( p > 0 implies ex i being Element of NAT st
( 1 / (i + 1) < p & i >= m ) )
consider k1 being Element of NAT such that
A1: p " < k1 by SEQ_4:10;
assume p > 0 ; :: thesis: ex i being Element of NAT st
( 1 / (i + 1) < p & i >= m )
then A2: 0 < p " by XREAL_1:124;
take i = k1 + m; :: thesis: ( 1 / (i + 1) < p & i >= m )
k1 <= k1 + m by NAT_1:11;
then p " < i by A1, XXREAL_0:2;
then (p " ) + 0 < i + 1 by XREAL_1:10;
then 1 / (i + 1) < 1 / (p " ) by A2, XREAL_1:78;
hence ( 1 / (i + 1) < p & i >= m ) by NAT_1:11, XCMPLX_1:218; :: thesis: verum