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

Metamath Proof Explorer

Theorem rlimle

Description: Comparison of the limits of two sequences. (Contributed by Mario Carneiro, 10-May-2016)

Ref Expression
Hypotheses rlimle.1 
|- ( ph -> sup ( A , RR* , < ) = +oo )
rlimle.2 
|- ( ph -> ( x e. A |-> B ) ~~>r D )
rlimle.3 
|- ( ph -> ( x e. A |-> C ) ~~>r E )
rlimle.4 
|- ( ( ph /\ x e. A ) -> B e. RR )
rlimle.5 
|- ( ( ph /\ x e. A ) -> C e. RR )
rlimle.6 
|- ( ( ph /\ x e. A ) -> B <_ C )
Assertion rlimle 
|- ( ph -> D <_ E )

Proof

Step Hyp Ref Expression
1 rlimle.1 
 |-  ( ph -> sup ( A , RR* , < ) = +oo )
2 rlimle.2 
 |-  ( ph -> ( x e. A |-> B ) ~~>r D )
3 rlimle.3 
 |-  ( ph -> ( x e. A |-> C ) ~~>r E )
4 rlimle.4 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
5 rlimle.5 
 |-  ( ( ph /\ x e. A ) -> C e. RR )
6 rlimle.6 
 |-  ( ( ph /\ x e. A ) -> B <_ C )
7 5 4 3 2 rlimsub 
 |-  ( ph -> ( x e. A |-> ( C - B ) ) ~~>r ( E - D ) )
8 5 4 resubcld 
 |-  ( ( ph /\ x e. A ) -> ( C - B ) e. RR )
9 5 4 subge0d 
 |-  ( ( ph /\ x e. A ) -> ( 0 <_ ( C - B ) <-> B <_ C ) )
10 6 9 mpbird 
 |-  ( ( ph /\ x e. A ) -> 0 <_ ( C - B ) )
11 1 7 8 10 rlimge0 
 |-  ( ph -> 0 <_ ( E - D ) )
12 1 3 5 rlimrecl 
 |-  ( ph -> E e. RR )
13 1 2 4 rlimrecl 
 |-  ( ph -> D e. RR )
14 12 13 subge0d 
 |-  ( ph -> ( 0 <_ ( E - D ) <-> D <_ E ) )
15 11 14 mpbid 
 |-  ( ph -> D <_ E )