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 
|- ( ph -> F e. V )
dfef2.2 
|- ( ph -> A e. CC )
dfef2.3 
|- ( ( ph /\ k e. NN ) -> ( F ` k ) = ( ( 1 + ( A / k ) ) ^ k ) )
Assertion dfef2 
|- ( ph -> F ~~> ( exp ` A ) )

Proof

Step Hyp Ref Expression
1 dfef2.1 
 |-  ( ph -> F e. V )
2 dfef2.2 
 |-  ( ph -> A e. CC )
3 dfef2.3 
 |-  ( ( ph /\ k e. NN ) -> ( F ` k ) = ( ( 1 + ( A / k ) ) ^ k ) )
4 ax-1cn 
 |-  1 e. CC
5 simpl 
 |-  ( ( A e. CC /\ x e. NN ) -> A e. CC )
6 nncn 
 |-  ( x e. NN -> x e. CC )
7 6 adantl 
 |-  ( ( A e. CC /\ x e. NN ) -> x e. CC )
8 nnne0 
 |-  ( x e. NN -> x =/= 0 )
9 8 adantl 
 |-  ( ( A e. CC /\ x e. NN ) -> x =/= 0 )
10 5 7 9 divcld 
 |-  ( ( A e. CC /\ x e. NN ) -> ( A / x ) e. CC )
11 addcl 
 |-  ( ( 1 e. CC /\ ( A / x ) e. CC ) -> ( 1 + ( A / x ) ) e. CC )
12 4 10 11 sylancr 
 |-  ( ( A e. CC /\ x e. NN ) -> ( 1 + ( A / x ) ) e. CC )
13 nnnn0 
 |-  ( x e. NN -> x e. NN0 )
14 13 adantl 
 |-  ( ( A e. CC /\ x e. NN ) -> x e. NN0 )
15 cxpexp 
 |-  ( ( ( 1 + ( A / x ) ) e. CC /\ x e. NN0 ) -> ( ( 1 + ( A / x ) ) ^c x ) = ( ( 1 + ( A / x ) ) ^ x ) )
16 12 14 15 syl2anc 
 |-  ( ( A e. CC /\ x e. NN ) -> ( ( 1 + ( A / x ) ) ^c x ) = ( ( 1 + ( A / x ) ) ^ x ) )
17 16 mpteq2dva 
 |-  ( A e. CC -> ( x e. NN |-> ( ( 1 + ( A / x ) ) ^c x ) ) = ( x e. NN |-> ( ( 1 + ( A / x ) ) ^ x ) ) )
18 nnrp 
 |-  ( x e. NN -> x e. RR+ )
19 18 ssriv 
 |-  NN C_ RR+
20 19 a1i 
 |-  ( A e. CC -> NN C_ RR+ )
21 eqid 
 |-  ( 0 ( ball ` ( abs o. - ) ) ( 1 / ( ( abs ` A ) + 1 ) ) ) = ( 0 ( ball ` ( abs o. - ) ) ( 1 / ( ( abs ` A ) + 1 ) ) )
22 21 efrlim 
 |-  ( A e. CC -> ( x e. RR+ |-> ( ( 1 + ( A / x ) ) ^c x ) ) ~~>r ( exp ` A ) )
23 20 22 rlimres2 
 |-  ( A e. CC -> ( x e. NN |-> ( ( 1 + ( A / x ) ) ^c x ) ) ~~>r ( exp ` A ) )
24 17 23 eqbrtrrd 
 |-  ( A e. CC -> ( x e. NN |-> ( ( 1 + ( A / x ) ) ^ x ) ) ~~>r ( exp ` A ) )
25 nnuz 
 |-  NN = ( ZZ>= ` 1 )
26 1zzd 
 |-  ( A e. CC -> 1 e. ZZ )
27 12 14 expcld 
 |-  ( ( A e. CC /\ x e. NN ) -> ( ( 1 + ( A / x ) ) ^ x ) e. CC )
28 27 fmpttd 
 |-  ( A e. CC -> ( x e. NN |-> ( ( 1 + ( A / x ) ) ^ x ) ) : NN --> CC )
29 25 26 28 rlimclim 
 |-  ( A e. CC -> ( ( x e. NN |-> ( ( 1 + ( A / x ) ) ^ x ) ) ~~>r ( exp ` A ) <-> ( x e. NN |-> ( ( 1 + ( A / x ) ) ^ x ) ) ~~> ( exp ` A ) ) )
30 24 29 mpbid 
 |-  ( A e. CC -> ( x e. NN |-> ( ( 1 + ( A / x ) ) ^ x ) ) ~~> ( exp ` A ) )
31 2 30 syl 
 |-  ( ph -> ( x e. NN |-> ( ( 1 + ( A / x ) ) ^ x ) ) ~~> ( exp ` A ) )
32 nnex 
 |-  NN e. _V
33 32 mptex 
 |-  ( x e. NN |-> ( ( 1 + ( A / x ) ) ^ x ) ) e. _V
34 33 a1i 
 |-  ( ph -> ( x e. NN |-> ( ( 1 + ( A / x ) ) ^ x ) ) e. _V )
35 1zzd 
 |-  ( ph -> 1 e. ZZ )
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 e. NN |-> ( ( 1 + ( A / x ) ) ^ x ) ) = ( x e. NN |-> ( ( 1 + ( A / x ) ) ^ x ) )
41 ovex 
 |-  ( ( 1 + ( A / k ) ) ^ k ) e. _V
42 39 40 41 fvmpt 
 |-  ( k e. NN -> ( ( x e. NN |-> ( ( 1 + ( A / x ) ) ^ x ) ) ` k ) = ( ( 1 + ( A / k ) ) ^ k ) )
43 42 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( ( x e. NN |-> ( ( 1 + ( A / x ) ) ^ x ) ) ` k ) = ( ( 1 + ( A / k ) ) ^ k ) )
44 43 3 eqtr4d 
 |-  ( ( ph /\ k e. NN ) -> ( ( x e. NN |-> ( ( 1 + ( A / x ) ) ^ x ) ) ` k ) = ( F ` k ) )
45 25 34 1 35 44 climeq 
 |-  ( ph -> ( ( x e. NN |-> ( ( 1 + ( A / x ) ) ^ x ) ) ~~> ( exp ` A ) <-> F ~~> ( exp ` A ) ) )
46 31 45 mpbid 
 |-  ( ph -> F ~~> ( exp ` A ) )