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	$⊢ F = (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})$
	effsumlt.2	$⊢ φ \to A \in ℝ^{+}$
	effsumlt.3	$⊢ φ \to N \in ℕ_{0}$
Assertion	effsumlt	$⊢ φ \to seq 0 (+ F) (N) < e^{A}$

Proof

Step	Hyp	Ref	Expression
1		effsumlt.1	$⊢ F = (n \in ℕ_{0} ⟼ \frac{A^{n}}{n!})$
2		effsumlt.2	$⊢ φ \to A \in ℝ^{+}$
3		effsumlt.3	$⊢ φ \to N \in ℕ_{0}$
4		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
5		0zd	$⊢ φ \to 0 \in ℤ$
6	1	eftval	$⊢ k \in ℕ_{0} \to F (k) = \frac{A^{k}}{k!}$
7	6	adantl	$⊢ (φ \land k \in ℕ_{0}) \to F (k) = \frac{A^{k}}{k!}$
8	2	rpred	$⊢ φ \to A \in ℝ$
9		reeftcl	$⊢ (A \in ℝ \land k \in ℕ_{0}) \to \frac{A^{k}}{k!} \in ℝ$
10	8 9	sylan	$⊢ (φ \land k \in ℕ_{0}) \to \frac{A^{k}}{k!} \in ℝ$
11	7 10	eqeltrd	$⊢ (φ \land k \in ℕ_{0}) \to F (k) \in ℝ$
12	4 5 11	serfre	$⊢ φ \to seq 0 (+ F) : ℕ_{0} ⟶ ℝ$
13	12 3	ffvelcdmd	$⊢ φ \to seq 0 (+ F) (N) \in ℝ$
14		eqid	$⊢ ℤ_{\geq (N + 1)} = ℤ_{\geq (N + 1)}$
15		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
16	3 15	syl	$⊢ φ \to N + 1 \in ℕ_{0}$
17		eqidd	$⊢ (φ \land k \in ℕ_{0}) \to F (k) = F (k)$
18		nn0z	$⊢ k \in ℕ_{0} \to k \in ℤ$
19		rpexpcl	$⊢ (A \in ℝ^{+} \land k \in ℤ) \to A^{k} \in ℝ^{+}$
20	2 18 19	syl2an	$⊢ (φ \land k \in ℕ_{0}) \to A^{k} \in ℝ^{+}$
21		faccl	$⊢ k \in ℕ_{0} \to k! \in ℕ$
22	21	adantl	$⊢ (φ \land k \in ℕ_{0}) \to k! \in ℕ$
23	22	nnrpd	$⊢ (φ \land k \in ℕ_{0}) \to k! \in ℝ^{+}$
24	20 23	rpdivcld	$⊢ (φ \land k \in ℕ_{0}) \to \frac{A^{k}}{k!} \in ℝ^{+}$
25	7 24	eqeltrd	$⊢ (φ \land k \in ℕ_{0}) \to F (k) \in ℝ^{+}$
26	8	recnd	$⊢ φ \to A \in ℂ$
27	1	efcllem	$⊢ A \in ℂ \to seq 0 (+ F) \in dom ⇝$
28	26 27	syl	$⊢ φ \to seq 0 (+ F) \in dom ⇝$
29	4 14 16 17 25 28	isumrpcl	$⊢ φ \to \sum_{k \in ℤ_{\geq (N + 1)}} F (k) \in ℝ^{+}$
30	13 29	ltaddrpd	$⊢ φ \to seq 0 (+ F) (N) < seq 0 (+ F) (N) + \sum_{k \in ℤ_{\geq (N + 1)}} F (k)$
31	1	efval2	$⊢ A \in ℂ \to e^{A} = \sum_{k \in ℕ_{0}} F (k)$
32	26 31	syl	$⊢ φ \to e^{A} = \sum_{k \in ℕ_{0}} F (k)$
33	11	recnd	$⊢ (φ \land k \in ℕ_{0}) \to F (k) \in ℂ$
34	4 14 16 17 33 28	isumsplit	$⊢ φ \to \sum_{k \in ℕ_{0}} F (k) = \sum_{k = 0}^{N + 1 - 1} F (k) + \sum_{k \in ℤ_{\geq (N + 1)}} F (k)$
35	3	nn0cnd	$⊢ φ \to N \in ℂ$
36		ax-1cn	$⊢ 1 \in ℂ$
37		pncan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N + 1 - 1 = N$
38	35 36 37	sylancl	$⊢ φ \to N + 1 - 1 = N$
39	38	oveq2d	$⊢ φ \to (0 \dots N + 1 - 1) = (0 \dots N)$
40	39	sumeq1d	$⊢ φ \to \sum_{k = 0}^{N + 1 - 1} F (k) = \sum_{k = 0}^{N} F (k)$
41		eqidd	$⊢ (φ \land k \in (0 \dots N)) \to F (k) = F (k)$
42	3 4	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 0}$
43		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
44	43 33	sylan2	$⊢ (φ \land k \in (0 \dots N)) \to F (k) \in ℂ$
45	41 42 44	fsumser	$⊢ φ \to \sum_{k = 0}^{N} F (k) = seq 0 (+ F) (N)$
46	40 45	eqtrd	$⊢ φ \to \sum_{k = 0}^{N + 1 - 1} F (k) = seq 0 (+ F) (N)$
47	46	oveq1d	$⊢ φ \to \sum_{k = 0}^{N + 1 - 1} F (k) + \sum_{k \in ℤ_{\geq (N + 1)}} F (k) = seq 0 (+ F) (N) + \sum_{k \in ℤ_{\geq (N + 1)}} F (k)$
48	32 34 47	3eqtrd	$⊢ φ \to e^{A} = seq 0 (+ F) (N) + \sum_{k \in ℤ_{\geq (N + 1)}} F (k)$
49	30 48	breqtrrd	$⊢ φ \to seq 0 (+ F) (N) < e^{A}$

Metamath Proof Explorer

Theorem effsumlt

Proof