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	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)$$
	efsep.2	$$⊢N=M+1$$
	efsep.3	$$⊢M\in {\mathbb{N}}_0$$
	efsep.4	$$⊢\phi \to A\in ℂ$$
	efsep.5	$$⊢\phi \to B\in ℂ$$
	efsep.6	$$⊢\phi \to {\mathrm{e}}^A=B+\sum _{k\in {\mathbb{Z}}_{\ge M}}F\left(k\right)$$
	efsep.7	$$⊢\phi \to B+\left(\frac{A^M}{M!}\right)=D$$
Assertion	efsep	$$⊢\phi \to {\mathrm{e}}^A=D+\sum _{k\in {\mathbb{Z}}_{\ge N}}F\left(k\right)$$

Proof

Step	Hyp	Ref	Expression
1		efsep.1	$$⊢F=\left(n\in {\mathbb{N}}_0⟼\frac{A^n}{n!}\right)$$
2		efsep.2	$$⊢N=M+1$$
3		efsep.3	$$⊢M\in {\mathbb{N}}_0$$
4		efsep.4	$$⊢\phi \to A\in ℂ$$
5		efsep.5	$$⊢\phi \to B\in ℂ$$
6		efsep.6	$$⊢\phi \to {\mathrm{e}}^A=B+\sum _{k\in {\mathbb{Z}}_{\ge M}}F\left(k\right)$$
7		efsep.7	$$⊢\phi \to B+\left(\frac{A^M}{M!}\right)=D$$
8		eqid	$$⊢{\mathbb{Z}}_{\ge M}={\mathbb{Z}}_{\ge M}$$
9	3	nn0zi	$$⊢M\in \mathbb{Z}$$
10	9	a1i	$$⊢\phi \to M\in \mathbb{Z}$$
11		eqidd	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge M}\right)\to F\left(k\right)=F\left(k\right)$$
12		eluznn0	$$⊢\left(M\in {\mathbb{N}}_0\wedge k\in {\mathbb{Z}}_{\ge M}\right)\to k\in {\mathbb{N}}_0$$
13	3 12	mpan	$$⊢k\in {\mathbb{Z}}_{\ge M}\to k\in {\mathbb{N}}_0$$
14	1	eftval	$$⊢k\in {\mathbb{N}}_0\to F\left(k\right)=\frac{A^k}{k!}$$
15	14	adantl	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to F\left(k\right)=\frac{A^k}{k!}$$
16		eftcl	$$⊢\left(A\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to \frac{A^k}{k!}\in ℂ$$
17	4 16	sylan	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to \frac{A^k}{k!}\in ℂ$$
18	15 17	eqeltrd	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to F\left(k\right)\in ℂ$$
19	13 18	sylan2	$$⊢\left(\phi \wedge k\in {\mathbb{Z}}_{\ge M}\right)\to F\left(k\right)\in ℂ$$
20	1	eftlcvg	$$⊢\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to seqM\left(+,F\right)\in \mathrm{dom}⇝$$
21	4 3 20	sylancl	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$
22	8 10 11 19 21	isum1p	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge M}}F\left(k\right)=F\left(M\right)+\sum _{k\in {\mathbb{Z}}_{\ge \left(M+1\right)}}F\left(k\right)$$
23	1	eftval	$$⊢M\in {\mathbb{N}}_0\to F\left(M\right)=\frac{A^M}{M!}$$
24	3 23	ax-mp	$$⊢F\left(M\right)=\frac{A^M}{M!}$$
25	2	eqcomi	$$⊢M+1=N$$
26	25	fveq2i	$$⊢{\mathbb{Z}}_{\ge \left(M+1\right)}={\mathbb{Z}}_{\ge N}$$
27	26	sumeq1i	$$⊢\sum _{k\in {\mathbb{Z}}_{\ge \left(M+1\right)}}F\left(k\right)=\sum _{k\in {\mathbb{Z}}_{\ge N}}F\left(k\right)$$
28	24 27	oveq12i	$$⊢F\left(M\right)+\sum _{k\in {\mathbb{Z}}_{\ge \left(M+1\right)}}F\left(k\right)=\left(\frac{A^M}{M!}\right)+\sum _{k\in {\mathbb{Z}}_{\ge N}}F\left(k\right)$$
29	22 28	eqtrdi	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge M}}F\left(k\right)=\left(\frac{A^M}{M!}\right)+\sum _{k\in {\mathbb{Z}}_{\ge N}}F\left(k\right)$$
30	29	oveq2d	$$⊢\phi \to B+\sum _{k\in {\mathbb{Z}}_{\ge M}}F\left(k\right)=B+\left(\frac{A^M}{M!}\right)+\sum _{k\in {\mathbb{Z}}_{\ge N}}F\left(k\right)$$
31		eftcl	$$⊢\left(A\in ℂ\wedge M\in {\mathbb{N}}_0\right)\to \frac{A^M}{M!}\in ℂ$$
32	4 3 31	sylancl	$$⊢\phi \to \frac{A^M}{M!}\in ℂ$$
33		peano2nn0	$$⊢M\in {\mathbb{N}}_0\to M+1\in {\mathbb{N}}_0$$
34	3 33	ax-mp	$$⊢M+1\in {\mathbb{N}}_0$$
35	2 34	eqeltri	$$⊢N\in {\mathbb{N}}_0$$
36	1	eftlcl	$$⊢\left(A\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to \sum _{k\in {\mathbb{Z}}_{\ge N}}F\left(k\right)\in ℂ$$
37	4 35 36	sylancl	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge N}}F\left(k\right)\in ℂ$$
38	5 32 37	addassd	$$⊢\phi \to B+\left(\frac{A^M}{M!}\right)+\sum _{k\in {\mathbb{Z}}_{\ge N}}F\left(k\right)=B+\left(\frac{A^M}{M!}\right)+\sum _{k\in {\mathbb{Z}}_{\ge N}}F\left(k\right)$$
39	30 38	eqtr4d	$$⊢\phi \to B+\sum _{k\in {\mathbb{Z}}_{\ge M}}F\left(k\right)=B+\left(\frac{A^M}{M!}\right)+\sum _{k\in {\mathbb{Z}}_{\ge N}}F\left(k\right)$$
40	7	oveq1d	$$⊢\phi \to B+\left(\frac{A^M}{M!}\right)+\sum _{k\in {\mathbb{Z}}_{\ge N}}F\left(k\right)=D+\sum _{k\in {\mathbb{Z}}_{\ge N}}F\left(k\right)$$
41	6 39 40	3eqtrd	$$⊢\phi \to {\mathrm{e}}^A=D+\sum _{k\in {\mathbb{Z}}_{\ge N}}F\left(k\right)$$