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:3;
assume p > 0 ; :: thesis: ex i being Element of NAT st
( 1 / (i + 1) < p & i >= m )
then A2: 0 < p " by XREAL_1:122;
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:8;
then 1 / (i + 1) < 1 / (p ") by A2, XREAL_1:76;
hence ( 1 / (i + 1) < p & i >= m ) by NAT_1:11, XCMPLX_1:216; :: thesis: verum