Step |
Hyp |
Ref |
Expression |
1 |
|
dfef2.1 |
⊢ ( 𝜑 → 𝐹 ∈ 𝑉 ) |
2 |
|
dfef2.2 |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
3 |
|
dfef2.3 |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐹 ‘ 𝑘 ) = ( ( 1 + ( 𝐴 / 𝑘 ) ) ↑ 𝑘 ) ) |
4 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
5 |
|
simpl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ ) → 𝐴 ∈ ℂ ) |
6 |
|
nncn |
⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℂ ) |
7 |
6
|
adantl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ ) → 𝑥 ∈ ℂ ) |
8 |
|
nnne0 |
⊢ ( 𝑥 ∈ ℕ → 𝑥 ≠ 0 ) |
9 |
8
|
adantl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ ) → 𝑥 ≠ 0 ) |
10 |
5 7 9
|
divcld |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ ) → ( 𝐴 / 𝑥 ) ∈ ℂ ) |
11 |
|
addcl |
⊢ ( ( 1 ∈ ℂ ∧ ( 𝐴 / 𝑥 ) ∈ ℂ ) → ( 1 + ( 𝐴 / 𝑥 ) ) ∈ ℂ ) |
12 |
4 10 11
|
sylancr |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ ) → ( 1 + ( 𝐴 / 𝑥 ) ) ∈ ℂ ) |
13 |
|
nnnn0 |
⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℕ0 ) |
14 |
13
|
adantl |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ ) → 𝑥 ∈ ℕ0 ) |
15 |
|
cxpexp |
⊢ ( ( ( 1 + ( 𝐴 / 𝑥 ) ) ∈ ℂ ∧ 𝑥 ∈ ℕ0 ) → ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑𝑐 𝑥 ) = ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) |
16 |
12 14 15
|
syl2anc |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ ) → ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑𝑐 𝑥 ) = ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) |
17 |
16
|
mpteq2dva |
⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑𝑐 𝑥 ) ) = ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ) |
18 |
|
nnrp |
⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℝ+ ) |
19 |
18
|
ssriv |
⊢ ℕ ⊆ ℝ+ |
20 |
19
|
a1i |
⊢ ( 𝐴 ∈ ℂ → ℕ ⊆ ℝ+ ) |
21 |
|
eqid |
⊢ ( 0 ( ball ‘ ( abs ∘ − ) ) ( 1 / ( ( abs ‘ 𝐴 ) + 1 ) ) ) = ( 0 ( ball ‘ ( abs ∘ − ) ) ( 1 / ( ( abs ‘ 𝐴 ) + 1 ) ) ) |
22 |
21
|
efrlim |
⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℝ+ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑𝑐 𝑥 ) ) ⇝𝑟 ( exp ‘ 𝐴 ) ) |
23 |
20 22
|
rlimres2 |
⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑𝑐 𝑥 ) ) ⇝𝑟 ( exp ‘ 𝐴 ) ) |
24 |
17 23
|
eqbrtrrd |
⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ⇝𝑟 ( exp ‘ 𝐴 ) ) |
25 |
|
nnuz |
⊢ ℕ = ( ℤ≥ ‘ 1 ) |
26 |
|
1zzd |
⊢ ( 𝐴 ∈ ℂ → 1 ∈ ℤ ) |
27 |
12 14
|
expcld |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℕ ) → ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ∈ ℂ ) |
28 |
27
|
fmpttd |
⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) : ℕ ⟶ ℂ ) |
29 |
25 26 28
|
rlimclim |
⊢ ( 𝐴 ∈ ℂ → ( ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ⇝𝑟 ( exp ‘ 𝐴 ) ↔ ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ⇝ ( exp ‘ 𝐴 ) ) ) |
30 |
24 29
|
mpbid |
⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ⇝ ( exp ‘ 𝐴 ) ) |
31 |
2 30
|
syl |
⊢ ( 𝜑 → ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ⇝ ( exp ‘ 𝐴 ) ) |
32 |
|
nnex |
⊢ ℕ ∈ V |
33 |
32
|
mptex |
⊢ ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ∈ V |
34 |
33
|
a1i |
⊢ ( 𝜑 → ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ∈ V ) |
35 |
|
1zzd |
⊢ ( 𝜑 → 1 ∈ ℤ ) |
36 |
|
oveq2 |
⊢ ( 𝑥 = 𝑘 → ( 𝐴 / 𝑥 ) = ( 𝐴 / 𝑘 ) ) |
37 |
36
|
oveq2d |
⊢ ( 𝑥 = 𝑘 → ( 1 + ( 𝐴 / 𝑥 ) ) = ( 1 + ( 𝐴 / 𝑘 ) ) ) |
38 |
|
id |
⊢ ( 𝑥 = 𝑘 → 𝑥 = 𝑘 ) |
39 |
37 38
|
oveq12d |
⊢ ( 𝑥 = 𝑘 → ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) = ( ( 1 + ( 𝐴 / 𝑘 ) ) ↑ 𝑘 ) ) |
40 |
|
eqid |
⊢ ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) = ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) |
41 |
|
ovex |
⊢ ( ( 1 + ( 𝐴 / 𝑘 ) ) ↑ 𝑘 ) ∈ V |
42 |
39 40 41
|
fvmpt |
⊢ ( 𝑘 ∈ ℕ → ( ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ‘ 𝑘 ) = ( ( 1 + ( 𝐴 / 𝑘 ) ) ↑ 𝑘 ) ) |
43 |
42
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ‘ 𝑘 ) = ( ( 1 + ( 𝐴 / 𝑘 ) ) ↑ 𝑘 ) ) |
44 |
43 3
|
eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) ) |
45 |
25 34 1 35 44
|
climeq |
⊢ ( 𝜑 → ( ( 𝑥 ∈ ℕ ↦ ( ( 1 + ( 𝐴 / 𝑥 ) ) ↑ 𝑥 ) ) ⇝ ( exp ‘ 𝐴 ) ↔ 𝐹 ⇝ ( exp ‘ 𝐴 ) ) ) |
46 |
31 45
|
mpbid |
⊢ ( 𝜑 → 𝐹 ⇝ ( exp ‘ 𝐴 ) ) |