Metamath Proof Explorer


Theorem efi4p

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, 30-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 efi4p.1 F = n 0 i A n n !
2 ax-icn i
3 mulcl i A i A
4 2 3 mpan A i A
5 1 ef4p i A e i A = 1 + i A + i A 2 2 + i A 3 6 + k 4 F k
6 4 5 syl A e i A = 1 + i A + i A 2 2 + i A 3 6 + k 4 F k
7 ax-1cn 1
8 addcl 1 i A 1 + i A
9 7 4 8 sylancr A 1 + i A
10 4 sqcld A i A 2
11 10 halfcld A i A 2 2
12 3nn0 3 0
13 expcl i A 3 0 i A 3
14 4 12 13 sylancl A i A 3
15 6cn 6
16 6re 6
17 6pos 0 < 6
18 16 17 gt0ne0ii 6 0
19 divcl i A 3 6 6 0 i A 3 6
20 15 18 19 mp3an23 i A 3 i A 3 6
21 14 20 syl A i A 3 6
22 9 11 21 addassd A 1 + i A + i A 2 2 + i A 3 6 = 1 + i A + i A 2 2 + i A 3 6
23 7 a1i A 1
24 23 4 11 21 add4d A 1 + i A + i A 2 2 + i A 3 6 = 1 + i A 2 2 + i A + i A 3 6
25 2nn0 2 0
26 mulexp i A 2 0 i A 2 = i 2 A 2
27 2 25 26 mp3an13 A i A 2 = i 2 A 2
28 i2 i 2 = 1
29 28 oveq1i i 2 A 2 = -1 A 2
30 29 a1i A i 2 A 2 = -1 A 2
31 sqcl A A 2
32 31 mulm1d A -1 A 2 = A 2
33 27 30 32 3eqtrd A i A 2 = A 2
34 33 oveq1d A i A 2 2 = A 2 2
35 2cn 2
36 2ne0 2 0
37 divneg A 2 2 2 0 A 2 2 = A 2 2
38 35 36 37 mp3an23 A 2 A 2 2 = A 2 2
39 31 38 syl A A 2 2 = A 2 2
40 34 39 eqtr4d A i A 2 2 = A 2 2
41 40 oveq2d A 1 + i A 2 2 = 1 + A 2 2
42 31 halfcld A A 2 2
43 negsub 1 A 2 2 1 + A 2 2 = 1 A 2 2
44 7 42 43 sylancr A 1 + A 2 2 = 1 A 2 2
45 41 44 eqtrd A 1 + i A 2 2 = 1 A 2 2
46 mulexp i A 3 0 i A 3 = i 3 A 3
47 2 12 46 mp3an13 A i A 3 = i 3 A 3
48 i3 i 3 = i
49 48 oveq1i i 3 A 3 = i A 3
50 47 49 eqtrdi A i A 3 = i A 3
51 50 oveq1d A i A 3 6 = i A 3 6
52 expcl A 3 0 A 3
53 12 52 mpan2 A A 3
54 negicn i
55 15 18 pm3.2i 6 6 0
56 divass i A 3 6 6 0 i A 3 6 = i A 3 6
57 54 55 56 mp3an13 A 3 i A 3 6 = i A 3 6
58 53 57 syl A i A 3 6 = i A 3 6
59 divcl A 3 6 6 0 A 3 6
60 15 18 59 mp3an23 A 3 A 3 6
61 53 60 syl A A 3 6
62 mulneg12 i A 3 6 i A 3 6 = i A 3 6
63 2 61 62 sylancr A i A 3 6 = i A 3 6
64 51 58 63 3eqtrd A i A 3 6 = i A 3 6
65 64 oveq2d A i A + i A 3 6 = i A + i A 3 6
66 61 negcld A A 3 6
67 adddi i A A 3 6 i A + A 3 6 = i A + i A 3 6
68 2 67 mp3an1 A A 3 6 i A + A 3 6 = i A + i A 3 6
69 66 68 mpdan A i A + A 3 6 = i A + i A 3 6
70 negsub A A 3 6 A + A 3 6 = A A 3 6
71 61 70 mpdan A A + A 3 6 = A A 3 6
72 71 oveq2d A i A + A 3 6 = i A A 3 6
73 65 69 72 3eqtr2d A i A + i A 3 6 = i A A 3 6
74 45 73 oveq12d A 1 + i A 2 2 + i A + i A 3 6 = 1 - A 2 2 + i A A 3 6
75 22 24 74 3eqtrd A 1 + i A + i A 2 2 + i A 3 6 = 1 - A 2 2 + i A A 3 6
76 75 oveq1d A 1 + i A + i A 2 2 + i A 3 6 + k 4 F k = 1 A 2 2 + i A A 3 6 + k 4 F k
77 6 76 eqtrd A e i A = 1 A 2 2 + i A A 3 6 + k 4 F k