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

Metamath Proof Explorer

Theorem climlec2

Description: Comparison of a constant to the limit of a sequence. (Contributed by NM, 28-Feb-2008) (Revised by Mario Carneiro, 1-Feb-2014)

Ref Expression
Hypotheses clim2ser.1 ⊢ Z = ℤ ≥ M
climlec2.2 ⊢ φ → M ∈ ℤ
climlec2.3 ⊢ φ → A ∈ ℝ
climlec2.4 ⊢ φ → F ⇝ B
climlec2.5 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ
climlec2.6 ⊢ φ ∧ k ∈ Z → A ≤ F ⁡ k
Assertion climlec2 ⊢ φ → A ≤ B

Proof

Step Hyp Ref Expression
1 clim2ser.1 ⊢ Z = ℤ ≥ M
2 climlec2.2 ⊢ φ → M ∈ ℤ
3 climlec2.3 ⊢ φ → A ∈ ℝ
4 climlec2.4 ⊢ φ → F ⇝ B
5 climlec2.5 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ
6 climlec2.6 ⊢ φ ∧ k ∈ Z → A ≤ F ⁡ k
7 3 recnd ⊢ φ → A ∈ ℂ
8 0z ⊢ 0 ∈ ℤ
9 uzssz ⊢ ℤ ≥ 0 ⊆ ℤ
10 zex ⊢ ℤ ∈ V
11 9 10 climconst2 ⊢ A ∈ ℂ ∧ 0 ∈ ℤ → ℤ × A ⇝ A
12 7 8 11 sylancl ⊢ φ → ℤ × A ⇝ A
13 eluzelz ⊢ k ∈ ℤ ≥ M → k ∈ ℤ
14 13 1 eleq2s ⊢ k ∈ Z → k ∈ ℤ
15 fvconst2g ⊢ A ∈ ℝ ∧ k ∈ ℤ → ℤ × A ⁡ k = A
16 3 14 15 syl2an ⊢ φ ∧ k ∈ Z → ℤ × A ⁡ k = A
17 3 adantr ⊢ φ ∧ k ∈ Z → A ∈ ℝ
18 16 17 eqeltrd ⊢ φ ∧ k ∈ Z → ℤ × A ⁡ k ∈ ℝ
19 16 6 eqbrtrd ⊢ φ ∧ k ∈ Z → ℤ × A ⁡ k ≤ F ⁡ k
20 1 2 12 4 18 5 19 climle ⊢ φ → A ≤ B