This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rlimge0

Description: The limit of a sequence of nonnegative reals is nonnegative. (Contributed by Mario Carneiro, 10-May-2016)

Ref Expression
Hypotheses rlimcld2.1 ⊢ φ → sup A ℝ * < = +∞
rlimcld2.2 ⊢ φ → x ∈ A ⟼ B ⇝ℝ C
rlimrecl.3 ⊢ φ ∧ x ∈ A → B ∈ ℝ
rlimge0.4 ⊢ φ ∧ x ∈ A → 0 ≤ B
Assertion rlimge0 ⊢ φ → 0 ≤ C

Proof

Step Hyp Ref Expression
1 rlimcld2.1 ⊢ φ → sup A ℝ * < = +∞
2 rlimcld2.2 ⊢ φ → x ∈ A ⟼ B ⇝ℝ C
3 rlimrecl.3 ⊢ φ ∧ x ∈ A → B ∈ ℝ
4 rlimge0.4 ⊢ φ ∧ x ∈ A → 0 ≤ B
5 3 recnd ⊢ φ ∧ x ∈ A → B ∈ ℂ
6 3 rered ⊢ φ ∧ x ∈ A → ℜ ⁡ B = B
7 4 6 breqtrrd ⊢ φ ∧ x ∈ A → 0 ≤ ℜ ⁡ B
8 1 2 5 7 rlimrege0 ⊢ φ → 0 ≤ ℜ ⁡ C
9 1 2 3 rlimrecl ⊢ φ → C ∈ ℝ
10 9 rered ⊢ φ → ℜ ⁡ C = C
11 8 10 breqtrd ⊢ φ → 0 ≤ C