Theorem rlimle

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

	Ref	Expression
Hypotheses	rlimle.1	$$⊢\phi \to sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
	rlimle.2	$$⊢\phi \to \left(x\in A⟼B\right)\underset{ℝ}{⇝}D$$
	rlimle.3	$$⊢\phi \to \left(x\in A⟼C\right)\underset{ℝ}{⇝}E$$
	rlimle.4	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
	rlimle.5	$$⊢\left(\phi \wedge x\in A\right)\to C\in ℝ$$
	rlimle.6	$$⊢\left(\phi \wedge x\in A\right)\to B\le C$$
Assertion	rlimle	$$⊢\phi \to D\le E$$

Proof

Step	Hyp	Ref	Expression
1		rlimle.1	$$⊢\phi \to sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
2		rlimle.2	$$⊢\phi \to \left(x\in A⟼B\right)\underset{ℝ}{⇝}D$$
3		rlimle.3	$$⊢\phi \to \left(x\in A⟼C\right)\underset{ℝ}{⇝}E$$
4		rlimle.4	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
5		rlimle.5	$$⊢\left(\phi \wedge x\in A\right)\to C\in ℝ$$
6		rlimle.6	$$⊢\left(\phi \wedge x\in A\right)\to B\le C$$
7	5 4 3 2	rlimsub	$$⊢\phi \to \left(x\in A⟼C-B\right)\underset{ℝ}{⇝}\left(E-D\right)$$
8	5 4	resubcld	$$⊢\left(\phi \wedge x\in A\right)\to C-B\in ℝ$$
9	5 4	subge0d	$$⊢\left(\phi \wedge x\in A\right)\to \left(0\le C-B\leftrightarrow B\le C\right)$$
10	6 9	mpbird	$$⊢\left(\phi \wedge x\in A\right)\to 0\le C-B$$
11	1 7 8 10	rlimge0	$$⊢\phi \to 0\le E-D$$
12	1 3 5	rlimrecl	$$⊢\phi \to E\in ℝ$$
13	1 2 4	rlimrecl	$$⊢\phi \to D\in ℝ$$
14	12 13	subge0d	$$⊢\phi \to \left(0\le E-D\leftrightarrow D\le E\right)$$
15	11 14	mpbid	$$⊢\phi \to D\le E$$