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 𝑍 = ( ℤ𝑀 )
climmpt2.2 ( 𝜑𝑀 ∈ ℤ )
climmpt2.3 ( 𝜑𝐹𝑉 )
climmpt2.5 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℂ )
Assertion climmpt2 ( 𝜑 → ( 𝐹𝐴 ↔ ( 𝑛𝑍 ↦ ( 𝐹𝑛 ) ) ⇝𝑟 𝐴 ) )

Proof

Step Hyp Ref Expression
1 climmpt2.1 𝑍 = ( ℤ𝑀 )
2 climmpt2.2 ( 𝜑𝑀 ∈ ℤ )
3 climmpt2.3 ( 𝜑𝐹𝑉 )
4 climmpt2.5 ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℂ )
5 eqid ( 𝑛𝑍 ↦ ( 𝐹𝑛 ) ) = ( 𝑛𝑍 ↦ ( 𝐹𝑛 ) )
6 1 5 climmpt ( ( 𝑀 ∈ ℤ ∧ 𝐹𝑉 ) → ( 𝐹𝐴 ↔ ( 𝑛𝑍 ↦ ( 𝐹𝑛 ) ) ⇝ 𝐴 ) )
7 2 3 6 syl2anc ( 𝜑 → ( 𝐹𝐴 ↔ ( 𝑛𝑍 ↦ ( 𝐹𝑛 ) ) ⇝ 𝐴 ) )
8 4 ralrimiva ( 𝜑 → ∀ 𝑘𝑍 ( 𝐹𝑘 ) ∈ ℂ )
9 fveq2 ( 𝑘 = 𝑚 → ( 𝐹𝑘 ) = ( 𝐹𝑚 ) )
10 9 eleq1d ( 𝑘 = 𝑚 → ( ( 𝐹𝑘 ) ∈ ℂ ↔ ( 𝐹𝑚 ) ∈ ℂ ) )
11 10 cbvralvw ( ∀ 𝑘𝑍 ( 𝐹𝑘 ) ∈ ℂ ↔ ∀ 𝑚𝑍 ( 𝐹𝑚 ) ∈ ℂ )
12 fveq2 ( 𝑚 = 𝑛 → ( 𝐹𝑚 ) = ( 𝐹𝑛 ) )
13 12 eleq1d ( 𝑚 = 𝑛 → ( ( 𝐹𝑚 ) ∈ ℂ ↔ ( 𝐹𝑛 ) ∈ ℂ ) )
14 13 cbvralvw ( ∀ 𝑚𝑍 ( 𝐹𝑚 ) ∈ ℂ ↔ ∀ 𝑛𝑍 ( 𝐹𝑛 ) ∈ ℂ )
15 11 14 bitri ( ∀ 𝑘𝑍 ( 𝐹𝑘 ) ∈ ℂ ↔ ∀ 𝑛𝑍 ( 𝐹𝑛 ) ∈ ℂ )
16 8 15 sylib ( 𝜑 → ∀ 𝑛𝑍 ( 𝐹𝑛 ) ∈ ℂ )
17 16 r19.21bi ( ( 𝜑𝑛𝑍 ) → ( 𝐹𝑛 ) ∈ ℂ )
18 17 fmpttd ( 𝜑 → ( 𝑛𝑍 ↦ ( 𝐹𝑛 ) ) : 𝑍 ⟶ ℂ )
19 1 2 18 rlimclim ( 𝜑 → ( ( 𝑛𝑍 ↦ ( 𝐹𝑛 ) ) ⇝𝑟 𝐴 ↔ ( 𝑛𝑍 ↦ ( 𝐹𝑛 ) ) ⇝ 𝐴 ) )
20 7 19 bitr4d ( 𝜑 → ( 𝐹𝐴 ↔ ( 𝑛𝑍 ↦ ( 𝐹𝑛 ) ) ⇝𝑟 𝐴 ) )