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 ( 𝐴 , ℝ* , < ) = +∞ )
	rlimcld2.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 )
	rlimrecl.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
	rlimge0.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ 𝐵 )
Assertion	rlimge0	⊢ ( 𝜑 → 0 ≤ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		rlimcld2.1	⊢ ( 𝜑 → sup ( 𝐴 , ℝ* , < ) = +∞ )
2		rlimcld2.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⇝𝑟 𝐶 )
3		rlimrecl.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
4		rlimge0.4	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ 𝐵 )
5	3	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
6	3	rered	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐵 ) = 𝐵 )
7	4 6	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( ℜ ‘ 𝐵 ) )
8	1 2 5 7	rlimrege0	⊢ ( 𝜑 → 0 ≤ ( ℜ ‘ 𝐶 ) )
9	1 2 3	rlimrecl	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
10	9	rered	⊢ ( 𝜑 → ( ℜ ‘ 𝐶 ) = 𝐶 )
11	8 10	breqtrd	⊢ ( 𝜑 → 0 ≤ 𝐶 )