taylply2

Description: The Taylor polynomial is a polynomial of degree (at most) N . This version of taylply shows that the coefficients of T are in a subring of the complex numbers. (Contributed by Mario Carneiro, 1-Jan-2017)

	Ref	Expression
Hypotheses	taylpfval.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	taylpfval.f	$⊢ φ \to F : A ⟶ ℂ$
	taylpfval.a	$⊢ φ \to A \subseteq S$
	taylpfval.n	$⊢ φ \to N \in ℕ_{0}$
	taylpfval.b	$⊢ φ \to B \in dom (S D^{n} F) (N)$
	taylpfval.t	$⊢ T = N (S Tayl F) B$
	taylply2.1	$⊢ φ \to D \in SubRing (ℂ_{fld})$
	taylply2.2	$⊢ φ \to B \in D$
	taylply2.3	$⊢ (φ \land k \in (0 \dots N)) \to \frac{(S D^{n} F) (k) (B)}{k!} \in D$
Assertion	taylply2	$⊢ φ \to (T \in Poly (D) \land \deg (T) \leq N)$

Proof

Step	Hyp	Ref	Expression
1		taylpfval.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		taylpfval.f	$⊢ φ \to F : A ⟶ ℂ$
3		taylpfval.a	$⊢ φ \to A \subseteq S$
4		taylpfval.n	$⊢ φ \to N \in ℕ_{0}$
5		taylpfval.b	$⊢ φ \to B \in dom (S D^{n} F) (N)$
6		taylpfval.t	$⊢ T = N (S Tayl F) B$
7		taylply2.1	$⊢ φ \to D \in SubRing (ℂ_{fld})$
8		taylply2.2	$⊢ φ \to B \in D$
9		taylply2.3	$⊢ (φ \land k \in (0 \dots N)) \to \frac{(S D^{n} F) (k) (B)}{k!} \in D$
10	1 2 3 4 5 6	taylpfval	$⊢ φ \to T = (x \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})$
11		simpr	$⊢ (φ \land x \in ℂ) \to x \in ℂ$
12		cnex	$⊢ ℂ \in V$
13	12	a1i	$⊢ φ \to ℂ \in V$
14		elpm2r	$⊢ ((ℂ \in V \land S \in \{ℝ, ℂ\}) \land (F : A ⟶ ℂ \land A \subseteq S)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
15	13 1 2 3 14	syl22anc	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} S)$
16		dvnbss	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land N \in ℕ_{0}) \to dom (S D^{n} F) (N) \subseteq dom F$
17	1 15 4 16	syl3anc	$⊢ φ \to dom (S D^{n} F) (N) \subseteq dom F$
18	2 17	fssdmd	$⊢ φ \to dom (S D^{n} F) (N) \subseteq A$
19		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
20	1 19	syl	$⊢ φ \to S \subseteq ℂ$
21	3 20	sstrd	$⊢ φ \to A \subseteq ℂ$
22	18 21	sstrd	$⊢ φ \to dom (S D^{n} F) (N) \subseteq ℂ$
23	22 5	sseldd	$⊢ φ \to B \in ℂ$
24	23	adantr	$⊢ (φ \land x \in ℂ) \to B \in ℂ$
25	11 24	subcld	$⊢ (φ \land x \in ℂ) \to x - B \in ℂ$
26		df-idp	$⊢ X^{p} = {I ↾}_{ℂ}$
27		mptresid	$⊢ {I ↾}_{ℂ} = (x \in ℂ ⟼ x)$
28	26 27	eqtri	$⊢ X^{p} = (x \in ℂ ⟼ x)$
29	28	a1i	$⊢ φ \to X^{p} = (x \in ℂ ⟼ x)$
30		fconstmpt	$⊢ ℂ \times \{B\} = (x \in ℂ ⟼ B)$
31	30	a1i	$⊢ φ \to ℂ \times \{B\} = (x \in ℂ ⟼ B)$
32	13 11 24 29 31	offval2	$⊢ φ \to X^{p} -_{f} (ℂ \times \{B\}) = (x \in ℂ ⟼ x - B)$
33		eqidd	$⊢ φ \to (y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k}) = (y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k})$
34		oveq1	$⊢ y = x - B \to y^{k} = {(x - B)}^{k}$
35	34	oveq2d	$⊢ y = x - B \to (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k} = (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}$
36	35	sumeq2sdv	$⊢ y = x - B \to \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k} = \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k}$
37	25 32 33 36	fmptco	$⊢ φ \to (y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k}) \circ (X^{p} -_{f} (ℂ \times \{B\})) = (x \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) {(x - B)}^{k})$
38	10 37	eqtr4d	$⊢ φ \to T = (y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k}) \circ (X^{p} -_{f} (ℂ \times \{B\}))$
39		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
40	39	subrgss	$⊢ D \in SubRing (ℂ_{fld}) \to D \subseteq ℂ$
41	7 40	syl	$⊢ φ \to D \subseteq ℂ$
42	41 4 9	elplyd	$⊢ φ \to (y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k}) \in Poly (D)$
43		cnfld1	$⊢ 1 = 1_{ℂ_{fld}}$
44	43	subrg1cl	$⊢ D \in SubRing (ℂ_{fld}) \to 1 \in D$
45	7 44	syl	$⊢ φ \to 1 \in D$
46		plyid	$⊢ (D \subseteq ℂ \land 1 \in D) \to X^{p} \in Poly (D)$
47	41 45 46	syl2anc	$⊢ φ \to X^{p} \in Poly (D)$
48		plyconst	$⊢ (D \subseteq ℂ \land B \in D) \to ℂ \times \{B\} \in Poly (D)$
49	41 8 48	syl2anc	$⊢ φ \to ℂ \times \{B\} \in Poly (D)$
50		subrgsubg	$⊢ D \in SubRing (ℂ_{fld}) \to D \in SubGrp (ℂ_{fld})$
51	7 50	syl	$⊢ φ \to D \in SubGrp (ℂ_{fld})$
52		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
53	52	subgcl	$⊢ (D \in SubGrp (ℂ_{fld}) \land u \in D \land v \in D) \to u + v \in D$
54	53	3expb	$⊢ (D \in SubGrp (ℂ_{fld}) \land (u \in D \land v \in D)) \to u + v \in D$
55	51 54	sylan	$⊢ (φ \land (u \in D \land v \in D)) \to u + v \in D$
56		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
57	56	subrgmcl	$⊢ (D \in SubRing (ℂ_{fld}) \land u \in D \land v \in D) \to u v \in D$
58	57	3expb	$⊢ (D \in SubRing (ℂ_{fld}) \land (u \in D \land v \in D)) \to u v \in D$
59	7 58	sylan	$⊢ (φ \land (u \in D \land v \in D)) \to u v \in D$
60		ax-1cn	$⊢ 1 \in ℂ$
61		cnfldneg	$⊢ 1 \in ℂ \to {inv}_{g} (ℂ_{fld}) (1) = - 1$
62	60 61	ax-mp	$⊢ {inv}_{g} (ℂ_{fld}) (1) = - 1$
63		eqid	$⊢ {inv}_{g} (ℂ_{fld}) = {inv}_{g} (ℂ_{fld})$
64	63	subginvcl	$⊢ (D \in SubGrp (ℂ_{fld}) \land 1 \in D) \to {inv}_{g} (ℂ_{fld}) (1) \in D$
65	51 45 64	syl2anc	$⊢ φ \to {inv}_{g} (ℂ_{fld}) (1) \in D$
66	62 65	eqeltrrid	$⊢ φ \to - 1 \in D$
67	47 49 55 59 66	plysub	$⊢ φ \to X^{p} -_{f} (ℂ \times \{B\}) \in Poly (D)$
68	42 67 55 59	plyco	$⊢ φ \to (y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k}) \circ (X^{p} -_{f} (ℂ \times \{B\})) \in Poly (D)$
69	38 68	eqeltrd	$⊢ φ \to T \in Poly (D)$
70	38	fveq2d	$⊢ φ \to \deg (T) = \deg ((y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k}) \circ (X^{p} -_{f} (ℂ \times \{B\})))$
71		eqid	$⊢ \deg ((y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k})) = \deg ((y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k}))$
72		eqid	$⊢ \deg (X^{p} -_{f} (ℂ \times \{B\})) = \deg (X^{p} -_{f} (ℂ \times \{B\}))$
73	71 72 42 67	dgrco	$⊢ φ \to \deg ((y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k}) \circ (X^{p} -_{f} (ℂ \times \{B\}))) = \deg ((y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k})) \deg (X^{p} -_{f} (ℂ \times \{B\}))$
74		eqid	$⊢ X^{p} -_{f} (ℂ \times \{B\}) = X^{p} -_{f} (ℂ \times \{B\})$
75	74	plyremlem	$⊢ B \in ℂ \to (X^{p} -_{f} (ℂ \times \{B\}) \in Poly (ℂ) \land \deg (X^{p} -_{f} (ℂ \times \{B\})) = 1 \land {(X^{p} -_{f} (ℂ \times \{B\}))}^{-1} [\{0\}] = \{B\})$
76	23 75	syl	$⊢ φ \to (X^{p} -_{f} (ℂ \times \{B\}) \in Poly (ℂ) \land \deg (X^{p} -_{f} (ℂ \times \{B\})) = 1 \land {(X^{p} -_{f} (ℂ \times \{B\}))}^{-1} [\{0\}] = \{B\})$
77	76	simp2d	$⊢ φ \to \deg (X^{p} -_{f} (ℂ \times \{B\})) = 1$
78	77	oveq2d	$⊢ φ \to \deg ((y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k})) \deg (X^{p} -_{f} (ℂ \times \{B\})) = \deg ((y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k})) \cdot 1$
79		dgrcl	$⊢ (y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k}) \in Poly (D) \to \deg ((y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k})) \in ℕ_{0}$
80	42 79	syl	$⊢ φ \to \deg ((y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k})) \in ℕ_{0}$
81	80	nn0cnd	$⊢ φ \to \deg ((y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k})) \in ℂ$
82	81	mulridd	$⊢ φ \to \deg ((y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k})) \cdot 1 = \deg ((y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k}))$
83	78 82	eqtrd	$⊢ φ \to \deg ((y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k})) \deg (X^{p} -_{f} (ℂ \times \{B\})) = \deg ((y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k}))$
84	70 73 83	3eqtrd	$⊢ φ \to \deg (T) = \deg ((y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k}))$
85	1	adantr	$⊢ (φ \land k \in (0 \dots N)) \to S \in \{ℝ, ℂ\}$
86	15	adantr	$⊢ (φ \land k \in (0 \dots N)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
87		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
88	87	adantl	$⊢ (φ \land k \in (0 \dots N)) \to k \in ℕ_{0}$
89		dvnf	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land k \in ℕ_{0}) \to (S D^{n} F) (k) : dom (S D^{n} F) (k) ⟶ ℂ$
90	85 86 88 89	syl3anc	$⊢ (φ \land k \in (0 \dots N)) \to (S D^{n} F) (k) : dom (S D^{n} F) (k) ⟶ ℂ$
91		simpr	$⊢ (φ \land k \in (0 \dots N)) \to k \in (0 \dots N)$
92		dvn2bss	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land k \in (0 \dots N)) \to dom (S D^{n} F) (N) \subseteq dom (S D^{n} F) (k)$
93	85 86 91 92	syl3anc	$⊢ (φ \land k \in (0 \dots N)) \to dom (S D^{n} F) (N) \subseteq dom (S D^{n} F) (k)$
94	5	adantr	$⊢ (φ \land k \in (0 \dots N)) \to B \in dom (S D^{n} F) (N)$
95	93 94	sseldd	$⊢ (φ \land k \in (0 \dots N)) \to B \in dom (S D^{n} F) (k)$
96	90 95	ffvelcdmd	$⊢ (φ \land k \in (0 \dots N)) \to (S D^{n} F) (k) (B) \in ℂ$
97	88	faccld	$⊢ (φ \land k \in (0 \dots N)) \to k! \in ℕ$
98	97	nncnd	$⊢ (φ \land k \in (0 \dots N)) \to k! \in ℂ$
99	97	nnne0d	$⊢ (φ \land k \in (0 \dots N)) \to k! \neq 0$
100	96 98 99	divcld	$⊢ (φ \land k \in (0 \dots N)) \to \frac{(S D^{n} F) (k) (B)}{k!} \in ℂ$
101	42 4 100 33	dgrle	$⊢ φ \to \deg ((y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k})) \leq N$
102	84 101	eqbrtrd	$⊢ φ \to \deg (T) \leq N$
103	69 102	jca	$⊢ φ \to (T \in Poly (D) \land \deg (T) \leq N)$

Metamath Proof Explorer

Theorem taylply2

Proof