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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
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 ≤ 𝐴 )