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 )