Metamath Proof Explorer


Theorem ef4p

Description: Separate out the first four terms of the infinite series expansion of the exponential function. (Contributed by Paul Chapman, 19-Jan-2008) (Revised by Mario Carneiro, 29-Apr-2014)

Ref Expression
Hypothesis ef4p.1 F = n 0 A n n !
Assertion ef4p A e A = 1 + A + A 2 2 + A 3 6 + k 4 F k

Proof

Step Hyp Ref Expression
1 ef4p.1 F = n 0 A n n !
2 df-4 4 = 3 + 1
3 3nn0 3 0
4 id A A
5 ax-1cn 1
6 addcl 1 A 1 + A
7 5 6 mpan A 1 + A
8 sqcl A A 2
9 8 halfcld A A 2 2
10 7 9 addcld A 1 + A + A 2 2
11 df-3 3 = 2 + 1
12 2nn0 2 0
13 df-2 2 = 1 + 1
14 1nn0 1 0
15 5 a1i A 1
16 1e0p1 1 = 0 + 1
17 0nn0 0 0
18 0cnd A 0
19 1 efval2 A e A = k 0 F k
20 nn0uz 0 = 0
21 20 sumeq1i k 0 F k = k 0 F k
22 19 21 eqtr2di A k 0 F k = e A
23 22 oveq2d A 0 + k 0 F k = 0 + e A
24 efcl A e A
25 24 addid2d A 0 + e A = e A
26 23 25 eqtr2d A e A = 0 + k 0 F k
27 eft0val A A 0 0 ! = 1
28 27 oveq2d A 0 + A 0 0 ! = 0 + 1
29 0p1e1 0 + 1 = 1
30 28 29 eqtrdi A 0 + A 0 0 ! = 1
31 1 16 17 4 18 26 30 efsep A e A = 1 + k 1 F k
32 exp1 A A 1 = A
33 fac1 1 ! = 1
34 33 a1i A 1 ! = 1
35 32 34 oveq12d A A 1 1 ! = A 1
36 div1 A A 1 = A
37 35 36 eqtrd A A 1 1 ! = A
38 37 oveq2d A 1 + A 1 1 ! = 1 + A
39 1 13 14 4 15 31 38 efsep A e A = 1 + A + k 2 F k
40 fac2 2 ! = 2
41 40 oveq2i A 2 2 ! = A 2 2
42 41 oveq2i 1 + A + A 2 2 ! = 1 + A + A 2 2
43 42 a1i A 1 + A + A 2 2 ! = 1 + A + A 2 2
44 1 11 12 4 7 39 43 efsep A e A = 1 + A + A 2 2 + k 3 F k
45 fac3 3 ! = 6
46 45 oveq2i A 3 3 ! = A 3 6
47 46 oveq2i 1 + A + A 2 2 + A 3 3 ! = 1 + A + A 2 2 + A 3 6
48 47 a1i A 1 + A + A 2 2 + A 3 3 ! = 1 + A + A 2 2 + A 3 6
49 1 2 3 4 10 44 48 efsep A e A = 1 + A + A 2 2 + A 3 6 + k 4 F k