Theorem tayl0 24335

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.)

Hypotheses

Ref	Expression
taylfval.s	⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
taylfval.f	⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
taylfval.a	⊢ (𝜑 → 𝐴 ⊆ 𝑆)
taylfval.n	⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞))
taylfval.b	⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))
taylfval.t	⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)

Assertion

Ref	Expression
tayl0	⊢ (𝜑 → (𝐵 ∈ dom 𝑇 ∧ (𝑇‘𝐵) = (𝐹‘𝐵)))

Distinct variable groups:   𝐵,𝑘   𝑘,𝐹   𝜑,𝑘   𝑘,𝑁   𝑆,𝑘

Allowed substitution hints:   𝐴(𝑘)   𝑇(𝑘)

Proof of Theorem tayl0

Step	Hyp	Ref	Expression
1		taylfval.a	. . . . 5 ⊢ (𝜑 → 𝐴 ⊆ 𝑆)
2		taylfval.s	. . . . . 6 ⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ})
3		recnprss 23887	. . . . . 6 ⊢ (𝑆 ∈ {ℝ, ℂ} → 𝑆 ⊆ ℂ)
4	2, 3	syl 17	. . . . 5 ⊢ (𝜑 → 𝑆 ⊆ ℂ)
5	1, 4	sstrd 3754	. . . 4 ⊢ (𝜑 → 𝐴 ⊆ ℂ)
6		fveq2 6353	. . . . . . . 8 ⊢ (𝑘 = 0 → ((𝑆 D𝑛 𝐹)‘𝑘) = ((𝑆 D𝑛 𝐹)‘0))
7	6	dmeqd 5481	. . . . . . 7 ⊢ (𝑘 = 0 → dom ((𝑆 D𝑛 𝐹)‘𝑘) = dom ((𝑆 D𝑛 𝐹)‘0))
8	7	eleq2d 2825	. . . . . 6 ⊢ (𝑘 = 0 → (𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘) ↔ 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘0)))
9		taylfval.b	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))
10	9	ralrimiva 3104	. . . . . 6 ⊢ (𝜑 → ∀𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))
11		taylfval.n	. . . . . . . 8 ⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞))
12		elxnn0 11577	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0* ↔ (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞))
13		0xr 10298	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ*
14	13	a1i 11	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0* → 0 ∈ ℝ*)
15		xnn0xr 11580	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0* → 𝑁 ∈ ℝ*)
16		xnn0ge0 12180	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0* → 0 ≤ 𝑁)
17		lbicc2 12501	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ* ∧ 𝑁 ∈ ℝ* ∧ 0 ≤ 𝑁) → 0 ∈ (0[,]𝑁))
18	14, 15, 16, 17	syl3anc 1477	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0* → 0 ∈ (0[,]𝑁))
19	12, 18	sylbir 225	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∨ 𝑁 = +∞) → 0 ∈ (0[,]𝑁))
20	11, 19	syl 17	. . . . . . 7 ⊢ (𝜑 → 0 ∈ (0[,]𝑁))
21		0zd 11601	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℤ)
22	20, 21	elind 3941	. . . . . 6 ⊢ (𝜑 → 0 ∈ ((0[,]𝑁) ∩ ℤ))
23	8, 10, 22	rspcdva 3455	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘0))
24		cnex 10229	. . . . . . . . . 10 ⊢ ℂ ∈ V
25	24	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → ℂ ∈ V)
26		taylfval.f	. . . . . . . . 9 ⊢ (𝜑 → 𝐹:𝐴⟶ℂ)
27		elpm2r 8043	. . . . . . . . 9 ⊢ (((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑pm 𝑆))
28	25, 2, 26, 1, 27	syl22anc 1478	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm 𝑆))
29		dvn0 23906	. . . . . . . 8 ⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ ↑pm 𝑆)) → ((𝑆 D𝑛 𝐹)‘0) = 𝐹)
30	4, 28, 29	syl2anc 696	. . . . . . 7 ⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘0) = 𝐹)
31	30	dmeqd 5481	. . . . . 6 ⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘0) = dom 𝐹)
32		fdm 6212	. . . . . . 7 ⊢ (𝐹:𝐴⟶ℂ → dom 𝐹 = 𝐴)
33	26, 32	syl 17	. . . . . 6 ⊢ (𝜑 → dom 𝐹 = 𝐴)
34	31, 33	eqtrd 2794	. . . . 5 ⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘0) = 𝐴)
35	23, 34	eleqtrd 2841	. . . 4 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
36	5, 35	sseldd 3745	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℂ)
37		cnfldbas 19972	. . . . . . 7 ⊢ ℂ = (Base‘ℂfld)
38		cnfld0 19992	. . . . . . 7 ⊢ 0 = (0g‘ℂfld)
39		cnring 19990	. . . . . . . 8 ⊢ ℂfld ∈ Ring
40		ringmnd 18776	. . . . . . . 8 ⊢ (ℂfld ∈ Ring → ℂfld ∈ Mnd)
41	39, 40	mp1i 13	. . . . . . 7 ⊢ (𝜑 → ℂfld ∈ Mnd)
42		ovex 6842	. . . . . . . . 9 ⊢ (0[,]𝑁) ∈ V
43	42	inex1 4951	. . . . . . . 8 ⊢ ((0[,]𝑁) ∩ ℤ) ∈ V
44	43	a1i 11	. . . . . . 7 ⊢ (𝜑 → ((0[,]𝑁) ∩ ℤ) ∈ V)
45	2	adantr 472	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑆 ∈ {ℝ, ℂ})
46	28	adantr 472	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐹 ∈ (ℂ ↑pm 𝑆))
47		simpr 479	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑘 ∈ ((0[,]𝑁) ∩ ℤ))
48	47	elin2d 3946	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑘 ∈ ℤ)
49	47	elin1d 3945	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑘 ∈ (0[,]𝑁))
50		nn0re 11513	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
51	50	rexrd 10301	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ*)
52		id 22	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑁 = +∞ → 𝑁 = +∞)
53		pnfxr 10304	. . . . . . . . . . . . . . . . . . . 20 ⊢ +∞ ∈ ℝ*
54	52, 53	syl6eqel 2847	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑁 = +∞ → 𝑁 ∈ ℝ*)
55	51, 54	jaoi 393	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 ∈ ℕ0 ∨ 𝑁 = +∞) → 𝑁 ∈ ℝ*)
56	11, 55	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ ℝ*)
57	56	adantr 472	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑁 ∈ ℝ*)
58		elicc1 12432	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ* ∧ 𝑁 ∈ ℝ*) → (𝑘 ∈ (0[,]𝑁) ↔ (𝑘 ∈ ℝ* ∧ 0 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)))
59	13, 57, 58	sylancr 698	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (𝑘 ∈ (0[,]𝑁) ↔ (𝑘 ∈ ℝ* ∧ 0 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁)))
60	49, 59	mpbid 222	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (𝑘 ∈ ℝ* ∧ 0 ≤ 𝑘 ∧ 𝑘 ≤ 𝑁))
61	60	simp2d 1138	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 0 ≤ 𝑘)
62		elnn0z 11602	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ0 ↔ (𝑘 ∈ ℤ ∧ 0 ≤ 𝑘))
63	48, 61, 62	sylanbrc 701	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑘 ∈ ℕ0)
64		dvnf 23909	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ {ℝ, ℂ} ∧ 𝐹 ∈ (ℂ ↑pm 𝑆) ∧ 𝑘 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑘):dom ((𝑆 D𝑛 𝐹)‘𝑘)⟶ℂ)
65	45, 46, 63, 64	syl3anc 1477	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → ((𝑆 D𝑛 𝐹)‘𝑘):dom ((𝑆 D𝑛 𝐹)‘𝑘)⟶ℂ)
66	65, 9	ffvelrnd 6524	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) ∈ ℂ)
67	63	faccld 13285	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (!‘𝑘) ∈ ℕ)
68	67	nncnd 11248	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (!‘𝑘) ∈ ℂ)
69	67	nnne0d 11277	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (!‘𝑘) ≠ 0)
70	66, 68, 69	divcld 11013	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℂ)
71		0cnd 10245	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 0 ∈ ℂ)
72	71, 63	expcld 13222	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (0↑𝑘) ∈ ℂ)
73	70, 72	mulcld 10272	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)) ∈ ℂ)
74		eqid 2760	. . . . . . . 8 ⊢ (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) = (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))
75	73, 74	fmptd 6549	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))):((0[,]𝑁) ∩ ℤ)⟶ℂ)
76		eldifi 3875	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0}) → 𝑘 ∈ ((0[,]𝑁) ∩ ℤ))
77	76, 63	sylan2 492	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0})) → 𝑘 ∈ ℕ0)
78		eldifsni 4466	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0}) → 𝑘 ≠ 0)
79	78	adantl 473	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0})) → 𝑘 ≠ 0)
80		elnnne0 11518	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℕ0 ∧ 𝑘 ≠ 0))
81	77, 79, 80	sylanbrc 701	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0})) → 𝑘 ∈ ℕ)
82	81	0expd 13238	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0})) → (0↑𝑘) = 0)
83	82	oveq2d 6830	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0})) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 0))
84	70	mul01d 10447	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 0) = 0)
85	76, 84	sylan2 492	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0})) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 0) = 0)
86	83, 85	eqtrd 2794	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0})) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)) = 0)
87		zex 11598	. . . . . . . . . 10 ⊢ ℤ ∈ V
88	87	inex2 4952	. . . . . . . . 9 ⊢ ((0[,]𝑁) ∩ ℤ) ∈ V
89	88	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((0[,]𝑁) ∩ ℤ) ∈ V)
90	86, 89	suppss2 7499	. . . . . . 7 ⊢ (𝜑 → ((𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) supp 0) ⊆ {0})
91	37, 38, 41, 44, 22, 75, 90	gsumpt 18581	. . . . . 6 ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))) = ((𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))‘0))
92	6	fveq1d 6355	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) = (((𝑆 D𝑛 𝐹)‘0)‘𝐵))
93		fveq2 6353	. . . . . . . . . . 11 ⊢ (𝑘 = 0 → (!‘𝑘) = (!‘0))
94		fac0 13277	. . . . . . . . . . 11 ⊢ (!‘0) = 1
95	93, 94	syl6eq 2810	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (!‘𝑘) = 1)
96	92, 95	oveq12d 6832	. . . . . . . . 9 ⊢ (𝑘 = 0 → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) = ((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1))
97		oveq2 6822	. . . . . . . . . 10 ⊢ (𝑘 = 0 → (0↑𝑘) = (0↑0))
98		0exp0e1 13079	. . . . . . . . . 10 ⊢ (0↑0) = 1
99	97, 98	syl6eq 2810	. . . . . . . . 9 ⊢ (𝑘 = 0 → (0↑𝑘) = 1)
100	96, 99	oveq12d 6832	. . . . . . . 8 ⊢ (𝑘 = 0 → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)) = (((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1) · 1))
101		ovex 6842	. . . . . . . 8 ⊢ (((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1) · 1) ∈ V
102	100, 74, 101	fvmpt 6445	. . . . . . 7 ⊢ (0 ∈ ((0[,]𝑁) ∩ ℤ) → ((𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))‘0) = (((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1) · 1))
103	22, 102	syl 17	. . . . . 6 ⊢ (𝜑 → ((𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))‘0) = (((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1) · 1))
104	30	fveq1d 6355	. . . . . . . . . 10 ⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘0)‘𝐵) = (𝐹‘𝐵))
105	104	oveq1d 6829	. . . . . . . . 9 ⊢ (𝜑 → ((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1) = ((𝐹‘𝐵) / 1))
106	26, 35	ffvelrnd 6524	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹‘𝐵) ∈ ℂ)
107	106	div1d 11005	. . . . . . . . 9 ⊢ (𝜑 → ((𝐹‘𝐵) / 1) = (𝐹‘𝐵))
108	105, 107	eqtrd 2794	. . . . . . . 8 ⊢ (𝜑 → ((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1) = (𝐹‘𝐵))
109	108	oveq1d 6829	. . . . . . 7 ⊢ (𝜑 → (((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1) · 1) = ((𝐹‘𝐵) · 1))
110	106	mulid1d 10269	. . . . . . 7 ⊢ (𝜑 → ((𝐹‘𝐵) · 1) = (𝐹‘𝐵))
111	109, 110	eqtrd 2794	. . . . . 6 ⊢ (𝜑 → (((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1) · 1) = (𝐹‘𝐵))
112	91, 103, 111	3eqtrd 2798	. . . . 5 ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))) = (𝐹‘𝐵))
113		ringcmn 18801	. . . . . . 7 ⊢ (ℂfld ∈ Ring → ℂfld ∈ CMnd)
114	39, 113	mp1i 13	. . . . . 6 ⊢ (𝜑 → ℂfld ∈ CMnd)
115		cnfldtps 22802	. . . . . . 7 ⊢ ℂfld ∈ TopSp
116	115	a1i 11	. . . . . 6 ⊢ (𝜑 → ℂfld ∈ TopSp)
117		mptexg 6649	. . . . . . . 8 ⊢ (((0[,]𝑁) ∩ ℤ) ∈ V → (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) ∈ V)
118	88, 117	mp1i 13	. . . . . . 7 ⊢ (𝜑 → (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) ∈ V)
119		funmpt 6087	. . . . . . . 8 ⊢ Fun (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))
120	119	a1i 11	. . . . . . 7 ⊢ (𝜑 → Fun (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))))
121		c0ex 10246	. . . . . . . 8 ⊢ 0 ∈ V
122	121	a1i 11	. . . . . . 7 ⊢ (𝜑 → 0 ∈ V)
123		snfi 8205	. . . . . . . 8 ⊢ {0} ∈ Fin
124	123	a1i 11	. . . . . . 7 ⊢ (𝜑 → {0} ∈ Fin)
125		suppssfifsupp 8457	. . . . . . 7 ⊢ ((((𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) ∈ V ∧ Fun (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) ∧ 0 ∈ V) ∧ ({0} ∈ Fin ∧ ((𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) supp 0) ⊆ {0})) → (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) finSupp 0)
126	118, 120, 122, 124, 90, 125	syl32anc 1485	. . . . . 6 ⊢ (𝜑 → (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) finSupp 0)
127	37, 38, 114, 116, 44, 75, 126	tsmsid 22164	. . . . 5 ⊢ (𝜑 → (ℂfld Σg (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))) ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))))
128	112, 127	eqeltrrd 2840	. . . 4 ⊢ (𝜑 → (𝐹‘𝐵) ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))))
129	36	subidd 10592	. . . . . . . 8 ⊢ (𝜑 → (𝐵 − 𝐵) = 0)
130	129	oveq1d 6829	. . . . . . 7 ⊢ (𝜑 → ((𝐵 − 𝐵)↑𝑘) = (0↑𝑘))
131	130	oveq2d 6830	. . . . . 6 ⊢ (𝜑 → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝐵 − 𝐵)↑𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))
132	131	mpteq2dv 4897	. . . . 5 ⊢ (𝜑 → (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝐵 − 𝐵)↑𝑘))) = (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))))
133	132	oveq2d 6830	. . . 4 ⊢ (𝜑 → (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝐵 − 𝐵)↑𝑘)))) = (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))))
134	128, 133	eleqtrrd 2842	. . 3 ⊢ (𝜑 → (𝐹‘𝐵) ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝐵 − 𝐵)↑𝑘)))))
135		taylfval.t	. . . 4 ⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵)
136	2, 26, 1, 11, 9, 135	eltayl 24333	. . 3 ⊢ (𝜑 → (𝐵𝑇(𝐹‘𝐵) ↔ (𝐵 ∈ ℂ ∧ (𝐹‘𝐵) ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝐵 − 𝐵)↑𝑘)))))))
137	36, 134, 136	mpbir2and 995	. 2 ⊢ (𝜑 → 𝐵𝑇(𝐹‘𝐵))
138	2, 26, 1, 11, 9, 135	taylf 24334	. . 3 ⊢ (𝜑 → 𝑇:dom 𝑇⟶ℂ)
139		ffun 6209	. . 3 ⊢ (𝑇:dom 𝑇⟶ℂ → Fun 𝑇)
140		funbrfv2b 6403	. . 3 ⊢ (Fun 𝑇 → (𝐵𝑇(𝐹‘𝐵) ↔ (𝐵 ∈ dom 𝑇 ∧ (𝑇‘𝐵) = (𝐹‘𝐵))))
141	138, 139, 140	3syl 18	. 2 ⊢ (𝜑 → (𝐵𝑇(𝐹‘𝐵) ↔ (𝐵 ∈ dom 𝑇 ∧ (𝑇‘𝐵) = (𝐹‘𝐵))))
142	137, 141	mpbid 222	1 ⊢ (𝜑 → (𝐵 ∈ dom 𝑇 ∧ (𝑇‘𝐵) = (𝐹‘𝐵)))

Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∧ w3a 1072   = wceq 1632   ∈ wcel 2139   ≠ wne 2932  Vcvv 3340   ∖ cdif 3712   ∩ cin 3714   ⊆ wss 3715  {csn 4321  {cpr 4323   class class class wbr 4804   ↦ cmpt 4881  dom cdm 5266  Fun wfun 6043  ⟶wf 6045  ‘cfv 6049  (class class class)co 6814   supp csupp 7464   ↑_pm cpm 8026  Fincfn 8123   finSupp cfsupp 8442  ℂcc 10146  ℝcr 10147  0cc0 10148  1c1 10149   · cmul 10153  +∞cpnf 10283  ℝ^*cxr 10285   ≤ cle 10287   − cmin 10478   / cdiv 10896  ℕcn 11232  ℕ₀cn0 11504  ℕ₀^*cxnn0 11575  ℤcz 11589  [,]cicc 12391  ↑cexp 13074  !cfa 13274   Σ_g cgsu 16323  Mndcmnd 17515  CMndccmn 18413  Ringcrg 18767  ℂ_fldccnfld 19968  TopSpctps 20958   tsums ctsu 22150   D^𝑛 cdvn 23847   Tayl ctayl 24326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115  ax-inf2 8713  ax-cnex 10204  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-mulcom 10212  ax-addass 10213  ax-mulass 10214  ax-distr 10215  ax-i2m1 10216  ax-1ne0 10217  ax-1rid 10218  ax-rnegex 10219  ax-rrecex 10220  ax-cnre 10221  ax-pre-lttri 10222  ax-pre-lttrn 10223  ax-pre-ltadd 10224  ax-pre-mulgt0 10225  ax-pre-sup 10226  ax-addf 10227  ax-mulf 10228

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-1st 7334  df-2nd 7335  df-supp 7465  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-1o 7730  df-oadd 7734  df-er 7913  df-map 8027  df-pm 8028  df-en 8124  df-dom 8125  df-sdom 8126  df-fin 8127  df-fsupp 8443  df-fi 8484  df-sup 8515  df-inf 8516  df-oi 8582  df-card 8975  df-pnf 10288  df-mnf 10289  df-xr 10290  df-ltxr 10291  df-le 10292  df-sub 10480  df-neg 10481  df-div 10897  df-nn 11233  df-2 11291  df-3 11292  df-4 11293  df-5 11294  df-6 11295  df-7 11296  df-8 11297  df-9 11298  df-n0 11505  df-xnn0 11576  df-z 11590  df-dec 11706  df-uz 11900  df-q 12002  df-rp 12046  df-xneg 12159  df-xadd 12160  df-xmul 12161  df-icc 12395  df-fz 12540  df-fzo 12680  df-seq 13016  df-exp 13075  df-fac 13275  df-hash 13332  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-struct 16081  df-ndx 16082  df-slot 16083  df-base 16085  df-sets 16086  df-ress 16087  df-plusg 16176  df-mulr 16177  df-starv 16178  df-tset 16182  df-ple 16183  df-ds 16186  df-unif 16187  df-rest 16305  df-topn 16306  df-0g 16324  df-gsum 16325  df-topgen 16326  df-mre 16468  df-mrc 16469  df-acs 16471  df-mgm 17463  df-sgrp 17505  df-mnd 17516  df-submnd 17557  df-grp 17646  df-minusg 17647  df-mulg 17762  df-cntz 17970  df-cmn 18415  df-abl 18416  df-mgp 18710  df-ur 18722  df-ring 18769  df-cring 18770  df-psmet 19960  df-xmet 19961  df-met 19962  df-bl 19963  df-mopn 19964  df-fbas 19965  df-fg 19966  df-cnfld 19969  df-top 20921  df-topon 20938  df-topsp 20959  df-bases 20972  df-cld 21045  df-ntr 21046  df-cls 21047  df-nei 21124  df-lp 21162  df-perf 21163  df-cnp 21254  df-haus 21341  df-fil 21871  df-fm 21963  df-flim 21964  df-flf 21965  df-tsms 22151  df-xms 22346  df-ms 22347  df-limc 23849  df-dv 23850  df-dvn 23851  df-tayl 24328

This theorem is referenced by:  dvntaylp0  24345