tayl0

Description: The Taylor series is always defined at the basepoint, with value equal to the value of the function. (Contributed by Mario Carneiro, 30-Dec-2016)

	Ref	Expression
Hypotheses	taylfval.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	taylfval.f	$⊢ φ \to F : A ⟶ ℂ$
	taylfval.a	$⊢ φ \to A \subseteq S$
	taylfval.n	$⊢ φ \to (N \in ℕ_{0} \lor N = +∞)$
	taylfval.b	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to B \in dom (S D^{n} F) (k)$
	taylfval.t	$⊢ T = N (S Tayl F) B$
Assertion	tayl0	$⊢ φ \to (B \in dom T \land T (B) = F (B))$

Proof

Step	Hyp	Ref	Expression
1		taylfval.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
2		taylfval.f	$⊢ φ \to F : A ⟶ ℂ$
3		taylfval.a	$⊢ φ \to A \subseteq S$
4		taylfval.n	$⊢ φ \to (N \in ℕ_{0} \lor N = +∞)$
5		taylfval.b	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to B \in dom (S D^{n} F) (k)$
6		taylfval.t	$⊢ T = N (S Tayl F) B$
7		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
8	1 7	syl	$⊢ φ \to S \subseteq ℂ$
9	3 8	sstrd	$⊢ φ \to A \subseteq ℂ$
10		fveq2	$⊢ k = 0 \to (S D^{n} F) (k) = (S D^{n} F) (0)$
11	10	dmeqd	$⊢ k = 0 \to dom (S D^{n} F) (k) = dom (S D^{n} F) (0)$
12	11	eleq2d	$⊢ k = 0 \to (B \in dom (S D^{n} F) (k) \leftrightarrow B \in dom (S D^{n} F) (0))$
13	5	ralrimiva	$⊢ φ \to \forall k \in ([0, N] \cap ℤ) B \in dom (S D^{n} F) (k)$
14		elxnn0	$⊢ N \in ℕ_{0}^{*} \leftrightarrow (N \in ℕ_{0} \lor N = +∞)$
15		0xr	$⊢ 0 \in ℝ^{*}$
16	15	a1i	$⊢ N \in ℕ_{0}^{} \to 0 \in ℝ^{}$
17		xnn0xr	$⊢ N \in ℕ_{0}^{} \to N \in ℝ^{}$
18		xnn0ge0	$⊢ N \in ℕ_{0}^{*} \to 0 \leq N$
19		lbicc2	$⊢ (0 \in ℝ^{} \land N \in ℝ^{} \land 0 \leq N) \to 0 \in [0, N]$
20	16 17 18 19	syl3anc	$⊢ N \in ℕ_{0}^{*} \to 0 \in [0, N]$
21	14 20	sylbir	$⊢ (N \in ℕ_{0} \lor N = +∞) \to 0 \in [0, N]$
22	4 21	syl	$⊢ φ \to 0 \in [0, N]$
23		0zd	$⊢ φ \to 0 \in ℤ$
24	22 23	elind	$⊢ φ \to 0 \in ([0, N] \cap ℤ)$
25	12 13 24	rspcdva	$⊢ φ \to B \in dom (S D^{n} F) (0)$
26		cnex	$⊢ ℂ \in V$
27	26	a1i	$⊢ φ \to ℂ \in V$
28		elpm2r	$⊢ ((ℂ \in V \land S \in \{ℝ, ℂ\}) \land (F : A ⟶ ℂ \land A \subseteq S)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
29	27 1 2 3 28	syl22anc	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} S)$
30		dvn0	$⊢ (S \subseteq ℂ \land F \in (ℂ ↑_{𝑝𝑚} S)) \to (S D^{n} F) (0) = F$
31	8 29 30	syl2anc	$⊢ φ \to (S D^{n} F) (0) = F$
32	31	dmeqd	$⊢ φ \to dom (S D^{n} F) (0) = dom F$
33	2	fdmd	$⊢ φ \to dom F = A$
34	32 33	eqtrd	$⊢ φ \to dom (S D^{n} F) (0) = A$
35	25 34	eleqtrd	$⊢ φ \to B \in A$
36	9 35	sseldd	$⊢ φ \to B \in ℂ$
37		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
38		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
39		cnring	$⊢ ℂ_{fld} \in Ring$
40		ringmnd	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in Mnd$
41	39 40	mp1i	$⊢ φ \to ℂ_{fld} \in Mnd$
42		ovex	$⊢ [0, N] \in V$
43	42	inex1	$⊢ [0, N] \cap ℤ \in V$
44	43	a1i	$⊢ φ \to [0, N] \cap ℤ \in V$
45	1	adantr	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to S \in \{ℝ, ℂ\}$
46	29	adantr	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to F \in (ℂ ↑_{𝑝𝑚} S)$
47		simpr	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to k \in ([0, N] \cap ℤ)$
48	47	elin2d	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to k \in ℤ$
49	47	elin1d	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to k \in [0, N]$
50		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
51	50	rexrd	$⊢ N \in ℕ_{0} \to N \in ℝ^{*}$
52		id	$⊢ N = +∞ \to N = +∞$
53		pnfxr	$⊢ +∞ \in ℝ^{*}$
54	52 53	eqeltrdi	$⊢ N = +∞ \to N \in ℝ^{*}$
55	51 54	jaoi	$⊢ (N \in ℕ_{0} \lor N = +∞) \to N \in ℝ^{*}$
56	4 55	syl	$⊢ φ \to N \in ℝ^{*}$
57	56	adantr	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to N \in ℝ^{*}$
58		elicc1	$⊢ (0 \in ℝ^{} \land N \in ℝ^{}) \to (k \in [0, N] \leftrightarrow (k \in ℝ^{*} \land 0 \leq k \land k \leq N))$
59	15 57 58	sylancr	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to (k \in [0, N] \leftrightarrow (k \in ℝ^{*} \land 0 \leq k \land k \leq N))$
60	49 59	mpbid	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to (k \in ℝ^{*} \land 0 \leq k \land k \leq N)$
61	60	simp2d	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to 0 \leq k$
62		elnn0z	$⊢ k \in ℕ_{0} \leftrightarrow (k \in ℤ \land 0 \leq k)$
63	48 61 62	sylanbrc	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to k \in ℕ_{0}$
64		dvnf	$⊢ (S \in \{ℝ, ℂ\} \land F \in (ℂ ↑_{𝑝𝑚} S) \land k \in ℕ_{0}) \to (S D^{n} F) (k) : dom (S D^{n} F) (k) ⟶ ℂ$
65	45 46 63 64	syl3anc	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to (S D^{n} F) (k) : dom (S D^{n} F) (k) ⟶ ℂ$
66	65 5	ffvelrnd	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to (S D^{n} F) (k) (B) \in ℂ$
67	63	faccld	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to k! \in ℕ$
68	67	nncnd	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to k! \in ℂ$
69	67	nnne0d	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to k! \neq 0$
70	66 68 69	divcld	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to \frac{(S D^{n} F) (k) (B)}{k!} \in ℂ$
71		0cnd	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to 0 \in ℂ$
72	71 63	expcld	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to 0^{k} \in ℂ$
73	70 72	mulcld	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k} \in ℂ$
74	73	fmpttd	$⊢ φ \to (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k}) : [0, N] \cap ℤ ⟶ ℂ$
75		eldifi	$⊢ k \in (([0, N] \cap ℤ) ∖ \{0\}) \to k \in ([0, N] \cap ℤ)$
76	75 63	sylan2	$⊢ (φ \land k \in (([0, N] \cap ℤ) ∖ \{0\})) \to k \in ℕ_{0}$
77		eldifsni	$⊢ k \in (([0, N] \cap ℤ) ∖ \{0\}) \to k \neq 0$
78	77	adantl	$⊢ (φ \land k \in (([0, N] \cap ℤ) ∖ \{0\})) \to k \neq 0$
79		elnnne0	$⊢ k \in ℕ \leftrightarrow (k \in ℕ_{0} \land k \neq 0)$
80	76 78 79	sylanbrc	$⊢ (φ \land k \in (([0, N] \cap ℤ) ∖ \{0\})) \to k \in ℕ$
81	80	0expd	$⊢ (φ \land k \in (([0, N] \cap ℤ) ∖ \{0\})) \to 0^{k} = 0$
82	81	oveq2d	$⊢ (φ \land k \in (([0, N] \cap ℤ) ∖ \{0\})) \to (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k} = (\frac{(S D^{n} F) (k) (B)}{k!}) \cdot 0$
83	70	mul01d	$⊢ (φ \land k \in ([0, N] \cap ℤ)) \to (\frac{(S D^{n} F) (k) (B)}{k!}) \cdot 0 = 0$
84	75 83	sylan2	$⊢ (φ \land k \in (([0, N] \cap ℤ) ∖ \{0\})) \to (\frac{(S D^{n} F) (k) (B)}{k!}) \cdot 0 = 0$
85	82 84	eqtrd	$⊢ (φ \land k \in (([0, N] \cap ℤ) ∖ \{0\})) \to (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k} = 0$
86		zex	$⊢ ℤ \in V$
87	86	inex2	$⊢ [0, N] \cap ℤ \in V$
88	87	a1i	$⊢ φ \to [0, N] \cap ℤ \in V$
89	85 88	suppss2	$⊢ φ \to (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k}) supp 0 \subseteq \{0\}$
90	37 38 41 44 24 74 89	gsumpt	$⊢ φ \to \underset{k \in [0, N] \cap ℤ}{\sum_{ℂ_{fld}}} (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k} = (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k}) (0)$
91	10	fveq1d	$⊢ k = 0 \to (S D^{n} F) (k) (B) = (S D^{n} F) (0) (B)$
92		fveq2	$⊢ k = 0 \to k! = 0!$
93		fac0	$⊢ 0! = 1$
94	92 93	eqtrdi	$⊢ k = 0 \to k! = 1$
95	91 94	oveq12d	$⊢ k = 0 \to \frac{(S D^{n} F) (k) (B)}{k!} = \frac{(S D^{n} F) (0) (B)}{1}$
96		oveq2	$⊢ k = 0 \to 0^{k} = 0^{0}$
97		0exp0e1	$⊢ 0^{0} = 1$
98	96 97	eqtrdi	$⊢ k = 0 \to 0^{k} = 1$
99	95 98	oveq12d	$⊢ k = 0 \to (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k} = (\frac{(S D^{n} F) (0) (B)}{1}) \cdot 1$
100		eqid	$⊢ (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k}) = (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k})$
101		ovex	$⊢ (\frac{(S D^{n} F) (0) (B)}{1}) \cdot 1 \in V$
102	99 100 101	fvmpt	$⊢ 0 \in ([0, N] \cap ℤ) \to (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k}) (0) = (\frac{(S D^{n} F) (0) (B)}{1}) \cdot 1$
103	24 102	syl	$⊢ φ \to (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k}) (0) = (\frac{(S D^{n} F) (0) (B)}{1}) \cdot 1$
104	31	fveq1d	$⊢ φ \to (S D^{n} F) (0) (B) = F (B)$
105	104	oveq1d	$⊢ φ \to \frac{(S D^{n} F) (0) (B)}{1} = \frac{F (B)}{1}$
106	2 35	ffvelrnd	$⊢ φ \to F (B) \in ℂ$
107	106	div1d	$⊢ φ \to \frac{F (B)}{1} = F (B)$
108	105 107	eqtrd	$⊢ φ \to \frac{(S D^{n} F) (0) (B)}{1} = F (B)$
109	108	oveq1d	$⊢ φ \to (\frac{(S D^{n} F) (0) (B)}{1}) \cdot 1 = F (B) \cdot 1$
110	106	mulid1d	$⊢ φ \to F (B) \cdot 1 = F (B)$
111	109 110	eqtrd	$⊢ φ \to (\frac{(S D^{n} F) (0) (B)}{1}) \cdot 1 = F (B)$
112	90 103 111	3eqtrd	$⊢ φ \to \underset{k \in [0, N] \cap ℤ}{\sum_{ℂ_{fld}}} (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k} = F (B)$
113		ringcmn	$⊢ ℂ_{fld} \in Ring \to ℂ_{fld} \in CMnd$
114	39 113	mp1i	$⊢ φ \to ℂ_{fld} \in CMnd$
115		cnfldtps	$⊢ ℂ_{fld} \in TopSp$
116	115	a1i	$⊢ φ \to ℂ_{fld} \in TopSp$
117		mptexg	$⊢ [0, N] \cap ℤ \in V \to (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k}) \in V$
118	87 117	mp1i	$⊢ φ \to (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k}) \in V$
119		funmpt	$⊢ Fun (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k})$
120	119	a1i	$⊢ φ \to Fun (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k})$
121		c0ex	$⊢ 0 \in V$
122	121	a1i	$⊢ φ \to 0 \in V$
123		snfi	$⊢ \{0\} \in Fin$
124	123	a1i	$⊢ φ \to \{0\} \in Fin$
125		suppssfifsupp	$⊢ (((k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k}) \in V \land Fun (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k}) \land 0 \in V) \land (\{0\} \in Fin \land (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k}) supp 0 \subseteq \{0\})) \to {finSupp}_{0} ((k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k}))$
126	118 120 122 124 89 125	syl32anc	$⊢ φ \to {finSupp}_{0} ((k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k}))$
127	37 38 114 116 44 74 126	tsmsid	$⊢ φ \to \underset{k \in [0, N] \cap ℤ}{\sum_{ℂ_{fld}}} (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k} \in (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k}))$
128	112 127	eqeltrrd	$⊢ φ \to F (B) \in (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k}))$
129	36	subidd	$⊢ φ \to B - B = 0$
130	129	oveq1d	$⊢ φ \to {(B - B)}^{k} = 0^{k}$
131	130	oveq2d	$⊢ φ \to (\frac{(S D^{n} F) (k) (B)}{k!}) {(B - B)}^{k} = (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k}$
132	131	mpteq2dv	$⊢ φ \to (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(B - B)}^{k}) = (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k})$
133	132	oveq2d	$⊢ φ \to ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(B - B)}^{k}) = ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) 0^{k})$
134	128 133	eleqtrrd	$⊢ φ \to F (B) \in (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(B - B)}^{k}))$
135	1 2 3 4 5 6	eltayl	$⊢ φ \to (B T F (B) \leftrightarrow (B \in ℂ \land F (B) \in (ℂ_{fld} tsums (k \in ([0, N] \cap ℤ) ⟼ (\frac{(S D^{n} F) (k) (B)}{k!}) {(B - B)}^{k}))))$
136	36 134 135	mpbir2and	$⊢ φ \to B T F (B)$
137	1 2 3 4 5 6	taylf	$⊢ φ \to T : dom T ⟶ ℂ$
138		ffun	$⊢ T : dom T ⟶ ℂ \to Fun T$
139		funbrfv2b	$⊢ Fun T \to (B T F (B) \leftrightarrow (B \in dom T \land T (B) = F (B)))$
140	137 138 139	3syl	$⊢ φ \to (B T F (B) \leftrightarrow (B \in dom T \land T (B) = F (B)))$
141	136 140	mpbid	$⊢ φ \to (B \in dom T \land T (B) = F (B))$

Metamath Proof Explorer

Theorem tayl0

Proof