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 0 A n n !
Assertion ef0lem A = 0 seq 0 + F 1

Proof

Step Hyp Ref Expression
1 eftval.1 F = n 0 A n n !
2 simpr A = 0 k 0 k 0
3 nn0uz 0 = 0
4 2 3 eleqtrrdi A = 0 k 0 k 0
5 elnn0 k 0 k k = 0
6 4 5 sylib A = 0 k 0 k k = 0
7 nnnn0 k k 0
8 7 adantl A = 0 k k 0
9 1 eftval k 0 F k = A k k !
10 8 9 syl A = 0 k F k = A k k !
11 oveq1 A = 0 A k = 0 k
12 0exp k 0 k = 0
13 11 12 sylan9eq A = 0 k A k = 0
14 13 oveq1d A = 0 k A k k ! = 0 k !
15 faccl k 0 k !
16 nncn k ! k !
17 nnne0 k ! k ! 0
18 16 17 div0d k ! 0 k ! = 0
19 8 15 18 3syl A = 0 k 0 k ! = 0
20 10 14 19 3eqtrd A = 0 k F k = 0
21 nnne0 k k 0
22 velsn k 0 k = 0
23 22 necon3bbii ¬ k 0 k 0
24 21 23 sylibr k ¬ k 0
25 24 adantl A = 0 k ¬ k 0
26 25 iffalsed A = 0 k if k 0 1 0 = 0
27 20 26 eqtr4d A = 0 k F k = if k 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 0
34 1 eftval 0 0 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 0
44 43 iftrued A = 0 k = 0 if k 0 1 0 = 1
45 41 44 eqtr4d A = 0 k = 0 F k = if k 0 1 0
46 27 45 jaodan A = 0 k k = 0 F k = if k 0 1 0
47 6 46 syldan A = 0 k 0 F k = if k 0 1 0
48 33 3 eleqtri 0 0
49 48 a1i A = 0 0 0
50 1cnd A = 0 k 0 1
51 fz0sn 0 0 = 0
52 51 eqimss2i 0 0 0
53 52 a1i A = 0 0 0 0
54 47 49 50 53 fsumcvg2 A = 0 seq 0 + F seq 0 + F 0
55 0z 0
56 55 40 seq1i A = 0 seq 0 + F 0 = 1
57 54 56 breqtrd A = 0 seq 0 + F 1