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	$$⊢\phi \to sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
	rlimcld2.2	$$⊢\phi \to \left(x\in A⟼B\right)\underset{ℝ}{⇝}C$$
	rlimrecl.3	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
	rlimge0.4	$$⊢\left(\phi \wedge x\in A\right)\to 0\le B$$
Assertion	rlimge0	$$⊢\phi \to 0\le C$$

Proof

Step	Hyp	Ref	Expression
1		rlimcld2.1	$$⊢\phi \to sup\left(A,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
2		rlimcld2.2	$$⊢\phi \to \left(x\in A⟼B\right)\underset{ℝ}{⇝}C$$
3		rlimrecl.3	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℝ$$
4		rlimge0.4	$$⊢\left(\phi \wedge x\in A\right)\to 0\le B$$
5	3	recnd	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℂ$$
6	3	rered	$$⊢\left(\phi \wedge x\in A\right)\to \Re \left(B\right)=B$$
7	4 6	breqtrrd	$$⊢\left(\phi \wedge x\in A\right)\to 0\le \Re \left(B\right)$$
8	1 2 5 7	rlimrege0	$$⊢\phi \to 0\le \Re \left(C\right)$$
9	1 2 3	rlimrecl	$$⊢\phi \to C\in ℝ$$
10	9	rered	$$⊢\phi \to \Re \left(C\right)=C$$
11	8 10	breqtrd	$$⊢\phi \to 0\le C$$