Theorem rlimge0

Description: The limit of a sequence of nonnegative reals is nonnegative. (Contributed by Mario Carneiro, 10-May-2016)

	Ref	Expression
Hypotheses	rlimcld2.1	|- ( ph -> sup ( A , RR* , < ) = +oo )
	rlimcld2.2	|- ( ph -> ( x e. A |-> B ) ~~>r C )
	rlimrecl.3	|- ( ( ph /\ x e. A ) -> B e. RR )
	rlimge0.4	|- ( ( ph /\ x e. A ) -> 0 <_ B )
Assertion	rlimge0	|- ( ph -> 0 <_ C )

Proof

Step	Hyp	Ref	Expression
1		rlimcld2.1	|- ( ph -> sup ( A , RR* , < ) = +oo )
2		rlimcld2.2	|- ( ph -> ( x e. A |-> B ) ~~>r C )
3		rlimrecl.3	|- ( ( ph /\ x e. A ) -> B e. RR )
4		rlimge0.4	|- ( ( ph /\ x e. A ) -> 0 <_ B )
5	3	recnd	|- ( ( ph /\ x e. A ) -> B e. CC )
6	3	rered	|- ( ( ph /\ x e. A ) -> ( Re ` B ) = B )
7	4 6	breqtrrd	|- ( ( ph /\ x e. A ) -> 0 <_ ( Re ` B ) )
8	1 2 5 7	rlimrege0	|- ( ph -> 0 <_ ( Re ` C ) )
9	1 2 3	rlimrecl	|- ( ph -> C e. RR )
10	9	rered	|- ( ph -> ( Re ` C ) = C )
11	8 10	breqtrd	|- ( ph -> 0 <_ C )