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 )