Metamath Proof Explorer


Theorem efsep

Description: Separate out the next term of the power series expansion of the exponential function. The last hypothesis allows the separated terms to be rearranged as desired. (Contributed by Paul Chapman, 23-Nov-2007) (Revised by Mario Carneiro, 29-Apr-2014)

Ref Expression
Hypotheses efsep.1 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) / ( ! ‘ 𝑛 ) ) )
efsep.2 𝑁 = ( 𝑀 + 1 )
efsep.3 𝑀 ∈ ℕ0
efsep.4 ( 𝜑𝐴 ∈ ℂ )
efsep.5 ( 𝜑𝐵 ∈ ℂ )
efsep.6 ( 𝜑 → ( exp ‘ 𝐴 ) = ( 𝐵 + Σ 𝑘 ∈ ( ℤ𝑀 ) ( 𝐹𝑘 ) ) )
efsep.7 ( 𝜑 → ( 𝐵 + ( ( 𝐴𝑀 ) / ( ! ‘ 𝑀 ) ) ) = 𝐷 )
Assertion efsep ( 𝜑 → ( exp ‘ 𝐴 ) = ( 𝐷 + Σ 𝑘 ∈ ( ℤ𝑁 ) ( 𝐹𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 efsep.1 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴𝑛 ) / ( ! ‘ 𝑛 ) ) )
2 efsep.2 𝑁 = ( 𝑀 + 1 )
3 efsep.3 𝑀 ∈ ℕ0
4 efsep.4 ( 𝜑𝐴 ∈ ℂ )
5 efsep.5 ( 𝜑𝐵 ∈ ℂ )
6 efsep.6 ( 𝜑 → ( exp ‘ 𝐴 ) = ( 𝐵 + Σ 𝑘 ∈ ( ℤ𝑀 ) ( 𝐹𝑘 ) ) )
7 efsep.7 ( 𝜑 → ( 𝐵 + ( ( 𝐴𝑀 ) / ( ! ‘ 𝑀 ) ) ) = 𝐷 )
8 eqid ( ℤ𝑀 ) = ( ℤ𝑀 )
9 3 nn0zi 𝑀 ∈ ℤ
10 9 a1i ( 𝜑𝑀 ∈ ℤ )
11 eqidd ( ( 𝜑𝑘 ∈ ( ℤ𝑀 ) ) → ( 𝐹𝑘 ) = ( 𝐹𝑘 ) )
12 eluznn0 ( ( 𝑀 ∈ ℕ0𝑘 ∈ ( ℤ𝑀 ) ) → 𝑘 ∈ ℕ0 )
13 3 12 mpan ( 𝑘 ∈ ( ℤ𝑀 ) → 𝑘 ∈ ℕ0 )
14 1 eftval ( 𝑘 ∈ ℕ0 → ( 𝐹𝑘 ) = ( ( 𝐴𝑘 ) / ( ! ‘ 𝑘 ) ) )
15 14 adantl ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝐹𝑘 ) = ( ( 𝐴𝑘 ) / ( ! ‘ 𝑘 ) ) )
16 eftcl ( ( 𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
17 4 16 sylan ( ( 𝜑𝑘 ∈ ℕ0 ) → ( ( 𝐴𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℂ )
18 15 17 eqeltrd ( ( 𝜑𝑘 ∈ ℕ0 ) → ( 𝐹𝑘 ) ∈ ℂ )
19 13 18 sylan2 ( ( 𝜑𝑘 ∈ ( ℤ𝑀 ) ) → ( 𝐹𝑘 ) ∈ ℂ )
20 1 eftlcvg ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
21 4 3 20 sylancl ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
22 8 10 11 19 21 isum1p ( 𝜑 → Σ 𝑘 ∈ ( ℤ𝑀 ) ( 𝐹𝑘 ) = ( ( 𝐹𝑀 ) + Σ 𝑘 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ( 𝐹𝑘 ) ) )
23 1 eftval ( 𝑀 ∈ ℕ0 → ( 𝐹𝑀 ) = ( ( 𝐴𝑀 ) / ( ! ‘ 𝑀 ) ) )
24 3 23 ax-mp ( 𝐹𝑀 ) = ( ( 𝐴𝑀 ) / ( ! ‘ 𝑀 ) )
25 2 eqcomi ( 𝑀 + 1 ) = 𝑁
26 25 fveq2i ( ℤ ‘ ( 𝑀 + 1 ) ) = ( ℤ𝑁 )
27 26 sumeq1i Σ 𝑘 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ( 𝐹𝑘 ) = Σ 𝑘 ∈ ( ℤ𝑁 ) ( 𝐹𝑘 )
28 24 27 oveq12i ( ( 𝐹𝑀 ) + Σ 𝑘 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ( 𝐹𝑘 ) ) = ( ( ( 𝐴𝑀 ) / ( ! ‘ 𝑀 ) ) + Σ 𝑘 ∈ ( ℤ𝑁 ) ( 𝐹𝑘 ) )
29 22 28 eqtrdi ( 𝜑 → Σ 𝑘 ∈ ( ℤ𝑀 ) ( 𝐹𝑘 ) = ( ( ( 𝐴𝑀 ) / ( ! ‘ 𝑀 ) ) + Σ 𝑘 ∈ ( ℤ𝑁 ) ( 𝐹𝑘 ) ) )
30 29 oveq2d ( 𝜑 → ( 𝐵 + Σ 𝑘 ∈ ( ℤ𝑀 ) ( 𝐹𝑘 ) ) = ( 𝐵 + ( ( ( 𝐴𝑀 ) / ( ! ‘ 𝑀 ) ) + Σ 𝑘 ∈ ( ℤ𝑁 ) ( 𝐹𝑘 ) ) ) )
31 eftcl ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐴𝑀 ) / ( ! ‘ 𝑀 ) ) ∈ ℂ )
32 4 3 31 sylancl ( 𝜑 → ( ( 𝐴𝑀 ) / ( ! ‘ 𝑀 ) ) ∈ ℂ )
33 peano2nn0 ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℕ0 )
34 3 33 ax-mp ( 𝑀 + 1 ) ∈ ℕ0
35 2 34 eqeltri 𝑁 ∈ ℕ0
36 1 eftlcl ( ( 𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → Σ 𝑘 ∈ ( ℤ𝑁 ) ( 𝐹𝑘 ) ∈ ℂ )
37 4 35 36 sylancl ( 𝜑 → Σ 𝑘 ∈ ( ℤ𝑁 ) ( 𝐹𝑘 ) ∈ ℂ )
38 5 32 37 addassd ( 𝜑 → ( ( 𝐵 + ( ( 𝐴𝑀 ) / ( ! ‘ 𝑀 ) ) ) + Σ 𝑘 ∈ ( ℤ𝑁 ) ( 𝐹𝑘 ) ) = ( 𝐵 + ( ( ( 𝐴𝑀 ) / ( ! ‘ 𝑀 ) ) + Σ 𝑘 ∈ ( ℤ𝑁 ) ( 𝐹𝑘 ) ) ) )
39 30 38 eqtr4d ( 𝜑 → ( 𝐵 + Σ 𝑘 ∈ ( ℤ𝑀 ) ( 𝐹𝑘 ) ) = ( ( 𝐵 + ( ( 𝐴𝑀 ) / ( ! ‘ 𝑀 ) ) ) + Σ 𝑘 ∈ ( ℤ𝑁 ) ( 𝐹𝑘 ) ) )
40 7 oveq1d ( 𝜑 → ( ( 𝐵 + ( ( 𝐴𝑀 ) / ( ! ‘ 𝑀 ) ) ) + Σ 𝑘 ∈ ( ℤ𝑁 ) ( 𝐹𝑘 ) ) = ( 𝐷 + Σ 𝑘 ∈ ( ℤ𝑁 ) ( 𝐹𝑘 ) ) )
41 6 39 40 3eqtrd ( 𝜑 → ( exp ‘ 𝐴 ) = ( 𝐷 + Σ 𝑘 ∈ ( ℤ𝑁 ) ( 𝐹𝑘 ) ) )