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 ( ( 𝑀 ∈ ℤ ∧ 𝐹𝑉 ) → ( 𝐹𝐴𝐺𝐴 ) )