Theorem taylf

Description: The Taylor series defines a function on a subset of the complex numbers. (Contributed by Mario Carneiro, 30-Dec-2016)

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

Proof

Step	Hyp	Ref	Expression
1		taylfval.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		taylfval.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
3		taylfval.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
4		taylfval.n	⊢ ( 𝜑 → ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) )
5		taylfval.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → 𝐵 ∈ dom ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) )
6		taylfval.t	⊢ 𝑇 = ( 𝑁 ( 𝑆 Tayl 𝐹 ) 𝐵 )
7	1 2 3 4 5 6	taylfval	⊢ ( 𝜑 → 𝑇 = ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) )
8		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
9	8	snssd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → { 𝑥 } ⊆ ℂ )
10	1 2 3 4 5	taylfvallem	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ⊆ ℂ )
11		xpss12	⊢ ( ( { 𝑥 } ⊆ ℂ ∧ ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ⊆ ℂ ) → ( { 𝑥 } × ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ⊆ ( ℂ × ℂ ) )
12	9 10 11	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( { 𝑥 } × ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ⊆ ( ℂ × ℂ ) )
13	12	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ⊆ ( ℂ × ℂ ) )
14		iunss	⊢ ( ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ⊆ ( ℂ × ℂ ) ↔ ∀ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ⊆ ( ℂ × ℂ ) )
15	13 14	sylibr	⊢ ( 𝜑 → ∪ 𝑥 ∈ ℂ ( { 𝑥 } × ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ⊆ ( ℂ × ℂ ) )
16	7 15	eqsstrd	⊢ ( 𝜑 → 𝑇 ⊆ ( ℂ × ℂ ) )
17		relxp	⊢ Rel ( ℂ × ℂ )
18		relss	⊢ ( 𝑇 ⊆ ( ℂ × ℂ ) → ( Rel ( ℂ × ℂ ) → Rel 𝑇 ) )
19	16 17 18	mpisyl	⊢ ( 𝜑 → Rel 𝑇 )
20	1 2 3 4 5 6	eltayl	⊢ ( 𝜑 → ( 𝑥 𝑇 𝑦 ↔ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ) )
21	20	biimpd	⊢ ( 𝜑 → ( 𝑥 𝑇 𝑦 → ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ) )
22	21	alrimiv	⊢ ( 𝜑 → ∀ 𝑦 ( 𝑥 𝑇 𝑦 → ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ) )
23		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
24		cnring	⊢ ℂfld ∈ Ring
25		ringcmn	⊢ ( ℂfld ∈ Ring → ℂfld ∈ CMnd )
26	24 25	mp1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ℂfld ∈ CMnd )
27		cnfldtps	⊢ ℂfld ∈ TopSp
28	27	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ℂfld ∈ TopSp )
29		ovex	⊢ ( 0 [,] 𝑁 ) ∈ V
30	29	inex1	⊢ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ∈ V
31	30	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( ( 0 [,] 𝑁 ) ∩ ℤ ) ∈ V )
32	1 2 3 4 5	taylfvallem1	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) ∧ 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ) → ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ∈ ℂ )
33	32	fmpttd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) : ( ( 0 [,] 𝑁 ) ∩ ℤ ) ⟶ ℂ )
34		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
35	34	cnfldhaus	⊢ ( TopOpen ‘ ℂfld ) ∈ Haus
36	35	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( TopOpen ‘ ℂfld ) ∈ Haus )
37	23 26 28 31 33 34 36	haustsms	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ∃* 𝑦 𝑦 ∈ ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) )
38	37	ex	⊢ ( 𝜑 → ( 𝑥 ∈ ℂ → ∃* 𝑦 𝑦 ∈ ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) )
39		moanimv	⊢ ( ∃* 𝑦 ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ↔ ( 𝑥 ∈ ℂ → ∃* 𝑦 𝑦 ∈ ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) )
40	38 39	sylibr	⊢ ( 𝜑 → ∃* 𝑦 ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) )
41		moim	⊢ ( ∀ 𝑦 ( 𝑥 𝑇 𝑦 → ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) ) → ( ∃* 𝑦 ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂfld tsums ( 𝑘 ∈ ( ( 0 [,] 𝑁 ) ∩ ℤ ) ↦ ( ( ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑘 ) ‘ 𝐵 ) / ( ! ‘ 𝑘 ) ) · ( ( 𝑥 − 𝐵 ) ↑ 𝑘 ) ) ) ) ) → ∃* 𝑦 𝑥 𝑇 𝑦 ) )
42	22 40 41	sylc	⊢ ( 𝜑 → ∃* 𝑦 𝑥 𝑇 𝑦 )
43	42	alrimiv	⊢ ( 𝜑 → ∀ 𝑥 ∃* 𝑦 𝑥 𝑇 𝑦 )
44		dffun6	⊢ ( Fun 𝑇 ↔ ( Rel 𝑇 ∧ ∀ 𝑥 ∃* 𝑦 𝑥 𝑇 𝑦 ) )
45	19 43 44	sylanbrc	⊢ ( 𝜑 → Fun 𝑇 )
46	45	funfnd	⊢ ( 𝜑 → 𝑇 Fn dom 𝑇 )
47		rnss	⊢ ( 𝑇 ⊆ ( ℂ × ℂ ) → ran 𝑇 ⊆ ran ( ℂ × ℂ ) )
48	16 47	syl	⊢ ( 𝜑 → ran 𝑇 ⊆ ran ( ℂ × ℂ ) )
49		rnxpss	⊢ ran ( ℂ × ℂ ) ⊆ ℂ
50	48 49	sstrdi	⊢ ( 𝜑 → ran 𝑇 ⊆ ℂ )
51		df-f	⊢ ( 𝑇 : dom 𝑇 ⟶ ℂ ↔ ( 𝑇 Fn dom 𝑇 ∧ ran 𝑇 ⊆ ℂ ) )
52	46 50 51	sylanbrc	⊢ ( 𝜑 → 𝑇 : dom 𝑇 ⟶ ℂ )