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 |
⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ⇝𝑟 𝐴 ) ) |