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

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