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

Metamath Proof Explorer

Theorem climmptf

Description: Exhibit a function G with the same convergence properties as the not-quite-function F . (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses climmptf.k ⊢ Ⅎ _ k F
climmptf.m ⊢ φ → M ∈ ℤ
climmptf.f ⊢ φ → F ∈ V
climmptf.z ⊢ Z = ℤ ≥ M
climmptf.g ⊢ G = k ∈ Z ⟼ F ⁡ k
Assertion climmptf ⊢ φ → F ⇝ A ↔ G ⇝ A

Proof

Step Hyp Ref Expression
1 climmptf.k ⊢ Ⅎ _ k F
2 climmptf.m ⊢ φ → M ∈ ℤ
3 climmptf.f ⊢ φ → F ∈ V
4 climmptf.z ⊢ Z = ℤ ≥ M
5 climmptf.g ⊢ G = k ∈ Z ⟼ F ⁡ k
6 nfcv ⊢ Ⅎ _ j F ⁡ k
7 nfcv ⊢ Ⅎ _ k j
8 1 7 nffv ⊢ Ⅎ _ k F ⁡ j
9 fveq2 ⊢ k = j → F ⁡ k = F ⁡ j
10 6 8 9 cbvmpt ⊢ k ∈ Z ⟼ F ⁡ k = j ∈ Z ⟼ F ⁡ j
11 5 10 eqtri ⊢ G = j ∈ Z ⟼ F ⁡ j
12 4 11 climmpt ⊢ M ∈ ℤ ∧ F ∈ V → F ⇝ A ↔ G ⇝ A
13 2 3 12 syl2anc ⊢ φ → F ⇝ A ↔ G ⇝ A