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