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 syl6req ⊢ ( 𝐴 ∈ ℂ → Σ 𝑘 ∈ ( ℤ≥ ‘ 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 syl6eq ⊢ ( 𝐴 ∈ ℂ → ( 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 ) ( 𝐹 ‘ 𝑘 ) ) )