Theorem reeftlcl

Description: Closure of the sum of an infinite tail of the series defining the exponential function. (Contributed by Paul Chapman, 17-Jan-2008) (Revised by Mario Carneiro, 30-Apr-2014)

	Ref	Expression
Hypothesis	eftl.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
Assertion	reeftlcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		eftl.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
2		eqid	⊢ ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ 𝑀 )
3		nn0z	⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ )
4	3	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) → 𝑀 ∈ ℤ )
5		eqidd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
6		eluznn0	⊢ ( ( 𝑀 ∈ ℕ0 ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ℕ0 )
7	6	adantll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑘 ∈ ℕ0 )
8	1	eftval	⊢ ( 𝑘 ∈ ℕ0 → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
9	7 8	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
10		simpll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝐴 ∈ ℝ )
11		reeftcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
12	10 7 11	syl2anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
13	9 12	eqeltrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
14		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
15	1	eftlcvg	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℕ0 ) → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
16	14 15	sylan	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
17	2 4 5 13 16	isumrecl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℕ0 ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ )