Theorem climge0

Description: A nonnegative sequence converges to a nonnegative number. (Contributed by NM, 11-Sep-2005) (Proof shortened by Mario Carneiro, 10-May-2016)

	Ref	Expression
Hypotheses	climshft2.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climshft2.2	$$⊢\phi \to M\in \mathbb{Z}$$
	climrecl.3	$$⊢\phi \to F⇝A$$
	climrecl.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
	climge0.5	$$⊢\left(\phi \wedge k\in Z\right)\to 0\le F\left(k\right)$$
Assertion	climge0	$$⊢\phi \to 0\le A$$

Proof

Step	Hyp	Ref	Expression
1		climshft2.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		climshft2.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		climrecl.3	$$⊢\phi \to F⇝A$$
4		climrecl.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
5		climge0.5	$$⊢\left(\phi \wedge k\in Z\right)\to 0\le F\left(k\right)$$
6	1	uzsup	$$⊢M\in \mathbb{Z}\to sup\left(Z,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
7	2 6	syl	$$⊢\phi \to sup\left(Z,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
8		climrel	$$⊢\mathrm{Rel}⇝$$
9	8	brrelex1i	$$⊢F⇝A\to F\in \mathrm{V}$$
10	3 9	syl	$$⊢\phi \to F\in \mathrm{V}$$
11		eqid	$$⊢\left(k\in Z⟼F\left(k\right)\right)=\left(k\in Z⟼F\left(k\right)\right)$$
12	1 11	climmpt	$$⊢\left(M\in \mathbb{Z}\wedge F\in \mathrm{V}\right)\to \left(F⇝A\leftrightarrow \left(k\in Z⟼F\left(k\right)\right)⇝A\right)$$
13	2 10 12	syl2anc	$$⊢\phi \to \left(F⇝A\leftrightarrow \left(k\in Z⟼F\left(k\right)\right)⇝A\right)$$
14	3 13	mpbid	$$⊢\phi \to \left(k\in Z⟼F\left(k\right)\right)⇝A$$
15	4	recnd	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
16	15	fmpttd	$$⊢\phi \to \left(k\in Z⟼F\left(k\right)\right):Z⟶ℂ$$
17	1 2 16	rlimclim	$$⊢\phi \to \left(\left(k\in Z⟼F\left(k\right)\right)\underset{ℝ}{⇝}A\leftrightarrow \left(k\in Z⟼F\left(k\right)\right)⇝A\right)$$
18	14 17	mpbird	$$⊢\phi \to \left(k\in Z⟼F\left(k\right)\right)\underset{ℝ}{⇝}A$$
19	7 18 4 5	rlimge0	$$⊢\phi \to 0\le A$$