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 ‘ 𝐴 ) = ( 𝐷 + Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑁 ) ( 𝐹 ‘ 𝑘 ) ) )