taylth

Description: Taylor's theorem. The Taylor polynomial of a N -times differentiable function is such that the error term goes to zero faster than ( x - B ) ^ N . This is Metamath 100 proof #35. (Contributed by Mario Carneiro, 1-Jan-2017)

	Ref	Expression
Hypotheses	taylth.f	$⊢ φ \to F : A ⟶ ℝ$
	taylth.a	$⊢ φ \to A \subseteq ℝ$
	taylth.d	$⊢ φ \to dom (ℝ D^{n} F) (N) = A$
	taylth.n	$⊢ φ \to N \in ℕ$
	taylth.b	$⊢ φ \to B \in A$
	taylth.t	$⊢ T = N (ℝ Tayl F) B$
	taylth.r	$⊢ R = (x \in (A ∖ \{B\}) ⟼ \frac{F (x) - T (x)}{{(x - B)}^{N}})$
Assertion	taylth	$⊢ φ \to 0 \in (R {lim}_{ℂ} B)$

Proof

Step	Hyp	Ref	Expression
1		taylth.f	$⊢ φ \to F : A ⟶ ℝ$
2		taylth.a	$⊢ φ \to A \subseteq ℝ$
3		taylth.d	$⊢ φ \to dom (ℝ D^{n} F) (N) = A$
4		taylth.n	$⊢ φ \to N \in ℕ$
5		taylth.b	$⊢ φ \to B \in A$
6		taylth.t	$⊢ T = N (ℝ Tayl F) B$
7		taylth.r	$⊢ R = (x \in (A ∖ \{B\}) ⟼ \frac{F (x) - T (x)}{{(x - B)}^{N}})$
8		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
9	8	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
10		ax-resscn	$⊢ ℝ \subseteq ℂ$
11		fss	$⊢ (F : A ⟶ ℝ \land ℝ \subseteq ℂ) \to F : A ⟶ ℂ$
12	1 10 11	sylancl	$⊢ φ \to F : A ⟶ ℂ$
13	1	adantr	$⊢ (φ \land (m \in (1 ..^N) \land 0 \in ((y \in (A ∖ \{B\}) ⟼ \frac{(ℝ D^{n} F) (N - m) (y) - (ℂ D^{n} T) (N - m) (y)}{{(y - B)}^{m}}) {lim}_{ℂ} B))) \to F : A ⟶ ℝ$
14	2	adantr	$⊢ (φ \land (m \in (1 ..^N) \land 0 \in ((y \in (A ∖ \{B\}) ⟼ \frac{(ℝ D^{n} F) (N - m) (y) - (ℂ D^{n} T) (N - m) (y)}{{(y - B)}^{m}}) {lim}_{ℂ} B))) \to A \subseteq ℝ$
15	3	adantr	$⊢ (φ \land (m \in (1 ..^N) \land 0 \in ((y \in (A ∖ \{B\}) ⟼ \frac{(ℝ D^{n} F) (N - m) (y) - (ℂ D^{n} T) (N - m) (y)}{{(y - B)}^{m}}) {lim}_{ℂ} B))) \to dom (ℝ D^{n} F) (N) = A$
16	4	adantr	$⊢ (φ \land (m \in (1 ..^N) \land 0 \in ((y \in (A ∖ \{B\}) ⟼ \frac{(ℝ D^{n} F) (N - m) (y) - (ℂ D^{n} T) (N - m) (y)}{{(y - B)}^{m}}) {lim}_{ℂ} B))) \to N \in ℕ$
17	5	adantr	$⊢ (φ \land (m \in (1 ..^N) \land 0 \in ((y \in (A ∖ \{B\}) ⟼ \frac{(ℝ D^{n} F) (N - m) (y) - (ℂ D^{n} T) (N - m) (y)}{{(y - B)}^{m}}) {lim}_{ℂ} B))) \to B \in A$
18		simprl	$⊢ (φ \land (m \in (1 ..^N) \land 0 \in ((y \in (A ∖ \{B\}) ⟼ \frac{(ℝ D^{n} F) (N - m) (y) - (ℂ D^{n} T) (N - m) (y)}{{(y - B)}^{m}}) {lim}_{ℂ} B))) \to m \in (1 ..^N)$
19		simprr	$⊢ (φ \land (m \in (1 ..^N) \land 0 \in ((y \in (A ∖ \{B\}) ⟼ \frac{(ℝ D^{n} F) (N - m) (y) - (ℂ D^{n} T) (N - m) (y)}{{(y - B)}^{m}}) {lim}_{ℂ} B))) \to 0 \in ((y \in (A ∖ \{B\}) ⟼ \frac{(ℝ D^{n} F) (N - m) (y) - (ℂ D^{n} T) (N - m) (y)}{{(y - B)}^{m}}) {lim}_{ℂ} B)$
20		fveq2	$⊢ y = x \to (ℝ D^{n} F) (N - m) (y) = (ℝ D^{n} F) (N - m) (x)$
21		fveq2	$⊢ y = x \to (ℂ D^{n} T) (N - m) (y) = (ℂ D^{n} T) (N - m) (x)$
22	20 21	oveq12d	$⊢ y = x \to (ℝ D^{n} F) (N - m) (y) - (ℂ D^{n} T) (N - m) (y) = (ℝ D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)$
23		oveq1	$⊢ y = x \to y - B = x - B$
24	23	oveq1d	$⊢ y = x \to {(y - B)}^{m} = {(x - B)}^{m}$
25	22 24	oveq12d	$⊢ y = x \to \frac{(ℝ D^{n} F) (N - m) (y) - (ℂ D^{n} T) (N - m) (y)}{{(y - B)}^{m}} = \frac{(ℝ D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}}$
26	25	cbvmptv	$⊢ (y \in (A ∖ \{B\}) ⟼ \frac{(ℝ D^{n} F) (N - m) (y) - (ℂ D^{n} T) (N - m) (y)}{{(y - B)}^{m}}) = (x \in (A ∖ \{B\}) ⟼ \frac{(ℝ D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}})$
27	26	oveq1i	$⊢ (y \in (A ∖ \{B\}) ⟼ \frac{(ℝ D^{n} F) (N - m) (y) - (ℂ D^{n} T) (N - m) (y)}{{(y - B)}^{m}}) {lim}_{ℂ} B = (x \in (A ∖ \{B\}) ⟼ \frac{(ℝ D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}}) {lim}_{ℂ} B$
28	19 27	eleqtrdi	$⊢ (φ \land (m \in (1 ..^N) \land 0 \in ((y \in (A ∖ \{B\}) ⟼ \frac{(ℝ D^{n} F) (N - m) (y) - (ℂ D^{n} T) (N - m) (y)}{{(y - B)}^{m}}) {lim}_{ℂ} B))) \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(ℝ D^{n} F) (N - m) (x) - (ℂ D^{n} T) (N - m) (x)}{{(x - B)}^{m}}) {lim}_{ℂ} B)$
29	13 14 15 16 17 6 18 28	taylthlem2	$⊢ (φ \land (m \in (1 ..^N) \land 0 \in ((y \in (A ∖ \{B\}) ⟼ \frac{(ℝ D^{n} F) (N - m) (y) - (ℂ D^{n} T) (N - m) (y)}{{(y - B)}^{m}}) {lim}_{ℂ} B))) \to 0 \in ((x \in (A ∖ \{B\}) ⟼ \frac{(ℝ D^{n} F) (N - (m + 1)) (x) - (ℂ D^{n} T) (N - (m + 1)) (x)}{{(x - B)}^{m + 1}}) {lim}_{ℂ} B)$
30	9 12 2 3 4 5 6 7 29	taylthlem1	$⊢ φ \to 0 \in (R {lim}_{ℂ} B)$

Metamath Proof Explorer

Theorem taylth

Proof