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 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) / ( ! ‘ 𝑛 ) ) )
Assertion ef4p ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) = ( ( ( ( 1 + 𝐴 ) + ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / 6 ) ) + Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( 𝐹𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 ef4p.1 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) / ( ! ‘ 𝑛 ) ) )
2 df-4 4 = ( 3 + 1 )
3 3nn0 3 ∈ ℕ0
4 id ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
5 ax-1cn 1 ∈ ℂ
6 addcl ( ( 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 1 + 𝐴 ) ∈ ℂ )
7 5 6 mpan ( 𝐴 ∈ ℂ → ( 1 + 𝐴 ) ∈ ℂ )
8 sqcl ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 2 ) ∈ ℂ )
9 8 halfcld ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 2 ) / 2 ) ∈ ℂ )
10 7 9 addcld ( 𝐴 ∈ ℂ → ( ( 1 + 𝐴 ) + ( ( 𝐴 ↑ 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 ( 𝐴 ∈ ℂ → 1 ∈ ℂ )
16 1e0p1 1 = ( 0 + 1 )
17 0nn0 0 ∈ ℕ0
18 0cnd ( 𝐴 ∈ ℂ → 0 ∈ ℂ )
19 1 efval2 ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) = Σ 𝑘 ∈ ℕ0 ( 𝐹𝑘 ) )
20 nn0uz 0 = ( ℤ ‘ 0 )
21 20 sumeq1i Σ 𝑘 ∈ ℕ0 ( 𝐹𝑘 ) = Σ 𝑘 ∈ ( ℤ ‘ 0 ) ( 𝐹𝑘 )
22 19 21 eqtr2di ( 𝐴 ∈ ℂ → Σ 𝑘 ∈ ( ℤ ‘ 0 ) ( 𝐹𝑘 ) = ( exp ‘ 𝐴 ) )
23 22 oveq2d ( 𝐴 ∈ ℂ → ( 0 + Σ 𝑘 ∈ ( ℤ ‘ 0 ) ( 𝐹𝑘 ) ) = ( 0 + ( exp ‘ 𝐴 ) ) )
24 efcl ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) ∈ ℂ )
25 24 addid2d ( 𝐴 ∈ ℂ → ( 0 + ( exp ‘ 𝐴 ) ) = ( exp ‘ 𝐴 ) )
26 23 25 eqtr2d ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) = ( 0 + Σ 𝑘 ∈ ( ℤ ‘ 0 ) ( 𝐹𝑘 ) ) )
27 eft0val ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 0 ) / ( ! ‘ 0 ) ) = 1 )
28 27 oveq2d ( 𝐴 ∈ ℂ → ( 0 + ( ( 𝐴 ↑ 0 ) / ( ! ‘ 0 ) ) ) = ( 0 + 1 ) )
29 0p1e1 ( 0 + 1 ) = 1
30 28 29 eqtrdi ( 𝐴 ∈ ℂ → ( 0 + ( ( 𝐴 ↑ 0 ) / ( ! ‘ 0 ) ) ) = 1 )
31 1 16 17 4 18 26 30 efsep ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) = ( 1 + Σ 𝑘 ∈ ( ℤ ‘ 1 ) ( 𝐹𝑘 ) ) )
32 exp1 ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 1 ) = 𝐴 )
33 fac1 ( ! ‘ 1 ) = 1
34 33 a1i ( 𝐴 ∈ ℂ → ( ! ‘ 1 ) = 1 )
35 32 34 oveq12d ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 1 ) / ( ! ‘ 1 ) ) = ( 𝐴 / 1 ) )
36 div1 ( 𝐴 ∈ ℂ → ( 𝐴 / 1 ) = 𝐴 )
37 35 36 eqtrd ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 1 ) / ( ! ‘ 1 ) ) = 𝐴 )
38 37 oveq2d ( 𝐴 ∈ ℂ → ( 1 + ( ( 𝐴 ↑ 1 ) / ( ! ‘ 1 ) ) ) = ( 1 + 𝐴 ) )
39 1 13 14 4 15 31 38 efsep ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) = ( ( 1 + 𝐴 ) + Σ 𝑘 ∈ ( ℤ ‘ 2 ) ( 𝐹𝑘 ) ) )
40 fac2 ( ! ‘ 2 ) = 2
41 40 oveq2i ( ( 𝐴 ↑ 2 ) / ( ! ‘ 2 ) ) = ( ( 𝐴 ↑ 2 ) / 2 )
42 41 oveq2i ( ( 1 + 𝐴 ) + ( ( 𝐴 ↑ 2 ) / ( ! ‘ 2 ) ) ) = ( ( 1 + 𝐴 ) + ( ( 𝐴 ↑ 2 ) / 2 ) )
43 42 a1i ( 𝐴 ∈ ℂ → ( ( 1 + 𝐴 ) + ( ( 𝐴 ↑ 2 ) / ( ! ‘ 2 ) ) ) = ( ( 1 + 𝐴 ) + ( ( 𝐴 ↑ 2 ) / 2 ) ) )
44 1 11 12 4 7 39 43 efsep ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) = ( ( ( 1 + 𝐴 ) + ( ( 𝐴 ↑ 2 ) / 2 ) ) + Σ 𝑘 ∈ ( ℤ ‘ 3 ) ( 𝐹𝑘 ) ) )
45 fac3 ( ! ‘ 3 ) = 6
46 45 oveq2i ( ( 𝐴 ↑ 3 ) / ( ! ‘ 3 ) ) = ( ( 𝐴 ↑ 3 ) / 6 )
47 46 oveq2i ( ( ( 1 + 𝐴 ) + ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / ( ! ‘ 3 ) ) ) = ( ( ( 1 + 𝐴 ) + ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / 6 ) )
48 47 a1i ( 𝐴 ∈ ℂ → ( ( ( 1 + 𝐴 ) + ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / ( ! ‘ 3 ) ) ) = ( ( ( 1 + 𝐴 ) + ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / 6 ) ) )
49 1 2 3 4 10 44 48 efsep ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) = ( ( ( ( 1 + 𝐴 ) + ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( ( 𝐴 ↑ 3 ) / 6 ) ) + Σ 𝑘 ∈ ( ℤ ‘ 4 ) ( 𝐹𝑘 ) ) )