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	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climshft2.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climrecl.3	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
	climrecl.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
	climge0.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ ( 𝐹 ‘ 𝑘 ) )
Assertion	climge0	⊢ ( 𝜑 → 0 ≤ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		climshft2.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		climshft2.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		climrecl.3	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
4		climrecl.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
5		climge0.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 0 ≤ ( 𝐹 ‘ 𝑘 ) )
6	1	uzsup	⊢ ( 𝑀 ∈ ℤ → sup ( 𝑍 , ℝ* , < ) = +∞ )
7	2 6	syl	⊢ ( 𝜑 → sup ( 𝑍 , ℝ* , < ) = +∞ )
8		climrel	⊢ Rel ⇝
9	8	brrelex1i	⊢ ( 𝐹 ⇝ 𝐴 → 𝐹 ∈ V )
10	3 9	syl	⊢ ( 𝜑 → 𝐹 ∈ V )
11		eqid	⊢ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) )
12	1 11	climmpt	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ V ) → ( 𝐹 ⇝ 𝐴 ↔ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ⇝ 𝐴 ) )
13	2 10 12	syl2anc	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ⇝ 𝐴 ) )
14	3 13	mpbid	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ⇝ 𝐴 )
15	4	recnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
16	15	fmpttd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) : 𝑍 ⟶ ℂ )
17	1 2 16	rlimclim	⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ⇝𝑟 𝐴 ↔ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ⇝ 𝐴 ) )
18	14 17	mpbird	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ⇝𝑟 𝐴 )
19	7 18 4 5	rlimge0	⊢ ( 𝜑 → 0 ≤ 𝐴 )