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 φ F V
dfef2.2 φ A
dfef2.3 φ k F k = 1 + A k k
Assertion dfef2 φ F e A

Proof

Step Hyp Ref Expression
1 dfef2.1 φ F V
2 dfef2.2 φ A
3 dfef2.3 φ k F k = 1 + A k k
4 ax-1cn 1
5 simpl A x A
6 nncn x x
7 6 adantl A x x
8 nnne0 x x 0
9 8 adantl A x x 0
10 5 7 9 divcld A x A x
11 addcl 1 A x 1 + A x
12 4 10 11 sylancr A x 1 + A x
13 nnnn0 x x 0
14 13 adantl A x x 0
15 cxpexp 1 + A x x 0 1 + A x x = 1 + A x x
16 12 14 15 syl2anc A x 1 + A x x = 1 + A x x
17 16 mpteq2dva A x 1 + A x x = x 1 + A x x
18 nnrp x x +
19 18 ssriv +
20 19 a1i A +
21 eqid 0 ball abs 1 A + 1 = 0 ball abs 1 A + 1
22 21 efrlim A x + 1 + A x x e A
23 20 22 rlimres2 A x 1 + A x x e A
24 17 23 eqbrtrrd A x 1 + A x x e A
25 nnuz = 1
26 1zzd A 1
27 12 14 expcld A x 1 + A x x
28 27 fmpttd A x 1 + A x x :
29 25 26 28 rlimclim A x 1 + A x x e A x 1 + A x x e A
30 24 29 mpbid A x 1 + A x x e A
31 2 30 syl φ x 1 + A x x e A
32 nnex V
33 32 mptex x 1 + A x x V
34 33 a1i φ x 1 + A x x V
35 1zzd φ 1
36 oveq2 x = k A x = A k
37 36 oveq2d x = k 1 + A x = 1 + A k
38 id x = k x = k
39 37 38 oveq12d x = k 1 + A x x = 1 + A k k
40 eqid x 1 + A x x = x 1 + A x x
41 ovex 1 + A k k V
42 39 40 41 fvmpt k x 1 + A x x k = 1 + A k k
43 42 adantl φ k x 1 + A x x k = 1 + A k k
44 43 3 eqtr4d φ k x 1 + A x x k = F k
45 25 34 1 35 44 climeq φ x 1 + A x x e A F e A
46 31 45 mpbid φ F e A