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

Metamath Proof Explorer

Theorem climmpt

Description: Exhibit a function G with the same convergence properties as the not-quite-function F . (Contributed by Mario Carneiro, 31-Jan-2014)

Ref Expression
Hypotheses 2clim.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climmpt.2 ⊢ 𝐺 = ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) )
Assertion climmpt ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 2clim.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 climmpt.2 ⊢ 𝐺 = ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) )
3 simpr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → 𝐹 ∈ 𝑉 )
4 fvex ⊢ ( ℤ≥ ‘ 𝑀 ) ∈ V
5 1 4 eqeltri ⊢ 𝑍 ∈ V
6 5 mptex ⊢ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ∈ V
7 2 6 eqeltri ⊢ 𝐺 ∈ V
8 7 a1i ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → 𝐺 ∈ V )
9 simpl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → 𝑀 ∈ ℤ )
10 fveq2 ⊢ ( 𝑘 = 𝑚 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) )
11 fvex ⊢ ( 𝐹 ‘ 𝑚 ) ∈ V
12 10 2 11 fvmpt ⊢ ( 𝑚 ∈ 𝑍 → ( 𝐺 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑚 ) )
13 12 eqcomd ⊢ ( 𝑚 ∈ 𝑍 → ( 𝐹 ‘ 𝑚 ) = ( 𝐺 ‘ 𝑚 ) )
14 13 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑚 ) = ( 𝐺 ‘ 𝑚 ) )
15 1 3 8 9 14 climeq ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ⇝ 𝐴 ↔ 𝐺 ⇝ 𝐴 ) )