Theorem effsumlt

Description: The partial sums of the series expansion of the exponential function at a positive real number are bounded by the value of the function. (Contributed by Paul Chapman, 21-Aug-2007) (Revised by Mario Carneiro, 29-Apr-2014)

	Ref	Expression
Hypotheses	effsumlt.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
	effsumlt.2	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
	effsumlt.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	effsumlt	⊢ ( 𝜑 → ( seq 0 ( + , 𝐹 ) ‘ 𝑁 ) < ( exp ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		effsumlt.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
2		effsumlt.2	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
3		effsumlt.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
5		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
6	1	eftval	⊢ ( 𝑘 ∈ ℕ0 → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
7	6	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) )
8	2	rpred	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
9		reeftcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
10	8 9	sylan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ )
11	7 10	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
12	4 5 11	serfre	⊢ ( 𝜑 → seq 0 ( + , 𝐹 ) : ℕ0 ⟶ ℝ )
13	12 3	ffvelrnd	⊢ ( 𝜑 → ( seq 0 ( + , 𝐹 ) ‘ 𝑁 ) ∈ ℝ )
14		eqid	⊢ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) = ( ℤ≥ ‘ ( 𝑁 + 1 ) )
15		peano2nn0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
16	3 15	syl	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
17		eqidd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
18		nn0z	⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℤ )
19		rpexpcl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑘 ∈ ℤ ) → ( 𝐴 ↑ 𝑘 ) ∈ ℝ+ )
20	2 18 19	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℝ+ )
21		faccl	⊢ ( 𝑘 ∈ ℕ0 → ( ! ‘ 𝑘 ) ∈ ℕ )
22	21	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑘 ) ∈ ℕ )
23	22	nnrpd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ! ‘ 𝑘 ) ∈ ℝ+ )
24	20 23	rpdivcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( ( 𝐴 ↑ 𝑘 ) / ( ! ‘ 𝑘 ) ) ∈ ℝ+ )
25	7 24	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ+ )
26	8	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
27	1	efcllem	⊢ ( 𝐴 ∈ ℂ → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )
28	26 27	syl	⊢ ( 𝜑 → seq 0 ( + , 𝐹 ) ∈ dom ⇝ )
29	4 14 16 17 25 28	isumrpcl	⊢ ( 𝜑 → Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ∈ ℝ+ )
30	13 29	ltaddrpd	⊢ ( 𝜑 → ( seq 0 ( + , 𝐹 ) ‘ 𝑁 ) < ( ( seq 0 ( + , 𝐹 ) ‘ 𝑁 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) )
31	1	efval2	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ 𝐴 ) = Σ 𝑘 ∈ ℕ0 ( 𝐹 ‘ 𝑘 ) )
32	26 31	syl	⊢ ( 𝜑 → ( exp ‘ 𝐴 ) = Σ 𝑘 ∈ ℕ0 ( 𝐹 ‘ 𝑘 ) )
33	11	recnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
34	4 14 16 17 33 28	isumsplit	⊢ ( 𝜑 → Σ 𝑘 ∈ ℕ0 ( 𝐹 ‘ 𝑘 ) = ( Σ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) )
35	3	nn0cnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
36		ax-1cn	⊢ 1 ∈ ℂ
37		pncan	⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
38	35 36 37	sylancl	⊢ ( 𝜑 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
39	38	oveq2d	⊢ ( 𝜑 → ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) = ( 0 ... 𝑁 ) )
40	39	sumeq1d	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) )
41		eqidd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑘 ) )
42	3 4	eleqtrdi	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 0 ) )
43		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℕ0 )
44	43 33	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
45	41 42 44	fsumser	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝐹 ‘ 𝑘 ) = ( seq 0 ( + , 𝐹 ) ‘ 𝑁 ) )
46	40 45	eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) = ( seq 0 ( + , 𝐹 ) ‘ 𝑁 ) )
47	46	oveq1d	⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... ( ( 𝑁 + 1 ) − 1 ) ) ( 𝐹 ‘ 𝑘 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) = ( ( seq 0 ( + , 𝐹 ) ‘ 𝑁 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) )
48	32 34 47	3eqtrd	⊢ ( 𝜑 → ( exp ‘ 𝐴 ) = ( ( seq 0 ( + , 𝐹 ) ‘ 𝑁 ) + Σ 𝑘 ∈ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ( 𝐹 ‘ 𝑘 ) ) )
49	30 48	breqtrrd	⊢ ( 𝜑 → ( seq 0 ( + , 𝐹 ) ‘ 𝑁 ) < ( exp ‘ 𝐴 ) )