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	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	taylfval.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
	taylfval.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
	taylfval.n	⊢ ( 𝜑 → ( 𝑁 ∈ ℕ₀ ∨ 𝑁 = +∞ ) )
	taylfval.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝐵 ∈ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) )
	taylfval.t	⊢ 𝑇 = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 )
Assertion	tayl0	⊢ ( 𝜑 → ( 𝐵 ∈ dom 𝑇 ∧ ( 𝑇 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐵 ) ) )

Proof

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

Metamath Proof Explorer

Theorem tayl0

Proof