This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )