Metamath Proof Explorer

Theorem climmpt2

Description: Relate an integer limit on a not-quite-function to a real limit. (Contributed by Mario Carneiro, 17-Sep-2014)

Ref Expression
Hypotheses climmpt2.1 ⊢ Z = ℤ ≥ M
climmpt2.2 ⊢ φ → M ∈ ℤ
climmpt2.3 ⊢ φ → F ∈ V
climmpt2.5 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
Assertion climmpt2 ⊢ φ → F ⇝ A ↔ n ∈ Z ⟼ F ⁡ n ⇝ℝ A

Proof

Step Hyp Ref Expression
1 climmpt2.1 ⊢ Z = ℤ ≥ M
2 climmpt2.2 ⊢ φ → M ∈ ℤ
3 climmpt2.3 ⊢ φ → F ∈ V
4 climmpt2.5 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
5 eqid ⊢ n ∈ Z ⟼ F ⁡ n = n ∈ Z ⟼ F ⁡ n
6 1 5 climmpt ⊢ M ∈ ℤ ∧ F ∈ V → F ⇝ A ↔ n ∈ Z ⟼ F ⁡ n ⇝ A
7 2 3 6 syl2anc ⊢ φ → F ⇝ A ↔ n ∈ Z ⟼ F ⁡ n ⇝ A
8 4 ralrimiva ⊢ φ → ∀ k ∈ Z F ⁡ k ∈ ℂ
9 fveq2 ⊢ k = m → F ⁡ k = F ⁡ m
10 9 eleq1d ⊢ k = m → F ⁡ k ∈ ℂ ↔ F ⁡ m ∈ ℂ
11 10 cbvralvw ⊢ ∀ k ∈ Z F ⁡ k ∈ ℂ ↔ ∀ m ∈ Z F ⁡ m ∈ ℂ
12 fveq2 ⊢ m = n → F ⁡ m = F ⁡ n
13 12 eleq1d ⊢ m = n → F ⁡ m ∈ ℂ ↔ F ⁡ n ∈ ℂ
14 13 cbvralvw ⊢ ∀ m ∈ Z F ⁡ m ∈ ℂ ↔ ∀ n ∈ Z F ⁡ n ∈ ℂ
15 11 14 bitri ⊢ ∀ k ∈ Z F ⁡ k ∈ ℂ ↔ ∀ n ∈ Z F ⁡ n ∈ ℂ
16 8 15 sylib ⊢ φ → ∀ n ∈ Z F ⁡ n ∈ ℂ
17 16 r19.21bi ⊢ φ ∧ n ∈ Z → F ⁡ n ∈ ℂ
18 17 fmpttd ⊢ φ → n ∈ Z ⟼ F ⁡ n : Z ⟶ ℂ
19 1 2 18 rlimclim ⊢ φ → n ∈ Z ⟼ F ⁡ n ⇝ℝ A ↔ n ∈ Z ⟼ F ⁡ n ⇝ A
20 7 19 bitr4d ⊢ φ → F ⇝ A ↔ n ∈ Z ⟼ F ⁡ n ⇝ℝ A