Metamath Proof Explorer


Theorem ef0lem

Description: The series defining the exponential function converges in the (trivial) case of a zero argument. (Contributed by Steve Rodriguez, 7-Jun-2006) (Revised by Mario Carneiro, 28-Apr-2014)

Ref Expression
Hypothesis eftval.1
|- F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
Assertion ef0lem
|- ( A = 0 -> seq 0 ( + , F ) ~~> 1 )

Proof

Step Hyp Ref Expression
1 eftval.1
 |-  F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
2 simpr
 |-  ( ( A = 0 /\ k e. ( ZZ>= ` 0 ) ) -> k e. ( ZZ>= ` 0 ) )
3 nn0uz
 |-  NN0 = ( ZZ>= ` 0 )
4 2 3 eleqtrrdi
 |-  ( ( A = 0 /\ k e. ( ZZ>= ` 0 ) ) -> k e. NN0 )
5 elnn0
 |-  ( k e. NN0 <-> ( k e. NN \/ k = 0 ) )
6 4 5 sylib
 |-  ( ( A = 0 /\ k e. ( ZZ>= ` 0 ) ) -> ( k e. NN \/ k = 0 ) )
7 nnnn0
 |-  ( k e. NN -> k e. NN0 )
8 7 adantl
 |-  ( ( A = 0 /\ k e. NN ) -> k e. NN0 )
9 1 eftval
 |-  ( k e. NN0 -> ( F ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
10 8 9 syl
 |-  ( ( A = 0 /\ k e. NN ) -> ( F ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
11 oveq1
 |-  ( A = 0 -> ( A ^ k ) = ( 0 ^ k ) )
12 0exp
 |-  ( k e. NN -> ( 0 ^ k ) = 0 )
13 11 12 sylan9eq
 |-  ( ( A = 0 /\ k e. NN ) -> ( A ^ k ) = 0 )
14 13 oveq1d
 |-  ( ( A = 0 /\ k e. NN ) -> ( ( A ^ k ) / ( ! ` k ) ) = ( 0 / ( ! ` k ) ) )
15 faccl
 |-  ( k e. NN0 -> ( ! ` k ) e. NN )
16 nncn
 |-  ( ( ! ` k ) e. NN -> ( ! ` k ) e. CC )
17 nnne0
 |-  ( ( ! ` k ) e. NN -> ( ! ` k ) =/= 0 )
18 16 17 div0d
 |-  ( ( ! ` k ) e. NN -> ( 0 / ( ! ` k ) ) = 0 )
19 8 15 18 3syl
 |-  ( ( A = 0 /\ k e. NN ) -> ( 0 / ( ! ` k ) ) = 0 )
20 10 14 19 3eqtrd
 |-  ( ( A = 0 /\ k e. NN ) -> ( F ` k ) = 0 )
21 nnne0
 |-  ( k e. NN -> k =/= 0 )
22 velsn
 |-  ( k e. { 0 } <-> k = 0 )
23 22 necon3bbii
 |-  ( -. k e. { 0 } <-> k =/= 0 )
24 21 23 sylibr
 |-  ( k e. NN -> -. k e. { 0 } )
25 24 adantl
 |-  ( ( A = 0 /\ k e. NN ) -> -. k e. { 0 } )
26 25 iffalsed
 |-  ( ( A = 0 /\ k e. NN ) -> if ( k e. { 0 } , 1 , 0 ) = 0 )
27 20 26 eqtr4d
 |-  ( ( A = 0 /\ k e. NN ) -> ( F ` k ) = if ( k e. { 0 } , 1 , 0 ) )
28 fveq2
 |-  ( k = 0 -> ( F ` k ) = ( F ` 0 ) )
29 oveq1
 |-  ( A = 0 -> ( A ^ 0 ) = ( 0 ^ 0 ) )
30 0exp0e1
 |-  ( 0 ^ 0 ) = 1
31 29 30 eqtrdi
 |-  ( A = 0 -> ( A ^ 0 ) = 1 )
32 31 oveq1d
 |-  ( A = 0 -> ( ( A ^ 0 ) / ( ! ` 0 ) ) = ( 1 / ( ! ` 0 ) ) )
33 0nn0
 |-  0 e. NN0
34 1 eftval
 |-  ( 0 e. NN0 -> ( F ` 0 ) = ( ( A ^ 0 ) / ( ! ` 0 ) ) )
35 33 34 ax-mp
 |-  ( F ` 0 ) = ( ( A ^ 0 ) / ( ! ` 0 ) )
36 fac0
 |-  ( ! ` 0 ) = 1
37 36 oveq2i
 |-  ( 1 / ( ! ` 0 ) ) = ( 1 / 1 )
38 1div1e1
 |-  ( 1 / 1 ) = 1
39 37 38 eqtr2i
 |-  1 = ( 1 / ( ! ` 0 ) )
40 32 35 39 3eqtr4g
 |-  ( A = 0 -> ( F ` 0 ) = 1 )
41 28 40 sylan9eqr
 |-  ( ( A = 0 /\ k = 0 ) -> ( F ` k ) = 1 )
42 simpr
 |-  ( ( A = 0 /\ k = 0 ) -> k = 0 )
43 42 22 sylibr
 |-  ( ( A = 0 /\ k = 0 ) -> k e. { 0 } )
44 43 iftrued
 |-  ( ( A = 0 /\ k = 0 ) -> if ( k e. { 0 } , 1 , 0 ) = 1 )
45 41 44 eqtr4d
 |-  ( ( A = 0 /\ k = 0 ) -> ( F ` k ) = if ( k e. { 0 } , 1 , 0 ) )
46 27 45 jaodan
 |-  ( ( A = 0 /\ ( k e. NN \/ k = 0 ) ) -> ( F ` k ) = if ( k e. { 0 } , 1 , 0 ) )
47 6 46 syldan
 |-  ( ( A = 0 /\ k e. ( ZZ>= ` 0 ) ) -> ( F ` k ) = if ( k e. { 0 } , 1 , 0 ) )
48 33 3 eleqtri
 |-  0 e. ( ZZ>= ` 0 )
49 48 a1i
 |-  ( A = 0 -> 0 e. ( ZZ>= ` 0 ) )
50 1cnd
 |-  ( ( A = 0 /\ k e. { 0 } ) -> 1 e. CC )
51 fz0sn
 |-  ( 0 ... 0 ) = { 0 }
52 51 eqimss2i
 |-  { 0 } C_ ( 0 ... 0 )
53 52 a1i
 |-  ( A = 0 -> { 0 } C_ ( 0 ... 0 ) )
54 47 49 50 53 fsumcvg2
 |-  ( A = 0 -> seq 0 ( + , F ) ~~> ( seq 0 ( + , F ) ` 0 ) )
55 0z
 |-  0 e. ZZ
56 55 40 seq1i
 |-  ( A = 0 -> ( seq 0 ( + , F ) ` 0 ) = 1 )
57 54 56 breqtrd
 |-  ( A = 0 -> seq 0 ( + , F ) ~~> 1 )