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

Metamath Proof Explorer

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 = ℤ ≥ M
climshft2.2 ⊢ φ → M ∈ ℤ
climrecl.3 ⊢ φ → F ⇝ A
climrecl.4 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ
climge0.5 ⊢ φ ∧ k ∈ Z → 0 ≤ F ⁡ k
Assertion climge0 ⊢ φ → 0 ≤ A

Proof

Step Hyp Ref Expression
1 climshft2.1 ⊢ Z = ℤ ≥ M
2 climshft2.2 ⊢ φ → M ∈ ℤ
3 climrecl.3 ⊢ φ → F ⇝ A
4 climrecl.4 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ
5 climge0.5 ⊢ φ ∧ k ∈ Z → 0 ≤ F ⁡ k
6 1 uzsup ⊢ M ∈ ℤ → sup Z ℝ * < = +∞
7 2 6 syl ⊢ φ → sup Z ℝ * < = +∞
8 climrel ⊢ Rel ⁡ ⇝
9 8 brrelex1i ⊢ F ⇝ A → F ∈ V
10 3 9 syl ⊢ φ → F ∈ V
11 eqid ⊢ k ∈ Z ⟼ F ⁡ k = k ∈ Z ⟼ F ⁡ k
12 1 11 climmpt ⊢ M ∈ ℤ ∧ F ∈ V → F ⇝ A ↔ k ∈ Z ⟼ F ⁡ k ⇝ A
13 2 10 12 syl2anc ⊢ φ → F ⇝ A ↔ k ∈ Z ⟼ F ⁡ k ⇝ A
14 3 13 mpbid ⊢ φ → k ∈ Z ⟼ F ⁡ k ⇝ A
15 4 recnd ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
16 15 fmpttd ⊢ φ → k ∈ Z ⟼ F ⁡ k : Z ⟶ ℂ
17 1 2 16 rlimclim ⊢ φ → k ∈ Z ⟼ F ⁡ k ⇝ℝ A ↔ k ∈ Z ⟼ F ⁡ k ⇝ A
18 14 17 mpbird ⊢ φ → k ∈ Z ⟼ F ⁡ k ⇝ℝ A
19 7 18 4 5 rlimge0 ⊢ φ → 0 ≤ A