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 A ℝ * < = +∞
rlimle.2 ⊢ φ → x ∈ A ⟼ B ⇝ℝ D
rlimle.3 ⊢ φ → x ∈ A ⟼ C ⇝ℝ E
rlimle.4 ⊢ φ ∧ x ∈ A → B ∈ ℝ
rlimle.5 ⊢ φ ∧ x ∈ A → C ∈ ℝ
rlimle.6 ⊢ φ ∧ x ∈ A → B ≤ C
Assertion rlimle ⊢ φ → D ≤ E

Proof

Step Hyp Ref Expression
1 rlimle.1 ⊢ φ → sup A ℝ * < = +∞
2 rlimle.2 ⊢ φ → x ∈ A ⟼ B ⇝ℝ D
3 rlimle.3 ⊢ φ → x ∈ A ⟼ C ⇝ℝ E
4 rlimle.4 ⊢ φ ∧ x ∈ A → B ∈ ℝ
5 rlimle.5 ⊢ φ ∧ x ∈ A → C ∈ ℝ
6 rlimle.6 ⊢ φ ∧ x ∈ A → B ≤ C
7 5 4 3 2 rlimsub ⊢ φ → x ∈ A ⟼ C − B ⇝ℝ E − D
8 5 4 resubcld ⊢ φ ∧ x ∈ A → C − B ∈ ℝ
9 5 4 subge0d ⊢ φ ∧ x ∈ A → 0 ≤ C − B ↔ B ≤ C
10 6 9 mpbird ⊢ φ ∧ x ∈ A → 0 ≤ C − B
11 1 7 8 10 rlimge0 ⊢ φ → 0 ≤ E − D
12 1 3 5 rlimrecl ⊢ φ → E ∈ ℝ
13 1 2 4 rlimrecl ⊢ φ → D ∈ ℝ
14 12 13 subge0d ⊢ φ → 0 ≤ E − D ↔ D ≤ E
15 11 14 mpbid ⊢ φ → D ≤ E