taylfval

Description: Define the Taylor polynomial of a function. The constant Tayl is a function of five arguments: S is the base set with respect to evaluate the derivatives (generally RR or CC ), F is the function we are approximating, at point B , to order N . The result is a polynomial function of x .

This "extended" version of taylpfval additionally handles the case N = +oo , in which case this is not a polynomial but an infinite series, the Taylor series 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	taylfval	⊢ ( 𝜑 → 𝑇 = ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) )

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		df-tayl	⊢ Tayl = ( 𝑠 ∈ { ℝ , ℂ } , 𝑓 ∈ ( ℂ ↑_pm 𝑠 ) ↦ ( 𝑛 ∈ ( ℕ₀ ∪ { +∞ } ) , 𝑎 ∈ ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑘 ) ↦ ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) ) ) )
8	7	a1i	⊢ ( 𝜑 → Tayl = ( 𝑠 ∈ { ℝ , ℂ } , 𝑓 ∈ ( ℂ ↑_pm 𝑠 ) ↦ ( 𝑛 ∈ ( ℕ₀ ∪ { +∞ } ) , 𝑎 ∈ ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑘 ) ↦ ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) ) ) ) )
9		eqidd	⊢ ( ( 𝜑 ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( ℕ₀ ∪ { +∞ } ) = ( ℕ₀ ∪ { +∞ } ) )
10		oveq12	⊢ ( ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) → ( 𝑠 D^𝑛 𝑓 ) = ( 𝑆 D^𝑛 𝐹 ) )
11	10	ad2antlr	⊢ ( ( ( 𝜑 ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ) → ( 𝑠 D^𝑛 𝑓 ) = ( 𝑆 D^𝑛 𝐹 ) )
12	11	fveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ) → ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑘 ) = ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) )
13	12	dmeqd	⊢ ( ( ( 𝜑 ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ) → dom ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑘 ) = dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) )
14	13	iineq2dv	⊢ ( ( 𝜑 ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑘 ) = ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) )
15	12	fveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ) → ( ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑘 ) ‘ 𝑎 ) = ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝑎 ) )
16	15	oveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ) → ( ( ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) = ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) )
17	16	oveq1d	⊢ ( ( ( 𝜑 ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ) → ( ( ( ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) = ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) )
18	17	mpteq2dva	⊢ ( ( 𝜑 ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) = ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) )
19	18	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) = ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) )
20	19	xpeq2d	⊢ ( ( 𝜑 ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) ) = ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) ) )
21	20	iuneq2d	⊢ ( ( 𝜑 ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) ) = ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) ) )
22	9 14 21	mpoeq123dv	⊢ ( ( 𝜑 ∧ ( 𝑠 = 𝑆 ∧ 𝑓 = 𝐹 ) ) → ( 𝑛 ∈ ( ℕ₀ ∪ { +∞ } ) , 𝑎 ∈ ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑘 ) ↦ ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑠 D^𝑛 𝑓 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) ) ) = ( 𝑛 ∈ ( ℕ₀ ∪ { +∞ } ) , 𝑎 ∈ ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ↦ ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) ) ) )
23		simpr	⊢ ( ( 𝜑 ∧ 𝑠 = 𝑆 ) → 𝑠 = 𝑆 )
24	23	oveq2d	⊢ ( ( 𝜑 ∧ 𝑠 = 𝑆 ) → ( ℂ ↑_pm 𝑠 ) = ( ℂ ↑_pm 𝑆 ) )
25		cnex	⊢ ℂ ∈ V
26	25	a1i	⊢ ( 𝜑 → ℂ ∈ V )
27		elpm2r	⊢ ( ( ( ℂ ∈ V ∧ 𝑆 ∈ { ℝ , ℂ } ) ∧ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) ) → 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) )
28	26 1 2 3 27	syl22anc	⊢ ( 𝜑 → 𝐹 ∈ ( ℂ ↑_pm 𝑆 ) )
29		nn0ex	⊢ ℕ₀ ∈ V
30		snex	⊢ { +∞ } ∈ V
31	29 30	unex	⊢ ( ℕ₀ ∪ { +∞ } ) ∈ V
32		0xr	⊢ 0 ∈ ℝ^*
33		nn0ssre	⊢ ℕ₀ ⊆ ℝ
34		ressxr	⊢ ℝ ⊆ ℝ^*
35	33 34	sstri	⊢ ℕ₀ ⊆ ℝ^*
36		pnfxr	⊢ +∞ ∈ ℝ^*
37		snssi	⊢ ( +∞ ∈ ℝ^* → { +∞ } ⊆ ℝ^* )
38	36 37	ax-mp	⊢ { +∞ } ⊆ ℝ^*
39	35 38	unssi	⊢ ( ℕ₀ ∪ { +∞ } ) ⊆ ℝ^*
40	39	sseli	⊢ ( 𝑛 ∈ ( ℕ₀ ∪ { +∞ } ) → 𝑛 ∈ ℝ^* )
41		elun	⊢ ( 𝑛 ∈ ( ℕ₀ ∪ { +∞ } ) ↔ ( 𝑛 ∈ ℕ₀ ∨ 𝑛 ∈ { +∞ } ) )
42		nn0ge0	⊢ ( 𝑛 ∈ ℕ₀ → 0 ≤ 𝑛 )
43		0lepnf	⊢ 0 ≤ +∞
44		elsni	⊢ ( 𝑛 ∈ { +∞ } → 𝑛 = +∞ )
45	43 44	breqtrrid	⊢ ( 𝑛 ∈ { +∞ } → 0 ≤ 𝑛 )
46	42 45	jaoi	⊢ ( ( 𝑛 ∈ ℕ₀ ∨ 𝑛 ∈ { +∞ } ) → 0 ≤ 𝑛 )
47	41 46	sylbi	⊢ ( 𝑛 ∈ ( ℕ₀ ∪ { +∞ } ) → 0 ≤ 𝑛 )
48		lbicc2	⊢ ( ( 0 ∈ ℝ^* ∧ 𝑛 ∈ ℝ^* ∧ 0 ≤ 𝑛 ) → 0 ∈ ( 0 [,] 𝑛 ) )
49	32 40 47 48	mp3an2i	⊢ ( 𝑛 ∈ ( ℕ₀ ∪ { +∞ } ) → 0 ∈ ( 0 [,] 𝑛 ) )
50		0z	⊢ 0 ∈ ℤ
51		inelcm	⊢ ( ( 0 ∈ ( 0 [,] 𝑛 ) ∧ 0 ∈ ℤ ) → ( ( 0 [,] 𝑛 ) ∩ ℤ ) ≠ ∅ )
52	49 50 51	sylancl	⊢ ( 𝑛 ∈ ( ℕ₀ ∪ { +∞ } ) → ( ( 0 [,] 𝑛 ) ∩ ℤ ) ≠ ∅ )
53		fvex	⊢ ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ∈ V
54	53	dmex	⊢ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ∈ V
55	54	rgenw	⊢ ∀ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ∈ V
56		iinexg	⊢ ( ( ( ( 0 [,] 𝑛 ) ∩ ℤ ) ≠ ∅ ∧ ∀ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ∈ V ) → ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ∈ V )
57	52 55 56	sylancl	⊢ ( 𝑛 ∈ ( ℕ₀ ∪ { +∞ } ) → ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ∈ V )
58	57	rgen	⊢ ∀ 𝑛 ∈ ( ℕ₀ ∪ { +∞ } ) ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ∈ V
59		eqid	⊢ ( 𝑛 ∈ ( ℕ₀ ∪ { +∞ } ) , 𝑎 ∈ ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ↦ ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) ) ) = ( 𝑛 ∈ ( ℕ₀ ∪ { +∞ } ) , 𝑎 ∈ ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ↦ ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) ) )
60	59	mpoexxg	⊢ ( ( ( ℕ₀ ∪ { +∞ } ) ∈ V ∧ ∀ 𝑛 ∈ ( ℕ₀ ∪ { +∞ } ) ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ∈ V ) → ( 𝑛 ∈ ( ℕ₀ ∪ { +∞ } ) , 𝑎 ∈ ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ↦ ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) ) ) ∈ V )
61	31 58 60	mp2an	⊢ ( 𝑛 ∈ ( ℕ₀ ∪ { +∞ } ) , 𝑎 ∈ ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ↦ ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) ) ) ∈ V
62	61	a1i	⊢ ( 𝜑 → ( 𝑛 ∈ ( ℕ₀ ∪ { +∞ } ) , 𝑎 ∈ ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ↦ ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) ) ) ∈ V )
63	8 22 24 1 28 62	ovmpodx	⊢ ( 𝜑 → ( 𝑆 Tayl 𝐹 ) = ( 𝑛 ∈ ( ℕ₀ ∪ { +∞ } ) , 𝑎 ∈ ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ↦ ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) ) ) )
64		simprl	⊢ ( ( 𝜑 ∧ ( 𝑛 = 𝑁 ∧ 𝑎 = 𝐵 ) ) → 𝑛 = 𝑁 )
65	64	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑛 = 𝑁 ∧ 𝑎 = 𝐵 ) ) → ( 0 [,] 𝑛 ) = ( 0 [,] 𝑁 ) )
66	65	ineq1d	⊢ ( ( 𝜑 ∧ ( 𝑛 = 𝑁 ∧ 𝑎 = 𝐵 ) ) → ( ( 0 [,] 𝑛 ) ∩ ℤ ) = ( ( 0 [,] 𝑁 ) ∩ ℤ ) )
67		simprr	⊢ ( ( 𝜑 ∧ ( 𝑛 = 𝑁 ∧ 𝑎 = 𝐵 ) ) → 𝑎 = 𝐵 )
68	67	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑛 = 𝑁 ∧ 𝑎 = 𝐵 ) ) → ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝑎 ) = ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) )
69	68	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑛 = 𝑁 ∧ 𝑎 = 𝐵 ) ) → ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) = ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) )
70	67	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑛 = 𝑁 ∧ 𝑎 = 𝐵 ) ) → ( 𝑥 − 𝑎 ) = ( 𝑥 − 𝐵 ) )
71	70	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑛 = 𝑁 ∧ 𝑎 = 𝐵 ) ) → ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) = ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) )
72	69 71	oveq12d	⊢ ( ( 𝜑 ∧ ( 𝑛 = 𝑁 ∧ 𝑎 = 𝐵 ) ) → ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) = ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) )
73	66 72	mpteq12dv	⊢ ( ( 𝜑 ∧ ( 𝑛 = 𝑁 ∧ 𝑎 = 𝐵 ) ) → ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) = ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) )
74	73	oveq2d	⊢ ( ( 𝜑 ∧ ( 𝑛 = 𝑁 ∧ 𝑎 = 𝐵 ) ) → ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) = ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) )
75	74	xpeq2d	⊢ ( ( 𝜑 ∧ ( 𝑛 = 𝑁 ∧ 𝑎 = 𝐵 ) ) → ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) ) = ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) )
76	75	iuneq2d	⊢ ( ( 𝜑 ∧ ( 𝑛 = 𝑁 ∧ 𝑎 = 𝐵 ) ) → ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝑎 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝑎 ) ↑ 𝑘 ) ) ) ) ) = ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) )
77		simpr	⊢ ( ( 𝜑 ∧ 𝑛 = 𝑁 ) → 𝑛 = 𝑁 )
78	77	oveq2d	⊢ ( ( 𝜑 ∧ 𝑛 = 𝑁 ) → ( 0 [,] 𝑛 ) = ( 0 [,] 𝑁 ) )
79	78	ineq1d	⊢ ( ( 𝜑 ∧ 𝑛 = 𝑁 ) → ( ( 0 [,] 𝑛 ) ∩ ℤ ) = ( ( 0 [,] 𝑁 ) ∩ ℤ ) )
80		iineq1	⊢ ( ( ( 0 [,] 𝑛 ) ∩ ℤ ) = ( ( 0 [,] 𝑁 ) ∩ ℤ ) → ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) = ∩ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) )
81	79 80	syl	⊢ ( ( 𝜑 ∧ 𝑛 = 𝑁 ) → ∩ 𝑘 ∈ ( ( 0 [,] 𝑛 ) ∩ ℤ ) dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) = ∩ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) )
82		pnfex	⊢ +∞ ∈ V
83	82	elsn2	⊢ ( 𝑁 ∈ { +∞ } ↔ 𝑁 = +∞ )
84	83	orbi2i	⊢ ( ( 𝑁 ∈ ℕ₀ ∨ 𝑁 ∈ { +∞ } ) ↔ ( 𝑁 ∈ ℕ₀ ∨ 𝑁 = +∞ ) )
85	4 84	sylibr	⊢ ( 𝜑 → ( 𝑁 ∈ ℕ₀ ∨ 𝑁 ∈ { +∞ } ) )
86		elun	⊢ ( 𝑁 ∈ ( ℕ₀ ∪ { +∞ } ) ↔ ( 𝑁 ∈ ℕ₀ ∨ 𝑁 ∈ { +∞ } ) )
87	85 86	sylibr	⊢ ( 𝜑 → 𝑁 ∈ ( ℕ₀ ∪ { +∞ } ) )
88	5	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) 𝐵 ∈ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) )
89		oveq2	⊢ ( 𝑛 = 𝑁 → ( 0 [,] 𝑛 ) = ( 0 [,] 𝑁 ) )
90	89	ineq1d	⊢ ( 𝑛 = 𝑁 → ( ( 0 [,] 𝑛 ) ∩ ℤ ) = ( ( 0 [,] 𝑁 ) ∩ ℤ ) )
91	90	neeq1d	⊢ ( 𝑛 = 𝑁 → ( ( ( 0 [,] 𝑛 ) ∩ ℤ ) ≠ ∅ ↔ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ≠ ∅ ) )
92	91 52	vtoclga	⊢ ( 𝑁 ∈ ( ℕ₀ ∪ { +∞ } ) → ( ( 0 [,] 𝑁 ) ∩ ℤ ) ≠ ∅ )
93	87 92	syl	⊢ ( 𝜑 → ( ( 0 [,] 𝑁 ) ∩ ℤ ) ≠ ∅ )
94		r19.2z	⊢ ( ( ( ( 0 [,] 𝑁 ) ∩ ℤ ) ≠ ∅ ∧ ∀ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) 𝐵 ∈ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ) → ∃ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) 𝐵 ∈ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) )
95	93 88 94	syl2anc	⊢ ( 𝜑 → ∃ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) 𝐵 ∈ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) )
96		elex	⊢ ( 𝐵 ∈ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) → 𝐵 ∈ V )
97	96	rexlimivw	⊢ ( ∃ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) 𝐵 ∈ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) → 𝐵 ∈ V )
98		eliin	⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ ∩ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) 𝐵 ∈ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ) )
99	95 97 98	3syl	⊢ ( 𝜑 → ( 𝐵 ∈ ∩ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ↔ ∀ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) 𝐵 ∈ dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ) )
100	88 99	mpbird	⊢ ( 𝜑 → 𝐵 ∈ ∩ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) dom ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) )
101		snssi	⊢ ( 𝑥 ∈ ℂ → { 𝑥 } ⊆ ℂ )
102	1 2 3 4 5	taylfvallem	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ⊆ ℂ )
103		xpss12	⊢ ( ( { 𝑥 } ⊆ ℂ ∧ ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ⊆ ℂ ) → ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ⊆ ( ℂ × ℂ ) )
104	101 102 103	syl2an2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ⊆ ( ℂ × ℂ ) )
105	104	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ⊆ ( ℂ × ℂ ) )
106		iunss	⊢ ( ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ⊆ ( ℂ × ℂ ) ↔ ∀ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ⊆ ( ℂ × ℂ ) )
107	105 106	sylibr	⊢ ( 𝜑 → ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ⊆ ( ℂ × ℂ ) )
108	25 25	xpex	⊢ ( ℂ × ℂ ) ∈ V
109	108	ssex	⊢ ( ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ⊆ ( ℂ × ℂ ) → ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ∈ V )
110	107 109	syl	⊢ ( 𝜑 → ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ∈ V )
111	63 76 81 87 100 110	ovmpodx	⊢ ( 𝜑 → ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 ) = ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) )
112	6 111	syl5eq	⊢ ( 𝜑 → 𝑇 = ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂ_fld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) )

Metamath Proof Explorer

Theorem taylfval

Proof