Theorem rlimle

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

	Ref	Expression
Hypotheses	rlimle.1	⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
	rlimle.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 )
	rlimle.3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 )
	rlimle.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	rlimle.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
	rlimle.6	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
Assertion	rlimle	⊢ ( 𝜑 → 𝐷 ≤ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		rlimle.1	⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
2		rlimle.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐷 )
3		rlimle.3	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ⇝𝑟 𝐸 )
4		rlimle.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
5		rlimle.5	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
6		rlimle.6	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
7	5 4 3 2	rlimsub	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 − 𝐵 ) ) ⇝𝑟 ( 𝐸 − 𝐷 ) )
8	5 4	resubcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
9	5 4	subge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 0 ≤ ( 𝐶 − 𝐵 ) ↔ 𝐵 ≤ 𝐶 ) )
10	6 9	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( 𝐶 − 𝐵 ) )
11	1 7 8 10	rlimge0	⊢ ( 𝜑 → 0 ≤ ( 𝐸 − 𝐷 ) )
12	1 3 5	rlimrecl	⊢ ( 𝜑 → 𝐸 ∈ ℝ )
13	1 2 4	rlimrecl	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
14	12 13	subge0d	⊢ ( 𝜑 → ( 0 ≤ ( 𝐸 − 𝐷 ) ↔ 𝐷 ≤ 𝐸 ) )
15	11 14	mpbid	⊢ ( 𝜑 → 𝐷 ≤ 𝐸 )