let p be Real; :: thesis: for m being Nat st p > 0 holds
ex i being Nat st
( 1 / (i + 1) < p & i >= m )
let m be Nat; :: thesis: ( p > 0 implies ex i being Nat st
( 1 / (i + 1) < p & i >= m ) )
consider k1 being Nat such that
A1: p " < k1 by SEQ_4:3;
assume p > 0 ; :: thesis: ex i being Nat st
( 1 / (i + 1) < p & i >= m )
then A2: 0 < p " ;
reconsider i = k1 + m as Nat ;
take i ; :: 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