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

Metamath Proof Explorer

Theorem climcn1lem

Description: The limit of a continuous function, theorem form. (Contributed by Mario Carneiro, 9-Feb-2014)

Ref Expression
Hypotheses climcn1lem.1 ⊢ Z = ℤ ≥ M
climcn1lem.2 ⊢ φ → F ⇝ A
climcn1lem.4 ⊢ φ → G ∈ W
climcn1lem.5 ⊢ φ → M ∈ ℤ
climcn1lem.6 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
climcn1lem.7 ⊢ H : ℂ ⟶ ℂ
climcn1lem.8 ⊢ A ∈ ℂ ∧ x ∈ ℝ + → ∃ y ∈ ℝ + ∀ z ∈ ℂ z − A < y → H ⁡ z − H ⁡ A < x
climcn1lem.9 ⊢ φ ∧ k ∈ Z → G ⁡ k = H ⁡ F ⁡ k
Assertion climcn1lem ⊢ φ → G ⇝ H ⁡ A

Proof

Step Hyp Ref Expression
1 climcn1lem.1 ⊢ Z = ℤ ≥ M
2 climcn1lem.2 ⊢ φ → F ⇝ A
3 climcn1lem.4 ⊢ φ → G ∈ W
4 climcn1lem.5 ⊢ φ → M ∈ ℤ
5 climcn1lem.6 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
6 climcn1lem.7 ⊢ H : ℂ ⟶ ℂ
7 climcn1lem.8 ⊢ A ∈ ℂ ∧ x ∈ ℝ + → ∃ y ∈ ℝ + ∀ z ∈ ℂ z − A < y → H ⁡ z − H ⁡ A < x
8 climcn1lem.9 ⊢ φ ∧ k ∈ Z → G ⁡ k = H ⁡ F ⁡ k
9 climcl ⊢ F ⇝ A → A ∈ ℂ
10 2 9 syl ⊢ φ → A ∈ ℂ
11 6 ffvelcdmi ⊢ z ∈ ℂ → H ⁡ z ∈ ℂ
12 11 adantl ⊢ φ ∧ z ∈ ℂ → H ⁡ z ∈ ℂ
13 10 7 sylan ⊢ φ ∧ x ∈ ℝ + → ∃ y ∈ ℝ + ∀ z ∈ ℂ z − A < y → H ⁡ z − H ⁡ A < x
14 1 4 10 12 2 3 13 5 8 climcn1 ⊢ φ → G ⇝ H ⁡ A