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 ( 𝜑 → 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 ( 𝜑𝐷𝐸 )