Metamath Proof Explorer


Theorem dfef2

Description: The limit of the sequence ( 1 + A / k ) ^ k as k goes to +oo is ( expA ) . This is another common definition of _e . (Contributed by Mario Carneiro, 1-Mar-2015)

Ref Expression
Hypotheses dfef2.1 ( 𝜑𝐹𝑉 )
dfef2.2 ( 𝜑𝐴 ∈ ℂ )
dfef2.3 ( ( 𝜑𝑘 ∈ ℕ ) → ( 𝐹𝑘 ) = ( ( 1 + ( 𝐴 / 𝑘 ) ) ↑ 𝑘 ) )
Assertion dfef2 ( 𝜑𝐹 ⇝ ( exp ‘ 𝐴 ) )

Proof

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 ‘ 𝐴 ) )