Theorem climge0

Description: A nonnegative sequence converges to a nonnegative number. (Contributed by NM, 11-Sep-2005) (Proof shortened by Mario Carneiro, 10-May-2016)

	Ref	Expression
Hypotheses	climshft2.1	|- Z = ( ZZ>= ` M )
	climshft2.2	|- ( ph -> M e. ZZ )
	climrecl.3	|- ( ph -> F ~~> A )
	climrecl.4	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
	climge0.5	|- ( ( ph /\ k e. Z ) -> 0 <_ ( F ` k ) )
Assertion	climge0	|- ( ph -> 0 <_ A )

Proof

Step	Hyp	Ref	Expression
1		climshft2.1	|- Z = ( ZZ>= ` M )
2		climshft2.2	|- ( ph -> M e. ZZ )
3		climrecl.3	|- ( ph -> F ~~> A )
4		climrecl.4	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
5		climge0.5	|- ( ( ph /\ k e. Z ) -> 0 <_ ( F ` k ) )
6	1	uzsup	|- ( M e. ZZ -> sup ( Z , RR* , < ) = +oo )
7	2 6	syl	|- ( ph -> sup ( Z , RR* , < ) = +oo )
8		climrel	|- Rel ~~>
9	8	brrelex1i	|- ( F ~~> A -> F e. _V )
10	3 9	syl	|- ( ph -> F e. _V )
11		eqid	|- ( k e. Z |-> ( F ` k ) ) = ( k e. Z |-> ( F ` k ) )
12	1 11	climmpt	|- ( ( M e. ZZ /\ F e. _V ) -> ( F ~~> A <-> ( k e. Z |-> ( F ` k ) ) ~~> A ) )
13	2 10 12	syl2anc	|- ( ph -> ( F ~~> A <-> ( k e. Z |-> ( F ` k ) ) ~~> A ) )
14	3 13	mpbid	|- ( ph -> ( k e. Z |-> ( F ` k ) ) ~~> A )
15	4	recnd	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
16	15	fmpttd	|- ( ph -> ( k e. Z |-> ( F ` k ) ) : Z --> CC )
17	1 2 16	rlimclim	|- ( ph -> ( ( k e. Z |-> ( F ` k ) ) ~~>r A <-> ( k e. Z |-> ( F ` k ) ) ~~> A ) )
18	14 17	mpbird	|- ( ph -> ( k e. Z |-> ( F ` k ) ) ~~>r A )
19	7 18 4 5	rlimge0	|- ( ph -> 0 <_ A )