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) Avoid ax-mulf . (Revised by GG, 30-Apr-2025)

	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	40	sseld	$⊢ D \in SubRing (ℂ_{fld}) \to (u \in D \to u \in ℂ)$
57	56	a1dd	$⊢ D \in SubRing (ℂ_{fld}) \to (u \in D \to (v \in D \to u \in ℂ))$
58	57	3imp	$⊢ (D \in SubRing (ℂ_{fld}) \land u \in D \land v \in D) \to u \in ℂ$
59	40	sseld	$⊢ D \in SubRing (ℂ_{fld}) \to (v \in D \to v \in ℂ)$
60	59	a1d	$⊢ D \in SubRing (ℂ_{fld}) \to (u \in D \to (v \in D \to v \in ℂ))$
61	60	3imp	$⊢ (D \in SubRing (ℂ_{fld}) \land u \in D \land v \in D) \to v \in ℂ$
62		ovmpot	$⊢ (u \in ℂ \land v \in ℂ) \to u (x \in ℂ, y \in ℂ ⟼ x y) v = u v$
63	58 61 62	syl2anc	$⊢ (D \in SubRing (ℂ_{fld}) \land u \in D \land v \in D) \to u (x \in ℂ, y \in ℂ ⟼ x y) v = u v$
64		mpocnfldmul	$⊢ (x \in ℂ, y \in ℂ ⟼ x y) = \cdot_{ℂ_{fld}}$
65	64	subrgmcl	$⊢ (D \in SubRing (ℂ_{fld}) \land u \in D \land v \in D) \to u (x \in ℂ, y \in ℂ ⟼ x y) v \in D$
66	63 65	eqeltrrd	$⊢ (D \in SubRing (ℂ_{fld}) \land u \in D \land v \in D) \to u v \in D$
67	66	3expb	$⊢ (D \in SubRing (ℂ_{fld}) \land (u \in D \land v \in D)) \to u v \in D$
68	7 67	sylan	$⊢ (φ \land (u \in D \land v \in D)) \to u v \in D$
69		ax-1cn	$⊢ 1 \in ℂ$
70		cnfldneg	$⊢ 1 \in ℂ \to {inv}_{g} (ℂ_{fld}) (1) = - 1$
71	69 70	ax-mp	$⊢ {inv}_{g} (ℂ_{fld}) (1) = - 1$
72		eqid	$⊢ {inv}_{g} (ℂ_{fld}) = {inv}_{g} (ℂ_{fld})$
73	72	subginvcl	$⊢ (D \in SubGrp (ℂ_{fld}) \land 1 \in D) \to {inv}_{g} (ℂ_{fld}) (1) \in D$
74	51 45 73	syl2anc	$⊢ φ \to {inv}_{g} (ℂ_{fld}) (1) \in D$
75	71 74	eqeltrrid	$⊢ φ \to - 1 \in D$
76	47 49 55 68 75	plysub	$⊢ φ \to X^{p} -_{f} (ℂ \times \{B\}) \in Poly (D)$
77	42 76 55 68	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)$
78	38 77	eqeltrd	$⊢ φ \to T \in Poly (D)$
79	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\})))$
80		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}))$
81		eqid	$⊢ \deg (X^{p} -_{f} (ℂ \times \{B\})) = \deg (X^{p} -_{f} (ℂ \times \{B\}))$
82	80 81 42 76	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\}))$
83		eqid	$⊢ X^{p} -_{f} (ℂ \times \{B\}) = X^{p} -_{f} (ℂ \times \{B\})$
84	83	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\})$
85	23 84	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\})$
86	85	simp2d	$⊢ φ \to \deg (X^{p} -_{f} (ℂ \times \{B\})) = 1$
87	86	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$
88		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}$
89	42 88	syl	$⊢ φ \to \deg ((y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k})) \in ℕ_{0}$
90	89	nn0cnd	$⊢ φ \to \deg ((y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k})) \in ℂ$
91	90	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}))$
92	87 91	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}))$
93	79 82 92	3eqtrd	$⊢ φ \to \deg (T) = \deg ((y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k}))$
94		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
95		dvnf	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land k \in ℕ_{0}) \to (S D^{n} F) (k) : dom (S D^{n} F) (k) ⟶ ℂ$
96	1 15 94 95	syl2an3an	$⊢ (φ \land k \in (0 \dots N)) \to (S D^{n} F) (k) : dom (S D^{n} F) (k) ⟶ ℂ$
97		id	$⊢ k \in (0 \dots N) \to k \in (0 \dots N)$
98		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)$
99	1 15 97 98	syl2an3an	$⊢ (φ \land k \in (0 \dots N)) \to dom (S D^{n} F) (N) \subseteq dom (S D^{n} F) (k)$
100	5	adantr	$⊢ (φ \land k \in (0 \dots N)) \to B \in dom (S D^{n} F) (N)$
101	99 100	sseldd	$⊢ (φ \land k \in (0 \dots N)) \to B \in dom (S D^{n} F) (k)$
102	96 101	ffvelcdmd	$⊢ (φ \land k \in (0 \dots N)) \to (S D^{n} F) (k) (B) \in ℂ$
103	94	adantl	$⊢ (φ \land k \in (0 \dots N)) \to k \in ℕ_{0}$
104	103	faccld	$⊢ (φ \land k \in (0 \dots N)) \to k! \in ℕ$
105	104	nncnd	$⊢ (φ \land k \in (0 \dots N)) \to k! \in ℂ$
106	104	nnne0d	$⊢ (φ \land k \in (0 \dots N)) \to k! \neq 0$
107	102 105 106	divcld	$⊢ (φ \land k \in (0 \dots N)) \to \frac{(S D^{n} F) (k) (B)}{k!} \in ℂ$
108	42 4 107 33	dgrle	$⊢ φ \to \deg ((y \in ℂ ⟼ \sum_{k = 0}^{N} (\frac{(S D^{n} F) (k) (B)}{k!}) y^{k})) \leq N$
109	93 108	eqbrtrd	$⊢ φ \to \deg (T) \leq N$
110	78 109	jca	$⊢ φ \to (T \in Poly (D) \land \deg (T) \leq N)$

Metamath Proof Explorer

Theorem taylply2

Proof